Skip to content

Latest commit

 

History

History
127 lines (117 loc) · 7.28 KB

README.md

File metadata and controls

127 lines (117 loc) · 7.28 KB
Raw

Schmitty the Solver

{-# OPTIONS --allow-exec #-}
{-# OPTIONS --guardedness #-}

open import Data.Integer
open import Data.List
open import Data.Product
open import Function
open import Relation.Binary.PropositionalEquality
open import SMT.Theories.Ints as Ints
open import SMT.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 ≡ y
verycool = solveZ3

So, basically, what Schmitty offers you is a well-typed embedding of some of the SMT-LIB language in Agda. That means you can't just 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's almost the script that our call to solveZ3 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, there must be a counter-example to our original goal!

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

Lucky us! It's very unsatisfiable… Wait, how did that work?! Did you just call Z3 while type checking?! Yes, dear reader, I did. You might’ve seen that I recently extended Agda with the execTC 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 that unsat 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 call get-model instead of check-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 that isn't true! We, uh… We do:

woops : ∀ (x y : ℤ) → x - y ≤ x + y → x ≡ y
woops = 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, and Reals—and two backends—Z3, and CVC4. If you’re missing your favourite theory or solver, your contribution is more than welcome!

Installation

Note that the path to z3 must be added to the list of trusted executables in Agda. See manual.

Roadmap

  • 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 to gallais/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 for combined theories (moderate);
  • Add support for logic declarations (moderate);
  • Add proof reconstruction for SAT using Kanso.Boolean.SatSolver (moderate);
  • Add proof reconstruction for Z3 proofs (cf. Proof Reconstruction for Z3 in Isabelle/HOL) (hard).