Bitwuzla

A Bitwuzla instance is created from a configuration options BitwuzlaOptions 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. BitwuzlaSorts and BitwuzlaTerms are independent of a Bitwuzla instance and can be shared across Bitwuzla instances.

A Bitwuzla instance is created via bitwuzla_new() and must be released via bitwuzla_delete().

Bitwuzla supports incremental solving via bitwuzla_push() and bitwuzla_pop(); querying the solver for the current set of assertions via bitwuzla_get_assertions(), model values via bitwuzla_get_value(), the unsat core via bitwuzla_get_unsat_core(), and unsat assumptions via bitwuzla_get_unsat_assumptions(); and printing the currently asserted formula via bitwuzla_print_formula(). The current statistics can be retrieved as a mapping from statistic names to values via bitwuzla_get_statistics().

Bitwuzla further supports configuring a termination callback via bitwuzla_set_termination_callback(), which allows to terminate Bitwuzla prematurely, during solving. This termination callback returns a int32_t to indicate if Bitwuzla should be terminated. Bitwuzla periodically checks this callback and terminates at the earliest possible opportunity if the callback function returns a value != 0.

typedef struct Bitwuzla Bitwuzla

The Bitwuzla solver.

Bitwuzla *bitwuzla_new(BitwuzlaTermManager *tm, const BitwuzlaOptions *options)

Create a new Bitwuzla instance.

The returned instance must be deleted via bitwuzla_delete().

See also

Parameters:

  • tm – The associated term manager instance.

  • options – The associated options (optional).

Returns:

A pointer to the created Bitwuzla instance.

void bitwuzla_delete(Bitwuzla *bitwuzla)

Delete a Bitwuzla instance.

The given instance must have been created via bitwuzla_new().

See also

Parameters:

bitwuzla – The Bitwuzla instance to delete.

void bitwuzla_set_termination_callback(Bitwuzla *bitwuzla, int32_t (*fun)(void*), void *state)

Configure a termination callback function.

The state of the callback can be retrieved via bitwuzla_get_termination_callback_state().

See also

Parameters:

  • bitwuzla – The Bitwuzla instance.

  • fun – The callback function, returns a value != 0 if bitwuzla should be terminated.

  • state – The argument to the callback function.

void *bitwuzla_get_termination_callback_state(Bitwuzla *bitwuzla)

Get the state of the termination callback function.

The returned object representing the state of the callback corresponds to the state configured as argument to the callback function via bitwuzla_set_termination_callback().

See also

Parameters:

bitwuzla – The Bitwuzla instance.

Returns:

The object passed as argument state to the callback function.

void bitwuzla_set_abort_callback(void (*fun)(const char *msg))

Configure an abort callback function, which is called instead of exit on abort conditions.

Note

If the abort callback function throws a C++ exception, this must be thrown via std::rethrow_if_nested.

Parameters:

fun – The callback function. Argument msg explains the reason for the abort.

void bitwuzla_push(Bitwuzla *bitwuzla, uint64_t nlevels)

Push context levels.

See also

Parameters:

  • bitwuzla – The Bitwuzla instance.

  • nlevels – The number of context levels to push.

void bitwuzla_pop(Bitwuzla *bitwuzla, uint64_t nlevels)

Pop context levels.

See also

Parameters:

  • bitwuzla – The Bitwuzla instance.

  • nlevels – The number of context levels to pop.

void bitwuzla_assert(Bitwuzla *bitwuzla, BitwuzlaTerm term)

Assert formula.

Parameters:

  • bitwuzla – The Bitwuzla instance.

  • term – The formula to assert.

BitwuzlaTerm *bitwuzla_get_assertions(Bitwuzla *bitwuzla, size_t *size)

Get the set of currently asserted formulas.

Returns:

The asserted formulas.

Returns:

An array with the set of asserted formulas of size size. Only valid until the next bitwuzla_get_assertions call.

bool bitwuzla_is_unsat_assumption(Bitwuzla *bitwuzla, BitwuzlaTerm 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 bitwuzla_check_sat() query returned BITWUZLA_UNSAT.

See also

Parameters:

  • bitwuzla – The Bitwuzla instance.

  • term – The assumption to check for.

Returns:

True if given assumption is an unsat assumption.

BitwuzlaTerm *bitwuzla_get_unsat_assumptions(Bitwuzla *bitwuzla, size_t *size)

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 bitwuzla_check_sat() query returned BITWUZLA_UNSAT.

See also

Parameters:

  • bitwuzla – The Bitwuzla instance.

  • size – Output parameter, stores the size of the returned array.

Returns:

An array with unsat assumptions of size size. Only valid until the next bitwuzla_get_unsat_assumptions call.

BitwuzlaTerm *bitwuzla_get_unsat_core(Bitwuzla *bitwuzla, size_t *size)

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 bitwuzla_check_sat() query returned BITWUZLA_UNSAT.

See also

Parameters:

  • bitwuzla – The Bitwuzla instance.

  • size – Output parameter, stores the size of the returned array.

Returns:

An array with unsat assertions of size size. Only valid until the next bitwuzla_get_unsat_core call.

void bitwuzla_simplify(Bitwuzla *bitwuzla)

Simplify the current input formula.

See also

Note

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

Parameters:

bitwuzla – The Bitwuzla instance.

BitwuzlaResult bitwuzla_check_sat(Bitwuzla *bitwuzla)

Check satisfiability of current input formula.

An input formula consists of assertions added via bitwuzla_assert(). The search for a solution can by guided by additionally making assumptions (see bitwuzla_check_sat_assuming).

See also

Note

Assertions and assumptions are combined via Boolean and.

Parameters:

bitwuzla – The Bitwuzla instance.

Returns:

BITWUZLA_SAT if the input formula is satisfiable and BITWUZLA_UNSAT if it is unsatisfiable, and BITWUZLA_UNKNOWN when neither satisfiability nor unsatisfiability was determined. This can happen when bitwuzla was terminated via a termination callback.

BitwuzlaResult bitwuzla_check_sat_assuming(Bitwuzla *bitwuzla, uint32_t argc, BitwuzlaTerm args[])

Check satisfiability of current input formula wrt to the given set of assumptions.

An input formula consists of assertions added via bitwuzla_assert(). The search for a solution can by guided by additionally making assumptions (the given set of assumptions args).

See also

Note

Assertions and assumptions are combined via Boolean and.

Parameters:

  • bitwuzla – The Bitwuzla instance.

  • argc – The number of assumptions in args.

  • args – The assumptions.

Returns:

BITWUZLA_SAT if the input formula is satisfiable and BITWUZLA_UNSAT if it is unsatisfiable, and BITWUZLA_UNKNOWN when neither satisfiability nor unsatisfiability was determined. This can happen when bitwuzla was terminated via a termination callback.

BitwuzlaTerm bitwuzla_get_value(Bitwuzla *bitwuzla, BitwuzlaTerm term)

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

Requires that the last bitwuzla_check_sat() query returned BITWUZLA_SAT.

See also

bitwuzla_check_sat

Parameters:

  • bitwuzla – The Bitwuzla instance.

  • term – The term to query a model value for.

Returns:

A term representing the model value of term term.

void bitwuzla_print_formula(Bitwuzla *bitwuzla, const char *format, FILE *file, uint8_t base)

Print the current input formula.

Note

Floating-point values are printed in terms of operator fp. Their component bit-vector values can only be printed in binary or decimal format. If base 16 is configured, the format for floating-point component bit-vector values defaults to binary format.

Parameters:

  • bitwuzla – The Bitwuzla instance.

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

  • file – The file to print the formula to.

  • base – The base of the string representation of bit-vector values; 2 for binary, 10 for decimal, and 16 for hexadecimal.

void bitwuzla_get_statistics(Bitwuzla *bitwuzla, const char ***keys, const char ***values, size_t *size)

Get current statistics.

The statistics are retrieved as a mapping from statistic name (keys) to statistic value (values).

Note

Output parameters keys and values are only valid until the next call to bitwuzla_get_statistics().

Parameters:

  • bitwuzla – The Bitwuzla instance.

  • keys – The resulting set of statistic names.

  • values – The resulting set of statistic values.

  • size – The resulting size of keys and values.

BitwuzlaTermManager *bitwuzla_get_term_mgr(Bitwuzla *bitwuzla)

Get term manager instance.

Parameters:

bitwuzla – The bitwuzla instance.

Returns:

Term manager instance used by given Bitwuzla instance.