Module Index: boolector¶

class
boolector.
Boolector
¶ Bases:
object
The class representing a Boolector instance.

Add
(a, b)¶ Create a bit vector addition.
Parameters
a
andb
must have the same bit width (see Automatic Constant Conversion).It is also possible to create an addition as follows (see Python Operator Overloading):
bvadd = a + b
Parameters:  a (
BoolectorNode
) – First bit vector operand.  b (
BoolectorNode
) – Second bit vector operand.
Returns: A bit vector node with the same bit width as
a
andb
.Return type:  a (

And
(a, b)¶ Create a bit vector and.
Parameters
a
andb
must have the same bit width (see Automatic Constant Conversion).It is also possible to create an and as follows (see Python Operator Overloading):
bvand = a & b
Parameters:  a (
BoolectorNode
) – First bit vector operand.  b (
BoolectorNode
) – Second bit vector operand.
Returns: A bit vector node with the same bit width as
a
andb
.Return type:  a (

Apply
(args, fun)¶ Create a function application on function
fun
with argumentsargs
(see Automatic Constant Conversion).It is also possible to create a function application as follows (see Python Operator Overloading):
app = fun(arg_0, ..., arg_n)
Parameters:  args (list) – A list of arguments to be applied.
 fun (
BoolectorNode
) – Function to apply argumentsargs
to.
Returns: A function application on function
fun
with argumentsargs
.Return type:

Array
(sort, symbol = None)¶ Create a onedimensional bit vector array variable of sort
sort
with symbolsymbol
.An array variable’s symbol is used as a simple means of identfication, either when printing a model via
Print_model()
, or generating file dumps viaDump()
. A symbol must be unique but may be None in case that no symbol should be assigned.Parameters:  sort (BoolectorSort) – Sort of the array elements.
 symbol (str) – Symbol of the array variable.
Returns: A bit vector array variable of sort
sort
with symbolsymbol
.Return type: 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 this function returns a fresh bit vector array variable.

ArraySort
(index, elem)¶ Create array sort.
See
Array()
.Parameters:  index – The sort of the array index.
 elem (
BoolectorSort
) – The sort of the array elements.
Returns: Array sort.
Return type:

Assert
(a, ...)¶ Add one or more constraints.
Added constraints can not be removed.
Parameters: a ( BoolectorNode
) – Bit vector expression with bit width 1.

Assume
(a, ...)¶  Add one or more assumptions.
You must enable Boolector’s incremental usage via
Set_opt()
before you can add assumptions. In contrast to assertions added viaAssert()
, assumptions are discarded after each call toSat()
. Assumptions and assertions are logicall combined via Boolean and. Assumption handling in Boolector is analogous to assumptions in MiniSAT.Parameters: a ( BoolectorNode
) – Bit vector expression with bit width 1.

BitVecSort
(width)¶ Create bit vector sort of bit width
width
.See
UF()
.Parameters: width (int) – Bit width. Returns: Bit vector sort of bit width width
.Return type: BoolectorSort

BoolSort
()¶ Create Boolean sort.
Currently, sorts in Boolector are used for uninterpreted functions, only.
See
UF()
.Returns: Sort of type Boolean. Return type: BoolectorSort

Clone
()¶ Clone an instance of Boolector.
The resulting Boolector instance is an exact (but disjunct) copy of its parent instance. Consequently, in a clone and its parent, nodes with the same id correspond to each other. Use
Match()
to match corresponding nodes.Returns: The exact (but disjunct) copy of a Boolector instance. Return type: Boolector

Concat
(a, b)¶ Create the concatenation of two bit vectors.
Parameters:  a (
BoolectorNode
) – First bit vector operand.  b (
BoolectorNode
) – Second bit vector operand.
Returns: A bit vector node with bitwidth
bit width of a + bit width of b
.Return type:  a (

Cond
(cond, a, b)¶ Create an ifthenelse.
If condition
cond
is true, thena
is returned, elseb
is returned.a
andb
must be either both arrays or both bit vectors (see Automatic Constant Conversion).Parameters:  cond (
BoolectorNode
) – Bit vector condition with bit width one.  a (
BoolectorNode
) – Array or bit vector operand representing the then case.  b (
BoolectorNode
) – Array or bit vector operand representing the else case.
Returns: Either
a
orb
.Return type:  cond (

Const
(c, width = 1)¶ Create a bit vector constant of value
c
and bit widthwidth
.Parameters: Returns: A bit vector constant of value
c
and bit widthwidth
.Return type: Note
Parameter
width
is only required ifc
is an integer.

Dec
(n)¶ Create a bit vector expression that decrements bit vector
n
by one.Parameters: n ( BoolectorNode
) – A bit vector node.Returns: A bit vector with the same bit width as n
, decremented by one.Return type: BoolectorNode

Dump
(format = "btor", outfile = None)¶ Dump input formula to output file.
Parameters:  format (str.) – A file format identifier string (use ‘btor’ for BTOR, ‘smt2’ for SMTLIB v2, ‘aig’ for binary AIGER (QF_BV only), and ‘aag’ for ASCII AIGER (QF_BV only)).
 outile – Output file name (default: stdout).

Eq
(a, b)¶ Create a bit vector or array equality.
Parameters
a
andb
are either bit vectors with the same bit width, or arrays of the same type (see Automatic Constant Conversion).It is also possible to create an equality as follows (see Python Operator Overloading):
eq = a == b
Parameters:  a (
BoolectorNode
) – First bit vector operand.  b (
BoolectorNode
) – Second bit vector operand.
Returns: A bit vector node with bit width one.
Return type:  a (

Failed
(a, ...)¶ Determine if any of the given assumptions are failed assumptions.
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.
See
Assume()
.Parameters: a ( BoolectorNode
) – Bit vector expression with bit width 1.Returns: list of boolean values, where True indicates that the assumption at given index is failed, and false otherwise. Return type: list(bool)

Fixate_assumptions
()¶ Add all assumptions added since the last
Sat()
call as assertions.See
Assume()
.

Fun
(params, body)¶ Create a function with function body
body
, parameterized overparams
.This kind of node is similar to macros in the SMTLIB v2 standard.
Parameters:  params (list) – A list of function parameters.
 body (
BoolectorNode
) – Function body parameterized overparams
.
Returns: A function over parameterized expression
body
.Return type: Note
As soon as a parameter is bound to a function, it can not be reused in other functions. Call a function via
Apply()
.

FunSort
(domain, codomain)¶ Create function sort.
See
UF()
.Parameters:  domain (list) – A list of all the function arguments’ sorts.
 codomain (
BoolectorSort
) – The sort of the function’s return value.
Returns: Function sort, which maps
domain
tocodomain
.Return type:

Get_opt
(opt)¶ Get the Boolector option with name
opt
.For a list of all available options, see
Set_opt()
.Parameters: opt (str) – Option name. Returns: Option with name opt
.Return type: BoolectorOpt

Iff
(a, b)¶ Create a Boolean equivalence.
Parameters
a
andb
must have bit width one (see Automatic Constant Conversion).Parameters:  a (
BoolectorNode
) – First bit vector operand.  b (
BoolectorNode
) – Second bit vector operand.
Returns: A Boolean equivalence
a
<=>b
.Return type:  a (

Implies
(a, b)¶ Create a Boolean implication.
Parameters
a
andb
must have bit width one (see Automatic Constant Conversion).Parameters:  a (
BoolectorNode
) – Bit vector node representing the premise.  b (
BoolectorNode
) – Bit vector node representing the conclusion.
Returns: A Boolean implication
a
=>b
.Return type:  a (

Inc
(n)¶ Create a bit vector expression that increments bit vector
n
by one.Parameters: n ( BoolectorNode
) – A bit vector node.Returns: A bit vector with the same bit width as n
, incremented by one.Return type: BoolectorNode

Match
(n)¶ Retrieve the node matching given node
n
by id.This is intended to be used for handling expressions of a cloned instance (see
Clone()
).E.g.,
btor = Boolector() v = btor.Var(btor.BitVecSort(16), "x") clone = btor.Clone() v_cloned = clone.Match(v)
Parameters: n ( BoolectorNode
) – Boolector node.Returns: The Boolector node that matches given node n
by id.Return type: BoolectorNode
Note
Only nodes created before the
Clone()
call can be matched.

Match_by_symbol
(s)¶ Retrieve the node matching symbol
s
.E.g.,
btor = Boolector() v = btor.Var(btor.BitVecSort(16), "x") w = btor.Match_by_symbol("x")
Parameters: s (str) – Symbol. Returns: The Boolector node that matches by symbol s
.Return type: BoolectorNode

Mul
(a, b)¶ Create a bit vector multiplication.
Parameters
a
andb
must have the same bit width (see Automatic Constant Conversion).It is also possible to create a multiplication as follows (see Python Operator Overloading):
bvmul = a * b
Parameters:  a (
BoolectorNode
) – First bit vector operand.  b (
BoolectorNode
) – Second bit vector operand.
Returns: A bit vector node with the same bit width as
a
andb
.Return type:  a (

Nand
(a, b)¶ Create a bit vector nand.
Parameters
a
andb
must have the same bit width (see Automatic Constant Conversion).Parameters:  a (
BoolectorNode
) – First bit vector operand.  b (
BoolectorNode
) – Second bit vector operand.
Returns: A bit vector node with the same bit width as
a
andb
.Return type:  a (

Ne
(a, b)¶ Create a bit vector or array inequality.
Parameters
a
andb
are either bit vectors with the same bit width, or arrays of the same type (see Automatic Constant Conversion).It is also possible to create an inequality as follows (see Python Operator Overloading):
ne = a != b
Parameters:  a (
BoolectorNode
) – First bit vector operand.  b (
BoolectorNode
) – Second bit vector operand.
Returns: A bit vector node with bit width one.
Return type:  a (

Neg
(n)¶ Create the two’s complement of bit vector node
n
.It is also possible to create the two’s complement as follows (see Python Operator Overloading):
bvneg = n
Parameters: n ( BoolectorNode
) – A bit vector node.Returns: The two’s complement of bit vector node n
.Return type: BoolectorNode

Nor
(a, b)¶ Create a bit vector nor.
Parameters
a
andb
must have the same bit width (see Automatic Constant Conversion).Parameters:  a (
BoolectorNode
) – First bit vector operand.  b (
BoolectorNode
) – Second bit vector operand.
Returns: A bit vector node with the same bit width as
a
andb
.Return type:  a (

Not
(n)¶ Create the one’s complement of bit vector node
n
.It is also possible to create the one’s complement as follows (see Python Operator Overloading):
bvnot = ~n
Parameters: n ( BoolectorNode
) – A bit vector node.Returns: The one’s complement of bit vector node n
.Return type: BoolectorNode

Options
()¶ Get a
BoolectorOptions
iterator.E.g.,
btor = Boolector() options = btor.Options() for o in options: # do something
Returns: An iterator to iterate over all Boolector options. Return type: BoolectorOptions

Or
(a, b)¶ Create a bit vector or.
Parameters
a
andb
must have the same bit width (see Automatic Constant Conversion).It is also possible to create an or as follows (see Python Operator Overloading):
bvor = a  b
Parameters:  a (
BoolectorNode
) – First bit vector operand.  b (
BoolectorNode
) – Second bit vector operand.
Returns: A bit vector node with the same bit width as
a
andb
.Return type:  a (

Param
(sort, symbol = None)¶ Create a function parameter of sort
sort
.This kind of node is used to create parameterized expressions, which in turn are used to create functions. Once a parameter is bound to a function, it cannot be reused in other functions.
Parameters:  sort – Sort of the function parameter.
 symbol (str) – Symbol of the function parameter.
Returns: A function parameter of sort
sort
.Return type:

Parse
(infile, outfile = None)¶ Parse input file.
Input file format may be either BTOR, SMTLIB v1, or SMTLIB v2, the file type is detected automatically.
E.g.,
btor = Boolector() (result, status, error_msg) = btor.Parse("example.btor")
Parameters: infile (str) – Input file name. Returns: A tuple (result, status, error_msg), where return value result
indicates an error (PARSE_ERROR
) if any, and else denotes the satisfiability result (SAT
orUNSAT
) in the incremental case, andUNKNOWN
otherwise. Return valuestatus
indicates a (known) status (SAT
orUNSAT
) as specified in the input file. In case of an error, an explanation of that error is stored inerror_msg
.

Print_model
(format = "btor", outfile = None)¶ Print model to output file.
Supported model formats are Boolector’s own model format (“btor”) and SMTLIB v2 (“smt2”).
This function prints the model for all inputs to output file
outfile
, e.g.:btor.Print_model()
A possible model would be:
2 00000100 x 3 00010101 y 4[00] 01 A
which in this case prints the assignments of array variable
A
, and bit vector variablesx
andy
. For bit vector variables, the first column indicates the id of an input, the second column its assignment, and the third column its name (symbol), if any. Array variableA
, on the other hand, has id 4, is an array with index and element bit width of 2, and its value at index 0 is 1.The corresponding model in SMTLIB v2 format would be:
btor.Print_model(format="smt2")
(model (definefun x () (_ BitVec 8) #b00000100) (definefun y () (_ BitVec 8) #b00010101) (definefun y ( (y_x0 (_ BitVec 2))) (ite (= y_x0 #b00) #b01 #00)) )
Parameters:  format – Model output format (default: “btor”).
 outfile (str) – Output file name (default: stdout).

Read
(a, b)¶ Create a read on array
a
at positionb
(see Automatic Constant Conversion).It is also possible to create a read as follows (see Python Operator Overloading):
read = a[b]
Parameters:  a (
BoolectorNode
) – Array operand.  b (
BoolectorNode
) – Bit vector operand.
Returns: A bit vector node with the same bitwidth as the elements of array
a
.Return type:  a (

Redand
(n)¶ Create an and reduction of node
n
.All bits of node
n
are combined by an Boolean and.Parameters: n ( BoolectorNode
) – A bit vector node.Returns: The and reduction of node n
.Return type: BoolectorNode

Redor
(n)¶ Create an or reduction of node
n
.All bits of node
n
are combined by an Boolean or.Parameters: n ( BoolectorNode
) – A bit vector node.Returns: The or reduction of node n
.Return type: BoolectorNode

Redxor
(n)¶ Create an xor reduction of node
n
.All bits of node
n
are combined by an Boolean xor.Parameters: n ( BoolectorNode
) – A bit vector node.Returns: The xor reduction of node n
.Return type: BoolectorNode

Rol
(a, b)¶ Create a rotate left.
Given bit vector node
b
, the value it represents is the number of bits by which nodea
is rotated to the left (see Automatic Constant Conversion).Parameters:  a (
BoolectorNode
) – First bit vector operand where the bit width is a power of two and greater than 1.  b (
BoolectorNode
) – Second bit vector operand with bit width log2 of the bit width ofa
.
Returns: A bit vector node with the same bit width as
a
.Return type:  a (

Ror
(a, b)¶ Create a rotate right.
Given bit vector node
b
, the value it represents is the number of bits by which nodea
is rotated to the right (see Automatic Constant Conversion).Parameters:  a (
BoolectorNode
) – First bit vector operand where the bit width is a power of two and greater than 1.  b (
BoolectorNode
) – Second bit vector operand with bit width log2 of the bit width ofa
.
Returns: A bit vector node with the same bit width as
a
.Return type:  a (

Saddo
(a, b)¶ Create a signed bit vector addition overflow detection.
Parameters
a
andb
must have the same bit width (see Automatic Constant Conversion).Parameters:  a (
BoolectorNode
) – First bit vector operand.  b (
BoolectorNode
) – Second bit vector operand.
Returns: A bit vector node with bit width one, which indicates if the addition of
a
andb
overflows in case both operands are treated as signed.Return type:  a (

Sat
(lod_limit = 1, sat_limit = 1)¶ Solve an input formula.
An input formula is defined by constraints added via
Assert()
. You can guide the search for a solution to an input formula by making assumptions viaAssume()
.If you want to call this function multiple times, you must enable Boolector’s incremental usage mode via
Set_opt()
. Otherwise, this function may only be called once.You can limit the search by the number of lemmas generated (
lod_limit
) and the number of conflicts encountered by the underlying SAT solver (sat_limit
).Parameters: Returns: SAT
if the input formula is satisfiable (under possibly given assumptions),UNSAT
if it is unsatisfiable, andUNKNOWN
if the instance could not be solved within given limits.Note
Assertions and assumptions are combined via Boolean and.
See also

Sdiv
(a, b)¶ Create a signed bit vector division.
Parameters
a
andb
must have the same bit width (see Automatic Constant Conversion).Parameters:  a (
BoolectorNode
) – First bit vector operand.  b (
BoolectorNode
) – Second bit vector operand.
Returns: A bit vector node with the same bit width as
a
andb
.Return type: 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 onUdiv()
. a (

Sdivo
(a, b)¶ Create a signed bit vector division overflow detection.
Parameters
a
andb
must have the same bit width (see Automatic Constant Conversion). An overflow can occur ifa
represents INT_MIN andb
represents 1.Parameters:  a (
BoolectorNode
) – First bit vector operand.  b (
BoolectorNode
) – Second bit vector operand.
Returns: A bit vector node with bit width one, which indicates if the division of
a
andb
overflows in case both operands are treated as signed.Return type: Note
Unsigned bit vector division does not overflow.
 a (

Set_opt
(opt, value)¶ Set option.
E.g., given a Boolector instance
btor
, model generation is enabled viabtor.Set_opt(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:

Set_sat_solver
(solver, optstr = None, clone = True)¶ Set the SAT solver to use.
E.g.,
btor = Boolector() btor.Set_sat_solver("MiniSAT")
Option
clone
enables nonincremental SAT solver usage (for every SAT call) by means of internal SAT solver cloning. Use this option with caution (might have a positive or negative impact on overall performance).Parameters: Returns: True if setting the SAT solver was successful and False otherwise.
Return type: Note
Parameters
optstr
andclone
are currently only supported by Lingeling.

Set_term
(fun, args)¶ Set a termination callback function.
Use this function to force Boolector to prematurely terminate if callback function
fun
returns True. Argumentsargs
tofun
may be passed as a single Python object (in case thatfun
takes only one argument), a tuple, or a list of arguments.E.g.,
import time def fun1 (arg): # timeout after 1 sec. return time.time()  arg > 1.0 def fun2 (arg0, arg1): # do something and return True/False ... btor = Boolector() btor.Set_term(fun1, time.time()) btor.Set_term(fun1, (time.time(),)) btor.Set_term(fun1, [time.time()]) btor.Set_term(fun2, (arg0, arg1)) btor.Set_term(run2, [arg0, arg1])
Parameters:  fun – A python function.
 args – A function argument or a list or tuple of function arguments.

Sext
(n, width)¶ Create signed extension.
Bit vector node
n
is padded withwidth
bits, where the padded value depends on the value of the most significant bit of noden
.Parameters:  n (
BoolectorNode
) – A bit vector node.  width (int) – Number of bits to pad.
Returns: A bit vector extended by
width
bits.Return type:  n (

Sgt
(a, b)¶ Create a signed greater than.
Parameters
a
andb
must have the same bit width (see Automatic Constant Conversion).Parameters:  a (
BoolectorNode
) – First bit vector operand.  b (
BoolectorNode
) – Second bit vector operand.
Returns: A bit vector node with bit width one.
Return type:  a (

Sgte
(a, b)¶ Create a signed greater than or equal.
Parameters
a
andb
must have the same bit width (see Automatic Constant Conversion).Parameters:  a (
BoolectorNode
) – First bit vector operand.  b (
BoolectorNode
) – Second bit vector operand.
Returns: A bit vector node with bit width one.
Return type:  a (

Simplify
()¶ Simplify current input formula.
Returns: SAT
if the input formula was simplified to true,UNSAT
if it was simplified to false, andUNKNOWN
, otherwise.Note
Each call to
Sat()
simplifies the input formula as a preprocessing step.

Slice
(n, upper, lower)¶ Create a bit vector slice of node
n
from indexupper
to indexlower
.It is also possible to use Python slices on bit vectors as follows:
n[upper:lower] # creates slice with upper limit 'upper' and lower limit 'lower' n[upper:] # creates slice with upper limit 'upper' and lower limit 0 n[:lower] # creates slice with upper limit 'n.width  1' and lower limit 'lower' n[:] # creates copy of node 'n'
Parameters:  n (
BoolectorNode
) – A bit vector node.  upper (int) – Upper index, which must be greater than or equal to zero, and less than the bit width of node
n
.  lower (int) – Lower index, which must be greater than or equal to zero, and less than or equal to
upper
.
Returns: A Bit vector with bit width
upper
lower
+ 1.Return type:  n (

Sll
(a, b)¶ Create a logical shift left.
Given bit vector node
b
, the value it represents is the number of zeroes shifted into nodea
from the right (see Automatic Constant Conversion).It is also possible to create a logical shift left as follows (see Python Operator Overloading):
bvshl = a << b
Parameters:  a (
BoolectorNode
) – First bit vector operand where the bit width is a power of two and greater than 1.  b (
BoolectorNode
) – Second bit vector operand with bit width log2 of the bit width ofa
.
Returns: A bit vector node with the same bit width as
a
.Return type:  a (

Slt
(a, b)¶ Create a signed less than.
Parameters
a
andb
must have the same bit width (see Automatic Constant Conversion).Parameters:  a (
BoolectorNode
) – First bit vector operand.  b (
BoolectorNode
) – Second bit vector operand.
Returns: A bit vector node with bit width one.
Return type:  a (

Slte
(a, b)¶ Create a signed less than or equal.
Parameters
a
andb
must have the same bit width (see Automatic Constant Conversion).Parameters:  a (
BoolectorNode
) – First bit vector operand.  b (
BoolectorNode
) – Second bit vector operand.
Returns: A bit vector node with bit width one.
Return type:  a (

Smod
(a, b)¶ Create a signed remainder where its sign matches the sign of the divisor.
Parameters
a
andb
must have the same bit width (see Automatic Constant Conversion).If
b
is zero, the result depends onUrem()
.Parameters:  a (
BoolectorNode
) – First bit vector operand.  b (
BoolectorNode
) – Second bit vector operand.
Returns: A bit vector node with the same bit width as
a
andb
.Return type:  a (

Smulo
(a, b)¶ Create a signed bit vector multiplication overflow detection.
Parameters
a
andb
must have the same bit width (see Automatic Constant Conversion).Parameters:  a (
BoolectorNode
) – First bit vector operand.  b (
BoolectorNode
) – Second bit vector operand.
Returns: A bit vector node with bit width one, which indicates if the multiplication of
a
andb
overflows in case both operands are treated as signed.Return type:  a (

Sra
(a, b)¶ Create an arithmetic shift right.
Analogously to
Srl()
, but whether zeroes or ones are shifted in depends on the most significant bit of nodea
(see Automatic Constant Conversion).Parameters:  a (
BoolectorNode
) – First bit vector operand where the bit width is a power of two and greater than 1.  b (
BoolectorNode
) – Second bit vector operand with bit width log2 of the bit width ofa
.
Returns: A bit vector node with the same bit width as
a
.Return type:  a (

Srem
(a, b)¶ Create a signed remainder.
Parameters
a
andb
must have the same bit width (see Automatic Constant Conversion). Ifb
is 0, the result of the unsigned remainder isa
. Ifb
is 0, the result of the unsigned remainder isa
.Analogously to
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 thatb
is zero, the result depends onUrem()
.Parameters:  a (
BoolectorNode
) – First bit vector operand.  b (
BoolectorNode
) – Second bit vector operand.
Returns: A bit vector node with the same bit width as
a
andb
.Return type:  a (

Srl
(a, b)¶ Create a logical shift right.
Given bit vector node
b
, the value it represents is the number of zeroes shifted into nodea
from the left (see Automatic Constant Conversion).It is also possible to create a logical shift right as follows (see Python Operator Overloading):
bvshr = a >> b
Parameters:  a (
BoolectorNode
) – First bit vector operand where the bit width is a power of two and greater than 1.  b (
BoolectorNode
) – Second bit vector operand with bit width log2 of the bit width ofa
.
Returns: A bit vector node with the same bit width as
a
.Return type:  a (

Ssubo
(a, b)¶ Create a signed bit vector subtraction overflow detection.
Parameters
a
andb
must have the same bit width (see Automatic Constant Conversion).Parameters:  a (
BoolectorNode
) – First bit vector operand.  b (
BoolectorNode
) – Second bit vector operand.
Returns: A bit vector node with bit width one, which indicates if the subtraction of
a
andb
overflows in case both operands are treated as signed.Return type:  a (

Sub
(a, b)¶ Create a bit vector subtraction.
Parameters
a
andb
must have the same bit width (see Automatic Constant Conversion).It is also possible to create a subtraction as follows (see Python Operator Overloading):
bvsub = a  b
Parameters:  a (
BoolectorNode
) – First bit vector operand.  b (
BoolectorNode
) – Second bit vector operand.
Returns: A bit vector node with the same bit width as
a
andb
.Return type:  a (

Terminate
()¶ Determine if Boolector has been terminated (and/or terminate Boolector) via the previously configured termination callback function.
See
Set_term()
.:return True if termination condition is fulfilled, else False. :rtype: bool

UF
(sort, symbol)¶ Create an uninterpreted function with sort
sort
and symbolsymbol
.An uninterpreted function’s symbol is used as a simple means of identification, either when printing a model via
Print_model()
, or generating file dumps viaDump()
. A symbol must be unique but may be None in case that no symbol should be assigned.Parameters:  sort (BoolectorSort) – Sort of the uninterpreted function.
 symbol (str) – Name of the uninterpreted function.
Returns: A function over parameterized expression
body
.Return type: 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.

Uaddo
(a, b)¶ Create an unsigned bit vector addition overflow detection.
Parameters
a
andb
must have the same bit width (see Automatic Constant Conversion).Parameters:  a (
BoolectorNode
) – First bit vector operand.  b (
BoolectorNode
) – Second bit vector operand.
Returns: A bit vector node with bit width one, which indicates if the addition of
a
andb
overflows in case both operands are treated as unsigned.Return type:  a (

Udiv
(a, b)¶ Create an unsigned bit vector division.
Parameters
a
andb
must have the same bit width (see Automatic Constant Conversion). Ifa
is 0, the division’s result is 1.It is also possible to create an unsigned division as follows (see Python Operator Overloading):
bvudiv = a / b
Parameters:  a (
BoolectorNode
) – First bit vector operand.  b (
BoolectorNode
) – Second bit vector operand.
Returns: A bit vector node with the same bit width as
a
andb
.Return type: Note
This behavior (division by zero returns 1) does not exactly comply with the SMTLIB v1 and v2 standards, where division by zero is handled as an uninterpreted function. Our semantics are motivated by real circuits where division by zero cannot be uninterpreted and consequently returns a result.
 a (

Uext
(n, width)¶ Create unsigned extension.
Bit vector node
n
is padded withwidth
zeroes.Parameters:  n (
BoolectorNode
) – A bit vector node.  width (int) – Number of zeros to pad.
Returns: A bit vector extended by
width
zeroes.Return type:  n (

Ugt
(a, b)¶ Create an unsigned greater than.
Parameters
a
andb
must have the same bit width (see Automatic Constant Conversion).It is also possible to create an unsigned greater than as follows (see Python Operator Overloading):
ugt = a > b
Parameters:  a (
BoolectorNode
) – First bit vector operand.  b (
BoolectorNode
) – Second bit vector operand.
Returns: A bit vector node with bit width one.
Return type:  a (

Ugte
(a, b)¶ Create an unsigned greater than or equal.
Parameters
a
andb
must have the same bit width (see Automatic Constant Conversion).It is also possible to create an unsigned greater than or equal as follows (see Python Operator Overloading):
ugte = a >= b
Parameters:  a (
BoolectorNode
) – First bit vector operand.  b (
BoolectorNode
) – Second bit vector operand.
Returns: A bit vector node with bit width one.
Return type:  a (

Ult
(a, b)¶ Create an unsigned less than.
Parameters
a
andb
must have the same bit width (see Automatic Constant Conversion).It is also possible to create an unsigned less than as follows (see Python Operator Overloading):
lt = a < b
Parameters:  a (
BoolectorNode
) – First bit vector operand.  b (
BoolectorNode
) – Second bit vector operand.
Returns: A bit vector node with bit width one.
Return type:  a (

Ulte
(a, b)¶ Create an unsigned less than or equal.
Parameters
a
andb
must have the same bit width (see Automatic Constant Conversion).It is also possible to create an unsigned less than or equal as follows (see Python Operator Overloading):
lte = a <= b
Parameters:  a (
BoolectorNode
) – First bit vector operand.  b (
BoolectorNode
) – Second bit vector operand.
Returns: A bit vector node with bit width one.
Return type:  a (

Umulo
(a, b)¶ Create an unsigned bit vector multiplication overflow detection.
Parameters
a
andb
must have the same bit width (see Automatic Constant Conversion).Parameters:  a (
BoolectorNode
) – First bit vector operand.  b (
BoolectorNode
) – Second bit vector operand.
Returns: A bit vector node with bit width one, which indicates if the multiplication of
a
andb
overflows in case both operands are treated as unsigned.Return type:  a (

Urem
(a, b)¶ Create an unsigned remainder.
Parameters
a
andb
must have the same bit width (see Automatic Constant Conversion). Ifb
is 0, the result of the unsigned remainder isa
.It is also possible to create an unsigned remainder as follows (see Python Operator Overloading):
bvurem = a % b
Parameters:  a (
BoolectorNode
) – First bit vector operand.  b (
BoolectorNode
) – Second bit vector operand.
Returns: A bit vector node with the same bit width as
a
andb
.Return type: Note
As in
Udiv()
, the behavior ifb
is 0 does not exactly comply to the SMTLIB v1 and v2 standards, where the result ist handled as uninterpreted function. Our semantics are motivated by real circuits, where result can not be uninterpreted. a (

Usubo
(a, b)¶ Create an unsigned bit vector subtraction overflow detection.
Parameters
a
andb
must have the same bit width (see Automatic Constant Conversion).Parameters:  a (
BoolectorNode
) – First bit vector operand.  b (
BoolectorNode
) – Second bit vector operand.
Returns: A bit vector node with bit width one, which indicates if the subtraction of
a
andb
overflows in case both operands are treated as unsigned.Return type:  a (

Var
(sort, symbol = None)¶ Create a bit vector variable of sort
sort
.A variable’s symbol is used as a simple means of identification, either when printing a model via
Print_model()
, or generating file dumps viaDump()
. A symbol must be unique but may be None in case that no symbol should be assigned.Parameters:  sort – Sort of the variable.
 symbol (str) – Symbol of the variable.
Returns: A bit vector variable of sort
sort
.Return type: 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.

Write
(array, index, value)¶ Create a write on array
array
at positionindex
with valuevalue
(see Automatic Constant Conversion).The array is updated at exactly one position, all other elements remain unchanged. The bit width of
index
must be the same as the bit width of the indices ofarray
. The bit width ofvalue
must be the same as the bit width of the elements ofarray
.Parameters:  array (
BoolectorNode
) – Array operand.  index (
BoolectorNode
) – Bit vector index.  value (
BoolectorNode
) – Bit vector value.
Returns: An array where the value at
index
has been updated withvalue
.Return type:  array (

Xnor
(a, b)¶ Create a bit vector xnor.
Parameters
a
andb
must have the same bit width (see Automatic Constant Conversion).Parameters:  a (
BoolectorNode
) – First bit vector operand.  b (
BoolectorNode
) – Second bit vector operand.
Returns: A bit vector node with the same bit width as
a
andb
.Return type:  a (

Xor
(a, b)¶ Create a bit vector xor.
Parameters
a
andb
must have the same bit width (see Automatic Constant Conversion).It is also possible to create an xor as follows (see Python Operator Overloading):
bvxor = a ^ b
Parameters:  a (
BoolectorNode
) – First bit vector operand.  b (
BoolectorNode
) – Second bit vector operand.
Returns: A bit vector node with the same bit width as
a
andb
.Return type:  a (


class
boolector.
BoolectorArrayNode
¶ Bases:
boolector.BoolectorNode
The class representing a Boolector array node.

index_width
¶ The bit with of the Boolector array node indices.


class
boolector.
BoolectorBVNode
¶ Bases:
boolector.BoolectorNode
The class representing a Boolector bit vector node.

class
boolector.
BoolectorConstNode
¶ Bases:
boolector.BoolectorBVNode
The class representing Boolector constant nodes.

bits
¶ The bit string of a Boolector constant node.


exception
boolector.
BoolectorException
¶ Bases:
Exception
The class representing a Boolector exception.

class
boolector.
BoolectorFunNode
¶ Bases:
boolector.BoolectorNode
The class representing a Boolector function node.

arity
¶ The arity of a Boolector function node.


class
boolector.
BoolectorNode
¶ Bases:
object
The class representing a Boolector node.

Dump
(format = "btor", outfile = None)¶ Dump node to output file.
Parameters:  format (str) – A file format identifier string (use ‘btor’ for BTOR and ‘smt2’ for SMTLIB v2).
 outfile (str) – Output file name (default: stdout).

assignment
¶ The assignment of a Boolector node.
May be queried only after a preceding call to
Sat()
returnedSAT
.If the queried node is a bit vector, its assignment is represented as string. If it is an array, its assignment is represented as a list of tuples
(index, value)
. If it is a function, its assignment is represented as a list of tuples(arg_0, ..., arg_n, value)
.

symbol
¶ The symbol of a Boolector node.
A node’s symbol is used as a simple means of identfication, either when printing a model via
Print_model()
, or generating file dumps viaDump()
.

width
¶ The bit width of a Boolector node.
If the node is an array, this indicates the bit width of the array elements. If the node is a function, this indicates the bit with of the function’s return value.


class
boolector.
BoolectorOpt
¶ Bases:
object
The class representing a Boolector option.

desc
¶ The description of a Boolector option.

dflt
¶ The default value of a Boolector option.

lng
¶ The long name of a Boolector option.

max
¶ The maximum value of a Boolector option.

min
¶ The minimum value of a Boolector option.

shrt
¶ The short name of a Boolector option.

val
¶ The current value of a Boolector option.
