Repository files navigation

{-# OPTIONS --allow-exec #-}{-# OPTIONS --guardedness #-}open importData.Integeropen importData.Listopen importData.Productopen importFunctionopen importRelation.Binary.PropositionalEqualityopen importSMT.Theories.Ints as Intsopen importSMT.Backend.Z3 Ints.theory

If you wanna solve some problems, you’re in luck! Schmitty is an Agda library which gives you bindings to SMT solvers! I know, cool right?!

verycool:∀ (x y: ℤ)→ x ≤ y→ y ≤ x→ x ≡ yverycool= solveZ3

So, basically, what Schmitty offers you is a well-typed embedding ofsome of the SMT-LIB language in Agda. That means you can'tjust shout “solve” at your problems, you can also write SMT queries yourself!

blegh: Script [] (INT ∷ INT ∷ []) (SAT ∷ [])blegh= `declare-const"x" INT      $ `declare-const"y" INT      $ `assert (`app₂ leq (#0) (#1))      $ `assert (`app₂ leq (#1) (#0))      $ `assert (`app₁ not (`app₂ eq (#0) (#1)))      $ `check-sat      $ []

Ohh, that'salmost the script that our call tosolveZ3 above generates! What a lucky coincidence! You see, top-level constants are existentially quantified, so that script asks Z3 to see if∃[ x ] ∃[ y ] (x ≤ y → y ≤ x → x ≢ y) is satisfiable… and if it is, then, well, theremust be a counter-example to our original goal!

_: z3 blegh ≡ unsat ∷ []_= refl

Lucky us! It'svery unsatisfiable… Wait, how did that work?! Did you justcall Z3 while type checking?! Yes, dear reader, I did. You might’ve seen that I recently extended Agda with theexecTC primitive, which allows you to make arbitrary system calls during type checking… well, within reason at least. Schmitty lets you take the script above, print it as an SMT-LIB term, and pass it to Z3!

Did you pick up on thatunsat there? Schmitty doesn’t just give you back the solver’s output… she’s kind enough to actually parse the output for you! In fact, when Schmitty prints the term, she also builds you an output parser, which parses the expected solver output, including models! Let’s make sure our next query is satisfiable!

yesss: Script [] (INT ∷ INT ∷ []) (MODEL (INT ∷ INT ∷ []) ∷ [])yesss= `declare-const"x" INT      $ `declare-const"y" INT      $ `assert (`app₂ leq (`app₂ sub (#0) (#1)) (`app₂ add (#0) (#1)))      $ `assert (`app₁ not (`app₂ eq (#0) (#1)))      $ `get-model      $ []

If we callget-model instead ofcheck-sat, Schmitty will give us back a valid model!

_: z3 yesss ≡ ((sat , +1 ∷ +0 ∷ []) ∷ [])_= refl

Okay, I know that wasn’t a particularly hard problem, but I was in a rush. Send me a pull-request if you’ve got more interesting questions for Schmitty!

Wait, we can get models? Cool! We could use that to get counter-examples, if you try to prove something thatisn't true! We, uh… We do:

woops:∀ (x y: ℤ)→ x - y ≤ x + y→ x ≡ ywoops= solveZ3-- > Found counter-example:--     x = + 1--     y = + 0--   refuting (z : + 1 ≤ + 1) → + 1 ≡ + 0--   when checking that the expression unquote solveZ3 has type--   (x y : ℤ) → x - y ≤ x + y → x ≡ y

Right now, Schmitty supports three theories—Core,Ints, andReals—and two backends—Z3, andCVC4. If you’re missing your favourite theory or solver, your contribution is more than welcome!

• agda (>=v2.6.2)
• agda-stdlib (>=v1.7)
• agdarsec (v0.5.0)

Note that the path toz3 must be added to the list of trusted executables in Agda. Seemanual.

• Issue: move theorems proved via SMT solvers into Prop or the Classical monad (moderate);
• Issue: only normalise closed subterms in error messages (moderate);
• Add error reporting to the parser (easy);
• Add backends for other SMT-LIB compliant solvers:(verit,bitwuzla,yices2,etc)
• Add theory of real arithmetic linked to Agda rational numbers (easy);
• Add theory of floating-point numbers linked to Agda floats (easy);
• Add theory of strings linked to Agda strings (easy);
• Add theory of sequences linked to Agda lists (moderate);
• Add theory of uninterpreted functions and constants linked to Agda names (moderate);
• Add theory of regular expressions linked togallais/aGdaREP (moderate);
• Add theory of algebraic datatypes linked to Agda datatypes (moderate);
• Add theory of arrays linked to an axiomatisation of Haskell arrays (moderate);
• Add support forcombined theories (moderate);
• Add support forlogic declarations (moderate);
• Add proof reconstruction for SAT usingKanso.Boolean.SatSolver (moderate);
• Add proof reconstruction forZ3 proofs (cf.Proof Reconstruction for Z3 in Isabelle/HOL) (hard).