C Interface¶
Macros¶

BOOLECTOR_PARSE_ERROR
¶ Preprocessor constant representing status
parse error
.See also

BOOLECTOR_PARSE_UNKNOWN
¶ Preprocessor constant representing status
parse unknown
.See also

BOOLECTOR_SAT
¶ Preprocessor constant representing status
satisfiable
.

BOOLECTOR_UNKNOWN
¶ Preprocessor constant representing status
unknown
.

BOOLECTOR_UNSAT
¶ Preprocessor constant representing status
unsatisfiable
.
Typedefs¶
Functions¶

BoolectorNode *
boolector_add
(Btor * btor, BoolectorNode * n0, BoolectorNode * n1)¶ Create bit vector addition.
The parameters
n0
andn1
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
andn1
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, int argc, BoolectorNode * n_fun)¶ Create a function application on function
n_fun
with argumentsarg_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 argumentsarg_nodes
.See also

BoolectorNode *
boolector_array
(Btor * btor, BoolectorSort sort, const char * symbol)¶ Create a onedimensional 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 viaboolector_dump_btor()
andboolector_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 symbolsymbol
.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, int * size)¶ Generate a model for an array expression.
If
boolector_sat()
has returnedBOOLECTOR_SAT
and model generation has been enabled. The function creates and stores the array of indices intoindices
and the array of corresponding values intovalues
. The number size ofindices
resp.values
is stored intosize
. 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. The bit vector assignments to the indices and values have to be freed byboolector_free_bv_assignment()
. Furthermore, the user has to free the array of indices and the array of values, respectively of sizesize
.Parameters:  btor – Boolector instance.
 n_array – Array operand for which the array model should be built.
 indices – Pointer to array of index strings.
 values – Pointer to array of value strings.
 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 sortelement
.See also

void
boolector_assert
(Btor * btor, BoolectorNode * node)¶ Add a constraint.
Use this function to assert
node
. Added constraints can not be deleted anymore. Afternode
has been asserted, it can be safely released byboolector_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 viaboolector_set_opt()
before you can add assumptions. In contrast to assertions added viaboolector_assert()
, assumptions are discarded after each call toboolector_sat()
. Assumptions and assertions are logically combined via Booleanand
. 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, int 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

BoolectorSort
boolector_bool_sort
(Btor * btor)¶ Create Boolean sort.
Parameters:  btor – Boolector instance.
Returns: Sort of type Boolean.
See also

const char *
boolector_bv_assignment
(Btor * btor, BoolectorNode * node)¶ Generate an assignment string for bit vector expression if
boolector_sat()
has returnedBOOLECTOR_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. Each character of the string can be
0
,1
orx
. The latter represents that the corresponding bit can be assigned arbitrarily.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. Useboolector_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, if you use
boolector_clone()
with MiniSAT or PicoSAT (no cloning support), Boolector can only be cloned prior to the firstboolector_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 ifthenelse.
If condition
n_cond
is true, thenn_then
is returned, elsen_else
is returned. Nodesn_then
andn_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
orn_else
.

BoolectorNode *
boolector_const
(Btor * btor, const char * bits)¶ Create bit vector constant representing the bit vector
bits
.Parameters:  btor – Boolector instance.
 bits – Nonempty 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_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.

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 optionauto_cleanup
viaboolector_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_btor2
(Btor * btor, FILE * file)¶ Dump formula to file in BTOR 2.0 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 SMTLIB 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 SMTLIB 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.

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

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 withboolector_has_opt()
andboolector_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

void
boolector_free_array_assignment
(Btor * btor, char ** indices, char ** values, int 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
andvalues
.
See also

void
boolector_free_bits
(Btor * btor, const char * bits)¶ Free a bits string for bit vector constants.
Parameters:  btor – Boolector instance.
 bits – String which has to be freed.
See also

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

void
boolector_free_uf_assignment
(Btor * btor, char ** args, char ** values, int 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
andvalues
.
See also

BoolectorNode *
boolector_fun
(Btor * btor, BoolectorNode ** param_nodes, int paramc, BoolectorNode * node)¶ Create a function with body
node
parameterized over parametersparam_nodes
.This kind of node is similar to macros in the SMTLIB 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
.See also

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, int 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

int
boolector_fun_sort_check
(Btor * btor, BoolectorNode ** arg_nodes, int 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 as a bit string.
Parameters:  btor – Boolector instance.
 node – Constant node.
Returns: String representing the bits of
node
.

Btor *
boolector_get_btor
(BoolectorNode * node)¶ Return the Boolector instance to which
node
belongs.Parameters:  node – Boolector node.
Returns: Boolector instance.

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
.

int
boolector_get_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_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

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
.

int
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 callboolector_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
.

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 withboolector_has_opt()
andboolector_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
andn1
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
andn1
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, int i, BoolectorSort sort)¶ Create bit vector constant representing the signed integer
i
of sortsort
.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 expression 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 bitvector sort.Parameters:  btor – Boolector instance.
 sort – Sort.
Returns: True if
sort
is a bitvector 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_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
andn1
have the same sort or not.Parameters:  btor – Boolector instance.
 n0 – First operand.
 n1 – Second operand.
Returns: True if
n0
andn1
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.

int
boolector_limited_sat
(Btor * btor, int lod_limit, int 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 viaboolector_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 – Limit for lemmas on demand (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, andBOOLECTOR_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 BoolectorNodenode
by id. This is intended to be used for handling expressions of a cloned instance (boolector_clone()
).Parameters:  btor – Boolector instance.
 node – Boolector node.
Returns: The Boolector node that matches given
node
in Boolector instancebtor
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 theboolector_clone()
call can be matched.

BoolectorNode *
boolector_match_node_by_id
(Btor * btor, int id)¶ Retrieve the node belonging to Boolector instance
btor
that matches givenid
.Parameters:  btor – Boolector instance.
 id – Boolector node id.
Returns: The Boolector node that matches given
node
in Boolector instancebtor
by id.Note
Matching a node against another increases the reference count of the returned match, which must therefore be released appropriately (
boolector_release()
).

BoolectorNode *
boolector_match_node_by_symbol
(Btor * btor, const char * symbol)¶ Retrieve the node belonging to Boolector instance
btor
that matches givensymbol
.Parameters:  btor – Boolector instance.
 symbol – The symbol of an expression.
Returns: The Boolector node that matches given
node
in Boolector instancebtor
by symbol.Note
Matching a node against another increases the reference count of the returned match, which must therefore be released appropriately (
boolector_release()
).

BoolectorNode *
boolector_mul
(Btor * btor, BoolectorNode * n0, BoolectorNode * n1)¶ Create a bitvector multiplication.
The parameters
n0
andn1
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
andn1
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 asnode
.

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 withboolector_has_opt()
andboolector_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
andn1
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 asnode
.

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
andn1
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 reused in other functions.
Parameters:  btor – Boolector instance.
 sort – Parameter sort.
 symbol – Name of parameter.
Returns: Parameter expression of sort
sort
and with symbolsymbol
.See also

int
boolector_parse
(Btor * btor, FILE * infile, const char * infile_name, FILE * outfile, char ** error_msg, int * status)¶ Parse input file.
Input file format may be either BTOR, SMTLIB v1, or SMTLIB 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 instatus
. All output (from commands like e.g. ‘checksat’ in SMTLIB v2) is printed tooutfile
.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: In the incremental case or in case of SMTLIB v2 (which requires a ‘checksat’ command), the function returns either
BOOLECTOR_SAT
,BOOLECTOR_UNSAT
orBOOLECTOR_UNKNOWN
. Otherwise, it always returnsBOOLECTOR_PARSE_UNKNOWN
. If a parse error occurs the function returnsBOOLECTOR_PARSE_ERROR
.

int
boolector_parse_btor
(Btor * btor, FILE * infile, const char * infile_name, FILE * outfile, char ** error_msg, int * 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
orBOOLECTOR_PARSE_ERROR
if a parse error occurred.

int
boolector_parse_smt1
(Btor * btor, FILE * infile, const char * infile_name, FILE * outfile, char ** error_msg, int * status)¶ Parse input file in SMTLIB 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 (right now SMTLIB v1 only) the function returns either
BOOLECTOR_SAT
,BOOLECTOR_UNSAT
orBOOLECTOR_UNKNOWN
, otherwise it always returnsBOOLECTOR_UNKNOWN
. If a parse error occurs the function returnsBOOLECTOR_PARSE_ERROR
.

int
boolector_parse_smt2
(Btor * btor, FILE * infile, const char * infile_name, FILE * outfile, char ** error_msg, int * status)¶ Parse input file in SMTLIB 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: BOOLECTOR_UNKNOWN
orBOOLECTOR_PARSE_ERROR
if a parse error occurred.

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 SMTLIB v2 format for printing models.
boolector_print_model (btor, "smt2", stdout);
A possible model would be:
(model (definefun x () (_ BitVec 8) #b00000100) (definefun y () (_ BitVec 8) #b00010101) (definefun 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.

BoolectorNode *
boolector_read
(Btor * btor, BoolectorNode * n_array, BoolectorNode * n_index)¶ Create a read on array
n_array
at positionn_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 ofn_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.
See also

void
boolector_release_sort
(Btor * btor, BoolectorSort sort)¶ Release sort (decrements reference counter).
Parameters:  btor – Boolector instance.
 sort – Sort to be released.

void
boolector_reset_assumptions
(Btor * btor)¶ Resets all added assumptions.
Parameters:  btor – Boolector instance.
See also

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.
Given bit vector node
n1
, the value it represents is the number of bits by which noden0
is rotated to the left.Parameters:  btor – Boolector instance.
 n0 – First bit vector operand where the bit width is a power of two and greater than 1.
 n1 – Second bit vector operand with bit width log2 of the bit width of
n0
.
Returns: Bit vector with the same bit width as
n0
.

BoolectorNode *
boolector_ror
(Btor * btor, BoolectorNode * n0, BoolectorNode * n1)¶ Create a rotate right.
Given bit vector node
n1
, the value it represents is the number of bits by which noden0
is rotated to the right.Parameters:  btor – Boolector instance.
 n0 – First bit vector operand where the bit width is a power of two and greater than 1.
 n1 – Second bit vector operand with bit width log2 of the bit width of
n0
.
Returns: Bit vector with the same bit width as
n0
.

BoolectorNode *
boolector_saddo
(Btor * btor, BoolectorNode * n0, BoolectorNode * n1)¶ Create a signed bit vector addition overflow detection.
The parameters
n0
andn1
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
andn1
overflows in case both operands are treated signed.

int
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 viaboolector_assume()
. Note that assertions and assumptions are combined by booleanand
.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 andBOOLECTOR_UNSAT
if the instance is unsatisfiable.

BoolectorNode *
boolector_sdiv
(Btor * btor, BoolectorNode * n0, BoolectorNode * n1)¶ Create signed division.
The parameters
n0
andn1
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
andb
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 onboolector_udiv()
.

BoolectorNode *
boolector_sdivo
(Btor * btor, BoolectorNode * n0, BoolectorNode * n1)¶ Create a signed bit vector division overflow detection.
The parameters
n0
andn1
must have the same bit width. An overflow can happen ifn0
represents INT_MIN andn1
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
andn1
overflows in case both operands are treated signed.Note
Unsigned division cannot overflow.

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 viaboolector_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)
 generate model for asserted expressions only (
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
Incremental mode for SMT1. Stop after first satisfiable formula (value
: 1) or solve all formulas (value
: 2).Note that currently, incremental mode while parsing an input file is only supported for SMTLIB v1 input.BTOR_OPT_INPUT_FORMAT
If unspecified, Boolector automatically detects the input file format while parsing.BTOR_OPT_OUTPUT_NUMBER_FORMAT
Force output number format (value
: binary: 0, hexadecimal: 1, decimal: 2).Boolector uses binary by default.BTOR_OPT_OUTPUT_FORMAT
Boolector uses BTOR by default.BTOR_OPT_ENGINE
Set solver engine (value
: BTOR_ENGINE_FUN: 0, BTOR_ENGINE_SLS: 1, BTOR_ENGINE_PROP: 2).Boolector uses BTOR_ENGINE_FUN by default.BTOR_OPT_SAT_ENGINE
Set sat solver engine (value
: BTOR_SAT_ENGINE_LINGELING, BTOR_SAT_ENGINE_PICOSAT, BTOR_SAT_ENGINE_MINISAT).Available option values and default values depend on the sat solvers configured.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
: 03) 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_ALL
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_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.Boolector uses BTOR_DP_QSORT_JUST by default. BTOR_DP_QSORT_JUST (0): order by score, highest score first
 BTOR_DP_QSORT_ASC (1): order by input id, ascending
 BTOR_DP_QSORT_DESC (2): 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.Boolector uses BTOR_JUST_HEUR_BRANCH_MIN_APP by default. BTOR_JUST_HEUR_LEF (0): always choose left branch
 BTOR_JUST_HEUR_BRANCH_MIN_APP (1): choose branch with minimum number of applies
 BTOR_JUST_HEUR_BRANCH_MIN_DEP (2): choose branch with minimum depth
BTOR_OPT_FUN_LAZY_SYNTHESIZE
Enable (
value
: 1) or disable (value
: 0) lazy synthesis of bit vector expressions.BTOR_OPT_FUN_EAGER_LEMMAS
Enable (value
: 1) or disable (value
: 0) eager generation lemmas.If enabled, in each refinement iteration, lemmas for all possible conflicts for the candidate model are generated (rather than generating one single lemma per refinement iteration).
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
Set move strategy for SLS engine.Boolector uses BTOR_SLS_STRAT_BEST_MOVE by default. BTOR_SLS_STRAT_BEST_MOVE (0): always choose best score improving move
 BTOR_SLS_STRAT_RAND_WALK (1): always choose random walk weighted by score
 BTOR_SLS_STRAT_FIRST_BEST_MOVE (2): always choose first best move (no matter if any other move is better)
 BTOR_SLS_STRAT_BEST_SAME_MOVE (3): 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 (4): 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) groupwise 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) rangewise bitflip 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) segmentwise bitflip 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
Choose mode for path selection.
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 ifthenelse 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 ifthenelse 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 ifthenelse 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 bitvector) is downpropagated 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.
Parameters:  btor – Boolector instance.
 opt – Option opt.
 val – Option value.

int
boolector_set_sat_solver
(Btor * btor, const char * solver)¶ Set the SAT solver to use.
Currently, we support
Lingeling
,PicoSAT
, andMiniSAT
as string value ofsolver
(case insensitive). This is however only possible if the corresponding solvers were enabled at compile time. Call this function afterboolector_new()
.Parameters:  btor – Boolector instance
 solver – Solver identifier string.
Returns: Nonzero value if setting the SAT solver was successful.

int
boolector_set_sat_solver_lingeling
(Btor * btor, const char * optstr, int nofork)¶ Use Lingeling as SAT solver.
This function is only available if Lingeling was enabled at compile time. Call this function after
boolector_new()
.Parameters:  btor – Boolector instance.
 optstr – Lingeling option string.
 nofork – Do not use fork/clone for Lingeling.
Returns: Nonzero value if setting the SAT solver was successful.

int
boolector_set_sat_solver_minisat
(Btor * btor)¶ Use MiniSAT as SAT solver.
This function is only available if MiniSAT was enabled at compile time. Call this function after
boolector_new()
.Parameters:  btor – Boolector instance.
Returns: Nonzero value if setting the SAT solver was successful.

int
boolector_set_sat_solver_picosat
(Btor * btor)¶ Use PicoSAT as SAT solver.
This function is only available if PicoSAT was enabled at compile time. Call this function after
boolector_new()
.Parameters:  btor – Boolector instance.
Returns: Nonzero value if setting the SAT solver was successful.

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, int (*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

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, int width)¶ Create signed extension.
The bit vector
node
is padded withwidth
bits where the value depends on the value of the most significant bit of noden
.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
andn1
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
andn1
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.

int
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, andBOOLECTOR_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 indexupper
to indexlower
.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.
Given node
n1
, the value it represents is the number of zeroes shifted into noden0
from the right.Parameters:  btor – Boolector instance.
 n0 – First bit vector operand where the bit width is a power of two and greater than 1.
 n1 – Second bit vector operand with bit width log2 of the bit width of
n0
.
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
andn1
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
andn1
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
andn1
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 onboolector_urem()
.

BoolectorNode *
boolector_smulo
(Btor * btor, BoolectorNode * n0, BoolectorNode * n1)¶ Create signed multiplication overflow detection.
The parameters
n0
andn1
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
andn1
overflows in case both operands are treated signed.

BoolectorNode *
boolector_sra
(Btor * btor, BoolectorNode * n0, BoolectorNode * n1)¶ Create an arithmetic shift right.
Analogously to
boolector_srl()
, but whether zeroes or ones are shifted in depends on the most significant bit ofn0
.Parameters:  btor – Boolector instance.
 n0 – First bit vector operand where the bit width is a power of two and greater than 1.
 n1 – Second bit vector operand with bit width log2 of the bit width of
n0
.
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
andn1
must have the same bit width. Ifn1
is zero, then the result isn0
.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 thatn1
is zero, the result depends onboolector_urem()
.

BoolectorNode *
boolector_srl
(Btor * btor, BoolectorNode * n0, BoolectorNode * n1)¶ Create a logical shift right.
Given node
n1
, the value it represents is the number of zeroes shifted into noden0
from the left.Parameters:  btor – Boolector instance.
 n0 – First bit vector operand where the bit width is a power of two and greater than 1.
 n1 – Second bit vector operand with bit width log2 of the bit width of
n0
.
Returns: Bit vector with the same bit width as
n0
andn1
.

BoolectorNode *
boolector_ssubo
(Btor * btor, BoolectorNode * n0, BoolectorNode * n1)¶ Create a signed bit vector subtraction overflow detection.
The parameters
n0
andn1
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
andn1
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
andn1
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.

int
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

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
andn1
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
andn1
overflows in case both operands are treated unsigned.

BoolectorNode *
boolector_udiv
(Btor * btor, BoolectorNode * n0, BoolectorNode * n1)¶ Create unsigned division.
The parameters
n0
andn1
must have the same bit width. Ifn1
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 SMTLIB 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, int width)¶ Create unsigned extension.
The bit vector
node
is padded withwidth
* 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 symbolsymbol
.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 viaboolector_dump_btor()
andboolector_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 symbolsymbol
.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.
See also

void
boolector_uf_assignment
(Btor * btor, BoolectorNode * n_uf, char *** args, char *** values, int * 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 arrayvalues
. Arraysargs
andvalues
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
andvalues
.
Note
This function can only be called if
boolector_sat()
returnedBOOLECTOR_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
andn1
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
andn1
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
andn1
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
andn1
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
andn1
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
andn1
overflows in case both operands are treated unsigned.

BoolectorNode *
boolector_unsigned_int
(Btor * btor, unsigned u, BoolectorSort sort)¶ Create bit vector constant representing the unsigned integer
u
of sortsort
.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
andn1
must have the same bit width. Ifn1
is zero, then the result isn0
.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 ifn1
is zero, does not exactly comply with the SMTLIB 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
andn1
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
andn1
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 symbolsymbol
.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 viaboolector_dump_btor()
andboolector_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 symbolsymbol
.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.

BoolectorNode *
boolector_write
(Btor * btor, BoolectorNode * n_array, BoolectorNode * n_index, BoolectorNode * n_value)¶ Create a write on array
n_array
at positionn_index
with valuen_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 ofn_array
. The bit width ofn_value
must be the same as the bit width of the elements ofn_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 withn_value
.

BoolectorNode *
boolector_xnor
(Btor * btor, BoolectorNode * n0, BoolectorNode * n1)¶ Create a bit vector xnor.
The parameters
n0
andn1
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
andn1
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
.