Abstract. We present an overview of Z3 internals to outline the main data-structures and algorithms used in Z3. The overarching aim is to help users gain more insight into formula encodings that have a better chance of being solved, what controls a user has over search behavior, and what information a user can extract from the solver. While we will try to address these questions by providing background on principles and examples of experiences, it is impossible to provide comprehensive answers. The hope is that shedding light into the internal workings of Z3 at a conceptual level offers a bridge towards developing an understanding of how to operate Z3 as well.
This document is written from the perspective of a developer of the SMT solver Z3. While it attempts to introduce an audience that includes many users to how to build an SMT solver, the main interest among users is more likely about how to best use an SMT solver. By introducing the internals of Z3 from the point of view of foundations, data-structures, algorithm design, and heuristics we introduce the reader to the development process. But, in this process, we also indirectly aim to address readers whose aim is to understand the how and why of using Z3. Many of the principles underlying the implementation of Z3 have been described in papers over several years and this document is not a substitute for these papers. We therefore often resort to references when material is covered elsewhere and instead attempt to reflect updated systems aspects.
Figure 1 shows a bird's eye view of the main components of Z3.
The main point of reference for Z3 is the GitHub repository
This document builds on top of and extends the material presented in [9] as part of a shorter tutorial.
You can use Z3 online from your browser. No installation is required
This guide complements the tutorial
Some of the internals are already described in depth in the Programming Z3 tutorial so they are covered in less detail here.
Z3 contains a collection of core engines for solving formulas. The engine used by default is based on the CDCL(T) architecture, but other engines are available and invoked for special classes of formulas where they are more suitable.
We here describe the solvers marked as SAT and SMT in Figure 1.
When SAT solving, as implemented using conflict driven clause learning, CDCL, is combined with theory solving
it augments propositional satisfiability with theory reasoning. The CDCL solver maintains a set of
formulas and a partial assignment to literals in that we refer to as .
The solver starts in a state , where is initially empty.
It then attempts to complete to a full model of to show that is satisfiable
and at the same time adds consequences
to to establish that is unsatisfiable. The transition between the search for a satisfying
solution and a consequence is handled by a conflict resolution phase.
The state during conflict resolution is a triple ,
where, besides the partial model and formula , there is also a conflict clause
false under .
The auxiliary function Theory is used to advance decisions, propagations and identify conflicts.
If Theory determines that is conflicting with respect to the literals in it produces a conflict clause , that
contains a subset of conflicting literals from . It can also produce a trail assignment , which is either a propagation
or decision and finally, if it determines that is satisfiable under trail it produces .
From the point of view of the CDCL(T) solver, theory reasoning is a module that can take a state during search and produce verdicts on how search should progress. We use the following verdicts of a theory invocation :
Thus, the verdict of Theory determines whether the partial model extends to a model of the theories, can identify a subset of as an unsatisfiable core, propagate the truth assignment of a literal , or create a new case split for a literal that has not already been assigned in . We write when the verdict is that extends to a valid theory model of , we write when is a conflict clause, based on negated literals from and , when the verdict is either a propagation or decision.
Example 1.
Consider the formula .
The initial state of search is
based on the empty partial assignment and the original formula. A possible next state is to propagate on the unit literal , producing
This step may be followed by a case split setting to false.
which triggers a unit-propagation
The resulting state is satisfiable in the theory of arithmetic. On the other hand, if we had chosen to set to true as well as , we would have encountered a conflicting state with conflict clause ^{1}:
The last decision is then reverted to produce the satisfiable state
A third scenario uses theory propagation. In this scenario, the decision is made, but instead of making a decision , the theory solver for arithmetic is given a chance to find opportunities for propagation. It deduces that together with implies , and therefore establishes the theory propagation
We are again eliding the unit literal from the explanation for . In practice, solvers automatically remove literals from conflict clauses that are necessarily false.
In the initial overview of the CDCL(T) loop, we left out other inference rules that are integral to efficient search.
Learn: Conflict clauses are added to the set of formulas . Conflict clauses are marked as redundant.
Restart: A suffix of the current partial model is abandoned.
In-processes: Clauses are inferred or marked redundant based on global inferences. This is usually done after a restart.
Garbage Collection: Redundant clauses are removed from .
To be well-behaved we expect Theory to produce propagations on literals that don't already appear in , and crucially enforce the main invariants:
That is, each conflict clause is a consequence of and each propagation is also a consequence of , and the premises of a propagation is justified by .
Z3 contains a dedicated engine for non-linear arithmetic over polynomials (Tarski's fragment [45]) [35]. The theory is decidable using cylindrical algebraic decomposition (CAD) [16]. The NLSAT engine implements the decision procedure for polynomial arithmetic. It uses a model constructing satisfiability engine (MC-SAT) to guide uses of CAD to a focused set of conflict clauses. Thus, the CAD algorithm is used on fragments of the entire formula for determining satisfiability, as opposed to globally on an entire formula.
The NLSAT engine is available as a one-shot engine for non-linear arithmetic formulas. It is also integrated with decision procedures in the CDCL(T) engine as an end-game solver.
Formulas that range over Constrained Horn Clauses (CHC) [7, 28] are solved using a dedicated engine, SPACER, [29] that builds on an engine inspired by IC3, [6, 30]. A Constrained Horn Clause is a formula of the form
where is a formula that is interpreted over a combination of theories, are uninterpreted predicates, and are terms over the bound variables and the theories from . The SPACER engine searches for a model for such that all clauses are true under the model.
The QSAT algorithm determines satisfiability of quantified formulas using theories that allow quantifier projection. There are two instances of QSAT, one for combinations of linear arithmetic, algebraic data-types, bit-vectors and arrays, the other is for non-linear polynomial arithmetic formulas over reals. They build on results developed in [3, 4, 42] and for solving NLSAT and Model-based projection introduced for SPACER. The algorithm is described in Programming Z3.
We will apply the following taxonomy when discussing the theory solvers. It extends the reduction approach to decision procedures [36] as explained in the context of Z3 in [18].
Bit-vectors are in the current solver treated as tuples of Boolean variables and all bit-vector operations are translated to Boolean SAT. The approach is called bit-blasting. Only mild equational reasoning is performed over bit-vectors. The benefits of the CDCL SAT engine have been mostly enjoyed for applications in symbolic execution of 32-bit arithmetic instructions. Bit-blasting has its limitations: applications that use quantifiers and applications around smart contracts that use 256 bits per word are stressing this approach. A revised bit-vector solver that integrates algebraic reasoning and lazy bit-blasting is therefore currently being developed.
Cardinality and Pseudo-Boolean inequalities can also be translated into CNF clauses. It is often an advantage when there are very few variables in the summations, but the overhead of translation can quickly become impractical. Z3 therefore contains dedicated solvers for cardinality and Pseudo-Boolean constraints.
Example 2.
Bit-blasting the arithmetic expression assuming both and consist of bits results in the formula
the result of the summation is given by . is the carry of adding the first bits of and . Pseudo-Boolean constraints like can be translated in multiple ways like translating it to bit-vector addition/multiplication as before, translating it to decision-diagrams or sorting-networks.
A decision diagram for this constraint looks like
which can be translated to a propositional formula. The sorting network approach sorts the bit-sequence to a sequence and asserts that has to be true.
The native solver instead tracks the partial sum of already assigned booleans and sets some of the remaining ones in case it is not possible to exceed the desired bound without them.
This theory captures a shared property of all theory: that equality is a congruence relation. The theory is described in many places, including in [8].
Let us use a simple example to illustrate the scope and main functionality of congruence closure based decision procedures for equality. We are given two equalities and one disequality
Their conjunction is unsatisfiable. Unsatisfiability is established by combining union-find [@UnionFind] data-structures to maintain equivalence classes and a data-structure of E-graphs to enforce congruences. In a first step, the terms are represented by unique nodes in a DAG structure for every sub-term. We represent the DAG structure as a sequence of definitions. Then equalities and disequalities are between nodes in DAG.
Process equality atoms using union-find. It establishes the equivalence classes
Then congruence closure triggers whenever there are two nodes, from different equivalence classes, labeled by the same function , with equal children. In our case belong to the same equivalence class so the nodes are merged.
When the children of the equality term are merged into the same equivalence class, the term is set to true. This contradicts that is already set to false.
The E-Node data-structure [22, 24, 39] is used to implement congruence closure efficiently. The main fields of an E-Node are
When a term occurs in a formula used by the solver it is compiled into an E-node . The E-node is initialized to
Example 3.
The result of internalizing the following term
is
The field is used to implement union-find. We use three fields to represent the union-find data-structure, comprising of:
Z3 performs eager path compression. It has the effect that the root node can always be accessed by a single pointer dereference. The singly-linked cyclic list of siblings of an equivalence class is used by operations that need to iterate over equivalence classes. Access to the equivalence class is used by E-matching and for propagation
Besides the E-nodes, the solver maintains a hash-table, we call etable, that is used to find the congruence root of a function application. It maps a function symbol and list of arguments to that are represented by root E-nodes into a congruence closure root. For the congruence closure root it maintains the invariant . We write to indicate that the etable tracks function applications to root nodes. In reality, the etable just stores the node and uses the function when computing the current hash of and equalities with other nodes.
The main functionality of congruence closure is to ensure that all equivalence classes that follow from equalities are inferred. It exposes the main function merge() to establish that two nodes are equal under justification . We describe justifications later in more detail. The main steps of merge are outlined below.
Roots | |
assume | |
assume | |
Erase | for each where : |
erase | |
Update Root | |
Justify | justify() |
Insert | for each : |
if then | |
etable | |
if then | |
append to | |
else | |
add to tomerge |
Roots: congruence closure always merges current roots of equivalence classes. If the roots are equal, there is nothing to merge. We assume that is chosen as root. The main mechanism for ensuring congruence closure has sub-quadratic running time is obtained by applying Hopcroft's method of merging the lesser half. Z3 makes an exception to this rule if is labeled by a term that qualifies as a value. To quickly identify if a congruence class contains a value, such as , it sets the root of a class to be the node representing the value.
Erase: Entries of the etable that are stale are removed. An entry is stale if it points to the old root as congruence closure representative.
Update Root: The root is updated along with size of equivalence classes and links into the cyclic list of siblings.
Justify: The justification for a merged equality is updated. We describe this functionality later.
Insert: Finally, the etable is updated by updating the field of parents from . It maintains a list tomerge of new nodes that are discovered congruent. An outer loop invokes merge on the list of new nodes until it is empty.
All operations on the E-Graph can be inverted. For this purpose, every merge is recorded in an undo trail. Other operations that update nodes are recorded in the same trail. For example, when is appended to the insertion into the cyclic list of parents is recorded so that it can be reverted. Reverting a merge requires updating the etable and is sensitive to whether a node was a congruence root:
The effect of unmerge() is as follows:
Erase | for each added from : |
erase | |
UnJustify | unjustify() |
Revert Root | |
Insert | for each : |
if | |
A justification is a reason for merging two nodes. There are two possible reasons for merging nodes:
NB: is justified recursively by justifying .
Invariant: Every non-root node points to a linked list of justifications leading to the root
NB The linked list does not follow direction of union-find.
Note that not all possible justifications are tracked, if merge() is invoked but already , then the justification for the equality of is dropped. In contrast, egg [26] keeps track of potential extra paths to find short proofs. Use cases within CDCL(T), that leverages amortized effect of backtracking search typically hedge on that the cost of finding a strongest conflict up front is outweighed by multiple attempts that converge on sufficiently strong conflicts.
We can create proofs from first-principles by using justifications. Suppose follows from a sequence merge(), merge(),, merge().
Then a proof of can be extracted using overloaded functions :
In the setting of CDCL(T), congruence closure is integrated with Boolean reasoning. For example, if is assigned true, , then the Boolean predicate can be propagated to true. Thus, congruence closure can be benefitial in propagation. On the other hand, propagations made by the CDCL(T) core need not be replicated by congruence closure: if the literal corresponding to is assigned to , then clausification of introduces clauses and , the ensure propagation to . Z3 therefore dampens the role of congruence closure for Boolean connectives that are handled by CDCL.
To track Boolean assignments the E-node data-structure includes the fields
Furthermore, equality is treated as a special function symbol. If the children of are merged, then the of is set to .
The E-graph also dispatches equality and disequality propagation between theories.
There are several alternate engines for arithmetical constraints in Z3. Some of the engines are engineered for fragments of arithmetic, such as difference arithmetic, where all inequalities are of the form , for a constant, and unit-two-variable-per-inequality (UTVPI), where all inequalities are of the form . A new main solver for general arithmetic formulas has emerged recently, with the longer term objective of entirely replacing Z3's legacy arithmetic solver. We will here describe internals of the newer solver in more detail.
In overview, the arithmetic solver uses a waterfall model for solving arithmetic constraints.
The solver for rational linear inequalities uses a dual simplex solver, as explained in [25]. It maintains a global set of equalities of the form , and each variable is assigned lower and upper bounds during search. The solver then checks for feasibility of the resulting system for dynamically changing bounds . The bounds are justified by assignments in .
Example 4.
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 definitions produce 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 values and 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 assignment is a model for the original formula.
Example 5.
From equalities infer that . Based on the tableau form, the solver is presented with the original equality atoms via slack variables
The tableau can be solved by setting . The slack variables are bounded when the equalities are asserted
The original solution is no longer valid, the values for are out of bounds. Pivoting re-establishes feasibility using a different solution, for example
with assignment . The variables and have the same value, but must they be equal under all assignments? We can establish this directly by subtracting the right-hand sides and from another and by factoring in the constant bounds to obtain the result . But subtraction is generally expensive if there are many bounded constants in the rows. The arithmetical operations are not required to infer that . Z3 uses two facts to infer the equality
Variables that satisfy these two criteria must be equal.
The mixed integer linear solver consists of several layers.
Each row is first normalized by multiplying it with the least common multiple of the denominators of each coefficient. For each row, it assembles a value from the fixed variables. A variable is fixed if the current values , are equal. Then it checks that the gcd of the coefficients to variables divide the fixed value. If they don't the row has no integer solution.
Example 6.
Assume we are given a row , where are fixed at , , and is the base variable.
Then it follows that which has no solution over the integers: The greatest common divisor of coefficients to the non-fixed variables () does not divide the constant offset from the fixed variables ().
Following [17], the integer solver moves non-basic variables away from their bounds in order to ensure that basic, integer, variables are assigned integer values. The process examines each non-basic variable and checks every row where it occurs to estimate a safe zone where its value can be changed without breaking any bounds. If the safe zone is sufficiently large to patch a basic integer variable, it performs an update. This heuristic is highly incomplete, but is able to locally patch several variables without resorting to more expensive analyses.
Example 7.
Suppose we are given a tableau of the form
where are basic variables and has bounds , has bounds , has bounds . The variable is initially assigned at the bound . Then and . But neither nor is close to their bounds. We can move to without violating the bound for because of . Thus, the freedom interval for is the range and within this range there is a solution, , where are integers and within their bounds.
An important factor in solving more satisfiable integer arithmetic instances is a method by Bromberger and Weidenbach [12, 13]. It allows detecting feasible inequalities over integer variables by solving a stronger linear system. In addition, we observed that the default strengthening proposed by Bromberger and Weidenbach can often be avoided: integer solutions can be guaranteed from weaker systems.
We will here recall the main method and our twist. In the following we let range over integer matrices and , , over integer vectors. The 1-norm of a matrix is a column vector, such that each entry is the sum of the absolute values of the elements in the corresponding row . We write to directly access the 1-norm of a row .
A (unit) cube is a polyhedron that is a Cartesian product of intervals of length one for each variable. Since each variable therefore contains an integer point, the interior of the polyhedron contains an integer point. The condition for a convex polyhedron to contain a cube can be recast as follows:
Example 8.
Suppose we have and wish to find an integer solution.
By solving we find
a model where . After rounding to and maintaining at we obtain an
integer solution to the original inequalities.
Our twist on Bromberger and Weidenbach's method is to avoid strengthening on selected inequalities. First, we note that difference inequalities of the form , where are integer variables and is an integer offset need not be strengthened. For octagon constraints , there is a boundary condition: they need only require strengthening if are assigned at mid-points between integral solutions. For example, if and , for . Our approach is described in detail in [5].
Similar to traditional MIP branch-and-bound methods, the solver creates somewhat eagerly case splits on bounds of integer variables if the dual simplex solver fails to assign them integer values. For example, Simplex may assign an integer variable , the value , in which case z3 creates a literal that triggers two branches and .
The arithmetic solver produces Gomory cuts from rows where the basic variables are non-integers after the non-basic variables have been pushed to the bounds. It also incorporates algorithms from [14, 23] to generate cuts after the linear systems have been transformed into Hermite matrices.
Similar to solving for integer feasibility, the arithmetic solver solves constraints over polynomials using a waterfall model for non-linear constraints. At the basis it maintains for every monomial term an equation , where is a variable that represents the monomial . The module for non-linear arithmetic then attempts to establish a valuation where , or derive a consequence that no such valuation exists. The stages in the waterfall model are summarized in the following paragraphs.
A relatively inexpensive step is to propagate and check bounds based on non-linear constraints. For example, for , then , if furthermore , we have the strengthened bound . Bounds propagation can also flow from bounds on to bounds on the variables that make up the monomial, such that when , then we learn the stronger bound on .
If , then and therefore , but we would not be able to deduce this fact if combining bounds individually for and because no bounds can be inferred for in isolation. The solver therefore attempts different re-distribution of multiplication in an effort to find stronger bounds.
Many constraints using polynomials can be checked for consistency by normalization. The Gröbner basis reduction algorithms provide a means to check consistency of a set of polynomial equations (which is complete if adding the Nullstellensatz checks). Z3 uses a best effort Gröbner basis reduction to find inconsistencies, cheaply, and propagate consequences. It first extracts equalities from Simplex rows where the basic variable is bounded. It adds equations for arithmetic variables that are defined as monomials.
Equations are pre-solved if they are linear and can be split into two groups, one containing a single variable that has a lower (upper) bound, the other with more than two variables with upper (lower) bounds. This avoids losing bounds information during completion.
After (partial) completion, perform constant propagation for equalities of the form . The equality is propagated to the linear solver.
After (partial) completion, perform factorization for factors of the form where are variables an is linear. We infer the clause .
We use an adaptation of ZDD (Zero suppressed decision diagrams [38, 40]) to represent polynomials. The representation has the advantage that polynomials are stored in a shared data-structure and operations over polynomials are memorized. A polynomial over the real is represented as an acyclic graph, where nodes are labeled by variables and edges are labeled by coefficients. For example, the polynomial is represented by the acyclic graph shown below.
The root node labeled by represents the polynomial , where is the polynomial of the left sub-graph and the polynomial of the right sub-graph. The left sub-graph is allowed to be labeled again by , but the right sub-graph may only have nodes labeled by variables that are smaller in a fixed ordering. The fixed ordering used in this example sets above . Then the polynomial for the right sub-graph is , and the polynomial with the left sub-graph is .
The Gröbner module performs a set of partial completion steps, preferring to eliminate variables that can be isolated, and expanding a bounded number of super-position steps (reductions by S-polynomials).
Following [15] we incrementally linearize monomial constraints. For example, we include lemmas of the form and , for .
As an end-game attempt, the solver attempts to solver the non-linear constraints using a complete solver for Tarski's fragment supported by the NLSat solver [35].
Z3 uses infinite precision integers and rationals. This ensures that all operations are sound and not subject to errors introduced by rounding. It uses a sparse matrix representation for the Dual Simplex tableau. Note that pivoting may turn an otherwise sparse matrix into a dense form. We also created a version that uses an LRU decomposition and floating point numbers but found that extending this version with efficient backtracking was not practical compared to the straight-forward sparse matrix format.
The arithmetic solver reduces operations such as integer modulus, remainder, and division into equations. It eagerly compiles bounds axioms of the form for atomic formulas .
Let us illustrate a use of reduction from richer theories to base theories based on a simple example based on refinement types. It encodes refinement types using auxiliary functions, as explained in [31]. Refinement types are not part of Z3, so the decision procedure we outline here is not available out of the box. One way to realize this theory is externally through the User-Propagator facility.
Abstractly, a refinement type of sort uses a predicate over . At least one element of must satisfy for the construction to make sense. The refinement type represents the elements of that satisfy . The properties we need to know about elements of can be encoded using two auxiliary functions that form a surjection from into with a partial inverse that maps elements from into . The properties of these functions are summarized as follows:
Let us illustrate the sort of natural numbers as a refinement type of integers:
Example 9.
We obtain a theory solver for formulas with refinement types by instantiating these axioms whenever there is a term introduced of sort introduced as part of the input or during search (from instantiating quantifiers). The main challenge with supporting this theory is to ensure that the new terms introduced from axiom instantiation are bounded. We don't want the solver to create terms .
For every sub-term of the form , where is not instantiate the axiom:
For every term of sort instantiate the axioms:
The theory of arrays in SMTLIB is formally based on two functions select
and store
and an axiomatization
for every array , index and value . Alluding to the intent that the theory of arrays is useful for modeling arrays in programming languages will henceforth use when we mean .
Z3 reduces the theory of arrays to reasoning about uninterpreted functions. It furthermore treats arrays as function spaces, which assuming more axioms about arrays. The first-order theory of arrays axiomatized above enjoys compactness and so the following formula is satisfiable^{2}
The same formula is not satisfiable when arrays range over function spaces. The distinction is only relevant when checking satisfiability of quantified formulas over arrays. In addition to functions and Z3 includes built-in functions , and the operator and lambdas. It includes also the function that provides a witness term for distinct arrays, and for accessing a default value.
The central functionality of the decision procedure for arrays is to ensure that a satisfying model under the theory of EUF translates to a satisfying model in the theory of arrays. To this end, the main service of the theory solver is to saturate the search state with reduction axioms for array terms that admit beta-reduction. We call these terms terms and they are defined by the beta-reduction axioms:
The reduction into EUF, is then, in a nutshell, an application of the following inference rule:
together with an inference rule to enforce extensionality
The decision procedure enforces several throttles [18] to avoid instantiating axioms when they are redundant. We here describe the main data-structures used by the instantiation engine.
The decision procedure maintains for every array node the following sets
When is merged with , and is the new root, the sets from are added to . The merge also looks for new redexes when and are merged:
For enforcing , the solver only instantiates the axiom because the axiom is instantiated eagerly when the term is created.
Extensionality is enforced on pairs of array terms , that are in shared positions. An array term is in a shared position when it occurs on one side of an equality or under a function that is not part of the theory of arrays. Furthermore, to ensure congruence for lambdas, if is a lambda term in a shared position and is in a shared position, the axiom is instantiated. Thus, lambda equality is at the time of writing enforced by a reduction to quantified formulas.
The theory of algebraic data-types is an SMTLIB2 standard [2]. The theory
allows declaring a datatype
sort, or a set of mutually recursive datatypes
sorts.
The elements of an algebraic datatype are the least set generated by the constructors in the type declaration.
You can declare algebraic data-types in SMTLIB2 using the declare-datatypes
command
(declare-datatypes ((Tree 1) (TreeList 1))
(
(par (T) (Tree leaf (node (value T) (children (TreeList T)))))
(par (T) (TreeList nil (cons (car (Tree T)) (cdr (TreeList T)))))
)
)
A legacy format that is less flexible, but a bit easier to formulate, is also available.
(declare-datatypes (T) ((Tree leaf (node (value T) (children TreeList)))
(TreeList nil (cons (car Tree) (cdr TreeList)))))
Z3 supports datatypes nested with sequences and arrays. The example below uses `Stmt' nested in a sequence.
(declare-sort Expr)
(declare-sort Var)
(declare-datatypes ((Stmt 0))
(((Assignment (lval Var) (rval Expr))
(If (cond Expr) (th Stmt) (el Stmt))
(Seq (stmts (Seq Stmt))))))
For arrays, datatypes are allowed only in the range of arrays.
Provide example with nested arrays
We will in the following use the notation for a constructor, for example Assignment
is a constructor;
for accessors corresponding to , for example lval
and rval
are accessors
corresponding to the constructor Assignment
. The predicate symbol is true if the term
is equal to a term headed by the constructor . The construct
assigns the term to an accessor field for the term . Note that it is possible to apply an
accessor to a data-type constructor that does not match. For example, taking the head of an empty list,
. The interpretation of is not fixed by the
theory, instead is treated as an uninterpreted function.
The theory solver for algebraic datatypes is implemented by adding theory axioms on demand. The theory axioms rely on the theory of uninterpreted functions. It builds a finite interpretation for every node of sort data-type and adds theory axioms on demand. Every E-node of data-type sort is assigned a constructor representation, initially null. If is equated to a node whose function is labeled by a constructor , the representative for is labeled by .
The saturation rules add theory axioms on demand to enforce that the theory of algebraic datatypes axioms are satisfied in a consistent state. Accessor axioms, update-field axioms are added as soon as terms are created. Recognizer axioms are added when the truth value of a recognizer is asserted. If a datatype has a single constructor, the recognizer is asserted as a unit. The occurs check is applied lazily. It ensures that the partially constructed model corresponds to acyclic algebraic datatypes.
If is a constructor node assert the axioms
If is of the form , where is an accessor for constructor , then assert the axioms
For recognizer atom we have to ensure that a node is assigned to a constructor that is consistent with the assignment to the recognizer atom. Thus, if is asserted to true, then must be equated to a term with constructor . Conversely, if is assigned with a constructor , then is false. The decision procedure ensures this correspondence lazily. If is asserted to true, then it ensures the axiom
where are the accessors for .
If is asserted to false, but equal to a node that is headed by , then it creates the conflict clause:
Something about covering constructors so all possible constructors are tested.
An occurs check violation is detected when there is a state satisfying the properties where each is of the form . Occurs checks are performed lazily in a final check.
Dually to saturation rules, the theory solver builds a finite model for algebraic datatypes. Model construction is interleaved with the CDCL(T) engine in a way that has subtle consequences. Model construction drives the constraints to a goal state where all terms ranging over an algebraic datatype have been assigned a constructor and all saturation rules have been applied. If there is a term that has not been assigned a constructor, the solver attempts to first guess an assignment to the term based on a non-recursive base case for the data-type (for mutually recursive data-types some types don't have non-recursive base cases, it is possible to drive towards a nested sub-term that has). The fact that the solver can guess a fixed base case constructor during model construction relies on the assumptions for theory combinations: other theories need only distinguish whether data-type terms are equal or distinct. The shape of terms is opaque to other theories. If a term cannot be assigned a non-recursive base case (say nil), it is assigned a non-recursive constructor (say, cons), that eventually allows assigning to a term that is arbitrarily deep and therefore can be distinct from any set of other terms .
The approach for model construction does not work if we introduce a sub-term predicate . The theory of algebraic data-types can be extended to the subterm relation while remaining decidable. If range over an algebraic data-type with two base case constructors and , and . Then unfairly guessing only before guessing cons, but neglecting leads to non-termination of a model constructing decision procedure with the sub-term relation.
The theory of algebraic data-types admits partial quantifier elimination.
Present MBP for ADT here specifically?
A prime example of a hybrid theory in Z3 is the theory of strings, regular expressions and sequences.
The theory of strings and regular expressions has entered mainstream SMT solving thanks to community efforts around standardization and solvers. The SMTLIB2 format for unicode strings [2]. It integrates operations that mix equational solving over the free monoid with integer arithmetic (for string lengths and extracting sub-strings). Regular expression constraints furthermore effectively introduce constraints that require unfolding recursive relations. Z3 uses symbolic derivatives [44] to handle regular expressions, noteworthy, with complementation and intersection handled by derivatives.
A second prolific example of a hybrid theory is Z3's model-based quantifier instantiation engine (MBQI). Here, a theory is encoded using a quantifier. The MBQI engine supports extensions of Bradley-Manna-Sipma's array property fragment [11] that effectively combines arithmetic with uninterpreted functions.
Floating point semantics can mainly be defined in terms of bit-vector operations. The solver for floating points uses this connection to reduce the theory of floating points to bit-vectors. There are also operations on floating points that connect with the theory of Reals. For formulas combining floating points and reals, the theory solver bridges bit-vector values with bounds over the Reals.
This section pops the abstraction level and examines the main data-structures, organization, algorithms and heuristics that are central to implementation of Z3. We examine the data-structures used for terms and formulas and then describe the setting for how theory solvers interact with the main CDCL(T) engine.
Z3 treats terms and formulas as a single entity, expressions. Expressions of Boolean type can be used as formulas, but they can also be nested within non-Boolean terms, as arguments to functions. Expressions are hash-consed, meaning they are unique up to term structure. It uses a hash-table when constructing a fresh term, such that if the same function is applied to the same arguments as a previously constructed term, the result of creating the term is the same pointer as the old term.
Variables that are to be bound by quantifiers are indexed using de-Brujin conventions, such that the index used for the innermost quantified variable is 0, and incremented outwards. For example, uses de-Bruijn indices 0 for and 1 for , and 2 for . To spare users an error-prone process of keeping track of indices, the external API offers a facility to create a quantified expression using a set of constant expressions instead of variables.
A representation of Z3 terms using the Koka language is as follows
type Expr
Var{ index : int; sort : Sort }
App{ f : FuncDecl; args : list<Expr> }
Quantifier{ b : Binder; decl : list<Declaration>; body : Expr; ...}
From input and during pre-processing assertions are represented in a structure of the form
For a standard input assertion the structure is initialized as . The proof of is that it was asserted. There are no dependencies for .
Input assertions can also be tracked for unsatisfiable cores.
The SMTLIB2 contains syntax for adding named formulas. The formulas are tracked by their names
and the solver can produce unsatisfiable cores over the tracking names.
Internally, the names are treated as (fresh) Boolean literals. Thus, formulas can also be
tracked by arbitrary formulas. The programmatic API contains a function Z3_solver_assert_and_track
(and variants surfaced in various programming languages) that allows asserting a formula modulo
a tracking assumption. When adding tracked formulas using tracking assumption , the
structure is initialized as .
Tactics (8) perform updates on the triple representation by applying inferences. Properly producing proof objects for tactics and tracking dependencies is supported in a best-effort manner: several tactics are disabled when the user requires proof objects or tracking dependencies. Dependencies can be viewed as light-weight proof objects. The mechanism for tracking dependencies is based on tracking a cone of influence, by taking unions, of formulas used to derive a new consequence.
While the input to Z3 is a set of formulas, the core solver works with clauses and E-nodes. The internalization process converts formulas into the internal data-structures bottom-up. Every sub-term that corresponds to a Boolean connective is compiled, thanks to the Tseitin transformation, into a fresh literal with associated set of clauses that define the literal. The terms from Boolean connectives may be assigned E-nodes, but the nodes do not participate in congruence rules, nor are, by default, allowed to be merged with the constants or : The CDCL(T) engine already enforces congruence rules and consistency with assignments to . The default is overridden if a term occurs as an argument to a non-Boolean connective. For example, in the term , the node merges with when the truth value to the literal is propagated. In this way, congruence closure can ensure consistency with respect to occurrences of .
Compilation of terms into E-nodes uses a top-down traversal of terms. The top-down traversal is replicated in each theory solver, where the compilation of terms depends on the solver. The arithmetic solver, for instance, compiles the term into a node and adds the basic row . Top-down compilation does not play well with small static stack sizes allocated by runtimes. The new core in Z3 therefore introduces a visitor pattern to allow top-down processing without using recursion stacks.
E-nodes are compiled dynamically during search. When a quantifier is instantiated or a solver introduces a new lemma that uses new terms, the E-nodes corresponding to new terms are introduced at a search level that may later be popped. Learned clauses may refer to these new terms in a scope where they are no longer internalized into E-nodes. The core solver therefore interacts with the scope mechanism of the CDCL solver to replay literals that are defined in deeper scopes.
In Z3, the solver for the theory of equality acts as a gate-keeper between the SAT solver and solvers for other theories. As Section 2.1 outlines, the SAT solver maintains a set of ground clauses and performs case splits and propagations and in this process consults the theory solver for the next propagation, case split or whether is a theory consistent model of .
There is a good reason why the theory of equality is central: this theory is shared among all other theories. Disjoint theory solvers establish satisfiability by reconciling equalities among shared sub-terms.
Every E-node has an attached set of theory solvers. A theory solver for a theory gets attached to a node when
Then, when a Boolean node is assigned to or by the CDCL solver, the truth assignment to is broadcast to all solvers attached to . Similarly, when two nodes are merged, and the theory is attached to a sibling of and a sibling of , then the equality is broadcast to .
In some cases, the core also broadcasts disequalities between E-nodes. Solvers cannot rely on complete propagation of disequalities, it is generally too costly to enumerate all pairwise disequalities. Propagation of disequalities is triggered by when the CDCL(T) core asserts a disequality , or when a theory solver propagates a disequality.
The set of terms tracked by a given theory is always a subset of all terms used in a formula. Particularly, if a formula encodes bit-vector properties, there are thousands of terms used for encoding Boolean formulas. Those terms are irrelevant to the theories. Each theory therefore maintains a dense encoding of the terms it tracks by maintaining an array of E-nodes associated with the theory. The index into this array is the identifier of the theory variable. This identifier is stored in the E-node data-structure so that when the core broadcasts an equality about it accesses the theory variables and that are indices to the array and broadcast . The original nodes are accessed from the theory solver's array, together with other attributes of