Module Index: pyboolector

class pyboolector.Boolector

The class representing a Boolector instance.

UNKNOWN = 0

Value representing an ‘unknown’ result of a call to Sat().

SAT = 10

Value representing a ‘sat’ result of a call to Sat().

UNSAT = 20

Value representing an ‘unsat’ result of a call to Sat().

PARSE_ERROR = 1

Value representing a ‘parse error’ result of a call to Sat().

Add(a, b)

Create a bit vector addition.

Parameters a and b 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
Returns

A bit vector node with the same bit width as a and b.

Return type

BoolectorNode

And(a, b)

Create a bit vector and.

Parameters a and b 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
Returns

A bit vector node with the same bit width as a and b.

Return type

BoolectorNode

Apply(args, fun)

Create a function application on function fun with arguments args (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)

See Fun(), UF().

Parameters

  • args (list) – A list of arguments to be applied.

  • fun (BoolectorNode) – Function to apply arguments args to.

Returns

A function application on function fun with arguments args.

Return type

BoolectorNode

Array(sort, symbol=None)

Create a one-dimensional bit vector array variable of sort sort with symbol symbol.

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 via Dump(). 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 symbol symbol.

Return type

BoolectorNode

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

BoolectorSort

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 via Assert(), assumptions are discarded after each call to Sat(). 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 (uint32_t) – 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

Note

If Lingeling is used as SAT solver, Boolector can be cloned at any time, since Lingeling also supports cloning. However, if you use Clone() with MiniSAT or PicoSAT (no cloning suppport), Boolector can only be cloned prior to the first Sat() call.

Concat(a, b)

Create the concatenation of two bit vectors.

Parameters
Returns

A bit vector node with bitwidth bit width of a + bit width of b.

Return type

BoolectorNode

Cond(cond, a, b)

Create an if-then-else.

If condition cond is true, then a is returned, else b is returned. a and b 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 or b.

Return type

BoolectorNode

Const(c, width=1)

Create a bit vector constant of value c and bit width width.

Parameters

  • c (int, bool, str) – Value of the constant.

  • width (uint32_t) – Bit width of the constant.

Returns

A bit vector constant of value c and bit width width.

Return type

BoolectorNode

Note

Parameter width is only required if c is an integer.

ConstArray(sort, value)

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

Parameters

  • btor – Boolector instance.

  • sort – Array sort which maps bit-vectors to bit-vectors.

  • value – Value to initialize array.

Returns

Constant bit-vector array of sort sort.

See also

Array()

Copyright()
Returns

The copyright information.

Return type

str

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 SMT-LIB 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 and b 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
Returns

A bit vector node with bit width one.

Return type

BoolectorNode

Exists(params, body)

Create an existentially quantified formula.

See Param()

Parameters

  • params (list) – A list of (existentially quantified) parameters.

  • body (BoolectorNode) – Formula existentially quantified over params.

Returns

A formula body existentially quantified over params.

Return type

BoolectorNode

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().

Forall(params, body)

Create an universally quantified formula.

See Param()

Parameters

  • params (list) – A list of (universally quantified) parameters.

  • body (BoolectorNode) – Formula universally quantified over params.

Returns

A formula body universally quantified over params.

Return type

BoolectorNode

Fun(params, body)

Create a function with function body body, parameterized over params.

This kind of node is similar to macros in the SMT-LIB v2 standard.

See Param(), Apply().

Parameters

  • params (list) – A list of function parameters.

  • body (BoolectorNode) – Function body parameterized over params.

Returns

A function over parameterized expression body.

Return type

BoolectorNode

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 to codomain.

Return type

BoolectorSort

Get_opt(opt)

Get the Boolector option with name opt.

For a list of all available options, see Set_opt().

Parameters

opt (int32_t) – Option identifier.

Returns

Option with name opt.

Return type

BoolectorOpt

GitId()
Returns

The git commit sha.

Return type

str

Iff(a, b)

Create a Boolean equivalence.

Parameters a and b must have bit width one (see Automatic Constant Conversion).

Parameters
Returns

A Boolean equivalence a <=> b.

Return type

BoolectorNode

Implies(a, b)

Create a Boolean implication.

Parameters a and b 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

BoolectorNode

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 and b 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
Returns

A bit vector node with the same bit width as a and b.

Return type

BoolectorNode

Nand(a, b)

Create a bit vector nand.

Parameters a and b must have the same bit width (see Automatic Constant Conversion).

Parameters
Returns

A bit vector node with the same bit width as a and b.

Return type

BoolectorNode

Ne(a, b)

Create a bit vector or array inequality.

Parameters a and b 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
Returns

A bit vector node with bit width one.

Return type

BoolectorNode

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 and b must have the same bit width (see Automatic Constant Conversion).

Parameters
Returns

A bit vector node with the same bit width as a and b.

Return type

BoolectorNode

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 and b 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
Returns

A bit vector node with the same bit width as a and b.

Return type

BoolectorNode

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.

See Fun(),

Apply().

Parameters

  • sort – Sort of the function parameter.

  • symbol (str) – Symbol of the function parameter.

Returns

A function parameter of sort sort.

Return type

BoolectorNode

Parse(infile, outfile=None)

Parse input file.

Input file format may be either BTOR, SMT-LIB v1, or SMT-LIB 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 or UNSAT) in the incremental case, and UNKNOWN otherwise. Return value status indicates a (known) status (SAT or UNSAT) as specified in the input file. In case of an error, an explanation of that error is stored in error_msg.

Pop(level)

Pop context levels.

Parameters

level – Number of levels to pop.

Note

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

See also

Assume()

Print_model(format='btor', outfile=None)

Print model to output file.

Supported model formats are Boolector’s own model format (“btor”) and SMT-LIB 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 variables x and y. 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 variable A, 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 SMT-LIB v2 format would be:

btor.Print_model(format="smt2")

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

  • format – Model output format (default: “btor”).

  • outfile (str) – Output file name (default: stdout).

Push(level)

Push new context levels.

Parameters

level – Number of context levels to create.

Note

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

See also

Assume()

Read(a, b)

Create a read on array a at position b (see Automatic Constant Conversion).

It is also possible to create a read as follows (see Python Operator Overloading):

read = a[b]
Parameters
Returns

A bit vector node with the same bitwidth as the elements of array a.

Return type

BoolectorNode

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

Repeat(a, n)

Create n concatenations of bit vector a.

Parameters

  • a (BoolectorNode) – Bit vector operand.

  • n (uint32_t) – The number of times node a should be repeated.

Returns

A bit vector node with bitwidth n * bit width of a.

Return type

BoolectorNode

Reset_assumptions()

Remove all assumptions added since the last Sat() call.

See Assume().

Rol(a, b)

Create a rotate left.

Given bit vector node b, the value it represents is the number of bits by which node a 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 of a.

Returns

A bit vector node with the same bit width as a.

Return type

BoolectorNode

Ror(a, b)

Create a rotate right.

Given bit vector node b, the value it represents is the number of bits by which node a 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 of a.

Returns

A bit vector node with the same bit width as a.

Return type

BoolectorNode

Saddo(a, b)

Create a signed bit vector addition overflow detection.

Parameters a and b must have the same bit width (see Automatic Constant Conversion).

Parameters
Returns

A bit vector node with bit width one, which indicates if the addition of a and b overflows in case both operands are treated as signed.

Return type

BoolectorNode

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 via Assume().

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

  • lod_limit (int32_t) – Limit for Lemmas on Demand (-1: unlimited).

  • sat_limit (int32_t) – Conflict limit for the SAT solver (-1: unlimited).

Returns

SAT if the input formula is satisfiable (under possibly given assumptions), UNSAT if it is unsatisfiable, and UNKNOWN if the instance could not be solved within given limits.

Note

Assertions and assumptions are combined via Boolean and.

See also

assignment

Sdiv(a, b)

Create a signed bit vector division.

Parameters a and b must have the same bit width (see Automatic Constant Conversion).

Parameters
Returns

A bit vector node with the same bit width as a and b.

Return type

BoolectorNode

Note

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

Sdivo(a, b)

Create a signed bit vector division overflow detection.

Parameters a and b must have the same bit width (see Automatic Constant Conversion). An overflow can occur if a represents INT_MIN and b represents -1.

Parameters
Returns

A bit vector node with bit width one, which indicates if the division of a and b overflows in case both operands are treated as signed.

Return type

BoolectorNode

Note

Unsigned bit vector division does not overflow.

Set_opt(opt, value)

Set option.

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

btor.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)

  • BTOR_OPT_INCREMENTAL

    Enable (value: 1) incremental mode.
    Note that incremental usage turns off some optimization techniques. Disabling incremental usage is currently not supported.

  • BTOR_OPT_INCREMENTAL_SMT1

    Set incremental mode for SMT-LIB v1 input.

    • BTOR_INCREMENTAL_SMT1_BASIC [default]: stop after first satisfiable formula

    • BTOR_INCREMENTAL_SMT1_CONTINUE: solve all formulas

  • BTOR_OPT_INPUT_FORMAT

    Force input file format.
    If unspecified, Boolector automatically detects the input file format while parsing.

    • BTOR_INPUT_FORMAT_BTOR: BTOR format

    • BTOR_INPUT_FORMAT_BTOR2: BTOR2 format

    • BTOR_INPUT_FORMAT_SMT1: SMT-LIB v1 format

    • BTOR_INPUT_FORMAT_SMT2: SMT-LIB v2 format

  • BTOR_OPT_OUTPUT_NUMBER_FORMAT

    Force output number format.

    • BTOR_OUTPUT_BASE_BIN [default]: binary

    • BTOR_OUTPUT_BASE_HEX: hexa-decimal

    • BTOR_OUTPUT_BASE_DEC: decimal

  • BTOR_OPT_OUTPUT_FORMAT

    Force output file format (value: BTOR: -1, SMT-LIB v1: 1, SMT-LIB v2: 2).

  • BTOR_OPT_ENGINE

    Set solver engine.

    • BTOR_ENGINE_FUN [default]: the default engine for all combinations of QF_AUFBV, uses lemmas on demand for QF_AUFBV and eager bit-blasting for QF_BV

    • BTOR_ENGINE_SLS: the score-based local search QF_BV engine

    • BTOR_ENGINE_PROP: the propagation-based local search QF_BV engine

    • BTOR_ENGINE_AIGPROP: the propagation-based local search QF_BV engine that operates on the bit-blasted formula (the AIG layer)

    • BTOR_ENGINE_QUANT: the quantifier engine (BV only)

  • BTOR_OPT_SAT_ENGINE

    Set sat solver engine.
    Available option values and default values depend on the sat solvers configured.

  • BTOR_OPT_AUTO_CLEANUP

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

  • BTOR_OPT_PRETTY_PRINT

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

  • BTOR_OPT_EXIT_CODES

    Enable (value:1) or disable (value:0) the use of Boolector exit codes (BOOLECTOR_SAT, BOOLECTOR_UNSAT, BOOLECTOR_UNKNOWN - see Macros).
    If disabled, on exit Boolector returns 0 if success (sat or unsat), and 1 in any other case.

  • BTOR_OPT_SEED

    Set seed for Boolector’s internal random number generator.
    Boolector uses 0 by default.

Simplifier Options:

  • BTOR_OPT_REWRITE_LEVEL

    Set the rewrite level (value: 0-3) of the rewriting engine.
    Boolector uses rewrite level 3 by default, rewrite levels are classified as follows:

    • 0: no rewriting

    • 1: term level rewriting

    • 2: more simplification techniques

    • 3: full rewriting/simplification

    Do not alter the rewrite level of the rewriting engine after creating expressions.

  • BTOR_OPT_SKELETON_PREPROC

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

  • BTOR_OPT_ACKERMANN

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

  • BTOR_OPT_BETA_REDUCE

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

  • BTOR_OPT_ELIMINATE_SLICES

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

  • BTOR_OPT_VAR_SUBST

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

  • BTOR_OPT_UCOPT

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

  • BTOR_OPT_MERGE_LAMBDAS

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

  • BTOR_OPT_EXTRACT_LAMBDAS

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

  • BTOR_OPT_NORMALIZE

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

  • BTOR_OPT_NORMALIZE_ADD

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

Fun Engine Options:

  • BTOR_OPT_FUN_PREPROP

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

  • BTOR_OPT_FUN_PRESLS

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

  • BTOR_OPT_FUN_DUAL_PROP

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

  • BTOR_OPT_FUN_DUAL_PROP_QSORT

    Set order in which inputs are assumed in dual propagation clone.

    • BTOR_DP_QSORT_JUST [default]: order by score, highest score first

    • BTOR_DP_QSORT_ASC: order by input id, ascending

    • BTOR_DP_QSORT_DESC: order by input id, descending

  • BTOR_OPT_FUN_JUST

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

  • BTOR_OPT_FUN_JUST_HEURISTIC

    Set heuristic that determines path selection for justification optimization.

    • BTOR_JUST_HEUR_BRANCH_MIN_APP [default]: choose branch with minimum number of applies

    • BTOR_JUST_HEUR_BRANCH_MIN_DEP: choose branch with minimum depth

    • BTOR_JUST_HEUR_LEFT: always choose left branch

  • BTOR_OPT_FUN_LAZY_SYNTHESIZE

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

  • BTOR_OPT_FUN_EAGER_LEMMAS

    Select mode for eager generation lemmas.

    • BTOR_FUN_EAGER_LEMMAS_NONE: do not generate lemmas eagerly (generate one single lemma per refinement iteration)

    • BTOR_FUN_EAGER_LEMMAS_CONF: only generate lemmas eagerly until the first conflict dependent on another conflict is found

    • BTOR_FUN_EAGER_LEMMAS_ALL: in each refinement iteration, generate lemmas for all conflicts

  • BTOR_OPT_PRINT_DIMACS

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

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

SLS Engine Options:

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

  • BTOR_OPT_SLS_STRATEGY

    Select move strategy for SLS engine.

    • BTOR_SLS_STRAT_BEST_MOVE: always choose best score improving move

    • BTOR_SLS_STRAT_RAND_WALK: always choose random walk weighted by score

    • BTOR_SLS_STRAT_FIRST_BEST_MOVE [default]: always choose first best move (no matter if any other move is better)

    • BTOR_SLS_STRAT_BEST_SAME_MOVE: determine move as best move even if its score is not better but the same as the score of the previous best move

    • BTOR_SLS_STRAT_ALWAYS_PROP: always choose propagation move (and recover with SLS move in case of conflict)

  • BTOR_OPT_SLS_JUST

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

  • BTOR_OPT_SLS_MOVE_GW

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

  • BTOR_OPT_SLS_MOVE_RANGE

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

  • BTOR_OPT_SLS_MOVE_SEGMENT

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

  • BTOR_OPT_SLS_MOVE_RAND_WALK

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

  • BTOR_OPT_SLS_PROB_MOVE_RAND_WALK

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

  • BTOR_OPT_SLS_MOVE_RAND_ALL

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

  • BTOR_OPT_SLS_MOVE_RAND_RANGE

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

  • BTOR_OPT_SLS_MOVE_PROP

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

  • BTOR_OPT_SLS_MOVE_PROP_N_PROP

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

  • BTOR_OPT_SLS_MOVE_PROP_N_SLS

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

  • BTOR_OPT_SLS_MOVE_PROP_FORCE_RW

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

  • BTOR_OPT_SLS_MOVE_INC_MOVE_TEST

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

  • BTOR_OPT_SLS_MOVE_RESTARTS

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

  • BTOR_OPT_SLS_MOVE_RESTARTS

    Enable (value: 1) or disable (value: 0) heuristic (bandit scheme) for selecting root constraints.
    If disabled, candidate root constraints are selected randomly.

Prop Engine Options:

  • BTOR_OPT_PROP_NPROPS

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

  • BTOR_OPT_PROP_USE_RESTARTS

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

  • BTOR_OPT_PROP_USE_RESTARTS

    Enable (value: 1) or disable (value: 0) heuristic (bandit scheme) for selecting root constraints.
    If enabled, root constraint selection via bandit scheme is based on a scoring scheme similar to the one employed in the SLS engine.
    If disabled, candidate root constraints are selected randomly.

  • BTOR_OPT_PROP_PATH_SEL

    Select mode for path selection.

    • BTOR_PROP_PATH_SEL_CONTROLLING: select path based on controlling inputs

    • BTOR_PROP_PATH_SEL_ESSENTIAL [default]: select path based on essential inputs

    • BTOR_PROP_PATH_SEL_RANDOM: select path based on random inputs

  • BTOR_OPT_PROP_PROB_USE_INV_VALUE

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

  • BTOR_OPT_PROP_PROB_FLIP_COND

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

  • BTOR_OPT_PROP_PROB_FLIP_COND_CONST

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

  • BTOR_OPT_PROP_FLIP_COND_CONST_DELTA

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

  • BTOR_OPT_PROP_FLIP_COND_CONST_NPATHSEL

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

  • BTOR_OPT_PROP_PROB_SLICE_KEEP_DC

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

  • BTOR_OPT_PROP_PROB_CONC_FLIP

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

  • BTOR_OPT_PROP_PROB_SLICE_FLIP

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

  • BTOR_OPT_PROP_PROB_EQ_FLIP

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

  • BTOR_OPT_PROP_PROB_AND_FLIP

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

  • BTOR_OPT_PROP_NO_MOVE_ON_CONFLICT

    Do not perform a propagation move when running into a conflict during inverse computation.
    (This is the default behavior for the SLS engine when propagation moves are enabled, where a conflict triggers a recovery by means of a regular SLS move.)

AIGProp Engine Options:

  • BTOR_OPT_AIGPROP_USE_RESTARTS

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

  • BTOR_OPT_AIGPROP_USE_RESTARTS

    Enable (value: 1) or disable (value: 0) heuristic (bandit scheme) for selecting root constraints.
    If enabled, root constraint selection via bandit scheme is based on a scoring scheme similar to the one employed in the SLS engine.
    If disabled, candidate root constraints are selected randomly.

  • BTOR_OPT_QUANT_SYNTH

Select synthesis mode for Skolem functions.

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

  • BTOR_QUANT_SYNTH_EL: use enumerative learning to synthesize skolem functions

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

  • BTOR_QUANT_SYNTH_EL_ELMC: chain BTOR_QUANT_SYNTH_EL and BTOR_QUANT_SYNTH_ELMC approaches to synthesize skolem functions

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

  • BTOR_OPT_QUANT_DUAL_SOLVER

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

  • BTOR_OPT_QUANT_SYNTH_LIMIT

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

  • BTOR_OPT_SYNTH_QI

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

  • BTOR_OPT_QUANT_DER

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

  • BTOR_OPT_QUANT_CER

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

  • BTOR_OPT_QUANT_MINISCOPE

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

Parameters

  • opt (int32_t) – Option identifier.

  • value (uint32_t) – Option value.

Set_sat_solver(solver, clone=True)

Set the SAT solver to use.

E.g.,

btor = Boolector()
btor.Set_sat_solver("MiniSAT")

Option clone enables non-incremental 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

  • solver (str) – Solver identifier string.

  • clone (bool) – Force non-incremental SAT solver usage.

Note

Parameter clone is 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. Arguments args to fun may be passed as a single Python object (in case that fun 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 with width bits, where the padded value depends on the value of the most significant bit of node n.

Parameters

  • n (BoolectorNode) – A bit vector node.

  • width (uint32_t) – Number of bits to pad.

Returns

A bit vector extended by width bits.

Return type

BoolectorNode

Sgt(a, b)

Create a signed greater than.

Parameters a and b must have the same bit width (see Automatic Constant Conversion).

Parameters
Returns

A bit vector node with bit width one.

Return type

BoolectorNode

Sgte(a, b)

Create a signed greater than or equal.

Parameters a and b must have the same bit width (see Automatic Constant Conversion).

Parameters
Returns

A bit vector node with bit width one.

Return type

BoolectorNode

Simplify()

Simplify current input formula.

Returns

SAT if the input formula was simplified to true, UNSAT if it was simplified to false, and UNKNOWN, 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 index upper to index lower.

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 (uint32_t) – Upper index, which must be greater than or equal to zero, and less than the bit width of node n.

  • lower (uint32_t) – 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

BoolectorNode

Sll(a, b)

Create a logical shift left.

Given bit vector node b, the value it represents is the number of zeroes shifted into node a 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 of a.

Returns

A bit vector node with the same bit width as a.

Return type

BoolectorNode

Slt(a, b)

Create a signed less than.

Parameters a and b must have the same bit width (see Automatic Constant Conversion).

Parameters
Returns

A bit vector node with bit width one.

Return type

BoolectorNode

Slte(a, b)

Create a signed less than or equal.

Parameters a and b must have the same bit width (see Automatic Constant Conversion).

Parameters
Returns

A bit vector node with bit width one.

Return type

BoolectorNode

Smod(a, b)

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

Parameters a and b must have the same bit width (see Automatic Constant Conversion).

If b is zero, the result depends on Urem().

Parameters
Returns

A bit vector node with the same bit width as a and b.

Return type

BoolectorNode

Smulo(a, b)

Create a signed bit vector multiplication overflow detection.

Parameters a and b must have the same bit width (see Automatic Constant Conversion).

Parameters
Returns

A bit vector node with bit width one, which indicates if the multiplication of a and b overflows in case both operands are treated as signed.

Return type

BoolectorNode

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 node a (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 of a.

Returns

A bit vector node with the same bit width as a.

Return type

BoolectorNode

Srem(a, b)

Create a signed remainder.

Parameters a and b must have the same bit width (see Automatic Constant Conversion). If b is 0, the result of the unsigned remainder is a. If b is 0, the result of the unsigned remainder is a.

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 that b is zero, the result depends on Urem().

Parameters
Returns

A bit vector node with the same bit width as a and b.

Return type

BoolectorNode

Srl(a, b)

Create a logical shift right.

Given bit vector node b, the value it represents is the number of zeroes shifted into node a 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 of a.

Returns

A bit vector node with the same bit width as a.

Return type

BoolectorNode

Ssubo(a, b)

Create a signed bit vector subtraction overflow detection.

Parameters a and b must have the same bit width (see Automatic Constant Conversion).

Parameters
Returns

A bit vector node with bit width one, which indicates if the subtraction of a and b overflows in case both operands are treated as signed.

Return type

BoolectorNode

Sub(a, b)

Create a bit vector subtraction.

Parameters a and b 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
Returns

A bit vector node with the same bit width as a and b.

Return type

BoolectorNode

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 symbol symbol.

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 via Dump(). A symbol must be unique but may be None in case that no symbol should be assigned.

See Apply(), FunSort().

Parameters

  • sort (BoolectorSort) – Sort of the uninterpreted function.

  • symbol (str) – Name of the uninterpreted function.

Returns

A function over parameterized expression body.

Return type

BoolectorNode

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 and b must have the same bit width (see Automatic Constant Conversion).

Parameters
Returns

A bit vector node with bit width one, which indicates if the addition of a and b overflows in case both operands are treated as unsigned.

Return type

BoolectorNode

Udiv(a, b)

Create an unsigned bit vector division.

Parameters a and b must have the same bit width (see Automatic Constant Conversion). If b 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
Returns

A bit vector node with the same bit width as a and b.

Return type

BoolectorNode

Note

This behavior (division by zero returns -1) does not exactly comply with the SMT-LIB 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.

Uext(n, width)

Create unsigned extension.

Bit vector node n is padded with width zeroes.

Parameters

  • n (BoolectorNode) – A bit vector node.

  • width (uint32_t) – Number of zeros to pad.

Returns

A bit vector extended by width zeroes.

Return type

BoolectorNode

Ugt(a, b)

Create an unsigned greater than.

Parameters a and b 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
Returns

A bit vector node with bit width one.

Return type

BoolectorNode

Ugte(a, b)

Create an unsigned greater than or equal.

Parameters a and b 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
Returns

A bit vector node with bit width one.

Return type

BoolectorNode

Ult(a, b)

Create an unsigned less than.

Parameters a and b 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
Returns

A bit vector node with bit width one.

Return type

BoolectorNode

Ulte(a, b)

Create an unsigned less than or equal.

Parameters a and b 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
Returns

A bit vector node with bit width one.

Return type

BoolectorNode

Umulo(a, b)

Create an unsigned bit vector multiplication overflow detection.

Parameters a and b must have the same bit width (see Automatic Constant Conversion).

Parameters
Returns

A bit vector node with bit width one, which indicates if the multiplication of a and b overflows in case both operands are treated as unsigned.

Return type

BoolectorNode

Urem(a, b)

Create an unsigned remainder.

Parameters a and b must have the same bit width (see Automatic Constant Conversion). If b is 0, the result of the unsigned remainder is a.

It is also possible to create an unsigned remainder as follows (see Python Operator Overloading):

bvurem = a % b
Parameters
Returns

A bit vector node with the same bit width as a and b.

Return type

BoolectorNode

Note

As in Udiv(), the behavior if b is 0 does not exactly comply to the SMT-LIB 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.

Usubo(a, b)

Create an unsigned bit vector subtraction overflow detection.

Parameters a and b must have the same bit width (see Automatic Constant Conversion).

Parameters
Returns

A bit vector node with bit width one, which indicates if the subtraction of a and b overflows in case both operands are treated as unsigned.

Return type

BoolectorNode

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 via Dump(). 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

BoolectorNode

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.

Version()
Returns

The version number.

Return type

str

Write(array, index, value)

Create a write on array array at position index with value value (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 of array. The bit width of value must be the same as the bit width of the elements of array.

Parameters
Returns

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

Return type

BoolectorNode

Xnor(a, b)

Create a bit vector xnor.

Parameters a and b must have the same bit width (see Automatic Constant Conversion).

Parameters
Returns

A bit vector node with the same bit width as a and b.

Return type

BoolectorNode

Xor(a, b)

Create a bit vector xor.

Parameters a and b 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
Returns

A bit vector node with the same bit width as a and b.

Return type

BoolectorNode

class pyboolector.BoolectorNode

The class representing a Boolector node.

btor

The Boolector instance this node is associated with.

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 SMT-LIB 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() returned SAT.

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 via Dump().

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.

The Python API of the SMT solver Boolector.

class pyboolector.BoolectorArrayNode

Bases: pyboolector.BoolectorNode

The class representing a Boolector array node.

index_width

The bit with of the Boolector array node indices.

class pyboolector.BoolectorBVNode

Bases: pyboolector.BoolectorNode

The class representing a Boolector bit vector node.

class pyboolector.BoolectorConstNode

Bases: pyboolector.BoolectorBVNode

The class representing Boolector constant nodes.

bits

The bit string of a Boolector constant node.

exception pyboolector.BoolectorException(msg)

Bases: Exception

The class representing a Boolector exception.

class pyboolector.BoolectorExistsNode

Bases: pyboolector.BoolectorQuantNode

The class representing a Boolector existentially quantified node.

class pyboolector.BoolectorForallNode

Bases: pyboolector.BoolectorQuantNode

The class representing a Boolector universally quantified node.

class pyboolector.BoolectorFunNode

Bases: pyboolector.BoolectorNode

The class representing a Boolector function node.

arity

The arity of a Boolector function node.

class pyboolector.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.

class pyboolector.BoolectorOptions

Bases: object

The class representing a Boolector option iterator (see Options()).

class pyboolector.BoolectorQuantNode

Bases: pyboolector.BoolectorBVNode

The class representing a Boolector quantified node.

is_exists()
Returns

True if node is an existential quantifier.

Return type

Bool

is_forall()
Returns

True if node is a universal quantifier.

Return type

Bool

class pyboolector.BoolectorSort

Bases: object

The class representing a Boolector sort.