## Z3: An Efficient SMT Solver

1 Z3 uses novel algorithms for quantifier instantiation and theory combination. It has textual format (SMT-LIB 2, Simplify, something like DIMACS) and binary API (C, .NET, OCalm).

2 Z3 is based on DPLL-based SAT solver (core theory solver, for equalities and UF), satelite solvers (for arithmetic, arrays), E-matching abstract machine (for quantifiers). Implemented in C++.

### Architecture

3 Simplifier: fast incomplete simplification. Compiler: compile AST into a clauses and congruence-closure nodes. Congruence Colsure Core: E-graph (see Simplify) propagates truth assignments receivde from the SAT solver. Theory combination. SAT solver: two-watch literals, lemma learning, conflict clauses, phase caching, non-chronological backtracking. Deleting clauses: they don't delete conflict clauses. Relevancy propagation: ignore atoms that don't care. 4 Quantifier instantiation using E-matching. Theory Solvers: linear arithmetic from Yices, bit-blasting. Model generation: model as a part of output.

Sergey Vartanov, 2007–2020