Add "boolector" and "mathsat" as possible prover settings.

Support for these provers was added in SBV version 3.

cryptol/REPL/Monad.hs

@@ -56,6 +56,7 @@ import qualified Cryptol.TypeCheck.AST as T
 import Cryptol.Utils.PP
 import Cryptol.Utils.Panic (panic)
 import qualified Cryptol.Parser.AST as P
+import Cryptol.Symbolic (proverNames)
 
 import Control.Monad (unless,when)
 import Data.IORef
@@ -382,8 +383,8 @@ userOptions  = mkOptionMap
     "The number of elements to display for infinite sequences."
   , OptionDescr "tests" (EnvNum 100) (const Nothing)
     "The number of random tests to try."
-  , OptionDescr "prover" (EnvString "cvc4") checkProver
-    "The external smt solver for :prove and :sat (cvc4, yices, or z3)."
+  , OptionDescr "prover" (EnvString "cvc4") checkProver $
+    "The external smt solver for :prove and :sat (" ++ proverListString ++ ")."
   , OptionDescr "iteSolver" (EnvBool False) (const Nothing)
     "Use smt solver to filter conditional branches in proofs."
   , OptionDescr "warnDefaulting" (EnvBool True) (const Nothing)
@@ -408,10 +409,13 @@ checkInfLength val = case val of
 checkProver :: EnvVal -> Maybe String
 checkProver val = case val of
   EnvString s
-    | s `elem` ["cvc4", "yices", "z3"] -> Nothing
-    | otherwise                        -> Just "prover must be cvc4, yices, or z3"
+    | s `elem` proverNames -> Nothing
+    | otherwise            -> Just $ "prover must be " ++ proverListString
   _ -> Just "unable to parse a value for prover"
 
+proverListString :: String
+proverListString = concatMap (++ ", ") (init proverNames) ++ "or " ++ last proverNames
+
 -- Environment Utilities -------------------------------------------------------
 
 whenDebug :: REPL () -> REPL ()

src/Cryptol/Symbolic.hs

@@ -40,11 +40,23 @@ import Cryptol.Utils.Panic(panic)
 
 -- External interface ----------------------------------------------------------
 
+proverConfigs :: [(String, SBV.SMTConfig)]
+proverConfigs =
+  [ ("cvc4"     , SBV.cvc4     )
+  , ("yices"    , SBV.yices    )
+  , ("z3"       , SBV.z3       )
+  , ("boolector", SBV.boolector)
+  , ("mathsat"  , SBV.mathSAT  )
+  ]
+
+proverNames :: [String]
+proverNames = map fst proverConfigs
+
 lookupProver :: String -> SBV.SMTConfig
-lookupProver "cvc4"  = SBV.cvc4
-lookupProver "yices" = SBV.yices
-lookupProver "z3"    = SBV.z3
-lookupProver s       = error $ "invalid prover: " ++ s
+lookupProver s =
+  case lookup s proverConfigs of
+    Just cfg -> cfg
+    Nothing  -> error $ "invalid prover: " ++ s
 
 prove :: (String, Bool, Bool) -> (Expr, Schema) -> M.ModuleCmd (Either String (Maybe [Eval.Value]))
 prove (proverName, useSolverIte, verbose) (expr, schema) = protectStack useSolverIte $ \modEnv -> do