A Bounded Model Checker For The Existential Theory of the Reals With Exp And Trig
Macintyre's theorem says that the identities of (ℝ, exp) are exactly the laws
of an exponential ring — a commutative ring with a map E satisfying
E 0 = 1 and E (x+y) = E x · E y. The reals are therefore generic for
identities: if two terms agree over ℝ they agree in every exponential ring, and
so a disagreement in any exponential ring is a disagreement over ℝ.
We use this idea to build the operations (+, -, *, /, sqrt, exp, sin, cos) as
circuits over Z/2^w. That is a bounded model checker for the existential
theory of the reals, done over the 2-adic integers truncated to w bits instead
of over ℝ.
The solver
lake build lake exe fpsan --bmcwidth 8 tests/unsat/pythagorean.smt2 # "unsat", exits 20 ./tests/run.sh # the whole corpus
(set-logic QF_EXPRING) (declare-const x Real) (assert (not (= (+ (* (sin x) (sin x)) (* (cos x) (cos x))) 1))) (check-sat) ; unsat
Exit codes are SMT-LIB's: sat = 10, unsat = 20, unknown = 0, error 1.
--bmcwidth
Variables are declared at sort Real, and the file says nothing about a width.
The width of the finite proxy — the circuits run over Z/2^w — is a parameter
of the run:
fpsan --bmcwidth 8 q.smt2 # unsat fpsan --bmcwidth 16 q.smt2 # sat, for `2^8 * x = 0`
That is the bounded-model-checking discipline. A query asks about ℝ; the width
says which finite proxy to ask it in, and the same file is meant to be run at
several. Defaults to 32, the width fpsan.cpp uses, and the more discriminating
choice — a narrower proxy collapses more values and so admits more identities
that hold in Z/2^w and fail over ℝ.
Other flags: --timeout <seconds> (default 60) and --no-check.
The input language
QF_EXPRING. Commands: set-logic, declare-const, declare-fun,
define-fun, assert, check-sat, exit, and the ignorable
set-info/set-option/get-model. The only term sort is Real.
Terms are the ring operations + - * / and neg, the imaginary unit i,
conj, inv, the four circuits exp, sin, cos, sqrt, and chains of
recurrences: (scev-add n c0 c1 … ck) is the pure sum chain
{c0,+,c1,+,…,+,ck} at iteration n, (scev-mul n c0 c1 … ck) the pure
product chain, both zero-based as in LLVM, and (binom i n) is C(n, i). They
also accept let (parallel, as SMT-LIB specifies), (! e :named g)
annotations, numerals in decimal or as #b1010 / #xff, and term-level
(ite cond a b) where cond is any formula. Formulas additionally accept ite
and xor.
(declare-const n Real) (declare-const a Real) (declare-const b Real) (declare-const c Real) (declare-const d Real) (assert (not (= (+ (scev-add n a b) (scev-add n c d)) ; {a,+,b} + {c,+,d} (scev-add n (+ a c) (+ b d))))) ; = {a+c,+,b+d} (check-sat) ; unsat, symbolic n, no SAT call
The chain equivalences of the Chains of Recurrences paper — every relational
lemma of SCEV-coq — decide this way: a chain is rewritten to its binomial
closed form and ring normalisation does the rest. A chain at a symbolic
iteration that the rewrite cannot settle is refused with a message saying so,
since it has no bit-level circuit to fall back to.
The term language and the formula language are one inductive indexed by a kind,
which is what lets a term-level ite take an arbitrary condition —
(ite (and (= x 0) (= y 0)) a b) rather than only an equation.
(_ BitVec n) and (_ bv7 8) are rejected rather than accepted and ignored,
each with a message naming the flag. Both encode a width, and a file written
with one means a specific width — silently running it at whatever
--bmcwidth says would answer a different question from the one its author
wrote.
One sort, and what a variable is
Every term denotes a GaussianBV w, a pair over Z/2^w, so i is the value
⟨0,1⟩ and Euler's formula is expressible in the object language. sin, cos,
sqrt and exp take the real part of their argument and return ⟨_, 0⟩,
which keeps every operation total with no side conditions. A free variable is real.
Equisatisfiability
We prove the translation equisatisfiable, in both directions
(denote_eq_false_of_unsat, denote_eq_true_of_sat). We prove every rewrite
pass meaning-preserving, so a query decided by rewriting never reaches a SAT
solver at all — and on this corpus that is most of them.
An unsat has its LRAT certificate replayed by verifyCert, and a sat has
its model reconstructed and then evaluated against the original formula by our
own semantics. These checks can be disabled with --no-check.
Additionally, we take as axiom the fact that if two circuits agree on the free exponential
ring, which we just take to be the reals, then they agree on any exponential
ring. This is the content of Macintyre 1981, it is Fpsan/Model.lean.