The Bitwuzla solver.

configure_terminator t f configure a termination callback function.

If terminator has been connected, Bitwuzla calls this function periodically to determine if the connected instance should be terminated.

• parameter t

  The Bitwuzla instance.

• parameter f

  The callback function, returns true if t should be terminated.

create options create a new Bitwuzla instance.

The returned instance can be deleted earlier via unsafe_delete.

• parameter options

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

• returns

  The created Bitwuzla instance.

push t nlevels push context levels.

• parameter t

  The Bitwuzla instance.

• parameter nlevels

  The number of context levels to push.

pop t nlevels pop context levels.

• parameter t

  The Bitwuzla instance.

• parameter nlevels

  The number of context levels to pop.

mk_assert t term assert formula.

• parameter t

  The Bitwuzla instance.

• parameter term

  The formula to assert.

get_assertions t get the set of currently asserted formulas.

• returns

  The assertion formulas.

pp_formula formatter t print the current input formula.

• parameter formatter

  The output formatter.

• parameter t

  The Bitwuzla instance.

simplify t simplify the current input formula.

• parameter t

  The Bitwuzla instance.

check_sat ~assumptions t 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 assumptions.

Assertions and assumptions are combined via Boolean and.

• parameter t

  The Bitwuzla instance.

• returns

  Sat if the input formula is satisfiable and Unsat if it is unsatisfiable, and Unknown when neither satisfiability nor unsatisfiability was determined. This can happen when t was terminated via a termination callback.

get_value t term get a term representing the model value of a given term.

Requires that the last check_sat query returned Sat.

• parameter t

  The Bitwuzla instance.

• parameter term

  The term to query a model value for.

• returns

  A term representing the model value of term term.

is_unsat_assumption t 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 unsat assumption generation has been enabled via Options.set.

Requires that the last check_sat query returned Unsat.

• parameter t

  The Bitwuzla instance.

• parameter term

  The assumption to check for.

• returns

  true if given assumption is an unsat assumption.

get_unsat_assumptions t 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 unsat assumption generation has been enabled via Options.set.

Requires that the last check_sat query returned Unsat.

• parameter t

  The Bitwuzla instance.

• returns

  An array with unsat assumptions.

get_unsat_core t get the set unsat core (unsat assertions).

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

Requires that unsat core generation has been enabled via Options.set.

Requires that the last check_sat query returned Unsat.

• parameter t

  The Bitwuzla instance.

• returns

  An array with unsat assertions.

Expert

delete t delete a Bitwuzla instance.

UNSAFE: call this ONLY to release the resources earlier if the instance is about to be garbage collected.

• parameter t

  The Bitwuzla instance to delete.