: An Efficient SMT Solver
1 Z3 uses novel algorithms for quantifier instantiation and theory combination. It has textual format ( , , something like ) and binary API (C, .NET, OCalm).
2 Z3 is based on -based SAT solver (core theory solver, for equalities and UF), satelite solvers (for arithmetic, arrays), E-matching abstract machine (for quantifiers). Implemented in C++.
3 Simplifier: fast incomplete simplification. Compiler: compile AST into a clauses and congruence-closure nodes. Congruence Colsure Core: E-graph (see ) 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 , bit-blasting. Model generation: model as a part of output.
Sergey Vartanov, 2007–2020