Satisfiability Modulo Custom Theories in Z3 (Tool Paper)
summary
Z3 adds user-propagators: an API to register ground terms and attach callbacks (fixed, equality, instantiate, final) written in C++/Python that can emit lemmas, conflicts or branching hints back to Z3. It replaces eager quantifier axioms for many domains and speeds tasks dramatically — 60-queens propositional solve drops from ~2s/128MB to 60ms/90MB; minimal sorting-network synthesis shows 44h vs 150h. Works best for Booleans/BitVectors, currently limited for integers/strings, and proof generation remains unresolved.
AI-written summary · about
chapters (9)
- 0:00Start
- 0:30SMT solvers
- 4:51Q: How does it work?
- 6:29Q: How can the callbacks interfere?
- 12:50Conflict Driven Lazy Encoding
- 13:50Custom Heuristics
- 16:31Quantifier Instantiation: Sorting Networks
- 20:10Lazy Axiom Instantiation - A CS Flavoured Motivation
- 20:56Lazy Axiom Instantiation - Generalization for Program Verification
related talks
30mAnalyzing Programs with SMT Solvers
15mAssertion-Based Optimization of Quantum Programs
15mInter-theory Dependency Analysis for SMT String Solvers
15mTowards Proof Stability in SMT-based Program Verification
30mSemantics-Guided Synthesis
22mTurning Catala into a Proof Platform for the Law
41mLiving inside a Theorem Proving Universe
15mVerifying and Improving Halide’s Term Rewriting System with Program Synthesis