From 0efbcb8cb41b859ae1212008050f487b45686e75 Mon Sep 17 00:00:00 2001 From: Chris Hathhorn Date: Tue, 31 Mar 2026 11:46:52 -0500 Subject: [PATCH 1/2] copilot-theorem: update examples to work with latest version. Refs #692. Some example programs in the copilot-theorem/example subdirectory have bitrotted, as they depend on a Copilot.Theorem.Prover.Z3 module that is no longer included in copilot-theorem.cabal (as of 6a67d89). Attempting to build any of these examples results in compilation failures. This commit fixes the examples so they will compile using the current version of copilot-theorem. --- copilot-theorem/examples/BoyerMoore.hs | 4 ++-- copilot-theorem/examples/Grey.hs | 6 +++--- copilot-theorem/examples/Incr.hs | 4 ++-- copilot-theorem/examples/SerialBoyerMoore.hs | 6 +++--- copilot-theorem/examples/SphericalWCV.hs | 6 +++--- copilot-theorem/examples/WCV.hs | 6 +++--- 6 files changed, 16 insertions(+), 16 deletions(-) diff --git a/copilot-theorem/examples/BoyerMoore.hs b/copilot-theorem/examples/BoyerMoore.hs index d4cebf638..572673b10 100644 --- a/copilot-theorem/examples/BoyerMoore.hs +++ b/copilot-theorem/examples/BoyerMoore.hs @@ -5,7 +5,7 @@ module BoyerMoore where import Copilot.Language hiding (length) import Copilot.Theorem -import Copilot.Theorem.Prover.Z3 +import Copilot.Theorem.Prover.SMT (induction, def, debug, z3) import Copilot.Core.Type @@ -71,7 +71,7 @@ spec = do maj = majorityVote ss induct :: Proof Universal -induct = induction def { nraNLSat = False, debug = False } +induct = induction def { debug = False } z3 -- | Initial value for a given type. -- diff --git a/copilot-theorem/examples/Grey.hs b/copilot-theorem/examples/Grey.hs index 9a1ca4319..6a87864d8 100644 --- a/copilot-theorem/examples/Grey.hs +++ b/copilot-theorem/examples/Grey.hs @@ -4,7 +4,7 @@ module Grey where import Copilot.Language import Copilot.Theorem -import Copilot.Theorem.Prover.Z3 +import Copilot.Theorem.Prover.SMT (def, Options (..), z3, kInduction, induction) import Prelude () import Data.String (fromString) @@ -32,7 +32,7 @@ spec = do r = extern "reset" Nothing induct :: Proof Universal -induct = induction def { nraNLSat = False, debug = False } +induct = induction def { debug = False } z3 kinduct :: Word32 -> Proof Universal -kinduct k = kInduction def { nraNLSat = False, startK = k, maxK = k, debug = False } +kinduct k = kInduction def { startK = k, maxK = k, debug = False } z3 diff --git a/copilot-theorem/examples/Incr.hs b/copilot-theorem/examples/Incr.hs index 3c39a008d..cb028df6e 100644 --- a/copilot-theorem/examples/Incr.hs +++ b/copilot-theorem/examples/Incr.hs @@ -4,7 +4,7 @@ import Prelude () import Copilot.Language import Copilot.Theorem -import Copilot.Theorem.Prover.Z3 +import Copilot.Theorem.Prover.SMT (def, induction, debug, z3) spec = do bounds <- prop "bounds" (forAll $ x < 255) @@ -16,4 +16,4 @@ spec = do x = [2] ++ (1 + x) induct :: Proof Universal -induct = induction def { nraNLSat = False, debug = True } +induct = induction def { debug = True } z3 diff --git a/copilot-theorem/examples/SerialBoyerMoore.hs b/copilot-theorem/examples/SerialBoyerMoore.hs index 5f0d42092..8b4ebdf9e 100644 --- a/copilot-theorem/examples/SerialBoyerMoore.hs +++ b/copilot-theorem/examples/SerialBoyerMoore.hs @@ -4,7 +4,7 @@ module SerialBoyerMoore where import Copilot.Language import Copilot.Theorem -import Copilot.Theorem.Prover.Z3 +import Copilot.Theorem.Prover.SMT (def, Options (..), induction, kInduction, z3) import Prelude () import Data.String (fromString) @@ -56,7 +56,7 @@ spec = do (p, s, j) = majority input induct :: Proof Universal -induct = induction def { nraNLSat = False, debug = False } +induct = induction def { debug = False } z3 kinduct :: Word32 -> Proof Universal -kinduct k = kInduction def { nraNLSat = False, startK = k, maxK = k, debug = False } +kinduct k = kInduction def { startK = k, maxK = k, debug = False } z3 diff --git a/copilot-theorem/examples/SphericalWCV.hs b/copilot-theorem/examples/SphericalWCV.hs index 74b899583..e1d128a30 100644 --- a/copilot-theorem/examples/SphericalWCV.hs +++ b/copilot-theorem/examples/SphericalWCV.hs @@ -8,7 +8,7 @@ import Prelude () import Copilot.Language import Copilot.Language.Reify import Copilot.Theorem -import Copilot.Theorem.Prover.Z3 +import Copilot.Theorem.Prover.SMT (def, debug, onlySat, onlyValidity, z3) import qualified Copilot.Language.Operators.Propositional as P @@ -241,7 +241,7 @@ localConvexity = do theorem "6" (P.not (forAll $ locallyConvex tau)) arithSat arith :: Proof Universal -arith = onlyValidity def { nraNLSat = True, debug = False } +arith = onlyValidity def { debug = False } z3 arithSat :: Proof Existential -arithSat = onlySat def { nraNLSat = True, debug = False } +arithSat = onlySat def { debug = False } z3 diff --git a/copilot-theorem/examples/WCV.hs b/copilot-theorem/examples/WCV.hs index 62c27f287..8aa7f8b5e 100644 --- a/copilot-theorem/examples/WCV.hs +++ b/copilot-theorem/examples/WCV.hs @@ -5,7 +5,7 @@ import Prelude () import Copilot.Language import Copilot.Language.Reify import Copilot.Theorem -import Copilot.Theorem.Prover.Z3 +import Copilot.Theorem.Prover.SMT (def, debug, onlySat, onlyValidity, z3) import qualified Copilot.Language.Operators.Propositional as P @@ -165,7 +165,7 @@ localConvexity = do theorem "6" (P.not (forAll $ locallyConvex tau)) arithSat arith :: Proof Universal -arith = onlyValidity def { nraNLSat = True, debug = False } +arith = onlyValidity def { debug = False } z3 arithSat :: Proof Existential -arithSat = onlySat def { nraNLSat = True, debug = False } +arithSat = onlySat def { debug = False } z3 From 06c4beff67fd2c8d58d66f4d0cf8e90aa4eac2fe Mon Sep 17 00:00:00 2001 From: Chris Hathhorn Date: Tue, 31 Mar 2026 12:31:53 -0500 Subject: [PATCH 2/2] copilot-theorem: Document changes in CHANGELOG. Refs #692. --- copilot-theorem/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-theorem/CHANGELOG b/copilot-theorem/CHANGELOG index 4aaf2cf97..39dbdc4af 100644 --- a/copilot-theorem/CHANGELOG +++ b/copilot-theorem/CHANGELOG @@ -1,3 +1,6 @@ +2026-03-31 + * Fix examples so they compile with latest copilot-theorem. (#692) + 2026-03-07 * Version bump (4.7). (#714)