From e0a49dd556b37e893020446ccc8bf90a8a154e8d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 7 Jun 2019 19:14:54 -0700 Subject: [PATCH] html pages for z3 python tutorial Signed-off-by: Nikolaj Bjorner --- .../tutorial/html/advanced-examples.htm | 861 +++++++++++++ .../tutorial/html/fixpoint-examples.htm | 651 ++++++++++ .../python/tutorial/html/guide-examples.htm | 1101 +++++++++++++++++ examples/python/tutorial/html/index.html | 1 + .../tutorial/html/strategies-examples.htm | 350 ++++++ 5 files changed, 2964 insertions(+) create mode 100644 examples/python/tutorial/html/advanced-examples.htm create mode 100644 examples/python/tutorial/html/fixpoint-examples.htm create mode 100644 examples/python/tutorial/html/guide-examples.htm create mode 100644 examples/python/tutorial/html/index.html create mode 100644 examples/python/tutorial/html/strategies-examples.htm diff --git a/examples/python/tutorial/html/advanced-examples.htm b/examples/python/tutorial/html/advanced-examples.htm new file mode 100644 index 000000000..e578aade8 --- /dev/null +++ b/examples/python/tutorial/html/advanced-examples.htm @@ -0,0 +1,861 @@ + + +Z3Py Advanced + + + + +

Advanced Topics

+ +

+Please send feedback, comments and/or corrections to leonardo@microsoft.com. +Your comments are very valuable. +

+ +

Expressions, Sorts and Declarations

+ +

In Z3, expressions, sorts and declarations are called ASTs. +ASTs are directed acyclic graphs. Every expression has a sort (aka type). +The method sort() retrieves the sort of an expression. +

+ + +
x = Int('x')
+y = Real('y')
+print (x + 1).sort()
+print (y + 1).sort()
+print (x >= 2).sort()
+
+ + +

The function eq(n1, n2) returns True if n1 +and n2 are the same AST. This is a structural test. +

+ + +
x, y = Ints('x y')
+print eq(x + y, x + y)
+print eq(x + y, y + x)
+n = x + y
+print eq(n, x + y)
+# x2 is eq to x
+x2 = Int('x') 
+print eq(x, x2)
+# the integer variable x is not equal to 
+# the real variable x
+print eq(Int('x'), Real('x'))
+
+ + +

The method hash() returns a hashcode for an AST node. +If eq(n1, n2) returns True, then n1.hash() +is equal to n2.hash(). +

+ + +
x = Int('x')
+print (x + 1).hash()
+print (1 + x).hash()
+print x.sort().hash()
+
+ + +

Z3 expressions can be divided in three basic groups: applications, +quantifiers and bounded/free variables. +Applications are all you need if your problems do not contain +universal/existential quantifiers. Although we say Int('x') is an +integer "variable", it is technically an integer constant, and internally +is represented as a function application with 0 arguments. +Every application is associated with a declaration and contains +0 or more arguments. The method decl() returns +the declaration associated with an application. The method num_args() +returns the number of arguments of an application, and arg(i) one of the arguments. +The function is_expr(n) returns True +if n is an expression. Similarly is_app(n) (is_func_decl(n)) +returns True if n is an application (declaration). +

+ + +
x = Int('x')
+print "is expression: ", is_expr(x)
+n = x + 1
+print "is application:", is_app(n)
+print "decl:          ", n.decl()
+print "num args:      ", n.num_args()
+for i in range(n.num_args()):
+    print "arg(", i, ") ->", n.arg(i)
+
+ + +

Declarations have names, they are retrieved using the method name(). +A (function) declaration has an arity, a domain and range sorts. +

+ + +
x   = Int('x')
+x_d = x.decl()
+print "is_expr(x_d):     ", is_expr(x_d)
+print "is_func_decl(x_d):", is_func_decl(x_d)
+print "x_d.name():       ", x_d.name()
+print "x_d.range():      ", x_d.range()
+print "x_d.arity():      ", x_d.arity()
+# x_d() creates an application with 0 arguments using x_d.
+print "eq(x_d(), x):     ", eq(x_d(), x)
+print "\n"
+# f is a function from (Int, Real) to Bool
+f   = Function('f', IntSort(), RealSort(), BoolSort())
+print "f.name():         ", f.name()
+print "f.range():        ", f.range()
+print "f.arity():        ", f.arity()
+for i in range(f.arity()):
+    print "domain(", i, "): ", f.domain(i)
+# f(x, x) creates an application with 2 arguments using f.
+print f(x, x)
+print eq(f(x, x).decl(), f)
+
+ + +

+The built-in declarations are identified using their kind. The kind +is retrieved using the method kind(). The complete list of built-in declarations +can be found in the file z3consts.py (z3_api.h) in the Z3 distribution. +

+ + +
x, y = Ints('x y')
+print (x + y).decl().kind() == Z3_OP_ADD
+print (x + y).decl().kind() == Z3_OP_SUB
+
+ + +

+The following example demonstrates how to substitute sub-expressions in Z3 expressions. +

+ + +
x, y = Ints('x y')
+f    = Function('f', IntSort(), IntSort(), IntSort())
+g    = Function('g', IntSort(), IntSort())
+n    = f(f(g(x), g(g(x))), g(g(y)))
+print n
+# substitute g(g(x)) with y and g(y) with x + 1
+print substitute(n, (g(g(x)), y), (g(y), x + 1))
+
+ + +

+The function Const(name, sort) declares a constant (aka variable) of the given sort. +For example, the functions Int(name) and Real(name) are shorthands for +Const(name, IntSort()) and Const(name, RealSort()). +

+ + +
x = Const('x', IntSort())
+print eq(x, Int('x'))
+
+a, b = Consts('a b', BoolSort())
+print And(a, b)
+
+ + +

Arrays

+ +

As part of formulating a programme of a mathematical theory of computation +McCarthy proposed a basic theory of arrays as characterized by +the select-store axioms. The expression Select(a, i) returns +the value stored at position i of the array a; +and Store(a, i, v) returns a new array identical to a, +but on position i it contains the value v. +In Z3Py, we can also write Select(a, i) as a[i]. +

+ + +
# Use I as an alias for IntSort()
+I = IntSort()
+# A is an array from integer to integer
+A = Array('A', I, I)
+x = Int('x')
+print A[x]
+print Select(A, x)
+print Store(A, x, 10)
+print simplify(Select(Store(A, 2, x+1), 2))
+
+ + +

+By default, Z3 assumes that arrays are extensional over select. +In other words, Z3 also enforces that if two arrays agree on all positions, +then the arrays are equal. +

+ +

+Z3 also contains various extensions +for operations on arrays that remain decidable and amenable +to efficient saturation procedures (here efficient means, +with an NP-complete satisfiability complexity). +We describe these extensions in the following using a collection of examples. +Additional background on these extensions is available in the +paper Generalized and Efficient Array Decision Procedures. +

+ +

+Arrays in Z3 are used to model unbounded or very large arrays. +Arrays should not be used to model small finite collections of values. +It is usually much more efficient to create different variables using list comprehensions. +

+ + +
# We want an array with 3 elements.
+# 1. Bad solution
+X = Array('x', IntSort(), IntSort())
+# Example using the array
+print X[0] + X[1] + X[2] >=0
+
+# 2. More efficient solution
+X = IntVector('x', 3)
+print X[0] + X[1] + X[2] >= 0
+print Sum(X) >= 0
+
+ + +

Select and Store

+ + +

Let us first check a basic property of arrays. +Suppose A is an array of integers, then the constraints +A[x] == x, Store(A, x, y) == A +are satisfiable for an array that contains an index x that maps to x, +and when x == y. +We can solve these constraints. +

+ + +
A = Array('A', IntSort(), IntSort())
+x, y = Ints('x y')
+solve(A[x] == x, Store(A, x, y) == A)
+
+ + +

The interpretation/solution for array variables is very similar to the one used for functions.

+ +

The problem becomes unsatisfiable/infeasible if we add the constraint x != y. + +

+ +
A = Array('A', IntSort(), IntSort())
+x, y = Ints('x y')
+solve(A[x] == x, Store(A, x, y) == A, x != y)
+
+ + +

Constant arrays

+ +

+The array that maps all indices to some fixed value can be specified in Z3Py using the +K(s, v) construct where s is a sort/type and v is an expression. +K(s, v) returns a array that maps any value of s into v. +The following example defines a constant array containing only ones. +

+ + +
AllOne = K(IntSort(), 1)
+a, i = Ints('a i')
+solve(a == AllOne[i])
+# The following constraints do not have a solution
+solve(a == AllOne[i], a != 1)
+
+ + +

Datatypes

+ +

Algebraic datatypes, known from programming languages such as ML, +offer a convenient way for specifying common data structures. Records +and tuples are special cases of algebraic datatypes, and so are +scalars (enumeration types). But algebraic datatypes are more +general. They can be used to specify finite lists, trees and other +recursive structures.

+ +

+The following example demonstrates how to declare a List in Z3Py. It is +more verbose than using the SMT 2.0 front-end, but much simpler than using +the Z3 C API. It consists of two phases. +First, we have to declare the new datatype, its constructors and accessors. +The function Datatype('List') declares a "placeholder" that will +contain the constructors and accessors declarations. The method +declare(cname, (aname, sort)+) declares a constructor named +cname with the given accessors. Each accessor has an associated sort +or a reference to the datatypes being declared. +For example, declare('cons', ('car', IntSort()), ('cdr', List)) +declares the constructor named cons that builds a new List +using an integer and a List. It also declares the accessors car and +cdr. The accessor car extracts the integer of a cons +cell, and cdr the list of a cons cell. +After all constructors were declared, we use the method create() to +create the actual datatype in Z3. Z3Py makes the new Z3 declarations and constants +available as slots of the new object. +

+ + +
# Declare a List of integers
+List = Datatype('List')
+# Constructor cons: (Int, List) -> List
+List.declare('cons', ('car', IntSort()), ('cdr', List))
+# Constructor nil: List
+List.declare('nil')
+# Create the datatype
+List = List.create()
+print is_sort(List)
+cons = List.cons
+car  = List.car
+cdr  = List.cdr
+nil  = List.nil
+# cons, car and cdr are function declarations, and nil a constant
+print is_func_decl(cons)
+print is_expr(nil)
+
+l1 = cons(10, cons(20, nil))
+print l1
+print simplify(cdr(l1))
+print simplify(car(l1))
+print simplify(l1 == nil)
+
+ + +

+The following example demonstrates how to define a Python function that +given a sort creates a list of the given sort. +

+ + +
def DeclareList(sort):
+    List = Datatype('List_of_%s' % sort.name())
+    List.declare('cons', ('car', sort), ('cdr', List))
+    List.declare('nil')
+    return List.create()
+
+IntList     = DeclareList(IntSort())
+RealList    = DeclareList(RealSort())
+IntListList = DeclareList(IntList)
+
+l1 = IntList.cons(10, IntList.nil)
+print l1
+print IntListList.cons(l1, IntListList.cons(l1, IntListList.nil))
+print RealList.cons("1/3", RealList.nil)
+
+print l1.sort()
+
+ + +

The example above demonstrates that Z3 supports operator overloading. +There are several functions named cons, but they are different since they receive and/or +return values of different sorts. +Note that it is not necessary to use a different sort name for each instance of the sort +list. That is, the expression 'List_of_%s' % sort.name() is not necessary, we +use it just to provide more meaningful names. +

+ +

+As described above enumeration types are a special case of algebraic datatypes. +The following example declares an enumeration type consisting of three values: +red, green and blue. +

+ + +
Color = Datatype('Color')
+Color.declare('red')
+Color.declare('green')
+Color.declare('blue')
+Color = Color.create()
+
+print is_expr(Color.green)
+print Color.green == Color.blue
+print simplify(Color.green == Color.blue)
+
+# Let c be a constant of sort Color
+c = Const('c', Color)
+# Then, c must be red, green or blue
+prove(Or(c == Color.green, 
+         c == Color.blue,
+         c == Color.red))
+
+ + +

+Z3Py also provides the following shorthand for declaring enumeration sorts. +

+ + +
Color, (red, green, blue) = EnumSort('Color', ('red', 'green', 'blue'))
+
+print green == blue
+print simplify(green == blue)
+
+c = Const('c', Color)
+solve(c != green, c != blue)
+
+ + +

+Mutually recursive datatypes can also be declared. The only difference is that we use +the function CreateDatatypes instead of the method create() to create +the mutually recursive datatypes. +

+ + +
TreeList = Datatype('TreeList')
+Tree     = Datatype('Tree')
+Tree.declare('leaf', ('val', IntSort()))
+Tree.declare('node', ('left', TreeList), ('right', TreeList))
+TreeList.declare('nil')
+TreeList.declare('cons', ('car', Tree), ('cdr', TreeList))
+
+Tree, TreeList = CreateDatatypes(Tree, TreeList)
+
+t1  = Tree.leaf(10)
+tl1 = TreeList.cons(t1, TreeList.nil)
+t2  = Tree.node(tl1, TreeList.nil)
+print t2
+print simplify(Tree.val(t1))
+
+t1, t2, t3 = Consts('t1 t2 t3', TreeList)
+
+solve(Distinct(t1, t2, t3))
+
+ + +

Uninterpreted Sorts

+ +

+Function and constant symbols in pure first-order logic are uninterpreted or free, +which means that no a priori interpretation is attached. +This is in contrast to arithmetic operators such as + and - +that have a fixed standard interpretation. +Uninterpreted functions and constants are maximally flexible; +they allow any interpretation that is consistent with the constraints over the function or constant. +

+ +

+To illustrate uninterpreted functions and constants let us introduce an (uninterpreted) sort A, +and the constants x, y ranging over A. +Finally let f be an uninterpreted function that takes one +argument of sort A and results in a value of sort A. +The example illustrates how one can force an interpretation where f applied twice to x results in x again, +but f applied once to x is different from x. +

+ + +
A    = DeclareSort('A')
+x, y = Consts('x y', A)
+f    = Function('f', A, A)
+
+s    = Solver()
+s.add(f(f(x)) == x, f(x) == y, x != y)
+
+print s.check()
+m = s.model()
+print m
+print "interpretation assigned to A:"
+print m[A]
+
+ + +

+The resulting model introduces abstract values for the elements in A, +because the sort A is uninterpreted. The interpretation for f in the +model toggles between the two values for x and y, which are different. +The expression m[A] returns the interpretation (universe) for the uninterpreted sort A +in the model m. +

+ +

Quantifiers

+ +

+Z3 is can solve quantifier-free problems containing arithmetic, bit-vector, Booleans, +arrays, functions and datatypes. Z3 also accepts and can work with formulas +that use quantifiers. It is no longer a decision procedure for +such formulas in general (and for good reasons, as there can be +no decision procedure for first-order logic). +

+ + +
f = Function('f', IntSort(), IntSort(), IntSort())
+x, y = Ints('x y')
+print ForAll([x, y], f(x, y) == 0)
+print Exists(x, f(x, x) >= 0)
+
+a, b = Ints('a b')
+solve(ForAll(x, f(x, x) == 0), f(a, b) == 1)
+
+ + +

+Nevertheless, Z3 is often able to handle formulas involving +quantifiers. It uses several approaches to handle quantifiers. +The most prolific approach is using pattern-based quantifier +instantiation. This approach allows instantiating quantified formulas +with ground terms that appear in the current search context based +on pattern annotations on quantifiers. +Z3 also contains a model-based quantifier instantiation +component that uses a model construction to find good terms to instantiate +quantifiers with; and Z3 also handles many decidable fragments. +

+ +

Note that in the previous example the constants x +and y were used to create quantified formulas. +This is a "trick" for simplifying the construction of quantified +formulas in Z3Py. Internally, these constants are replaced by +bounded variables. The next example demonstrates that. The method +body() retrives the quantified expression. +In the resultant formula the bounded variables are free. +The function Var(index, sort) creates a bounded/free variable +with the given index and sort. +

+ + +
f = Function('f', IntSort(), IntSort(), IntSort())
+x, y = Ints('x y')
+f = ForAll([x, y], f(x, y) == 0)
+print f.body()
+v1 = f.body().arg(0).arg(0)
+print v1
+print eq(v1, Var(1, IntSort()))
+
+ + +

Modeling with Quantifiers

+ +

+Suppose we want to model an object oriented type system with single inheritance. +We would need a predicate for sub-typing. Sub-typing should be a partial order, +and respect single inheritance. For some built-in type constructors, +such as for array_of, sub-typing should be monotone. +

+ + +
Type     = DeclareSort('Type')
+subtype  = Function('subtype', Type, Type, BoolSort())
+array_of = Function('array_of', Type, Type)
+root     = Const('root', Type)
+
+x, y, z  = Consts('x y z', Type)
+
+axioms = [ ForAll(x, subtype(x, x)),
+           ForAll([x, y, z], Implies(And(subtype(x, y), subtype(y, z)),
+                                     subtype(x, z))),
+           ForAll([x, y], Implies(And(subtype(x, y), subtype(y, x)),
+                                  x == y)),
+           ForAll([x, y, z], Implies(And(subtype(x, y), subtype(x, z)),
+                                     Or(subtype(y, z), subtype(z, y)))),
+           ForAll([x, y], Implies(subtype(x, y),
+                                  subtype(array_of(x), array_of(y)))),
+           
+           ForAll(x, subtype(root, x))
+           ]
+s = Solver()
+s.add(axioms)
+print s
+print s.check()
+print "Interpretation for Type:"
+print s.model()[Type]
+print "Model:"
+print s.model()
+
+ + +

Patterns

+ +

+The Stanford Pascal verifier and the subsequent Simplify theorem prover pioneered +the use of pattern-based quantifier instantiation. +The basic idea behind pattern-based quantifier instantiation is in a sense straight-forward: +Annotate a quantified formula using a pattern that contains all the bound variables. +So a pattern is an expression (that does not contain binding operations, such as quantifiers) +that contains variables bound by a quantifier. Then instantiate the quantifier whenever a term + that matches the pattern is created during search. This is a conceptually easy starting point, +but there are several subtleties that are important. +

+ +

+In the following example, the first two options make sure that Model-based quantifier instantiation engine is disabled. +We also annotate the quantified formula with the pattern f(g(x)). +Since there is no ground instance of this pattern, the quantifier is not instantiated, and +Z3 fails to show that the formula is unsatisfiable. +

+ + +
f = Function('f', IntSort(), IntSort())
+g = Function('g', IntSort(), IntSort())
+a, b, c = Ints('a b c')
+x = Int('x')
+
+s = Solver()
+s.set(auto_config=False, mbqi=False)
+
+s.add( ForAll(x, f(g(x)) == x, patterns = [f(g(x))]),
+       g(a) == c,
+       g(b) == c,
+       a != b )
+
+# Display solver state using internal format
+print s.sexpr()
+print s.check()
+
+ + +

When the more permissive pattern g(x) is used. Z3 proves the formula +to be unsatisfiable. More restrive patterns minimize the number of +instantiations (and potentially improve performance), but they may +also make Z3 "less complete". +

+ + +
f = Function('f', IntSort(), IntSort())
+g = Function('g', IntSort(), IntSort())
+a, b, c = Ints('a b c')
+x = Int('x')
+
+s = Solver()
+s.set(auto_config=False, mbqi=False)
+
+s.add( ForAll(x, f(g(x)) == x, patterns = [g(x)]),
+       g(a) == c,
+       g(b) == c,
+       a != b )
+
+# Display solver state using internal format
+print s.sexpr()
+print s.check()
+
+ + +

+Some patterns may also create long instantiation chains. Consider the following assertion. +

+ +
+ForAll([x, y], Implies(subtype(x, y),
+                       subtype(array_of(x), array_of(y))),
+       patterns=[subtype(x, y)])
+
+ +

+The axiom gets instantiated whenever there is some ground term of the +form subtype(s, t). The instantiation causes a fresh ground term +subtype(array_of(s), array_of(t)), which enables a new +instantiation. This undesirable situation is called a matching +loop. Z3 uses many heuristics to break matching loops. +

+ +

+Before elaborating on the subtleties, we should address an important +first question. What defines the terms that are created during search? +In the context of most SMT solvers, and of the Simplify theorem +prover, terms exist as part of the input formula, they are of course +also created by instantiating quantifiers, but terms are also +implicitly created when equalities are asserted. The last point means +that terms are considered up to congruence and pattern matching takes +place modulo ground equalities. We call the matching problem +E-matching. For example, if we have the following equalities: +

+ + +
f = Function('f', IntSort(), IntSort())
+g = Function('g', IntSort(), IntSort())
+a, b, c = Ints('a b c')
+x = Int('x')
+
+s = Solver()
+s.set(auto_config=False, mbqi=False)
+
+s.add( ForAll(x, f(g(x)) == x, patterns = [f(g(x))]),
+       a == g(b),
+       b == c,
+       f(a) != c )
+
+print s.check()
+
+ + +

+The terms f(a) and f(g(b)) are equal modulo the +equalities. The pattern f(g(x)) can be matched and x bound to b +and the equality f(g(b)) == b is deduced. +

+ +

+While E-matching is an NP-complete problem, the main sources of overhead in larger verification +problems comes from matching thousands of patterns in the context of an evolving set of terms and +equalities. Z3 integrates an efficient E-matching engine using term indexing techniques. +

+ +

Multi-patterns

+ +

+In some cases, there is no pattern that contains all bound variables +and does not contain interpreted symbols. In these cases, we use +multi-patterns. In the following example, the quantified formula +states that f is injective. This quantified formula is annotated with +the multi-pattern MultiPattern(f(x), f(y)). +

+ + +
A = DeclareSort('A')
+B = DeclareSort('B')
+f = Function('f', A, B)
+a1, a2 = Consts('a1 a2', A)
+b      = Const('b', B)
+x,  y  = Consts('x y', A)
+
+s = Solver()
+s.add(a1 != a2,
+      f(a1) == b,
+      f(a2) == b,
+      ForAll([x, y], Implies(f(x) == f(y), x == y),
+             patterns=[MultiPattern(f(x), f(y))])
+      )
+print s.check()
+
+ + +

+The quantified formula is instantiated for every pair of occurrences +of f. A simple trick allows formulating injectivity of f in such a way +that only a linear number of instantiations is required. The trick is +to realize that f is injective if and only if it has a partial +inverse. +

+ + +
A = DeclareSort('A')
+B = DeclareSort('B')
+f = Function('f', A, B)
+finv = Function('finv', B, A)
+a1, a2 = Consts('a1 a2', A)
+b      = Const('b', B)
+x,  y  = Consts('x y', A)
+
+s = Solver()
+s.add(a1 != a2,
+      f(a1) == b,
+      f(a2) == b,
+      ForAll(x, finv(f(x)) == x)
+      )
+print s.check()
+
+ + +

Other attributes

+ +

+In Z3Py, the following additional attributes are supported: qid (quantifier identifier +for debugging), weight (hint to the quantifier instantiation module: "more weight equals less instances"), +no_patterns (expressions that should not be used as patterns, skid (identifier +prefix used to create skolem constants/functions. +

+ +

Multiple Solvers

+ +

In Z3Py and Z3 4.0 multiple solvers can be simultaneously used. +It is also very easy to copy assertions/formulas from one solver to another. +

+ + +
x, y = Ints('x y')
+s1 = Solver()
+s1.add(x > 10, y > 10)
+s2 = Solver()
+# solver s2 is empty
+print s2
+# copy assertions from s1 to s2
+s2.add(s1.assertions())
+print s2
+
+ + +

Unsat Cores and Soft Constraints

+ +

Z3Py also supports unsat core extraction. The basic idea is to use +assumptions, that is, auxiliary propositional variables that we want to track. +Assumptions are also available in the Z3 SMT 2.0 frontend, and in other Z3 front-ends. +They are used to extract unsatisfiable cores. They may be also used to "retract" +constraints. Note that, assumptions are not really soft constraints, but they can be used to implement them. +

+ + +
p1, p2, p3 = Bools('p1 p2 p3')
+x, y = Ints('x y')
+# We assert Implies(p, C) to track constraint C using p
+s = Solver()
+s.add(Implies(p1, x > 10),
+      Implies(p1, y > x),
+      Implies(p2, y < 5),
+      Implies(p3, y > 0))
+print s
+# Check satisfiability assuming p1, p2, p3 are true
+print s.check(p1, p2, p3)
+print s.unsat_core()
+
+# Try again retracting p2
+print s.check(p1, p3)
+print s.model()
+
+ + +

The example above also shows that a Boolean variable (p1) can be used to track +more than one constraint. Note that Z3 does not guarantee that the unsat cores are minimal. +

+ +

Formatter

+ +

+Z3Py uses a formatter (aka pretty printer) for displaying formulas, expressions, solvers, and other +Z3 objects. The formatter supports many configuration options. +The command set_option(html_mode=False) makes all formulas and expressions to be +displayed in Z3Py notation. +

+ + +
x = Int('x')
+y = Int('y')
+print x**2 + y**2 >= 1
+set_option(html_mode=False)
+print x**2 + y**2 >= 1
+
+ + +

By default, Z3Py will truncate the output if the object being displayed is too big. +Z3Py uses … to denote the output is truncated. +The following configuration options can be set to control the behavior of Z3Py's formatter: +

+ + + + +
x = IntVector('x', 20)
+y = IntVector('y', 20)
+f = And(Sum(x) >= 0, Sum(y) >= 0)
+
+set_option(max_args=5)
+print "\ntest 1:"
+print f
+
+print "\ntest 2:"
+set_option(max_args=100, max_lines=10)
+print f
+
+print "\ntest 3:"
+set_option(max_width=300)
+print f
+
+ + + + diff --git a/examples/python/tutorial/html/fixpoint-examples.htm b/examples/python/tutorial/html/fixpoint-examples.htm new file mode 100644 index 000000000..33f401391 --- /dev/null +++ b/examples/python/tutorial/html/fixpoint-examples.htm @@ -0,0 +1,651 @@ + + +Z3Py Fixedpoints + + + + +

Fixedpoints

+ +

+

+ +

+This tutorial illustrates uses of Z3's fixedpoint engine. +The following papers + +μZ - An Efficient Engine for Fixed-Points with Constraints. +(CAV 2011) and + +Generalized Property Directed Reachability (SAT 2012) +describe some of the main features of the engine. +

+ +

+Please send feedback, comments and/or corrections to +nbjorner@microsoft.com. +

+ +

Introduction

+ + +

+This tutorial covers some of the fixedpoint utilities available with Z3. +The main features are a basic Datalog engine, an engine with relational +algebra and an engine based on a generalization of the Property +Directed Reachability algorithm. +

+ + +

Basic Datalog

+ +

The default fixed-point engine is a bottom-up Datalog engine. +It works with finite relations and uses finite table representations +as hash tables as the default way to represent finite relations. +

+ +

Relations, rules and queries

+ +The first example illustrates how to declare relations, rules and +how to pose queries. + + +
fp = Fixedpoint()
+
+a, b, c = Bools('a b c')
+
+fp.register_relation(a.decl(), b.decl(), c.decl())
+fp.rule(a,b)
+fp.rule(b,c)
+fp.set(engine='datalog')
+
+print "current set of rules\n", fp
+print fp.query(a)
+
+fp.fact(c)
+print "updated set of rules\n", fp
+print fp.query(a)
+print fp.get_answer()
+
+ + +The example illustrates some of the basic constructs. +
+  fp = Fixedpoint()
+
+creates a context for fixed-point computation. +
+ fp.register_relation(a.decl(), b.decl(), c.decl())
+
+Register the relations a, b, c as recursively defined. +
+ fp.rule(a,b)
+
+Create the rule that a follows from b. +In general you can create a rule with multiple premises and a name using +the format +
+ fp.rule(head,[body1,...,bodyN],name)
+
+The name is optional. It is used for tracking the rule in derivation proofs. + +Continuing with the example, a is false unless b is established. +
+ fp.query(a)
+
+Asks if a can be derived. The rules so far say that a +follows if b is established and that b follows if c +is established. But nothing establishes c and b is also not +established, so a cannot be derived. +
+ fp.fact(c)
+
+Add a fact (shorthand for fp.rule(c,True)). +Now it is the case that a can be derived. + +

Explanations

+

+It is also possible to get an explanation for a derived query. +For the finite Datalog engine, an explanation is a trace that +provides information of how a fact was derived. The explanation +is an expression whose function symbols are Horn rules and facts used +in the derivation. +

+ +
fp = Fixedpoint()
+
+a, b, c = Bools('a b c')
+
+fp.register_relation(a.decl(), b.decl(), c.decl())
+fp.rule(a,b)
+fp.rule(b,c)
+fp.fact(c)
+fp.set(generate_explanations=True, engine='datalog')
+print fp.query(a)
+print fp.get_answer()
+
+ + +

Relations with arguments

+

+Relations can take arguments. We illustrate relations with arguments +using edges and paths in a graph. +

+ +
fp = Fixedpoint()
+fp.set(engine='datalog')
+
+s = BitVecSort(3)
+edge = Function('edge', s, s, BoolSort())
+path = Function('path', s, s, BoolSort())
+a = Const('a',s)
+b = Const('b',s)
+c = Const('c',s)
+
+fp.register_relation(path,edge)
+fp.declare_var(a,b,c)
+fp.rule(path(a,b), edge(a,b))
+fp.rule(path(a,c), [edge(a,b),path(b,c)])
+
+v1 = BitVecVal(1,s)
+v2 = BitVecVal(2,s)
+v3 = BitVecVal(3,s)
+v4 = BitVecVal(4,s)
+
+fp.fact(edge(v1,v2))
+fp.fact(edge(v1,v3))
+fp.fact(edge(v2,v4))
+
+print "current set of rules", fp
+
+
+print fp.query(path(v1,v4)), "yes we can reach v4 from v1"
+
+print fp.query(path(v3,v4)), "no we cannot reach v4 from v3"
+
+ + +The example uses the declaration +
+ fp.declare_var(a,b,c)
+
+to instrument the fixed-point engine that a, b, c +should be treated as variables +when they appear in rules. Think of the convention as they way bound variables are +passed to quantifiers in Z3Py. + +

Rush Hour

+

+A more entertaining example of using the basic fixed point engine +is to solve the Rush Hour puzzle. The puzzle is about moving +a red car out of a gridlock. We have encoded a configuration +and compiled a set of rules that encode the legal moves of the cars +given the configuration. Other configurations can be tested by +changing the parameters passed to the constructor for Car. +We have encoded the configuration from + +an online puzzle you can solve manually, or cheat on by asking Z3. +

+ +
class Car():
+    def __init__(self, is_vertical, base_pos, length, start, color):
+	self.is_vertical = is_vertical
+	self.base = base_pos
+	self.length = length
+	self.start = start
+	self.color = color
+
+    def __eq__(self, other):
+	return self.color == other.color
+
+    def __ne__(self, other):
+	return self.color != other.color
+
+dimension = 6
+
+red_car = Car(False, 2, 2, 3, "red")
+cars = [
+    Car(True, 0, 3, 0, 'yellow'),
+    Car(False, 3, 3, 0, 'blue'),
+    Car(False, 5, 2, 0, "brown"),
+    Car(False, 0, 2, 1, "lgreen"),
+    Car(True,  1, 2, 1, "light blue"),
+    Car(True,  2, 2, 1, "pink"),
+    Car(True,  2, 2, 4, "dark green"),
+    red_car,
+    Car(True,  3, 2, 3, "purple"),
+    Car(False, 5, 2, 3, "light yellow"),
+    Car(True,  4, 2, 0, "orange"),
+    Car(False, 4, 2, 4, "black"),
+    Car(True,  5, 3, 1, "light purple")
+    ]
+
+num_cars = len(cars)
+B = BoolSort()
+bv3 = BitVecSort(3)
+
+
+state = Function('state', [ bv3 for c in cars] + [B])
+
+def num(i):
+    return BitVecVal(i,bv3)
+
+def bound(i):
+    return Const(cars[i].color, bv3)
+
+fp = Fixedpoint()
+fp.set(generate_explanations=True)
+fp.declare_var([bound(i) for i in range(num_cars)])
+fp.register_relation(state)
+
+def mk_state(car, value):
+    return state([ (num(value) if (cars[i] == car) else bound(i))
+		   for i in range(num_cars)])
+
+def mk_transition(row, col, i0, j, car0):
+    body = [mk_state(car0, i0)]
+    for index in range(num_cars):
+	car = cars[index]
+	if car0 != car:
+	    if car.is_vertical and car.base == col:
+		for i in range(dimension):
+		    if i <= row and row < i + car.length and i + car.length <= dimension:
+			   body += [bound(index) != num(i)]
+	    if car.base == row and not car.is_vertical:
+		for i in range(dimension):
+		    if i <= col and col < i + car.length and i + car.length <= dimension:
+			   body += [bound(index) != num(i)]
+
+    s = "%s %d->%d" % (car0.color, i0, j)
+			
+    fp.rule(mk_state(car0, j), body, s)
+    
+
+def move_down(i, car):
+    free_row = i + car.length
+    if free_row < dimension:
+	mk_transition(free_row, car.base, i, i + 1, car)
+            
+
+def move_up(i, car):
+    free_row = i  - 1
+    if 0 <= free_row and i + car.length <= dimension:
+	mk_transition(free_row, car.base, i, i - 1, car)
+
+def move_left(i, car):
+    free_col = i - 1;
+    if 0 <= free_col and i + car.length <= dimension:
+	mk_transition(car.base, free_col, i, i - 1, car)
+	
+
+def move_right(i, car):
+    free_col = car.length + i
+    if free_col < dimension:
+	mk_transition(car.base, free_col, i, i + 1, car)
+	
+
+# Initial state:
+fp.fact(state([num(cars[i].start) for i in range(num_cars)]))
+
+# Transitions:
+for car in cars:
+    for i in range(dimension):
+	if car.is_vertical:
+	    move_down(i, car)
+	    move_up(i, car)
+	else:
+	    move_left(i, car)
+	    move_right(i, car)
+    
+
+def get_instructions(ans):
+    lastAnd = ans.arg(0).children()[-1]
+    trace = lastAnd.children()[1]
+    while trace.num_args() > 0:
+	print trace.decl()
+	trace = trace.children()[-1]
+
+print fp
+
+goal = state([ (num(4) if cars[i] == red_car else bound(i))
+	       for i in range(num_cars)])
+fp.query(goal)
+
+get_instructions(fp.get_answer())
+    
+
+ + + +

Abstract Domains

+The underlying engine uses table operations +that are based on relational algebra. Representations are +opaque to the underlying engine. +Relational algebra operations are well defined for arbitrary relations. +They don't depend on whether the relations denote a finite or an +infinite set of values. +Z3 contains two built-in tables for infinite domains. +The first is for intervals of integers and reals. +The second is for bound constraints between two integers or reals. +A bound constraint is of the form x or x . +When used in conjunction, they form +an abstract domain that is called the + +Pentagon abstract +domain. Z3 implements reduced products +of abstract domains that enables sharing constraints between +the interval and bounds domains. + +

+Below we give a simple example that illustrates a loop at location l0. +The loop is incremented as long as the loop counter does not exceed an upper +bound. Using the combination of bound and interval domains +we can collect derived invariants from the loop and we can also establish +that the state after the loop does not exceed the bound. +

+ + + +
I  = IntSort()
+B  = BoolSort()
+l0 = Function('l0',I,I,B)
+l1 = Function('l1',I,I,B)
+
+s = Fixedpoint()
+s.set(engine='datalog',compile_with_widening=True,
+      unbound_compressor=False)
+
+s.register_relation(l0,l1)
+s.set_predicate_representation(l0, 'interval_relation', 'bound_relation')
+s.set_predicate_representation(l1, 'interval_relation', 'bound_relation')
+
+m, x, y = Ints('m x y')
+
+s.declare_var(m, x, y)
+s.rule(l0(0,m),   0 < m)
+s.rule(l0(x+1,m), [l0(x,m), x < m])
+s.rule(l1(x,m),   [l0(x,m), m <= x])
+
+print "At l0 we learn that x, y are non-negative:"
+print s.query(l0(x,y))
+print s.get_answer()
+
+print "At l1 we learn that x <= y and both x and y are bigger than 0:"
+print s.query(l1(x,y))
+print s.get_answer()
+
+
+print "The state where x < y is not reachable"
+print s.query(And(l1(x,y), x < y))
+
+ + +The example uses the option +
+   set_option(dl_compile_with_widening=True)
+
+to instrument Z3 to apply abstract interpretation widening on loop boundaries. + + +

Engine for Property Directed Reachability

+ +A different underlying engine for fixed-points is based on +an algorithm for Property Directed Reachability (PDR). +The PDR engine is enabled using the instruction +
+  set_option(dl_engine=1)
+
+The version in Z3 applies to Horn clauses with arithmetic and +Boolean domains. When using arithmetic you should enable +the main abstraction engine used in Z3 for arithmetic in PDR. +
+ set_option(dl_pdr_use_farkas=True)
+
+The engine also works with domains using algebraic +data-types and bit-vectors, although it is currently not +overly tuned for either. +The PDR engine is targeted at applications from symbolic model +checking of software. The systems may be infinite state. +The following examples also serve a purpose of showing +how software model checking problems (of safety properties) +can be embedded into Horn clauses and solved using PDR. + +

Procedure Calls

+

+McCarthy's 91 function illustrates a procedure that calls itself recursively +twice. The Horn clauses below encode the recursive function: + +

+
+  mc(x) = if x > 100 then x - 10 else mc(mc(x+11))
+
+ +The general scheme for encoding recursive procedures is by creating a predicate +for each procedure and adding an additional output variable to the predicate. +Nested calls to procedures within a body can be encoded as a conjunction +of relations. + + + +
mc = Function('mc', IntSort(), IntSort(), BoolSort())
+n, m, p = Ints('n m p')
+
+fp = Fixedpoint()
+
+fp.declare_var(n,m)
+fp.register_relation(mc)
+
+fp.rule(mc(m, m-10), m > 100)
+fp.rule(mc(m, n), [m <= 100, mc(m+11,p),mc(p,n)])
+    
+print fp.query(And(mc(m,n),n < 90))
+print fp.get_answer()
+
+print fp.query(And(mc(m,n),n < 91))
+print fp.get_answer()
+
+print fp.query(And(mc(m,n),n < 92))
+print fp.get_answer()
+
+ + +The first two queries are unsatisfiable. The PDR engine produces the same proof of unsatisfiability. +The proof is an inductive invariant for each recursive predicate. The PDR engine introduces a +special query predicate for the query. + +

Bakery

+ +

+We can also prove invariants of reactive systems. It is convenient to encode reactive systems +as guarded transition systems. It is perhaps for some not as convenient to directly encode +guarded transitions as recursive Horn clauses. But it is fairly easy to write a translator +from guarded transition systems to recursive Horn clauses. We illustrate a translator +and Lamport's two process Bakery algorithm in the next example. +

+ + +
set_option(relevancy=0,verbose=1)
+
+def flatten(l):
+    return [s for t in l for s in t]
+
+
+class TransitionSystem():
+    def __init__(self, initial, transitions, vars1):
+	self.fp = Fixedpoint()        
+	self.initial     = initial
+	self.transitions = transitions
+	self.vars1 = vars1
+
+    def declare_rels(self):
+	B = BoolSort()
+	var_sorts   = [ v.sort() for v in self.vars1 ]
+	state_sorts = var_sorts
+	self.state_vals = [ v for v in self.vars1 ]
+	self.state_sorts  = state_sorts
+	self.var_sorts = var_sorts
+	self.state  = Function('state', state_sorts + [ B ])
+	self.step   = Function('step',  state_sorts + state_sorts + [ B ])
+	self.fp.register_relation(self.state)
+	self.fp.register_relation(self.step)
+
+# Set of reachable states are transitive closure of step.
+
+    def state0(self):
+	idx = range(len(self.state_sorts))
+	return self.state([Var(i,self.state_sorts[i]) for i in idx])
+	
+    def state1(self):
+	n = len(self.state_sorts)
+	return self.state([Var(i+n, self.state_sorts[i]) for i in range(n)])
+
+    def rho(self):
+	n = len(self.state_sorts)
+	args1 = [ Var(i,self.state_sorts[i]) for i in range(n) ]
+	args2 = [ Var(i+n,self.state_sorts[i]) for i in range(n) ]
+	args = args1 + args2 
+	return self.step(args)
+
+    def declare_reachability(self):
+	self.fp.rule(self.state1(), [self.state0(), self.rho()])
+
+
+# Define transition relation
+
+    def abstract(self, e):
+	n = len(self.state_sorts)
+	sub = [(self.state_vals[i], Var(i,self.state_sorts[i])) for i in range(n)]
+	return substitute(e, sub)
+	
+    def declare_transition(self, tr):
+	len_s  = len(self.state_sorts)
+	effect = tr["effect"]
+	vars1  = [Var(i,self.state_sorts[i]) for i in range(len_s)] + effect
+	rho1  = self.abstract(self.step(vars1))
+	guard = self.abstract(tr["guard"])
+	self.fp.rule(rho1, guard)
+	
+    def declare_transitions(self):
+	for t in self.transitions:
+	    self.declare_transition(t)
+
+    def declare_initial(self):
+	self.fp.rule(self.state0(),[self.abstract(self.initial)])
+	
+    def query(self, query):
+	self.declare_rels()
+	self.declare_initial()
+	self.declare_reachability()
+	self.declare_transitions()
+	query = And(self.state0(), self.abstract(query))
+	print self.fp
+	print query
+	print self.fp.query(query)
+	print self.fp.get_answer()
+#	print self.fp.statistics()
+
+
+L = Datatype('L')
+L.declare('L0')
+L.declare('L1')
+L.declare('L2')
+L = L.create()
+L0 = L.L0
+L1 = L.L1
+L2 = L.L2
+
+
+y0 = Int('y0')
+y1 = Int('y1')
+l  = Const('l', L)
+m  = Const('m', L)
+
+
+t1 = { "guard" : l == L0,
+       "effect" : [ L1, y1 + 1, m, y1 ] }
+t2 = { "guard" : And(l == L1, Or([y0 <= y1, y1 == 0])),
+       "effect" : [ L2, y0,     m, y1 ] }
+t3 = { "guard" : l == L2,
+       "effect" : [ L0, IntVal(0), m, y1 ]}
+s1 = { "guard" : m == L0,
+       "effect" : [ l,  y0, L1, y0 + 1 ] }
+s2 = { "guard" : And(m == L1, Or([y1 <= y0, y0 == 0])),
+       "effect" : [ l,  y0, L2, y1 ] }
+s3 = { "guard" : m == L2,
+       "effect" : [ l,  y0, L0, IntVal(0) ]}
+
+
+ptr = TransitionSystem( And(l == L0, y0 == 0, m == L0, y1 == 0),
+			[t1, t2, t3, s1, s2, s3],
+			[l, y0, m, y1])
+
+ptr.query(And([l == L2, m == L2 ]))
+
+ +The rather verbose (and in no way minimal) inductive invariants are produced as answers. + +

Functional Programs

+We can also verify some properties of functional programs using Z3's +generalized PDR. Let us here consider an example from + +Predicate Abstraction and CEGAR for Higher-Order Model +Checking, Kobayashi et.al. PLDI 2011. +We encode functional programs by taking a suitable operational +semantics and encoding an evaluator that is specialized to +the program being verified (we don't encode a general purpose +evaluator, you should partial evaluate it to help verification). +We use algebraic data-types to encode the current closure that is +being evaluated. + + +
# let max max2 x y z = max2 (max2 x y) z
+# let f x y = if x > y then x else y
+# assert (f (max f x y z) x) = (max f x y z)
+
+
+Expr = Datatype('Expr')
+Expr.declare('Max')
+Expr.declare('f')
+Expr.declare('I', ('i', IntSort()))
+Expr.declare('App', ('fn',Expr),('arg',Expr))
+Expr = Expr.create()
+Max  = Expr.Max
+I    = Expr.I
+App  = Expr.App
+f    = Expr.f
+Eval = Function('Eval',Expr,Expr,Expr,BoolSort())
+
+x   = Const('x',Expr)
+y   = Const('y',Expr)
+z   = Const('z',Expr)
+r1  = Const('r1',Expr)
+r2  = Const('r2',Expr)
+max = Const('max',Expr)
+xi  = Const('xi',IntSort())
+yi  = Const('yi',IntSort())
+
+fp = Fixedpoint()
+fp.register_relation(Eval)
+fp.declare_var(x,y,z,r1,r2,max,xi,yi)
+
+# Max max x y z = max (max x y) z
+fp.rule(Eval(App(App(App(Max,max),x),y), z, r2),
+	[Eval(App(max,x),y,r1),
+	 Eval(App(max,r1),z,r2)])
+
+# f x y = x if x >= y
+# f x y = y if x < y
+fp.rule(Eval(App(f,I(xi)),I(yi),I(xi)),xi >= yi)
+fp.rule(Eval(App(f,I(xi)),I(yi),I(yi)),xi < yi)
+
+print fp.query(And(Eval(App(App(App(Max,f),x),y),z,r1),
+		   Eval(App(f,x),r1,r2),
+		   r1 != r2))
+
+print fp.get_answer()
+
+ + + + + diff --git a/examples/python/tutorial/html/guide-examples.htm b/examples/python/tutorial/html/guide-examples.htm new file mode 100644 index 000000000..f79d5d91e --- /dev/null +++ b/examples/python/tutorial/html/guide-examples.htm @@ -0,0 +1,1101 @@ + + +Z3Py Guide + + + + + +

Z3 API in Python

+

Z3 is a high performance theorem prover developed at Microsoft Research. +Z3 is used in many applications such as: software/hardware verification and testing, constraint solving, analysis of hybrid systems, +security, biology (in silico analysis), and geometrical problems.

+

This tutorial demonstrates the main capabilities of Z3Py: the Z3 API in Python. +No Python background is needed to read this tutorial. However, it is useful to learn Python (a fun language!) at some point, and +there are many excellent free resources for doing so (Python Tutorial). +

+ +

The Z3 distribution also contains the C, .Net and OCaml APIs. The source code of Z3Py is available in +the Z3 distribution, feel free to modify it to meet your needs. The source code also demonstrates how to use new features in Z3 4.0. +Other cool front-ends for Z3 include Scala^Z3 and SBV.

+ +

+Be sure to follow along with the examples by clicking the load in editor link in the +corner. See what Z3Py says, try your own scripts, and experiment! +

+ +

+Please send feedback, comments and/or corrections to leonardo@microsoft.com. +Your comments are very valuable. +

+ +

Getting Started

+ +

Let us start with the following simple example:

+ + +
x = Int('x')
+y = Int('y')
+solve(x > 2, y < 10, x + 2*y == 7)
+
+ + +

The function Int('x') creates an integer variable in Z3 named x. +The solve function solves a system of constraints. The example above uses +two variables x and y, and three constraints. +Z3Py like Python uses = for assignment. The operators <, +<=, +>, +>=, +== and +!= for comparison. +In the example above, the expression x + 2*y == 7 is a Z3 constraint. +Z3 can solve and crunch formulas. +

+ +

+The next examples show how to use the Z3 formula/expression simplifier. +

+ + +
x = Int('x')
+y = Int('y')
+print simplify(x + y + 2*x + 3)
+print simplify(x < y + x + 2)
+print simplify(And(x + 1 >= 3, x**2 + x**2 + y**2 + 2 >= 5))
+
+ + +

+By default, Z3Py (for the web) displays formulas and expressions using mathematical notation. +As usual, ∧ is the logical and, ∨ is the logical or, and so on. +The command set_option(html_mode=False) makes all formulas and expressions to be +displayed in Z3Py notation. This is also the default mode for the offline version of Z3Py that +comes with the Z3 distribution. +

+ + +
x = Int('x')
+y = Int('y')
+print x**2 + y**2 >= 1
+set_option(html_mode=False)
+print x**2 + y**2 >= 1
+
+ + +

+Z3 provides functions for traversing expressions. +

+ + +
x = Int('x')
+y = Int('y')
+n = x + y >= 3
+print "num args: ", n.num_args()
+print "children: ", n.children()
+print "1st child:", n.arg(0)
+print "2nd child:", n.arg(1)
+print "operator: ", n.decl()
+print "op name:  ", n.decl().name()
+
+ + +

+Z3 provides all basic mathematical operations. Z3Py uses the same operator precedence of the Python language. +Like Python, ** is the power operator. Z3 can solve nonlinear polynomial constraints. +

+ + +
x = Real('x')
+y = Real('y')
+solve(x**2 + y**2 > 3, x**3 + y < 5)
+
+ + +

+The procedure Real('x') creates the real variable x. +Z3Py can represent arbitrarily large integers, rational numbers (like in the example above), +and irrational algebraic numbers. An irrational algebraic number is a root of a polynomial with integer coefficients. +Internally, Z3 represents all these numbers precisely. +The irrational numbers are displayed in decimal notation for making it easy to read the results. +

+ + +
x = Real('x')
+y = Real('y')
+solve(x**2 + y**2 == 3, x**3 == 2)
+
+set_option(precision=30)
+print "Solving, and displaying result with 30 decimal places"
+solve(x**2 + y**2 == 3, x**3 == 2)
+
+ + +

+The procedure set_option is used to configure the Z3 environment. It is used to set global configuration options +such as how the result is displayed. The option set_option(precision=30) sets the number of decimal places used when displaying results. +The ? mark in 1.2599210498? indicates the output is truncated. +

+ +

+The following example demonstrates a common mistake. The expression 3/2 is a Python integer and not a Z3 rational number. +The example also shows different ways to create rational numbers in Z3Py. The procedure Q(num, den) creates a +Z3 rational where num is the numerator and den is the denominator. The RealVal(1) creates a Z3 real number +representing the number 1. +

+ + +
print 1/3
+print RealVal(1)/3
+print Q(1,3)
+
+x = Real('x')
+print x + 1/3
+print x + Q(1,3)
+print x + "1/3"
+print x + 0.25
+
+ + +

+Rational numbers can also be displayed in decimal notation. +

+ + +
x = Real('x')
+solve(3*x == 1)
+
+set_option(rational_to_decimal=True)
+solve(3*x == 1)
+
+set_option(precision=30)
+solve(3*x == 1)
+
+ + +

+A system of constraints may not have a solution. In this case, we say the system is unsatisfiable. +

+ + +
x = Real('x')
+solve(x > 4, x < 0)
+
+ + +

+Like in Python, comments begin with the hash character # and are terminated by the end of line. +Z3Py does not support comments that span more than one line. +

+ + +
# This is a comment
+x = Real('x') # comment: creating x
+print x**2 + 2*x + 2  # comment: printing polynomial
+
+ + +

Boolean Logic

+ +

+Z3 supports Boolean operators: And, Or, Not, Implies (implication), +If (if-then-else). Bi-implications are represented using equality ==. +The following example shows how to solve a simple set of Boolean constraints. +

+ + +
p = Bool('p')
+q = Bool('q')
+r = Bool('r')
+solve(Implies(p, q), r == Not(q), Or(Not(p), r))
+
+
+ + +

+The Python Boolean constants True and False can be used to build Z3 Boolean expressions. +

+ + +
p = Bool('p')
+q = Bool('q')
+print And(p, q, True)
+print simplify(And(p, q, True))
+print simplify(And(p, False))
+
+ + +

The following example uses a combination of polynomial and Boolean constraints. +

+ + +
p = Bool('p')
+x = Real('x')
+solve(Or(x < 5, x > 10), Or(p, x**2 == 2), Not(p))
+
+ + +

Solvers

+ +

Z3 provides different solvers. The command solve, used in the previous examples, is implemented using the Z3 solver API. +The implementation can be found in the file z3.py in the Z3 distribution. +The following example demonstrates the basic Solver API. +

+ + +
x = Int('x')
+y = Int('y')
+
+s = Solver()
+print s
+
+s.add(x > 10, y == x + 2)
+print s
+print "Solving constraints in the solver s ..."
+print s.check()
+
+print "Create a new scope..."
+s.push()
+s.add(y < 11)
+print s
+print "Solving updated set of constraints..."
+print s.check()
+
+print "Restoring state..."
+s.pop()
+print s
+print "Solving restored set of constraints..."
+print s.check()
+
+ + +

+The command Solver() creates a general purpose solver. Constraints can be added using the method add. +We say the constraints have been asserted in the solver. The method check() solves the asserted constraints. +The result is sat (satisfiable) if a solution was found. The result is unsat (unsatisfiable) if +no solution exists. We may also say the system of asserted constraints is infeasible. Finally, a solver may fail +to solve a system of constraints and unknown is returned. +

+ +

+In some applications, we want to explore several similar problems that share several constraints. +We can use the commands push and pop for doing that. +Each solver maintains a stack of assertions. The command push creates a new scope by +saving the current stack size. +The command pop removes any assertion performed between it and the matching push. +The check method always operates on the content of solver assertion stack. +

+ +

+The following example shows an example that Z3 cannot solve. The solver returns unknown in this case. +Recall that Z3 can solve nonlinear polynomial constraints, but 2**x is not a polynomial. +

+ + +
x = Real('x')
+s = Solver()
+s.add(2**x == 3)
+print s.check()
+
+ + +

+The following example shows how to traverse the constraints asserted into a solver, and how to collect performance statistics for +the check method. +

+ + +
x = Real('x')
+y = Real('y')
+s = Solver()
+s.add(x > 1, y > 1, Or(x + y > 3, x - y < 2))
+print "asserted constraints..."
+for c in s.assertions():
+    print c
+
+print s.check()
+print "statistics for the last check method..."
+print s.statistics()
+# Traversing statistics
+for k, v in s.statistics():
+    print "%s : %s" % (k, v)
+
+ + +

+The command check returns sat when Z3 finds a solution for the set of asserted constraints. +We say Z3 satisfied the set of constraints. We say the solution is a model for the set of asserted +constraints. A model is an interpretation that makes each asserted constraint true. +The following example shows the basic methods for inspecting models. +

+ + +
x, y, z = Reals('x y z')
+s = Solver()
+s.add(x > 1, y > 1, x + y > 3, z - x < 10)
+print s.check()
+
+m = s.model()
+print "x = %s" % m[x]
+
+print "traversing model..."
+for d in m.decls():
+    print "%s = %s" % (d.name(), m[d])
+
+ + +

In the example above, the function Reals('x y z') creates the variables. x, y and z. +It is shorthand for: +

+ +
+x = Real('x')
+y = Real('y')
+z = Real('z')
+
+ +

+The expression m[x] returns the interpretation of x in the model m. +The expression "%s = %s" % (d.name(), m[d]) returns a string where the first %s is replaced with +the name of d (i.e., d.name()), and the second %s with a textual representation of the +interpretation of d (i.e., m[d]). Z3Py automatically converts Z3 objects into a textual representation +when needed. +

+ +

Arithmetic

+ +

Z3 supports real and integer variables. They can be mixed in a single problem. +Like most programming languages, Z3Py will automatically add coercions converting integer expressions to real ones when needed. +The following example demonstrates different ways to declare integer and real variables. +

+ + +
x = Real('x')
+y = Int('y')
+a, b, c = Reals('a b c')
+s, r = Ints('s r')
+print x + y + 1 + (a + s)
+print ToReal(y) + c
+
+ + +

The function ToReal casts an integer expression into a real expression.

+ +

Z3Py supports all basic arithmetic operations.

+ + +
a, b, c = Ints('a b c')
+d, e = Reals('d e')
+solve(a > b + 2,
+      a == 2*c + 10,
+      c + b <= 1000,
+      d >= e)
+
+ + +

The command simplify applies simple transformations on Z3 expressions.

+ + +
x, y = Reals('x y')
+# Put expression in sum-of-monomials form
+t = simplify((x + y)**3, som=True)
+print t
+# Use power operator
+t = simplify(t, mul_to_power=True)
+print t
+
+ + +

The command help_simplify() prints all available options. +Z3Py allows users to write option in two styles. The Z3 internal option names start with : and words are separated by -. +These options can be used in Z3Py. Z3Py also supports Python-like names, +where : is suppressed and - is replaced with _. +The following example demonstrates how to use both styles. +

+ + +
x, y = Reals('x y')
+# Using Z3 native option names
+print simplify(x == y + 2, ':arith-lhs', True)
+# Using Z3Py option names
+print simplify(x == y + 2, arith_lhs=True)
+
+print "\nAll available options:"
+help_simplify()
+
+ + +

Z3Py supports arbitrarily large numbers. The following example demonstrates how to perform basic arithmetic using larger integer, rational and irrational numbers. +Z3Py only supports algebraic irrational numbers. Algebraic irrational numbers are sufficient for presenting the solutions of systems of polynomial constraints. +Z3Py will always display irrational numbers in decimal notation since it is more convenient to read. The internal representation can be extracted using the method sexpr(). +It displays Z3 internal representation for mathematical formulas and expressions in s-expression (Lisp-like) notation. +

+ + +
x, y = Reals('x y')
+solve(x + 10000000000000000000000 == y, y > 20000000000000000)
+
+print Sqrt(2) + Sqrt(3)
+print simplify(Sqrt(2) + Sqrt(3))
+print simplify(Sqrt(2) + Sqrt(3)).sexpr()
+# The sexpr() method is available for any Z3 expression
+print (x + Sqrt(y) * 2).sexpr()
+
+ + +

Machine Arithmetic

+ +

+Modern CPUs and main-stream programming languages use +arithmetic over fixed-size bit-vectors. +Machine arithmetic is available in Z3Py as Bit-Vectors. +They implement the +precise semantics of unsigned and of +signed two-complements arithmetic. + +

+

+The following example demonstrates how to create bit-vector variables and constants. +The function BitVec('x', 16) creates a bit-vector variable in Z3 named x with 16 bits. +For convenience, integer constants can be used to create bit-vector expressions in Z3Py. +The function BitVecVal(10, 32) creates a bit-vector of size 32 containing the value 10. +

+ + +
x = BitVec('x', 16)
+y = BitVec('y', 16)
+print x + 2
+# Internal representation
+print (x + 2).sexpr()
+
+# -1 is equal to 65535 for 16-bit integers 
+print simplify(x + y - 1)
+
+# Creating bit-vector constants
+a = BitVecVal(-1, 16)
+b = BitVecVal(65535, 16)
+print simplify(a == b)
+
+a = BitVecVal(-1, 32)
+b = BitVecVal(65535, 32)
+# -1 is not equal to 65535 for 32-bit integers 
+print simplify(a == b)
+
+ + +

+In contrast to programming languages, such as C, C++, C#, Java, +there is no distinction between signed and unsigned bit-vectors +as numbers. Instead, Z3 provides special signed versions of arithmetical operations +where it makes a difference whether the bit-vector is treated as signed or unsigned. +In Z3Py, the operators +<, +<=, +>, +>=, /, % and >> correspond to the signed versions. +The corresponding unsigned operators are +ULT, +ULE, +UGT, +UGE, UDiv, URem and LShR. +

+ + +
# Create to bit-vectors of size 32
+x, y = BitVecs('x y', 32)
+
+solve(x + y == 2, x > 0, y > 0)
+
+# Bit-wise operators
+# & bit-wise and
+# | bit-wise or
+# ~ bit-wise not
+solve(x & y == ~y)
+
+solve(x < 0)
+
+# using unsigned version of < 
+solve(ULT(x, 0))
+
+ + +

+The operator >> is the arithmetic shift right, and +<< is the shift left. The logical shift right is the operator LShR. +

+ + +
# Create to bit-vectors of size 32
+x, y = BitVecs('x y', 32)
+
+solve(x >> 2 == 3)
+
+solve(x << 2 == 3)
+
+solve(x << 2 == 24)
+
+ + +

Functions

+ +

+Unlike programming languages, where functions have side-effects, can throw exceptions, +or never return, functions in Z3 have no side-effects and are total. +That is, they are defined on all input values. This includes functions, such +as division. Z3 is based on first-order logic. +

+ +

+Given a constraints such as x + y > 3, we have been saying that x and y +are variables. In many textbooks, x and y are called uninterpreted constants. +That is, they allow any interpretation that is consistent with the constraint x + y > 3. +

+ +

+More precisely, function and constant symbols in pure first-order logic are uninterpreted or free, +which means that no a priori interpretation is attached. +This is in contrast to functions belonging to the signature of theories, +such as arithmetic where the function + has a fixed standard interpretation +(it adds two numbers). Uninterpreted functions and constants are maximally flexible; +they allow any interpretation that is consistent with the constraints over the function or constant. +

+ +

+To illustrate uninterpreted functions and constants let us the uninterpreted integer constants (aka variables) +x, y. Finally let f be an uninterpreted function that takes one argument of type (aka sort) integer +and results in an integer value. +The example illustrates how one can force an interpretation where f +applied twice to x results in x again, but f applied once to x is different from x. +

+ + +
x = Int('x')
+y = Int('y')
+f = Function('f', IntSort(), IntSort())
+solve(f(f(x)) == x, f(x) == y, x != y)
+
+ + +

The solution (interpretation) for f should be read as f(0) is 1, f(1) is 0, and f(a) +is 1 for all a different from 0 and 1. +

+ +

In Z3, we can also evaluate expressions in the model for a system of constraints. The following example shows how to +use the evaluate method.

+ + +
x = Int('x')
+y = Int('y')
+f = Function('f', IntSort(), IntSort())
+s = Solver()
+s.add(f(f(x)) == x, f(x) == y, x != y)
+print s.check()
+m = s.model()
+print "f(f(x)) =", m.evaluate(f(f(x)))
+print "f(x)    =", m.evaluate(f(x))
+
+ + +

Satisfiability and Validity

+ +

A formula/constraint F is valid if F always evaluates to true for any assignment of appropriate values to its +uninterpreted symbols. +A formula/constraint F is satisfiable if there is some assignment of appropriate values +to its uninterpreted symbols under which F evaluates to true. +Validity is about finding a proof of a statement; satisfiability is about finding a solution to a set of constraints. +Consider a formula F containing a and b. +We can ask whether F is valid, that is whether it is always true for any combination of values for +a and b. If F is always +true, then Not(F) is always false, and then Not(F) will not have any satisfying assignment (i.e., solution); that is, +Not(F) is unsatisfiable. That is, +F is valid precisely when Not(F) is not satisfiable (is unsatisfiable). +Alternately, +F is satisfiable if and only if Not(F) is not valid (is invalid). +The following example proves the deMorgan's law. +

+ +

The following example redefines the Z3Py function prove that receives a formula as a parameter. +This function creates a solver, adds/asserts the negation of the formula, and check if the negation is unsatisfiable. +The implementation of this function is a simpler version of the Z3Py command prove. +

+ + +
p, q = Bools('p q')
+demorgan = And(p, q) == Not(Or(Not(p), Not(q)))
+print demorgan
+
+def prove(f):
+    s = Solver()
+    s.add(Not(f))
+    if s.check() == unsat:
+        print "proved"
+    else:
+        print "failed to prove"
+
+print "Proving demorgan..."
+prove(demorgan)
+
+ + +

List Comprehensions

+ +

+Python supports list comprehensions. +List comprehensions provide a concise way to create lists. They can be used to create Z3 expressions and problems in Z3Py. +The following example demonstrates how to use Python list comprehensions in Z3Py. +

+ + +
# Create list [1, ..., 5] 
+print [ x + 1 for x in range(5) ]
+
+# Create two lists containing 5 integer variables
+X = [ Int('x%s' % i) for i in range(5) ]
+Y = [ Int('y%s' % i) for i in range(5) ]
+print X
+
+# Create a list containing X[i]+Y[i]
+X_plus_Y = [ X[i] + Y[i] for i in range(5) ]
+print X_plus_Y
+
+# Create a list containing X[i] > Y[i]
+X_gt_Y = [ X[i] > Y[i] for i in range(5) ]
+print X_gt_Y
+
+print And(X_gt_Y)
+
+# Create a 3x3 "matrix" (list of lists) of integer variables
+X = [ [ Int("x_%s_%s" % (i+1, j+1)) for j in range(3) ]
+      for i in range(3) ]
+pp(X)
+
+ + +

In the example above, the expression "x%s" % i returns a string where %s is replaced with the value of i.

+ +

The command pp is similar to print, but it uses Z3Py formatter for lists and tuples instead of Python's formatter.

+ +

Z3Py also provides functions for creating vectors of Boolean, Integer and Real variables. These functions +are implemented using list comprehensions. +

+ + +
X = IntVector('x', 5)
+Y = RealVector('y', 5)
+P = BoolVector('p', 5)
+print X
+print Y
+print P
+print [ y**2 for y in Y ]
+print Sum([ y**2 for y in Y ])
+
+ + +

Kinematic Equations

+ +

+In high school, students learn the kinematic equations. +These equations describe the mathematical relationship between displacement (d), +time (t), acceleration (a), initial velocity (v_i) and final velocity (v_f). +In Z3Py notation, we can write these equations as: +

+
+   d == v_i * t + (a*t**2)/2,
+   v_f == v_i + a*t
+
+ +

Problem 1

+ +

+Ima Hurryin is approaching a stoplight moving with a velocity of 30.0 m/s. +The light turns yellow, and Ima applies the brakes and skids to a stop. +If Ima's acceleration is -8.00 m/s2, then determine the displacement of the +car during the skidding process. +

+ + +
d, a, t, v_i, v_f = Reals('d a t v__i v__f')
+
+equations = [
+   d == v_i * t + (a*t**2)/2,
+   v_f == v_i + a*t,
+]
+print "Kinematic equations:"
+print equations
+
+# Given v_i, v_f and a, find d
+problem = [
+    v_i == 30,
+    v_f == 0,
+    a   == -8
+]
+print "Problem:"
+print problem
+
+print "Solution:"
+solve(equations + problem)
+
+ + + +

Problem 2

+ +

+Ben Rushin is waiting at a stoplight. When it finally turns green, Ben accelerated from rest at a rate of +a 6.00 m/s2 for a time of 4.10 seconds. Determine the displacement of Ben's car during this time period. +

+ + +
d, a, t, v_i, v_f = Reals('d a t v__i v__f')
+
+equations = [
+   d == v_i * t + (a*t**2)/2,
+   v_f == v_i + a*t,
+]
+
+# Given v_i, t and a, find d
+problem = [
+    v_i == 0,
+    t   == 4.10,
+    a   == 6
+]
+
+solve(equations + problem)
+
+# Display rationals in decimal notation
+set_option(rational_to_decimal=True)
+
+solve(equations + problem)
+
+ + +

Bit Tricks

+ +

Some low level hacks are very popular with C programmers. +We use some of these hacks in the Z3 implementation. +

+ +

Power of two

+ +

This hack is frequently used in C programs (Z3 included) to test whether a machine integer is a power of two. +We can use Z3 to prove it really works. The claim is that x != 0 && !(x & (x - 1)) is true if and only if x +is a power of two. +

+ + +
x      = BitVec('x', 32)
+powers = [ 2**i for i in range(32) ]
+fast   = And(x != 0, x & (x - 1) == 0)
+slow   = Or([ x == p for p in powers ])
+print fast
+prove(fast == slow)
+
+print "trying to prove buggy version..."
+fast   = x & (x - 1) == 0
+prove(fast == slow)
+
+ + +

Opposite signs

+ +

The following simple hack can be used to test whether two machine integers have opposite signs.

+ + +
x      = BitVec('x', 32)
+y      = BitVec('y', 32)
+
+# Claim: (x ^ y) < 0 iff x and y have opposite signs
+trick  = (x ^ y) < 0
+
+# Naive way to check if x and y have opposite signs
+opposite = Or(And(x < 0, y >= 0),
+              And(x >= 0, y < 0))
+
+prove(trick == opposite)
+
+ + +

Puzzles

+ +

Dog, Cat and Mouse

+ +

Consider the following puzzle. Spend exactly 100 dollars and buy exactly 100 animals. +Dogs cost 15 dollars, cats cost 1 dollar, and mice cost 25 cents each. +You have to buy at least one of each. +How many of each should you buy? +

+ + +
# Create 3 integer variables
+dog, cat, mouse = Ints('dog cat mouse')
+solve(dog >= 1,   # at least one dog
+      cat >= 1,   # at least one cat
+      mouse >= 1, # at least one mouse
+      # we want to buy 100 animals
+      dog + cat + mouse == 100,
+      # We have 100 dollars (10000 cents):
+      #   dogs cost 15 dollars (1500 cents), 
+      #   cats cost 1 dollar (100 cents), and 
+      #   mice cost 25 cents 
+      1500 * dog + 100 * cat + 25 * mouse == 10000)
+
+ + +

Sudoku

+ +

Sudoku is a very popular puzzle. +The goal is to insert the numbers in the boxes to satisfy only one condition: each row, column and +3x3 box must contain the digits 1 through 9 exactly once. +

+ + + +

+The following example encodes the sudoku problem in Z3. Different sudoku instances can be solved +by modifying the matrix instance. This example makes heavy use of +list comprehensions +available in the Python programming language. +

+ + +
# 9x9 matrix of integer variables
+X = [ [ Int("x_%s_%s" % (i+1, j+1)) for j in range(9) ]
+      for i in range(9) ]
+
+# each cell contains a value in {1, ..., 9}
+cells_c  = [ And(1 <= X[i][j], X[i][j] <= 9)
+             for i in range(9) for j in range(9) ]
+
+# each row contains a digit at most once
+rows_c   = [ Distinct(X[i]) for i in range(9) ]
+
+# each column contains a digit at most once
+cols_c   = [ Distinct([ X[i][j] for i in range(9) ])
+             for j in range(9) ]
+
+# each 3x3 square contains a digit at most once
+sq_c     = [ Distinct([ X[3*i0 + i][3*j0 + j]
+                        for i in range(3) for j in range(3) ])
+             for i0 in range(3) for j0 in range(3) ]
+
+sudoku_c = cells_c + rows_c + cols_c + sq_c
+
+# sudoku instance, we use '0' for empty cells
+instance = ((0,0,0,0,9,4,0,3,0),
+            (0,0,0,5,1,0,0,0,7),
+            (0,8,9,0,0,0,0,4,0),
+            (0,0,0,0,0,0,2,0,8),
+            (0,6,0,2,0,1,0,5,0),
+            (1,0,2,0,0,0,0,0,0),
+            (0,7,0,0,0,0,5,2,0),
+            (9,0,0,0,6,5,0,0,0),
+            (0,4,0,9,7,0,0,0,0))
+
+instance_c = [ If(instance[i][j] == 0,
+                  True,
+                  X[i][j] == instance[i][j])
+               for i in range(9) for j in range(9) ]
+
+s = Solver()
+s.add(sudoku_c + instance_c)
+if s.check() == sat:
+    m = s.model()
+    r = [ [ m.evaluate(X[i][j]) for j in range(9) ]
+          for i in range(9) ]
+    print_matrix(r)
+else:
+    print "failed to solve"
+
+ + +

Eight Queens

+ +

+The eight queens puzzle is the problem of placing eight chess queens on an 8x8 chessboard so that no two queens attack each other. +Thus, a solution requires that no two queens share the same row, column, or diagonal. +

+ +

+

+ + +
# We know each queen must be in a different row.
+# So, we represent each queen by a single integer: the column position
+Q = [ Int('Q_%i' % (i + 1)) for i in range(8) ]
+
+# Each queen is in a column {1, ... 8 }
+val_c = [ And(1 <= Q[i], Q[i] <= 8) for i in range(8) ]
+
+# At most one queen per column
+col_c = [ Distinct(Q) ]
+
+# Diagonal constraint
+diag_c = [ If(i == j,
+              True,
+              And(Q[i] - Q[j] != i - j, Q[i] - Q[j] != j - i))
+           for i in range(8) for j in range(i) ]
+
+solve(val_c + col_c + diag_c)
+
+ + +

Application: Install Problem

+ +

The install problem consists of determining whether a new set of packages can be installed in a system. +This application is based on the article +OPIUM: Optimal Package Install/Uninstall Manager. +Many packages depend on other packages to provide some functionality. +Each distribution contains a meta-data file that +explicates the requirements of each package of the distribution. +The meta-data contains details like the name, version, etc. More importantly, it contains +depends and conflicts +clauses that stipulate which other packages should be on the +system. The depends clauses stipulate which other packages must be present. +The conflicts clauses stipulate which other packages must not be present. +

+ +

The install problem can be easily solved using Z3. The idea is to define a Boolean variable for each +package. This variable is true if the package must be in the system. If package a depends on +packages b, c and z, we write: +

+ +
+DependsOn(a, [b, c, z])
+
+ +

DependsOn is a simple Python function that creates Z3 constraints that capture the +depends clause semantics. +

+ +
+def DependsOn(pack, deps):
+   return And([ Implies(pack, dep) for dep in deps ])
+
+ +

+Thus, Depends(a, [b, c, z]) generates the constraint +

+ +
+And(Implies(a, b), Implies(a, c), Implies(a, z))
+
+ +

That is, if users install package a, they must also install packages +b, c and z. +

+ +

+If package d conflicts with package e, we write Conflict(d, e). +Conflict is also a simple Python function. +

+ +
+def Conflict(p1, p2):
+    return Or(Not(p1), Not(p2))
+
+ +

Conflict(d, e) generates the constraint Or(Not(d), Not(e)). +With these two functions, we can easily encode the example in the +Opium article (Section 2) in Z3Py as: +

+ + +
def DependsOn(pack, deps):
+    return And([ Implies(pack, dep) for dep in deps ])
+
+def Conflict(p1, p2):
+    return Or(Not(p1), Not(p2))
+
+a, b, c, d, e, f, g, z = Bools('a b c d e f g z')
+
+solve(DependsOn(a, [b, c, z]),
+      DependsOn(b, [d]),
+      DependsOn(c, [Or(d, e), Or(f, g)]),
+      Conflict(d, e),
+      a, z)
+
+ + +

+Note that the example contains the constraint +

+ +
+DependsOn(c, [Or(d, e), Or(f, g)]),
+
+ +

+The meaning is: to install c, we must install d or e, and f or g +

+ +

Now, we refine the previous example. First, we modify DependsOn to allow +us to write DependsOn(b, d) instead of DependsOn(b, [d]). We also +write a function install_check that returns a list of packages that must be installed +in the system. The function Conflict is also modified. It can now receive multiple +arguments. +

+ + +
def DependsOn(pack, deps):
+    if is_expr(deps):
+        return Implies(pack, deps)
+    else:
+        return And([ Implies(pack, dep) for dep in deps ])
+
+def Conflict(*packs):
+    return Or([ Not(pack) for pack in packs ])
+
+a, b, c, d, e, f, g, z = Bools('a b c d e f g z')
+
+def install_check(*problem):
+    s = Solver()
+    s.add(*problem)
+    if s.check() == sat:
+        m = s.model()
+        r = []
+        for x in m:
+            if is_true(m[x]):
+                # x is a Z3 declaration
+                # x() returns the Z3 expression
+                # x.name() returns a string
+                r.append(x())
+        print r
+    else:
+        print "invalid installation profile"
+
+print "Check 1"
+install_check(DependsOn(a, [b, c, z]),
+              DependsOn(b, d),
+              DependsOn(c, [Or(d, e), Or(f, g)]),
+              Conflict(d, e),
+              Conflict(d, g),
+              a, z)
+
+print "Check 2"
+install_check(DependsOn(a, [b, c, z]),
+              DependsOn(b, d),
+              DependsOn(c, [Or(d, e), Or(f, g)]),
+              Conflict(d, e),
+              Conflict(d, g),
+              a, z, g)
+
+ + +

Using Z3Py Locally

+ +

Z3Py is part of the Z3 distribution. It is located in the python subdirectory. +To use it locally, you have to include the following command in your Python script.

+
+from Z3 import *
+
+

+The Z3 Python frontend directory must be in your PYTHONPATH environment variable. +Z3Py will automatically search for the Z3 library (z3.dll (Windows), libz3.so (Linux), or libz3.dylib (OSX)). +You may also initialize Z3Py manually using the command: +

+
+init("z3.dll")
+
+ + + diff --git a/examples/python/tutorial/html/index.html b/examples/python/tutorial/html/index.html new file mode 100644 index 000000000..8c75ff0da --- /dev/null +++ b/examples/python/tutorial/html/index.html @@ -0,0 +1 @@ + \ No newline at end of file diff --git a/examples/python/tutorial/html/strategies-examples.htm b/examples/python/tutorial/html/strategies-examples.htm new file mode 100644 index 000000000..0d5e6424b --- /dev/null +++ b/examples/python/tutorial/html/strategies-examples.htm @@ -0,0 +1,350 @@ + + +Z3Py Strategies + + + + +

Strategies

+ +

+High-performance solvers, such as Z3, contain many tightly integrated, handcrafted heuristic +combinations of algorithmic proof methods. While these heuristic +combinations tend to be highly tuned for known classes of problems, +they may easily perform very badly on new classes of problems. +This issue is becoming increasingly pressing +as solvers begin to gain the attention of practitioners in diverse areas of science and engineering. +In many cases, changes to the solver heuristics can make a +tremendous difference. +

+ +

+In this tutorial we show how to create custom strategies using the basic building blocks +available in Z3. Z3Py and Z3 4.0 implement the ideas proposed in this article. +

+ +

+Please send feedback, comments and/or corrections to leonardo@microsoft.com. +Your comments are very valuable. +

+ +

Introduction

+ +

+Z3 implements a methodology for orchestrating reasoning +engines where "big" symbolic reasoning steps are represented as +functions known as tactics, and tactics are composed using +combinators known as tacticals. Tactics process sets of +formulas called Goals. +

+ +

+When a tactic is applied to some goal G, four different outcomes +are possible. The tactic succeeds in showing G to be satisfiable (i.e., feasible); +succeeds in showing G to be unsatisfiable (i.e., infeasible); produces a sequence of subgoals; or fails. +When reducing a goal G to a sequence of subgoals G1, ..., +Gn, we face the problem of model conversion. +A model converter construct a model for G +using a model for some subgoal Gi. +

+ +

In the following example, we create a goal g consisting of three formulas, and a tactic t +composed of two built-in tactics: simplify and solve-eqs. The tactic simplify +apply transformations equivalent to the ones found in the command simplify. The tactic solver-eqs +eliminate variables using Gaussian elimination. Actually, solve-eqs is not restricted only to linear arithmetic. +It can also eliminate arbitrary variables. Then, combinator Then applies simplify to the input goal +and solve-eqs to each subgoal produced by simplify. In this example, only one subgoal is produced. +

+ + +
x, y = Reals('x y')
+g  = Goal()
+g.add(x > 0, y > 0, x == y + 2)
+print g
+
+t1 = Tactic('simplify')
+t2 = Tactic('solve-eqs')
+t  = Then(t1, t2)
+print t(g)
+
+ + +

In the example above, variable x is eliminated, and is not present the resultant goal. +

+ +

In Z3, we say a clause is any constraint of the form Or(f_1, ..., f_n). +The tactic split-clause will select a clause Or(f_1, ..., f_n) in the input goal, and split it +n subgoals. One for each subformula f_i. +

+ + +
x, y = Reals('x y')
+g  = Goal()
+g.add(Or(x < 0, x > 0), x == y + 1, y < 0)
+
+t = Tactic('split-clause')
+r = t(g)
+for g in r: 
+    print g
+
+ + +

Tactics

+ +

Z3 comes equipped with many built-in tactics. +The command describe_tactics() provides a short description of all built-in tactics. +

+ + +
describe_tactics()
+
+ + +

Z3Py comes equipped with the following tactic combinators (aka tacticals): +

+ + + +

The following example demonstrate how to use these combinators.

+ + +
x, y, z = Reals('x y z')
+g = Goal()
+g.add(Or(x == 0, x == 1), 
+      Or(y == 0, y == 1), 
+      Or(z == 0, z == 1),
+      x + y + z > 2)
+
+# Split all clauses"
+split_all = Repeat(OrElse(Tactic('split-clause'),
+                          Tactic('skip')))
+print split_all(g)
+
+split_at_most_2 = Repeat(OrElse(Tactic('split-clause'),
+                          Tactic('skip')),
+                         1)
+print split_at_most_2(g)
+
+# Split all clauses and solve equations
+split_solve = Then(Repeat(OrElse(Tactic('split-clause'),
+                                 Tactic('skip'))),
+                   Tactic('solve-eqs'))
+
+print split_solve(g)
+
+ + +

In the tactic split_solver, the tactic solve-eqs discharges all but one goal. +Note that, this tactic generates one goal: the empty goal which is trivially satisfiable (i.e., feasible)

+ +

The list of subgoals can be easily traversed using the Python for statement.

+ + +
x, y, z = Reals('x y z')
+g = Goal()
+g.add(Or(x == 0, x == 1), 
+      Or(y == 0, y == 1), 
+      Or(z == 0, z == 1),
+      x + y + z > 2)
+
+# Split all clauses"
+split_all = Repeat(OrElse(Tactic('split-clause'),
+                          Tactic('skip')))
+for s in split_all(g):
+    print s
+
+ + +

A tactic can be converted into a solver object using the method solver(). +If the tactic produces the empty goal, then the associated solver returns sat. +If the tactic produces a single goal containing False, then the solver returns unsat. +Otherwise, it returns unknown. +

+ + +
bv_solver = Then('simplify', 
+                 'solve-eqs', 
+                 'bit-blast', 
+                 'sat').solver()
+
+x, y = BitVecs('x y', 16)
+solve_using(bv_solver, x | y == 13, x > y)
+
+ + +

In the example above, the tactic bv_solver implements a basic bit-vector solver using equation solving, +bit-blasting, and a propositional SAT solver. Note that, the command Tactic is suppressed. +All Z3Py combinators automatically invoke Tactic command if the argument is a string. +Finally, the command solve_using is a variant of the solve command where the first +argument specifies the solver to be used. +

+ +

In the following example, we use the solver API directly instead of the command solve_using. +We use the combinator With to configure our little solver. We also include the tactic aig +which tries to compress Boolean formulas using And-Inverted Graphs. +

+ + +
bv_solver = Then(With('simplify', mul2concat=True),
+                 'solve-eqs', 
+                 'bit-blast', 
+                 'aig',
+                 'sat').solver()
+x, y = BitVecs('x y', 16)
+bv_solver.add(x*32 + y == 13, x & y < 10, y > -100)
+print bv_solver.check()
+m = bv_solver.model()
+print m
+print x*32 + y, "==", m.evaluate(x*32 + y)
+print x & y, "==", m.evaluate(x & y)
+
+ + +

The tactic smt wraps the main solver in Z3 as a tactic.

+ + +
x, y = Ints('x y')
+s = Tactic('smt').solver()
+s.add(x > y + 1)
+print s.check()
+print s.model()
+
+ + +

Now, we show how to implement a solver for integer arithmetic using SAT. The solver is complete +only for problems where every variable has a lower and upper bound. +

+ + +
s = Then(With('simplify', arith_lhs=True, som=True),
+         'normalize-bounds', 'lia2pb', 'pb2bv', 
+         'bit-blast', 'sat').solver()
+x, y, z = Ints('x y z')
+solve_using(s, 
+            x > 0, x < 10, 
+            y > 0, y < 10, 
+            z > 0, z < 10,
+            3*y + 2*x == z)
+# It fails on the next example (it is unbounded)
+s.reset()
+solve_using(s, 3*y + 2*x == z)
+
+ + +

+Tactics can be combined with solvers. For example, we can apply a tactic to a goal, produced a set of subgoals, +then select one of the subgoals and solve it using a solver. The next example demonstrates how to do that, and how to +use model converters to convert a model for a subgoal into a model for the original goal. +

+ + +
t = Then('simplify', 
+         'normalize-bounds', 
+         'solve-eqs')
+
+x, y, z = Ints('x y z')
+g = Goal()
+g.add(x > 10, y == x + 3, z > y)
+
+r = t(g)
+# r contains only one subgoal
+print r
+
+s = Solver()
+s.add(r[0])
+print s.check()
+# Model for the subgoal
+print s.model()
+# Model for the original goal
+print r.convert_model(s.model())
+
+ + +

Probes

+ +

+Probes (aka formula measures) are evaluated over goals. +Boolean expressions over them can be built using relational operators and Boolean connectives. +The tactic FailIf(cond) fails if the given goal does not satisfy the condition cond. +Many numeric and Boolean measures are available in Z3Py. The command describe_probes() provides the list of +all built-in probes. +

+ + +
describe_probes()
+
+ + +

In the following example, we build a simple tactic using FailIf. It also shows that a probe can be applied directly +to a goal.

+ + +
x, y, z = Reals('x y z')
+g = Goal()
+g.add(x + y + z > 0)
+
+p = Probe('num-consts')
+print "num-consts:", p(g)
+
+t = FailIf(p > 2)
+try:
+    t(g)
+except Z3Exception:
+    print "tactic failed"
+
+print "trying again..."
+g = Goal()
+g.add(x + y > 0)
+print t(g)
+
+ + +

Z3Py also provides the combinator (tactical) If(p, t1, t2) which is a shorthand for:

+ +
OrElse(Then(FailIf(Not(p)), t1), t2)
+ +

The combinator When(p, t) is a shorthand for:

+ +
If(p, t, 'skip')
+ +

The tactic skip just returns the input goal. +The following example demonstrates how to use the If combinator.

+ + +
x, y, z = Reals('x y z')
+g = Goal()
+g.add(x**2 - y**2 >= 0)
+
+p = Probe('num-consts')
+t = If(p > 2, 'simplify', 'factor')
+
+print t(g)
+
+g = Goal()
+g.add(x + x + y + z >= 0, x**2 - y**2 >= 0)
+
+print t(g)
+
+ + + +