Bitwuzla

A bitwuzla::Bitwuzla instance is created from a configuration options bitwuzla::Options instance. This options instance must be configured before creating the Bitwuzla instance: after the Bitwuzla instance is created, configuration options are fixed and cannot be changed. bitwuzla::Sorts and bitwuzla::Terms are independent of a bitwuzla::Bitwuzla instance and can be shared across Bitwuzla instances.

Bitwuzla supports incremental solving via bitwuzla::Bitwuzla::push() and bitwuzla::Bitwuzla::pop(); querying the solver for the current set of assertions via bitwuzla::Bitwuzla::get_assertions(), model values via bitwuzla::Bitwuzla::get_value(), the unsat core via bitwuzla::Bitwuzla::get_unsat_core(), and unsat assumptions via bitwuzla::Bitwuzla::get_unsat_assumptions(); and printing the currently asserted formula via bitwuzla::Bitwuzla::print_formula(). The current statistics can be retrieved as a mapping from statistic names to values via bitwuzla::Bitwuzla::statistics().

Bitwuzla further supports configuring a termination callback via bitwuzla::Terminator, which implements a callback function bitwuzla::Terminator::terminate() to allow terminating Bitwuzla prematurely, during solving. This termination callback returns a bool to indicate if Bitwuzla should be terminated. Bitwuzla periodically checks this callback and terminates at the earliest possible opportunity if the callback function returns true.

namespace bitwuzla {

class Bitwuzla

The Bitwuzla solver instance.

Public Functions

Bitwuzla(TermManager &tm, const Options &options = Options())

Constructor.

Parameters:

  • tm – The associated term manager instance.

  • options – The associated options instance. Options must be configured at this point.

Bitwuzla(const Options &options = Options())

Constructor.

Note

: (deprecated) Uses the global thread-local term manager.

Parameters:

options – The associated options instance. Options must be configured at this point.

~Bitwuzla()

Destructor.

Bitwuzla(const Bitwuzla &bitwuzla) = delete

Disallow copy construction.

Bitwuzla &operator=(const Bitwuzla &bitwuzla) = delete

Disallow copy assignment.

void configure_terminator(Terminator *terminator)

Connect or disconnect associated termination configuration instance.

Note

Only one terminator can be connected at a time. This will disconnect a previously connected terminator before connecting a new one.

Parameters:

terminator – The terminator instance. Nullptr disconnects the currently associated terminator.

void push(uint32_t nlevels)

Push context levels.

See also

Parameters:

nlevels – The number of context levels to push.

void pop(uint32_t nlevels)

Pop context levels.

See also

Parameters:

nlevels – The number of context levels to pop.

void assert_formula(const Term &term)

Assert formula.

Parameters:

term – The formula to assert.

std::vector<Term> get_assertions()

Get the set of currently asserted formulas.

Returns:

The assertion formulas.

bool is_unsat_assumption(const Term &term)

Determine if an assumption is an unsat assumption.

Unsat assumptions are assumptions that force an input formula to become unsatisfiable. Unsat assumptions handling in Bitwuzla is analogous to failed assumptions in MiniSAT.

Requires that the last check_sat() query returned Result::UNSAT.

See also

Parameters:

term – The assumption to check for.

Returns:

True if given assumption is an unsat assumption.

std::vector<Term> get_unsat_assumptions()

Get the set of unsat assumptions.

Unsat assumptions are assumptions that force an input formula to become unsatisfiable. Unsat assumptions handling in Bitwuzla is analogous to failed assumptions in MiniSAT.

Requires that the last check_sat() query returned Result::UNSAT.

See also

Returns:

A vctor with unsat assumptions.

std::vector<Term> get_unsat_core()

Get the unsat core (unsat assertions).

The unsat core consists of the set of assertions that force an input formula to become unsatisfiable.

Requires that the last check_sat() query returned Result::UNSAT.

See also

Returns:

A vector with unsat assertions.

void simplify()

Simplify the current input formula.

See also

Note

Each call to Bitwuzla::check_sat() simplifies the input formula as a preprocessing step. It is not necessary to call this function explicitly in the general case.

Result check_sat(const std::vector<Term> &assumptions = {})

Check satisfiability of current input formula.

An input formula consists of assertions added via assert_formula(). The search for a solution can by guided by making assumptions via passing a vector of assumptions to check_sat().

See also

Note

Assertions and assumptions are combined via Boolean and.

Returns:

Result::SAT if the input formula is satisfiable and Result::UNSAT if it is unsatisfiable, and Result::UNKNOWN when neither satisfiability nor unsatisfiability was determined. This can happen when this Bitwuzla instance was terminated via a termination callback.

Term get_value(const Term &term)

Get a term representing the model value of a given term.

Requires that the last check_sat() query returned Result::SAT.

See also

check_sat()

Parameters:

term – The term to query a model value for.

Returns:

A term representing the model value of term term.

void print_formula(std::ostream &out, const std::string &format = "smt2") const

Print the current input formula to the given output stream.

Parameters:

  • out – The output stream.

  • format – The output format for printing the formula. Currently, only "smt2" for the SMT-LIB v2 format is supported.

std::map<std::string, std::string> statistics() const

Get current statistics.

Returns:

A map of strings of statistics entries, maps statistic name to value.

TermManager &term_mgr()
Returns:

The associated term manager instance.

}