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 [44]) [34]. 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, 27] are solved using a dedicated engine, SPACER, [28] that builds on an engine inspired by IC3, [6, 29]. 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, 41] 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 [35] as explained in the context of Z3 in [17].

\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 [21, 23, 38] 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 [25] 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 [24]. 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$).

This GCD test is extended to as follows. For each row $a x + b y + c = 0$, where

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

Let $ll := \lceil \frac{l}{\gcd(b,c)} \rceil$, $uu := \lfloor \frac{u}{\gcd(b,c)} \rfloor$. If $uu > ll$, there is no solution for $x$ within the bounds for $x$.

Patching

When a tableau with integer variables is feasible, all non-basic variables can be assumed to be integers: Dual simplex moves non-basic variables to their bounds and the bounds are integers. Only the basic variables could be non-integral (they are still within their bounds). Patching seeks changing values to non-basic values to move as many basic variables to integers.

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.

Z3 patching works by shifting a non-basic variable by $\delta$ to make a dependent basic variable integral. 

   for $x_b$ in basic variables, such that $\beta(x_b) \not\in Z$:
       for $\alpha y$ in row of $x_b$ with $\alpha \not\in Z$:
           find $\delta$ such that the update $\beta(y) := \beta(y) + \delta$
            is feasible and fixes more basic variables than it breaks

Given a row $x_b + \alpha y + r = 0$, where $x_b$ is a basic variable, $y$ is non-basic variable multiplied by the fraction $\alpha$, and $r$ is the remainding of the row, the shift amount $\delta$ is computed based on the following analysis.

Take first the fractional parts of $\beta(x_b)$ and $\alpha$:

The goal is to compute integers

These two integers are the minimal amount to move the value $\beta(y)$ to make the value of $\beta(x_b)$ integral.

Let $Z$ be the set of integers. We solve for $\delta \in Z$ such that $L := \frac{x_1}{x_2}+\frac{a_1}{a_2}\delta \in Z$ too. If $L \in Z$ then $a_2 \frac{x_1}{x_2}+ a_1\delta$ is also an integer. Therefore $a_2 \frac{x_1}{x_2} \in Z$. That means $a_2 := t x_2$ for some $t \in Z$, because $x_1$ and $x_2$ are coprime. By substituting $a_2$ with $x_2 t$ we get $L:= \frac{x_1}{x_2}+\frac{a_1}{x_2 t}\delta$ and $L x_2 := x_1+\frac{a_1}{t}\delta \in Z$. Since $t \uparrow a_2$, and $a_2$ and $a_1$ are coprime, $t \uparrow \delta$. Therefore, we search for $\delta$ in form $\delta :=m t$, $m \in Z$. We obtain $L:= \frac{x_1}{x_2}+\frac{a_1}{x_2 t} m t = \frac{x_1+m a_1}{x_2}$. From $L \in Z$ follows $x_2 k = x_1 + m a_1$ for some $k \in Z$. We can rewrite the last equality as $x_1 = a_1 m - x_2 k$. Because $x_2 \uparrow a_2$, and $a_1$ and $a_2$ are coprime, $x_2$ and $a_1$ are mutually prime too. That means that for some $u, v$ we have $1 = a_1 u + x_2 v$. We can show that if $\delta := u t x_1$ then $\frac{x_1}{x_2}+\frac{a_1}{a_2}\delta \in Z$.

From the other side, for any $\gamma \in Z$ satisfying $\frac{x_1}{x_2}+\frac{a_1}{a_2}\gamma \in Z$ holds $\frac{a_1(\delta - \gamma)}{a_2} \in Z$. Since $a_1$ and $a_2$ are coprime, $a_2 \uparrow (\delta - \gamma)$, and $\gamma := \delta \mod a_2$. We conclude that $\delta^+ = \delta \mod a_2$, and $\delta^{-} = \delta^+ - a_2$.

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, 22] 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 [37, 39]) 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 [34].

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 [30]. 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 [17] 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