`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?