Add What4 provers alongside the SBV provers with names such as w4-z3,

`w4-yices`, etc.  Implement What4 based "offline" solving using
the pseudo-solver name `w4-offline`.

src/Cryptol/REPL/Command.hs

@@ -7,6 +7,7 @@
 -- Portability :  portable
 
 {-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE MultiWayIf #-}
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE PatternGuards #-}
 {-# LANGUAGE RecordWildCards #-}
@@ -80,7 +81,7 @@ import Cryptol.Utils.Panic(panic)
 import qualified Cryptol.Parser.AST as P
 import qualified Cryptol.Transform.Specialize as S
 import Cryptol.Symbolic (ProverCommand(..), QueryType(..), SatNum(..),ProverStats,ProverResult(..))
---import qualified Cryptol.Symbolic.SBV as SBV
+import qualified Cryptol.Symbolic.SBV as SBV
 import qualified Cryptol.Symbolic.What4 as W4
 
 import qualified Control.Exception as X
@@ -106,7 +107,9 @@ import System.Directory(getHomeDirectory,setCurrentDirectory,doesDirectoryExist
 import Data.Map (Map)
 import qualified Data.Map as Map
 import qualified Data.Set as Set
-import System.IO(hFlush,stdout,openTempFile,hClose)
+import System.IO
+         (Handle,hFlush,stdout,openTempFile,hClose,openFile
+         ,IOMode(..),hGetContents,hSeek,SeekMode(..))
 import System.Random.TF(newTFGen)
 import Numeric (showFFloat)
 import qualified Data.Text as T
@@ -486,7 +489,7 @@ qcCmd qcMode str =
 -- may be generated multiple times.  If the test vectors were chosen
 -- randomly without replacement, the proportion would instead be @k/n@.
 --
--- We compute raising to the @k@ power in the log domain to improve 
+-- We compute raising to the @k@ power in the log domain to improve
 -- numerical precision. The equivalant comptutation is:
 --   @-expm1( k * log1p (-1/n) )@
 --
@@ -557,67 +560,53 @@ cmdProveSat isSat str = do
   proverName <- getKnownUser "prover"
   fileName   <- getKnownUser "smtfile"
   let mfile = if fileName == "-" then Nothing else Just fileName
-  case proverName :: String of
-    "offline" -> do
-      result <- offlineProveSat isSat str mfile
-      case result of
-        Left msg -> rPutStrLn msg
-        Right smtlib -> do
-          let filename = fromMaybe "standard output" mfile
-          let satWord | isSat = "satisfiability"
-                      | otherwise = "validity"
-          rPutStrLn $
-              "Writing to SMT-Lib file " ++ filename ++ "..."
-          rPutStrLn $
-            "To determine the " ++ satWord ++
-            " of the expression, use an external SMT solver."
-          case mfile of
-            Just path -> io $ writeFile path smtlib
-            Nothing -> rPutStr smtlib
-    _ -> do
-      (firstProver,result,stats) <- rethrowErrorCall (onlineProveSat isSat str mfile)
-      case result of
-        EmptyResult         ->
-          panic "REPL.Command" [ "got EmptyResult for online prover query" ]
-        ProverError msg     -> rPutStrLn msg
-        ThmResult ts        -> do
-          rPutStrLn (if isSat then "Unsatisfiable" else "Q.E.D.")
-          (t, e) <- mkSolverResult cexStr (not isSat) (Left ts)
-          bindItVariable t e
-        AllSatResult tevss -> do
-          let tess = map (map $ \(t,e,_) -> (t,e)) tevss
-              vss  = map (map $ \(_,_,v) -> v)     tevss
-          resultRecs <- mapM (mkSolverResult cexStr isSat . Right) tess
-          let collectTes tes = (t, es)
-                where
-                  (ts, es) = unzip tes
-                  t = case nub ts of
-                        [t'] -> t'
-                        _ -> panic "REPL.Command.onlineProveSat"
-                               [ "satisfying assignments with different types" ]
-              (ty, exprs) =
-                case resultRecs of
-                  [] -> panic "REPL.Command.onlineProveSat"
-                          [ "no satisfying assignments after mkSolverResult" ]
-                  [(t, e)] -> (t, [e])
-                  _        -> collectTes resultRecs
-          pexpr <- replParseExpr str
 
-          ~(EnvBool yes) <- getUser "show-examples"
-          when yes $ forM_ vss (printCounterexample isSat pexpr)
+  if proverName `elem` ["offline","w4-offline"] then
+     offlineProveSat proverName isSat str mfile
+  else
+     do (firstProver,result,stats) <- rethrowErrorCall (onlineProveSat proverName isSat str mfile)
+        case result of
+          EmptyResult         ->
+            panic "REPL.Command" [ "got EmptyResult for online prover query" ]
+          ProverError msg     -> rPutStrLn msg
+          ThmResult ts        -> do
+            rPutStrLn (if isSat then "Unsatisfiable" else "Q.E.D.")
+            (t, e) <- mkSolverResult cexStr (not isSat) (Left ts)
+            bindItVariable t e
+          AllSatResult tevss -> do
+            let tess = map (map $ \(t,e,_) -> (t,e)) tevss
+                vss  = map (map $ \(_,_,v) -> v)     tevss
+            resultRecs <- mapM (mkSolverResult cexStr isSat . Right) tess
+            let collectTes tes = (t, es)
+                  where
+                    (ts, es) = unzip tes
+                    t = case nub ts of
+                          [t'] -> t'
+                          _ -> panic "REPL.Command.onlineProveSat"
+                                 [ "satisfying assignments with different types" ]
+                (ty, exprs) =
+                  case resultRecs of
+                    [] -> panic "REPL.Command.onlineProveSat"
+                            [ "no satisfying assignments after mkSolverResult" ]
+                    [(t, e)] -> (t, [e])
+                    _        -> collectTes resultRecs
+            pexpr <- replParseExpr str
 
-          case (ty, exprs) of
-            (t, [e]) -> bindItVariable t e
-            (t, es ) -> bindItVariables t es
+            ~(EnvBool yes) <- getUser "show-examples"
+            when yes $ forM_ vss (printCounterexample isSat pexpr)
 
-      seeStats <- getUserShowProverStats
-      when seeStats (showProverStats firstProver stats)
+            case (ty, exprs) of
+              (t, [e]) -> bindItVariable t e
+              (t, es ) -> bindItVariables t es
 
-onlineProveSat :: Bool
+        seeStats <- getUserShowProverStats
+        when seeStats (showProverStats firstProver stats)
+
+onlineProveSat :: String
+               -> Bool
                -> String -> Maybe FilePath
                -> REPL (Maybe String,ProverResult,ProverStats)
-onlineProveSat isSat str mfile = do
-  proverName <- getKnownUser "prover"
+onlineProveSat proverName isSat str mfile = do
   verbose <- getKnownUser "debug"
   satNum <- getUserSatNum
   modelValidate <- getUserProverValidate
@@ -638,12 +627,16 @@ onlineProveSat isSat str mfile = do
         , pcExpr         = expr
         , pcSchema       = schema
         }
-  (firstProver, res) <- liftModuleCmd $ W4.satProve cmd
+  (firstProver, res) <-
+     if | proverName `elem` W4.proverNames  -> liftModuleCmd $ W4.satProve cmd
+        | proverName `elem` SBV.proverNames -> liftModuleCmd $ SBV.satProve cmd
+        | otherwise -> panic "onlineProveSat" ["unexpected prover name", proverName]
+
   stas <- io (readIORef timing)
   return (firstProver,res,stas)
 
-offlineProveSat :: Bool -> String -> Maybe FilePath -> REPL (Either String String)
-offlineProveSat isSat str mfile = do
+offlineProveSat :: String -> Bool -> String -> Maybe FilePath -> REPL ()
+offlineProveSat proverName isSat str mfile = do
   verbose <- getKnownUser "debug"
   modelValidate <- getUserProverValidate
   parseExpr <- replParseExpr str
@@ -652,7 +645,7 @@ offlineProveSat isSat str mfile = do
   timing <- io (newIORef 0)
   let cmd = ProverCommand {
           pcQueryType    = if isSat then SatQuery (SomeSat 0) else ProveQuery
-        , pcProverName   = "offline"
+        , pcProverName   = proverName
         , pcVerbose      = verbose
         , pcValidate     = modelValidate
         , pcProverStats  = timing
@@ -661,7 +654,47 @@ offlineProveSat isSat str mfile = do
         , pcExpr         = expr
         , pcSchema       = schema
         }
-  liftModuleCmd $ W4.satProveOffline cmd
+
+  put <- getPutStr
+  let putLn x = put (x ++ "\n")
+  let displayMsg =
+        do let filename = fromMaybe "standard output" mfile
+           let satWord | isSat = "satisfiability"
+                       | otherwise = "validity"
+           putLn $
+               "Writing to SMT-Lib file " ++ filename ++ "..."
+           putLn $
+             "To determine the " ++ satWord ++
+             " of the expression, use an external SMT solver."
+
+  case proverName of
+    "offline" ->
+      do result <- liftModuleCmd $ SBV.satProveOffline cmd
+         case result of
+           Left msg -> rPutStrLn msg
+           Right smtlib -> do
+             io $ displayMsg
+             case mfile of
+               Just path -> io $ writeFile path smtlib
+               Nothing -> rPutStr smtlib
+
+    "w4-offline" ->
+      do result <- liftModuleCmd $ W4.satProveOffline cmd $ \f ->
+                     do displayMsg
+                        case mfile of
+                          Just path ->
+                            X.bracket (openFile path WriteMode) hClose f
+                          Nothing ->
+                            withRWTempFile "smtOutput.tmp" $ \h ->
+                              do f h
+                                 hSeek h AbsoluteSeek 0
+                                 hGetContents h >>= put
+
+         case result of
+           Just msg -> rPutStrLn msg
+           Nothing -> return ()
+
+    _ -> panic "offlineProveSat" ["unexpected offline solver name", proverName]
 
 rIdent :: M.Ident
 rIdent  = M.packIdent "result"
@@ -844,6 +877,15 @@ editCmd path =
        _ <- replEdit p
        reloadCmd
 
+withRWTempFile :: String -> (Handle -> IO a) -> IO a
+withRWTempFile name k =
+  X.bracket
+    (do tmp <- getTemporaryDirectory
+        let esc c = if isAscii c && isAlphaNum c then c else '_'
+        openTempFile tmp (map esc name))
+    (\(nm,h) -> hClose h >> removeFile nm)
+    (k . snd)
+
 withROTempFile :: String -> ByteString -> (FilePath -> REPL a) -> REPL a
 withROTempFile name cnt k =
   do (path,h) <- mkTmp

src/Cryptol/REPL/Monad.hs

@@ -95,8 +95,8 @@ import Cryptol.Utils.Panic (panic)
 import Cryptol.Utils.Logger(Logger, logPutStr, funLogger)
 import qualified Cryptol.Parser.AST as P
 import Cryptol.Symbolic (SatNum(..))
---import qualified Cryptol.Symbolic.SBV as SBV (proverNames, checkProverInstallation)
-import qualified Cryptol.Symbolic.What4 as W4 (proverNames, checkProverInstallation)
+import qualified Cryptol.Symbolic.SBV as SBV (proverNames, checkProverInstallation)
+import qualified Cryptol.Symbolic.What4 as W4 (proverNames)
 
 import Control.Monad (ap,unless,when)
 import Control.Monad.Base
@@ -794,20 +794,27 @@ checkInfLength val = case val of
 checkProver :: Checker
 checkProver val = case val of
   EnvString s
-    | s `notElem` W4.proverNames ->
-      noWarns $ Just $ "Prover must be " ++ proverListString
-    | s `elem` ["offline", "any"] -> noWarns Nothing
-    | otherwise ->
-      do available <- W4.checkProverInstallation s
+    | s `elem` ["offline", "any", "w4-offline"] -> noWarns Nothing
+    | s `elem` W4.proverNames ->
+      do -- TODO! Implement solver installation testing for What4
+         return (Nothing, [])
+    | s `elem` SBV.proverNames ->
+      do available <- SBV.checkProverInstallation s
          let ws = if available
                      then []
                      else ["Warning: " ++ s ++ " installation not found"]
          return (Nothing, ws)
 
+    | otherwise ->
+      noWarns $ Just $ "Prover must be " ++ proverListString
+
   _ -> noWarns $ Just "unable to parse a value for prover"
 
+allProvers :: [String]
+allProvers = SBV.proverNames ++ W4.proverNames
+
 proverListString :: String
-proverListString = concatMap (++ ", ") (init W4.proverNames) ++ "or " ++ last W4.proverNames
+proverListString = concatMap (++ ", ") (init allProvers) ++ "or " ++ last allProvers
 
 checkSatNum :: Checker
 checkSatNum val = case val of
@@ -861,4 +868,3 @@ z3exists = do
   case mPath of
     Nothing -> return (Just Z3NotFound)
     Just _  -> return Nothing
-

src/Cryptol/Symbolic/What4.hs

@@ -19,19 +19,18 @@
 
 module Cryptol.Symbolic.What4
  ( proverNames
- , checkProverInstallation
+-- , checkProverInstallation
  , satProve
  , satProveOffline
  ) where
 
 import Control.Monad.IO.Class
 import Control.Monad (when, foldM)
---import Control.Monad.Writer (WriterT, runWriterT, tell, lift)
---import Data.List (intercalate, genericLength)
 import qualified Data.Map as Map
---import Data.IORef(IORef)
 import qualified Control.Exception as X
---import Data.Maybe (fromMaybe)
+import System.IO (Handle)
+import Data.Time
+import Data.IORef
 
 import qualified Cryptol.ModuleSystem as M hiding (getPrimMap)
 import qualified Cryptol.ModuleSystem.Env as M
@@ -40,17 +39,12 @@ import qualified Cryptol.ModuleSystem.Monad as M
 
 import qualified Cryptol.Eval as Eval
 import qualified Cryptol.Eval.Concrete as Concrete
---import           Cryptol.Eval.Concrete (Concrete(..))
---import qualified Cryptol.Eval.Monad as Eval
---import           Cryptol.Eval.Type (TValue(..), evalType)
 
 import qualified Cryptol.Eval.Value as Eval
 import           Cryptol.Eval.What4
 import           Cryptol.Symbolic
 import           Cryptol.TypeCheck.AST
 import           Cryptol.Utils.Ident (Ident)
---import           Cryptol.Utils.PP
-import           Cryptol.Utils.Panic(panic)
 import           Cryptol.Utils.Logger(logPutStrLn)
 
 import qualified What4.Config as W4
@@ -61,9 +55,6 @@ import qualified What4.SatResult as W4
 import qualified What4.SWord as SW
 import           What4.Solver
 import qualified What4.Solver.Adapter as W4
---import qualified What4.Solver.Z3 as Z3
---import qualified What4.Solver.Yices as Yices
---import qualified What4.Solver.CVC4 as CVC4
 
 import           Data.Parameterized.Nonce
 
@@ -86,14 +77,14 @@ doW4Eval sym evo m =
 
 proverConfigs :: [(String, SolverAdapter st)]
 proverConfigs =
-  [ ("cvc4"     , cvc4Adapter )
-  , ("yices"    , yicesAdapter )
-  , ("z3"       , z3Adapter )
-  , ("boolector", boolectorAdapter )
+  [ ("w4-cvc4"     , cvc4Adapter )
+  , ("w4-yices"    , yicesAdapter )
+  , ("w4-z3"       , z3Adapter )
+  , ("w4-boolector", boolectorAdapter )
+  , ("w4-offline"  , z3Adapter )
 {-
   , ("mathsat"  , SBV.mathSAT  )
   , ("abc"      , SBV.abc      )
-  , ("offline"  , SBV.defaultSMTCfg )
   , ("any"      , SBV.defaultSMTCfg )
 -}
   ]
@@ -107,10 +98,10 @@ lookupProver s =
    Just cfg -> pure cfg
    Nothing  -> fail ("Invalid prover: " ++ s)
 
-checkProverInstallation :: String -> IO Bool
-checkProverInstallation s =
-  do putStrLn "TODO! What4 check solver installation"
-     return True
+--checkProverInstallation :: String -> IO Bool
+--checkProverInstallation _s =
+--  do putStrLn "TODO! What4 check solver installation"
+--     return True
 
 proverError :: String -> M.ModuleCmd (Maybe String, ProverResult)
 proverError msg (_,modEnv) =
@@ -142,21 +133,22 @@ satProve ProverCommand {..} =
             , logReason = "solver query"
             }
 
+    start <- liftIO $ getCurrentTime
+
     let ?evalPrim = evalPrim sym
     case predArgTypes pcSchema of
       Left msg -> return (Nothing, ProverError msg)
       Right ts ->
-         do when pcVerbose $ lPutStrLn "Simulating..."
-
-            args <- liftIO $ mapM (freshVariable sym) ts
+         when pcVerbose (lPutStrLn "Simulating...") >> liftIO (
+         do args <- mapM (freshVariable sym) ts
 
             (safety,b) <-
-               liftIO $ doW4Eval sym evo $
+               doW4Eval sym evo $
                    do env <- Eval.evalDecls (What4 sym) extDgs mempty
                       v <- Eval.evalExpr (What4 sym) env pcExpr
                       Eval.fromVBit <$> foldM Eval.fromVFun v (map (pure . varToSymValue sym) args)
 
-            liftIO $ case pcQueryType of
+            result <- case pcQueryType of
               ProveQuery ->
                 do q <- W4.notPred sym =<< W4.andPred sym safety b
                    singleQuery sym evo primMap pcProverName logData ts args q
@@ -165,6 +157,44 @@ satProve ProverCommand {..} =
                 do q <- W4.andPred sym safety b
                    multiSATQuery sym evo primMap pcProverName logData ts args q num
 
+            end <- getCurrentTime
+            writeIORef pcProverStats (diffUTCTime end start)
+            return result)
+
+satProveOffline :: ProverCommand -> ((Handle -> IO ()) -> IO ()) -> M.ModuleCmd (Maybe String)
+satProveOffline ProverCommand {..} outputContinuation =
+  protectStack (\msg (_,modEnv) -> return (Right (Just msg, modEnv), [])) $
+  \(evo,modEnv) -> do
+  M.runModuleM (evo,modEnv) $ do
+    let extDgs = allDeclGroups modEnv ++ pcExtraDecls
+    let lPutStrLn = M.withLogger logPutStrLn
+
+    sym <- M.io (W4.newExprBuilder W4.FloatIEEERepr CryptolState globalNonceGenerator)
+
+    let ?evalPrim = evalPrim sym
+    case predArgTypes pcSchema of
+      Left msg -> return (Just msg)
+      Right ts ->
+         do when pcVerbose $ lPutStrLn "Simulating..."
+            liftIO $ do
+              args <- mapM (freshVariable sym) ts
+
+              (safety,b) <-
+                 doW4Eval sym evo $
+                     do env <- Eval.evalDecls (What4 sym) extDgs mempty
+                        v <- Eval.evalExpr (What4 sym) env pcExpr
+                        Eval.fromVBit <$> foldM Eval.fromVFun v (map (pure . varToSymValue sym) args)
+
+              q <- case pcQueryType of
+                ProveQuery ->
+                  W4.notPred sym =<< W4.andPred sym safety b
+                SatQuery _ ->
+                  W4.andPred sym safety b
+
+              let adpt = z3Adapter
+              W4.extendConfig (W4.solver_adapter_config_options adpt) (W4.getConfiguration sym)
+              outputContinuation (\hdl -> solver_adapter_write_smt2 adpt sym hdl [q])
+              return Nothing
 
 decSatNum :: SatNum -> SatNum
 decSatNum (SomeSat n) | n > 0 = SomeSat (n-1)
@@ -242,8 +272,9 @@ singleQuery ::
   [VarShape sym] ->
   W4.Pred sym ->
   IO (Maybe String, ProverResult)
-singleQuery sym evo primMap "all" logData ts args query =
-  do fail "TODO portfolio solver!"
+
+--singleQuery _sym _evo _primMap "all" _logData _ts _args _query =
+--  do fail "TODO portfolio solver!"
 
 singleQuery sym evo primMap solverName logData ts args query =
   do adpt <- lookupProver solverName
@@ -365,135 +396,6 @@ varToConcreteValue evalFn v =
 
 
 
-{-
-  let (isSat, mSatNum) = case pcQueryType of
-        ProveQuery -> (False, Nothing)
-        SatQuery sn -> case sn of
-          SomeSat n -> (True, Just n)
-          AllSat    -> (True, Nothing)
-
-  provers <-
-    case pcProverName of
-      "any" -> M.io SBV.sbvAvailableSolvers
-      _ -> return [(lookupProver pcProverName) { SBV.transcript = pcSmtFile
-                                               , SBV.allSatMaxModelCount = mSatNum
-                                               }]
-
-
-  let provers' = [ p { SBV.timing = SaveTiming pcProverStats
-                     , SBV.verbose = pcVerbose
-                     , SBV.validateModel = pcValidate
-                     } | p <- provers ]
-  let tyFn = if isSat then existsFinType else forallFinType
-
-  let runProver fn tag e = do
-        case provers of
-          [prover] -> do
-            when pcVerbose $
-              lPutStrLn $ "Trying proof with " ++
-                                        show (SBV.name (SBV.solver prover))
-            res <- M.io (fn prover e)
-            when pcVerbose $
-              lPutStrLn $ "Got result from " ++
-                                        show (SBV.name (SBV.solver prover))
-            return (Just (SBV.name (SBV.solver prover)), tag res)
-          _ ->
-            return ( Nothing
-                   , [ SBV.ProofError
-                         prover
-                         [":sat with option prover=any requires option satNum=1"]
-                         Nothing
-                     | prover <- provers ]
-                   )
-      runProvers fn tag e = do
-        when pcVerbose $
-          lPutStrLn $ "Trying proof with " ++
-                  intercalate ", " (map (show . SBV.name . SBV.solver) provers)
-        (firstProver, timeElapsed, res) <- M.io (fn provers' e)
-        when pcVerbose $
-          lPutStrLn $ "Got result from " ++ show firstProver ++
-                                            ", time: " ++ showTDiff timeElapsed
-        return (Just firstProver, tag res)
-  let runFn = case pcQueryType of
-        ProveQuery -> runProvers SBV.proveWithAny thmSMTResults
-        SatQuery sn -> case sn of
-          SomeSat 1 -> runProvers SBV.satWithAny satSMTResults
-          _         -> runProver SBV.allSatWith allSatSMTResults
-  let addAsm = case pcQueryType of
-        ProveQuery -> \x y -> SBV.svOr (SBV.svNot x) y
-        SatQuery _ -> \x y -> SBV.svAnd x y
-
- let ?evalPrim = evalPrim
-  case predArgTypes pcSchema of
-    Left msg -> return (Nothing, ProverError msg)
-    Right ts -> do when pcVerbose $ lPutStrLn "Simulating..."
-                   (_,v) <- doSBVEval evo $
-                              do env <- Eval.evalDecls SBV extDgs mempty
-                                 Eval.evalExpr SBV env pcExpr
-                   prims <- M.getPrimMap
-                   runRes <- runFn $ do
-                               (args, asms) <- runWriterT (mapM tyFn ts)
-                               (_,b) <- doSBVEval evo (Eval.fromVBit <$>
-                                          foldM Eval.fromVFun v (map pure args))
-                               return (foldr addAsm b asms)
-                   let (firstProver, results) = runRes
-                   esatexprs <- case results of
-                     -- allSat can return more than one as long as
-                     -- they're satisfiable
-                     (SBV.Satisfiable {} : _) -> do
-                       tevss <- mapM mkTevs results
-                       return $ AllSatResult tevss
-                       where
-                         mkTevs result = do
-                           let Right (_, cvs) = SBV.getModelAssignment result
-                               (vs, _) = parseValues ts cvs
-                               sattys = unFinType <$> ts
-                           satexprs <-
-                             doEval evo (zipWithM (Concrete.toExpr prims) sattys vs)
-                           case zip3 sattys <$> (sequence satexprs) <*> pure vs of
-                             Nothing ->
-                               panic "Cryptol.Symbolic.sat"
-                                 [ "unable to make assignment into expression" ]
-                             Just tevs -> return $ tevs
-                     -- prove returns only one
-                     [SBV.Unsatisfiable {}] ->
-                       return $ ThmResult (unFinType <$> ts)
-                     -- unsat returns empty
-                     [] -> return $ ThmResult (unFinType <$> ts)
-                     -- otherwise something is wrong
-                     _ -> return $ ProverError (rshow results)
-                            where rshow | isSat = show .  SBV.AllSatResult . (False,False,False,)
-                                        | otherwise = show . SBV.ThmResult . head
-                   return (firstProver, esatexprs)
--}
-
-satProveOffline :: ProverCommand -> M.ModuleCmd (Either String String)
-satProveOffline ProverCommand {..} =
-  protectStack (\msg (_,modEnv) -> return (Right (Left msg, modEnv), [])) $
-  \(_evOpts,_modEnv) -> do
-    fail "TODO! satProveOffline"
-{-
-    let isSat = case pcQueryType of
-          ProveQuery -> False
-          SatQuery _ -> True
-    let extDgs = allDeclGroups modEnv ++ pcExtraDecls
-    let tyFn = if isSat then existsFinType else forallFinType
-    let addAsm = if isSat then SBV.svAnd else \x y -> SBV.svOr (SBV.svNot x) y
-    let ?evalPrim = evalPrim
-    case predArgTypes pcSchema of
-      Left msg -> return (Right (Left msg, modEnv), [])
-      Right ts ->
-        do when pcVerbose $ logPutStrLn (Eval.evalLogger evOpts) "Simulating..."
-           (_,v) <- doSBVEval evOpts $
-                      do env <- Eval.evalDecls SBV extDgs mempty
-                         Eval.evalExpr SBV env pcExpr
-           smtlib <- SBV.generateSMTBenchmark isSat $ do
-             (args, asms) <- runWriterT (mapM tyFn ts)
-             (_,b) <- doSBVEval evOpts
-                          (Eval.fromVBit <$> foldM Eval.fromVFun v (map pure args))
-             return (foldr addAsm b asms)
-           return (Right (Right smtlib, modEnv), [])
--}
 
 protectStack :: (String -> M.ModuleCmd a)
              -> M.ModuleCmd a