Programming Constraint Services with Z3

A tutorial - Automata, Logic and Games, NUS

Nikolaj Bjørner
Microsoft Research

Contents

Slides

Overview

Goal of this tutorial is to give an overview of what you can do with Z3 from the perspectives of:

  • What is expressible: Logics and Theories.

  • Adaptability: Mapping logical queries to Z3.

  • Programmability: using the API.

  • Efficiency: Algorithms.

Z3

  • A state-of-art Satisfiability Modulo Theories (SMT) solver from Microsoft Research

  • Targets applications in software engineering

  • Leonardo de Moura, Nikolaj Bjørner, and Christoph Wintersteiger

    • Contributions from Ken McMillan, Mikolas Janota, Loris d'Antoni, George Karpenkov, Dan Lieuw and several others
    • Contributions are solicited
  • On github: https://github.com/Z3prover/z3.git

    • MIT open source license

Logical Queries

\[\begin{mdmathpre}%mdk \mathrm{Satisfiability}~~~&~\varphi \rightsquigarrow \mathid{sat},~\mathid{unsat},~\mathid{timeout}~\smallskip \\ \mathrm{Certificates}~~~~~&~\varphi \rightsquigarrow \mathid{model},~\mathid{proof},~\mathid{unsat}~\mathid{core}~\smallskip\\ \mathrm{Interpolation}~~~~&~\varphi[\mathid{x},\mathid{y}]~\rightarrow \mathid{I}[\mathid{x}]~\rightarrow \psi[\mathid{x},\mathid{z}]~\smallskip\\ \mathrm{Optimization}~~~~~&~\max \mathid{x}~\mid \varphi \smallskip \\ \mathrm{Consequences}~~~~~&~\varphi \rightarrow \varphi_1~\wedge \ldots \wedge \varphi_\mathid{n}\smallskip\\ \mathrm{Sat\ subsets}~~~~~&~\psi_1~\wedge \psi_2,\ \psi_1~\wedge \psi_3\smallskip\\ \mathrm{Unsat\ cores}~~~~~&~\neg(\psi_1~\wedge \psi_2),\ \neg(\psi_1~\wedge \psi_3)\medskip\\ \mathrm{Model\ counting}~~&~|\{~\mathid{x}~\mid \varphi\}|~\medskip\\ \mathrm{All\ models}~~~~~~&~\mathid{Ideal}(\varphi),~\mathid{M}_1~\models \varphi,~\mathid{M}_2~\models \varphi,~\ldots \medskip\\ \mathrm{Model\ probability}~&~\ldots \end{mdmathpre}%mdk \]

Logics and Theories


  • Terms
  • Logical Connectives
  • Quantifiers, Variables


  • Propositional logic
  • Theory of Equality
  • Uninterpreted Functions
  • Arrays
  • Arithmetic
  • Arrays
  • Algebraic Data-types
  • Bit-vectors, Floating points
  • Sequences, Strings

Basic SAT

\[\begin{mdmathpre}%mdk (\mathid{Tie}~\vee \mathid{Shirt})~\wedge (\neg \mathid{Tie}~\vee \mathid{Shirt})~\wedge (\neg \mathid{Tie}~\vee \neg \mathid{Shirt}) \end{mdmathpre}%mdk \]



  Tie, Shirt = Bools('Tie Shirt')
  s = Solver()
  s.add(Or(Tie, Shirt), Or(Not(Tie), Shirt), Or(Not(Tie), Not(Shirt)))
  print s.check()
  print s.model()

Basic SMT

I = IntSort()
f = Function('f', I, I)
x, y, z = Ints('x y z')
A = Array('A',I,I)

fml = Implies(x + 2 == y, f(Select(Store(A, x, 3), y - 2)) == f(y - x + 1))

s = Solver()
s.add(Not(fml))
print s.check()

Logical Language

  • Terms
  • Logical Connectives
  • Quantifiers, Variables

DPLL [20]

\[ \twodpstate{\underbrace{M}_{\mbox{partial assignment}}}{\underbrace{F}_{\mbox{clauses}}} \]



\[\begin{mdmathpre}%mdk \mathsf{Guess}~~~~~&~\twodpstate{\mathid{p}}{\mathid{p}~\vee \mathid{q},~\overline{\mathid{q}}~\vee \mathid{r}}~&~\Longrightarrow &~\twodpstate{\mathid{p},~\overline{\mathid{q}}}{\mathid{p}~\vee \mathid{q},~\overline{\mathid{q}}~\vee \mathid{r}}\\ \\ \mathsf{Deduce}~~~~&~\twodpstate{\mathid{q}}{\mathid{p}~\vee \mathid{q},~\overline{\mathid{q}}~\vee \mathid{r}}~&~\Longrightarrow &~\twodpstate{\mathid{q},~\mathid{r}}{\mathid{p}~\vee \mathid{q},~\overline{\mathid{q}}~\vee \mathid{r}}\\ \\ \mathsf{Backtrack}~&~\twodpstate{\mathid{p},~\overline{\mathid{s}},~\mathid{q}}{\mathid{s}~\vee \mathid{q},~\overline{\mathid{p}}~\vee \overline{\mathid{q}}}~&~\Longrightarrow &~\twodpstate{\mathid{p},~\mathid{s}}{\mathid{s}~\vee \mathid{q},~\overline{\mathid{p}}~\vee \overline{\mathid{q}}} \end{mdmathpre}%mdk \]

CDCL: Modern Search [50]

  • Efficient indexing (two-watch literal)

  • Non-chronological backtracking (backjumping)

  • Lemma learning

  • Variable and phase selection

  • Garbage collection, restarts

CDCL: State [45]

  • $\mathcal{A}$: Atomic predicates $p, q, r, \ldots$

  • $\ell\in\mathcal{L}$: Literals over atoms $p, \overline{q}, \overline{q}, \ldots$

  • $M \subseteq \mathcal{L}$: Partial assignment without complementary literals.

  • $C$: A clause - disjunction of literals.

  • $\ell^d$: a decision literal.

  • $\ell^C$: a literal with explanation clause $C$, where $\ell$ is a disjunct in $C$. The literal $\ell$ is assigned relative to partial assignment $M$ when all other literals in $C$ occur negatively in $M$.

  • $F$: A set of clauses.

CDCL: Formal System [6]

\[\begin{array}{lllll} {\sf Initialize} & & \Longrightarrow & \twodpstate{}{F} & \mbox{$F$ is a set of clauses} \\ {\sf Decide} & \twodpstate{M}{F} & \Longrightarrow & \twodpstate{M\ell^d}{F} & \left\{ \begin{array}{l} \mbox{$\ell$ or $\neg{\ell}$ occurs in $F$} \\ \mbox{$\ell$ unassigned in $M$} \end{array} \right. \\ {\sf Propagate} & \twodpstate{M}{F, C \vee \ell} & \Longrightarrow & \twodpstate{M\ell^{C\vee\ell}}{F, C \vee \ell} & \left\{ \begin{array}{l} \mbox{$\ell$ unassigned in $M$}, \\ \compl{C} \subseteq M \end{array} \right. \\ {\sf Conflict} & \twodpstate{M}{F,C} \ & \Longrightarrow & \conflstate{M}{F,C}{C} & \mbox{ $C$ is false under $M$} \\ {\sf Resolve} & \conflstate{M}{F}{C'\vee \neg{\ell}} \ & \Longrightarrow & \conflstate{M}{F}{C \vee C'} & \ell^{C\vee \ell} \in M \\ {\sf Backjump} & \conflstate{M\ell_0^dM'}{F}{C \vee \ell} \ & \Longrightarrow & \twodpstate{M\ell^{C\vee\ell}}{F, C\vee \ell} & \compl{C}\subseteq M, \neg\ell \subseteq \ell_0^dM' \\ {\sf Restart} & \twodpstate{M}{F} & \Longrightarrow & \twodpstate{}{F} \\ {\sf Unsat} & \conflstate{M}{F}{\emptyset} & \Longrightarrow & {\tt unsat} \\ {\sf Sat} & \twodpstate{M}{F} & \Longrightarrow & M & \left\{ \begin{array}{l} \mbox{$M$ is $T$ consistent} \\ \mbox{and is a model for $F$.} \end{array} \right. \end{array} \]

CDCL(T)

\[\begin{array}{llllll} {\sf T-Propagate} & \twodpstate{M}{F} & \Longrightarrow & \twodpstate{M\ell^{C\vee\ell}}{F} & \left\{ \begin{array}{l} \mbox{$\ell$ unassigned in $M$} \\ \mbox{$\ell$ or $\neg{\ell}$ occurs in $F$} \\ \mbox{$T \vdash C \vee \ell$}\\ \compl{C} \subseteq M \end{array} \right. \\ {\sf T-Conflict} & \twodpstate{M}{F} & \Longrightarrow & \conflstate{M}{F}{C} & \compl{C} \subseteq M,\ T \models C. \end{array} \]

CDCL(T) Example

BasicTheory

Models and Proofs

Theorem 1.
For every $\Model$, exactly one of the two conditions hold:

  • $\Model' \models F$ for some $\Model'$ where $\Model\subseteq \Model'$.
  • $F \vdash_{\Pi} \overline{\Model'}$ for some $\Model'$ where $\Model'\subseteq\Model$ and some resolution proof $\Pi$.

Corollary 1.
$\exists \Model \ . \ \Model \models F \ \ \mbox{xor} \ \ \exists \Pi \ . \ F \vdash_{\Pi} \emptyset$

CDCL realizes the dichotomy by interleaving model and consequence finding:

Corollary 2.
If $F \vdash_{\Pi} C$, then for every $\Model$ where $\overline{C} \subseteq \Model$: $\Model \not\models F$.

Corollary 3.
If $\Model \models\neg F$, i.e., $\overline{C}\subseteq \Model$ for some $C \in F$, then for every consequence $D$ from $C$ using forced literals in $\Model$ it is the case that $\overline{D} \subseteq \Model$ and there is no $\Model' \supseteq \overline{D}$ such that $\Model'\models F$.

Realizing the dichotomy

Main invariants preserved by CDCL:

  • Conflict state: For the state $\conflstate{\Model}{F}{C}$ it is the case that $\overline{C} \subseteq \Model$ and $F \vdash C$.
  • Propagation: For the state $\searchstate{\Model}{F}$ and $\conflstate{\Model}{F}{D}$, whenever $\Model = \Model_1\ell^{C\vee\ell}\Model_2$, then $\overline{C} \subseteq \Model_1$ and $F \vdash_{\Pi} C \vee \ell$.

Illustrating the invariants

${\sf Backjump}:$

\[ \conflstate{M\ell_0^dM'}{F}{C \vee \ell} \ \Longrightarrow \twodpstate{M\ell^{C\vee\ell}}{F, C\vee \ell} \]

if $\compl{C}\subseteq M, \neg\ell \subseteq \ell_0^dM'$

  • Finds First Unique Implication Point (FUIP)
    • minimizes number of decision literals in $M$.
    • maximizes propagated literals in $M$

Theories

Equality and Uninterpreted functions

EUF

  (declare-sort A)
  (declare-fun f (A) A)
  (declare-const x A)
  (assert (= (f (f x)) x))
  (assert (= (f (f (f x))) x))
  (check-sat)
  
  (assert (not (= (f x) x)))
  (check-sat)

Deciding Equality

\begin{tikzpicture} \matrix[nodes={draw},row sep=0.3cm,column sep=0.5cm] { \node [rectangle, draw=none] (eq) {:}; & \node [circle, draw] (a) {$a$}; & \node [circle, draw] (b) {$b$}; & \node [circle, draw] (c) {$c$}; & \node [circle, draw] (d) {$d$}; & \node [circle, draw] (e) {$e$}; & \node [circle, draw] (s) {$s$}; & \node [circle, draw] (t) {$t$}; \\ }; \end{tikzpicture}
\begin{tikzpicture} \matrix[nodes={draw}, row sep=0.3cm,column sep=0.5cm] { \node [rectangle, draw=none] (eq) {$a = b: $}; & \node [circle, draw] (ab) {$a, b$}; & \node [circle, draw] (c) {$c$}; & \node [circle, draw] (d) {$d$}; & \node [circle, draw] (e) {$e$}; & \node [circle, draw] (s) {$s$}; & \node [circle, draw] (t) {$ t$}; \\ }; \end{tikzpicture}
\begin{tikzpicture} \matrix[nodes={draw}, row sep=0.3cm,column sep=0.5cm] { \node [rectangle, draw=none] (eq) {$a = b, b = c: $}; & \node [circle, draw] (abc) {$a, b, c$}; & \node [circle, draw] (d) {$d$}; & \node [circle, draw] (e) {$e$}; & \node [circle, draw] (s) {$s$}; & \node [circle, draw] (t) {$t$}; \\ }; \end{tikzpicture}
\begin{tikzpicture} \matrix[nodes={draw}, row sep=0.3cm,column sep=0.5cm] { \node [rectangle, draw=none] (eq) {$a = b, b = c, d = e: $}; & \node [circle, draw] (abc) {$a, b, c$}; & \node [circle, draw] (de) {$d, e$}; & \node [circle, draw] (s) {$s$}; & \node [circle, draw] (t) {$t$}; \\ }; \end{tikzpicture}
\begin{tikzpicture} \matrix[nodes={draw}, row sep=0.3cm,column sep=0.5cm] { \node [rectangle, draw=none] (eq) {$a = b, b = c, d = e, b = s: $}; & \node [circle, draw] (abcs) {$a, b, c, s$}; & \node [circle, draw] (de) {$d, e$}; & \node [circle, draw] (t) {$t$}; \\ }; \end{tikzpicture}
\begin{tikzpicture} \matrix[nodes={draw}, row sep=0.3cm,column sep=0.5cm] { \node [rectangle, draw=none] (eq) {$a = b, b = c, d = e, b = s, d = t: $}; & \node [circle, draw] (abcs) {$a, b, c, s$}; & \node [circle, draw] (det) {$d, e, t$}; \\ }; \end{tikzpicture}

Disequalities

\begin{tikzpicture} \matrix[nodes={draw}, row sep=0.3cm,column sep=0.5cm] { \node [rectangle, draw=none] (eq) {$a = b, b = c, d = e, b = s, d = t, a \neq d: $}; & \node [circle, draw] (abcs) {$a, b, c, s$}; & \node [circle, draw] (det) {$d, e, t$}; \\ }; \end{tikzpicture}
\begin{tikzpicture} \matrix[nodes={draw}, row sep=0.3cm,column sep=0.5cm] { \node [rectangle, draw=none] (eq) {$a = b, b = c, d = e, b = s, d = t, c \neq s: $}; & \node [circle, draw, color=red] (abcs) {$a, b, c, s$}; & \node [circle, draw] (det) {$d, e, t$}; \\ }; \end{tikzpicture}
\begin{tikzpicture} \matrix[nodes={draw}, row sep=0.3cm,column sep=0.5cm] { \node [rectangle, draw=none] (eq) {$a = b, b = c, d = e, b = s, d = t, e \neq t: $}; & \node [circle, draw] (abcs) {$a, b, c, s$}; & \node [circle, draw, color=red] (det) {$d, e, t$}; \\ }; \end{tikzpicture}

Variants of union-find are effective to decide equality.

Free functions

$a = b, b = c, d = e, b = s, d = t, f(a, g(d)) \neq f(b, g(e))$

Congruence rule

\[ x_1 = y_1 \cdots x_n = y_n \ \Rightarrow \ f(x_1, \ldots, x_n) = f(y_1, \ldots, y_n) \]

Naming sub-terms

$a = b, b = c, d = e, b = s, d = t, f(a, g(d)) \neq f(b, {\color{red}v_1})$ ${\color{red}v_1 := g(e)}$


$a = b, b = c, d = e, b = s, d = t, f(a, {\color{red}v_2}) \neq f(b, v_1)$ $v_1 := g(e), {\color{red}v_2 := g(d)}$


$a = b, b = c, d = e, b = s, d = t, {\color{red}v_3} \neq f(b, v_1)$ $v_1 := g(e), v_2 := g(d), {\color{red}v_3 := f(a, v_2)}$


$a = b, b = c, d = e, b = s, d = t, v_3 \neq {\color{red}v_4}$ $v_1 := g(e), v_2 := g(d), v_3 := f(a, v_2), {\color{red}v_4 := f(b, v_1)}$

\begin{tikzpicture} \matrix[nodes={draw}, row sep=0.3cm,column sep=0.5cm] { \node [circle, draw] (abcs) {$a, b, c, s$}; & \node [circle, draw] (det) {$d, e, t$}; & \node [circle, draw] (v1) {$v_1$}; & \node [circle, draw] (v2) {$v_2$}; & \node [circle, draw] (v3) {$v_3$}; & \node [circle, draw] (v4) {$v_4$}; \\ }; \end{tikzpicture}

Applying Congruence (1)

\[\begin{array}{l} a = b, b = c, d = e, b = s, d = t, v_3 \neq v_4 \\ v_1 := g(e), v_2 := g(d), v_3 := f(a, v_2), v_4 := f(b, v_1) \end{array} \]
\begin{tikzpicture} \matrix[nodes={draw}, row sep=0.3cm,column sep=0.5cm] { \node [circle, draw] (abcs) {$a, b, c, s$}; & \node [circle, draw] (det) {$d, e, t$}; & \node [circle, draw] (v1) {$v_1$}; & \node [circle, draw] (v2) {$v_2$}; & \node [circle, draw] (v3) {$v_3$}; & \node [circle, draw] (v4) {$v_4$}; \\ }; \end{tikzpicture}
\[ e = d \ \Rightarrow \ g(e) = g(d) \]
\begin{tikzpicture} \matrix[nodes={draw}, row sep=0.3cm,column sep=0.5cm] { \node [circle, draw] (abcs) {$a, b, c, s$}; & \node [circle, draw] (det) {$d, e, t$}; & \node [circle, draw, color=red] (v12) {$v_1, v_2$}; & \node [circle, draw] (v3) {$v_3$}; & \node [circle, draw] (v4) {$v_4$}; \\ }; \end{tikzpicture}

Applying Congruence (2)

\[\begin{array}{l} a = b, b = c, d = e, b = s, d = t, v_3 \neq v_4 \\ v_1 := g(e), v_2 := g(d), v_3 := f(a, v_2), v_4 := f(b, v_1) \end{array} \]

$a = b, b = c, d = e, b = s, d = t, f(a, g(d)) \neq f(b, g(e))$

\begin{tikzpicture} \matrix[nodes={draw}, row sep=0.3cm,column sep=0.5cm] { \node [circle, draw] (abcs) {$a, b, c, s$}; & \node [circle, draw] (det) {$d, e, t$}; & \node [circle, draw] (v12) {$v_1, v_2$}; & \node [circle, draw] (v3) {$v_3$}; & \node [circle, draw] (v4) {$v_4$}; \\ }; \end{tikzpicture}
\[ a = b, v_2 = v_1 \Rightarrow \ f(a, v_2) = f(b, v_1) \]
\begin{tikzpicture} \matrix[nodes={draw}, row sep=0.3cm,column sep=0.5cm] { \node [circle, draw] (abcs) {$a, b, c, s$}; & \node [circle, draw] (det) {$d, e, t$}; & \node [circle, draw] (v12) {$v_1, v_2$}; & \node [circle, draw, color=red] (v34) {$v_3, v_4$}; \\ }; \end{tikzpicture}

EUF Models

A satisfiable version:

$a = b, b = c, d = e, b = s, d = t, f(a, g(d)) \neq {\color{red}f(g(e), b)}$

$a = b, b = c, d = e, b = s, d = t, v_3 \neq v_4$
$v_1 := g(e), v_2 := g(d), v_3 := f(a, v_2), v_4 := f(v_1, b)$

\begin{tikzpicture} \matrix[nodes={draw}, row sep=0.3cm,column sep=0.5cm] { \node [circle, draw] (abcs) {$a, b, c, s$}; & \node [circle, draw] (det) {$d, e, t$}; & \node [circle, draw] (v12) {$v_1, v_2$}; & \node [circle, draw] (v3) {$v_3$}; & \node [circle, draw] (v4) {$v_4$}; \\ }; \end{tikzpicture}

EUF Models (II)

  • Associate a distinct value with each equivalence class.
\begin{tikzpicture} \matrix[nodes={draw}, row sep=0.3cm,column sep=0.5cm] { \node [circle, draw] (abcs) {$\diamond_1: a, b, c, s$}; & \node [circle, draw] (det) {$\diamond_2: d, e, t$}; & \node [circle, draw] (v12) {$\diamond_3: v_1, v_2$}; & \node [circle, draw] (v3) {$\diamond_4: v_3$}; & \node [circle, draw] (v4) {$\diamond_5: v_4$}; \\ }; \end{tikzpicture}
  • $M(a) = M(b) = M(c) = M(s) := \diamond_1$
  • $M(d) = M(e) = M(t) := \diamond_2$
  • $M(g) = \{ \diamond_1 \mapsto \diamond_3, \diamond_2 \mapsto \diamond_3, \mathrm{else} \mapsto \diamond_6 \}$
  • $M(f) = \{ (\diamond_1, \diamond_3) \mapsto \diamond_4, (\diamond_3, \diamond_2) \mapsto \diamond_5, \mathrm{else} \mapsto \diamond_7 \}$

Linear Arithmetic

Linear Arithmetic Example

(set-logic QF_IDL) ; optional in Z3
(declare-fun t11 () Int)
(declare-fun t12 () Int)
(declare-fun t21 () Int)
(declare-fun t22 () Int)
(declare-fun t31 () Int)
(declare-fun t32 () Int)

(assert (and (>= t11 0) (>= t12 (+ t11 2)) (<= (+ t12 1) 8)))
(assert (and (>= t21 0) (>= t22 (+ t21 3)) (<= (+ t22 1) 8)))
(assert (and (>= t31 0) (>= t32 (+ t31 2)) (<= (+ t32 3) 8)))
(assert (or (>= t11 (+ t21 3)) (>= t21 (+ t11 2))))
(assert (or (>= t11 (+ t31 2)) (>= t31 (+ t11 2))))
(assert (or (>= t21 (+ t31 2)) (>= t31 (+ t21 3))))
(assert (or (>= t12 (+ t22 1)) (>= t22 (+ t12 1))))
(assert (or (>= t12 (+ t32 3)) (>= t32 (+ t12 1))))
(assert (or (>= t22 (+ t32 3)) (>= t32 (+ t22 1))))
(check-sat)
(get-model) ; display the model  

Algorithmic Fragments of Arithmetic

Logic Fragment Solver Example
LRA Linear Real Arithmetic Dual Simplex $x + \frac{1}{2}y \leq 3$
LIA Linear Integer Arithmetic CutSat $a + 3b \leq 3$
LIRA Mixed Real/Integer Cuts + Branch $x + a \geq 4$
IDL Integer Difference Logic Floyd-Warshall $a - b \leq 4$
RDL Real Difference Logic Bellman-Ford
UTVPI Unit two-variable per inequality $x + y \leq 4$
NRA Polynomial Real Arithmetic Model based CAD $x^2 + y^2 < 1$

Other Fragments of Arithmetic

  • NIA - There is no decision procedure for integer polynomial constraints

    • Z3 falls back to incomplete heuristics
    • NIA over bounded integers may get translated to bit-vector constraints


    Theories, where Z3 falls back to general solvers:

  • Bi-linear real arithmetic

  • Non-unit two-variable per inequality

  • At most one unit positive variable per inequality (Horn)

Bellman-Ford

Solve difference logic using graph $O(m\cdot n)$ Bellman-Ford network flow algorithm. Negative cycle $\Rightarrow$ unsat.

BellmanFord

General form Simplex [21]

General form $Ax = 0$ and $lo_j \leq x_j \leq hi_j$

\[ x \geq 0, (x + y \leq 2 \vee x + 2y \geq 6), (x + y = 2 \vee x + 2y > 4) \]

$\leadsto$

\[\begin{mdmathpre}%mdk \mdmathindent{2}\mathid{s}_1~:=~\mathid{x}~+~\mathid{y},~\mathid{s}_2~:=~\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~=~2~\vee \mathid{s}_2~>~4) \end{mdmathpre}%mdk \]

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

From Definitions to a Tableau

${\color{red}s_1} := x + y, {\color{red}s_2} := x + 2y$



${\color{red}s_1} = x + y$
${\color{red}s_2} = x + 2y$



${\color{red}s_1} - x - y = 0$ - ${\color{red}s_1, s_2}$ are basic (dependent)
${\color{red}s_2} - x - 2y = 0$ - $x, y$ are non-basic

Pivoting

  • Value of non-basic variable $x_j$ can be chosen between $lo_j$ and $hi_j$.
  • Value of basic variable is a function of non-basic variable values.
  • Pivoting swaps basic and non-basic variables.
    • used to get values of basic variables within bounds.

Arrays

Arrays

; This example illustrates different uses of the arrays
; supported in Z3.
; This includes Combinatory Array Logic 
; (de Moura & Bjorner, FMCAD 2009).
;
(define-sort A () (Array Int Int))
(declare-fun x () Int)
(declare-fun y () Int)
(declare-fun z () Int)
(declare-fun a1 () A)
(declare-fun a2 () A)
(declare-fun a3 () A)
(push) ; illustrate select-store
(assert (= (select a1 x) x))
(assert (= (store a1 x y) a1))
(check-sat)
(get-model)
(assert (not (= x y)))
(check-sat)
(pop)
(define-fun all1_array () A ((as const A) 1))
(simplify (select all1_array x))
(define-sort IntSet () (Array Int Bool))
(declare-fun a () IntSet)
(declare-fun b () IntSet)
(declare-fun c () IntSet)
(push) ; illustrate map
(assert (not (= ((_ map and) a b) ((_ map not) ((_ map or) ((_ map not) b) ((_ map not) a))))))
(check-sat)
(pop)
(push) 
(assert (and (select ((_ map and) a b) x) (not (select a x))))
(check-sat)
(pop)
(push) 
(assert (and (select ((_ map or) a b) x) (not (select a x))))
(check-sat)
(get-model)
(assert (and (not (select b x))))
(check-sat)
;; unsat, so there is no model.
(pop)  
(push) ; illustrate default
(assert (= (default a1) 1))
(assert (not (= a1 ((as const A) 1))))  
(check-sat)
(get-model)
(assert (= (default a2) 1))
(assert (not (= a1 a2)))
(check-sat)
(get-model)
(pop)
(exit)    

Arrays as Combinators [42]

  A = Array(Index, Elem) # array sort 
  
  a[i]             # index array 'a' at index 'i'
                   # Select(a, i)
  
  Store(a, i, v)   # update array 'a' with value 'v' at index 'i'
                   # = lambda j: If(i == j, v, a[j])
    
  Const(v, A)      # constant array
                   # = lambda j: v
  
  Map(f, a)        # map function 'f' on values of 'a'
                   # = lambda j: f(a[j])

  Ext(a, b)        # Extensionality
                   # Implies(a[Ext(a, b)] == b[Ext(a, b)], a == b)

Array Decision Procedure

Example Store(a, i, v)

  • Each occurrence of Store(a, i, v) and b[j],

    • Assert Store(a, i, v)[j] == If(i == j, v, a[j])
    • Assert Store(a, i, v)[i] == v
  • Each shared occurrences of $a, b$:

    • Assert $a[\mbox{Ext}(a, b)] = b[\mbox{Ext}(a,b)] \ \implies \ a = b$.
  • Suppose we are given a model $M$ satisfying all asserted equalities.

    • $M$ assigns values to $a[i]\in \mathcal{T}$ terms.
    • Extend: $M(a) := \left[ M(i) \mapsto M(a[i])\; \mid\; a[i] \in \mathcal{T}; \ \mbox{else}\ \mapsto \diamond_{\mbox{default}} \right]$.
    • Claim: $M(a)$ satisfies Store axioms.

Efficient Array Decision Procedures

  • Use current partial interpretation to guide axiom instantiation.

  • Rough sketch:

    • If $u := Sore(a, i, v), w := b[j], u \sim b$ (congruent) in current state
      • Assert $i = j \vee u[j] = a[j]$.
    • If $u := Store(a, i, v), w := b[j], a \sim b$ in current state
      • Assert $i = j \vee Store(a, i, v)[j] = a[j]$
  • Also important to limit set of $i, j$ pairs.

    • Z3 uses relevancy propagation to prune don't care literals
    • Boolector uses dual propagation to extract small implicant

Bit-Vectors

Bit-Vectors

(define-fun is-power-of-two ((x (_ BitVec 4))) Bool 
  (= #x0 (bvand x (bvsub x #x1))))
(declare-const a (_ BitVec 4))
(assert 
 (not (= (is-power-of-two a) 
         (or (= a #x0) 
             (= a #x1) 
             (= a #x2) 
             (= a #x4) 
             (= a #x8)))))
(check-sat)

Floating Points

Floating point example

(declare-fun X () (_ FloatingPoint 11 53))

(assert (fp.isNormal X))
(assert (not (fp.isSubnormal X)))
(assert (not (fp.isZero X)))
(assert (not (fp.isInfinite X)))
(assert (not (fp.isNaN X)))
(assert (not (fp.isNegative X)))
(assert (fp.isPositive X))

(check-sat)
(get-model)

Sequences and Strings

Sequence Example

(declare-const a String)
(declare-const b String)
(declare-const c String)
(assert (str.prefixof b a))
(assert (str.suffixof c a))
(assert (= (str.len a) (+ (str.len b) (str.len c))))
(assert (not (= a (str.++ b c))))
(check-sat)  

Queues

\[\begin{mdmathpre}%mdk \mdmathindent{2}\mathid{xA}~=~\mathid{Bx}~\leftarrow \Gamma \\ \mdmathindent{6}\Rightarrow \mathid{A}~=~\mathid{B}_2\mathid{B}_1,~\mathid{ext}(\mathid{x},\mathid{B})~\leftarrow \Gamma,~\mathid{B}~=~\mathid{B}_1\mathid{B}_2\\ \\ \mdmathindent{2}\mathid{xA}~=~\mathid{By}~\leftarrow \Gamma\\ \mdmathindent{6}\Rightarrow \mathid{x}~=~\mathid{B}_1,~\mathid{A}~=~\mathid{B}_2\mathid{y}~\leftarrow \Gamma,~\mathid{B}~=~\mathid{B}_1\mathid{B}_2\\ \mdmathindent{6}\Rightarrow \mathid{y}~=~\mathid{A}_2,~\mathid{B}~=~\mathid{xA}_1~\leftarrow \Gamma,~\mathid{A}~=~\mathid{A}_1\mathid{A}_2\\ \mdmathindent{6}\Rightarrow \mathid{x}~=~\mathid{Bz},~\mathid{zA}~=~\mathid{y}~\leftarrow \Gamma,~\mathid{z}~\mathid{is}~\mathid{fresh}\\ \\ \mdmathindent{2}\mathid{ext}(\mathid{x},\mathid{A}),~\mathid{ext}(\mathid{x},\mathid{B})~\leftarrow \Gamma\\ \mdmathindent{6}\Rightarrow \mathid{compat}(\mathid{A},~\mathid{B},~|\mathid{x}|),~\mathid{ext}(\mathid{x},~\mathid{A})~\leftarrow \Gamma\\ \mdmathindent{5} \end{mdmathpre}%mdk \]

Algebraic Data-types

Non-linear Arithmetic

Decision Procedure Highlight [30]