C Interface¶

Macros¶

BOOLECTOR_PARSE_ERROR¶: Preprocessor constant representing status parse error.

See also

boolector_parse()

BOOLECTOR_PARSE_UNKNOWN¶: Preprocessor constant representing status parse unknown.

See also

boolector_parse()

BOOLECTOR_SAT¶: Preprocessor constant representing status satisfiable.

See also

boolector_sat(), boolector_limited_sat(), boolector_simplify()

BOOLECTOR_UNKNOWN¶: Preprocessor constant representing status unknown.

See also

boolector_sat(), boolector_limited_sat(), boolector_simplify()

BOOLECTOR_UNSAT¶: Preprocessor constant representing status unsatisfiable.

See also

boolector_sat(), boolector_limited_sat(), boolector_simplify()

Typedefs¶

Functions¶

BoolectorNode *boolector_add(Btor *btor, BoolectorNode *n0, BoolectorNode *n1)¶

Create bit-vector addition.

The parameters n0 and n1 must have the same bit width.

Parameters

btor – Boolector instance.
n0 – First bit-vector operand.
n1 – Second bit-vector operand.

Returns

Bit-vector addition with the same bit width as the operands.

BoolectorNode *boolector_and(Btor *btor, BoolectorNode *n0, BoolectorNode *n1)¶

Create a bit-vector and.

The parameters n0 and n1 must have the same bit width.

Parameters

btor – Boolector instance.
n0 – First bit-vector operand.
n1 – Second bit-vector operand.

Returns

Bit-vector with the same bit width as the operands.

BoolectorNode *boolector_apply(Btor *btor, BoolectorNode **arg_nodes, uint32_t argc, BoolectorNode *n_fun)¶

Create a function application on function n_fun with arguments arg_nodes.

Parameters

btor – Boolector instance.
arg_nodes – Arguments to be applied.
argc – Number of arguments to be applied.
n_fun – Function expression.

Returns

Function application on function n_fun with arguments arg_nodes.

See also

boolector_fun(), boolector_uf()

BoolectorNode *boolector_array(Btor *btor, BoolectorSort sort, const char *symbol)¶

Create a one-dimensional bit-vector array with sort sort.

An array variable’s symbol is used as a simple means of identification, either when printing a model via boolector_print_model(), or generating file dumps via boolector_dump_btor() and boolector_dump_smt2(). A symbol must be unique but may be NULL in case that no symbol should be assigned.

Parameters

btor – Boolector instance.
sort – Array sort which maps bit-vectors to bit-vectors.
symbol – Name of array variable.

Returns

Bit-vector array of sort sort and with symbol symbol.

Note

In contrast to composite expressions, which are maintained uniquely w.r.t. to their kind, inputs (and consequently, bit width), array variables are not. Hence, each call to boolector_array() with the same arguments will return a fresh array variable.

void boolector_array_assignment(Btor *btor, BoolectorNode *n_array, char ***indices, char ***values, uint32_t *size)¶

Generate a model for an array expression.

If boolector_sat() has returned BOOLECTOR_SAT and model generation has been enabled. The function creates and stores the array of indices into indices and the array of corresponding values into values. The number size of indices resp. values is stored into size. The array model simply inspects the set of reads rho, which is associated with each array expression. See our publication Lemmas on Demand for Lambdas for details. At indices that do not occur in the model, it is assumed that the array stores a globally unique default value, for example 0. If the model of a constant array is queried the default value of the constant array is indicated via index ‘*’. The bit-vector assignments to the indices and values have to be freed by boolector_free_bv_assignment(). Furthermore, the user has to free the array of indices and the array of values, respectively of size size.

Parameters

btor – Boolector instance.
n_array – Array operand for which the array model should be built.
indices – Pointer to array of index strings. The string representation will use binary, decimal or hexadecimal number format, depending on the configuration of option BTOR_OPT_OUTPUT_NUMBER_FORMAT (binary by default).
values – Pointer to array of value strings. The string representation will use binary, decimal or hexadecimal number format, depending on the configuration of option BTOR_OPT_OUTPUT_NUMBER_FORMAT (binary by default).
size – Pointer to size.

See also

boolector_set_opt() for enabling model generation.

BoolectorSort boolector_array_sort(Btor *btor, BoolectorSort index, BoolectorSort element)¶

Create array sort.

Parameters

btor – Boolector instance.
index – Index sort of array.
element – Element sort of array.

Returns

Array sort which maps sort index to sort element.

See also

boolector_array()

void boolector_assert(Btor *btor, BoolectorNode *node)¶

Add a constraint.

Use this function to assert node. Added constraints can not be deleted anymore. After node has been asserted, it can be safely released by boolector_release().

Parameters

btor – Boolector instance.
node – Bit-vector expression with bit width one.

void boolector_assume(Btor *btor, BoolectorNode *node)¶

Add an assumption.

Use this function to assume node. You must enable Boolector’s incremental usage via boolector_set_opt() before you can add assumptions. In contrast to assertions added via boolector_assert(), assumptions are discarded after each call to boolector_sat(). Assumptions and assertions are logically combined via Boolean and. Assumption handling in Boolector is analogous to assumptions in MiniSAT.

Parameters

btor – Boolector instance.
node – Bit-vector expression with bit width one.

BoolectorSort boolector_bitvec_sort(Btor *btor, uint32_t width)¶

Create bit-vector sort of bit width width.

Parameters

btor – Boolector instance.
width – Bit width.

Returns

Bit-vector sort of bit width width.

See also

boolector_var(), boolector_param()

uint32_t boolector_bitvec_sort_get_width(Btor *btor, BoolectorSort sort)¶

Get the bit width of a bit-vector sort.

Parameters

btor – Boolector instance.
node – Boolector sort.

Returns

Bit width of sort.

BoolectorSort boolector_bool_sort(Btor *btor)¶

Create Boolean sort.

Parameters

btor – Boolector instance.

Returns

Sort of type Boolean.

See also

boolector_var(), boolector_param()

const char *boolector_bv_assignment(Btor *btor, BoolectorNode *node)¶

Generate an assignment string for bit-vector expression if boolector_sat() has returned BOOLECTOR_SAT and model generation has been enabled.

The expression can be an arbitrary bit-vector expression which occurs in an assertion or current assumption. The assignment string has to be freed by boolector_free_bv_assignment().

Parameters

btor – Boolector instance.
node – Bit-vector expression.

Returns

String representing a satisfying assignment to bit-vector variables and a consistent assignment for arbitrary bit-vector expressions. The string representation will use binary, decimal or hexadecimal number format, depending on the configuration of option BTOR_OPT_OUTPUT_NUMBER_FORMAT (binary by default).

See also

boolector_set_opt() for enabling model generation.

Btor *boolector_clone(Btor *btor)¶

Clone an instance of Boolector.

The resulting Boolector instance is an exact copy of given Boolector instance btor. Consequently, in a clone and its parent, nodes with the same id correspond to each other. Use boolector_match_node() to match corresponding nodes.

Parameters

btor – Original Boolector instance.

Returns

The exact (but disjunct) copy of the Boolector instance btor.

Note

If Lingeling is used as SAT solver, Boolector can be cloned at any time, since Lingeling also supports cloning. However, with all other SAT solver that do not support cloning, Boolector can only be cloned prior to the first boolector_sat() call.

BoolectorNode *boolector_concat(Btor *btor, BoolectorNode *n0, BoolectorNode *n1)¶

Create the concatenation of two bit-vectors.

Parameters

btor – Boolector instance.
n0 – First bit-vector operand.
n1 – Second bit-vector operand.

Returns

Bit-vector with the bit width bit width of n0 + bit width of n1.

BoolectorNode *boolector_cond(Btor *btor, BoolectorNode *n_cond, BoolectorNode *n_then, BoolectorNode *n_else)¶

Create an if-then-else.

If condition n_cond is true, then n_then is returned, else n_else is returned. Nodes n_then and n_else must be either both arrays or both bit vectors.

Parameters

btor – Boolector instance.
n_cond – Bit-vector condition with bit width one.
n_then – Array or bit-vector operand representing the if case.
n_else – Array or bit-vector operand representing the else case.

Returns

Either n_then or n_else.

BoolectorNode *boolector_const(Btor *btor, const char *bits)¶

Create bit-vector constant representing the bit-vector bits.

Parameters

btor – Boolector instance.
bits – Non-empty and terminated string consisting of zeroes and/or ones representing the bit-vector constant specified by bits.

Returns

Bit-vector constant with bit width strlen (bits).

BoolectorNode *boolector_const_array(Btor *btor, BoolectorSort sort, BoolectorNode *value)¶

Create a one-dimensional constant bit-vector array with sort sort initialized with value value.

Parameters

btor – Boolector instance.
sort – Array sort which maps bit-vectors to bit-vectors.
value – Value to initialize array.

Returns

Constant bit-vector array of sort sort.

See also

boolector_array()

BoolectorNode *boolector_constd(Btor *btor, BoolectorSort sort, const char *str)¶

Create bit-vector constant representing the decimal number str.

Parameters

btor – Boolector instance.
sort – Bit-vector sort of ‘str’.
str – Non-empty and terminated string representing a negative or postive decimal number.

Returns

Bit-vector constant with sort sort.

BoolectorNode *boolector_consth(Btor *btor, BoolectorSort sort, const char *str)¶

Create bit-vector constant representing the hexadecimal number str.

Parameters

btor – Boolector instance.
sort – Bit-vector sort of ‘str’.
str – Non-empty and terminated string representing a hexadecimal number.

Returns

Bit-vector constant with sort sort.

BoolectorNode *boolector_copy(Btor *btor, BoolectorNode *node)¶

Copy expression (increments reference counter).

Parameters

btor – Boolector instance.
node – Boolector node to be copied.

Returns

Node node with reference counter incremented.

BoolectorSort boolector_copy_sort(Btor *btor, BoolectorSort sort)¶

Copy sort (increments reference counter).

Parameters

btor – Boolector instance.
sort – Sort to be copied.

Returns

Sort sort with reference counter incremented.

const char *boolector_copyright(Btor *btor)¶

Get Boolector’s copyright notice.

Parameters

btor – Boolector instance

Returns

A string with Boolector’s copyright notice.

BoolectorNode *boolector_dec(Btor *btor, BoolectorNode *node)¶

Create bit-vector expression that decrements bit-vector node by one.

Parameters

btor – Boolector instance.
node – Bit-vector operand.

Returns

Bit-vector with the same bit width as node decremented by one.

void boolector_delete(Btor *btor)¶

Delete a boolector instance and free its resources.

Parameters

btor – Boolector instance.

Note

Expressions that have not been released properly will not be deleted from memory. Use boolector_get_refs() to debug reference counting. You can also set option auto_cleanup via boolector_set_opt() in order to do the cleanup automatically.

void boolector_dump_aiger_ascii(Btor *btor, FILE *file, bool merge_roots)¶

Dumps bit-vector formula to file in ascii AIGER format.

Parameters

btor – Boolector instance
file – Output file.
merge_roots – Merge all roots of AIG.

void boolector_dump_aiger_binary(Btor *btor, FILE *file, bool merge_roots)¶

Dumps bit-vector formula to file in ascii AIGER format.

Parameters

btor – Boolector instance
file – Output file.
merge_roots – Merge all roots of AIG.

void boolector_dump_btor(Btor *btor, FILE *file)¶

Dump formula to file in BTOR format.

Parameters

btor – Boolector instance.
file – File to which the formula should be dumped. The file must be have been opened by the user before.

void boolector_dump_btor_node(Btor *btor, FILE *file, BoolectorNode *node)¶

Recursively dump node to file in BTOR format.

Parameters

btor – Boolector instance.
file – File to which the expression should be dumped. The file must be have been opened by the user before.
node – The expression which should be dumped.

void boolector_dump_smt2(Btor *btor, FILE *file)¶

Dumps formula to file in SMT-LIB v2 format.

Parameters

btor – Boolector instance
file – Output file.

void boolector_dump_smt2_node(Btor *btor, FILE *file, BoolectorNode *node)¶

Recursively dump node to file in SMT-LIB v2 format.

Parameters

btor – Boolector instance.
file – File to which the expression should be dumped. The file must be have been opened by the user before.
node – The expression which should be dumped.

BoolectorNode *boolector_eq(Btor *btor, BoolectorNode *n0, BoolectorNode *n1)¶

Create bit-vector or array equality.

Both operands are either bit-vectors with the same bit width or arrays of the same type.

Parameters

btor – Boolector instance.
n0 – First operand.
n1 – Second operand.

Returns

Bit-vector with bit width one.

BoolectorNode *boolector_exists(Btor *btor, BoolectorNode *param[], uint32_t paramc, BoolectorNode *body)¶

Create an existentially quantifed formula.

exists (params[0] … params[paramc - 1]) body

Parameters

btor – Boolector instance.
params – Array of quantified variables.
paramc – length of params array.
body – Term where params may occur.

Returns

Existentially quantified formula.

bool boolector_failed(Btor *btor, BoolectorNode *node)¶

Determine if assumption node is a failed assumption.

Failed assumptions are those assumptions, that force an input formula to become unsatisfiable. Failed assumptions handling in Boolector is analogous to failed assumptions in MiniSAT.

Parameters

btor – Boolector instance.
node – Bit-vector expression with bit width one.

Returns

true if assumption is failed, and false otherwise.

See also

boolector_assume()

BoolectorNode *boolector_false(Btor *btor)¶

Create bit-vector constant zero with bit width one.

Parameters

btor – Boolector instance.

Returns

Bit-vector constant zero with bit width one.

BtorOption boolector_first_opt(Btor *btor)¶

Get the opt of the first option in Boolector’s option list.

Given a Boolector instance btor, you can use this in combination with boolector_has_opt() and boolector_next_opt() in order to iterate over Boolector options as follows:

for (s = boolector_first_opt (btor);
     boolector_has_opt (btor, s);
     s = boolector_next_opt (btor, s))
  {...}

Parameters

btor – Btor instance.

Returns

opt of the first option in Boolector’s option list.

void boolector_fixate_assumptions(Btor *btor)¶

Add all assumptions as assertions.

Parameters

btor – Boolector instance.

See also

boolector_assume()

BoolectorNode *boolector_forall(Btor *btor, BoolectorNode *params[], uint32_t paramc, BoolectorNode *body)¶

Create a universally quantified formula.

forall (params[0] … params[paramc - 1]) body

Parameters

btor – Boolector instance.
params – Array of quantified variables.
paramc – length of params array.
body – Term where params may occur.

Returns

Universally quantified formula.

void boolector_free_array_assignment(Btor *btor, char **indices, char **values, uint32_t size)¶

Free an assignment string for arrays of bit-vectors.

Parameters

btor – Boolector instance.
indices – Array of index strings of size size.
values – Array of values strings of size size.
size – Size of arrays indices and values.

See also

boolector_array_assignment()

void boolector_free_bits(Btor *btor, const char *bits)¶

Free a bits string retrieved via boolector_get_bits().

Parameters

btor – Boolector instance.
bits – String which has to be freed.

See also

boolector_get_bits()

void boolector_free_bv_assignment(Btor *btor, const char *assignment)¶

Free an assignment string for bit-vectors.

Parameters

btor – Boolector instance.
assignment – String which has to be freed.

See also

boolector_bv_assignment()

void boolector_free_uf_assignment(Btor *btor, char **args, char **values, uint32_t size)¶

Free assignment strings for uninterpreted functions.

Parameters

btor – Boolector instance.
args – Array of argument strings of size size.
values – Array of value string of size size.
size – Size of arrays args and values.

See also

boolector_uf_assignment()

BoolectorNode *boolector_fun(Btor *btor, BoolectorNode **param_nodes, uint32_t paramc, BoolectorNode *node)¶

Create a function with body node parameterized over parameters param_nodes.

This kind of node is similar to macros in the SMT-LIB standard 2.0. Note that as soon as a parameter is bound to a function, it can not be reused in other functions. Call a function via boolector_apply().

Parameters

btor – Boolector instance.
param_nodes – Parameters of function.
paramc – Number of parameters.
node – Function body parameterized over param_nodes.

Returns

Function over parameterized expression node.

BoolectorSort boolector_fun_get_codomain_sort(Btor *btor, const BoolectorNode *node)¶

Get the codomain sort of given function node node. The result does not have to be released.

Parameters

btor – Boolector instance.
node – Boolector function node.

Returns

Codomain sort of function node.

BoolectorSort boolector_fun_get_domain_sort(Btor *btor, const BoolectorNode *node)¶

Get the domain sort of given function node node. The result does not have to be released.

Parameters

btor – Boolector instance.
node – Boolector function node.

Returns

Domain sort of function node.

BoolectorSort boolector_fun_sort(Btor *btor, BoolectorSort *domain, uint32_t arity, BoolectorSort codomain)¶

Create function sort.

Parameters

btor – Boolector instance.
domain – A list of all the function arguments’ sorts.
arity – Number of elements in domain (must be > 0).
codomain – The sort of the function’s return value.

Returns

Function sort which maps given domain to given codomain.

See also

boolector_uf()

int32_t boolector_fun_sort_check(Btor *btor, BoolectorNode **arg_nodes, uint32_t argc, BoolectorNode *n_fun)¶

Check if sorts of given arguments matches the function signature.

Parameters

btor – Boolector instance.
arg_nodes – Arguments to be checked.
argc – Number of arguments to be checked.
n_fun – Function expression.

Returns

-1 if all sorts are correct, otherwise it returns the position of the incorrect argument.

const char *boolector_get_bits(Btor *btor, BoolectorNode *node)¶

Get the bit-vector of a constant node represented as a bit string. Must be freed via boolector_free_bits().

Parameters

btor – Boolector instance.
node – Constant node.

Returns

String representing the bits of node.

See also

boolector_free_bits()

Btor *boolector_get_btor(BoolectorNode *node)¶

Return the Boolector instance to which node belongs.

Parameters

node – Boolector node.

Returns

Boolector instance.

BoolectorNode **boolector_get_failed_assumptions(Btor *btor)¶

Get all failed assumptions (see boolector_failed()).

Returns the list of failed assumptions in a zero-terminated array of pointers to BoolectorNodes. The nodes in this array do not have to be released. The memory allocated for this array is maintained by Boolector, it does not have to be freed.

Parameters

btor – Boolector instance.

Returns

A pointer to an array of pointers to BoolectorNodes.

uint32_t boolector_get_fun_arity(Btor *btor, BoolectorNode *node)¶

Get the arity of function node.

Parameters

btor – Boolector instance.
node – Function node.

Returns

Arity of node.

uint32_t boolector_get_index_width(Btor *btor, BoolectorNode *n_array)¶

Get the bit width of indices of n_array.

Parameters

btor – Boolector instance.
n_array – Array operand.

Returns

Bit width of indices of n_array

int32_t boolector_get_node_id(Btor *btor, BoolectorNode *node)¶

Get the id of a given node.

Parameters

btor – Boolector instance.
node – Boolector node.

Returns

Id of node.

uint32_t boolector_get_opt(Btor *btor, BtorOption opt)¶

Get the current value of an option.

Parameters

btor – Btor instance.
opt – Option opt.

Returns

Current value of opt.

const char *boolector_get_opt_desc(Btor *btor, BtorOption opt)¶

Get the description of an option.

Parameters

btor – Btor instance.
opt – Option opt.

Returns

Description of opt.

uint32_t boolector_get_opt_dflt(Btor *btor, BtorOption opt)¶

Get the default value of an option.

Parameters

btor – Btor instance.
opt – Option opt.

Returns

Default value of opt.

const char *boolector_get_opt_lng(Btor *btor, BtorOption opt)¶

Get the long name of an option.

Parameters

btor – Btor instance.
opt – Option opt.

Returns

Short opt of opt.

uint32_t boolector_get_opt_max(Btor *btor, BtorOption opt)¶

Get the max value of an option.

Parameters

btor – Btor instance.
opt – Option opt.

Returns

Max value of opt.

uint32_t boolector_get_opt_min(Btor *btor, BtorOption opt)¶

Get the min value of an option.

Parameters

btor – Btor instance.
opt – Option opt.

Returns

Min value of opt.

const char *boolector_get_opt_shrt(Btor *btor, BtorOption opt)¶

Get the short name of an option.

Parameters

btor – Btor instance.
opt – Option opt.

Returns

Short opt of opt.

uint32_t boolector_get_refs(Btor *btor)¶

Get the number of external references to the boolector library.

Internally, Boolector manages an expression DAG with reference counting. Use boolector_release() to properly release an expression. Before you finally call boolector_delete(), boolector_get_refs() should return 0.

Parameters

btor – Boolector instance.

Returns

Number of external references owned by the user.

BoolectorSort boolector_get_sort(Btor *btor, const BoolectorNode *node)¶

Get the sort of given node. The result does not have to be released.

Parameters

btor – Boolector instance.
node – Boolector node.

Returns

Sort of node.

const char *boolector_get_symbol(Btor *btor, BoolectorNode *node)¶

Get the symbol of an expression.

Parameters

btor – Boolector instance.
node – Boolector node.

Returns

Symbol of expression.

FILE *boolector_get_trapi(Btor *btor)¶

Return API trace file.

Parameters

btor – Boolector instance.

Returns

API trace output file.

uint32_t boolector_get_width(Btor *btor, BoolectorNode *node)¶

Get the bit width of an expression.

If the expression is an array, it returns the bit width of the array elements. If the expression is a function, it returns the bit width of the function’s return value.

Parameters

btor – Boolector instance.
node – Boolector node.

Returns

Bit width of node.

const char *boolector_git_id(Btor *btor)¶

Get Boolector’s git id string.

Parameters

btor – Boolector instance.

Returns

A string with Boolector’s git id.

bool boolector_has_opt(Btor *Btor, BtorOption opt)¶

Check if Boolector has a given option.

Given a Boolector instance btor, you can use this in combination with boolector_has_opt() and boolector_next_opt() in order to iterate over Boolector options as follows:

for (s = boolector_first_opt (btor);
     boolector_has_opt (btor, s);
     s = boolector_next_opt (btor, s))
  {...}

Parameters

btor – Btor instance.
opt – Option opt.

Returns

True if Boolector has the given option, and false otherwise.

BoolectorNode *boolector_iff(Btor *btor, BoolectorNode *n0, BoolectorNode *n1)¶

Create Boolean equivalence.

The parameters n0 and n1 must have bit width one.

Parameters

btor – Boolector instance.
n0 – First bit-vector operand.
n1 – Second bit-vector operand.

Returns

Equivalence n0 <=> n1 with bit width one.

BoolectorNode *boolector_implies(Btor *btor, BoolectorNode *n0, BoolectorNode *n1)¶

Create boolean implication.

The parameters n0 and n1 must have bit width one.

Parameters

btor – Boolector instance.
n0 – Bit-vector node representing the premise.
n1 – Bit-vector node representing the conclusion.

Returns

Implication n0 => n1 with bit width one.

BoolectorNode *boolector_inc(Btor *btor, BoolectorNode *node)¶

Create bit-vector expression that increments bit-vector node by one.

Parameters

btor – Boolector instance.
node – Bit-vector operand.

Returns

Bit-vector with the same bit width as node incremented by one.

BoolectorNode *boolector_int(Btor *btor, int32_t i, BoolectorSort sort)¶

Create bit-vector constant representing the signed integer i of sort sort.

The constant is obtained by either truncating bits or by signed extension (padding with ones).

Parameters

btor – Boolector instance.
i – Signed integer value.
sort – Sort of constant.

Returns

Bit-vector constant of sort sort.

bool boolector_is_array(Btor *btor, BoolectorNode *node)¶

Determine if given node is an array node.

Parameters

btor – Boolector instance.
node – Boolector node.

Returns

True if node is an array, and false otherwise.

bool boolector_is_array_sort(Btor *btor, BoolectorSort sort)¶

Determine if sort is an array sort.

Parameters

btor – Boolector instance.
sort – Sort.

Returns

True if sort is an array sort, and false otherwise.

bool boolector_is_array_var(Btor *btor, BoolectorNode *node)¶

Determine if given node is an array variable.

Parameters

btor – Boolector instance.
node – Boolector node.

Returns

True if node is an array variable, and false otherwise.

bool boolector_is_bitvec_sort(Btor *btor, BoolectorSort sort)¶

Determine if sort is a bit-vector sort.

Parameters

btor – Boolector instance.
sort – Sort.

Returns

True if sort is a bit-vector sort, and false otherwise.

bool boolector_is_bound_param(Btor *btor, BoolectorNode *node)¶

Determine if given parameter node is bound by a function.

Parameters

btor – Boolector instance.
node – Parameter node.

Returns

True if node is bound, and false otherwise.

bool boolector_is_bv_const_max_signed(Btor *btor, BoolectorNode *node)¶

Determine if given node is a bit-vector constant representing the maximum signed value (01…1).

Parameters

btor – Boolector instance.
node – Boolector node.

Returns

True if node is a bit-vector constant representing the maximum signed value, and false otherwise.

bool boolector_is_bv_const_min_signed(Btor *btor, BoolectorNode *node)¶

Determine if given node is a bit-vector constant representing the minimum signed value (10…0).

Parameters

btor – Boolector instance.
node – Boolector node.

Returns

True if node is a bit-vector constant representing the minimum signed value, and false otherwise.

bool boolector_is_bv_const_one(Btor *btor, BoolectorNode *node)¶

Determine if given node is a bit-vector constant representing one.

Parameters

btor – Boolector instance.
node – Boolector node.

Returns

True if node is a bit-vector constant representing one, and false otherwise.

bool boolector_is_bv_const_ones(Btor *btor, BoolectorNode *node)¶

Determine if given node is a bit-vector constant representing the maximum unsigned value (all ones)..

Parameters

btor – Boolector instance.
node – Boolector node.

Returns

True if node is a bit-vector constant with all ones, and false otherwise.

bool boolector_is_bv_const_zero(Btor *btor, BoolectorNode *node)¶

Determine if given node is a bit-vector constant representing zero.

Parameters

btor – Boolector instance.
node – Boolector node.

Returns

True if node is a bit-vector constant representing zero, and false otherwise.

bool boolector_is_const(Btor *btor, BoolectorNode *node)¶

Determine if given node is a constant node.

Parameters

btor – Boolector instance.
node – Boolector node.

Returns

True if node is a constant, and false otherwise.

bool boolector_is_equal_sort(Btor *btor, BoolectorNode *n0, BoolectorNode *n1)¶

Determine if n0 and n1 have the same sort or not.

Parameters

btor – Boolector instance.
n0 – First operand.
n1 – Second operand.

Returns

True if n0 and n1 have the same sort, and false otherwise.

bool boolector_is_fun(Btor *btor, BoolectorNode *node)¶

Determine if given node is a function node.

Parameters

btor – Boolector instance.
node – Boolector node.

Returns

True if node is a function, and false otherwise.

bool boolector_is_fun_sort(Btor *btor, BoolectorSort sort)¶

Determine if sort is a function sort.

Parameters

btor – Boolector instance.
sort – Sort.

Returns

True if sort is a function sort, and false otherwise.

bool boolector_is_param(Btor *btor, BoolectorNode *node)¶

Determine if given node is a parameter node.

Parameters

btor – Boolector instance.
node – Boolector node.

Returns

True if node is a parameter, and false otherwise.

bool boolector_is_uf(Btor *btor, BoolectorNode *node)¶

Determine if given node is an uninterpreted function node.

Parameters

btor – Boolector instance.
node – Boolector node.

Returns

True if node is an uninterpreted function, and false otherwise.

bool boolector_is_var(Btor *btor, BoolectorNode *node)¶

Determine if given node is a bit-vector variable.

Parameters

btor – Boolector instance.
node – Boolector node.

Returns

True if node is a bit-vector variable, and false otherwise.

int32_t boolector_limited_sat(Btor *btor, int32_t lod_limit, int32_t sat_limit)¶

Solve an input formula and limit the search by the number of lemmas generated and the number of conflicts encountered by the underlying SAT solver.

An input formula is defined by constraints added via boolector_assert(). You can guide the search for a solution to an input formula by making assumptions via boolector_assume().

If you want to call this function multiple times then you must enable Boolector’s incremental usage mode via boolector_set_opt() before. Otherwise, this function can only be called once.

Parameters

btor – Boolector instance.
lod_limit – Lemma limit (-1 unlimited).
sat_limit – Conflict limit for SAT solver (-1 unlimited).

Returns

BOOLECTOR_SAT if the input formula is satisfiable (under possibly given assumptions), BOOLECTOR_UNSAT if the instance is unsatisfiable, and BOOLECTOR_UNKNOWN if the instance could not be solved within given limits.

BoolectorNode *boolector_match_node(Btor *btor, BoolectorNode *node)¶

Retrieve the node belonging to Boolector instance btor that matches given BoolectorNode node by id. This is intended to be used for handling expressions of a cloned instance (boolector_clone()). Aborts no matching node exists in given Boolector instance.

Parameters

btor – Boolector instance.
node – Boolector node.

Returns

The Boolector node that matches given node in Boolector instance btor by id.

Note

Matching a node against another increases the reference count of the returned match, which must therefore be released appropriately (boolector_release()). Only nodes created before a boolector_clone() call can be matched.

BoolectorNode *boolector_match_node_by_id(Btor *btor, int32_t id)¶

Retrieve the node belonging to Boolector instance btor that matches given id. Aborts if no node with given id exists in given Boolector instance.

Parameters

btor – Boolector instance.
id – Boolector node id.

Returns

The Boolector node that matches given node in Boolector instance btor by id.

Note

Matching a node against another increases the reference count of the returned match, which must therefore be released appropriately (boolector_release()). Only nodes created before a boolector_clone() call can be matched.

BoolectorNode *boolector_match_node_by_symbol(Btor *btor, const char *symbol)¶

Retrieve the node belonging to Boolector instance btor that matches given symbol. Aborts if no node with given symbol exists in given Boolector instance.

Parameters

btor – Boolector instance.
symbol – The symbol of an expression.

Returns

The Boolector node that matches given node in Boolector instance btor by id.

Note

Matching a node against another increases the reference count of the returned match, which must therefore be released appropriately (boolector_release()). Only nodes created before a boolector_clone() call can be matched.

BoolectorNode *boolector_max_signed(Btor *btor, BoolectorSort sort)¶

Create bit-vector maximum signed value constant of sort sort.

Parameters

btor – Boolector instance.
sort – Sort of constant.

Returns

Bit-vector constant representing the minimum signed value of sort sort.

BoolectorNode *boolector_min_signed(Btor *btor, BoolectorSort sort)¶

Create bit-vector minimum signed value constant of sort sort.

Parameters

btor – Boolector instance.
sort – Sort of constant.

Returns

Bit-vector constant representing the minimum signed value of sort sort.

BoolectorNode *boolector_mul(Btor *btor, BoolectorNode *n0, BoolectorNode *n1)¶

Create a bit-vector multiplication.

The parameters n0 and n1 must have the same bit width.

Parameters

btor – Boolector instance.
n0 – First bit-vector operand.
n1 – Second bit-vector operand.

Returns

Bit-vector multiplication with the same bit width as the operands.

BoolectorNode *boolector_nand(Btor *btor, BoolectorNode *n0, BoolectorNode *n1)¶

Create a bit-vector nand.

The parameters n0 and n1 must have the same bit width.

Parameters

btor – Boolector instance.
n0 – First bit-vector operand.
n1 – Second bit-vector operand.

Returns

Bit-vector with the same bit width as the operands.

BoolectorNode *boolector_ne(Btor *btor, BoolectorNode *n0, BoolectorNode *n1)¶

Create bit-vector or array inequality.

Both operands are either bit-vectors with the same bit width or arrays of the same type.

Parameters

btor – Boolector instance.
n0 – First operand.
n1 – Second operand.

Returns

Bit-vector with bit width one.

BoolectorNode *boolector_neg(Btor *btor, BoolectorNode *node)¶

Create the two’s complement of bit-vector node.

Parameters

btor – Boolector instance.
node – Bit-vector node.

Returns

Bit-vector representing the two’s complement of node with the same bit width as node.

Btor *boolector_new(void)¶

Create a new instance of Boolector.

Returns: New Boolector instance.

BtorOption boolector_next_opt(Btor *btor, BtorOption opt)¶

Given current option opt, get the opt of the next option in Boolector’s option list.

Given a Boolector instance btor, you can use this in combination with boolector_has_opt() and boolector_next_opt() in order to iterate over Boolector options as follows:

for (s = boolector_first_opt (btor);
     boolector_has_opt (btor, s);
     s = boolector_next_opt (btor, s))
  {...}

Parameters

btor – Btor instance.
opt – Option opt.

Returns

opt of the next option in Boolector’s option list, or 0 if no such next option does exist.

BoolectorNode *boolector_nor(Btor *btor, BoolectorNode *n0, BoolectorNode *n1)¶

Create a bit-vector nor.

The parameters n0 and n1 must have the same bit width.

Parameters

btor – Boolector instance.
n0 – First bit-vector operand.
n1 – Second bit-vector operand.

Returns

Bit-vector with the same bit width as the operands.

BoolectorNode *boolector_not(Btor *btor, BoolectorNode *node)¶

Create the one’s complement of bit-vector node.

Parameters

btor – Boolector instance.
node – bit-vector node.

Returns

Bit-vector representing the one’s complement of node with the same bit width as node.

BoolectorNode *boolector_one(Btor *btor, BoolectorSort sort)¶

Create bit-vector constant one of sort sort.

Parameters

btor – Boolector instance.
sort – Sort of constant.

Returns

Bit-vector constant one of sort sort.

BoolectorNode *boolector_ones(Btor *btor, BoolectorSort sort)¶

Create bit-vector constant of sort sort, where each bit is set to one.

Parameters

btor – Boolector instance.
sort – Sort of constant.

Returns

Bit-vector constant -1 of sort sort.

BoolectorNode *boolector_or(Btor *btor, BoolectorNode *n0, BoolectorNode *n1)¶

Create a bit-vector or.

The parameters n0 and n1 must have the same bit width.

Parameters

btor – Boolector instance.
n0 – First bit-vector operand.
n1 – Second bit-vector operand.

Returns

Bit-vector with the same bit width as the operands.

BoolectorNode *boolector_param(Btor *btor, BoolectorSort sort, const char *symbol)¶

Create function parameter of sort sort.

This kind of node is used to create parameterized expressions, which are used to create functions. Once a parameter is bound to a function, it cannot be re-used in other functions.

Parameters

btor – Boolector instance.
sort – Parameter sort.
symbol – Name of parameter.

Returns

Parameter expression of sort sort and with symbol symbol.

See also

boolector_fun(), boolector_apply()

int32_t boolector_parse(Btor *btor, FILE *infile, const char *infile_name, FILE *outfile, char **error_msg, int32_t *status, bool *parsed_smt2)¶

Parse input file.

Input file format may be either BTOR, BTOR2, SMT-LIB v1, or SMT-LIB v2, the file type is detected automatically. If the parser encounters an error, an explanation of that error is stored in error_msg. If the input file specifies a (known) status of the input formula (either sat or unsat), that status is stored in status. All output (from commands like e.g. ‘check-sat’ in SMT-LIB v2) is printed to outfile.

Parameters

btor – Boolector instance.
infile – Input file.
infile_name – Input file name.
outfile – Output file.
error_msg – Error message.
status – Status of the input formula.
parsed_smt2 – Flag indicating if an SMT-LIB v2 was parsed.

Returns

If the input issues a call to check sat (in case of incremental SMT-LIB v1 case or SMT-LIB v2), this function returns either BOOLECTOR_SAT, BOOLECTOR_UNSAT or BOOLECTOR_UNKNOWN. Otherwise, it always returns BOOLECTOR_PARSE_UNKNOWN. If a parse error occurs the function returns BOOLECTOR_PARSE_ERROR.

int32_t boolector_parse_btor(Btor *btor, FILE *infile, const char *infile_name, FILE *outfile, char **error_msg, int32_t *status)¶

Parse input file in BTOR format.

See boolector_parse().

Parameters

btor – Boolector instance.
infile – Input file.
infile_name – Input file name.
outfile – Output file.
error_msg – Error message.
status – Status of the input formula.

Returns

BOOLECTOR_UNKNOWN or BOOLECTOR_PARSE_ERROR if a parse error occurred.

int32_t boolector_parse_btor2(Btor *btor, FILE *infile, const char *infile_name, FILE *outfile, char **error_msg, int32_t *status)¶

Parse input file in BTOR2 format.

See boolector_parse().

Parameters

btor – Boolector instance.
infile – Input file.
infile_name – Input file name.
outfile – Output file.
error_msg – Error message.
status – Status of the input formula.

Returns

BOOLECTOR_UNKNOWN or BOOLECTOR_PARSE_ERROR if a parse error occurred.

int32_t boolector_parse_smt1(Btor *btor, FILE *infile, const char *infile_name, FILE *outfile, char **error_msg, int32_t *status)¶

Parse input file in SMT-LIB v1 format.

See boolector_parse().

Parameters

btor – Boolector instance.
infile – Input file.
infile_name – Input file name.
outfile – Input file.
error_msg – Error message.
status – Status of the input formula.

Returns

In the incremental case, the function returns either BOOLECTOR_SAT, BOOLECTOR_UNSAT or BOOLECTOR_UNKNOWN, otherwise it always returns BOOLECTOR_UNKNOWN. If a parse error occurs the function returns BOOLECTOR_PARSE_ERROR.

int32_t boolector_parse_smt2(Btor *btor, FILE *infile, const char *infile_name, FILE *outfile, char **error_msg, int32_t *status)¶

Parse input file in SMT-LIB v2 format. See boolector_parse().

Parameters

btor – Boolector instance.
infile – Input file.
infile_name – Input file name.
outfile – Output file.
error_msg – Error message.
status – Status of the input formula.

Returns

The function returns either BOOLECTOR_SAT, BOOLECTOR_UNSAT or BOOLECTOR_UNKNOWN. If a parse error occurs, the function returns BOOLECTOR_PARSE_ERROR.

void boolector_pop(Btor *btor, uint32_t level)¶

Pop context levels.

Parameters

btor – Boolector instance.
level – Number of context levels to pop (must be at least 1).

Note

Assumptions added via boolector_assume() are not affected by context level changes and are only valid until the next boolector_sat() call no matter at what level they were assumed.

See also

boolector_assume()

void boolector_print_model(Btor *btor, char *format, FILE *file)¶

Print model to output file. This function prints the model for all inputs to the output file file. Supported output formats for the model to be printed are:

btor

Use boolector’s own output format for printing models.
```
boolector_print_model (btor, "btor", stdout);
```
A possible model would be:
```
2 00000100 x
3 00010101 y
4[00] 01 A
```
where the first column indicates the id of an input, the second column its assignment, and the third column its name (or symbol), if any. Note that in case that an input is an uninterpreted function or an array variable, values in square brackets indicate parameter resp. index values.

smt2

Use SMT-LIB v2 format for printing models.

boolector_print_model (btor, "smt2", stdout);

A possible model would be:

(model
  (define-fun x () (_ BitVec 8) #b00000100)
  (define-fun y () (_ BitVec 8) #b00010101)
  (define-fun y (
   (y_x0 (_ BitVec 2)))
    (ite (= y_x0 #b00) #b01
      #00))
)

Parameters

btor – Boolector instance.
format – A string identifying the output format.
file – Output file.

void boolector_print_stats(Btor *btor)¶

Print statistics.

Parameters

btor – Boolector instance.

void boolector_push(Btor *btor, uint32_t level)¶

Push new context levels.

Parameters

btor – Boolector instance.
level – Number of context levels to create (must be a least 1).

Note

Assumptions added via boolector_assume() are not affected by context level changes and are only valid until the next boolector_sat() call no matter at what level they were assumed.

See also

boolector_assume()

BoolectorNode *boolector_read(Btor *btor, BoolectorNode *n_array, BoolectorNode *n_index)¶

Create a read on array n_array at position n_index.

Parameters

btor – Boolector instance.
n_array – Array operand.
n_index – Bit-vector index. The bit width of n_index must have the same bit width as the indices of n_array.

Returns

Bit-vector with the same bit width as the elements of n_array.

BoolectorNode *boolector_redand(Btor *btor, BoolectorNode *node)¶

Create and reduction of node node.

All bits of node are combined by a Boolean and.

Parameters

btor – Boolector instance.
node – Bit-vector node.

Returns

Bit-vector with bit width one.

BoolectorNode *boolector_redor(Btor *btor, BoolectorNode *node)¶

Create or reduction of node node.

All bits of node node are combined by a Boolean or.

Parameters

btor – Boolector instance.
node – Bit-vector node.

Returns

Bit-vector with bit width one.

BoolectorNode *boolector_redxor(Btor *btor, BoolectorNode *node)¶

Create xor reduction of node node.

All bits of node are combined by a Boolean xor.

Parameters

btor – Boolector instance.
node – Bit-vector node.

Returns

Bit-vector with bit width one.

void boolector_release(Btor *btor, BoolectorNode *node)¶

Release expression (decrements reference counter).

Parameters

btor – Boolector instance.
node – Boolector node to be released.

void boolector_release_all(Btor *btor)¶

Release all expressions and sorts.

Parameters

btor – Boolector instance.

void boolector_release_sort(Btor *btor, BoolectorSort sort)¶

Release sort (decrements reference counter).

Parameters

btor – Boolector instance.
sort – Sort to be released.

BoolectorNode *boolector_repeat(Btor *btor, BoolectorNode *node, uint32_t n)¶

Create n concatenations of a given node node.

Parameters

btor – Boolector instance.
node – Bit-vector operand.
n – Number of times to repeat the given node.

Returns

A node representing n concatenations of node node.

void boolector_reset_assumptions(Btor *btor)¶

Resets all added assumptions.

Parameters

btor – Boolector instance.

See also

boolector_assume()

void boolector_reset_stats(Btor *btor)¶

Reset statistics (time statistics not included).

Parameters

btor – Boolector instance.

void boolector_reset_time(Btor *btor)¶

Reset time statistics.

Parameters

btor – Boolector instance.

BoolectorNode *boolector_rol(Btor *btor, BoolectorNode *n0, BoolectorNode *n1)¶

Create a rotate left, with the number of bits to rotate by given as a bit-vector.

The parameters n0 and n1 must either have the same bit width or the bit width of n0 must be a power of two (greater than 1) and the bit width of n1 must be log2 of the bit width of n0.

Parameters

btor – Boolector instance.
n0 – First bit-vector operand.
n1 – Second bit-vector operand.

Returns

Bit-vector with the same bit width as n0.

BoolectorNode *boolector_roli(Btor *btor, BoolectorNode *n, uint32_t nbits)¶

Create a rotate left, with the number of bits to rotate by given as a numeral (unsigned integer).

Parameters

btor – Boolector instance.
n – Bit-vector operand.
nbits – Number of bits to rotate by.

Returns

Bit-vector with the same bit width as n.

BoolectorNode *boolector_ror(Btor *btor, BoolectorNode *n0, BoolectorNode *n1)¶

Create a rotate right, with the number of bits to rotate by given as a bit-vector.

The parameters n0 and n1 must either have the same bit width or the bit width of n0 must be a power of two (greater than 1) and the bit width of n1 must be log2 of the bit width of n0.

Parameters

btor – Boolector instance.
n0 – First bit-vector operand.
n1 – Second bit-vector operand.

Returns

Bit-vector with the same bit width as n0.

BoolectorNode *boolector_rori(Btor *btor, BoolectorNode *n, uint32_t nbits)¶

Create a rotate right, with the number of bits to rotate by given as a numeral (unsigned integer).

Parameters

btor – Boolector instance.
n – Bit-vector operand.
nbits – Number of bits to rotate by.

Returns

Bit-vector with the same bit width as n.

BoolectorNode *boolector_saddo(Btor *btor, BoolectorNode *n0, BoolectorNode *n1)¶

Create a signed bit-vector addition overflow detection.

The parameters n0 and n1 must have the same bit width.

Parameters

btor – Boolector instance.
n0 – First bit-vector operand.
n1 – Second bit-vector operand.

Returns

Bit-vector with bit width one, which indicates if the addition of n0 and n1 overflows in case both operands are treated signed.

int32_t boolector_sat(Btor *btor)¶

Solve an input formula.

An input formula is defined by constraints added via boolector_assert(). You can guide the search for a solution to an input formula by making assumptions via boolector_assume(). Note that assertions and assumptions are combined by boolean and.

If you want to call this function multiple times, you must enable Boolector’s incremental usage mode via boolector_set_opt() before. Otherwise, this function may only be called once.

Parameters

btor – Boolector instance.

Returns

BOOLECTOR_SAT if the instance is satisfiable and BOOLECTOR_UNSAT if the instance is unsatisfiable.

BoolectorNode *boolector_sdiv(Btor *btor, BoolectorNode *n0, BoolectorNode *n1)¶

Create signed division.

The parameters n0 and n1 must have the same bit width.

Parameters

btor – Boolector instance.
n0 – First bit-vector operand.
n1 – Second bit-vector operand.

Returns

Bit-vector with the same bit width as the operands.

Note

Signed division is expressed by means of unsigned division, where either node is normalized in case that its sign bit is 1. If the sign bits of a and b do not match, two’s complement is performed on the result of the previous unsigned division. Hence, the behavior in case of a division by zero depends on boolector_udiv().

BoolectorNode *boolector_sdivo(Btor *btor, BoolectorNode *n0, BoolectorNode *n1)¶

Create a signed bit-vector division overflow detection.

The parameters n0 and n1 must have the same bit width. An overflow can happen if n0 represents INT_MIN and n1 represents -1.

Parameters

btor – Boolector instance.
n0 – First bit-vector operand.
n1 – Second bit-vector operand.

Returns

Bit-vector with bit width one, which indicates if the division of n0 and n1 overflows in case both operands are treated signed.

Note

Unsigned division cannot overflow.

void boolector_set_abort(void (*fun)(const char *msg))¶

Set an abort callback that is called instead of exit on abort conditions.

It is recommended to set this function prior to creating Boolector instances.

Note

This function is not thread safe (the function pointer is maintained as a global variable). It you use threading, make sure to set the abort function prior to creating threads.

Parameters

fun – The abort callback function.
msg – The abort error message.

void boolector_set_msg_prefix(Btor *btor, const char *prefix)¶

Set a verbosity message prefix.

Parameters

btor – Boolector instance.
prefix – Prefix string.

void boolector_set_opt(Btor *btor, BtorOption opt, uint32_t val)¶

Set option.

E.g., given a Boolector instance btor, model generation is enabled via

boolector_set_opt (btor, BTOR_OPT_MODEL_GEN, 1);

General Options:

BTOR_OPT_MODEL_GEN

Enable (value: 1 or 2) or disable (value: 0) generation of a model for satisfiable instances.

There are two modes for model generation:
- generate model for asserted expressions only (value: 1)
- generate model for all expressions (value: 2)
BTOR_OPT_INCREMENTAL

Enable (value: 1) incremental mode.

Note that incremental usage turns off some optimization techniques. Disabling incremental usage is currently not supported.
BTOR_OPT_INCREMENTAL_SMT1

Set incremental mode for SMT-LIB v1 input.
- BTOR_INCREMENTAL_SMT1_BASIC [default]: stop after first satisfiable formula
- BTOR_INCREMENTAL_SMT1_CONTINUE: solve all formulas
BTOR_OPT_INPUT_FORMAT

Force input file format.

If unspecified, Boolector automatically detects the input file format while parsing.
- BTOR_INPUT_FORMAT_BTOR: BTOR format
- BTOR_INPUT_FORMAT_BTOR2: BTOR2 format
- BTOR_INPUT_FORMAT_SMT1: SMT-LIB v1 format
- BTOR_INPUT_FORMAT_SMT2: SMT-LIB v2 format
BTOR_OPT_OUTPUT_NUMBER_FORMAT

Force output number format.
- BTOR_OUTPUT_BASE_BIN [default]: binary
- BTOR_OUTPUT_BASE_HEX: hexa-decimal
- BTOR_OUTPUT_BASE_DEC: decimal
BTOR_OPT_OUTPUT_FORMAT

Force output file format (value: BTOR: -1, SMT-LIB v1: 1, SMT-LIB v2: 2).
- BTOR_OUTPUT_FORMAT_BTOR [default]: BTOR format
- BTOR_OUTPUT_FORMAT_BTOR2: BTOR2 format
- BTOR_OUTPUT_FORMAT_SMT2: SMT-LIB v2 format
- BTOR_OUTPUT_FORMAT_AIGER_ASCII: Aiger ascii format
- BTOR_OUTPUT_FORMAT_AIGER_BINARY: Aiger binary format
BTOR_OPT_ENGINE

Set solver engine.
- BTOR_ENGINE_FUN [default]: the default engine for all combinations of QF_AUFBV, uses lemmas on demand for QF_AUFBV and eager bit-blasting for QF_BV
- BTOR_ENGINE_SLS: the score-based local search QF_BV engine
- BTOR_ENGINE_PROP: the propagation-based local search QF_BV engine
- BTOR_ENGINE_AIGPROP: the propagation-based local search QF_BV engine that operates on the bit-blasted formula (the AIG layer)
- BTOR_ENGINE_QUANT: the quantifier engine (BV only)
BTOR_OPT_SAT_ENGINE

Set sat solver engine.

Available option values and default values depend on the sat solvers configured.
- BTOR_SAT_ENGINE_CADICAL: CaDiCaL
- BTOR_SAT_ENGINE_CMS: CryptoMiniSat
- BTOR_SAT_ENGINE_LINGELING: Lingeling
- BTOR_SAT_ENGINE_MINISAT: MiniSat
- BTOR_SAT_ENGINE_PICOSAT: PicoSAT
BTOR_OPT_AUTO_CLEANUP

Enable (value:1) or disable (value:0) auto cleanup of all references held on exit.
BTOR_OPT_PRETTY_PRINT

Enable (value: 1) or disable (value: 0) pretty printing when dumping.
BTOR_OPT_EXIT_CODES

Enable (value:1) or disable (value:0) the use of Boolector exit codes (BOOLECTOR_SAT, BOOLECTOR_UNSAT, BOOLECTOR_UNKNOWN - see Macros).

If disabled, on exit Boolector returns 0 if success (sat or unsat), and 1 in any other case.
BTOR_OPT_SEED

Set seed for Boolector’s internal random number generator.

Boolector uses 0 by default.

Simplifier Options:

BTOR_OPT_REWRITE_LEVEL

Set the rewrite level (value: 0-3) of the rewriting engine.

Boolector uses rewrite level 3 by default, rewrite levels are classified as follows:
- 0: no rewriting
- 1: term level rewriting
- 2: more simplification techniques
- 3: full rewriting/simplification
Do not alter the rewrite level of the rewriting engine after creating expressions.
BTOR_OPT_SKELETON_PREPROC

Enable (value: 1) or disable (value: 0) skeleton preprocessing during simplification.
BTOR_OPT_ACKERMANN

Enable (value: 1) or disable (value: 0) the eager addition of Ackermann constraints for function applications.
BTOR_OPT_BETA_REDUCE

Enable (value: 1) or disable (value: 0) the eager elimination of lambda expressions via beta reduction.
BTOR_OPT_ELIMINATE_SLICES

Enable (value: 1) or disable (value: 0) slice elimination on bit vector variables.
BTOR_OPT_VAR_SUBST

Enable (value: 1) or disable (value: 0) variable substitution during simplification.
BTOR_OPT_UCOPT

Enable (value: 1) or disable (value: 0) unconstrained optimization.
BTOR_OPT_MERGE_LAMBDAS

Enable (value: 1) or disable (value: 0) merging of lambda expressions.
BTOR_OPT_EXTRACT_LAMBDAS

Enable (value: 1) or disable (value: 0) extraction of common array patterns as lambda terms.
BTOR_OPT_NORMALIZE

Enable (value: 1) or disable (value: 0) normalization of addition, multiplication and bit-wise and.
BTOR_OPT_NORMALIZE_ADD

Enable (value: 1) or disable (value: 0) normalization of addition.

Fun Engine Options:

BTOR_OPT_FUN_PREPROP

Enable (value: 1) or disable (value: 0) prop engine as preprocessing step within sequential portfolio setting.
BTOR_OPT_FUN_PRESLS

Enable (value: 1) or disable (value: 0) sls engine as preprocessing step within sequential portfolio setting.
BTOR_OPT_FUN_DUAL_PROP

Enable (value: 1) or disable (value: 0) dual propagation optimization.
BTOR_OPT_FUN_DUAL_PROP_QSORT

Set order in which inputs are assumed in dual propagation clone.
- BTOR_DP_QSORT_JUST [default]: order by score, highest score first
- BTOR_DP_QSORT_ASC: order by input id, ascending
- BTOR_DP_QSORT_DESC: order by input id, descending
BTOR_OPT_FUN_JUST

Enable (value: 1) or disable (value: 0) justification optimization.
BTOR_OPT_FUN_JUST_HEURISTIC

Set heuristic that determines path selection for justification optimization.
- BTOR_JUST_HEUR_BRANCH_MIN_APP [default]: choose branch with minimum number of applies
- BTOR_JUST_HEUR_BRANCH_MIN_DEP: choose branch with minimum depth
- BTOR_JUST_HEUR_LEFT: always choose left branch
BTOR_OPT_FUN_LAZY_SYNTHESIZE

Enable (value: 1) or disable (value: 0) lazy synthesis of bit vector expressions.
BTOR_OPT_FUN_EAGER_LEMMAS

Select mode for eager generation lemmas.
- BTOR_FUN_EAGER_LEMMAS_NONE: do not generate lemmas eagerly (generate one single lemma per refinement iteration)
- BTOR_FUN_EAGER_LEMMAS_CONF: only generate lemmas eagerly until the first conflict dependent on another conflict is found
- BTOR_FUN_EAGER_LEMMAS_ALL: in each refinement iteration, generate lemmas for all conflicts
BTOR_OPT_PRINT_DIMACS

Enable (value: 1) or disable (value: 0) DIMACS printer.

When enabled Boolector will record the CNF sent to the SAT solver and prints it to stdout.

SLS Engine Options:

BTOR_OPT_SLS_NFIPS Set the number of bit flips used as a limit for the sls engine. Disabled if 0.
BTOR_OPT_SLS_STRATEGY

Select move strategy for SLS engine.
- BTOR_SLS_STRAT_BEST_MOVE: always choose best score improving move
- BTOR_SLS_STRAT_RAND_WALK: always choose random walk weighted by score
- BTOR_SLS_STRAT_FIRST_BEST_MOVE [default]: always choose first best move (no matter if any other move is better)
- BTOR_SLS_STRAT_BEST_SAME_MOVE: determine move as best move even if its score is not better but the same as the score of the previous best move
- BTOR_SLS_STRAT_ALWAYS_PROP: always choose propagation move (and recover with SLS move in case of conflict)
BTOR_OPT_SLS_JUST

Enable (value: 1) or disable (value: 0) justification based path selection during candidate selection.
BTOR_OPT_SLS_MOVE_GW

Enable (value: 1) or disable (value: 0) group-wise moves, where rather than changing the assignment of one single candidate variable, all candidate variables are set at the same time (using the same strategy).
BTOR_OPT_SLS_MOVE_RANGE

Enable (value: 1) or disable (value: 0) range-wise bit-flip moves, where the bits within all ranges from 2 to the bit width (starting from the LSB) are flipped at once.
BTOR_OPT_SLS_MOVE_SEGMENT

Enable (value: 1) or disable (value: 0) segment-wise bit-flip moves, where the bits within segments of multiples of 2 are flipped at once.
BTOR_OPT_SLS_MOVE_RAND_WALK

Enable (value: 1) or disable (value: 0) random walk moves, where one out of all possible neighbors is randomly selected (with given probability, see BTOR_OPT_SLS_PROB_MOVE_RAND_WALK) for a randomly selected candidate variable.
BTOR_OPT_SLS_PROB_MOVE_RAND_WALK

Set the probability with which a random walk is chosen if random walks are enabled (see BTOR_OPT_SLS_MOVE_RAND_WALK).
BTOR_OPT_SLS_MOVE_RAND_ALL

Enable (value: 1) or disable (value: 0) the randomization of all candidate variables (rather than a single randomly selected candidate variable) in case no best move has been found.
BTOR_OPT_SLS_MOVE_RAND_RANGE

Enable (value: 1) or disable (value: 0) the randomization of bit ranges (rather than all bits) of a candidate variable(s) to be randomized in case no best move has been found.
BTOR_OPT_SLS_MOVE_PROP

Enable (value: 1) or disable (value: 0) propagation moves (chosen with a given ratio of number of propagation moves to number of regular SLS moves, see BTOR_OPT_SLS_MOVE_PROP_N_PROP and BTOR_OPT_SLS_MOVE_PROP_N_SLS).
BTOR_OPT_SLS_MOVE_PROP_N_PROP

Set the number of propagation moves to be performed when propagation moves are enabled (propagation moves are chosen with a ratio of propagation moves to regular SLS moves, see BTOR_OPT_SLS_MOVE_PROP and BTOR_OPT_SLS_MOVE_PROP_N_SLS).
BTOR_OPT_SLS_MOVE_PROP_N_SLS

Set the number of regular SLS moves to be performed when propagation moves are enabled (propagation moves are chosen with a ratio of propagation moves to regular SLS moves, see BTOR_OPT_SLS_MOVE_PROP and BTOR_OPT_SLS_MOVE_PROP_N_PROP).
BTOR_OPT_SLS_MOVE_PROP_FORCE_RW

Enable (value: 1) or disable (value: 0) that random walks are forcibly chosen as recovery moves in case of conflicts when a propagation move is performed (rather than performing a regular SLS move).
BTOR_OPT_SLS_MOVE_INC_MOVE_TEST

Enable (value: 1) or disable (value: 0) that during best move selection, if the current candidate variable with a previous neighbor yields the currently best score, this neighbor assignment is used as a base for further neighborhood exploration (rather than its current assignment).
BTOR_OPT_SLS_MOVE_RESTARTS

Enable (value: 1) or disable (value: 0) restarts.
BTOR_OPT_SLS_MOVE_RESTARTS

Enable (value: 1) or disable (value: 0) heuristic (bandit scheme) for selecting root constraints.

If disabled, candidate root constraints are selected randomly.

Prop Engine Options:

BTOR_OPT_PROP_NPROPS

Set the number of propagation (steps) used as a limit for the propagation engine. Disabled if 0.
BTOR_OPT_PROP_USE_RESTARTS

Enable (value: 1) or disable (value: 0) restarts.
BTOR_OPT_PROP_USE_RESTARTS

Enable (value: 1) or disable (value: 0) heuristic (bandit scheme) for selecting root constraints.

If enabled, root constraint selection via bandit scheme is based on a scoring scheme similar to the one employed in the SLS engine.

If disabled, candidate root constraints are selected randomly.
BTOR_OPT_PROP_PATH_SEL

Select mode for path selection.
- BTOR_PROP_PATH_SEL_CONTROLLING: select path based on controlling inputs
- BTOR_PROP_PATH_SEL_ESSENTIAL [default]: select path based on essential inputs
- BTOR_PROP_PATH_SEL_RANDOM: select path based on random inputs
BTOR_OPT_PROP_PROB_USE_INV_VALUE

Set probabiality with which to choose inverse values over consistent values.

BTOR_OPT_PROP_PROB_FLIP_COND

Set probability with which to select the path to the condition (in case of an if-then-else operation) rather than the enabled branch during down propagation.

BTOR_OPT_PROP_PROB_FLIP_COND_CONST

Set probbiality with which to select the path to the condition (in case of an if-then-else operation) rather than the enabled branch during down propagation if either of the ‘then’ or ‘else’ branch is constant.

BTOR_OPT_PROP_FLIP_COND_CONST_DELTA

Set delta by which BTOR_OPT_PROP_PROB_FLIP_COND_CONST is decreased or increased after a limit BTOR_OPT_PROP_FLIP_COND_CONST_NPATHSEL is reached.

BTOR_OPT_PROP_FLIP_COND_CONST_NPATHSEL

Set the limit for how often the path to the condition (in case of an if-then-else operation) may be selected bevor BTOR_OPT_PROP_PROB_FLIP_COND_CONST is decreased or increased by BTOR_OPT_PROP_PROB_FLIP_COND_CONST_DELTA.

BTOR_OPT_PROP_PROB_SLICE_KEEP_DC

Set probability with which to keep the current value of the don’t care bits of a slice operation (rather than fully randomizing all of them) when selecting an inverse or consistent value.
BTOR_OPT_PROP_PROB_CONC_FLIP

Set probability with which to use the corresponing slice of current assignment with max. one of its bits flipped (rather than using the corresponding slice of the down propagated assignment) as result of consistent value selection for concats.

BTOR_OPT_PROP_PROB_SLICE_FLIP

Set probability with which to use the current assignment of the operand of a slice operation with one of the don’t care bits flipped (rather than fully randomizing all of them, both for inverse and consistent value selection) if their current assignment is not kept (see BTOR_OPT_PROP_PROB_SLICE_KEEP_DC).

BTOR_OPT_PROP_PROB_EQ_FLIP

Set probability with which the current assignment of the selected node with one of its bits flipped (rather than a fully randomized bit-vector) is down-propagated in case of an inequality (both for inverse and consistent value selection).

BTOR_OPT_PROP_PROB_AND_FLIP

Set probability with which the current assignment of the don’t care bits of the selected node with max. one of its bits flipped (rather than fully randomizing all of them) in case of an and operation (for both inverse and consistent value selection).

BTOR_OPT_PROP_NO_MOVE_ON_CONFLICT

Do not perform a propagation move when running into a conflict during inverse computation.

(This is the default behavior for the SLS engine when propagation moves are enabled, where a conflict triggers a recovery by means of a regular SLS move.)

AIGProp Engine Options:

BTOR_OPT_AIGPROP_USE_RESTARTS

Enable (value: 1) or disable (value: 0) restarts.
BTOR_OPT_AIGPROP_USE_RESTARTS

Enable (value: 1) or disable (value: 0) heuristic (bandit scheme) for selecting root constraints.

If enabled, root constraint selection via bandit scheme is based on a scoring scheme similar to the one employed in the SLS engine.

If disabled, candidate root constraints are selected randomly.
BTOR_OPT_QUANT_SYNTH

Select synthesis mode for Skolem functions.

BTOR_QUANT_SYNTH_NONE: do not synthesize skolem functions (use model values for instantiation)

BTOR_QUANT_SYNTH_EL: use enumerative learning to synthesize skolem functions

BTOR_QUANT_SYNTH_ELMC: use enumerative learning modulo the predicates in the cone of influence of the existential variables to synthesize skolem functions

BTOR_QUANT_SYNTH_EL_ELMC: chain BTOR_QUANT_SYNTH_EL and BTOR_QUANT_SYNTH_ELMC approaches to synthesize skolem functions

BTOR_QUANT_SYNTH_ELMR: use enumerative learning modulo the given root constraints to synthesize skolem functions

BTOR_OPT_QUANT_DUAL_SOLVER

Enable (value: 1) or disable (value: 0) solving the dual (negated) version of the quantified bit-vector formula.
BTOR_OPT_QUANT_SYNTH_LIMIT

Set the limit of enumerated expressions for the enumerative learning synthesis algorithm.
BTOR_OPT_SYNTH_QI

Enable (value: 1) or disable (value: 0) generalization of quantifier instantiations via enumerative learning.
BTOR_OPT_QUANT_DER

Enable (value: 1) or disable (value: 0) destructive equality resolution simplification.
BTOR_OPT_QUANT_CER

Enable (value: 1) or disable (value: 0) constructive equality resolution simplification.
BTOR_OPT_QUANT_MINISCOPE

Enable (value: 1) or disable (value: 0) miniscoping.

Parameters

btor – Boolector instance.
opt – Option opt.
val – Option value.

void boolector_set_sat_solver(Btor *btor, const char *solver)¶

Set the SAT solver to use.

Currently, we support Lingeling, PicoSAT, and MiniSAT as string value of solver (case insensitive). This is however only possible if the corresponding solvers were enabled at compile time. Call this function after boolector_new().

Parameters

btor – Boolector instance
solver – Solver identifier string.

void boolector_set_symbol(Btor *btor, BoolectorNode *node, const char *symbol)¶

Set the symbol of an expression.

Parameters

btor – Boolector instance.
node – Boolector node.
symbol – The symbol to be set.

void boolector_set_term(Btor *btor, int32_t (*fun)(void*), void *state)¶

Set a termination callback.

param btor

Boolector instance.

param fun

The termination callback function.

param state

The argument to the termination callback function.

See also

boolector_terminate()

void boolector_set_trapi(Btor *btor, FILE *apitrace)¶

Set the output API trace file and enable API tracing.

Parameters

btor – Boolector instance.
apitrace – Output file.

Note

The API trace output file can also be set via the environment variable BTORAPITRACE=<filename>.

BoolectorNode *boolector_sext(Btor *btor, BoolectorNode *node, uint32_t width)¶

Create signed extension.

The bit-vector node is padded with width bits where the value depends on the value of the most significant bit of node n.

Parameters

btor – Boolector instance.
node – Bit-vector node.
width – Number of bits to pad.

Returns

A bit-vector extended by width bits.

BoolectorNode *boolector_sgt(Btor *btor, BoolectorNode *n0, BoolectorNode *n1)¶

Create a signed greater than.

The parameters n0 and n1 must have the same bit width.

Parameters

btor – Boolector instance.
n0 – First bit-vector operand.
n1 – Second bit-vector operand.

Returns

Bit-vector with bit width one.

BoolectorNode *boolector_sgte(Btor *btor, BoolectorNode *n0, BoolectorNode *n1)¶

Create a signed greater than or equal.

The parameters n0 and n1 must have the same bit width.

Parameters

btor – Boolector instance.
n0 – First bit-vector operand.
n1 – Second bit-vector operand.

Returns

Bit-vector with bit width one.

int32_t boolector_simplify(Btor *btor)¶

Simplify current input formula.

Parameters

btor – Boolector instance.

Returns

BOOLECTOR_SAT if the input formula was simplified to true, BOOLECTOR_UNSAT if it was simplified to false, and BOOLECTOR_UNKNOWN otherwise.

Note

Each call to boolector_sat() simplifies the input formula as a preprocessing step.

BoolectorNode *boolector_slice(Btor *btor, BoolectorNode *node, uint32_t upper, uint32_t lower)¶

Create a bit-vector slice of node from index upper to index lower.

Parameters

btor – Boolector instance.
node – Bit-vector node.
upper – Upper index which must be greater than or equal to zero, and less than the bit width of node.
lower – Lower index which must be greater than or equal to zero, and less than or equal to upper.

Returns

Bit-vector with bit width upper - lower + 1.

BoolectorNode *boolector_sll(Btor *btor, BoolectorNode *n0, BoolectorNode *n1)¶

Create a logical shift left.

The parameters n0 and n1 must either have the same bit width or the bit width of n0 must be a power of two (greater than 1) and the bit width of n1 must be log2 of the bit width of n0.

Parameters

btor – Boolector instance.
n0 – First bit-vector operand.
n1 – Second bit-vector operand.

Returns

Bit-vector with the same bit width as n0.

BoolectorNode *boolector_slt(Btor *btor, BoolectorNode *n0, BoolectorNode *n1)¶

Create a signed less than.

The parameters n0 and n1 must have the same bit width.

Parameters

btor – Boolector instance.
n0 – First bit-vector operand.
n1 – Second bit-vector operand.

Returns

Bit-vector with bit width one.

BoolectorNode *boolector_slte(Btor *btor, BoolectorNode *n0, BoolectorNode *n1)¶

Create a signed less than or equal.

The parameters n0 and n1 must have the same bit width.

Parameters

btor – Boolector instance.
n0 – First bit-vector operand.
n1 – Second bit-vector operand.

Returns

Bit-vector with bit width one.

BoolectorNode *boolector_smod(Btor *btor, BoolectorNode *n0, BoolectorNode *n1)¶

Create a, signed remainder where its sign matches the sign of the divisor.

The parameters n0 and n1 must have the same bit width.

Parameters

btor – Boolector instance.
n0 – First bit-vector operand.
n1 – Second bit-vector operand.

Returns

Bit-vector with the same bit width as the operands.

Note

If n1 is zero, the behavior of this function depends on boolector_urem().

BoolectorNode *boolector_smulo(Btor *btor, BoolectorNode *n0, BoolectorNode *n1)¶

Create signed multiplication overflow detection.

The parameters n0 and n1 must have the same bit width.

Parameters

btor – Boolector instance.
n0 – First bit-vector operand.
n1 – Second bit-vector operand.

Returns

Bit-vector with bit width one, which indicates if the multiplication of n0 and n1 overflows in case both operands are treated signed.

BoolectorNode *boolector_sra(Btor *btor, BoolectorNode *n0, BoolectorNode *n1)¶

Create an arithmetic shift right.

The parameters n0 and n1 must either have the same bit width or the bit width of n0 must be a power of two (greater than 1) and the bit width of n1 must be log2 of the bit width of n0.

Parameters

btor – Boolector instance.
n0 – First bit-vector operand.
n1 – Second bit-vector operand.

Returns

Bit-vector with the same bit width as n0.

BoolectorNode *boolector_srem(Btor *btor, BoolectorNode *n0, BoolectorNode *n1)¶

Create a signed remainder.

The parameters n0 and n1 must have the same bit width. If n1 is zero, then the result is n0.

Parameters

btor – Boolector instance.
n0 – First bit-vector operand.
n1 – Second bit-vector operand.

Returns

Bit-vector with the same bit width as the operands.

Note

Analogously to boolector_sdiv(), the signed remainder is expressed by means of the unsigned remainder, where either node is normalized in case that its sign bit is 1. Hence, in case that n1 is zero, the result depends on boolector_urem().

BoolectorNode *boolector_srl(Btor *btor, BoolectorNode *n0, BoolectorNode *n1)¶

Create a logical shift right.

The parameters n0 and n1 must either have the same bit width or the bit width of n0 must be a power of two (greater than 1) and the bit width of n1 must be log2 of the bit width of n0.

Parameters

btor – Boolector instance.
n0 – First bit-vector operand.
n1 – Second bit-vector operand.

Returns

Bit-vector with the same bit width as n0.

BoolectorNode *boolector_ssubo(Btor *btor, BoolectorNode *n0, BoolectorNode *n1)¶

Create a signed bit-vector subtraction overflow detection.

The parameters n0 and n1 must have the same bit width.

Parameters

btor – Boolector instance.
n0 – First bit-vector operand.
n1 – Second bit-vector operand.

Returns

Bit-vector with bit width one, which indicates if the subtraction of n0 and n1 overflows in case both operands are treated signed.

BoolectorNode *boolector_sub(Btor *btor, BoolectorNode *n0, BoolectorNode *n1)¶

Create a bit-vector subtraction.

The parameters n0 and n1 must have the same bit width.

Parameters

btor – Boolector instance.
n0 – First bit-vector operand.
n1 – Second bit-vector operand.

Returns

Bit-vector with the same bit width as the operands.

int32_t boolector_terminate(Btor *btor)¶

Determine if a given Boolector instance has been terminated (and or terminate Boolector) via the previously configured termination callback function.

Parameters

btor – Boolector instance.

Returns

True if Boolector is terminated, and false otherwise.

See also

boolector_set_term()

BoolectorNode *boolector_true(Btor *btor)¶

Create constant true. This is represented by the bit-vector constant one with bit width one.

Parameters

btor – Boolector instance.

Returns

Bit-vector constant one with bit width one.

BoolectorNode *boolector_uaddo(Btor *btor, BoolectorNode *n0, BoolectorNode *n1)¶

Create an unsigned bit-vector addition overflow detection.

The parameters n0 and n1 must have the same bit width.

Parameters

btor – Boolector instance.
n0 – First bit-vector operand.
n1 – Second bit-vector operand.

Returns

Bit-vector with bit width one, which indicates if the addition of n0 and n1 overflows in case both operands are treated unsigned.

BoolectorNode *boolector_udiv(Btor *btor, BoolectorNode *n0, BoolectorNode *n1)¶

Create unsigned division.

The parameters n0 and n1 must have the same bit width. If n1 is zero, then the result is -1.

Parameters

btor – Boolector instance.
n0 – First bit-vector operand.
n1 – Second bit-vector operand.

Returns

Bit-vector with the same bit width as the operands.

Note

The behavior that division by zero returns -1 does not exactly comply with the SMT-LIB standard 1.2 and 2.0 where division by zero is handled as uninterpreted function. Our semantics are motivated by real circuits where division by zero cannot be uninterpreted and of course returns a result.

BoolectorNode *boolector_uext(Btor *btor, BoolectorNode *node, uint32_t width)¶

Create unsigned extension.

The bit-vector node is padded with width * zeroes.

Parameters

btor – Boolector instance.
node – Bit-vector node.
width – Number of zeroes to pad.

Returns

A bit-vector extended by width zeroes.

BoolectorNode *boolector_uf(Btor *btor, BoolectorSort sort, const char *symbol)¶

Create an uninterpreted function with sort sort and with symbol symbol. btor Boolector instance.

An uninterpreted function’s symbol is used as a simple means of identification, either when printing a model via boolector_print_model(), or generating file dumps via boolector_dump_btor() and boolector_dump_smt2(). A symbol must be unique but may be NULL in case that no symbol should be assigned.

Parameters

sort – Sort of the uninterpreted function.
symbol – Name of the uninterpreted function.

Returns

Uninterpreted function of sort sort and with symbol symbol.

Note

In contrast to composite expressions, which are maintained uniquely w.r.t. to their kind, inputs (and consequently, bit width), uninterpreted functions are not. Hence, each call to this function returns a fresh uninterpreted function.

void boolector_uf_assignment(Btor *btor, BoolectorNode *n_uf, char ***args, char ***values, uint32_t *size)¶

Generate a model for an uninterpreted function. The function creates and stores the assignments of the function’s arguments to array args and the function’s return values to array values. Arrays args and values represent assignment pairs of arguments and values, i.e., instantiating a function with args[i] yields value values[i]. For functions with arity > 1 args[i] contains a space separated string of argument assignments, where the order of the assignment strings corresponds to the order of the function’s arguments.

Parameters

btor – Boolector instance.
n_uf – Uninterpreted function node.
args – Pointer to array of argument assignment strings.
values – Pointer to array of value assignment strings.
size – Size of arrays args and values.

Note

This function can only be called if boolector_sat() returned BOOLECTOR_SAT and model generation was enabled.

See also

boolector_set_opt() for enabling model generation

BoolectorNode *boolector_ugt(Btor *btor, BoolectorNode *n0, BoolectorNode *n1)¶

Create an unsigned greater than.

The parameters n0 and n1 must have the same bit width.

Parameters

btor – Boolector instance.
n0 – First bit-vector operand.
n1 – Second bit-vector operand.

Returns

Bit-vector with bit width one.

BoolectorNode *boolector_ugte(Btor *btor, BoolectorNode *n0, BoolectorNode *n1)¶

Create an unsigned greater than or equal.

The parameters n0 and n1 must have the same bit width.

Parameters

btor – Boolector instance.
n0 – First bit-vector operand.
n1 – Second bit-vector operand.

Returns

Bit-vector with bit width one.

BoolectorNode *boolector_ult(Btor *btor, BoolectorNode *n0, BoolectorNode *n1)¶

Create an unsigned less than.

The parameters n0 and n1 must have the same bit width.

Parameters

btor – Boolector instance.
n0 – First bit-vector operand.
n1 – Second bit-vector operand.

Returns

Bit-vector with bit width one.

BoolectorNode *boolector_ulte(Btor *btor, BoolectorNode *n0, BoolectorNode *n1)¶

Create an unsigned less than or equal.

The parameters n0 and n1 must have the same bit width.

Parameters

btor – Boolector instance.
n0 – First bit-vector operand.
n1 – Second bit-vector operand.

Returns

Bit-vector with bit width one.

BoolectorNode *boolector_umulo(Btor *btor, BoolectorNode *n0, BoolectorNode *n1)¶

Create an unsigned bit-vector multiplication overflow detection.

The parameters n0 and n1 must have the same bit width.

Parameters

btor – Boolector instance.
n0 – First bit-vector operand.
n1 – Second bit-vector operand.

Returns

Bit-vector with bit width one, which indicates if the multiplication of n0 and n1 overflows in case both operands are treated unsigned.

BoolectorNode *boolector_unsigned_int(Btor *btor, uint32_t u, BoolectorSort sort)¶

Create bit-vector constant representing the unsigned integer u of sort sort.

The constant is obtained by either truncating bits or by unsigned extension (padding with zeroes).

Parameters

btor – Boolector instance.
u – Unsigned integer value.
sort – Sort of constant.

Returns

Bit-vector constant of sort sort.

BoolectorNode *boolector_urem(Btor *btor, BoolectorNode *n0, BoolectorNode *n1)¶

Create an unsigned remainder.

The parameters n0 and n1 must have the same bit width. If n1 is zero, then the result is n0.

Parameters

btor – Boolector instance.
n0 – First bit-vector operand.
n1 – Second bit-vector operand.

Returns

Bit-vector with the same bit width as the operands.

Note

As in boolector_udiv() the behavior if n1 is zero, does not exactly comply with the SMT-LIB standard 1.2 and 2.0 where the result is handled as uninterpreted function. Our semantics are motivated by real circuits, where results can not be uninterpreted.

BoolectorNode *boolector_usubo(Btor *btor, BoolectorNode *n0, BoolectorNode *n1)¶

Create an unsigned bit-vector subtraction overflow detection.

The parameters n0 and n1 must have the same bit width.

Parameters

btor – Boolector instance.
n0 – First bit-vector operand.
n1 – Second bit-vector operand.

Returns

Bit-vector with bit width one, which indicates if the subtraction of n0 and n1 overflows in case both operands are treated unsigned.

BoolectorNode *boolector_var(Btor *btor, BoolectorSort sort, const char *symbol)¶

Create a bit-vector variable of sort sort and with symbol symbol.

A variable’s symbol is used as a simple means of identification, either when printing a model via boolector_print_model(), or generating file dumps via boolector_dump_btor() and boolector_dump_smt2(). A symbol must be unique but may be NULL in case that no symbol should be assigned.

Parameters

btor – Boolector instance.
sort – Variable sort.
symbol – Name of variable.

Returns

Bit-vector variable of sort sort and with symbol symbol.

Note

In contrast to composite expressions, which are maintained uniquely w.r.t. to their kind, inputs (and consequently, bit width), variables are not. Hence, each call to this function returns a fresh bit-vector variable.

const char *boolector_version(Btor *btor)¶

Get Boolector’s version string.

Parameters

btor – Boolector instance.

Returns

A string with Boolector’s version.

BoolectorNode *boolector_write(Btor *btor, BoolectorNode *n_array, BoolectorNode *n_index, BoolectorNode *n_value)¶

Create a write on array n_array at position n_index with value n_value.

The array is updated at exactly one position, all other elements remain unchanged. The bit width of n_index must be the same as the bit width of the indices of n_array. The bit width of n_value must be the same as the bit width of the elements of n_array.

Parameters

btor – Boolector instance.
n_array – Array operand.
n_index – Bit-vector index.
n_value – Bit-vector value.

Returns

An array where the value at index n_index has been updated with n_value.

BoolectorNode *boolector_xnor(Btor *btor, BoolectorNode *n0, BoolectorNode *n1)¶

Create a bit-vector xnor.

The parameters n0 and n1 must have the same bit width.

Parameters

btor – Boolector instance.
n0 – First bit-vector operand.
n1 – Second bit-vector operand.

Returns

Bit-vector with the same bit width as the operands.

BoolectorNode *boolector_xor(Btor *btor, BoolectorNode *n0, BoolectorNode *n1)¶

Create a bit-vector xor.

The parameters n0 and n1 must have the same bit width.

Parameters

btor – Boolector instance.
n0 – First bit-vector operand.
n1 – Second bit-vector operand.

Returns

Bit-vector with the same bit width as the operands.

BoolectorNode *boolector_zero(Btor *btor, BoolectorSort sort)¶

Create bit-vector constant zero of sort sort.

Parameters

btor – Boolector instance.
sort – Sort of bit-vector constant.

Returns

Bit-vector constant zero of sort sort.

C Interface¶

Macros¶

Typedefs¶

Functions¶

Deprecated¶