Z3 Internals (Draft)
Nikolaj Bjørner
Microsoft Research
Clemens Eisenhofer
TU Wien
Arie Gurfinkel
U Waterloo
Nuno P. Lopes
U Lisbon
Leonardo de Moura
Microsoft Research
Lev Nachmanson
Microsoft Research
Christoph Wintersteiger
Microsoft Research

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.

1. Introduction

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.

Z3Overall

Figure 1. Overall system architecture of Z3

1.1. Resources

The main point of reference for Z3 is the GitHub repository

https://​github.​com/​z3prover/​z3

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

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

This guide complements the tutorial

https://​z3prover.​github.​io/​papers/​programmingz3.​html

Some of the internals are already described in depth in the Programming Z3 tutorial so they are covered in less detail here.

2. Solver Cores

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.

2.1. CDCL(T) - SAT in the light of Theory Solvers

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 $F$ of formulas and a partial assignment to literals in $F$ that we refer to as $M$.
The solver starts in a state $\langle M, F\rangle$, where $M$ is initially empty. It then attempts to complete $M$ to a full model of $F$ to show that $F$ is satisfiable and at the same time adds consequences to $F$ to establish that $F$ 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 $\langle M; F; C\rangle$, where, besides the partial model $M$ and formula $F$, there is also a conflict clause $C$ false under $M$. The auxiliary function Theory is used to advance decisions, propagations and identify conflicts. If Theory determines that $F$ is conflicting with respect to the literals in $M$ it produces a conflict clause $C$, that contains a subset of conflicting literals from $M$. It can also produce a trail assignment $A$, which is either a propagation or decision and finally, if it determines that $F$ is satisfiable under trail $M$ it produces $SAT$.

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 $\Theory(M;F)$:

Thus, the verdict of Theory determines whether the partial model extends to a model of the theories, can identify a subset of $M$ as an unsatisfiable core, propagate the truth assignment of a literal $\ell$, or create a new case split $\Decision{\ell}$ for a literal $\ell$ that has not already been assigned in $M$. We write $SAT = \Theory(M,F)$ when the verdict is that $M$ extends to a valid theory model of $F$, we write $C = \Theory(M,F)$ when $C$ is a conflict clause, based on negated literals from $M$ and $A = \Theory(M,F)$, when the verdict $A$ is either a propagation or decision.

\[\begin{mdmathpre}%mdk \\ \mbox{Sat}~&~\langle \mathid{M};~{\mathid{F}}~\rangle &~\Rightarrow &~\mathid{SAT}~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~&~\mathid{SAT}~=~\Theory(\mathid{M},~\mathid{F})\\ \\ \mbox{Conflict}~&~\langle \mathid{M};~\mathid{F}~\rangle &~\Rightarrow &~\langle \mathid{M};~\mathid{F};~\mathid{C}~\rangle &~\mathid{C}~=~\Theory(\mathid{M},~\mathid{F})~\\ \\ \mbox{Augment}~&~\langle \mathid{M};~{\mathid{F}}~\rangle &~\Rightarrow &~\langle \mathid{M},~\mathid{A};~\mathid{F}~\rangle &~\mathid{A}~=~\Theory(\mathid{M},~\mathid{F})~\\ \\ \mbox{Unsat}~&~\langle \emptyset;~{\mathid{F}};~{\mathid{C}}~\rangle &~\Rightarrow &~\mathid{UNSAT}~\\ \\ \mbox{Resume}~&~\langle \mathid{M},~\Decision{\overline{\ell}};~{\mathid{F}};~\mathid{C}~\rangle &~\Rightarrow &~\langle \mathid{M},~\Propagation{\ell}{\mathid{C}};~{\mathid{F}}~\rangle &~\ell \in {\mathid{C}}\\ \\ \mbox{Resolve}~&~\langle \mathid{M},~\Propagation{\ell}{\mathid{C}'};~\mathid{F};~{\mathid{C}}\rangle &~\Rightarrow &~\langle \mathid{M};~\mathid{F};~(\mathid{C}~\setminus \{\overline{\ell}\})~\cup (\mathid{C}'\setminus\{{\ell}\})~\rangle &~\overline{\ell}~\in {\mathid{C}}\\ \\ \mbox{Backtrack}~&~\langle \mathid{M},~\mathid{A};~\mathid{F};~\mathid{C}~\rangle &~\Rightarrow &~\langle \mathid{M};~\mathid{F};~{\mathid{C}}~\rangle &~\mathid{otherwise}\\ \end{mdmathpre}%mdk \]

Example 1.
Consider the formula $(x > 0 \vee y > 0) \wedge x + y < 0$. The initial state of search is

\[\langle \emptyset; (x > 0 \vee y > 0)\wedge x + y < 0\rangle \]

based on the empty partial assignment $\emptyset$ and the original formula. A possible next state is to propagate on the unit literal $x + y < 0$, producing

\[\langle \Propagation{x + y < 0}{x + y < 0}; (x > 0 \vee y > 0) \wedge x + y < 0\rangle \]

This step may be followed by a case split setting $x > 0$ to false.

\[\langle \Propagation{x + y < 0}{x + y < 0},\Decision{\neg(x > 0)}; (x > 0 \vee y > 0) \wedge x + y < 0\rangle \]

which triggers a unit-propagation

\[\langle \Propagation{x + y < 0}{x + y < 0},\Decision{\neg(x > 0)},\Propagation{y > 0}{x > 0 \vee y > 0}; (x > 0 \vee y > 0) \wedge x + y < 0\rangle \]

The resulting state is satisfiable in the theory of arithmetic. On the other hand, if we had chosen to set $x > 0$ to true as well as $y > 0$, we would have encountered a conflicting state with conflict clause $\neg (x > 0) \vee \neg (y > 0)$1:

\[\langle \Propagation{x + y < 0}{x + y < 0},\Decision{x > 0},\Decision{y > 0};\ (x > 0 \vee y > 0) \wedge x + y < 0; \ \neg (x > 0) \vee \neg (y > 0)\rangle \]

The last decision is then reverted to produce the satisfiable state

\[\langle \Propagation{x + y < 0}{x + y < 0},\Decision{x > 0},\Propagation{\neg(y > 0)}{\neg (x > 0) \vee \neg (y > 0)};\ (x > 0 \vee y > 0) \wedge x + y < 0\rangle \]

A third scenario uses theory propagation. In this scenario, the decision $x > 0$ is made, but instead of making a decision $y > 0$, the theory solver for arithmetic is given a chance to find opportunities for propagation. It deduces that $x + y < 0$ together with $x > 0$ implies $\neg(y > 0)$, and therefore establishes the theory propagation

\[\langle \Propagation{x + y < 0}{x + y < 0},\Decision{x > 0},\Propagation{\neg(y > 0)}{\neg(y > 0) \vee \neg (x > 0)};\ (x > 0 \vee y > 0) \wedge x + y < 0\rangle \]

We are again eliding the unit literal $x + y < 0$ from the explanation for $\neg(y > 0)$. In practice, solvers automatically remove literals from conflict clauses that are necessarily false.

2.1.1. Other Inference Rules

In the initial overview of the CDCL(T) loop, we left out other inference rules that are integral to efficient search.

2.1.2. Invariants

To be well-behaved we expect Theory to produce propagations on literals that don't already appear in $M$, and crucially enforce the main invariants:

That is, each conflict clause is a consequence of $F$ and each propagation is also a consequence of $F$, and the premises of a propagation is justified by $T$.

2.2. NLSAT (MC-SAT)

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.

2.3. SPACER

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

\[\begin{mdmathpre}%mdk \mdmathindent{3}&~\forall \vec{\mathid{x}}~\ .~\ \varphi \land \mathid{P}(\mathid{t})~\land \mathid{Q}(\mathid{s})~\implies \mathid{R}(\mathid{u})~~~~\\ \mathid{or}~&~\forall \vec{\mathid{x}}~\ .~\ \varphi \land \mathid{P}(\mathid{t})~\land \mathid{Q}(\mathid{s})~\implies \false \end{mdmathpre}%mdk \]

where $\varphi$ is a formula that is interpreted over a combination of theories, $P, Q, R$ are uninterpreted predicates, and $t, s, u$ are terms over the bound variables $\vec{x}$ and the theories from $\varphi$. The SPACER engine searches for a model for $P, Q, R$ such that all clauses are true under the model.

2.4. QSAT

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.

3. Decision Procedures

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].

\begin{picture}(270,210)(0,-10) \multiput(75,40)(0,77){3}{\oval(20,20)[tr]} \multiput(75,0)(0,77){3}{\oval(20,20)[br]} \multiput(10,40)(0,77){3}{\oval(20,20)[tl]} \multiput(0,0)(0,77){3}{\line(0,1){40}} \multiput(85,0)(0,77){3}{\line(0,1){40}} \multiput(10,50)(0,77){3}{\line(1,0){65}} \multiput(10,-10)(0,77){3}{\line(1,0){65}} \multiput(10,0)(0,77){3}{\oval(20,20)[bl]} \put(16,155){\shortstack{E-matching\\ based \\ Quantifier\\ Instantiation}} \put(16, 92){\shortstack{EUF + SAT}} \put(16,0){\shortstack{Model\\ based \\ Quantifier\\ Instantiation}} \put(267,195){\oval(20,20)[tr]} \put(267,0){\oval(20,20)[br]} \put(149,195){\oval(20,20)[tl]} \put(149,0){\oval(20,20)[bl]} \put(149,-10){\line(1,0){120}} \put(149,205){\line(1,0){120}} \put(139,0){\line(0,1){195}} \put(277,0){\line(0,1){195}} \multiput(255,20)(0,37){5}{\oval(20,20)[tr]} \multiput(255,10)(0,37){5}{\oval(20,20)[br]} \multiput(165,10)(0,37){5}{\oval(20,20)[bl]} \multiput(165,20)(0,37){5}{\oval(20,20)[tl]} \multiput(155,10)(0,37){5}{\line(0,1){10}} \multiput(265,10)(0,37){5}{\line(0,1){10}} \multiput(165,30)(0,37){5}{\line(1,0){90}} \multiput(165,0)(0,37){5}{\line(1,0){90}} \put(170,12){Strings/Sequences} \put(185,50){Datatypes} \put(185,86){Bit-vectors} \put(195,122){Arrays} \put(185,158){Arithmetic} \put(190,190){Theories} \put(42,50){\vector(0,1){17}} \put(42,67){\vector(0,-1){17}} \put(42,127){\vector(0,1){17}} \put(42,144){\vector(0,-1){17}} \put(85,95){\vector(1,0){54}} \put(139,95){\vector(-1,0){54}} \end{picture}
Figure 2. Architecture of Z3's SMT Core solver.

3.1. Boolean Theories

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 $x + y \ge 2$ assuming both $x$ and $y$ consist of $2$ bits results in the formula

\[\begin{mdmathpre}%mdk \mathid{z}_1~&\equiv (\mathid{x}_1~\vee \mathid{y}_1)~\wedge (\lnot \mathid{x}_1~\vee \lnot \mathid{y}_1)\\ \mathid{c}_2~&\equiv (\mathid{x}_1~\wedge \mathid{y}_1)\\ \mathid{z}_2~&\equiv (\mathid{x}_2~\vee \mathid{y}_2~\vee \mathid{c}_2)~\wedge (\lnot \mathid{x}_2~\vee \mathid{y}_2~\vee \mathid{c}_2)~\wedge (\mathid{x}_2~\vee \lnot \mathid{y}_2~\vee \lnot \mathid{c}_2)~\wedge (\lnot \mathid{x}_2~\vee \lnot \mathid{y}_2~\vee \lnot \mathid{c}_2)\\ \mathid{z}_2& \end{mdmathpre}%mdk \]

the result of the summation is given by $z = (z_1, z_2)$. $c_2$ is the carry of adding the first bits of $x$ and $y$. Pseudo-Boolean constraints like $x + \lnot y + 2z \ge 2$ 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

\[\begin{mdmathpre}%mdk \mathid{if}~\mathid{z}:&&&\\ &~\mathid{true}&&\\ \mathid{else}:&&&\\ &~\mathid{if}~\mathid{x}:&&\\ &&\mathid{if}~\lnot \mathid{y}:&\\ &&&~\mathid{true}\\ &&\mathid{else}:&\\ &&&\mathid{false}\\ &\mathid{else}:\\ &&\mathid{false}& \end{mdmathpre}%mdk \]

which can be translated to a propositional formula. The sorting network approach sorts the bit-sequence $\langle x, \lnot y, z, z\rangle$ to a sequence $\langle s_1, s_2, s_3, s_4 \rangle$ and asserts that $s_3$ 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.

3.2. Equality and Uninterpreted Functions

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

\[ a \simeq f(f(a)), a \simeq f(f(f(a))), a \not\simeq f(a) \]

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.

\[\begin{mdmathpre}%mdk \mdmathindent{2}\mathid{n}_1~\equiv \mathid{f}(\mathid{a}),~\mathid{n}_2~\equiv \mathid{f}(\mathid{n}_1),~\mathid{n}_3~\equiv \mathid{f}(\mathid{n}_2)~\\\\ \mdmathindent{2}\mathid{a}~\simeq \mathid{n}_2,~\mathid{a}~\simeq \mathid{n}_3,~\mathid{a}~\not\simeq \mathid{n}_1 \end{mdmathpre}%mdk \]

Process equality atoms using union-find. It establishes the equivalence classes

\[ \{ a, n_2, n_3 \}, \{ n_1 \} \]

Then congruence closure triggers whenever there are two nodes, $n_1, n_2$ from different equivalence classes, labeled by the same function $f$, with equal children. In our case $a, n_2$ belong to the same equivalence class so the nodes $n_1, n_3$ are merged.

\[\{ a, n_2, n_3, n_1 \} \]

When the children of the equality term $a \simeq n_1$ are merged into the same equivalence class, the term $a \simeq n_1$ is set to true. This contradicts that $a \simeq n_1$ is already set to false.

3.2.1. E-Node

The E-Node data-structure [22, 24, 39] is used to implement congruence closure efficiently. The main fields of an E-Node are

\[\begin{mdmathpre}%mdk \mdmathindent{4}\mathid{n}~:~&~\langle &~\mathid{f}:~&~\mathid{Func}~~&~\mbox{function symbol}\\ \mdmathindent{8}&~~~~~~&~\mathid{ts}:~&~\mathid{N}^*~&~\mbox{arguments}\\ \mdmathindent{8}&~~~~~~&~\mathid{find}:~&~\mathid{N}~\times \mathid{N}~\times \Nat &~\mbox{link to representative, sibling and class size}\\ \mdmathindent{8}&~~~~~~&~\mathid{P}:~~~~&~\mathid{N}^*~~~&~\mbox{list of parents}~~~~~~~~~~~~\\ \mdmathindent{8}&~~~~~~&~\mathid{cg}:~~~&~\mathid{N}~~~~&~\mbox{congruence representative}\\ \mdmathindent{8}&~~~~~~&~\mathid{j}:~~~~&~\mathid{null}~|~\mathid{Just}~\times \mathid{N}~&~\mbox{pointer to justification and node}\\ \mdmathindent{8}&~\rangle \end{mdmathpre}%mdk \]

When a term $f(ts)$ occurs in a formula used by the solver it is compiled into an E-node $n$. The E-node $n$ is initialized to

\[ n \leftarrow \langle f = f, ts = ts, \find = (n,n,1), P = null, cg = n, j = null \rangle. \]

Example 3.
The result of internalizing the following term

\[ f(g(a), g(a), a) \]

is

\[\begin{mdmathpre}%mdk \mdmathindent{2}\mathid{n}_1~&~:=~&~\langle \mathid{f}~=~\mathid{a},~\mathid{ts}~=~[],~\find =~(\mathid{n}_1,~\mathid{n}_1,~1),~\mathid{P}~=~[\mathid{n}_2,~\mathid{n}_3],~\mathid{cg}~=~\mathid{n}_1,~\mathid{j}~=~\mathid{null}~\rangle\\ \mdmathindent{2}\mathid{n}_2~&~:=~&~\langle \mathid{f}~=~\mathid{g},~\mathid{ts}~=~[\mathid{n}_1],~\find =~(\mathid{n}_2,~\mathid{n}_2,~1),~\mathid{P}~=~[\mathid{n}_3],~\mathid{cg}~=~\mathid{n}_2,~\mathid{j}~=~\mathid{null}~\rangle\\ \mdmathindent{2}\mathid{n}_3~&~:=~&~\langle \mathid{f}~=~\mathid{f},~\mathid{ts}~=~[\mathid{n}_2,~\mathid{n}_2,~\mathid{n}_1],~\find =~(\mathid{n}_3,~\mathid{n}_3,~1),~\mathid{P}~=~[],~\mathid{cg}~=~\mathid{n}_3,~\mathid{j}~=~\mathid{null}~\rangle\\ \end{mdmathpre}%mdk \]

The field $\find$ 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 $f$ and list of arguments to $f$ that are represented by root E-nodes into a congruence closure root. For the congruence closure root $n$ it maintains the invariant $n.cg = \mathit{etable}[n.f, \rootNode(n.ts)]$. We write $\mathit{etable}[n.f, \rootNode(n.ts)]$ to indicate that the etable tracks function applications to root nodes. In reality, the etable just stores the node $n$ and uses the $\rootNode$ function when computing the current hash of $n$ and equalities with other nodes.

3.2.2. Merge

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($n_1, n_2, j$) to establish that two nodes $n_1, n_2$ are equal under justification $j$. We describe justifications later in more detail. The main steps of merge are outlined below.

Roots $r_1 \leftarrow \rootNode(n_1), r_2 \leftarrow \rootNode(n_2)$
assume $r_1 \neq r_2$
assume $r_1.sz \leq r_2.sz$
Erase for each $p \in r_1.P$ where $p.cg = p$:
    erase $\mathit{etable}[p.f, \rootNode(p.ts)]$
Update Root $r_1.\find \leftarrow r_2$
Justify justify($r_1, r_2, j$)
Insert for each $p \in r_1.P$:
  if $\mathit{etable}[p.f,\rootNode(p.ts)] = null$ then
     $\mathit{etable}[p.f,\rootNode(p.ts)] \leftarrow p$
  $p.cg \leftarrow$ etable$[p.f, \rootNode(p.ts)]$
  if $p.cg = p$ then
    append $p$ to $r_2.P$
  else
    add $\langle p.cg, p, cc\rangle$ to tomerge

3.2.3. Unmerge

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 $p$ is appended to $r_2.P$ 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($r_1, r_2$) is as follows:

Erase for each $p \in r_2.P$ added from $r_1.P$:
  erase $\mathit{etable}[p.f, \rootNode(p.ts)]$
UnJustify unjustify($r_1, r_2, j$)
Revert Root $r_1.\find \leftarrow r_1$
Insert for each $p \in r_1.P$:
  if $p.cg \neq p \lor \rootNode(p.ts) \neq \rootNode(p.cg)$
     $\mathit{etable}[p.f,\rootNode(p.ts)] \leftarrow p.cg \leftarrow p$

3.2.4. Justifications

A justification is a reason for merging two nodes. There are two possible reasons for merging nodes:

  1. A literal $\ell: s \simeq t$ is asserted. The justification is the literal $\ell$.
  2. Nodes are merged due to congruence closure.
\[\begin{mdmathpre}%mdk \mdmathindent{3}\mathid{Just}~::=~\ell:~\mathid{s}~\simeq \mathid{t}~|~\mathid{cc}:~\mathid{f}(\mathid{ts})~\simeq \mathid{f}(\mathid{ts}') \end{mdmathpre}%mdk \]

NB: $cc: f(ts) \simeq f(ts')$ is justified recursively by justifying $ts \simeq ts'$.

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.

\[\begin{mdmathpre}%mdk \mdmathindent{4}\mathid{r}_1~\leftarrow \rootNode(\mathid{n}_1)\\ \mdmathindent{4}\mathid{r}_2~\leftarrow \rootNode(\mathid{n}_2)\\ \mdmathindent{4}\mathid{r}_1.\find \leftarrow \mathid{r}_2\\ \mdmathindent{4}\mathid{old}~\mathid{justification}:~\mathid{n}_1~\stackrel{\mathid{j}_1}{\rightarrow}~\mathid{n}^1_1~\stackrel{\mathid{j}_2}{\rightarrow}~\mathid{n}^2_1~\cdots \stackrel{\mathid{j}_\mathid{m}}{\rightarrow}~\mathid{r}_1\\ \mdmathindent{4}\mathid{new}~\mathid{justification}:~\mathid{n}_1~\stackrel{\mathid{j}_1}{\leftarrow}~\mathid{n}^1_1~\stackrel{\mathid{j}_2}{\leftarrow}~\mathid{n}^2_1~\cdots \stackrel{\mathid{j}_\mathid{m}}{\leftarrow}~\mathid{r}_1\\ \mdmathindent{4}\mathid{add}~\mathid{justification}:~\mathid{n}_1~\stackrel{\mathid{j}}{\rightarrow}~\mathid{n}_2 \end{mdmathpre}%mdk \]

justificationunionfind

Note that not all possible justifications are tracked, if merge($n_1, n_2, j$) is invoked but already $\rootNode(n_1) = \rootNode(n_2)$, then the justification $j$ for the equality of $n_1, n_2$ 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.

3.2.5. From justifications to proofs

We can create proofs from first-principles by using justifications. Suppose $\rootNode(s) = \rootNode(t)$ follows from a sequence merge($s_1, t_1, \ell_1$), merge($s_2, t_2, \ell_2$),$\ldots$, merge($s_k, t_k, \ell_k$).

Then a proof of $s \simeq t$ can be extracted using overloaded functions $\pi$:

\[\begin{array}{ll} \proof(s \simeq t) & = \begin{array}{c} \AxiomC{$\proof(s \stackrel{j}{\rightarrow} \cdots a)$} \AxiomC{$\proof(t \stackrel{j'}{\rightarrow} \cdots a)$} \RightLabel{symm} \UnaryInfC{$a \simeq t$} \RightLabel{trans} \BinaryInfC{$s \simeq t$} \DisplayProof\\[2em] \mbox{$a$ is a least common $\rightarrow$ ancestor of $s, t$} \end{array} \end{array} \]
\[\begin{array}{ll} \proof(s \stackrel{j}{\rightarrow} t \stackrel{j'}{\rightarrow} \cdots u) & = \begin{array}{c} \AxiomC{$\proof(j, s \simeq t)$} \AxiomC{$\proof(t \stackrel{j'}{\rightarrow} \cdots u)$} \RightLabel{trans} \BinaryInfC{$s \simeq u$} \DisplayProof \end{array} \\[1.5em] \proof(s) & = \begin{array}{c} \AxiomC{\mbox{}} \RightLabel{refl} \UnaryInfC{$s \simeq s$} \DisplayProof \end{array} \\[1.5em] \proof(\ell : s \simeq t, s \simeq t) & = \ell \\[1.5em] \proof(\ell : t \simeq s, s \simeq t) & = \begin{array}{c} \AxiomC{$\ell$} \RightLabel{symm} \UnaryInfC{$s \simeq t$} \DisplayProof \end{array} \\[1.5em] \proof(cc: f(ts) \simeq f(ts'), f..) & = \begin{array}{c} \AxiomC{$\proof(ts_1 \simeq ts'_1), \ldots, \proof(ts_k \simeq ts'_k)$} \RightLabel{cong} \UnaryInfC{$f(ts) \simeq f(ts')$} \DisplayProof \end{array} \end{array} \]

3.2.6. Integration with Boolean reasoning

In the setting of CDCL(T), congruence closure is integrated with Boolean reasoning. For example, if $p(a)$ is assigned true, $a \simeq b$, then the Boolean predicate $p(b)$ 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 $a \wedge b$ is assigned to $\true$, then clausification of $a\wedge b$ introduces clauses $\neg (a \wedge b) \vee a$ and $\neg (a \wedge b) \vee b$, the ensure propagation to $a, b$. 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 $n_1, n_2$ of $n_3: n_1 \simeq n_2$ are merged, then the $\mathit{value}$ of $n_3$ is set to $\true$.

The E-graph also dispatches equality and disequality propagation between theories.

3.3. Arithmetic

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 $x - y \leq k$, for $k$ a constant, and unit-two-variable-per-inequality (UTVPI), where all inequalities are of the form $\pm x \pm y \leq k$. 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.

Arithmetic

Figure 3. An overview of Arithmetical Decision Procedures in Z3

3.3.1. Rational linear arithmetic

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 $A\vec{x} = 0$, and each variable $x_j$ is assigned lower and upper bounds during search. The solver then checks for feasibility of the resulting system $A\vec{x} = 0, lo_j \leq x_j \leq hi_j, \forall j$ for dynamically changing bounds $lo_j, hi_j$. The bounds are justified by assignments in $M$.

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 $s_1, s_2$ and represents the formula as

\[\begin{mdmathpre}%mdk \mdmathindent{2}\mathid{s}_1~\equiv \mathid{x}~+~\mathid{y},~\mathid{s}_2~\equiv \mathid{x}~+~2\mathid{y},\\ \mdmathindent{2}\mathid{x}~\geq 0,~(\mathid{s}_1~\leq 2~\vee \mathid{s}_2~\geq 6),~(\mathid{s}_1~\geq 2~\vee \mathid{s}_2~>~4) \end{mdmathpre}%mdk \]

Only bounds (e.g., $s_1 \leq 2$) are asserted during search.

The first two equalities form the tableau. Thus, the definitions ${s_1} \equiv x + y, {s_2} \equiv x + 2y$ produce the equalities

\[{s_1} = x + y, \ {s_2} = x + 2y \]

They are equivalent to the normal form:

\[{s_1} - x - y = 0, \ {s_2} - x - 2y = 0 \]

where ${s_1, s_2}$ are 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. 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 $x = y = s_1 = s_2 = 0$ and bounds $x \geq 0, s_1 \leq 2, s_1 \geq 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.

Finding equal variables - cheaply

Example 5.
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

\[\begin{mdmathpre}%mdk \mdmathindent{4}\mathid{s}_1~=~\mathid{x}~+~\mathid{u}~-~\mathid{y},~\mathid{s}_2~=~\mathid{y}~-~\mathid{u}~-~\mathid{z},~1~\leq \mathid{u}~\leq 1 \end{mdmathpre}%mdk \]

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

\[\begin{mdmathpre}%mdk \mdmathindent{4}\mathid{s}_1~=~\mathid{x}~+~\mathid{u}~-~\mathid{y},~\mathid{s}_2~=~\mathid{y}~-~\mathid{u}~-~\mathid{z},~1~\leq \mathid{u}~\leq 1,~0~\leq \mathid{s}_1~\leq 0,~0~\leq \mathid{s}_2~\leq 0 \end{mdmathpre}%mdk \]

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

\[ x = z - u - s_1, y = z - u - s_2, 1 \leq u \leq 1, 0 \leq s_1 \leq 0, 0 \leq s_2 \leq 0 \]

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. The arithmetical operations are not required to infer that $x = y$. Z3 uses two facts to infer the equality

Variables that satisfy these two criteria must be equal.

3.3.2. Integer linear arithmetic

The mixed integer linear solver consists of several layers.

GCD consistency

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 $x_j$ is fixed if the current values $lo_j$, $hi_j$ 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 $5/6x + 3/6y + z + 5/6u = 0$, where $x, y$ are fixed at $2 \leq x \leq 2$, $-1 \leq u \leq -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$).

Patching

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

\[\begin{mdmathpre}%mdk \mdmathindent{1}\mathid{y}~-~\frac{1}{2}~\mathid{x}~=~0\\ \mdmathindent{1}\mathid{z}~-~\frac{1}{3}~\mathid{x}~~=~0 \end{mdmathpre}%mdk \]

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.

Cubes

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 $A, A'$ range over integer matrices and $a$, $b$, $c$ over integer vectors. The 1-norm $\onenorm{A}$ of a matrix is a column vector, such that each entry $i$ is the sum of the absolute values of the elements in the corresponding row $A_i$. We write $\onenorm{A_i}$ to directly access the 1-norm of a row $i$.

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 $3x + y \leq 9 \wedge - 3y \leq -2$ and wish to find an integer solution. By solving $3x + y \leq 9 - \frac{1}{2}(3 + 1) = 7, -3y \leq -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.

Our twist on Bromberger and Weidenbach's method is to avoid strengthening on selected inequalities. First, we note that difference inequalities of the form $x - y \leq k$, where $x, y$ are integer variables and $k$ is an integer offset need not be strengthened. For octagon constraints $\pm x \pm y \leq 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 $V(x) = \frac{1}{2}$ and $V(y) = \frac{3}{2}$, for $x + y \leq 2$. Our approach is described in detail in [5].

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 \leq 0$ that triggers two branches $x \leq 0$ and $\neg(x \leq 0) \equiv x \geq 1$.

Gomory and Hermite 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. It also incorporates algorithms from [14, 23] to generate cuts after the linear systems have been transformed into Hermite matrices.

3.3.3. 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$ an equation $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 attempts to establish a valuation $V$ where $V(m) = V(x) \cdot V(x) \cdot V(y)$, or derive a consequence that no such valuation exists. The stages in the waterfall model are summarized in the following paragraphs.

Bounds propagation on monomials

A relatively inexpensive step is to propagate and check bounds based on non-linear constraints. For example, for $y \geq 3$, then $m = x\cdot x\cdot y \geq 3$, if furthermore $x \leq -2$, we have the strengthened bound $m \geq 12$. Bounds propagation can also flow from bounds on $m$ to bounds on the variables that make up the monomial, such that when $m \geq 8, 1 \leq y \leq 2, x \leq 0$, then we learn the stronger bound $x \leq -2$ on $x$.

Bounds propagation with Horner expansions

If $x \geq 2, y \geq -1, z \geq 2$, then $y + z \geq 1$ and therefore $x\cdot (y + z) \geq 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.

Gröbner reduction

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 $v = v_1\ldots v_k$ for arithmetic variables that are defined as monomials.

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 $5x^2y + xy + y + x + 1$ is represented by the acyclic graph shown below.

\usetikzlibrary{shapes,arrows} \usetikzlibrary{positioning} \tikzstyle{block} = [rectangle, draw, text centered, rounded corners, minimum height=2em] \tikzstyle{line} = [draw, -latex'] \begin{tikzpicture}[node distance = 3em, scale = 0.2] \node [circle, draw] (xroot) {$x$}; \node [circle, below of = xroot, left of= xroot, draw] (xnext) {$x$}; \node [circle, below of = xnext, left of= xnext, draw] (y1) {$y$}; \node [circle, below of = xnext, right of = xnext] (yempty) {}; \node [circle, right of= yempty, draw] (y2) {$y$}; \node [circle, below of = y1, left of = y1] (t1) {$5$}; \node [circle, below of = y1, right of = y1] (t2) {$0$}; \node [circle, right of = t2] (t3) {$1$}; \node [circle, below of = y2, right of = y2] (t4) {$1$}; \path [line] (xroot.west) -- (xnext.north); \path [line] (xroot.east) -- (y2.north); \path [line] (xnext.west) -- (y1.north); \path [line] (xnext.east) -- (y2.north); \path [line] (y1.west) -- (t1.north); \path [line] (y1.east) -- (t2.north); \path [line] (y2.west) -- (t3.north); \path [line] (y2.east) -- (t4.north); \end{tikzpicture}

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)$.

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).

Incremental linearization

Following [15] we incrementally linearize monomial constraints. For example, we include lemmas of the form $x = 0 \rightarrow m = 0$ and $x = 1 \rightarrow m = y$, for $m = x^2y$.

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 [35].

3.3.4. Data-structures

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 $x \geq 3 \implies x \geq 2$ for atomic formulas $x \geq 3, x\geq 2$.

3.4. Reducible Theories

3.4.1. Refinement Types

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 $S$ uses a predicate $p$ over $S$. At least one element of $S$ must satisfy $p$ for the construction to make sense. The refinement type $S \mid p$ represents the elements of $S$ that satisfy $p$. The properties we need to know about elements of $S\mid p$ can be encoded using two auxiliary functions that form a surjection $\relaxOp$ from $S \mid p$ into $S$ with a partial inverse $\restrictOp$ that maps elements from $S$ into $S \mid p$. The properties of these functions are summarized as follows:

\[\begin{mdmathpre}%mdk \mdmathindent{2}\mathid{p}~:~\mathid{S}~\rightarrow \mathid{Bool}\\ \mdmathindent{2}\relaxOp :~\mathid{S}~\mid \mathid{p}~\rightarrow \mathid{S}\\ \mdmathindent{2}\restrictOp :~\mathid{S}~\rightarrow \mathid{S}~\mid \mathid{p}\\ \mdmathindent{2}\forall \mathid{x}~:~\mathid{S}~\mid \mathid{p}~\ .~\ \restrictOp(\relaxOp(\mathid{x}))~=~\mathid{x}\\ \mdmathindent{2}\forall \mathid{s}~:~\mathid{S}~\ .~\ \mathid{p}(\mathid{s})\ \rightarrow \ \relaxOp(\restrictOp(\mathid{s}))~=~\mathid{s}\\ \mdmathindent{2}\forall \mathid{x}~:~\mathid{S}~\mid \mathid{p}~\ .~\ \mathid{p}(\relaxOp(\mathid{x})) \end{mdmathpre}%mdk \]

Let us illustrate the sort of natural numbers as a refinement type of integers:

Example 9.

\[\begin{mdmathpre}%mdk \mdmathindent{2}\mathid{sort}~\mathid{Nat}~=~\mathid{Int}~\mid \lambda \mathid{x}~\ .~\ \mathid{x}~\geq 0\\ \mdmathindent{2}\forall \mathid{n}~:~\mathid{Nat}~\ .~\ \restrictOp(\relaxOp(\mathid{n}))~=~\mathid{n}~\wedge \relaxOp(\mathid{n})~\geq 0\\ \mdmathindent{2}\forall \mathid{i}~:~\mathid{Int}~\ .~\ \mathid{i}~\geq 0~\rightarrow \relaxOp(\restrictOp(\mathid{i}))~=~\mathid{i} \end{mdmathpre}%mdk \]

We obtain a theory solver for formulas with refinement types by instantiating these axioms whenever there is a term $t$ introduced of sort $S \mid p$ 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 $\relaxOp(\restrictOp(\relaxOp(\restrictOp(\ldots))))$.

3.4.2. Arrays

The theory of arrays in SMTLIB is formally based on two functions select and store and an axiomatization

\[\begin{mdmathpre}%mdk \mdmathindent{2}\mathit{select}(\Astore(\mathid{A},~\mathid{i},~\mathid{v}),~\mathid{j})~=~\mathbf{if}\ \mathid{i}~\simeq \mathid{j}\ \mathbf{then}\ \mathid{v}\ \mathbf{else}\ \mathit{select}(\mathid{A},~\mathid{j})~\\\\ \mdmathindent{2}\forall \mathid{i}~.~\mathit{select}(\mathid{A},~\mathid{i})~\simeq \mathit{select}(\mathid{B},~\mathid{i})~\implies \mathid{A}~\simeq \mathid{B} \end{mdmathpre}%mdk \]

for every array $A, B$, index $i, j$ and value $v$. Alluding to the intent that the theory of arrays is useful for modeling arrays in programming languages will henceforth use $A[i]$ when we mean $\mathit{select}(A, i)$.

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 satisfiable2

\[\forall a : Array(Int, Int) \ . \ \exists k \ . \ \forall i \geq k \ . \ a[i] \simeq 0. \]

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 $\Astore$ and $\mathit{select}$ Z3 includes built-in functions $\Amap$, $\Aconst$ and the operator $\Aasarray$ and lambdas. It includes also the function $\Aext$ that provides a witness term for distinct arrays, and $\delta(A)$ 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 $\beta$ reduction axioms for array terms that admit beta-reduction. We call these terms $\lambda$ terms and they are defined by the beta-reduction axioms:

\[\begin{mdmathpre}%mdk \beta(\Astore(\mathid{A},\mathid{j},\mathid{v})[\mathid{i}])~&~=~&~\mathit{if}\ \mathid{i}~\simeq \mathid{j}\ \mathit{then}~\ \mathid{v}~\ \mathit{else}\ \mathid{A}[\mathid{i}]\\ \beta(\Amap(\mathid{f},\mathid{A},\mathid{B})[\mathid{i}])~&~=~&~\mathid{f}(\mathid{A}[\mathid{i}],\mathid{B}[\mathid{i}])\\ \beta(\Aasarray(\mathid{f})[\mathid{i}])~&~=~&~\mathid{f}(\mathid{i})\\ \beta(\Aconst(\mathid{v})[\mathid{i}])~&~=~&~\mathid{v}\\ \beta((\lambda \mathid{x}~\ .~\ \mathid{M})[\mathid{i}])~&~=~&~\mathid{M}[\mathid{i}/\mathid{x}] \end{mdmathpre}%mdk \]

The reduction into EUF, is then, in a nutshell, an application of the following inference rule:

\[\AxiomC{$b$ is a lambda term} \AxiomC{$a[j]$ is a term} \AxiomC{$b \sim a$ ($a, b$ are equal under EUF)} \TrinaryInfC{$b[j] = \beta(b[j])$} \DisplayProof \]

together with an inference rule to enforce extensionality

\[A[\Aext(A,B)] \simeq B[\Aext(A, B)] \implies A \simeq B \]

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 $n$ the following sets

\[\begin{mdmathpre}%mdk \mathit{ParentSelects}(\mathid{n})~&~=~&~\{~\mathid{A}[\mathid{i}]~\mid \mathid{A}~\sim \mathid{n}~\}~\\ \mathit{ParentLambdas}(\mathid{n})~&~=~&~\{~\Astore(\mathid{A},\mathid{i},\mathid{v})~\mid \mathid{A}~\sim \mathid{n}\}~\cup \{~\Amap(\mathid{f},~\ldots,~\mathid{A},~\ldots)~\mid \mathid{A}~\sim \mathid{n}~\}~\\ \mathit{Lambdas}(\mathid{n})~~~~~~~&~=~&~\{~\Aconst(\mathid{v})~\mid \Aconst(\mathid{v})~\sim \mathid{n}~\}~\cup \\ \mdmathindent{26}&~~~&~\{~\Amap(\mathid{f},\ldots)~\mid \Amap(\mathid{f},\ldots)~\sim \mathid{n}~\}~\cup \\ \mdmathindent{26}&~~~&~\{~\Astore(\ldots)~\mid \Astore(\ldots)~\sim \mathid{n}~\}~\cup \\ \mdmathindent{26}&~~~&~\{~\Aasarray(\mathid{f})~\mid \Aasarray(\mathid{f})~\sim \mathid{n}~\}~\cup \\ \mdmathindent{26}&~~~&~\{~\lambda \mathid{x}~\ .~\ \mathid{M}~\mid \lambda \mathid{x}~\ .~\ \mathid{M}~\sim \mathid{n}~\}~ \end{mdmathpre}%mdk \]

When $n_1$ is merged with $n_2$, and $n_1$ is the new root, the sets from $n_2$ are added to $n_1$. The merge also looks for new redexes when $n$ and $n'$ are merged:

\[\AxiomC{$n \sim n'$} \AxiomC{$A[j] \in \mathit{ParentSelects}(n)$} \AxiomC{$\lambda \in \mathit{Lambdas}(n') \cup \mathit{ParentLambdas}(n')$} \TrinaryInfC{$n \simeq n' \implies \lambda[j] = \beta(\lambda[j])$} \DisplayProof \]

For enforcing $\Astore(A, i, v)[j] = \beta(\Astore(A, i, v)[j])$, the solver only instantiates the axiom $i \simeq j \lor \Astore(A, i, v)[j] \simeq A[j]$ because the axiom $\Astore(A,i,v)[i] \simeq v$ is instantiated eagerly when the term $\Astore(A, i, v)$ is created.

Extensionality is enforced on pairs of array terms $A, B$, 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 $A \equiv \lambda x \ . \ M$ is a lambda term in a shared position and $B$ is in a shared position, the axiom $\lambda x \ . \ M \simeq B \implies \forall i \ . \ M[x/i] \simeq B[i]$ is instantiated. Thus, lambda equality is at the time of writing enforced by a reduction to quantified formulas.

3.4.3. Algebraic Datatypes

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 $C$ for a constructor, for example Assignment is a constructor; $acc_1, \ldots, acc_n$ for accessors corresponding to $C$, for example lval and rval are accessors corresponding to the constructor Assignment. The predicate symbol $isC(t)$ is true if the term $t$ is equal to a term headed by the constructor $C$. The construct $\{ t \mbox{ with } \mathit{field} := s \}$ assigns the term $s$ to an accessor field for the term $t$. 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, $\mathit{head}(\mathit{nil})$. The interpretation of $\mathit{head}(\mathit{nil})$ is not fixed by the theory, instead $\mathit{head}$ 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 $n$ of data-type sort is assigned a constructor representation, initially null. If $n$ is equated to a node $n'$ whose function is labeled by a constructor $C$, the representative for $n$ is labeled by $n'$.

Saturation Rules

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.

Accessor axioms:

If $n$ is a constructor node $C(a_1, \ldots, a_m)$ assert the axioms

\[\begin{mdmathpre}%mdk \mdmathindent{2}\mathid{n}~\simeq \mathid{C}(\mathid{a}_1,~\ldots,~\mathid{a}_\mathid{m})~\implies \mathid{acc}_1(\mathid{n})~\simeq \mathid{a}_1~\land \ldots \land \mathid{acc}_\mathid{m}(\mathid{n})~\simeq \mathid{a}_\mathid{m} \end{mdmathpre}%mdk \]
Update field axioms:

If $n$ is of the form $n := \{ r \ \mathbf{with}\ field := v \}$, where $\mathit{field}$ is an accessor for constructor $C$, then assert the axioms

\[\begin{mdmathpre}%mdk \mdmathindent{2}\mathid{isC}(\mathid{r})~~~~~~&~\implies &~~\mathid{acc}_\mathid{j}(\mathid{n})~\simeq \mathid{acc}_\mathid{j}(\mathid{r})~&~\mbox{for}~&~\mathid{acc}_\mathid{j}~\neq \mathit{field}~\\ \mdmathindent{2}\mathid{isC}(\mathid{r})~~~~~~&~\implies &~~\mathit{field}(\mathid{n})~\simeq \mathid{v}~\\ \mdmathindent{2}\neg \mathid{isC}(\mathid{r})~&~\implies &~~\mathid{n}~\simeq \mathid{r}\\ \mdmathindent{2}\mathid{isC}(\mathid{r})~~~~~~&~\implies &~~\mathid{isC}(\mathid{n}) \end{mdmathpre}%mdk \]
Recognizers

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 $isC(n)$ is asserted to true, then $n$ must be equated to a term with constructor $C$. Conversely, if $n$ is assigned with a constructor $C' \neq C$, then $isC(n)$ is false. The decision procedure ensures this correspondence lazily. If $isC(n)$ is asserted to true, then it ensures the axiom

\[\begin{mdmathpre}%mdk \mdmathindent{2}\mathid{isC}(\mathid{n})~\implies \mathid{n}~\simeq \mathid{C}(\mathid{acc}_1(\mathid{n}),~\ldots,~\mathid{acc}_\mathid{m}(\mathid{n}))~~ \end{mdmathpre}%mdk \]

where $acc_1, \ldots, acc_m$ are the accessors for $C$.

If $isC(n)$ is asserted to false, but $n$ equal to a node $n'$ that is headed by $C$, then it creates the conflict clause:

\[\begin{mdmathpre}%mdk \mdmathindent{3}\mathid{n}~\simeq \mathid{n}'~\implies \mathid{isC}(\mathid{n})~&~\mbox{if}~&~\mathid{n}'~\mbox{ is of the form $C(\ldots)$} \end{mdmathpre}%mdk \]

Something about covering constructors so all possible constructors are tested.

Occurs check

An occurs check violation is detected when there is a state satisfying the properties $n_1 \simeq n_1', n_2 \simeq n_2', \ldots, n_k \simeq n_1$ where each $n_i'$ is of the form $C_i(\ldots, n_{i+1}, \ldots)$. Occurs checks are performed lazily in a final check.

Model construction rules

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 $t$ cannot be assigned a non-recursive base case (say nil), it is assigned a non-recursive constructor (say, cons), that eventually allows assigning $t$ to a term that is arbitrarily deep and therefore can be distinct from any set of other terms $t_2, t_3, \ldots$.

The approach for model construction does not work if we introduce a sub-term predicate $t \preceq s$. The theory of algebraic data-types can be extended to the subterm relation while remaining decidable. If $t, s$ range over an algebraic data-type with two base case constructors $\mathit{nil}_1$ and $\mathit{nil}_2$, and $s = \mathit{nil}_2$. Then unfairly guessing only $\mathit{nil}_1$ before guessing cons, but neglecting $\mathit{nil}_2$ leads to non-termination of a model constructing decision procedure with the sub-term relation.

Quantifier Elimination and Algebraic Datatypes

The theory of algebraic data-types admits partial quantifier elimination.

Present MBP for ADT here specifically?

3.5. Hybrid Theories

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.

3.5.1. Sequences/Strings/Regex

3.5.2. Floating points

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.

4. Data-structure and algorithm internals

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.

4.1. Terms and Formulas

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, $\exists x \forall y, z, p(x, y, z)$ uses de-Bruijn indices 0 for $z$ and 1 for $y$, and 2 for $x$. 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; ...}

4.2. Representing assertions

From input and during pre-processing assertions are represented in a structure of the form

\[\begin{mdmathpre}%mdk \mdmathindent{1}\langle &~\varphi &~:~&~\mathit{Bool}~~~~~~~&~\mbox{the current formula}\\ \mdmathindent{9}&~\pi &~:~&~\mathit{Proof}~~~~~~&~\mbox{a justification for the formula}\\ \mdmathindent{9}&~\delta &~:~&~\mathit{Dependency}~&~\mbox{A dependency structure for the formula}\\ \mdmathindent{1}\rangle \end{mdmathpre}%mdk \]

For a standard input assertion $\varphi$ the structure is initialized as $\langle \varphi, \mathtt{asserted}(\varphi), null \rangle$. The proof of $\varphi$ is that it was asserted. There are no dependencies for $\varphi$.

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 $p$, the structure is initialized as $\langle \varphi, \mathtt{asserted}(\varphi), p \rangle$.

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.

4.3. Compiling terms and formulas into clauses and E-nodes

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 $\true$ or $\false$: The CDCL(T) engine already enforces congruence rules and consistency with assignments to $\true/\false$. The default is overridden if a term occurs as an argument to a non-Boolean connective. For example, in the term $f(a \land b)$, the node $n_{a \land b}$ merges with $\true/\false$ when the truth value to the literal $\ell_{a \land b}$ is propagated. In this way, congruence closure can ensure consistency with respect to occurrences of $f$.

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 $x + y + x$ into a node $n$ and adds the basic row $n = 2x + y$. Top-down compilation does not play well with small static stack sizes allocated by $\text{C}\texttt{++}$ 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.

4.4. Interaction with the CDCL(T) core

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 $F$ and performs case splits and propagations and in this process consults the theory solver $\Theory(M;F)$ for the next propagation, case split or whether $M$ is a theory consistent model of $F$.

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 $T$ gets attached to a node $n$ when

Then, when a Boolean node $n$ is assigned to $\true$ or $\false$ by the CDCL solver, the truth assignment to $n$ is broadcast to all solvers attached to $n$. Similarly, when two nodes $n, n'$ are merged, and the theory $T$ is attached to a sibling of $n$ and a sibling of $n'$, then the equality $n \simeq n'$ is broadcast to $T$.

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 $n \not\simeq n'$, 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 $n \simeq n'$ it accesses the theory variables $v_n$ and $v_{n'}$ that are indices to the array and broadcast $v_{n} \simeq v_{n'}$. The original nodes $n, n'$ are accessed from the theory solver's array, together with other attributes of