Practical Use: Formats and Tools¶

SMT-LIB¶

SMT-LIB is a common file format for SMT formulas and scripts. It currently lists eight theories (e.g. arrays with extensionality, integers, reals) and 29 sorted logics that use and combine theories as well as impose restrictions on the formulas. As some examples:

“QF_UF”: quantifier-free formulas with uninterpreted functions
“QF_LIA”: quantifier-free formulas with linear arithmetic over integers
“QF_UFLRA”: quantifier-free formulas with uninterpreted functions and linear arithmetic over reals
“LIA”: formulas with linear arithmetic over integers

The SMT-LIB site also contains a large number of benchmark instances. The syntax resembles that of the Common Lisp language. As an example, an expression $$x + 1 \le y$$ is written as (<= (+ x 1) y). In addition to variable and formula declarations, there are some scripting commands (check-sat, get-model etc) allowing interactive use. Incremental use is also supported as formulas can be pushed to and popped from an assertion stack. One can play with SMT-LIB online at http://rise4fun.com/Z3.

Our earlier “C function equivalence problem” can be given in the SMT-LIB format as follows:

(set-logic QF_UF)
(set-info :source | An SMT-LIB formulation of C program equivalence.|)
(set-info :smt-lib-version 2.0)
(declare-sort U 0)
(declare-fun in () U)
(declare-fun out1 () U)
(declare-fun out2 () U)
(declare-fun out3 () U)
(declare-fun outprime () U)
(declare-fun f (U U) U)
(assert (and (= out1 in) (and
 (= out2 (f out1 in)) (and
 (= out3 (f out2 in)) (and
 (= outprime (f (f in in) in)) (and
 (not (= out3 outprime))))))))
(check-sat)
(exit)

Here

The first line defines the applied logic, quantifier-free $ \EUF $.
The second line is a comment for humans and the third declares the applied format version.
A new type (aka sort) $ U $ is then declared, as well as the constants (nullary functions) of the type $ U $. Note: in SMT-LIB terms, “variables” are not used but free constants.
The symbol $ f $ is then declared as a binary function $ U \times U \to U $.
The formula is then asserted and its satisfiability queried (a tool will answer “unsat”).

Similarly, the jobshop example in the SMT-LIB format is

(set-logic QF_RDL)
(set-info :source | A jobshop scheduling problem instance.|)
(set-info :smt-lib-version 2.0)
(set-option :produce-models true)
(declare-fun s_1_1 () Real)
(declare-fun s_1_2 () Real)
(declare-fun s_1_3 () Real)
(declare-fun s_2_1 () Real)
(declare-fun s_2_2 () Real)
(declare-fun s_2_3 () Real)
(declare-fun budget () Real)
(assert (and (>= s_1_1 0) (>= s_2_1 0)))
(assert (and (<= (+ s_1_1 6) s_1_2) (<= (+ s_1_2 9) s_1_3)))
(assert (and (<= (+ s_2_1 7) s_2_2) (<= (+ s_2_2 2) s_2_3)))
(assert (or (<= (+ s_1_1 6) s_2_3) (<= (+ s_2_3 7) s_1_1)))
(assert (or (<= (+ s_1_2 9) s_2_2) (<= (+ s_2_2 2) s_1_2)))
(assert (or (<= (+ s_1_3 2) s_2_3) (<= (+ s_2_3 7) s_1_3)))
(assert (and (<= (+ s_1_3 2) budget) (<= (+ s_2_3 7) budget)))
(push 1)
(echo "Trying with the budget 19")
(assert (= budget 19))
(check-sat)
(pop 1)
(echo "Trying with the budget 20")
(assert (= budget 20))
(check-sat)
(get-model)
(exit)

SMT Competition¶

The SMT Competition is a public competition between SMT solvers, organized since 2005. It has motivated solver implementers to adopt the common SMT-LIB format for describing SMT formulas and partly contributed to the fact that the SMT solvers have improved significantly during these over ten years.

Some SMT Solvers¶

Z3 by Microsoft Research. Open-source (MIT license). Documentation in wiki and an online tutorial.
CVC4 by NYU and Univ. Iowa. Open-source.
veriT by D. Déharbe, P. Fontaine, and others. Open-source.
OpenSMT by Roberto Bruttomesso. Open-source.
Boolector by Armin Biere.
MathSAT 5 by Fondazione Bruno Kessler and DISI-University of Trento. Closed-source.
Barcelogic Commercial. A system description paper: Bofill et al, The Barcelogic SMT Solver, Proc. CAV 2008, pp 294–298
Yices by SRI International. Source-code available for non-commercial use.
dReal by CMU. Open-source.

Using the Z3 solver in Python¶

In addition to SMT-LIB format, SMT solvers can also support their own input format and APIs in some programming languages. In this course, we use Z3 through its Python API.

The Z3 theorem prover/SMT solver has an API for many programming languages, including Python. If you are unfamiliar with Python, see, e.g., this Python tutorial. To get Z3, one can either:

Use pip to install the z3-solver package. In Ubuntu Linux, this can be done with:

python3 -m venv z3env
source z3env/bin/activate
pip install z3-solver
z3 -version

Either clone the source code git repository and build it according to the instructions given there, or download pre-compiled release binaries available for many platforms.

In this case, in order to run Z3 from Python, Python must be able to find the Z3 Python bindings and runtime library. In Ubuntu Linux, set the PYTHONPATH and LD_LIBRARY_PATH environment variables. For instance, in the “bash” shell say
```
export LD_LIBRARY_PATH=$LD_LIBRARY_PATH:/my/path/z3/bin
export PYTHONPATH=$PYTHONPATH:/my/path/z3/bin/python
```
where /my/path/z3/bin/ is the directory inside the Z3 release that contains the libraries and the “python” directory.

After installation, you should now be able to run this small test file, call it z3-test.py,

# Import Z3 so that we can use it
from z3 import *

if __name__ == '__main__':
    # Declare real-valued variables x and y
    x = Real('x')          
    y = Real('y')
    # Get a solver instance
    s = Solver()
    # Add two linear inequality constraints
    s.add(x < 10, 2*y < x)
    # Is the conjunction of the constraints satisfiable?
    status = s.check() 
    # In this case,it should be!
    assert status == sat
    # Print a model
    print(s.model())

and get something like this:

pc82:~$ python3 z3-test.py 
[y = 0, x = 1/2]

For slides, tutorials etc, visit the Z3 wiki. For the API documentation, you can

build them if you cloned the source code (see instructions), or
visit this web site.

Our earlier “C function equivalence” problem can be expressed with Z3 and Python as follows:

from z3 import *

if __name__ == '__main__':
    T = DeclareSort('T')       # Declare the sort,
    f = Function('f', T, T, T) # the uninterpreted function, and
    inp = Const('in', T)       # the free constants (aka variables)
    out1 = Const('out1', T)
    out2 = Const('out2', T)
    out3 = Const('out3', T)
    outprime = Const('outprime', T)
    # Get a solver instance
    s = Solver()
    # Add the constraints
    s.add(out1 == inp, out2 == f(out1, inp), out3 == f(out2, inp))
    s.add(outprime == f(f(inp, inp), inp))
    s.add(out3 != outprime)
    # Are the constraints satisfiable?
    status = s.check()
    if status == sat:
        print("Satisfiable")
        print(s.model())
    elif status == unsat: print("Unsatisfiable")
    else: print("Unknown")

Below is a small example illustrating some common constructions in Z3. Especially, observe how Boolean conectives are formed. The Python operators are not overloaded, but one should use the Z3 methods. Consider the line 12. It shows how to construct an implication, and a conjunction. On line 13, we see how negation and disjunction are constructed. Furthermore, observe that conjunction and disjunction allow arbitrarily many arguments, and that they can also be given as a list. This is convenient when the formulas are generated automatically, and the number of arguments can depend on the parameters of the problem.

The lines 14, 15, and 17 show how to use Z3 incrementally. On line 14, a new backtracking point is created in the solver. On line 15, a new formula is added to the solver, and the satisfiability is queried on line 16. Then on line 17, the formula is removed from the solver, by returning the solver state to the one just before creating the backtracking point.

from z3 import *
# Integer-valued variables
x = Int('x')
y = Int('y')
# Boolean variables
a = Bool('a')
# Solver instance
s = Solver()
# Negation, conjunction, disjuntion, implication.
# Both multiple arguments and lists are supported.
# Do NOT use Python 'not', 'and, and 'or'!
s.add(Implies(a, And(y == x + 1, y == -x + 2)))
s.add(Implies(Not(a), Or([y == x + 1, y == -x + 2, x==y])))
s.push() # Create a backtracking point
s.add(a == True) # Any solutions in which a is true?
print(s.check())
s.pop() # Remove the constraint a==True
print(s.check())
print(s.model())