Movatterモバイル変換

1. Introduction

Satisfiability Modulo Theories (SMT) problem is a decision problem for logical formulas with respect to combinations of background theories such as arithmetic, bit-vectors, arrays, and uninterpreted functions.Z3 is an efficient SMT solver with specialized algorithms for solving backgroundtheories. SMT solving enjoys a synergetic relationship with software analysis, verification and symbolic execution tools. This is in many respects thanks to the emphasis on supporting domains commonly found in programs and specifications.There are several scenarios where part of a query posed by these tools can be cast in terms of formulas in a supported logic. It is then useful for thetool writer to have an idea of what are available supported logics, and have an idea of how formulas are solved. But interacting with SMTsolvers is not always limited to posing a query as a single formula. It may require a sequence of interactions to obtain a usable answerand the need emerges for the tool writer for having an idea of what methods and knobs are available. In summary, this tutorial aims to answer the following types of questionsthrough examples and a touch of theory:

• What are the available features in Z3, and what are they designed to be used for?

• What are the underlying algorithms used in Z3?

• How can I program applications on top of Z3?

Figure 1 shows an overall systems diagram of Z3, as of version 4.8.The top left summarizes the interfaces to Z3. One can interact with Z3 over SMT-LIB2 scripts supplied as a text file or pipe to Z3, or using API calls from a high-level programming language that are proxies for calls over a C-based API. We focus on using the Python front-end as a means ofinterfacing with Z3, and start out describing the abstract syntax of terms andformulas accepted by Z3 in Section 2.Formulas draw from symbols whose meaning are defined by a set ofTheories, Section 3.Solvers, Sections 4, 5 and 6, provide services for deciding satisfiability of formula.Tactics, Section 7, provide means forpre-processing simplification and creating sub-goals. Z3 also provides some servicesthat are not purely satisfiability queries.Optimization, Section 8,services allow users to solve satisfiability modulo objective functions to maximize orminimize values. There are also specialized procedures for enumeratingconsequences (backbone literals)described in Section 4.6.6.

1.1. Resources

The main point of reference for Z3 is the GitHub repository

Examples from this tutorial that are executable can be found on

There are several systems that program with Z3. They use a variety of front-ends, some use OCaml, others C++, and others use the SMT-LIB2 text interfaces. A few instances that use the Python front-end include

• Dennis Yurichev assembled a significant number of case studiesdrawn from puzzles and code analysis and presents many of theexamples using the Python front-endhttps://​yurichev.​com/​writings/​SAT_​SMT_​by_​example.​pdf.

• The Ivy system is written in Python and uses Z3

  https://​github.​com/​Microsoft/​ivy.

• The binary analysis kit Angr system is written in Python and uses Z3

  https://​docs.​angr.​io/​.

• There is an online tutorial of z3

  https://​microsoft.​github.​io/​z3guide.

1.2. Sources

The material in this tutorial is assembled from several sources.Some of the running examples originate from slides that have circulated in the SAT and SMT community. The first SAT example isshamelessly lifted from Armin Biere's SAT tutorials and other examples appear in slides by Natarajan Shankar.

2. Logical Interfaces to Z3

Z3 takes as input simple-sorted formulas that may contain symbols with pre-defined meanings defined by atheory.This section provides an introduction to logical formulas that can be used as input to Z3.

As a basis, propositional formulas are built from atomic variables and logical connectives.An example propositional logical formulaaccepted by Z3 is:

from z3import *Tie,Shirt=Bools('Tie Shirt')  s=Solver()  s.add(Or(Tie,Shirt),Or(Not(Tie),Shirt),Or(Not(Tie),Not(Shirt)))print(s.check())print(s.model())

The example introduces two Boolean variablesTie andShirt. It then creates aSolver object and adds three assertions.

The call tos.check() produces a verdictsat; there is a satisfying assignment for the formulas. A satisfying model, whereTie is false andShirt is true, can be extracted usings.model().For convenience the Python front-end to Z3 contains some shorthand functions. The functionsolve sets up a solver, adds assertions, checks satisfiability, and prints a model if one is available.

Propositional logic is an important, but smaller subset of formulas handled by Z3. It can reason about formulas that combine symbols from several theories, such as the theories for arrays and arithmetic:

Z=IntSort()  f=Function('f',Z,Z)  x, y, z=Ints('x y z')A=Array('A',Z,Z)  fml=Implies(x +2 == y, f(Store(A, x,3)[y -2]) == f(y - x +1))  solve(Not(fml))

The formulafml is valid. It is true for all values of integersx,y,z, arrayA, and no matter what the graph of the functionf is. Note thatz does not even occur in the formula, but we declare it here because we will usez to represent an integer variable.Note that we are usingarray[index] as shorthand forSelect(array, index).We can manually verify the validity of the formula using the following argument:The integer constantsx andy are created using the functionInts thatcreates a list of integer constants.Under the assumption thatx + 2 = y, the right side of the implication simplifies to

f(Store(A, x,3)[x]) == f(3)

as we have replaced occurrences ofy byx + 2. There are no restrictions on whatf is, sothe equality withf on both sides will only follow if the arguments tof are the same. Thus, we are left to establish

Store(A, x,3)[x] ==3

The left side is a term in the theory of arrays, which captures applicative maps.Store updates the arrayAat positionx with the value 3. Then...[x] retrieves the contents of the array at indexx, which in thiscase is 3.Dually, thenegation offml is unsatisfiable and the call to Z3 producesunsat.

Formulas accepted by Z3 generally follow the formats described in the SMT-LIB2 standard [4].This standard (currently at version 2.6) defines a textual language for first-order multi-sortedlogic and a set oflogics that are defined by a selection of background theories. For example, the logic ofquantifier-free linear integer arithmetic, known in SMT-LIB2 asQF_LIA, is a fragment of first-order logic, where formulas arequantifier free, variables range over integers, interpreted constants are integers, the allowed functions are+,-, integer multiplication, division, remainder, modulus with a constant, and the allowed relationsare, besides equality that is part of every theory, also<, <=, >=, >.As an example, we provide an SMT-LIB and a Python variant of the same arbitrary formula:

 (set-logicQF_LIA) (declare-const xInt) (declare-const yInt) (assert (> (+ (mod x4) (*3 (div y2))) (- x y))) (check-sat)

Python version:

 solve((x %4) +3 * (y /2) > x - y)

It is also possible to extract an SMT-LIB2 representation of a solver state.

from z3import *x, y=Ints('x y')s=Solver()s.add((x %4) +3 * (y /2) > x - y)print(s.sexpr())

produces the output

(declare-fun y ()Int)(declare-fun x ()Int)(assert (> (+ (mod x4) (*3 (div y2))) (- x y)))

2.1. Sorts

Generally, SMT-LIB2 formulas use a finite set of simple sorts. It includes the built-in sortBool, and supported theoriesdefine their own sorts, noteworthyInt,Real, bit-vectors(_BitVec n)for every positive bit-widthn, arrays
(ArrayIndexElem) for every sortIndex andElem,String and sequences(SeqS) for every sortS.It is also possible to declare new sorts. Their domains may never be empty.Thus, the formula

S=DeclareSort('S') s=Const('s',S) solve(ForAll(s, s != s))

is unsatisfiable.

2.2. Signatures

Formulas may include a mixture of interpreted and free functions and constants.For example, the integer constants 0 and 28 are interpreted, while constantsx,y used in the previous example are free. Constants are treated as nullary functions.Functions that take arguments can be declared, such asf = Function('f', Z, Z) creates the function declaration that takes one integerargument and its range is an integer. Functions with Boolean range can be used to createformulas.

2.3. Terms and Formulas

Formulas that are used in assertions or added to solvers are terms of Boolean sort. Otherwise, terms of Boolean and non-Boolean sortmay be mixed in any combination where sorts match up.For example

B=BoolSort()f=Function('f',B,Z)g=Function('g',Z,B)a=Bool('a')solve(g(1+f(a)))

could produce a solution of the form

[a=False, f= [else ->0], g= [else ->True]]

The model assignsa to False, the graph off mapsall arguments to0, and the graph ofg maps all values toTrue.Standard built-in logical connectives areAnd, Or, Not, Implies, Xor. Bi-implication is a special case of equality, so from Python, when sayinga == b for Booleana andb it is treated as a logical formula for the bi-implication ofa andb.

A set of utilities are available to traverse expressions once they are created.Every function application has a functiondeclaration and a set ofargumentsaccessed as children.

x=Int('x')y=Int('y')n= x + y >=3print("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())

2.4. Quantifiers and Lambda binding

Universal and existential quantifiers bind variables to the scope of the quantifiedformula. For example

solve([y == x +1,ForAll([y],Implies(y <=0, x < y))])

has no solution because no matter what value we assigned tox, there is a value fory that is non-positive and smaller than that value. The bound occurrence ofy is unrelated to the free occurrence wherey is restricted to bex + 1.The equality constrainty == x + 1 should also not be mistaken for an assignment toy. It isnot the case thatbound occurrences ofy are a synonym forx + 1.Notice that the slightly different formula

solve([y == x +1,ForAll([y],Implies(y <=0, x > y))])

has a solution wherex is 1 and the free occurrence ofy is 2.

Z3 supports also-binding with rudimentary reasoning support based on a model-constructing instantiation engine.s may be convenient when expressing properties of arrays and Z3 uses array sorts for representing thesorts of lambda expressions. Thus, the result ofmemset is an array from integers to integers, that produces the valuey in the range fromlo tohi and otherwise behaves asm outside the range.Z3 reasons about quantifier free formulas that containsmemset by instantiating the body ofthe.

m, m1=Array('m',Z,Z),Array('m1',Z,Z)def memset(lo, hi, y, m):returnLambda([x],If(And(lo <= x, x <= hi), y,Select(m, x)))solve([m1 == memset(1,700, z, m),Select(m1,6) != z])

Lambda binding is convenient for creating closures. Recall that meainingofLambda([x,y], e), wheree is an expression with freeoccurrences ofx andy is as a function that takes two argumentsand substitutes their values forx andy ine.Z3 uses Lambda lifting, in conjunction with Reynold's defunctionalization, to reduce reasoning about closures to universally quantified definitions.Z3 treats arrays as general function spaces. All first-order definable functions may be arrays.Some second-order theorems can be established by synthesizing terms by instantiation.Thus,

Q=Array('Q',Z,B)prove(Implies(ForAll(Q,Implies(Select(Q, x),Select(Q, y))),               x == y))

is provable. Z3 synthesizes an instantiation corresponding toLambda(z, z == x) forQ.

3. Theories

We will here summarize the main theories supported in Z3. In a few cases we will give a brief taste of decision procedures used for these theories. Readers who wish to gain a more in-depth understanding of how these decision procedures are implemented may follow some of thecitations.

3.1. EUF: Equality and Uninterpreted Functions

The logic ofequality and uninterpreted function, EUF, is a basic ingredient for first-order predicate logic.Before there are theories, there are constants, functions and predicate symbols, and the built-in relation of equality.In the following example,f is a unary function,x a constant. The first invocation ofsolve is feasible witha model wherex is interpreted as an element inS andf is an identify function. The second invocation ofsolveis infeasible; there are no models wheref mapsx to anything but itself given the two previous equalities.

S=DeclareSort('S')  f=Function('f',S,S)  x=Const('x',S)  solve(f(f(x)) == x, f(f(f(x))) == x)  solve(f(f(x)) == x, f(f(f(x))) == x, f(x) != x)

Decision procedures for quantifier-free EUF formulas are usually based onunion-find [59] to maintain equivalence classes of terms that are equated.Pictorially, a sequence of equality assertions produceone equivalence class that captures the transitivity of equality.

It is possible to check for satisfiability of disequalities by checking whetherthe equivalence classes associated with two disequal terms are the same or not.Thus, adding does not produce a contradiction, and it can be checkedby comparing's class representative with's representative.

On the other hand, when asserting, we can deduce a conflict asthe two terms asserted to be disequal belong to the same class. Class membershipwith union-find data-structures is amortized nearly constant time.

Union-find alone is insufficient when function symbols are used, as with the following example,

In this case decision procedures require reasoning with the congruence rule

As a preparation for solving our example, let us introduce constantsthat can be used as shorthands for sub-terms. Thus, introduceconstants as representatives for thefour compound sub-terms.

Having only the equality information available we obtain the equivalence classes:

Working bottom-up, the congruence rule dictates that the classes for andshould be merged. Thus,

implies the following coarser set of equivalences.

At this point, the congruence rule can be applied a second time,

producing the equivalence classes

The classes for and are now merged. As our original formula required these tobe distinct, congruence closure reasoning determines that the formula is unsatisfiable.

3.1.1. Congruence Closure

We have implicitly used the notion ofcongruence closure [27] to check satisfiability of equalities.Let us more formally define this notion.Let be a set of terms and set of equalities over.Acongruence closure over modulo is the finest partition of, such that:

• if, then are in the same partition in.

• for,

  • if are in same partition of for each,
  • then are in the same partition under.

3.1.2. EUF Models

A satisfiable version of the running example is:

It induces the following definitions and equalities:
and we can associate a distinct value with each equivalence class.

When presenting the formula to Z3 as

S=DeclareSort('S')a, b, c, d, e, s, t=Consts('a b c d e s t',S)f=Function('f',S,S,S)g=Function('g',S,S)solve([a == b, b == c, d == e, b == s,        d == t, f(a, g(d)) != f(g(e), b)])

it produces a model, that may look as follows:

[s=S!val!0, b=S!val!0, a=S!val!0, c=S!val!0, d=S!val!1, e=S!val!1, t=S!val!1, f= [(S!val!2,S!val!0) ->S!val!4,else ->S!val!3], g= [else ->S!val!2]]

In the model the valueS!val!0 is a fresh constant that is distinct fromS!val!1.The graph forf maps the arguments(S!val!2, S!val!0) toS!val!4. Allother arguments are mapped by theelse clause toS!val!3. Theelse clauseis used as the default interpretation of arguments that are not listed in the interpretation.The interpretation ofS is a finite set

    {S!val!0,S!val!1,S!val!2,S!val!3,S!val!4}.

3.2. Arithmetic

Arithmetical constraints are nearly ubiquitous in software models. Even though mainstream software operates with finite precision arithmetic,that is modeled precisely using bit-vectors, arithmetic over unbounded integers can often be used in a sound way to model software. Furthermore, arithmetic over the reals has been used for diverse areas such as models of cyber-physical systems or for axiomatic economics.

3.2.1. Solving LRA: Linear Real Arithmetic

We provide an outline of Z3's main procedure for solving formulas over linear real arithmetic [28].It maintains a (dual) Simplex tableau that encodes equalities of the form. Feasibility of the equalities depends on bounds,, currently associated with the variables.For the following formula

  x, y=Reals('x y')  solve([x >=0,Or(x + y <=2, x +2*y >=6),Or(x + y >=2, x +2*y >4)])

Z3 introduces auxiliary variables and represents the formula as

Only bounds (e.g.,) are asserted during search.

The first two equalities form the tableau. Thus, the definitionsproduce the equalities

They are equivalent to the normal form:

where are basic (dependent) and are non-basic.In dual Simplex tableaux, values of a non-basic variable can be chosen between and.The value of a basic variable is a function of non-basic variable values.It is the unique value that satisfies the unique row where the basic variable occurs. Pivoting swaps basic and non-basic variables and is used to get values of basic variables within bounds.For example, assume we start with a set of initial valuesand bounds. Then has to be 2 and it is made non-basic. Instead becomes basic:

The new tableau updates the assignment of variables to. The resulting assignmentis a model for the original formula.

3.2.2. Solving Arithmetical Fragments

The solvers available to reason about arithmetical constraints are wildly differentdepending on what fragments of arithmetic is used.We summarize the main fragments, available decision procedures, and examples in Table 1 where range over reals and range over integers.

There are many more fragments of arithmetic that benefit from specialized solvers. We later discuss some of the fragments where integer variables are restricted to the valueswhen describing Pseudo-Boolean constraints. Other fragments that arenot currently handled in Z3 in any special wayinclude fragments listed in Table 2.

A user of Z3 may appreciate that a domain can be modeled using a fragment of the theory of arithmetic thatis already supported, or belongs to a class where no special support is available. On a practical side, it is worth noting that Z3 uses infinite precision arithmetic by default. Thus, integers and rationals are represented without rounding. The benefit is that the representation ensures soundness of the results, but operations by decision procedures mayend up producing large numerals taking most of the execution time. Thus, users who produce linear arithmeticconstraints with large coefficients or long decimal expansions may face performance barriers.

3.3. Arrays

The declaration

A=Array('A',IntSort(),IntSort())

introduces a constantA of the array sort mappingintegers to integers. We can solve constraints over arrays, such as

solve(A[x] == x,Store(A, x, y) ==A)

which produces a solution wherex necessarily equalsy.

Z3 treats arrays as function spaces, thus a functionf(x, y)can be converted to an array using a

Lambda([x, y], f(x, y))

Iff has sort, thenLambda([x, y], f(x, y)) has sortArray(A,B,C).A set of built-in functions are available forarrays. We summarize them together with theirrepresentation usingLambdabindings.

    a[i]# select array 'a' at index 'i'# Select(a, i)Store(a, i, v)# update array 'a' with value 'v' at index 'i'# = Lambda(j, If(i == j, v, a[j]))K(D, v)# constant Array(D, R), where R is sort of 'v'.# = Lambda(j, v)Map(f, a)# map function 'f' on values of 'a'# = Lambda(j, f(a[j]))Ext(a, b)# Extensionality# Implies(a[Ext(a, b)] == b[Ext(a, b)], a == b)

3.3.1. Deciding Arrays by Reduction to EUF

Formulas using the combinatorsStore, K, Map, Ext are checked for satisfiability byexpanding the respective definitionson sub-terms. We illustrate how occurrences ofStore produce constraints over EUF. In the following, assume we are given a solvers with ground assertions using arrays.

For each occurrence ins ofStore(a, i, v) andb[j], add the following assertions:

• s.add(Store(a, i, v)[j] ==If(i == j, v, a[j]))
• s.add(Store(a, i, v)[i] == v)

The theory of arrays isextensional. That is, two arrays are equal if they behave the same on all selected indices. When Z3 producesmodels for quantifier free formulas in the theory of extensional arraysit ensures that two arrays are equal in a model whenever they behave the sameon all indices.Extensionality is enforced on array terms, insby instantiating the axiom of extensionality.

• s.add(Implies(ForAll(i, a[i] == b[i]), a == b))

Since the universal quantifier occurs in a negative polarity we can introduce aSkolem functionExt that depends ona andb and represent the extensionalityrequirement as:

• s.add(Implies(a[Ext(a, b)] == b[Ext(a, b)], a == b))

We can convince ourselves that asserting these additional constraints force models of a solvers to satisfy the array axioms.Suppose we are given a model satisfying all the additional asserted equalities.These equalities enforce the axioms forStore on all indices that occur ins. They also enforce extensionality between arrays: Two arrays are equal if and only if theyevaluate to the same value on all indices ins.

3.4. Bit-Vectors

Let us play with some bit-fiddling.The resource

lists a substantialrepertoire of bit-vector operations that can be used as alternatives to potentially more expensiveoperations.Note that modern compilers already contain a vast set of optimizations that automatically performthese conversions and Z3 can be used to check and synthesize such optimizations [46].For example, to test whether a bit-vector is a power of two we can use a combinationof bit-wise operations and subtraction:

def is_power_of_two(x):returnAnd(x !=0,0 == (x & (x -1)))x=BitVec('x',4)prove(is_power_of_two(x) ==Or([x ==2**ifor iin range(4)]))

The absolute value of a variable can be obtained using addition and xor with a sign bit.

v=BitVec('v',32)mask= v >>31prove(If(v >0, v, -v) == (v + mask) ^ mask)

Notice that the Python variablemask corresponds to the expressionv >>31, the right arithmetic (signed) shift ofv.Notice also, that in classical first-order logic, all operations aretotal.In particular, for bit-vector arithmetic-v is fully specified, in contrastto, say C, which specifies that-v isundefined whenvis a signed integer with the value.

3.4.1. Solving bit-vectors

Z3 mostly uses a bit-blasting approach to deciding bit-vectors.By bit-blasting we refer to a reduction of bit-vector constraints topropositional logic by treating each bit in a bit-vector as a propositional variable.Let us illustrate how bit-vector addition is compiled to a set ofclauses. The expressionv + w, wherev andware bit-vectors is represented by a vectorout of output bits.The relation betweenv,w andout is provided by clausesthe encode a ripple-carry adder seen in Figure 2. The encoding usesan auxiliary vector ofcarry bits that are internal to the adder.

3.4.2. Floating Point Arithmetic

Floating points are bit-vectors with an interpretation specified by the IEEE floating point standard.

x=FP('x',FPSort(3,4))print(10 + x)

It declares a floating point numberx with 3 bits in the exponent and 4 for the significand.The result of adding 10 tox is1.25*(2**3) + x. We see that 10 is representedas a floating point number with exponent 3, that is the bit-vector 011. The significandis 1010.

3.5. Algebraic Datatypes

The theory of first-order algebraic data-types captures the theory of finite trees.It is characterized by the properties that:

• All trees are finite (occurs check).

• All trees are generated from the constructors (no junk).

• Two trees are equal if and only if they are constructed exactly the same way (no confusion).

A basic example of a binary tree data-type is given in Figure 3.

Tree=Datatype('Tree')Tree.declare('Empty')Tree.declare('Node', ('left',Tree), ('data',Z), ('right',Tree))Tree=Tree.create()t=Const('t',Tree)solve(t !=Tree.Empty)

It may produce the solution

[t=Node(Empty,0,Empty)]

Similarly, one can prove that a tree cannot be a part of itself.

prove(t !=Tree.Node(t,0, t))

3.6. Sequences and Strings

The theory of strings and sequences extend on the theory of the free monoidwith a few additional functions that are useful for strings and sequences.A length operation is built-in for strings and sequences, andthere are operations for converting strings to natural numbers and back.

If the lengths of a prefix and suffix of a string add up to the lengthof the string, the string itself must be the concatenation of the prefix and suffix:

s, t, u=Strings('s t u')prove(Implies(And(PrefixOf(s, t),SuffixOf(u, t),Length(t) ==Length(s) +Length(u)),              t ==Concat(s, u)))

One can concatenate single elements to a sequence as units:

s, t=Consts('s t',SeqSort(IntSort()))solve(Concat(s,Unit(IntVal(2))) ==Concat(Unit(IntVal(1)), t))prove(Concat(s,Unit(IntVal(2))) !=Concat(Unit(IntVal(1)), s))

There are two solvers available in Z3 for strings. They can be exchangedby setting the parameter

• s.set("smt.string_solver","seq") with contributions by Thai Trinh, or
• s.set("smt.string_solver","z3str3") by Murphy Berzish.

3.7. Special Relations

In some cases it is possible to use first-order axioms to capture all requiredproperties of relations. For example, to say thatR is a partial order it suffices to assert the axioms:

  s=Solver()A=DeclareSort("A")R=Function('R',A,A,B)  x, y, z=Consts('x y z',A)  s.add(ForAll([x],R(x, x)))    s.add(ForAll([x,y],Implies(And(R(x, y),R(y, x)), x == y)))  s.add(ForAll([x,y,z],Implies(And(R(x, y),R(y, z)),R(x, z))))# and other assertions using R

The catch is that reasoning aboutR often requires instantiating the full transitive closure of the relation. This is impractical when the numberof instances can lead to a quadratic overhead compared to the size of the initialconstraints. For example, when assertings.add(R(a1,a2),R(a2,a3),...,R(a999,a1000))we obtain half a million instances. Instead of axiomatizing a relation to be a partialordering, Z3 allows to declare a relation that as a built-in property satisfies the partialordering axioms. Thus, the definition

R=PartialOrder(A,0)

creates a binary relationR overA that satisfiesthe partial order axioms. The second argument is an unsigned integer used to distinguish the partial orderR from other partial order relations over the same signature. ThusPartialOrder(A,2) creates a partial ordering relation thatis different fromR because it uses a different index. As usual, other properties of the relation have to be added to the solvers. The built-in decision procedure for partial orders avoids the quadraticinstantiation from the transitive closure axiom. It reasons about graph reachability to check consistency of assertions involvingR.

Other binary relations that have special relations support areTotal Linear orders:

  s.Add(ForAll([x],R(x, x)))    s.Add(ForAll([x,y],Implies(And(R(x, y),R(y, x)), x == y)))  s.Add(ForAll([x,y,z],Implies(And(R(x, y),R(y, z)),R(x, z))))  s.Add(ForAll([x,y],Or(R(x, y),R(y, x))))# use instead:R=LinearOrder(A,0)

Tree-like orderings:

  s.Add(ForAll([x],R(x, x)))    s.Add(ForAll([x,y],Implies(And(R(x, y),R(y, x)), x == y)))  s.Add(ForAll([x,y,z],Implies(And(R(x, y),R(y, z)),R(x, z))))  s.Add(ForAll([x,y,z],Implies(And(R(x, y),R(x, z)),Or(R(y, z),R(z, y)))))# use instead:R=TreeOrder(A,0)

Piecewise Linear orders:

  s.Add(ForAll([x],R(x, x)))    s.Add(ForAll([x,y],Implies(And(R(x, y),R(y, x)), x == y)))  s.Add(ForAll([x,y,z],Implies(And(R(x, y),R(y, z)),R(x, z))))  s.Add(ForAll([x,y,z],Implies(And(R(x, y),R(x, z)),Or(R(y, z),R(z, y)))))  s.Add(ForAll([x,y,z],Implies(And(R(y, x),R(z, x)),Or(R(y, z),R(z, y)))))# use instead:R=PiecewiseLinearOrder(A,0)

Additional examples of special relations constraints are available online.

3.8. Transitive Closure

The transitive closure of a relation is a property that cannot be fully axiomatized usingfirst-order formalisms. Quantifier-free formulas using the transitive closure of relationsremain decidable, however, using a finite model construction.Given a relation binaryR, thetransitive closure ofR is anotherrelationTC_R that relates two elements by if there is a non-empty paththat connect them throughR. To create a transitive closure or transitive reflexive closure ofR.

R=Function('R',A,A,B)TC_R=TransitiveClosure(R)  s=Solver()  a, b, c=Consts('a b c',A)  s.add(R(a, b))  s.add(R(b, c))  s.add(Not(TC_R(a, c)))print(s.check())# produces unsat

4. Interfacing with Solvers

Solvers maintain a set of formulas and supports satisfiability checking, and scope management: Formulas that are added under one scope can beretracted when the scope is popped. In this section we describe the interfaceto solvers. Section 5 provides a set of use cases and section 6 describes the underlying solverimplementations available in Z3.

4.1. Incrementality

Solvers can be used to check satisfiability of assertions in an incremental way.An initial set of assertions can be checked for satisiability followedby additional assertions and checks. Assertions can be retracted usingscopes that are pushed and popped. Under the hood, Z3 uses a one-shot solverduring the first check. If further calls are made into the solver, the default behavior is to switch to anincremental solver. The incremental solver uses the SMT core, see 6.1, by default. For use-cases that don't require all features by the SMT core, it may be beneficiary to use specializedsolvers, such as solvers for finite domains (bit-vectors, enumeration types, bounded integers, and Booleans)as specified using theQF_FD logic.

4.2. Scopes

The operationspush andpop create, respectively revert, local scopes. Assertions that are added within apushare retracted on a matchingpop. Thus, the following sessionresults in the verdictssat,unsat, andsat.

p, q, r=Bools('p q r')s=Solver()s.add(Implies(p, q))s.add(Not(q))print(s.check())s.push()s.add(p)print(s.check())s.pop()print(s.check())

4.3. Assumptions

Alternative to scopes, it is possible to check satisfiability under the assumption of a set of literals.Thus, the session

s.add(Implies(p, q))s.add(Not(q))print(s.check(p))

also produces the verdictunsat as the conjunction of,, isunsat.The methodassert_and_track(q, p) has the same effect of addingImplies(p, q),and it addsp as an implicit assumption. Our running example becomes

p, q=Bools('p q')s=Solver()s.add(Not(q))s.assert_and_track(q, p)print(s.check())

4.4. Cores

We can extract a subset of assumptions used to derive unsatisfiability. Such subsets of assumptions are known asunsatisfiable cores, or simply as acore.In the following example, the unsatisfiable core has the single elementp. The unrelated assumptionv does not appear in the core.

p, q, r, v=Bools('p q r v')s=Solver()s.add(Not(q))s.assert_and_track(q, p)s.assert_and_track(r, v)print(s.check())print(s.unsat_core())

Note that we invokes.check() prior to extracting a core.Cores are only available after the last call tos.check() producedunsat.

By default solvers do not return minimal cores. A core isminimal if there is no proper subset that is also a core.The default behavior can be changed when the solvercorresponds to either the SMT Core or SAT Core(if the underlying solver is created from a sequence ofpre-processing tactics, core minimization is not guaranteed to take effect).To force core minimization users can rely on setting the following parameters:

def set_core_minimize(s):    s.set("sat.core.minimize","true")# For Bit-vector theories    s.set("smt.core.minimize","true")# For general SMT

4.5. Models

Whens.check() returnssat Z3 can provide a model that assigns valuesto the free constants and functions in the assertions. The current model is accessedusings.model() and it offers access to an interpretation of the active assertions ins. Consider the example:

f=Function('f',Z,Z)x, y=Ints('x y')s.add(f(x) > y, f(f(y)) == y)print(s.check())print(s.model())

A possible model fors is:

[y=0, x=2, f= [0 ->3,3 ->0,else ->1]]

You can access models. They have a set of entries. Each entry maps a constant or function declaration(constants are treated as nullary functions) to aninterpretation. It maps constants to a constantexpression and it maps functions to afunction interpretation.The stub

m= s.model()for din m:print(d, m[d])

iterates over the assignments in a model and produces the output

y0x2f [0 ->3,3 ->0,else ->1]

Function interpretations comprise a set of entries that specifyhow the function behaves on selected argument combinations, and aelse_value that covers arguments not listed in the entries.

num_entries= m[f].num_entries()for iin range(num_entries):print(m[f].entry(i))print("else", m[f].else_value())

It produces the output

[0,3][3,0]else1

The easiest way to access a model is to use theeval methodthat lets you evaluate arbitrary expressions over a model. It reduces expressions to a constant that is consistent with theway the model interprets the constants and functions. For our model from above

print(m.eval(x), m.eval(f(3)), m.eval(f(4)))

produces the output 2, 0, 1.

4.6. Other Methods

4.6.1. Statistics

You can gain a sneak peek at what the solver did by extracting statistics.The call

print(s.statistics())

displays values of internal counters maintained by the decision procedures.They are mostly valuable when coupled with a detailed understanding of howthe decision procedures work, but may be used as an introductory view intothe characteristics of a search.

4.6.2. Proofs

Proof objects, that follow a natural deduction style, are available from the Solver interface [20]. You have to enable proof production at top level in order to retrieve proofs.

s.set("produce-proofs",True)s.add()assert unsat == s.check()print(s.proof())

The granularity of proof objects is on a best-effort basis. Proofs for the SMT Core, are relatively fined-grained, whileproofs for procedures that perform quantifier elimination, for instance QSAT described in Section 6.4, are exposed as big opaque steps.

4.6.3. Retrieving Solver State

You can retrieve the current set of assertions in a solver usings.assertions(), the set of unit literals usings.units() and literals that are non-units usings.non_units(). The solver state can be printed to SMT-LIB2 formatusings.sexpr().

4.6.4. Cloning Solver State and using Z3 from Multiple Threads

The methods.translate(ctx) clones the solver state into a new solver based on the contextthat is passed in. It is useful for creating separate non-interferring states of a solver.

All methods for creating sorts, expressions, solvers and similar objects take an optionalContext argument.By default, theContext is set to a default global container. Operations on objects created with the same context are not thread safe, but two parallel threads can operate safely on objects created by two different contexts.

4.6.5. Loading formulas

The methodss.from_file ands.from_string adds constraints to a solver statefrom a file or string. Files are by default assumed to be in the SMT2 format. If a file name ends withdimacs they are assumed to be in the DIMACS propositional format.

4.6.6. Consequences

Product configuration systems use constraints to describethe space of all legal configurations. As parametersget fixed, fewer and fewer configuration options are available.For instance, once the model of a car has been fixed, some optionsfor wheel sizes become unavailable. It is furthermore possiblethat only one option is available for some configurations, oncesome parameters are fixed. Z3 can be used to answer queries of the form:Given a configuration space of values, when fixing values, what is the largestsubset of values thatbecome fixed? Furthermore, for some value that is fixed,provide an explanation, in terms of the values that were fixed in, for why got fixed. The functionality is availablethrough theconsequences method.

a, b, c, d=Bools('a b c d')s=Solver()s.add(Implies(a, b),Implies(c, d))# background formulaprint(s.consequences([a, c],# assumptions                     [b, c, d]))# what is implied?

produces the result:

(sat, [Implies(c, c),Implies(a, b),Implies(c, d)])

In terms for SAT terminology, consequence finding produces the set of allbackbone literals. It is useful for finding fixed parameters [37] in product configuration settings.

Z3 relies on a procedure that integrates tightly with the CDCL,Conflict Driven Clause Learning [58], algorithm, and it contains two implementations of the procedure, one in the SAT core, anotherin the SMT core. Section 6.1.1 expands on CDCL and integrations with theories.

4.6.7. Cubes

You can ask Z3 to suggest a case split or a sequence of case splits through the cubing method.It can be used for partitioning the search space into sub-problems that can be solved in parallel, or alternatively simplify the problem for CDCL engines.

s=SolverFor("QF_FD")s.add()s.set("sat.restart.max",100)def cube_and_conquer(s):for cubein s.cube():if len(cube) ==0:return unknownif is_true(cube[0]):return sat            is_sat= s.check(cube):if is_sat == unknown:          s1= s.translate(s.ctx)          s1.add(cube)          is_sat= cube_and_conquer(s1)if is_sat != unsat:return is_satreturn unsat

When the underlying solver is based on the SAT Core, see Section 6.2, it usesa lookahead solver to select cubes [31]. By default, the cuber produces two branches,corresponding to a case split on a single literal. The SAT Core based cuber can be configuredto produce cubes that represent several branches. An empty cube indicates a failure, suchas the solver does not support cubing (only the SMT and SAT cores support cubing, and genericsolvers based on tactics do not), or a timeout or resource bound was encountered during cubing.A cube comprising of the Boolean constanttrue indicates that the state of the solver issatisfiable. Finally, it is possible for thes.cube() method to return an empty set of cubes.This happens when the state ofs is unsatisfiable.Each branch is represented as a conjunctionof literals. The cut-off for branches is configured using

• sat.lookahead.cube.cutoff

We summarize some of the configuration parameters that depend on the value ofcutoff in Table 3.

Heuristics used to control which literal is selected in cubes can be configured using the parameter:

• sat.lookahead.reward

5. Using Solvers

We now describe a collection of algorithms.They are developed on top of the interfaces described in the previous section.

5.1. Blocking evaluations

Models can be used to refine the state of a solver. For example, we may wish to invoke the solver in a loop where new calls to the solver blocks solutions that evaluate the constants to the exact same assignment.

def block_model(s):    m= s.model()    s.add(Or([ f() != m[f]for fin m.decls()if f.arity() ==0]))

It is naturally also possible to block models based on the evaluationof only a selected set of terms, and not all constants mentioned in themodel. The correspondingblock_model is then

def block_model(s, terms):    m= s.model()    s.add(Or([t != m.eval(t, model_completion=True)for tin terms]))

A loop that cycles through multiple solutions can then be formulated:

def all_smt(s, terms):while sat == s.check():print(s.model())       block_model(s, terms)

A limitation of this approach is that the solver state is innudatedwith new lemmas that accumulate over multiple calls. Z3 does not offerany built-in method for solution enumeration that would avoid this overhead, but you can approximate a space efficient solver using scopes:

def all_smt(s, initial_terms):def block_term(s, m, t):        s.add(t != m.eval(t, model_completion=True))def fix_term(s, m, t):        s.add(t == m.eval(t, model_completion=True))def all_smt_rec(terms):if sat == s.check():           m= s.model()yield mfor iin range(len(terms)):               s.push()               block_term(s, m, terms[i])for jin range(i):                   fix_term(s, m, terms[j])yieldfrom all_smt_rec(terms[i:])               s.pop()yieldfrom all_smt_rec(list(initial_terms))

Theall_smt method splits the search space into disjoint models. It does so by dividingit into portions according to thefirst term in a list of terms evaluatingdifferently in the next set of models.

5.2. All-SMT with user propagators

Theuser propagator plugin allows to track assignments to Boolean and Bit-vector expressions.In response, the solver can be constrained by callbacks that propagate consequences and blockunsatisfiable combinations of assignments.We illustrate the most basic functionality of the propagator for all-SAT enumeration.Every complete assignment to a set of tracked expressions is blocked, forcing a new combination of assignments.

classBlockTracked(UserPropagateBase):def __init__(self, s):UserPropagateBase.__init__(self, s)        self.trail= []        self.lim= []        self.add_fixed(lambda x, v: self._fixed(x, v))        self.add_final(lambda: self._final())def push(self):        self.lim += [len(self.trail)]def pop(self, n):        self.trail= self.trail[0:self.lim[len(self.lim) - n]]        self.lim= self.lim[0:len(self.lim)-n]def _fixed(self, x, v):        self.trail += [(x, v)]def _final(self):print(self.trail)        self.conflict([xfor x, vin self.trail])

To illustrate the functionality, we use an example with four Booleans, three of which are tracked.

s=SimpleSolver()b=BlockTracked(s)x, y, z, u=Bools('x y z u')b.add(x)b.add(y)b.add(z)s.add(Or(x,Not(y)),Or(z, u),Or(Not(z), x))print(s.check())

5.3. Maximizing Satisfying Assignments

Another use of models is to use them as a guide to a notion of optimal model.Amaximal satisfying solution, in shortmss, for a set of formulaspsis a subset ofps that is consistent with respect to the solver statesand cannot be extended to a bigger subset ofps without becoming inconsistentrelative tos. We provide a procedure, from [48], for finding a maximal satisfying subset in Figure 5.It extends a setmss greedily by adding as many satisfied predicates fromps in each round as possible. If it finds some predicatep that it cannot add, it notes that itis a backbone with respect to the currentmss. As a friendly hint, it includes the negation ofp when querying the solver in future rounds.

def tt(s, f):return is_true(s.model().eval(f))def get_mss(s, ps):if sat != s.check():return []    mss= { qfor qin psif tt(s, q) }return get_mss(s, mss, ps)def get_mss(s, mss, ps):    ps= ps - mss    backbones= set([])while len(ps) >0:       p= ps.pop()if sat == s.check(mss | backbones | { p }):          mss= mss | { p } | { qfor qin psif tt(s, q) }          ps= ps - msselse:          backbones= backbones | {Not(p) }return mss

5.4. All Cores and Correction Sets

The Marco procedure [45] combines models and cores in a processthat enumerates all unsatisfiable cores and all maximalsatisfying subsets of a set of formulasps withrespect to solvers. It maintains amap solverthat tells us which subsets ofps are not yetknown to be a superset of a core or a subset ofanmss.

def ff(s, p):return is_false(s.model().eval(p))def marco(s, ps):    map=Solver()    set_core_minimize(s)while map.check() == sat:        seed= {pfor pin psifnot ff(map, p)}if s.check(seed) == sat:           mss= get_mss(s, seed, ps)           map.add(Or(ps - mss))yield"MSS", msselse:           mus= s.unsat_core()           map.add(Not(And(mus)))yield"MUS", mus

Efficiently enumerating cores and correction sets is an active area of research.Many significant improvements have been developed over the above basic implementation [1–3,48,51,55].

5.5. Bounded Model Checking

Figure 7 illustrates a bounded model checking procedure [5] that takes a transition system as input and checks if a goal is reachable.Transition systems are described as

where is a predicate over, that describes the initial states, is a transition relation over.The set of reachable states is the set inductively defined as valuations of, such that either or there is a reachable and values for, such that. A goal is reachable if there is some reachablestate where.

In Python we provide the initial condition asinit, using variablesxs, the transitiontrans that uses variablesxs, xns, fvs, andgoal using variablesxs.Bounded model checking unfolds the transition relationtrans until it can establish thatthe goal is reachable. Bounded model checking diverges ifgoal is unreachable.The functionsubstitute(e, subst) takes an expressione and a list of pairssubst of the form[(x1, y1), (x2, y2),..] and replaces variablesx1, x2,.. byy1, y2,.. ine.

index=0def fresh(s):global index    index +=1returnConst("!f%d" % index, s)def zipp(xs, ys):return [pfor pin zip(xs, ys)]def bmc(init, trans, goal, fvs, xs, xns):    s=Solver()    s.add(init)    count=0whileTrue:print("iteration", count)        count +=1        p= fresh(BoolSort())        s.add(Implies(p, goal))if sat == s.check(p):print (s.model())return        s.add(trans)        ys= [fresh(x.sort())for xin xs]        nfvs= [fresh(x.sort())for xin fvs]        trans= substitute(trans,                            zipp(xns + xs + fvs, ys + xns + nfvs))        goal= substitute(goal, zipp(xs, xns))        xs, xns, fvs= xns, ys, nfvs

x0, x1=Consts('x0 x1',BitVecSort(4))bmc(x0 ==0, x1 == x0 +3, x0 ==10, [], [x0], [x1])

Bounded model checking is good for establishing reachability, but does notproduce certificates for non-reachability (or safety). The IC3 [10] algorithm is complete for both reachability and non-reachability. You can find a simplistic implementation of IC3 using the Python API online

5.6. Propositional Interpolation

It is possible to compute interpolants using models and cores [13].A procedure that computes an interpolant for formulas,, where is unsatisfiable proceeds by initializing and saturating a state with respect to the rules:

The partial interpolant produced by pogo satisfies. It terminates when.The condition ensures that the algorithm makes progress and suggests using an implicant of in each iteration. Such an implicant can be obtained from a model for.

def mk_lit(m, x):if is_true(m.eval(x)):return xelse:returnNot(x)def pogo(A,B, xs):while sat ==A.check():       m=A.model()L= [mk_lit(m, x)for xin xs]if unsat ==B.check(L):          notL=Not(And(B.unsat_core()))yield notLA.add(notL)else:print("expecting unsat")break

A=SolverFor("QF_FD")B=SolverFor("QF_FD")a1, a2, b1, b2, x1, x2=Bools('a1 a2 b1 b2 x1 x2')A.add(a1 == x1, a2 != a1, a2 != x2)B.add(b1 == x1, b2 != b1, b2 == x2)print(list(pogo(A,B, [x1, x2])))

5.7. Monadic Decomposition

Suppose we are given a formula using variables and.When is it possible to rewrite it as a Boolean combination of formulas and?We say that the formulas and aremonadic; theyonly depend on one variable. An application of monadic decompositionis to convertextended symbolic finite transducers intoregular symbolicfinite transducers. The regular versions are amenable to analysis and optimization.A procedure for monadic decompositionwas developed in [60], and we here recall the Python prototype.

from z3import *def nu_ab(R, x, y, a, b):    x_= [Const("x_%d" %i, x[i].sort())for iin range(len(x))]    y_= [Const("y_%d" %i, y[i].sort())for iin range(len(y))]returnOr(Exists(y_,R(x+y_) !=R(a+y_)),Exists(x_,R(x_+y) !=R(x_+b)))def isUnsat(fml):    s=Solver(); s.add(fml);return unsat == s.check()def lastSat(s, m, fmls):if len(fmls) ==0:return m    s.push(); s.add(fmls[0])if s.check() == sat: m= lastSat(s, s.model(), fmls[1:])           s.pop();return mdef mondec(R, variables):print(variables)    phi=R(variables);if len(variables)==1:return phi    l= int(len(variables)/2)    x, y= variables[0:l], variables[l:]def dec(nu, pi):if isUnsat(And(pi, phi)):returnBoolVal(False)if isUnsat(And(pi,Not(phi))):returnBoolVal(True)        fmls= [BoolVal(True), phi, pi]#try to extend nu        m= lastSat(nu,None, fmls)#nu must be consistentassert(m !=None)                                 a= [ m.evaluate(z,True)for zin x ]        b= [ m.evaluate(z,True)for zin y ]        psi_ab=And(R(a+y),R(x+b))        phi_a= mondec(lambda z:R(a+z), y)        phi_b= mondec(lambda z:R(z+b), x)        nu.push()#exclude: x~a and y~b        nu.add(nu_ab(R, x, y, a, b))                      t= dec(nu,And(pi, psi_ab))         f= dec(nu,And(pi,Not(psi_ab)))        nu.pop()returnIf(And(phi_a, phi_b), t, f)#nu is initially truereturn dec(Solver(),BoolVal(True))

def test_mondec(k):R=lambda v:And(v[1] >0, (v[1] & (v[1] -1)) ==0,                     (v[0] & (v[1] % ((1 << k) -1))) !=0)    bvs=BitVecSort(2*k)#use 2k-bit bitvectors    x, y=Consts('x y', bvs)    res= mondec(R, [x, y])assert(isUnsat(res !=R([x, y])))#check correctnessprint("mondec1(",R([x, y]),") =", res)test_mondec(2)

5.8. Subterm simplification

The simplification routine exposed by Z3 performs only rudimentary algebraic simplifications. It also does not use contextual information into account. In the followingexample we develop a custom simplifiersimplifythat uses the current context to find subterms that areequal to the term being considered. In the example below,the term is equal to.

H=Int('H')s=Solver()t=4 +4 * (((H -1) /2) /2)s.add(H %4 ==0)s.check()m= s.model()print(t,"-->", simplify(s, m, t))

To extract set of subterms it is useful to avoid traversingthe same term twice.

def subterms(t):    seen= {}def subterms_rec(t):if is_app(t):for chin t.children():if chin seen:continue                seen[ch]=Trueyield chyieldfrom subterms_rec(ch)return { sfor sin subterms_rec(t) }

We can then define the simplification routine:

def are_equal(s, t1, t2):    s.push()    s.add(t1 != t2)    r= s.check()    s.pop()return r == unsatdef simplify(slv, mdl, t):    subs= subterms(t)    values= { s: mdl.eval(s)for sin subs }    values[t]= mdl.eval(t)def simplify_rec(t):                subs= subterms(t)for sin subs:if s.sort().eq(t.sort())and values[s].eq(values[t])and are_equal(slv, s, t):return simplify_rec(s)        chs= [simplify_rec(ch)for chin t.children()]return t.decl()(chs)return simplify_rec(t)

6. Solver Implementations

There are five main solvers embedded in Z3.The SMT Solver is a general purpose solver that covers a wide range of supported theories.It is supplemented with specialized solvers for SAT formulas, polynomial arithmetic, Horn clauses and quantified formulas over theories that admit quantifier-elimination.

6.1. SMT Core

The SMT Solver is a general purpose solver that covers a wide range of supported theories. It is built around a CDCL(T) architecture where theorysolvers interact with a SAT+ EUF blackboard. Theory solvers, on the right in Figure 11, communicatewith a core that exchanges equalities between variables and assignmentsto atomic predicates. The core is responsible for case splitting, whichis handled by a CDCL SAT solver, and for letting each theory learn constraintsand equalities that are relevant in the current branch.

To force using the SMT solver a user can create asimple solver using the functionSimpleSolver.

The SMT solver integrates two strategies for quantifier instantiation.By default, both strategies are enabled. To disable them, one has todisable automatic configuration mode and then disable the instantiationstrategy:

s.set("smt.auto_config",False)# disable automatic SMT core# configurations.set("smt.mbqi",False)# disable model based# quantifier instantiations.set("smt.ematching",False)# disable ematching based# quantifier instantiation

6.1.1. CDCL(T): SAT+ Theories

The architecture of mainstream SMT solvers, including Z3's SMT core, usesa SAT solver to enumerate combinations of truth assignments to atoms.The truth assignments satisfy a propositional abstraction of the formula.Theory solvers are used to check if assignment admit a model modulothe theories. The resulting architecture is known as DPLL(T) [54], but we refer to this as CDCL(T) because it really relies on SAT solversthat incorporateConflict Driven Clause Learning [58], which goes beyond the algorithm associated with DPLL [19].Importantly, CDCL supplies facilities for learning new clauses during search.The learned clauses block future case splits from exploring the same failedbranches. Take the following example

s.add(x >=0, y == x +1,Or(y >2, y <1))

by introducing the names:

p1, p2, p3, p4=Bools('p1 p2 p3 p4')#              = x >= 0, y == x + 1, y > 2, y < 1

we obtain a propositional formula

And(p1, p2,Or(p3, p4))

It is satisfiable and a possible truth assignment is

p1, p2, p3, p4=True,True,False,True

It requires satisfiability of the following conjunction:

x >=0, y == x +1,Not(y >2), y <1

It is already the case that

x >=0, y == x +1, y <1

isunsat. To avoid this assignment we require also satisfying the blocking clause

Or(Not(p1),Not(p2),Not(p4))

The new truth assignment

p1, p2, p3, p4=True,True,True,False

produces

x >=0, y == x +1, y >2,Not(y <1)

which is satisfiable.The example illustrates the steps used in a CDCL(T)integration where the Theory Solver processes the final result of a SAT Solver. We can simulate this procedure using Z3's API.Figure 12 shows a CDCL(T) solverthat leverages a propositional solverprop to check a propositional abstraction and a theory solvertheory whose role is to check conjunctions of literalsproduced byprop. Figure 13 lists auxiliaryroutines required to create the abstraction.

def simple_cdclT(clauses):    prop=Solver()    theory=Solver()    abs= {}    prop.add(abstract_clauses(abs, clauses))    theory.add([p == abs[p]for pin abs])whileTrue:        is_sat= prop.check()if sat == is_sat:            m= prop.model()            lits= [mk_lit(m, abs[p])for pin abs]if unsat == theory.check(lits):                prop.add(Not(And(theory.unsat_core())))else:print(theory.model())returnelse:print(is_sat)return

index=0def abstract_atom(abs, atom):global indexif atomin abs:return abs[atom]    p=Bool("p%d" % index)    index +=1    abs[atom]= preturn pdef abstract_lit(abs, lit):if is_not(lit):returnNot(abstract_atom(abs, lit.arg(0)))return abstract_atom(abs, lit)def abstract_clause(abs, clause):returnOr([abstract_lit(abs, lit)for litin clause])def abstract_clauses(abs, clauses):return [abstract_clause(abs, clause)for clausein clauses]def mk_lit(m, p):if is_true(m.eval(p)):return pelse:returnNot(p)

We call it asimple CDCL(T) solver as it does notexpose important features to drive performance.Importantly, efficient CDCL(T) solvers integratetheory propagation that let theories interact withthe SAT solver to propagate assignments to atoms. Instead of adding blocking clauses by the time the SATsolver is done the theory solver interacts tightly withthe SAT solver during back-jumping.

6.1.2. Theories+ Theories

In practice we need to solve a combination of theories.The formulas we used in the initial example

  x +2 == y, f(Store(A, x,3)[y -2]) != f(y - x +1)

integrate several theory solvers. For modularity, it is desirable to maintainseparate solvers per theory. To achieve thisobjective the main questions that an integration needs to address are:

• Determine when the union of two theories is consistent.
• Given solvers for and, how can we build a solver for.

We can address this objective when thereis aneffective theory over the shared signature of, that when embedable into implies is consistent. Sufficient conditions for this setting were identified by Nelson and Oppen [52]:

Let us define the ingredients of this theorem.

Disjoint Theories

Two theories are disjoint if they do not share function/constant and predicate symbols. is the only exception. For example,

• The theories of arithmetic and arrays are disjoint.
  • Arithmetic symbols:0, -1,1, -2,2, +, -, *, >, <, ==, >=.
  • Array symbols:Select,Store

The process ofpurification can be used as a formal tool to bring formulas into signature-disjoint form. It introduces fresh symbols for shared sub-terms. A purified version of our running example is:

Functions:  f(v1) != f(v2)Arrays:     v1 == v3[v4], v3 ==Store(x, y, v5)Arithmetic: x +2 == y, v2 == y - x +1, v4 == y -2, v5 ==2

In reality, purification is a no-op: the fresh variables correspond directly to nodes in the abstract syntax trees for expressions.

Stably Infinite Theories

A theory is stably infinite if every satisfiable quantifier-free formula is satisfiable in an infinite model.

• EUF and arithmetic are stably infinite.

• Bit-vectors are not.

Nelson-Oppen combination.

Let and be consistent, stably infinite theoriesover disjoint (countable) signatures. Assume satisfiability of conjunction ofliterals can be decided in and time respectively.Then

1. The combined theory is consistent and stably infinite.

2. Satisfiability of quantifier free conjunction of literals can be decidedin.

3. If and areconvex, then so is and satisfiability in can be decidedin.

Convexity.

A theory isconvex if for every finite sets of literals, and every disjunction:

Many theories are convex and therefore admit efficient theory combinations

• Linear Real Arithmetic is convex.

• Horn equational theories are convex.

  • Horn equations are formulas of the form.

Finally note that every convex theory with non trivial models is stably infinite.

But, far from every theory is convex. Notably,

• Integer arithmetic

  • implies.

• Real non-linear arithmetic

  • implies.

• The theory of arrays

  • Store(a, i, v)[j] == v impliesi == j ora[j] == v.

A Reduction Approach to Theory Combination [21,43].

Theory Combination in Z3 is essentially by reduction to a set of core theories comprising of Arithmetic, EUF and SAT.Bit-vectors and finite domains translate to propositional SAT.Other theories arereduced to core theories. We provided an example of this reduction in Section 3.3.

6.1.3. E-matching based quantifier instantiation

E-matching [24] based quantifier instantiation uses ground terms to find candidate instantiations of quantifiers.Take the example

a, b, c, x=Ints('a b c x')f=Function('f',Z,Z)g=Function('g',Z,Z,Z)prove(Implies(And(ForAll(x, f(g(x, c)) == a), b == c, g(c, b) == c),              f(b) == a))

The smallest sub-term that properly containsx isg(x, c).Thispattern contains all the bound variables of the universal quantifier. Under the ground equalityb == c and instantiation ofx byc, it equalsg(c, b). This triggers an instantiationby the following tautology

Implies(ForAll(x, f(g(x, c)) == a), f(g(c, c)) == a))

Chasing the equalitiesf(g(c, c)) == a, g(c, b) == c, b == cwe derivef(b) == a, which proves the implication.

The example illustrated that E-matching takes as starting point apattern term, that captures the variables bound by a quantifier. It derives an substitution, such that equals someuseful term, modulo someuseful equalities.A useful source ofuseful terms are the current ground terms maintained during search,and the current asserted equalities during search may be used as theuseful equalities.Thecongruence closure structurecc introduced in Section 3.1.1 contains relevantinformation to track ground equalities. For each ground term it represents an equivalence class of terms that are congruent in the current context. Now, given a pattern we can compute a set of substitutions modulo the current congruence closure by invoking

where E-matching is defined by recursion on the pattern:

It is not always possible to capture all quantified variables in a single pattern.For this purpose E-matching is applied to a sequence of patterns, known as amulti-pattern,that collectively contains all bound variables.

The secret sauce to efficiency is to find instantiations

• with as little overhead as possible,
• across large sets of terms, and
• incrementally.

Z3 uses code-trees [56] to address scale bottlenecks for search involving thousands of patterns and terms.

6.1.4. Model-Based Quantifier Instantiation

E-matching provides a highly syntactic restriction on instantiations. An alternative to E-matching is based on using a current model of the quantifier-free part of the search state. It is used to evaluate the universal quantifiers that have to be satisfiedin order for the current model to extend to a full model of the conjunction of allasserted constraints. We call this methodModel-Based Quantifier Instantiation[9,25,29,61].Take the following example:

from z3import *Z=IntSort()f=Function('f',Z,Z)g=Function('g',Z,Z)a, n, x=Ints('a n x')solve(ForAll(x,Implies(And(0 <= x, x <= n), f(x + a) == g(x))),      a >10, f(a) >=2, g(3) <= -10)

It may produce a model of the form

[a=11, n=0, f= [else ->2], g= [3 -> -10,else -> f(Var(0) +11)]]

The interpretation ofg maps 3 to-10, and all other values are mappedto however is interpreted (which happens to be the constant 2).

The method that allowed finding this satisfying assignmentis based on a model evaluation loop. At a high level it canbe described as the following procedure, which checkssatisfiability of

where is quantifier free and for sake of illustration we havea single quantified formula with quantifier free body.The Model-Based Quantifier Instantiation, MBQI, procedure is described in Figure 14:

s.add()whileTrue:if unsat == s.check():return unsatM= s.model()   checker=Solver()   checker.add()if unsat == checker.check():return satM= checker.model()   find, such that.   s.add()

We use the notation to say that is partially evaluated using interpretation, for example:

• Let, and

• , then

For our example formula assume we have a model of the quantifier-free constraintsas follows

[a=11, n=0, f= [else ->2], g= [else -> -10]]

The negated body of the quantifier, instantiated to the model is

And(0 <= x, x <=0, [else ->2](x +11) != [else -> -10](x))

It is satisfied with the instantiationx = 0, which is congruent ton under the current model.We therefore instantiate the quantifier withx = n and add the constraint

Implies(And(0 <= n, n <= n), f(n + a) == g(n))

But notice a syntactic property of the quantifier body. It can be read as a definition for the graph ofg over the range0 <= x, x <= n.This format is an instance ofguarded definitions [35]. Hence, we record this reading when creating the next model forg. In the next round,a,n, andf are instantiated as before, andg(3) evaluates to-10 as before, but elsewhere follows the graph off(x + a), and thus the model forg is given by[3 -> -10,else -> f(11 +Var(0))].

Model-Based Quantifier Instantiation is quite powerful when search space for instantiation terms is finite. It covers many decidable logical fragments, including EPR (Effectively Propositional Reasoning), UFBV (uninterpreted functions and bit-vectors), the Array property fragment [11] and extensions [29]. We will here only give a taste with an example from UFBV [61]:

Char=BitVecSort(8)f=Function('f',Char,Char)f1=Function('f1',Char,Char)a, x=Consts('a x',Char)solve(UGE(a,0), f1 (a +1) ==0,ForAll(x,Or(x == a +1, f1(x) == f(x))))

The following model is a possible solution:

[a=0, f= [else ->1], f1= [1 ->0,else -> f(Var(0))]]

UFBV is the quantified logic of uninterpreted functions of bit-vectors.All sorts and variables have to be over bit-vectors, and standard bit-vector operations are allowed.It follows that the problem is finite domain and therefore decidable. It isn't easy, however. The quantifier-free fragment is not only NP hard, it is NEXPTIME hard; it can be encoded into EPR [57].The quantified fragment is another complexity jump.Related toUFBV, decision procedures for quantified bit-vector formulas were developed by John and Chakraborty in [38–40], and by Niemetz et alin [53].

Recall taht EPR is a fragment of first-order logic where formulas have the quantifierprefix, thus a block of existential quantified variablesfollowed by a block of universally quantified variables. The formula inside the quantifier prefixis a Boolean combination of equalities, disequalities between bound variables and free constantsas well as predicate symbols applied to bound variables or free constants. Noteworthy, EPR formulasdo not contain functions. It is easy to see that EPR is decidable by first replacing the existentially quantifiedvariables by fresh constants and then instantiate the universally quantified variables by all combinations of thefree constant. If the resulting ground formula is satisfiable, we obtain a finite model of the quantifiedformula by bounding the size of the universe by the free constants. The formula,where is a free constant, is in EPR.

6.2. SAT Core

The SAT Core is an optimized self-contained SAT solver that solves propositional formulas. It takes advantage of the fact that it operates over propositional theoriesand performs advanced in-processing steps.The SAT solver also acts as a blackboard for select Boolean predicatesthat express cardinality and arithmetical (pseudo-Boolean) constraints over literals.

Generally, theories that are finite domain, are solved using the SAT solver.Z3 identifies quantifier-free finite domain theories using a designated logicQF_FD.It supports propositional logic, bit-vector theories, pseudo-Boolean constraints, and enumeration data-types. For example, the following scenario introduces an enumerationtype for color, and bit-vectorsu,v. It requires that at least 2 out ofthree predicatesu + v <= 3, v <= 20, u <= 10 are satisfied.

from z3import *s=SolverFor("QF_FD")Color, (red, green, blue)=EnumSort('Color', ['red','green','blue'])clr=Const('clr',Color)u, v=BitVecs('u v',32)s.add(u >= v,If(v > u +1, clr != red, clr != green),      clr == green,AtLeast(u + v <=3, v <=20, u <=10,2))print(s.check())print(s.model())

is satisfiable, and a possible model is:

[v=4, u=2147483647, clr= green]