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(TermManager &tm, SatSolverFactory &sat_factory, const Options &options = Options())

Constructor for configuration with external SAT solver factory.

Warning

This constructor is experimental and may change in future versions.

Parameters:

  • tm – The associated term manager instance.

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

  • sat_factory – The associated SAT solver factory.

~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.

Term simplify(const Term &term)

Simplify the given term.

See also

Note

Each call to Bitwuzla::check_sat() simplifies the input formula as a preprocessing step.

Parameters:

term – The term to simplify.

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.

Term get_interpolant(const std::vector<Term> &A)

Get a term representing the interpolant I given the current set of assertions, partitioned into partitions A and B such that (and A B) is unsat and (=> A I) and (=> I (not B)).

Partition A is the given set of assertions, partition B consists of the remaining assertions that are not in A.

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

See also

check_sat()

Note

Assertions in A and B must be currently asserted formulas.

Warning

The signature of this function is experimental and may change in future versions.

Parameters:

A – The set of formulas representing partition A. This must be a strict subset of the set of current assertions.

Returns:

Interpolant I such that (=> A I) and (=> I (not B)).

std::vector<Term> get_interpolants(const std::vector<std::vector<Term>> &A)

Get an inductive sequence of interpolants \(\langle I_1, \ldots, I_n \rangle\) given the current set of assertions \(F\) and a sequence of partitions.

The sequence of partitions is given as a list of set increments \(\{A_1, \ldots, A_n\}\) of asserted formulas \(F = \{F_1, F_2, \ldots, F_n\}\), which expands into sets of partitions

\[\{(A_1, B_1), (A_2, B_2), \ldots, (A_n, B_n)\}\]

such that

\[\begin{split}A_1 &= F_1 \\ A_2 &= F_1\,\cup\,F_2 \\ \ldots & \\ A_n & = F_1\,\cup\,F_2\,\cup\,\ldots\,\cup\,F_n \\\end{split}\]

and

\[B_i = F \setminus A_i \text{ with } A_i \wedge B_i \models \bot.\]

The resulting sequence of interpolants is inductive, i.e., it holds that \((I_i \wedge F_{i+1}) \rightarrow I_{i+1}\).

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

See also

check_sat()

Note

Assertions in \(A_i\) must be currently asserted formulas.

Note

Current SAT state must be unsat.

Warning

The signature of this function is experimental and may change in future versions.

Parameters:

A – The set of A increments.

Returns:

The interpolation sequence.

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.

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

Print the current unsat core as benchmark to the given output stream.

Requires that the last check_sat() query returned Result::UNSAT and unsat cores are enabled.

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.

}