Abstract. Modular combination of theory solvers is an integral theme in engineering modern SMT solvers. The CDCL(T) architecture provides an overall setting for how theory solvers may cooperate around a SAT solver based on conflict driven clause learning. The Nelson-Oppen framework provides the interface contracts between theory solvers for disjoint signatures. This paper provides an update on theories integrated in Z3. We briefly review principles of theory integration in CDCL(T) and then examine the theory solvers available in Z3, with special emphasis on two recent solvers: a new solver for arithmetic and a pluggable user solver that allows callbacks to invoke propagations and detect conflicts.
The aim of this paper is to provide an up-to-date overview of Z3's core solver engines. While some of the engines date back quite some time, other engines have been replaced over time, added, and even some have been removed; and then re-added in different guise. A recent addition has been a theory solver for arithmetic developed from the ground up. We give an overview of the main features of this new engine and explain selected new approaches used in the solver. A recent addition includes a mechanism for pluggable propagation. We also provide an introduction to this engine.
We will apply the following taxonomy when discussing the theory solvers. It extends the reduction approach to decision procedures [17] as explained in the context of Z3 in [12].
Z3 now has two CDCL(T) solvers. For main SMT workloads it offers a CDCL(T) core that integrates all the theories that we mention here. This core is a continuation of the main solver of Z3 since its inception. A core with near up-to-date advances in SAT solving has been used so far for workloads originating from bit-vector and Pseudo-Boolean constraints. This core is currently being updated to handle most if not all the SMT workloads of the legacy core with the intent of modernizing Z3's core and allowing integration of new techniques around in-processing, logging of clausal proofs, model repair, and other goodies. From the perspective of this paper, we do not distinguish these cores. Z3 exposes several other core solvers that either build on top of the SMT solver or entirely bypass it. For Horn clauses, Z3 contains dedicated engines for finite domain Horn clauses using finite hash-tables, and for Constrained Horn Clauses (CHC) it uses the SPACER [18] solver; for quantifier-free formulas over Tarski's fragment of polynomial arithmetic it exposes a self-contained solver; and for quantified formulas for theories that admit quantifier-elimination it exposes self-contained solvers.
In this section, we recall the main mechanisms used in mainstream modern SAT solvers in the light of theory solving.
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 determes 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 .
which triggers a propagation
The resulting state is satisfiable in the theory of arithmetic. On the other hand, if we had made the case split on instead of , and then guess the assignment , 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 implies , and therefore establishes the theory propagation
We are again eliding the unit literal from the explanation for .
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 .
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.
A first base theory is the theory of uninterpreted functions. This theory captures a shared property of all theory: that equality is a congruence relation. The theory is described many places, including in [5].
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 [14]. 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 .
The new arithmetic solver contains a novel, efficient, method for finding pairs of variables that are forced equal. By finding such variable, the arithmetic solver can then propagate equalities to other theories. Such equality propagation can make a big difference for efficiently integrating arithmetic in hybrid theories, such as the theory of sequences. We will in the following outline the new idea.
A starting point is a tableau with bounds . The tableau contains a sub-tableau of equalities where at most two variables are non-fixed in every equation, such that the coefficients of the non-fixed variables have the same absolute value. That is, let be a system of linear equations of the form , where are variables and is a constant, and for . It is relatively cheap to detect whether a row in a tableau corresponds to such an equation: it can have at most two non-fixed variables whose coefficients must have the same absolute values. We assume that the variable values and the constants are rational numbers. For bounds propagation it is only relevant to consider feasible tableaux. So has a solution , so we have for every . Let us call variables and equivalent if in every solution of they have the same values.
Given and , we provide an efficient algorithm for finding pairs of variables such that is equivalent to .
Let us start from an example. Consider the following system
and solution
By examining , we might suspect that the , and are pairwise equivalent. However, if we increase by one we have another solution
Since , we can conclude that is not equivalent to either or . But we can prove that and are equivalent. Another observation is that each variable changed its value by : changing as or as .
We introduce our algorithm by recalling which inference rules it simulates, without actually literally performing the inferences. The inferences are
The goal of deriving implied equalities is achieved if we can infer an equality using the above inference rules. Now, the crucial observation is that there is no need to perform arithmetic on the constant offsets because we have a valuation and the property for every derived equation :
So it is enough to look at the variables and check if their values are the same for a derived equality. The benefit of avoiding arithmetic on the coefficients can be significant when the coefficients cannot be represented using ordinary 64-bit registers, but require arbitrary precision arithmetic. Note that the same method also detects fixed variables; whenever deriving , we have proved to be fixed at value . In this case, the method needs to calculate . All other variables connected to through binary equalities are naturally also fixed.
To implement search over the derivation rules efficiently, we build a depth-first search forest where the nodes are annotated by variables annotated by signs and their values from . Edges are annotated by octagon equations. The forest is built by picking a so-far unprocessed variable and growing a tree under it by traversing all equations involving the variable. During the tree expansion the algorithm checks if two nodes with the same value and same signs are connected. To propagate a new equality we trace back the path that was used to derive the equality and assemble the justifications from each row.
Example 2.
Let us show how the procedure works on the example from above and valuation .
Starting with the node , the equation
produces the children and .
The second child can be expanded in turn into
, , .
This establishes a path from to .
The two nodes are labeled by the same values and same signs.
The mixed integer linear solver comprises of several layers. It contains several substantial improvements over Z3's original arithmetic solver and currently outperforms the legacy solver on the main SMTLIB benchmark sets, and to our knowledge mostly on user scenarios.
Each row is first normalized by multiplying it with the 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.
Following [11], 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.
One of the deciding factors in leapfrogging the previous solver relied on a method by Bromberger and Weidenbach [7, 8]. It allows to detect 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 3.
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 [4].
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.
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 [9, 13] 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 as follows:
A relatively inexpensive step is to propagate and check bounds based on 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.
We use an adaptation of ZDD (Zero suppressed decision diagrams [19, 20]) to represent polynomials. The representation has the advantage that polynomials are stored in a shared data-structure and operations over polynomials are memoized. 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.
Following [10] 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 [16].
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 [15]. 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 4.
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 is 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:
Z3 reduces the theory of arrays to reasoning about uninterpreted functions. It furthermore treats arrays as function spaces. The first-order theory of arrays enjoys compactness and so the following formula is satisfiable2
The same formula is not satisfiable when arrays range over function spaces. The distinction is only relevant for formulas that contain quantifiers over arrays.
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:
Floating point semantics can 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.
The theory of algebraic datatypes is compiled into uninterpreted functions. In this theory, constructors are injective functions. Injectivity is ensured by adding axioms for partial inverses. For the example of LISP S-expressions these axioms are:
The main functionality provided by the theory solver that cannot be reduced to EUF is the occurs check.
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 [1]. 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 [21] 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 [6] that effectively combines arithmetic with uninterpreted functions.
The universe of theories is in principle unbounded. Many theories can be captured using a set of quantified axioms and therefore be handled by machinery for quantifiers. But encodings have their own limitations, noteworthy it might not be possible to encode a theory using a small number of axioms. Users can of course encode theory solvers directly themselves within Z3's core. This has been accomplished in the case of Z3Str3 [2], but it is a significant engineering effort and ties a theory to a fixed signature. A more flexible approach was exposed around 2010 in the format of user theories. A user theory plugin could be encoded outside of Z3 and it integrated with the main CDCL(T) engine. Some examples of the user theory were presented in [3]. The user theories were subsequently removed from Z3 as it was not possible to properly integrate them in model construction. Recent experiences with solving constraint satisfaction problems suggested that a restricted version of user theories would be instrumental. A variant of user theories have therefore been resurrected under the banner of a user propagator to capture its main functionality: it allows client code participate in propagation and creating conflicts in response to variable assignments.
We will illustrate the user propagator by a simple example. The example illustrates as a Pseudo-Boolean constraint that when encoded directly would be quadratic in the number of variables. The user propagator, though, does not require quadratic space overhead. We encode the constraint that
and every subset that contributes to the sum and contains at least half of the variables must add up to at least 10. We first define the variables used in the problem:
from z3 import *
xs = BitVecs(["x%d" % i for i in range(8)], 10)Then a user-propagator can be initialized by sub-classing to the UserPropagateBase
class that implements the main interface to Z3's user propagation functionality.
class UserPropagate(UserPropagateBase):
def __init__(self, s):
super(self.__class__, self).__init__(s)
self.add_fixed(self.myfix)
self.add_final(self.myfinal)
self.xvalues = {}
self.id2x = {self.add(x) : x for x in xs}
self.x2id = { self.id2x[id] : id for id in self.id2x }
self.trail = []
self.lim = []
self.sum = 0The map xvalues tracks the values of assigned variables
and id2x and x2id maps tracks the identifiers that Z3 uses for variables with the original variables.
The sum maintains the running sum of according to our unusual constraint.
The class must implement methods for pushing and popping backtrackable scopes.
We use a trail to record closures that are invoked to restore the previous state
and lim to maintain the the size of the trail for the current scope.
# overrides a base class method
def push(self):
self.lim.append(len(self.trail))
# overrides a base class method
def pop(self, num_scopes):
lim_sz = len(self.lim)-num_scopes
trail_sz = self.lim[lim_sz]
while len(self.trail) > trail_sz:
fn = self.trail.pop()
fn()
self.lim = self.lim[0:lim_sz]We can then define the main callback used when a variable tracked by identifier id is fixed to a value e.
The identifier is returned by the solver when calling the function self.add(x) on term x. It uses
this identifier to communicate the state of the term x. When terms range over bit-vectors and Booleans
(but not integers or other types), the a client can register a callback with self.add_fixed to pick up
a state where the variable is given a full assignment.
For our example, the value is going to be a bit-vector constant, from which we can extract an unsigned integer into v.
The trail is augmented with a restore point to the old state and the summation is then updated
and the Pseudo-Boolean inequalities are then enforced.
def myfix(self, id, e):
x = self.id2x[id]
v = e.as_long()
old_sum = self.sum
self.trail.append(lambda : self.undo(old_sum, x))
for w in self.xvalues.values():
if v + w == 42:
if v > 30 or w > 30:
self.sum += 3
else:
self.sum += 1
self.xvalues[x] = v
if self.sum > 100:
self.conflict([self.x2id[x] for x in self.xvalues])
elif self.sum < 10 and len(self.xvalues) > len(xs)/2:
self.conflict([self.x2id[x] for x in self.xvalues])It remains to define the last auxiliary methods for backtracking and testing.
def undo(self, s, x):
self.sum = s
del self.xvalues[x]
def myfinal(self):
print(self.xvalues)
s = SimpleSolver()
for x in xs:
s.add(x % 2 == 1)
p = UserPropagate(s)
s.check()
print(s.model()) In this example, it takes relatively few conflicts to establish a satisfying assignment, one where 9 out of 10 variables are set to 1 and the last variable is set to 41. The solver is only as good as the propagation strength and the quality of the conflicts it can generate. For instance, if we change the condition to the constraints are not solved with the same ease.
The user propagator also allows to register callbacks when two added terms are known to be equal to the solver, and when two variables are known to be distinct. Note again that the use-case for the user propagator is for Bit-vector and Boolean variables.
We provided an overview of solver integration in Z3 with special emphasis on a newly revised arithmetic solver and a user propagator. While most applications use a small combination of mainstream theories, there is plenty of room for expanding theory solvers both in depth, in terms of capabilities and efficiency; and expand the repertoire of solvers to new theories. While applications have been enabled by current SMT solvers, they also introduce new challenges by highlighting bottlenecks and shortcomings. Current efforts center around modernizing Z3's entire core engine around up-to-date SAT solving techniques. Among many potential advantages it would allow Z3 to apply in-processing simplifications for quantifiers and SMT theories, and for instance, handle large bit-vectors by integrating algebraic methods, incremental bit-blasting, local search and leverage other recent advances in bit-vector reasoning. The universe (of solvers) is still expanding.