Boolector Python API documentation¶

Interface¶

Python interface

Quickstart¶

First, create a Boolector instance:
btor = Boolector()
You can configure this instance via Set_opt(). E.g., if you want to enable model generation:
btor.Set_opt(BTOR_OPT_MODEL_GEN, 1)
For a detailed description of all configurable options, see Set_opt().

Next you can either parse an input file, and/or generate expressions to be either asserted via Aassert(), or, if incremental usage is enabled, assumed via Assume() (analogously to MiniSAT). Note that Boolector’s internal design is motivated by hardware design, hence we do not distinguish between type ‘Boolean’ and type ‘bit vector of length 1’.

E.g., if you want to parse an input file “example.btor”, use Parse():
(result, status, error_msg) = btor.Parse("example.btor")
Incremental usage is not enabled, hence, if the parser does not encounter an error, it returns UNKNOWN (for a more detailed description of the parsers return values, see Parse()). However, if the parser encounters an error, it returns PARSE_ERROR, and an explanation of that error is stored in error_msg. If the input file specifies a (known) status of the input formula (either satisfiable or unsatisfiable), that status is stored in status.

As an example for generating and asserting expressions via Assert(), consider the following example:
0 < x <= 100, 0 < y <= 100, x * y < 100
Given the Boolector instance created above, we generate and assert the following expressions:
x = btor.Var(8, "x")
y = btor.Var(8, "y")

btor.Assert(0 < x)
btor.Assert(x <= 100)
btor.Assert(0 < y)
btor.Assert(y <= 100)
btor.Assert(x * y < 100)

umulo = btor.Umulo(x, y)  # overflow bit of x * y
btor.Assert(~umulo)       # do not allow overflows
After parsing an input file and/or asserting/assuming expressions, the satisfiability of the resulting formula can be determined via Sat(). If the resulting formula is satisfiable and model generation has been enabled via Set_opt(), you can either print the resulting model via Print_model(), or query assignments of bit vector and array variables or uninterpreted functions via assignment. Note that querying assignments is not limited to variables—you can query the assignment of any arbitrary expression.

E.g., given the example above, we first determine if the formula is satisfiable via Sat() (which it is):
result = btor.Sat()
Now you can either query the assignments of variables x and y
print(x.assignment)  # prints: 00000100
print(y.assignment)  # prints: 00010101
print("{} {}".format(x.symbol, x.assignment))  # prints: x 00000100
print("{} {}".format(y.symbol, y.assignment))  # prints: y 00010101
or print the resulting model via Print_model(). Boolector supports printing models in its own format (“btor”, the default) or in SMT-LIB v2 format (“smt2”):
btor.Print_model()
A possible model would be:
2 00000100 x
3 00010101 y
which in this case indicates the assignments of bit vector variables x and y. Note that the first column indicates the id of an input, the second column its assignment, and the third column its name (or symbol) if any. In the case that the formula includes arrays as input, their values at a certain index are indicated as follows:
4[00] 01 A
where A has id 4 and is an array with index and element bit width of 2, and its value at index 0 is 1.

Printing the above model in SMT-LIB v2 format:
btor.print_model (format="smt2")
A possible model would be:
(model
  (define-fun x () (_ BitVec 8) #b00000100)
  (define-fun y () (_ BitVec 8) #b00010101)
  (define-fun y (
   (y_x0 (_ BitVec 2)))
   (ite (= y_x0 #b00) #b01
     #00))
)

Python Operator Overloading¶

For convenience the Boolector Python API provides the following overloaded operators on bit vectors (BoolectorBVNode):

Arithmetic operators: + - * / %

x = btor.Var(32)
y = btor.Var(32)

bvadd  = x + y  # btor.Add(x, y)
bvsub  = x - y  # btor.Sub(x, y)
bvmul  = x * y  # btor.Mul(x, y)
bvudiv = x / y  # btor.Udiv(x, y)
bvurem = x % y  # btor.Urem(x, y)
bvneg  = -x     # btor.Neg(x)

Bitwise operators: ~ & | ^ << >>

z = btor.Var(5)

bvnot = ~x      # btor.Not(x)
bvand = x & y   # btor.And(x, y)
bvor  = x | y   # btor.Or(x, y)
bvxor = x ^ y   # btor.Xor(x, y)
bvshl = x << z  # btor.Sll(x, z)
bvshr = x >> z  # btor.Srl(x, z)

Comparison operators: < <= == != >= >

lt   = x < y   # btor.Ult(x, y)
lte  = x <= y  # btor.Ulte(x, y)
eq   = x == y  # btor.Eq(x, y)
ne   = x != y  # btor.Ne(x, y)
ugte = x >= y  # btor.Ugte(x, y)
ugt  = x > y   # btor.Ugt(x, y)

Python slices: It is possible to use Python slices on bit vectors (see Slice()), e.g.:

slice_5_2  = x[5:2]  # btor.Slice(x, 5, 2)
slice_5_0  = x[5:]   # btor.Slice(x, 5, 0)
slice_31_5 = x[:5]   # btor.Slice(x, x.width - 1, 5)
slice_31_0 = x[:]    # btor.Slice(x, x.width - 1, 0) -- copies variable 'x'

Further, the API also provides convenient ways to create reads (see Read()) on arrays, and function applications (see Apply()).

Reads on arrays:

a = btor.Array(8, 32)

read = a[x]  # btor.Read(a, x)

Function applications:

bv8 = btor.BitVecSort(8)
bv32 = btor.BitVecSort(32)
f = btor.UF(btor.FunSort([bv32, bv32], bv8))

app = f(x, y)  # btor.Apply([x, y], f)

Automatic Constant Conversion¶

For almost every method of Boolector that creates nodes, instead of passing arguments of the type BoolectorNode, the Python API allows to pass constants as arguments. The only requirement is that it must be possible to derive the bit width of the constant operands from the remaining operands. For example, binary operators like Add() operands may be a constant, and its bit width will be derived from the other non-constant operand, e.g.:
btor.Add(x, 42)         # btor.Add(x, btor.Const(42, x.width))
btor.And(0x2a, x)       # btor.And(btor.Const(0x2a, x.width), x)
btor.Udiv(0b101010, x)  # btor.Udiv(btor.Const(0b101010, x.width), x)
For all shift operations it is possible to define the shift width as constant, e.g.:
btor.Sll(x, 5)  # btor.Sll(x, btor.Const(5, math.ceil(math.log(x.width, 2))))
btor.Ror(x, 5)  # btor.Ror(x, btor.Const(5, math.ceil(math.log(x.width, 2))))
For operations on arrays all arguments may be constant (except the array itself) since the bit width of the operands can be derived from the array, e.g.:
btor.Read(a, 42)       # btor.Read(a, btor.Const(42, a.index_with))
btor.Write(a, 42, 10)  # btor.Write(a, btor.Const(42, a.index_width), btor.Const(10, a.width))
This also applies to the arguments of function applications, which can be derived from the function’s signature, e.g.:
btor.Apply([42, 10], f)  # btor.Apply([btor.Const(42, ...), btor.Const(10, ...)], f)
Note

Automatic constant conversion is not possible for the following operators: Not(), Neg(), Redor(), Redxor(), Redand(), Slice(), Uext(), Sext(), Inc(), Dec(), and Concat() as the bit with of the resulting node cannot be determined.

Options¶

Boolector can be configured either via Set_opt(), or via environment variables of the form:
BTOR<capitalized option name without '_'>=<value>
For a list and detailed descriptions of all available options, see Set_opt().

E.g., given a Boolector instance btor, model generation is enabled either via
btor.Set_opt(BTOR_OPT_MODEL_GEN, 1)
or via setting the environment variable
BTORMODELGEN=1

API Tracing¶

API tracing allows to record every call to Boolector’s public API. The resulting trace can be replayed and the replayed sequence behaves exactly like the original Boolector run. This is particularly useful for debugging purposes, as it enables replaying erroneous behaviour. API tracing can be enabled either via setting the environment variable BTORAPITRACE=<filename>.

E.g., given a Boolector instance ‘btor’, enabling API tracing is done as follows:
BTORAPITRACE="error.trace"

Internals¶

Boolector internally maintains a directed acyclic graph (DAG) of expressions. By asserting an expression, it will be permanently added to the formula. Assumptions, in contrast, are cleared after a call to Sat(). You can query assumptions that force a formula to be unsatisfiable via Failed().

Operators¶

Boolector internally describes expressions by means of a set of base operators as documented in BTOR. Boolector’s API, however, provides a richer set of operators for convenience, where non-base operators are internally rewritten to use base operators only. E.g., two’s complement (Neg()) is rewritten as one’s complement and addition of 1. Note that this behaviour is not influenced by the rewrite level chosen.

Rewriting¶

Boolector simplifies expressions and the expression DAG by means of rewriting and supports three so-called rewrite levels. Increasing rewrite levels increase the extent of rewriting performed, and a rewrite level of 0 is equivalent to disabling rewriting at all. Note that Boolector not only simplifies expressions during construction of the expression DAG—for each call to ref boolector_sat, various simplification techniques and rewriting phases are initiated. You can force Boolector to initiate rewriting and simplify the expression DAG via Simplify(). The rewrite level can be configured via Set_opt().

Examples¶

import os
import boolector
from boolector import Boolector

if __name__ == "__main__":
    b = Boolector() 

### Creating Boolector nodes

    # Sorts
    _boolsort = b.BoolSort()
    _bvsort   = b.BitVecSort(128)
    _arrsort  = b.ArraySort(_bvsort, _bvsort)
    _funsort  = b.FunSort([_boolsort, _boolsort, _bvsort, _bvsort], _boolsort)

    # Constants
    _const = b.Const("10010101")
    _zero  = b.Const(0, 128)
    _ones  = b.Const(-1, 129)
    _true  = b.Const(True)
    _false = b.Const(False)
    _one   = b.Const(1, 128)
    _uint  = b.Const(77, 128)
    _int   = b.Const(-77, 128)

    # Variables
    _var   = b.Var(_bvsort, "var_symbol")
    _param = b.Param(_bvsort, "param_symbol")  # used as function parameters
    _array = b.Array(_arrsort, "array_symbol")
    _uf    = b.UF(_funsort)

    # One's complement  
    _not0    = b.Not(_const)
    _not1    = ~_const

    # Two's complement 
    _neg0    = b.Neg(_zero)
    _neg1    = -_zero

    # Reduction operations on bit vectors
    _redor   = b.Redor(_ones)
    _redxor  = b.Redxor(_one)
    _redand  = b.Redand(_uint)

    # Slicing of bit vectors 
    _slice0  = b.Slice(_param, 8, 0)
    _slice1  = _param[8:0]
    _slice3  = _param[:]   # copy
    _slice2  = _param[8:]  # lower is 0
    _slice4  = _param[:0]  # upper is _param.width - 1
    _slice5  = _param[8]   # extract bit at position 8, equiv. to _param[8:8]
    _slice5  = _param[8:8] # equiv. to _param[8]

    # Unsigned/signed extension
    _uext    = b.Uext(_true, 127)
    _sext    = b.Sext(_false, 127)

    _inc     = b.Inc(_not0)
    _dec     = b.Dec(_not1)
    
    _implies0 = b.Implies(_redor, _redxor) 
    _implies1 = b.Implies(False, _redor)
    _implies2 = b.Implies(True, _redxor)

    _iff0     = b.Iff(True, _redxor)
    _iff1     = b.Iff(_redor, _redxor)
    _iff2     = b.Iff(False, _redxor)

    _xor0     = b.Xor(_uext, _sext)
    _xor1     = _uext ^ _sext
    _xor2     = b.Xor(0xff, _sext)
    _xor3     = 0xff ^ _sext

    _and0     = b.And(_inc, _dec)
    _and1     = b.And(128, _dec)
    _and2     = b.And(_dec, 0xaa)
    _and3     = _dec & 0xaa

    _nand0    = b.Nand(_inc, _dec)
    _nand1    = b.Nand(128, _dec)
    _nand2    = b.Nand(_dec, 0xaa)
    _nand3    = ~(_dec & 0xaa) 

    _or0      = b.Or(_inc, _dec)
    _or1      = b.Or(128, _dec)
    _or2      = b.Or(_dec, 0xaa)
    _or3      = _dec | 0xaa

    _nor0     = b.Nor(_inc, _dec)
    _nor1     = b.Nor(128, _dec)
    _nor2     = b.Nor(_dec, 0xaa)
    _nor3     = ~(_dec | 0xaa) 

    _eq0      = b.Eq(_inc, _dec)
    _eq1      = b.Eq(128, _dec)
    _eq2      = b.Eq(_dec, 0xaa)
    _eq3      = _dec == 0xaa

    _neq0     = b.Ne(_inc, _dec)
    _neq1     = b.Ne(128, _dec)
    _neq2     = b.Ne(_dec, 0xaa)
    _neq3     = _dec != 0xaa

    _add0     = b.Add(_inc, _dec)
    _add1     = b.Add(128, _dec)
    _add2     = b.Add(_dec, 0xaa)
    _add3     = _dec + 0xaa

    _uaddo0   = b.Uaddo(_inc, _dec)
    _uaddo1   = b.Uaddo(128, _dec)
    _uaddo2   = b.Uaddo(_dec, 0xaa)

    _saddo0   = b.Saddo(_inc, _dec)
    _saddo1   = b.Saddo(128, _dec)
    _saddo2   = b.Saddo(_dec, 0xaa)

    _mul0     = b.Mul(_inc, _dec)
    _mul1     = b.Mul(128, _dec)
    _mul2     = b.Mul(_dec, 0xaa)
    _mul3     = _dec * 0xaa

    _umulo0   = b.Umulo(_inc, _dec)
    _umulo1   = b.Umulo(128, _dec)
    _umulo2   = b.Umulo(_dec, 0xaa)

    _smulo0   = b.Smulo(_inc, _dec)
    _smulo1   = b.Smulo(128, _dec)
    _smulo2   = b.Smulo(_dec, 0xaa)

    _ult0     = b.Ult(_inc, _dec)
    _ult1     = b.Ult(128, _dec)
    _ult2     = b.Ult(_dec, 0xaa)
    _ult3     = _dec < 0xaa

    _slt0     = b.Slt(_inc, _dec)
    _slt1     = b.Slt(128, _dec)
    _slt2     = b.Slt(_dec, 0xaa)

    _ulte0    = b.Ulte(_inc, _dec)
    _ulte1    = b.Ulte(128, _dec)
    _ulte2    = b.Ulte(_dec, 0xaa)
    _ulte3    = _dec <= 0xaa

    _slte0    = b.Slte(_inc, _dec)
    _slte1    = b.Slte(128, _dec)
    _slte2    = b.Slte(_dec, 0xaa)

    _ugt0     = b.Ugt(_inc, _dec)
    _ugt1     = b.Ugt(128, _dec)
    _ugt2     = b.Ugt(_dec, 0xaa)
    _ugt3     = _dec > 0xaa

    _sgt0     = b.Sgt(_inc, _dec)
    _sgt1     = b.Sgt(128, _dec)
    _sgt2     = b.Sgt(_dec, 0xaa)

    _ugte0    = b.Ugte(_inc, _dec)
    _ugte1    = b.Ugte(128, _dec)
    _ugte2    = b.Ugte(_dec, 0xaa)
    _ugte3    = _dec >= 0xaa

    _sgte0    = b.Sgte(_inc, _dec)
    _sgte1    = b.Sgte(128, _dec)
    _sgte2    = b.Sgte(_dec, 0xaa)

    _sll0     = b.Sll(_dec, 5)
    _sll1     = b.Sll(_dec, 0b100)
    _sll2     = _dec << 5

    _srl0     = b.Srl(_dec, 5)
    _srl1     = b.Srl(_dec, 0b100)
    _srl2     = _dec >> 5

    _sra0     = b.Sra(_dec, 5)
    _sra1     = b.Sra(_dec, 0b100)

    _rol0     = b.Rol(_dec, 5)
    _rol1     = b.Rol(_dec, 0b100)

    _ror0     = b.Ror(_dec, 5)
    _ror1     = b.Ror(_dec, 0b100)

    _sub0     = b.Sub(_inc, _dec)
    _sub1     = b.Sub(128, _dec)
    _sub2     = b.Sub(_dec, 0xaa)
    _sub3     = _dec - 0xaa

    _ssubo0   = b.Ssubo(_inc, _dec)
    _ssubo1   = b.Ssubo(128, _dec)
    _ssubo2   = b.Ssubo(_dec, 0xaa)

    _udiv0    = b.Udiv(_inc, _dec)
    _udiv1    = b.Udiv(128, _dec)
    _udiv2    = b.Udiv(_dec, 0xaa)
    _udiv3    = _dec / 0xaa

    _urem0    = b.Urem(_inc, _dec)
    _urem1    = b.Urem(128, _dec)
    _urem2    = b.Urem(_dec, 0xaa)
    _urem3    = _dec % 0xaa

    _sdiv0    = b.Sdiv(-_inc, _dec)
    _sdiv1    = b.Sdiv(128, -_dec)
    _sdiv2    = b.Sdiv(_dec, -0xaa)

    _srem0    = b.Srem(-_inc, _dec)
    _srem1    = b.Srem(128, -_dec)
    _srem2    = b.Srem(_dec, -0xaa)

    _sdivo0   = b.Sdivo(-_inc, _dec)
    _sdivo1   = b.Sdivo(128, -_dec)
    _sdivo2   = b.Sdivo(_dec, -0xaa)

    _smod0    = b.Smod(-_inc, _dec)
    _smod1    = b.Smod(128, -_dec)
    _smod2    = b.Smod(_dec, -0xaa)

    # Concatenation of bit vectors
    _concat   = b.Concat(_dec, _inc)

    # Reads on arrays
    _read0    = b.Read(_array, _var) 
    _read1    = b.Read(_array, 12)
    _read2    = _array[_var]
    _read3    = _array[0x1a]

    # Writes on arrays
    _write0   = b.Write(_array, _var, _var) 
    _write1   = b.Write(_array, 10, 0b00001) 

    # If-Then-Else on bit vectors
    _cond0    = b.Cond(_read0[0], _read0, _read1)
    _cond1    = b.Cond(False, _read0, _read1)
    _cond2    = b.Cond(True, 1, _read1)

    # If-Then-Else on arrays 
    _cond3    = b.Cond(0, _write0, _write1)

    # Function
    p0        = b.Param(_bvsort)
    p1        = b.Param(_bvsort)
    _fun      = b.Fun([p0, p1], b.Cond(p0 < p1, p0, p1))

    # Function applications
    _apply0   = b.Apply([_var, _var], _fun)
    _apply1   = b.Apply([1, 2], _fun)
    _apply2   = _fun(1, 2)
    _apply3   = b.Apply([_true, _false, _var, _var], _uf)
    _apply4   = b.Apply([1, True, 3, 42], _uf)
    _apply5   = b.Apply([1, False, 3, 42], _uf)
    _apply6   = _uf(1, False, 3, 42)

### Node attributes and methods

    # Get symbol
    s = _var.symbol
    s = _apply4.symbol

    # Set symbol
    _var.symbol = "new_symbol"

    # Get bit width
    w = _apply4.width
    w = _fun.width

    # Get bit width of array index 
    w = _array.index_width

    # Get arity of functions
    a = _fun.arity
    a = _uf.arity

    # Get bit vector representation of constants as string
    bits = _const.bits

    # Dump nodes to stdout or files (default format is BTOR) 
    _apply4.Dump()
    # Dump to file 'dump.btor'
    _apply4.Dump(outfile="dump.btor")
    _apply4.Dump("smt2")
    # Dump to file 'dump.smt2'
#    _apply4.Dump("smt2", "dump.smt2")

### Boolector methods

    # Available options
    b.Options()
    # Print available options
    print("Available Boolector options:")
    print("\n".join(["  " + str(o) for o in b.Options()]))

    # Set options
    b.Set_opt(boolector.BTOR_OPT_INCREMENTAL, 1)
    b.Set_opt(boolector.BTOR_OPT_MODEL_GEN, 1)

    # Get options
    o = b.Get_opt(boolector.BTOR_OPT_MODEL_GEN)
#    print(o.lng)  # long option name
#    print(o.shrt) # short option name
#    print(o.desc) # description
#    print(o.min)  # min value
#    print(o.max)  # max value
#    print(o.dflt) # default value
#    print(o.val)  # current value

    # Set SAT solver (can only be done before the first Sat() call)
    # Lingeling is the default SAT solver
    #b.Set_sat_solver("MiniSAT")
    
    # Assert formulas
    b.Assert(_cond0[1])
    b.Assert(_apply5 != _apply3)

    # Assume formulas
    b.Assume(_cond1[1])

    # Run simplification separately
    res = b.Simplify()

    # Clone boolector instance 'b'
    bb = b.Clone()

    # Check sat
    res = b.Sat()
    # Check sat with limits
#    res = b.Sat(100, 10000)
#    res = b.Sat(lod_limit=100, sat_limit=10000)

    # Get model or query assignments for nodes
    if res == b.SAT:
        # Get model and print to stdout
        b.Print_model()
        # Get model and print to file 'model.out'
#        b.Print_model("model.out")

         # Query assignments
#        print("Query assignments:")
#        print("{} {}".format(_var.symbol, _var.assignment))
#        print("{} {}".format(_array.symbol, _array.assignment))
#        print("{} {}".format(_uf.symbol, _uf.assignment))

    # Get matching node of _cond0 in clone 'bb'
    _cond0_matched = bb.Match(_cond0)
    # Assume
    bb.Assume(~_cond0_matched[1])
    bb.Assume(_cond0_matched[2])
    # Check sat
    res = bb.Sat()

    if res == b.UNSAT:
        # Check if assumptions are failed
        bb.Failed(~_cond0_matched[1])
        bb.Failed(_cond0_matched[2])

    os.remove("dump.btor") 

Table Of Contents

Previous topic

Next topic