Abstract
The theory of arithmetic is integral to many uses of SMT solvers. Z3 has implemented native solvers for arithmetic reasoning since its first release. We present a full re-implementation of Z3’s original arithmetic solver. It is based on substantial experiences from user feedback, engineering and experimentation. While providing a comprehensive overview of the main components we emphasize selected new insights we arrived at while developing and testing the solver.
You have full access to this open access chapter, Download conference paper PDF
1 Introduction
The theory of arithmetic is among the most prolific theories used in SMT solvers. It is used across a wide set of applications, and they have a wide range of demands. Supporting efficient theory solvers for arithmetic requires balancing feature support, ranging from linear, difference logic, to linear real, linear integer, non-linear polynomial arithmetic and in cases transcendental functions such as exponentiation. The aim of this paper is to provide a high-level, yet self-contained, overview of internal ingredients of the arithmetic solver. It seeks to explain tool users what to expect of solving methodologies when using Z3 for arithmetic. We assume familiarity of basics of SMT solving using CDCL(T), e.g., [5]. While make an effort to cover all features for completeness, we devote attention to highlight a selection that to our knowledge are unique for arithmetic solvers. These highlights include (1) how the solver patches linear real programming solutions to find solutions to integer variables, (2) heuristics that are new in how the solver finds Gomory cuts, and (3) the solver’s integration of Gröbner basis computation for solving non-linear constraints. User pain points around SMT have to our experience centered dominantly around quantifiers and non-linear arithmetic. A complete (for non-linear reals) solver that integrates with other theories and quantifier reasoning becomes relevant. The new arithmetic solver that we describe here was first integrated in version 4.8.8 of z3, turned on as default in the next release, and subjected to later significant revisions. To evaluate the contribution of each feature we use benchmarks drawn from SMTLIB benchmark sets [3] and benchmarks supplied by a user, Certora [12].
In overview, the arithmetic solver uses a waterfall model for solving arithmetic constraints. It is illustrated with additional details in Fig. 1.
-
First, it establishes feasibility with respect to linear inequalities. Variables are solved over the rationals; Sect. 3.
-
Second, it establishes feasibility with respect to mixed integer linear constraints; Integer variables are considered solved if they are assigned integer values while satisfying linear inequalities; Sect. 4.
-
Finally, it establishes feasibility with respect to non-linear polynomial constraints; Sect. 5.
The rest of the paper elaborates on the components of the solver. For completeness, we go through all relevant pieces. We highlight parts that to our knowledge are novel.
2 Design Goals and Implementation Choices
The SMT formalism for arithmetic in many cases subsumes formalisms used by mixed integer, MIP, solvers. However, there are several fundamental differences between the workloads we have tuned the arithmetic solver for compared to workloads seen by MIP solvers. Z3 uses infinite precision “big-num” numeral representations, in contrast to using floating points. The drawback is that the arithmetic solver is impractical on linear programming optimization problems, but the engine avoids having to compensate for rounding errors and numerical instability. The solver uses a sparse matrix representation for the Dual Simplex tableau. 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. Finally, the solver remains integrated within a CDCL engine that favors an eager case split strategy leaving it to conflict analysis to block infeasible branches. This contrasts mainstream MIP designs that favor a search tree of relatively few branches where the engine performs significant analysis before case splits.
3 Linear Real Arithmetic
The solver first determines whether arithmetic constraints are feasibility over the reals. It also attempts to propagate equalities eagerly for shared variables and infer stronger bounds of variables.
3.1 Linear Solving
Based on [21] the solver for real linear inequalities uses a dual simplex solver. It partitions the variables into basic and non-basic variables, and maintains a global set of equalities of the form \(x_{bi} + \sum _j a_{ij}x_j = 0\), where i refers to the i’th row, \(x_{bi}\) is basic and \(x_j\) range over non-basic variables. It also maintains an evaluation \(\beta \), such that \(\beta (x_{bi}) + \sum _j a_{ij}\beta (x_j)= 0\) for each row i. Each variable \(x_j\) is assigned lower and upper bounds during search. The solver then checks whether \(lo_j \le \beta (x_j) \le hi_j\), for bounds \(lo_j, hi_j\) that are dynamically added and removed by Boolean decisions \(x_j \le hi_j\), \(x_j \ge lo_j\). If the bounds are violated, it updates the evaluation and pivots if necessary. We recall the approach using an example.
Example 1
For the following formula
the solver introduces auxiliary variables \(s_1, s_2\) and represents the formula as
Only bounds (e.g., \(s_1 \le 2\)) are asserted during search. The slack variables \(s_1, s_2\) are initially basic (dependent) and x, y are non-basic. In dual Simplex tableaux, values of a non-basic variable \(x_j\) can be chosen between \(lo_j\) and \(hi_j\). The value of a basic variable is a function of non-basic variable values. Pivoting swaps basic and non-basic variables and moves basic variables within their bounds to bounds violations. For example, assume we start with a set of initial values \(x = y = s_1 = s_2 = 0\) and bounds \(x \ge 0, s_1 \le 2, s_1 \ge 2\). Then \(s_1\) has to be 2 and it is made non-basic. Instead, y becomes basic: \( {y} + x - s_1 = 0, \ {s_2} + x - 2s_1 = 0. \) The new tableau updates the assignment of variables to \(x = 0, s_1 = 2, s_2 = 4, y = 2\). The resulting assignment is a model for the original formula.
3.2 Finding Equal Variables - Cheaply
It is useful to have the arithmetic solver propagate implied equalities when arithmetic is used in combination with other theories, or even when it solves non-linear arithmetic constraints. Equality propagation is disabled for pure arithmetic theories, such as QF_LIA, QF_LRA [3]. Z3 originally used a method based on storing offset equalities in a hash table. An offset equality is of the form \(x_i = y + k\), where k is a numeric constant. Offset equalities are extracted from rows that contain \(x_i\) as a basic variable, and contains only one other non-fixed variable y, while other variables are fixed and their lower (upper) bounds add up to k. It turns out that computing k is expensive when the tableau contains large numeric constants. Hash table operations contribute with additional overhead. It turns out that neither the offset hash-table, nor computing k, is really necessary. We describe our new method, using an example. We first described the method for avoiding to compute offsets in [8]. The description there relies on building a tree data-structure for connecting variables and fails to leverage that the dual simplex tableau can be used directly.
Example 2
From equalities \(x + 1 = y, y - 1 = z\) infer that \(x = z\). Based on the tableau form, the solver is presented with the original equality atoms via slack variables
The tableau can be solved by setting \(x = 0, y = 0, z = 0, s_1 = 1, s_2 = -1, u = 1\). The slack variables are bounded when the equalities are asserted
The original solution is no longer valid, the values for \(s_1, s_2\) are out of bounds. Pivoting re-establishes feasibility using a different solution, for example
with assignment \(z = 0, x = y = -1\). The variables x and y have the same value, but must they be equal under all assignments? We can establish this directly by subtracting the right-hand sides \(z - u - s_1\) and \(z - u - s_2\) from another and by factoring in the constant bounds to obtain the result 0. But subtraction is generally expensive if there are many bounded constants in the rows. Such arithmetical operations are not required to infer that \(x = y\).
Z3 uses the following conditions to infer an equality between variables x, y having the same values in the current assignment:
-
x is basic, and the tableau has row \(x - y + \alpha = 0\),
-
x, y are connected through a non-basic variable z in a pair of the tableau rows in one of the following forms (1) \(x - z + \alpha = 0, y - z + \alpha ' = 0\), (2) \(x + z + \alpha = 0, y + z + \alpha ' = 0\),
where \(\alpha , \alpha '\) are linear combinations of fixed variables.
We experimented with generalizing the connection between equal variables to allow non-unit coefficients on z, but it did not result in measurable improvements.
3.3 Bounds Propagation
It is not uncommon that SMT formulas contain different bounds for the same variable, such as one atom \(x \ge 2\) and another atom \(x \ge 3\). When the atom \(x \ge 3\) is assigned to true, the solver can directly propagate \(x \ge 3\). Bounds can also be inferred indirectly. With a row \(x - 2y = 0\) and bound \(y \ge 1\), it follows that \(x \ge 2\). To implement direct bounds propagation, the solver maintains an index that maps each variable to the set of bounds atoms where it occurs. To implement indirect bounds propagation, the solver queries updated rows for whether they imply bounds that are stronger than the currently asserted bounds. If so, these stronger bounds are used by the index for direct bounds propagation.
4 Integer Linear Arithmetic
The mixed integer linear solver consists of several layers that first attempt to patch integer variables form solutions over reals to solutions over integers. Then, if patching fails to correct all integer variables, it checks for integer infeasibility by checking light-weight Diophantine feasibility criteria and then resort to variants of Gomory Cuts and Branch and Bound.
4.1 Patching
In a feasible tableau we can assume that all non-basic variables are at their bounds and therefore if they have integer sort they are assigned integer values. Only the basic variables could be assigned non-integer values. Patching seeks changing values of non-basic values in order to assign integer values to basic variables. A related method, that diversifies values of variables using freedom intervals was described in [18], but we found it does not preserve integral assignments.
Thus, we patch rows with basic variables \(x_b \not \in \mathcal {Z}\). We use a process that seeks a \(\delta \), such that \(|\delta |\) is minimal and the row with \(x_b\) is of the form \(x_b + \alpha y + \alpha 'x' = 0\), where \(\alpha \not \in \mathcal {Z}\), such that the update \(\beta (y) := \beta (y) + \delta \) is within the bounds of y, \(x_b\) is assigned an integer value and such that \(x_b\) becomes integer without breaking any bounds in the tableau.
Example 3
Suppose we are given a tableau of the form \( y - \frac{1}{2} x = 0, \ z - \frac{1}{3} x = 0 \) where y, z are basic variables and x has bounds [3, 10], y has bounds \([-3,4]\), z has bounds \([-5,12]\). The variable x is initially assigned at the bound \(\beta (x) = 3\). Then \(\beta (y) = \frac{3}{2}\) and \(\beta (z) = 1\). But neither y nor z is close to their bounds. We can move x to 8 without violating the bound for y because of \(y - \frac{1}{2} x = 0\). Thus, the freedom interval for x is the range [3, 8] and within this range there is a solution, \(x = 6\), where y, z are integers and within their bounds.
4.2 Cubes
An important factor in solving more satisfiable integer arithmetic instances is a method by Bromberger and Weidenbach [9, 10]. It allows detecting feasible inequalities over integer variables by solving a stronger linear system. Their method relies on the following property: The inequalities \(Ax \le b\) are integer feasible, for matrix A and vectors x, b, if \(Ax \le b - \frac{1}{2}|\!|A|\!|_1\) has a solution over the reals. We use the 1-norm \(|\!|A|\!|_1\) of a matrix as a column vector, such that each entry i is the sum of the absolute values of the elements in the corresponding row \(A_i\).
Example 4
Suppose we have \(3x + y \le 9 \wedge - 3y \le -2\) and wish to find an integer solution. By solving \(3x + y \le 9 - \frac{1}{2}(3 + 1) = 7, -3y \le -2 - \frac{1}{2}3 = -3.5\) we find a model where \(y = \frac{7}{6}, x = 0\). After rounding y to 1 and maintaining x at 0 we obtain an integer solution to the original inequalities.
Z3 includes a twist relative to [10] that allows to avoid strengthening on selected inequalities [6]. First, we note that difference inequalities of the form \(x - y \le k\), where x, y are integer variables and k is an integer offset need not be strengthened: they have a solution over reals if and only if they have a solution over integers. For octagon constraints \(\pm x \pm y \le k\), there is a boundary condition: they need only require strengthening if x, y are assigned at mid-points between integral solutions. For example, if \(\beta (x) = \frac{1}{2}\) and \(\beta (y) = \frac{3}{2}\), for \(x + y \le 2\).
4.3 GCD Consistency
A basic test for integer infeasibility is by enforcing divisibility constraints.
Example 5
Assume we are given a row \(5/6x + 3/6y + z + 5/6u = 0\), where x, y are fixed at \(2 \le x \le 2\), \(-1 \le u \le -1\), and z is the base variable. Then it follows that \(5 + 3(y + 2z) = 0\) which has no solution over the integers: The greatest common divisor of coefficients to the non-fixed variables (3) does not divide the constant offset from the fixed variables (5).
The basic test is extended as follows. For each row \(a x + b y + c = 0\), where
-
a, b, c and x, y are vectors of integer constants and variables, respectively.
-
the coefficients in a are all the same and smaller than the coefficients in b
-
the variables x are bounded
Let \(l := a\cdot lb(x), u := a \cdot ub(x)\). That is, the lower and upper bounds for \(a\cdot x\) based on the bounds for x. If \(\lfloor \frac{u}{\gcd (b,c)} \rfloor > \lceil \frac{l}{\gcd (b,c)} \rceil \), then there is no solution for x within the bounds for x.
4.4 Branching
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 x, the value \(\frac{1}{2}\), in which case z3 creates a literal \(x \le 0\) that triggers two branches \(x \le 0\) and \(\lnot (x \le 0) \equiv x \ge 1\).
4.5 Cuts
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. Z3 implements Chvátal-Goromy cuts described in [21]. It also implements algorithms from [13, 20] to generate cuts after the linear systems have been transformed into Hermitian matrices. It is a long-standing and timely challenge [1] to harness the effectiveness of selecting cuts. While the solver takes [21] as starting point, it incorporates a few heuristics and enhancements.
Recall that a row \(\sum _{j=0}^{k} a_j\cdot x_j + x_b = 0\) from the tableau is called a Gomory row, and is eligible for Gomory cut, if \(x_b\) is a basic variable and \(x_j\) are non-basic variables, \(x_b\) is an integral variable, but \(\beta (x_b)\) is not integral, and for each \(x_j\) we have \(\beta (x_j) = lo_j\) or \(\beta (x_j) = hi_j\), and the bounds are not strict.
We use a relaxed definition of Gomory rows. For a non-basic integral variable \(x_j\) we allow for value \(\beta (x_j)\) to be not at a bound when \(\beta (x_j)\), and \(a_j\) are both integers: Let us call such \(x_j\) row integral.
To select a cut variable, our main heuristic sorts all Gomory rows from the tableau by the distance of \(\beta (x_b)\) from the nearest integer, that is \(\min \{ {\beta (x_b)-\lfloor \beta (x_b) \rfloor , \lceil \beta (x_b) \rceil - \beta (x_b)} \}\), and pick a few of them having the minimal distance to produce the cuts. We break the ties by preferring the variables that are used in more terms. Heuristics used previously relied on distances to bounds.
We also look for the case when \(x_b\) is at an extremum. For example, if for all \(x_j\) we have \(\beta (x_j) = lo_j\), and \(a_j > 0\) then \(x_b\) is at the maximum, and we deduce \(x_b \le \lfloor \beta (x_b) \rfloor \). The explanations of the Gomory term do not include constraints on \(x_j\) for \(j \in A\) from the relaxed definition, but in case of an extremum these constraints should be added.
Cuts are consequences of the current bounds. By default the solver adds new rows to the Dual Simplex tableau corresponding to cuts, but makes an exception when the new rows include large numerals. In analogy the solver avoids bounds propagation, Sect. 3.3, when computation of bounds relies on big-num arithmetic. Similarly, cuts that involve large coefficients are first added to a temporary scope where the tableau is checked for feasibility. The cuts are only re-added within the main scope if the temporary tableau is infeasible.
5 Non-linear Arithmetic
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 \(x \cdot x \cdot y\), a definition \(m = x \cdot x \cdot y\), where m is a variable that represents the monomial \(x \cdot x \cdot y\). The module for non-linear arithmetic then collects the monomial definitions that are violated by the current evaluation, that is \(\beta (m) \ne \beta (x) \cdot \beta (x) \cdot \beta (y)\). It attempts to establish a valuation \(\beta '\) where \(\beta '(m) = \beta '(x) \cdot \beta '(x) \cdot \beta '(y)\), or derive a consequence that no such evaluation exists.
5.1 Patch Monomials
A patch for a variable x is admissible if the update \(\beta (x) := v\) does not break any integer linear constraints and x does not occur in monomial equations that are not already false under \(\beta \).
-
Set \(\beta (m) := \beta (x) \cdot \beta (x) \cdot \beta (y)\) and check if the patch of m is admissible.
-
Try to set \(\beta (y) := \beta (m) / (\beta (x) \cdot \beta (x))\), provided \(\beta {x}\) is not 0, and check that the patch for x is admissible.
-
When \(\beta (m) = r^2\) for a rational and \(m := x \cdot x\) try patching x by setting \(\beta (x) := \pm r\).
5.2 Bounds Propagation
A relatively inexpensive step is to propagate and check bounds based on non-linear constraints. For example, for \(y \ge 3\), then \(m = x\cdot x\cdot y \ge 3\), if furthermore \(x \le -2\), we have the strengthened bound \(m \ge 12\). Bounds propagation can also flow from bounds on m to bounds on the variables that make up the monomial, such that when \(m \ge 8, 1 \le y \le 2, x \le 0\), then we learn the stronger bound \(x \le -2\) on x. It uses an interval arithmetic abstraction, that understands bounds propagation over squares. Thus, if \(-2 \le x \le 2\), then \(0 \le x^2 \le 4\) instead of \(-4 \le x^2 \le 4\).
The solver also performs Horner expansions of polynomials to derive stronger bounds. For example, if \(x \ge 2, y \ge -1, z \ge 2\), then \(y + z \ge 1\) and therefore \(x\cdot (y + z) \ge 2\), but we would not be able to deduce this fact if combining bounds individually for \(x\cdot y\) and \(x \cdot z\) because no bounds can be inferred for \(x \cdot y\) in isolation. The solver therefore attempts different re-distribution of multiplication in an effort to find stronger bounds.
5.3 Adding Bounds
Non-linear bounds propagation only triggers if all variables are either bounded from above or below or occur with an even power. The solver includes a pass where it adds a bound case split \(x \ge 0\) to variables x where \(lo_x = -\infty , hi_x = +\infty \). The added case split may help trigger bounds propagation, such as detecting conflicts on \(xy > 0, xz > 0, y > 0 > z\).
5.4 Gröbner reduction
Z3 uses a best effort Gröbner basis reduction to find inconsistencies, cheaply, and propagate consequences. While Gröbner basis heuristics are not new to Z3, they have evolved and to our knowledge the integration is unique among SMT solvers. Recall that reduced Gröbner basis for a set of polynomial equations \(p_1 = 0, \ldots , p_k = 0\) is a set \(q_1 = 0, \ldots , q_m = 0\), such that every \(p_i\) is a linear sum of \(q_j\)’s, and the leading monomials of every pair \(q_i, q_j\), \(i \ne j\), have no common factors. Since Z3 uses completion as a heuristic to make partial inferences, it does not seek to compute a basis. 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).
Z3 first adds equations \(m = x_1\ldots x_k\) for monomial definitions that are violated. It then traverses the transitive cone of influence of Simplex rows that contain one of the added variables from monomial definitions. It only considers rows where the basic variable is bounded. Rows where the basic variable is unbounded are skipped because the basic variable can be solved for over the reals. Fixed variables are replaced by constants, and the bounds constraints that fixes the variables are recorded as dependencies with the added equation. Thus, the equations handled by the Gröbner basis reduction are of the form \(\langle p_i: xy + 3z + 3 = 0, d_i: \{3 \le u \le 3\} \rangle \), where \(p_i\) is a polynomial and \(d_i\) is a set of dependencies corresponding to fixed variables that were replaced by constants in \(p_i\). In the example, we replaced u by 3 and the definition \(\langle m = xy, \emptyset \rangle \) resolved m by xy. Dependencies are accumulated when two polynomials are resolved to infer a new derived equality. Generally, when \(\langle xy + p_1 = 0, d_1\rangle , \langle xz + p_2 = 0, d_2 \rangle \) are two polynomial equations, then \(\langle zp_1 - yp_2 = 0, d_1 \cup d_2\rangle \) can be derived accumulating the premises \(d_1, d_2\).
Finally, 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, the derived equations are post-processed:
-
Constant Propagation. For equalities of the form \(x = 0\) or \(ax + b = 0\). If the current assignment to x does not satisfy the equation, then the equality is propagated as a lemma.
-
Linear Propagation. As a generalization of constant propagation, if the completion contains linear equations that evaluate to false under the current assignment, then these linear equations are added to the Simplex Tableau. Example 6 illustrates a use where this propagation is useful.
-
Factorization. Identify factors of the form \(x y p \simeq 0\) where x, y are variables an p is linear. We infer the clause \(x y p \simeq 0 \Rightarrow x \simeq 0 \vee y \simeq 0 \vee p \simeq 0\).
Example 6
(Combining Gröbner completion and Linear Solving). We include an example obtained from Yoav Rodeh at Certora. The instance was not solvable prior to adding simplex propagation. To solve it, Certora relied on treating multiplication as an uninterpreted function and including selected axioms for modular arithmetic and multiplication that were instantiated by E-matching. The distilled example is:
where \(L = N \;\textrm{div}\;2, U = 1 + L\), \(m_r = (x \cdot ( ite (y \ge 0, y, N + y))) \ \text{ mod }\ N\). We assume N is even, such as \(N = 2^{256}\). The solver associates a variable m with \(x \cdot y\) and \(m'\) with \(x \cdot y'\) and \(y'\) with \( ite (y \ge 0, y, N + y)\) and includes the constraints \(0 \le m_r < N, m_q \cdot N + m_r = m'\), where \(m_q\) is an integer variable. The most interesting case is where \(y < 0\), so \(y' = y + N\). Gröbner basis completion then allows to derive \(m_q N + m_r = m' = x(y + N) = xy + xN = m + xN\), which by integer linear arithmetic reasoning (the extended GCD test) contradicts \(m \ne m_r\) because the absolute value of both variables is below N.
Our extraction of linear constraints represents a partial integration of linear programming and polynomial arithmetic, that favors only including linear inequalities over variables and monomials that are already present. Our implementation does not include any variables for new monomials produced by completion. In comparison, the approach in [25] proposes a domain for abstract interpretation that populates a linear solver with all equations produced by a completion. We have not experimented in depth with extending our approach with a full basis, or use it as a starting point for finding lemmas based on Positivstellensatz or other extension mechanisms [32, 34].
We use an adaptation of ZDD (Zero suppressed decision diagrams [29, 30]) 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. Figure 2 shows a polynomial stored in a polynomial decision diagram, PDD.
The root node labeled by x represents the polynomial \(x\cdot l + r\), where l is the polynomial of the left sub-graph and r the polynomial of the right sub-graph. The left sub-graph is allowed to be labeled again by x, 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 x above y. Then the polynomial for the right sub-graph is \(y + 1\), and the polynomial with the left sub-graph is \(5xy + (y + 1)\).
5.5 Incremental Linearization
Following [14] we incrementally linearize monomial definitions that currently evaluate to false. For example, we include lemmas of the form \(x = 0 \rightarrow m = 0\) and \(x = 1 \rightarrow m = y\), for \(m = x^2y\). Incremental linearization proceeds by first applying linearizations that are considered cheap, such as case splitting on whether variables take values 0, 1, −1, when these boundary conditions are exhausted, instantiates lemmas based on monotonicity of multiplication and tangents. It is possible that there are overlapping monomial definitions, such as \(m' = x \cdot y\). Then incremental linearization takes into account that the definition for m can be factored into \(m' \cdot x\). It also uses specialized congruence closure reasoning, recognizing equalities modulo signs, such that when \(m = x \cdot y, m' = z \cdot y\) and \(x = -z\) in the current context, then \(m \sim -m'\).
To find all factorizations of monomial \(m = \prod _{i \in A}{x_i} \) as \(m = m_0 \cdot m_1\), we choose \(a \in A\) and enumerate over all proper subsets B of A containing a. For each B we check that \(m_0 = \prod _{i \in B}{x_i}\) and \(m_1 = \prod _{i \in A \setminus B}{x_i}\) are monomials.
To support floating point arithmetic reasoning we also include incremental linearization lemmas for special cases of exponentiation [15]. We also added rules for incremental linearization of divisibility operations. The front-end to the core arithmetic solver axiomatizes integer and real division operations using multiplication and addition, so that the solver does not have to reason about division. Nevertheless, we found use cases for instantiating axioms of the form \(y > 0 \wedge x > z \Rightarrow x/y > z/y\) (when the input contains terms x/y, z/y) bypassing indirect reasoning around constraints created by axioms.
5.6 NLSat
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 [24]. NLSAT is complete for non-linear arithmetic and includes branch-and-bound to handle cases of integer arithmetic. It can therefore sometimes be used to solve goals, bypassing the partial heuristics entirely. The solver therefore includes selected calls to NLSat with a small resource bound to close branches before attempting incomplete heuristics such as incomplete linearization. The results in Sect. 7 suggests that our use of NLSat with a resource bound currently incurs significant overhead on easy problems, but overall is an advantage. We found that it is sometimes the case that turning off NLSat all-together can speed up the solver significantly, but is overall a disadvantage.
6 Shared Equalities
Z3 uses model-based theory combination [18] for sharing equalities between theories. In the context of arithmetic it means that in a satisfiable state shared variables where \(\beta (x) = \beta (y)\) it also holds that the literal \(x \simeq y\) is assigned to true. For larger benchmarks we observed that there can be a significant overhead in checking whether a term occurs in a shared context because it relies on properties of which parent terms it occurs. We therefore introduced a way to cache the property of being shared in the E-nodes. The property gets invalidated when the a new parent E-node is added or the congruence class of the E-node is merged.
7 Evaluation
To get an idea of how the new solver compares and how the individual features of weigh on performance we conducted a set of measurements. They are based on three benchmark sets: QF_LIA, SMTLIB2 benchmarks for the theory of quantifier-free integer linear arithmetic, QF_NIA, SMTLIB2 benchmarks for the theory of quantifier-free non-linear integer arithmetic, and benchmark-submission, a smaller set of verification conditions obtained from Certora. Data associated with the measurements summarized in this Section are available from [7]. We ran the solvers for 600 s and measured how many problems are solved within 600 s. We compared default settings of the solvers with CVC5 [2, 17, 26], MathSat5 [16, 28], and Yices2 [22, 37], and Z3’s legacy arithmetic solver, which is available by setting the option smt.arith.solver=2. The advances relative to the legacy solver are noticable. Compared to other solvers, Yices2 and MathSat5 shine as fast out of the gates solving relatively more problems within 1 s. The are mainly limited by the set of supported features, such as lack of support for algebraic data-types. We compare how many instances the solvers handle within 1 s, within 1–10 s, 10–100 s, and 10–600 s. We also list timeouts and cases where the solver returns unknown because of incompleteness, and cases where benchmarks are unhandled, either because the solver runs out of allocated virtual memory set to 2 GB, or due to unsupported features. The version of Z3 used for the experiments corresponds to 4.12.5.
Figure 3 shows results of evaluating z3 when disabling selected features. It suggests that using NLSat to eagerly close branches comes with a steep cost for easy benchmarks. It can likely be tuned in future versions of Z3. The eager use of NLSat still provides an overall benefit. Z3 also uses tactics that run a few strategies with a 5 s resource bounds early on to find models using SAT encodings and selected branch-and-bound strategies. They are also a cause of relatively slow startup. The default tactics can be overridden. The feature with overall biggest impact is incremental linearization. While it is run after gcd tests, bounds propagation and Gröbner saturation, it has a significant effect. Other features have each a relative minor effect in isolation. The solver relies on their cumulative effect.
8 Summary and Discussion
We presented the architecture and a cross-cut of system innovations in a new arithmetic solver in Z3. It is shown to provide good advances relative to the legacy arithmetic solver, and our evaluation suggests it compares very well with other state-of-art SMT solvers. The new solver enabled us to addresses some design choices with the previous solver that limited extensibility. Notably, the new solver separates its representation of arithmetic constraints from terms shared by other solvers through an E-graph. We noticed that limitation of using shared terms is that the boundary for when to treat a sub-term as a variable or a polynomial is inherently ambiguous. The legacy solver is also highly incomplete for non-linear reasoning (over the reals).
Many avenues for further innovations and tuning remain. Another important aspect is trust. Implementing the many features of the arithmetic solver is inherently a complex task. Many bugs get uncovered by fuzzing [11, 23, 27, 31, 33, 35, 36] both in the legacy and new solver, bearing witness to the difficulty of creating a correct solver. The solver therefore supports a number of ways to validate results. The easiest validation is for satisfiable formulas, where the satisfiable formula is model checked against the returned model. The main difficulty with satisfiable models is to correctly track interpretations of under-specified operations, such as division by 0. To check that consequences produced by the solver are valid, there is a self-validator enabled by the smt.arith.validate=true. It uses the legacy arithmetic solver to check lemmas and propagations. There is also a mechanism for creating certificates that can be processed offline or online. With each theory axiom and propagation produced by the solver, it produces a certificate object that can be used to validate inferences by the arithmetic solver. The certificates are exposed in proof objects [19] and also as annotations in proof logs [4]. Z3 contains a built-in proof checker for proof logs. The proof checker for arithmetic certificates validates conflicts that can be justified by using Farkas lemma and bounds propagations that use cuts. It currently falls back to invoking Z3 on lemmas (using the legacy arithmetic solver) for non-linear lemmas and other cases not covered by the built-in checker. Certificates created for QF_LRA are fully handled, while self-contained or independent proof checking for more expressive fragments of arithmetic is future work.
References
Balcan, M.-F., Prasad, S., Sandholm, T., Vitercik, E. Structural analysis of branch-and-cut and the learnability of gomory mixed integer cuts. In: Koyejo, S., Mohamed, S., Agarwal, A., Belgrave, D., Cho, K., Oh, A. (eds.) Advances in Neural Information Processing Systems 35: Annual Conference on Neural Information Processing Systems 2022, NeurIPS 2022, New Orleans, LA, USA, November 28–December 9 2022 (2022)
Barbosa, H., et al.: cvc5: a versatile and industrial-strength SMT solver. In: TACAS 2022, Part I. LNCS, vol. 13243, pp. 415–442. Springer, Cham (2022). https://doi.org/10.1007/978-3-030-99524-9_24
Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB) (2016)
Bjørner, N.: Proofs for SMT (2022). https://z3prover.github.io/slides/proofs.html
Bjørner, N., et al.: Z3 internals (2023). https://z3prover.github.io/papers/z3internals.html
Bjørner, N., Nachmanson, L.: Theorem recycling for theorem proving. In: Vampire (2017)
Bjørner, N., Nachmanson, L.: Supplementary data (2024). https://github.com/z3prover/doc/arithmetic
Bjørner, N., Nachmanson, L.: Navigating the universe of Z3 theory solvers. In: Carvalho, G., Stolz, V. (eds.) SBMF 2020. LNCS, vol. 12475, pp. 8–24. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-63882-5_2
Bromberger, M., Weidenbach, C.: Fast cube tests for LIA constraint solving. In: IJCAR (2016)
Bromberger, M., Weidenbach, C.: New techniques for linear arithmetic: cubes and equalities. Formal Methods Syst. Des. 51(3), 433–461 (2017)
Brummayer, R., Lonsing, F., Biere, A.: Automated testing and debugging of SAT and QBF solvers. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol. 6175, pp. 44–57. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14186-7_6
Certora: Certora Benchmarks (2023). https://github.com/jar-ben/benchmark-submission
Christ, J., Hoenicke, J.: Cutting the mix. In: CAV (2015)
Cimatti, A., Griggio, A., Irfan, A., Roveri, M., Sebastiani, R.: Experimenting on solving nonlinear integer arithmetic with incremental linearization. In: SAT (2018)
Cimatti, A., Griggio, A., Irfan, A., Roveri, M., Sebastiani, R.: Incremental linearization for satisfiability and verification modulo nonlinear arithmetic and transcendental functions. ACM Trans. Comput. Log. 19(3), 19:1–19:52 (2018)
Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The MathSAT5 SMT solver. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 93–107. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-36742-7_7
CVC5: CVC5 executable (2024). https://github.com/cvc5/cvc5/releases/. For the experiments we used the newest available version at the time https://cvc5.stanford.edu/downloads/builds/x86_64-win64-production/cvc5-2024-01-08-x86_64-win64-production.exe. It is no longer available for download, but would have to be recreated from Git state. We reran experiments using the current release, March 2024 with degraded results
de Moura, L.M., Bjørner, N.: Model-based theory combination. Electron. Notes Theor. Comput. Sci. 198(2), 37–49 (2008)
de Moura, L.M., Bjørner, N.: Proofs and refutations, and Z3. In: Rudnicki, P., Sutcliffe, G., Konev, B., Schmidt, R.A., Schulz, S. (eds.) Proceedings of the LPAR 2008 Workshops, Knowledge Exchange: Automated Provers and Proof Assistants, and the 7th International Workshop on the Implementation of Logics, Doha, Qatar, 22 November 2008, volume 418 of CEUR Workshop Proceedings. CEUR-WS.org (2008)
Dillig, I., Dillig, T., Aiken, A.: Cuts from proofs: a complete and practical technique for solving linear inequalities over integers. In: CAV (2009)
Dutertre, B., de Moura, L.: A fast linear-arithmetic solver for DPLL(T). In: CAV (2006)
Dutertre, B.: Yices 2.2. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 737–744. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08867-9_49
Hwang, D.: Z3 Issue tracker (2024). https://github.com/z3prover/z3
Jovanovic, D., de Moura, L.M.: Solving non-linear arithmetic. In: IJCAR (2012)
Kincaid, Z., Koh, N., Zhu, S.: When less is more: consequence-finding in a weak theory of arithmetic. Proc. ACM Program. Lang. 7(POPL), 1275–1307 (2023)
Kremer, G., Reynolds, A., Barrett, C., Tinelli, C.: Cooperating techniques for solving nonlinear real arithmetic in the cvc5 SMT solver (system description). In: Blanchette, J., Kovács, L., Pattinson, D. (eds.) IJCAR 2022. LNCS, vol. 13385, pp. 95–105. Springer, Cham (2022). https://doi.org/10.1007/978-3-031-10769-6_7
Mansur, M.N., Christakis, M., Wüstholz, V., Zhang, F.: Detecting critical bugs in SMT solvers using blackbox mutational fuzzing. In: Devanbu, P., Cohen, M.B., Zimmermann, T. (eds.) ESEC/FSE 2020: 28th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, Virtual Event, USA, 8–13 November 2020, pp. 701–712. ACM (2020)
MathSat5: MathSat5 executable (2024). https://mathsat.fbk.eu/download.php?file=mathsat-5.6.10-win64-msvc.zip
Minato, S.: Zero-suppressed BDDs for set manipulation in combinatorial problems. In: Dunlop, A.E. (ed.) DAC (1993)
Nishino, M., Yasuda, N., Minato, S., Nagata, M.: Zero-suppressed sentential decision diagrams. In: AAAI (2016)
Park, J., Winterer, D., Zhang, C., Su, Z.: Generative type-aware mutation for testing SMT solvers. Proc. ACM Program. Lang. 5(OOPSLA), 1–19 (2021)
Platzer, A., Quesel, J.-D., Rümmer, P.: Real world verification. In: Schmidt, R.A. (ed.) CADE 2009. LNCS (LNAI), vol. 5663, pp. 485–501. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02959-2_35
Sun, M., Yang, Y., Wang, Y., Wen, M., Jia, H., Zhou, Y.: SMT solver validation empowered by large pre-trained language models. In: 2023 38th IEEE/ACM International Conference on Automated Software Engineering (ASE), pp. 1288–1300 (2023)
Tiwari, A.: An algebraic approach for the unsatisfiability of nonlinear constraints. In: Ong, L. (ed.) CSL 2005. LNCS, vol. 3634, pp. 248–262. Springer, Heidelberg (2005). https://doi.org/10.1007/11538363_18
Winterer, D., Zhang, C., Su, Z.: On the unusual effectiveness of type-aware operator mutations for testing SMT solvers. Proc. ACM Program. Lang. 4(OOPSLA):193:1–193:25 (2020)
Winterer, D., Zhang, C., Su, Z.: Validating SMT solvers via semantic fusion. In: Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 718–730 (2020)
Yices2. Yices2 executable (2024). https://yices.csl.sri.com/releases/2.6.4/yices-2.6.4-x86_64-pc-mingw32-static-gmp.zip
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Copyright information
© 2024 The Author(s)
About this paper
Cite this paper
Bjørner, N., Nachmanson, L. (2024). Arithmetic Solving in Z3. In: Gurfinkel, A., Ganesh, V. (eds) Computer Aided Verification. CAV 2024. Lecture Notes in Computer Science, vol 14681. Springer, Cham. https://doi.org/10.1007/978-3-031-65627-9_2
Download citation
DOI: https://doi.org/10.1007/978-3-031-65627-9_2
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-65626-2
Online ISBN: 978-3-031-65627-9
eBook Packages: Computer ScienceComputer Science (R0)