copilot-theorem: Copilot.Theorem.Prover.Z3 is dead code

[RyanGlScott]

The Copilot.Theorem.Prover.Z3 module has not included in the copilot-theorem.cabal file ever since 6a67d89, and as such, it is dead code. Moreover, the code has bitrotted since then, as trying to compile it with a modern version of copilot-theorem fails:

src/Copilot/Theorem/Prover/Z3.hs:27:1: error:
    Could not find module ‘Data.Unit’
    Perhaps you meant
      Data.Bit (needs flag -package-id bitvec-1.1.5.0)
      Data.Bit (needs flag -package-id bitvec-1.1.5.0)
      Data.Bit (needs flag -package-id bitvec-1.1.5.0)
    Use -v (or `:set -v` in ghci) to see a list of the files searched for.
   |
27 | import Data.Unit (Unit(..))
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^

src/Copilot/Theorem/Prover/Z3.hs:37:1: error:
    Could not find module ‘Language.SMTLib2’
    Use -v (or `:set -v` in ghci) to see a list of the files searched for.
   |
37 | import Language.SMTLib2
   | ^^^^^^^^^^^^^^^^^^^^^^^

src/Copilot/Theorem/Prover/Z3.hs:38:1: error:
    Could not find module ‘Language.SMTLib2.Pipe’
    Use -v (or `:set -v` in ghci) to see a list of the files searched for.
   |
38 | import Language.SMTLib2.Pipe
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^

src/Copilot/Theorem/Prover/Z3.hs:39:1: error:
    Could not find module ‘Language.SMTLib2.Connection’
    Use -v (or `:set -v` in ghci) to see a list of the files searched for.
   |
39 | import Language.SMTLib2.Connection
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

src/Copilot/Theorem/Prover/Z3.hs:40:1: error:
    Could not find module ‘Language.SMTLib2.Strategy’
    Use -v (or `:set -v` in ghci) to see a list of the files searched for.
   |
40 | import Language.SMTLib2.Strategy
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

src/Copilot/Theorem/Prover/Z3.hs:42:1: error:
    Could not find module ‘Language.SMTLib2.Internals’
    Use -v (or `:set -v` in ghci) to see a list of the files searched for.
   |
42 | import Language.SMTLib2.Internals hiding (Var)
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

src/Copilot/Theorem/Prover/Z3.hs:44:1: error:
    Could not load module ‘System.Console.ANSI’
    It is a member of the hidden package ‘ansi-terminal-1.1.2’.
    Perhaps you need to add ‘ansi-terminal’ to the build-depends in your .cabal file.
    It is a member of the hidden package ‘ansi-terminal-1.0.2’.
    Perhaps you need to add ‘ansi-terminal’ to the build-depends in your .cabal file.
    Use -v (or `:set -v` in ghci) to see a list of the files searched for.
   |
44 | import System.Console.ANSI
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^

[ivanperez-keera]

The following reveals that there are several examples that rely on that module:

$ grep -nHre 'Copilot.Theorem.Prover.Z3'  --include='*.cabal' --include='*.hs'
copilot-theorem/examples/Incr.hs:7:import Copilot.Theorem.Prover.Z3
copilot-theorem/examples/Grey.hs:7:import Copilot.Theorem.Prover.Z3
copilot-theorem/examples/SerialBoyerMoore.hs:7:import Copilot.Theorem.Prover.Z3
copilot-theorem/examples/SphericalWCV.hs:11:import Copilot.Theorem.Prover.Z3
copilot-theorem/examples/WCV.hs:8:import Copilot.Theorem.Prover.Z3
copilot-theorem/examples/BoyerMoore.hs:8:import Copilot.Theorem.Prover.Z3

Would those work out of the box with Copilot.Theorem.What4?

[RyanGlScott]

These wouldn't work out of the box with Copilot.Theorem.What4, if only because the API for Copilot.Theorem.Prover.Z3 is quite different from the API for Copilot.Theorem.What4. It's likely possible to migrate these examples from the former to the latter, but it would require some work to do so.

A potentially easier lift would be to migrate these examples from Copilot.Theorem.Prover.Z3 to Copilot.Theorem.Prover.SMT. As I understand it, the latter is the spiritual successor to the former, and it is possible to make the examples run by making relatively minor code changes:

Details

diff --git a/copilot-theorem/examples/BoyerMoore.hs b/copilot-theorem/examples/BoyerMoore.hs
index d4cebf63..505ec1e2 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

 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 9a1ca431..667922aa 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

 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 3c39a008..ba0feaec 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

 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 5f0d4209..a0e570d0 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

 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 74b89958..2fb54e19 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

 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 62c27f28..1bbd6fc8 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

 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

It's not straightforward to check that these changes preserve the original intent of these examples, partly because some of these examples lack Specs. This seems like it would be a good start, however.

[ivanperez-keera]

I converted this to a discussion to have a conversation first about what should happen. When we have a clear idea of what we need to do, we can file the necessary issues.

[RyanGlScott]

I still think that converting the examples over to Copilot.Theorem.Prover.SMT would be the wisest course of action. Is there enough of a consensus here to open a Copilot issue about this?

[RyanGlScott]

I've opened #692 for the task of porting the examples over to use Copilot.Theorem.Prover.SMT. As noted in #684 (comment), we want to defer the task of removing Copilot.Theorem.Prover.Z3 for later.