kore-exec: Add option --solver-reset-interval

kore/app/exec/Main.hs

@@ -2,6 +2,7 @@ module Main (main) where
 
 import Prelude.Kore
 
+import qualified Control.Lens as Lens
 import Control.Monad.Catch
     ( MonadMask
     , SomeException
@@ -10,11 +11,13 @@ import Control.Monad.Catch
     , throwM
     )
 import Control.Monad.Extra as Monad
-import qualified Data.Char as Char
 import Data.Default
     ( def
     )
 import qualified Data.Foldable as Foldable
+import Data.Generics.Product
+    ( field
+    )
 import Data.Limit
     ( Limit (..)
     , maybeLimit
@@ -35,6 +38,7 @@ import qualified Data.Text.IO as Text
     ( putStrLn
     , readFile
     )
+import qualified GHC.Generics as GHC
 import Options.Applicative
     ( InfoMod
     , Parser
@@ -160,6 +164,14 @@ import qualified Kore.Syntax.Definition as Definition.DoNotUse
 import Kore.Unparser
     ( unparse
     )
+import Options.SMT
+    ( KoreSolverOptions (..)
+    , Solver (..)
+    , ensureSmtPreludeExists
+    , parseKoreSolverOptions
+    , unparseKoreSolverOptions
+    , writeKoreSolverFiles
+    )
 import Pretty
     ( Doc
     , Pretty (..)
@@ -172,7 +184,6 @@ import Prof
     )
 import SMT
     ( MonadSMT
-    , TimeOut (..)
     )
 import qualified SMT
 import Stats
@@ -192,7 +203,7 @@ data KoreSearchOptions =
         -- ^ The maximum bound on the number of search matches
         , searchType :: !SearchType
         -- ^ The type of search to perform
-        }
+        } deriving (GHC.Generic)
 
 parseKoreSearchOptions :: Parser KoreSearchOptions
 parseKoreSearchOptions =
@@ -262,23 +273,6 @@ applyKoreSearchOptions koreSearchOptions@(Just koreSearchOpts) koreExecOpts =
             ONE -> Limit 1
             _ -> Unlimited
 
--- | Available SMT solvers
-data Solver = Z3 | None
-    deriving (Eq, Ord, Show)
-    deriving (Enum, Bounded)
-
-parseSolver :: Parser Solver
-parseSolver =
-    option (snd <$> readSum longName options)
-    $  metavar "SOLVER"
-    <> long longName
-    <> help ("SMT solver for checking constraints: " <> knownOptions)
-    <> value Z3
-  where
-    longName = "smt"
-    knownOptions = intercalate ", " (map fst options)
-    options = [ (map Char.toLower $ show s, s) | s <- [minBound .. maxBound] ]
-
 -- | Main options record
 data KoreExecOptions = KoreExecOptions
     { definitionFileName  :: !FilePath
@@ -289,19 +283,17 @@ data KoreExecOptions = KoreExecOptions
     -- ^ Name for file to contain the output pattern
     , mainModuleName      :: !ModuleName
     -- ^ The name of the main module in the definition
-    , smtTimeOut          :: !SMT.TimeOut
-    , smtPrelude          :: !(Maybe FilePath)
-    , smtSolver           :: !Solver
     , breadthLimit        :: !(Limit Natural)
     , depthLimit          :: !(Limit Natural)
     , strategy            :: !(String, [RewriteRule RewritingVariableName] -> Strategy (Prim (RewriteRule RewritingVariableName)))
+    , koreSolverOptions   :: !KoreSolverOptions
     , koreLogOptions      :: !KoreLogOptions
     , koreSearchOptions   :: !(Maybe KoreSearchOptions)
     , koreProveOptions    :: !(Maybe KoreProveOptions)
     , koreMergeOptions    :: !(Maybe KoreMergeOptions)
     , rtsStatistics       :: !(Maybe FilePath)
     , bugReport           :: !BugReport
-    }
+    } deriving (GHC.Generic)
 
 -- | Command Line Argument Parser
 parseKoreExecOptions :: TimeSpec -> Parser KoreExecOptions
@@ -332,35 +324,17 @@ parseKoreExecOptions startTime =
                 )
             )
         <*> parseMainModuleName
-        <*> option readSMTTimeOut
-            ( metavar "SMT_TIMEOUT"
-            <> long "smt-timeout"
-            <> help "Timeout for calls to the SMT solver, in milliseconds"
-            <> value defaultTimeOut
-            )
-        <*> optional
-            ( strOption
-                ( metavar "SMT_PRELUDE"
-                <> long "smt-prelude"
-                <> help "Path to the SMT prelude file"
-                )
-            )
-        <*> parseSolver
         <*> parseBreadthLimit
         <*> parseDepthLimit
         <*> parseStrategy
+        <*> parseKoreSolverOptions
         <*> parseKoreLogOptions (ExeName "kore-exec") startTime
         <*> pure Nothing
         <*> optional parseKoreProveOptions
         <*> optional parseKoreMergeOptions
         <*> optional parseRtsStatistics
         <*> parseBugReport
-    SMT.Config { timeOut = defaultTimeOut } = SMT.defaultConfig
-    readSMTTimeOut = do
-        i <- auto
-        if i <= 0
-            then readerError "smt-timeout must be a positive integer."
-            else return $ SMT.TimeOut $ Limit i
+
     parseBreadthLimit = Limit <$> breadth <|> pure Unlimited
     parseDepthLimit = Limit <$> depth <|> pure Unlimited
     parseStrategy =
@@ -375,6 +349,7 @@ parseKoreExecOptions startTime =
             [ ("any", priorityAnyStrategy)
             , ("all", priorityAllStrategy)
             ]
+
     breadth =
         option auto
             (  metavar "BREADTH"
@@ -387,6 +362,7 @@ parseKoreExecOptions startTime =
             <> long "depth"
             <> help "Execute up to DEPTH steps."
             )
+
     parseMainModuleName =
         GlobalMain.parseModuleName
             "MODULE"
@@ -446,12 +422,10 @@ koreExecSh
         patternFileName
         outputFileName
         mainModuleName
-        (TimeOut timeout)
-        smtPrelude
-        smtSolver
         breadthLimit
         depthLimit
         strategy
+        koreSolverOptions
         koreLogOptions
         koreSearchOptions
         koreProveOptions
@@ -474,10 +448,6 @@ koreExecSh
             , patternFileName $> "--pattern pgm.kore"
             , outputFileName $> "--output result.kore"
             , pure $ "--module " <> unpack (getModuleName mainModuleName)
-            , (\limit -> unwords ["--smt-timeout", show limit])
-                <$> maybeLimit Nothing Just timeout
-            , smtPrelude $> unwords ["--smt-prelude", defaultSmtPreludeFilePath]
-            , pure $ "--smt " <> fmap Char.toLower (show smtSolver)
             , (\limit -> unwords ["--breadth", show limit])
                 <$> maybeLimit Nothing Just breadthLimit
             , (\limit -> unwords ["--depth", show limit])
@@ -486,6 +456,7 @@ koreExecSh
             , rtsStatistics $>
                 unwords ["--rts-statistics", defaultRtsStatisticsFilePath]
             ]
+        , unparseKoreSolverOptions koreSolverOptions
         , unparseKoreLogOptions koreLogOptions
         , maybe mempty unparseKoreSearchOptions koreSearchOptions
         , maybe mempty unparseKoreProveOptions koreProveOptions
@@ -497,9 +468,6 @@ defaultDefinitionFilePath KoreExecOptions { koreProveOptions }
   | isJust koreProveOptions = "vdefinition.kore"
   | otherwise               = "definition.kore"
 
-defaultSmtPreludeFilePath :: FilePath
-defaultSmtPreludeFilePath = "prelude.smt2"
-
 defaultRtsStatisticsFilePath :: FilePath
 defaultRtsStatisticsFilePath = "rts-statistics.json"
 
@@ -527,7 +495,7 @@ writeOptionsAndKoreFiles
     opts@KoreExecOptions
         { definitionFileName
         , patternFileName
-        , smtPrelude
+        , koreSolverOptions
         , koreSearchOptions
         , koreProveOptions
         , koreMergeOptions
@@ -545,8 +513,7 @@ writeOptionsAndKoreFiles
         (reportDirectory </> defaultDefinitionFilePath opts)
     Foldable.for_ patternFileName
         $ flip copyFile (reportDirectory </> "pgm.kore")
-    Foldable.for_ smtPrelude
-        $ flip copyFile (reportDirectory </> defaultSmtPreludeFilePath)
+    writeKoreSolverFiles koreSolverOptions reportDirectory
     Foldable.for_ koreSearchOptions
         (writeKoreSearchFiles reportDirectory)
     Foldable.for_ koreMergeOptions
@@ -569,18 +536,10 @@ main = do
             parserInfoModifiers
     Foldable.for_ (localOptions options) mainWithOptions
 
--- | Ensure that the SMT prelude file exists, if specified.
-ensureSmtPreludeExists :: Maybe FilePath -> IO ()
-ensureSmtPreludeExists =
-    Foldable.traverse_ $ \filePath ->
-        Monad.whenM
-            (not <$> doesFileExist filePath)
-            (error $ "SMT prelude file does not exist: " <> filePath)
-
 mainWithOptions :: KoreExecOptions -> IO ()
 mainWithOptions execOptions = do
-    let KoreExecOptions { koreLogOptions, bugReport, smtPrelude } = execOptions
-    ensureSmtPreludeExists smtPrelude
+    let KoreExecOptions { koreLogOptions, koreSolverOptions, bugReport } = execOptions
+    ensureSmtPreludeExists koreSolverOptions
     exitCode <-
         withBugReport Main.exeName bugReport $ \tmpDir -> do
             writeOptionsAndKoreFiles tmpDir execOptions
@@ -841,7 +800,7 @@ execute
     -> Main r
 execute options mainModule worker =
     clockSomethingIO "Executing"
-        $ case smtSolver of
+        $ case solver of
             Z3   -> withZ3
             None -> withoutSMT
   where
@@ -854,11 +813,13 @@ execute options mainModule worker =
             )
             worker
     withoutSMT = SMT.runNoSMT worker
-    KoreExecOptions { smtTimeOut, smtPrelude, smtSolver } = options
+    KoreSolverOptions { timeOut, resetInterval, prelude, solver } =
+        Lens.view (field @"koreSolverOptions") options
     config =
         SMT.defaultConfig
-            { SMT.timeOut = smtTimeOut
-            , SMT.preludeFile = smtPrelude
+            { SMT.timeOut = timeOut
+            , SMT.resetInterval = resetInterval
+            , SMT.prelude = prelude
             }
 
 loadPattern :: LoadedModule -> Maybe FilePath -> Main (TermLike VariableName)

kore/app/repl/Main.hs

@@ -11,29 +11,22 @@ import Options.Applicative
     ( InfoMod
     , Parser
     , argument
-    , auto
     , flag
     , fullDesc
     , header
     , help
     , long
     , metavar
-    , option
     , progDesc
-    , readerError
     , short
     , str
     , strOption
-    , value
     )
 import System.Exit
     ( exitFailure
     , exitWith
     )
 
-import Data.Limit
-    ( Limit (..)
-    )
 import Kore.BugReport
 import Kore.Exec
     ( proveWithRepl
@@ -58,6 +51,10 @@ import Kore.Step.SMT.Lemma
 import Kore.Syntax.Module
     ( ModuleName (..)
     )
+import Options.SMT
+    ( KoreSolverOptions (..)
+    , parseKoreSolverOptions
+    )
 import qualified SMT
 import System.Clock
     ( Clock (Monotonic)
@@ -73,17 +70,11 @@ data KoreModule = KoreModule
     , moduleName :: !ModuleName
     }
 
--- | SMT Timeout and (optionally) a custom prelude path.
-data SmtOptions = SmtOptions
-    { timeOut :: !SMT.TimeOut
-    , prelude :: !(Maybe FilePath)
-    }
-
 -- | Options for the kore repl.
 data KoreReplOptions = KoreReplOptions
     { definitionModule :: !KoreModule
     , proveOptions     :: !KoreProveOptions
-    , smtOptions       :: !SmtOptions
+    , smtOptions       :: !KoreSolverOptions
     , replMode         :: !ReplMode
     , scriptModeOutput :: !ScriptModeOutput
     , replScript       :: !ReplScript
@@ -97,7 +88,7 @@ parseKoreReplOptions startTime =
     KoreReplOptions
     <$> parseMainModule
     <*> parseKoreProveOptions
-    <*> parseSmtOptions
+    <*> parseKoreSolverOptions
     <*> parseReplMode
     <*> parseScriptModeOutput
     <*> parseReplScript
@@ -116,23 +107,6 @@ parseKoreReplOptions startTime =
                 "module"
                 "Kore main module name."
 
-    parseSmtOptions :: Parser SmtOptions
-    parseSmtOptions =
-        SmtOptions
-        <$> option readSMTTimeOut
-            (  metavar "SMT_TIMEOUT"
-            <> long "smt-timeout"
-            <> help "Timeout for calls to the SMT solver, in miliseconds"
-            <> value defaultTimeOut
-            )
-        <*> optional
-            ( strOption
-                (  metavar "SMT_PRELUDE"
-                <> long "smt-prelude"
-                <> help "Path to the SMT prelude file"
-                )
-            )
-
     parseReplMode :: Parser ReplMode
     parseReplMode =
         flag
@@ -163,14 +137,6 @@ parseKoreReplOptions startTime =
                 )
             )
 
-    SMT.Config { timeOut = defaultTimeOut } = SMT.defaultConfig
-
-    readSMTTimeOut = do
-        i <- auto
-        if i <= 0
-            then readerError "smt-timeout must be a positive integer."
-            else return $ SMT.TimeOut $ Limit i
-
     parseOutputFile :: Parser OutputFile
     parseOutputFile =
         OutputFile
@@ -230,7 +196,8 @@ mainWithOptions
                     smtConfig =
                         SMT.defaultConfig
                             { SMT.timeOut = smtTimeOut
-                            , SMT.preludeFile = smtPrelude
+                            , SMT.resetInterval = smtResetInterval
+                            , SMT.prelude = smtPrelude
                             }
 
                 when
@@ -290,5 +257,8 @@ mainWithOptions
     smtTimeOut :: SMT.TimeOut
     smtTimeOut = timeOut smtOptions
 
-    smtPrelude :: Maybe FilePath
+    smtResetInterval :: SMT.ResetInterval
+    smtResetInterval = resetInterval smtOptions
+
+    smtPrelude :: SMT.Prelude
     smtPrelude = prelude smtOptions