From ae49c8d8b695758d9b0d77cfc28b92f2e67eac2b Mon Sep 17 00:00:00 2001 From: ana-pantilie Date: Thu, 22 Oct 2020 16:55:32 +0300 Subject: [PATCH 01/13] solver-reset-interval: add command line option --- kore/app/exec/Main.hs | 19 ++++++++++++++++++- kore/src/SMT.hs | 9 +++++++++ 2 files changed, 27 insertions(+), 1 deletion(-) diff --git a/kore/app/exec/Main.hs b/kore/app/exec/Main.hs index 0daef001fa..eb093c2148 100644 --- a/kore/app/exec/Main.hs +++ b/kore/app/exec/Main.hs @@ -290,6 +290,7 @@ data KoreExecOptions = KoreExecOptions , mainModuleName :: !ModuleName -- ^ The name of the main module in the definition , smtTimeOut :: !SMT.TimeOut + , smtResetInterval :: !SMT.ResetInterval , smtPrelude :: !(Maybe FilePath) , smtSolver :: !Solver , breadthLimit :: !(Limit Natural) @@ -338,6 +339,12 @@ parseKoreExecOptions startTime = <> help "Timeout for calls to the SMT solver, in milliseconds" <> value defaultTimeOut ) + <*> option readSMTResetInterval + ( metavar "SMT_RESET_INTERVAL" + <> long "smt-reset-interval" + <> help "Reset the solver after this number of queries" + <> value defaultResetInterval + ) <*> optional ( strOption ( metavar "SMT_PRELUDE" @@ -356,11 +363,17 @@ parseKoreExecOptions startTime = <*> optional parseRtsStatistics <*> parseBugReport SMT.Config { timeOut = defaultTimeOut } = SMT.defaultConfig + SMT.Config { resetInterval = defaultResetInterval } = SMT.defaultConfig readSMTTimeOut = do i <- auto if i <= 0 then readerError "smt-timeout must be a positive integer." else return $ SMT.TimeOut $ Limit i + readSMTResetInterval = do + i <- auto + if i <= 0 + then readerError "smt-reset-interval must be a positive integer." + else return $ SMT.ResetInterval i parseBreadthLimit = Limit <$> breadth <|> pure Unlimited parseDepthLimit = Limit <$> depth <|> pure Unlimited parseStrategy = @@ -447,6 +460,8 @@ koreExecSh outputFileName mainModuleName (TimeOut timeout) + -- TODO: what is this? + (SMT.ResetInterval _) smtPrelude smtSolver breadthLimit @@ -854,10 +869,12 @@ execute options mainModule worker = ) worker withoutSMT = SMT.runNoSMT worker - KoreExecOptions { smtTimeOut, smtPrelude, smtSolver } = options + KoreExecOptions { smtTimeOut, smtResetInterval, smtPrelude, smtSolver } = + options config = SMT.defaultConfig { SMT.timeOut = smtTimeOut + , SMT.resetInterval = smtResetInterval , SMT.preludeFile = smtPrelude } diff --git a/kore/src/SMT.hs b/kore/src/SMT.hs index bf7e2cec59..bf791489d0 100644 --- a/kore/src/SMT.hs +++ b/kore/src/SMT.hs @@ -15,6 +15,7 @@ module SMT , Config (..) , defaultConfig , TimeOut (..) + , ResetInterval (..) , Result (..) , Constructor (..) , ConstructorArgument (..) @@ -422,6 +423,11 @@ instance MonadSMT m => MonadSMT (ExceptT e m) newtype TimeOut = TimeOut { getTimeOut :: Limit Integer } deriving (Eq, Ord, Read, Show) +-- | Reset interval for solver. +newtype ResetInterval = + ResetInterval { getResetInterval :: Integer } + deriving (Eq, Ord, Read, Show) + -- | Solver configuration data Config = Config @@ -435,6 +441,8 @@ data Config = -- ^ optional log file name , timeOut :: TimeOut -- ^ query time limit + , resetInterval :: ResetInterval + -- ^ reset solver after this number of queries } -- | Default configuration using the Z3 solver. @@ -449,6 +457,7 @@ defaultConfig = , preludeFile = Nothing , logFile = Nothing , timeOut = TimeOut (Limit 40) + , resetInterval = ResetInterval 100 } initSolver :: Config -> SMT () From 1a2693fa50b2773bf0979b02d0aa00cc3cef57c1 Mon Sep 17 00:00:00 2001 From: ana-pantilie Date: Thu, 22 Oct 2020 18:46:12 +0300 Subject: [PATCH 02/13] SMT.incrementQueryCounter: use reset value from config --- kore/app/repl/Main.hs | 1 + kore/src/SMT.hs | 19 +++++++++++++++---- 2 files changed, 16 insertions(+), 4 deletions(-) diff --git a/kore/app/repl/Main.hs b/kore/app/repl/Main.hs index 6db4ca2e6a..54f597e662 100644 --- a/kore/app/repl/Main.hs +++ b/kore/app/repl/Main.hs @@ -79,6 +79,7 @@ data SmtOptions = SmtOptions , prelude :: !(Maybe FilePath) } +-- TODO: add solver-reset-interval -- | Options for the kore repl. data KoreReplOptions = KoreReplOptions { definitionModule :: !KoreModule diff --git a/kore/src/SMT.hs b/kore/src/SMT.hs index bf791489d0..12541d2562 100644 --- a/kore/src/SMT.hs +++ b/kore/src/SMT.hs @@ -344,14 +344,16 @@ unshareSolverHandle action = do {- | Increase the 'queryCounter' and indicate if the solver should be reset. -} -incrementQueryCounter :: Monad monad => StateT SolverHandle monad Bool -incrementQueryCounter = do +incrementQueryCounter + :: Monad monad => ResetInterval -> StateT SolverHandle monad Bool +incrementQueryCounter (ResetInterval resetInterval) = do Lens.modifying (field @"queryCounter") (+ 1) counter <- Lens.use (field @"queryCounter") -- Due to an issue with the SMT solver, we need to reinitialise it after a -- number of runs, specified here. This number can be adjusted based on -- experimentation. - pure (counter >= 100) + traceShowM resetInterval + pure (toInteger counter >= resetInterval) instance MonadSMT SMT where withSolver action = @@ -360,7 +362,10 @@ instance MonadSMT SMT where Exception.finally action (do withSolver' pop - needReset <- modifySolverHandle incrementQueryCounter + resetInterval' <- extractResetInterval + needReset <- + modifySolverHandle + (incrementQueryCounter resetInterval') when needReset reinit ) @@ -547,3 +552,9 @@ setTimeOut TimeOut { getTimeOut } = setOption ":timeout" (SimpleSMT.int timeOut) Unlimited -> return () + +-- | Extract the reset interval value from the configuration. +extractResetInterval :: SMT ResetInterval +extractResetInterval = + SMT (Reader.asks config) + >>= return . resetInterval From 39bc5b6dea21b781987d1779bdb9c57fb2cdd9dc Mon Sep 17 00:00:00 2001 From: ana-pantilie Date: Thu, 22 Oct 2020 18:54:58 +0300 Subject: [PATCH 03/13] Main.koreExecSh: add case for solver reset interval --- kore/app/exec/Main.hs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/kore/app/exec/Main.hs b/kore/app/exec/Main.hs index eb093c2148..a5b25b1486 100644 --- a/kore/app/exec/Main.hs +++ b/kore/app/exec/Main.hs @@ -460,8 +460,7 @@ koreExecSh outputFileName mainModuleName (TimeOut timeout) - -- TODO: what is this? - (SMT.ResetInterval _) + (SMT.ResetInterval resetInterval) smtPrelude smtSolver breadthLimit @@ -491,6 +490,7 @@ koreExecSh , pure $ "--module " <> unpack (getModuleName mainModuleName) , (\limit -> unwords ["--smt-timeout", show limit]) <$> maybeLimit Nothing Just timeout + , pure $ unwords ["--smt-reset-interval", show resetInterval] , smtPrelude $> unwords ["--smt-prelude", defaultSmtPreludeFilePath] , pure $ "--smt " <> fmap Char.toLower (show smtSolver) , (\limit -> unwords ["--breadth", show limit]) From c6dc2c0ec4f39f86fe3d88a57aa090233358994d Mon Sep 17 00:00:00 2001 From: ana-pantilie Date: Thu, 22 Oct 2020 18:55:29 +0300 Subject: [PATCH 04/13] Clean-up: remove trace --- kore/src/SMT.hs | 1 - 1 file changed, 1 deletion(-) diff --git a/kore/src/SMT.hs b/kore/src/SMT.hs index 12541d2562..38d78a3725 100644 --- a/kore/src/SMT.hs +++ b/kore/src/SMT.hs @@ -352,7 +352,6 @@ incrementQueryCounter (ResetInterval resetInterval) = do -- Due to an issue with the SMT solver, we need to reinitialise it after a -- number of runs, specified here. This number can be adjusted based on -- experimentation. - traceShowM resetInterval pure (toInteger counter >= resetInterval) instance MonadSMT SMT where From 6d2d7576b5543eeae0835ef81e9d7d3257b34f1b Mon Sep 17 00:00:00 2001 From: ana-pantilie Date: Thu, 22 Oct 2020 19:08:59 +0300 Subject: [PATCH 05/13] Factor out readPositiveInteger --- kore/app/exec/Main.hs | 28 ++++++++++++++++++---------- 1 file changed, 18 insertions(+), 10 deletions(-) diff --git a/kore/app/exec/Main.hs b/kore/app/exec/Main.hs index a5b25b1486..c4a37bd77a 100644 --- a/kore/app/exec/Main.hs +++ b/kore/app/exec/Main.hs @@ -362,18 +362,24 @@ parseKoreExecOptions startTime = <*> optional parseKoreMergeOptions <*> optional parseRtsStatistics <*> parseBugReport + SMT.Config { timeOut = defaultTimeOut } = SMT.defaultConfig SMT.Config { resetInterval = defaultResetInterval } = SMT.defaultConfig - readSMTTimeOut = do - i <- auto - if i <= 0 - then readerError "smt-timeout must be a positive integer." - else return $ SMT.TimeOut $ Limit i - readSMTResetInterval = do - i <- auto - if i <= 0 - then readerError "smt-reset-interval must be a positive integer." - else return $ SMT.ResetInterval i + + readPositiveInteger ctor optionName = do + readInt <- auto + when (readInt <= 0) err + return . ctor $ readInt + where + err = + readerError + . unwords + $ [optionName, "must be a positive integer."] + + readSMTTimeOut = readPositiveInteger (SMT.TimeOut . Limit) "smt-timeout" + readSMTResetInterval = + readPositiveInteger SMT.ResetInterval "smt-reset-interval" + parseBreadthLimit = Limit <$> breadth <|> pure Unlimited parseDepthLimit = Limit <$> depth <|> pure Unlimited parseStrategy = @@ -388,6 +394,7 @@ parseKoreExecOptions startTime = [ ("any", priorityAnyStrategy) , ("all", priorityAllStrategy) ] + breadth = option auto ( metavar "BREADTH" @@ -400,6 +407,7 @@ parseKoreExecOptions startTime = <> long "depth" <> help "Execute up to DEPTH steps." ) + parseMainModuleName = GlobalMain.parseModuleName "MODULE" From 04132b9e5834a774fc3f49fdd29bf08f5e65ac45 Mon Sep 17 00:00:00 2001 From: ana-pantilie Date: Thu, 22 Oct 2020 19:17:12 +0300 Subject: [PATCH 06/13] kore-repl: add command line option here as well --- kore/app/repl/Main.hs | 31 +++++++++++++++++++++++++------ 1 file changed, 25 insertions(+), 6 deletions(-) diff --git a/kore/app/repl/Main.hs b/kore/app/repl/Main.hs index 54f597e662..702bd507b3 100644 --- a/kore/app/repl/Main.hs +++ b/kore/app/repl/Main.hs @@ -76,10 +76,10 @@ data KoreModule = KoreModule -- | SMT Timeout and (optionally) a custom prelude path. data SmtOptions = SmtOptions { timeOut :: !SMT.TimeOut + , resetInterval :: !SMT.ResetInterval , prelude :: !(Maybe FilePath) } --- TODO: add solver-reset-interval -- | Options for the kore repl. data KoreReplOptions = KoreReplOptions { definitionModule :: !KoreModule @@ -126,6 +126,12 @@ parseKoreReplOptions startTime = <> help "Timeout for calls to the SMT solver, in miliseconds" <> value defaultTimeOut ) + <*> option readSMTResetInterval + ( metavar "SMT_RESET_INTERVAL" + <> long "smt-reset-interval" + <> help "Reset the solver after this number of queries" + <> value defaultResetInterval + ) <*> optional ( strOption ( metavar "SMT_PRELUDE" @@ -165,12 +171,21 @@ parseKoreReplOptions startTime = ) SMT.Config { timeOut = defaultTimeOut } = SMT.defaultConfig + SMT.Config { resetInterval = defaultResetInterval } = SMT.defaultConfig + + readPositiveInteger ctor optionName = do + readInt <- auto + when (readInt <= 0) err + return . ctor $ readInt + where + err = + readerError + . unwords + $ [optionName, "must be a positive integer."] - readSMTTimeOut = do - i <- auto - if i <= 0 - then readerError "smt-timeout must be a positive integer." - else return $ SMT.TimeOut $ Limit i + readSMTTimeOut = readPositiveInteger (SMT.TimeOut . Limit) "smt-timeout" + readSMTResetInterval = + readPositiveInteger SMT.ResetInterval "smt-reset-interval" parseOutputFile :: Parser OutputFile parseOutputFile = @@ -231,6 +246,7 @@ mainWithOptions smtConfig = SMT.defaultConfig { SMT.timeOut = smtTimeOut + , SMT.resetInterval = smtResetInterval , SMT.preludeFile = smtPrelude } @@ -291,5 +307,8 @@ mainWithOptions smtTimeOut :: SMT.TimeOut smtTimeOut = timeOut smtOptions + smtResetInterval :: SMT.ResetInterval + smtResetInterval = resetInterval smtOptions + smtPrelude :: Maybe FilePath smtPrelude = prelude smtOptions From c45c53617452793c88810882e9a8025c69ab0208 Mon Sep 17 00:00:00 2001 From: ana-pantilie Date: Thu, 22 Oct 2020 20:15:27 +0300 Subject: [PATCH 07/13] SMT.Config: make fields strict --- kore/src/SMT.hs | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/kore/src/SMT.hs b/kore/src/SMT.hs index 38d78a3725..1703cf27b5 100644 --- a/kore/src/SMT.hs +++ b/kore/src/SMT.hs @@ -435,17 +435,17 @@ newtype ResetInterval = -- | Solver configuration data Config = Config - { executable :: FilePath + { executable :: !FilePath -- ^ solver executable file name - , arguments :: [String] + , arguments :: ![String] -- ^ default command-line arguments to solver - , preludeFile :: Maybe FilePath + , preludeFile :: !(Maybe FilePath) -- ^ prelude of definitions to initialize solver - , logFile :: Maybe FilePath + , logFile :: !(Maybe FilePath) -- ^ optional log file name - , timeOut :: TimeOut + , timeOut :: !TimeOut -- ^ query time limit - , resetInterval :: ResetInterval + , resetInterval :: !ResetInterval -- ^ reset solver after this number of queries } From d9778712fc0d98cb137efca8d5e374c5c5326ac5 Mon Sep 17 00:00:00 2001 From: ana-pantilie Date: Thu, 22 Oct 2020 21:50:50 +0300 Subject: [PATCH 08/13] Add Options.SMT; WIP clean-up solver options in kore-exec Main --- kore/app/exec/Main.hs | 111 +++++++++++++++------------------- kore/src/Options/SMT.hs | 128 ++++++++++++++++++++++++++++++++++++++++ 2 files changed, 174 insertions(+), 65 deletions(-) create mode 100644 kore/src/Options/SMT.hs diff --git a/kore/app/exec/Main.hs b/kore/app/exec/Main.hs index c4a37bd77a..51bb13fce8 100644 --- a/kore/app/exec/Main.hs +++ b/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 @@ -15,6 +16,9 @@ import Data.Default ( def ) import qualified Data.Foldable as Foldable +import Data.Generics.Product + ( field + ) import Data.Limit ( Limit (..) , maybeLimit @@ -53,6 +57,7 @@ import Options.Applicative , value ) import qualified Options.Applicative as Options +import qualified GHC.Generics as GHC import System.Clock ( Clock (Monotonic) , TimeSpec @@ -160,6 +165,12 @@ import qualified Kore.Syntax.Definition as Definition.DoNotUse import Kore.Unparser ( unparse ) +import Options.SMT + ( KoreSolverOptions (..) + , Prelude (..) + , Solver (..) + , parseKoreSolverOptions + ) import Pretty ( Doc , Pretty (..) @@ -192,7 +203,7 @@ data KoreSearchOptions = -- ^ The maximum bound on the number of search matches , searchType :: !SearchType -- ^ The type of search to perform - } + } (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,13 +283,10 @@ 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 - , smtResetInterval :: !SMT.ResetInterval - , 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) @@ -333,29 +324,10 @@ parseKoreExecOptions startTime = ) ) <*> parseMainModuleName - <*> option readSMTTimeOut - ( metavar "SMT_TIMEOUT" - <> long "smt-timeout" - <> help "Timeout for calls to the SMT solver, in milliseconds" - <> value defaultTimeOut - ) - <*> option readSMTResetInterval - ( metavar "SMT_RESET_INTERVAL" - <> long "smt-reset-interval" - <> help "Reset the solver after this number of queries" - <> value defaultResetInterval - ) - <*> 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 @@ -467,13 +439,10 @@ koreExecSh patternFileName outputFileName mainModuleName - (TimeOut timeout) - (SMT.ResetInterval resetInterval) - smtPrelude - smtSolver breadthLimit depthLimit strategy + koreSolverOptions koreLogOptions koreSearchOptions koreProveOptions @@ -496,11 +465,11 @@ koreExecSh , patternFileName $> "--pattern pgm.kore" , outputFileName $> "--output result.kore" , pure $ "--module " <> unpack (getModuleName mainModuleName) - , (\limit -> unwords ["--smt-timeout", show limit]) - <$> maybeLimit Nothing Just timeout - , pure $ unwords ["--smt-reset-interval", show resetInterval] - , smtPrelude $> unwords ["--smt-prelude", defaultSmtPreludeFilePath] - , pure $ "--smt " <> fmap Char.toLower (show smtSolver) + -- , (\limit -> unwords ["--smt-timeout", show limit]) + -- <$> maybeLimit Nothing Just timeout + -- , pure $ unwords ["--smt-reset-interval", show resetInterval] + -- , 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]) @@ -526,6 +495,14 @@ defaultSmtPreludeFilePath = "prelude.smt2" defaultRtsStatisticsFilePath :: FilePath defaultRtsStatisticsFilePath = "rts-statistics.json" +writeKoreSolverFiles :: KoreSolverOptions -> FilePath -> IO () +writeKoreSolverFiles + KoreSolverOptions { prelude = Prelude smtPrelude } + reportFile + = + Foldable.for_ smtPrelude + $ flip copyFile (reportFile defaultSmtPreludeFilePath) + writeKoreSearchFiles :: FilePath -> KoreSearchOptions -> IO () writeKoreSearchFiles reportFile KoreSearchOptions { searchFileName } = copyFile searchFileName $ reportFile <> "/searchFile.kore" @@ -550,7 +527,7 @@ writeOptionsAndKoreFiles opts@KoreExecOptions { definitionFileName , patternFileName - , smtPrelude + , koreSolverOptions , koreSearchOptions , koreProveOptions , koreMergeOptions @@ -568,8 +545,9 @@ writeOptionsAndKoreFiles (reportDirectory defaultDefinitionFilePath opts) Foldable.for_ patternFileName $ flip copyFile (reportDirectory "pgm.kore") - Foldable.for_ smtPrelude - $ flip copyFile (reportDirectory defaultSmtPreludeFilePath) + -- Foldable.for_ smtPrelude + -- $ flip copyFile (reportDirectory defaultSmtPreludeFilePath) + writeKoreSolverFiles koreSolverOptions reportDirectory Foldable.for_ koreSearchOptions (writeKoreSearchFiles reportDirectory) Foldable.for_ koreMergeOptions @@ -593,17 +571,20 @@ main = do 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) +ensureSmtPreludeExists :: KoreSolverOptions -> IO () +ensureSmtPreludeExists KoreSolverOptions { prelude = Prelude smtPrelude } = + Foldable.traverse_ + (\filePath -> + Monad.whenM + (not <$> doesFileExist filePath) + (error $ "SMT prelude file does not exist: " <> filePath) + ) + smtPrelude 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 @@ -864,7 +845,7 @@ execute -> Main r execute options mainModule worker = clockSomethingIO "Executing" - $ case smtSolver of + $ case solver of Z3 -> withZ3 None -> withoutSMT where @@ -877,8 +858,8 @@ execute options mainModule worker = ) worker withoutSMT = SMT.runNoSMT worker - KoreExecOptions { smtTimeOut, smtResetInterval, smtPrelude, smtSolver } = - options + KoreSolverOptions { timeOut, resetInterval, prelude, solver } = + Lens.view (field @"koreSolverOptions") options config = SMT.defaultConfig { SMT.timeOut = smtTimeOut diff --git a/kore/src/Options/SMT.hs b/kore/src/Options/SMT.hs new file mode 100644 index 0000000000..4c777298f9 --- /dev/null +++ b/kore/src/Options/SMT.hs @@ -0,0 +1,128 @@ +{- | +Copyright : (c) Runtime Verification, 2020 +License : NCSA +-} + +module Options.SMT + ( KoreSolverOptions (..) + , Prelude (..) + , Solver (..) + , parseKoreSolverOptions + , unparseKoreLogOptions + ) where + +import Prelude.Kore + +import qualified Data.Char as Char +import Data.List + ( intercalate + ) +import Options.Applicative + ( InfoMod + , Parser + , argument + , auto + , fullDesc + , header + , help + , long + , metavar + , option + , progDesc + , readerError + , str + , strOption + , value + ) +import qualified Options.Applicative as Options + +import Data.Limit + ( Limit (..) + , maybeLimit + ) +import SMT hiding + ( Solver + ) + +data KoreSolverOptions = KoreSolverOptions + { timeOut :: !TimeOut + , resetInterval :: !ResetInterval + , prelude :: !Prelude + , solver :: !Solver + } + +newtype Prelude = Prelude { getPrelude :: Maybe FilePath } + +parseKoreSolverOptions :: Parser KoreSolverOptions +parseKoreSolverOptions = + KoreSolverOptions + <$> option readSMTTimeOut + ( metavar "SMT_TIMEOUT" + <> long "smt-timeout" + <> help "Timeout for calls to the SMT solver, in milliseconds" + <> value defaultTimeOut + ) + <*> option readSMTResetInterval + ( metavar "SMT_RESET_INTERVAL" + <> long "smt-reset-interval" + <> help "Reset the solver after this number of queries" + <> value defaultResetInterval + ) + <*> + (Prelude <$> + optional + ( strOption + ( metavar "SMT_PRELUDE" + <> long "smt-prelude" + <> help "Path to the SMT prelude file" + ) + ) + ) + <*> parseSolver + where + SMT.Config { timeOut = defaultTimeOut } = SMT.defaultConfig + SMT.Config { resetInterval = defaultResetInterval } = SMT.defaultConfig + + readPositiveInteger ctor optionName = do + readInt <- auto + when (readInt <= 0) err + return . ctor $ readInt + where + err = + readerError + . unwords + $ [optionName, "must be a positive integer."] + + readSMTTimeOut = readPositiveInteger (SMT.TimeOut . Limit) "smt-timeout" + readSMTResetInterval = + readPositiveInteger SMT.ResetInterval "smt-reset-interval" + +unparseKoreLogOptions = undefined + +-- | 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] ] + +readSum :: String -> [(String, value)] -> Options.ReadM (String, value) +readSum longName options = do + opt <- str + case lookup opt options of + Just val -> pure (opt, val) + _ -> readerError (unknown opt ++ known) + where + knownOptions = intercalate ", " (map fst options) + unknown opt = "Unknown " ++ longName ++ " '" ++ opt ++ "'. " + known = "Known " ++ longName ++ "s are: " ++ knownOptions ++ "." From 176d8431bcb63dfdb9bf4a7ed68a677b86d56a63 Mon Sep 17 00:00:00 2001 From: ana-pantilie Date: Fri, 23 Oct 2020 14:12:27 +0300 Subject: [PATCH 09/13] kore-exec Main: use KoreSolverOptions --- kore/app/exec/Main.hs | 53 ++++++++++++----------------------------- kore/src/Options/SMT.hs | 34 +++++++++++++++++--------- kore/src/SMT.hs | 12 +++++++--- 3 files changed, 47 insertions(+), 52 deletions(-) diff --git a/kore/app/exec/Main.hs b/kore/app/exec/Main.hs index 51bb13fce8..84f6d21a8b 100644 --- a/kore/app/exec/Main.hs +++ b/kore/app/exec/Main.hs @@ -11,7 +11,6 @@ import Control.Monad.Catch , throwM ) import Control.Monad.Extra as Monad -import qualified Data.Char as Char import Data.Default ( def ) @@ -39,6 +38,7 @@ import qualified Data.Text.IO as Text ( putStrLn , readFile ) +import qualified GHC.Generics as GHC import Options.Applicative ( InfoMod , Parser @@ -57,7 +57,6 @@ import Options.Applicative , value ) import qualified Options.Applicative as Options -import qualified GHC.Generics as GHC import System.Clock ( Clock (Monotonic) , TimeSpec @@ -167,9 +166,10 @@ import Kore.Unparser ) import Options.SMT ( KoreSolverOptions (..) - , Prelude (..) , Solver (..) + , defaultSmtPreludeFilePath , parseKoreSolverOptions + , unparseKoreSolverOptions ) import Pretty ( Doc @@ -183,7 +183,6 @@ import Prof ) import SMT ( MonadSMT - , TimeOut (..) ) import qualified SMT import Stats @@ -203,7 +202,7 @@ data KoreSearchOptions = -- ^ The maximum bound on the number of search matches , searchType :: !SearchType -- ^ The type of search to perform - } (GHC.Generic) + } deriving (GHC.Generic) parseKoreSearchOptions :: Parser KoreSearchOptions parseKoreSearchOptions = @@ -293,7 +292,7 @@ data KoreExecOptions = KoreExecOptions , koreMergeOptions :: !(Maybe KoreMergeOptions) , rtsStatistics :: !(Maybe FilePath) , bugReport :: !BugReport - } + } deriving (GHC.Generic) -- | Command Line Argument Parser parseKoreExecOptions :: TimeSpec -> Parser KoreExecOptions @@ -335,23 +334,6 @@ parseKoreExecOptions startTime = <*> optional parseRtsStatistics <*> parseBugReport - SMT.Config { timeOut = defaultTimeOut } = SMT.defaultConfig - SMT.Config { resetInterval = defaultResetInterval } = SMT.defaultConfig - - readPositiveInteger ctor optionName = do - readInt <- auto - when (readInt <= 0) err - return . ctor $ readInt - where - err = - readerError - . unwords - $ [optionName, "must be a positive integer."] - - readSMTTimeOut = readPositiveInteger (SMT.TimeOut . Limit) "smt-timeout" - readSMTResetInterval = - readPositiveInteger SMT.ResetInterval "smt-reset-interval" - parseBreadthLimit = Limit <$> breadth <|> pure Unlimited parseDepthLimit = Limit <$> depth <|> pure Unlimited parseStrategy = @@ -465,11 +447,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 - -- , pure $ unwords ["--smt-reset-interval", show resetInterval] - -- , 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]) @@ -478,6 +455,7 @@ koreExecSh , rtsStatistics $> unwords ["--rts-statistics", defaultRtsStatisticsFilePath] ] + , unparseKoreSolverOptions koreSolverOptions , unparseKoreLogOptions koreLogOptions , maybe mempty unparseKoreSearchOptions koreSearchOptions , maybe mempty unparseKoreProveOptions koreProveOptions @@ -489,15 +467,12 @@ defaultDefinitionFilePath KoreExecOptions { koreProveOptions } | isJust koreProveOptions = "vdefinition.kore" | otherwise = "definition.kore" -defaultSmtPreludeFilePath :: FilePath -defaultSmtPreludeFilePath = "prelude.smt2" - defaultRtsStatisticsFilePath :: FilePath defaultRtsStatisticsFilePath = "rts-statistics.json" writeKoreSolverFiles :: KoreSolverOptions -> FilePath -> IO () writeKoreSolverFiles - KoreSolverOptions { prelude = Prelude smtPrelude } + KoreSolverOptions { prelude = SMT.Prelude smtPrelude } reportFile = Foldable.for_ smtPrelude @@ -545,8 +520,8 @@ writeOptionsAndKoreFiles (reportDirectory defaultDefinitionFilePath opts) Foldable.for_ patternFileName $ flip copyFile (reportDirectory "pgm.kore") - -- Foldable.for_ smtPrelude - -- $ flip copyFile (reportDirectory defaultSmtPreludeFilePath) + Foldable.for_ unwrappedPrelude + $ flip copyFile (reportDirectory defaultSmtPreludeFilePath) writeKoreSolverFiles koreSolverOptions reportDirectory Foldable.for_ koreSearchOptions (writeKoreSearchFiles reportDirectory) @@ -554,6 +529,8 @@ writeOptionsAndKoreFiles (writeKoreMergeFiles reportDirectory) Foldable.for_ koreProveOptions (writeKoreProveFiles reportDirectory) + where + KoreSolverOptions { prelude = SMT.Prelude unwrappedPrelude } = koreSolverOptions exeName :: ExeName exeName = ExeName "kore-exec" @@ -572,7 +549,7 @@ main = do -- | Ensure that the SMT prelude file exists, if specified. ensureSmtPreludeExists :: KoreSolverOptions -> IO () -ensureSmtPreludeExists KoreSolverOptions { prelude = Prelude smtPrelude } = +ensureSmtPreludeExists KoreSolverOptions { prelude = SMT.Prelude smtPrelude } = Foldable.traverse_ (\filePath -> Monad.whenM @@ -862,9 +839,9 @@ execute options mainModule worker = Lens.view (field @"koreSolverOptions") options config = SMT.defaultConfig - { SMT.timeOut = smtTimeOut - , SMT.resetInterval = smtResetInterval - , SMT.preludeFile = smtPrelude + { SMT.timeOut = timeOut + , SMT.resetInterval = resetInterval + , SMT.prelude = prelude } loadPattern :: LoadedModule -> Maybe FilePath -> Main (TermLike VariableName) diff --git a/kore/src/Options/SMT.hs b/kore/src/Options/SMT.hs index 4c777298f9..a962f4f135 100644 --- a/kore/src/Options/SMT.hs +++ b/kore/src/Options/SMT.hs @@ -5,10 +5,10 @@ License : NCSA module Options.SMT ( KoreSolverOptions (..) - , Prelude (..) , Solver (..) , parseKoreSolverOptions - , unparseKoreLogOptions + , unparseKoreSolverOptions + , defaultSmtPreludeFilePath ) where import Prelude.Kore @@ -18,17 +18,12 @@ import Data.List ( intercalate ) import Options.Applicative - ( InfoMod - , Parser - , argument + ( Parser , auto - , fullDesc - , header , help , long , metavar , option - , progDesc , readerError , str , strOption @@ -51,8 +46,6 @@ data KoreSolverOptions = KoreSolverOptions , solver :: !Solver } -newtype Prelude = Prelude { getPrelude :: Maybe FilePath } - parseKoreSolverOptions :: Parser KoreSolverOptions parseKoreSolverOptions = KoreSolverOptions @@ -97,7 +90,22 @@ parseKoreSolverOptions = readSMTResetInterval = readPositiveInteger SMT.ResetInterval "smt-reset-interval" -unparseKoreLogOptions = undefined +unparseKoreSolverOptions :: KoreSolverOptions -> [String] +unparseKoreSolverOptions + KoreSolverOptions + { timeOut = TimeOut unwrappedTimeOut + , resetInterval + , prelude = Prelude unwrappedPrelude + , solver + } + = + catMaybes + [ (\limit -> unwords ["--smt-timeout", show limit]) + <$> maybeLimit Nothing Just unwrappedTimeOut + , pure $ unwords ["--smt-reset-interval", show resetInterval] + , unwrappedPrelude $> unwords ["--smt-prelude", defaultSmtPreludeFilePath] + , pure $ "--smt " <> fmap Char.toLower (show solver) + ] -- | Available SMT solvers data Solver = Z3 | None @@ -126,3 +134,7 @@ readSum longName options = do knownOptions = intercalate ", " (map fst options) unknown opt = "Unknown " ++ longName ++ " '" ++ opt ++ "'. " known = "Known " ++ longName ++ "s are: " ++ knownOptions ++ "." + + +defaultSmtPreludeFilePath :: FilePath +defaultSmtPreludeFilePath = "prelude.smt2" diff --git a/kore/src/SMT.hs b/kore/src/SMT.hs index 1703cf27b5..6cd50fa1af 100644 --- a/kore/src/SMT.hs +++ b/kore/src/SMT.hs @@ -16,6 +16,7 @@ module SMT , defaultConfig , TimeOut (..) , ResetInterval (..) + , Prelude (..) , Result (..) , Constructor (..) , ConstructorArgument (..) @@ -432,6 +433,9 @@ newtype ResetInterval = ResetInterval { getResetInterval :: Integer } deriving (Eq, Ord, Read, Show) +-- | TODO: docs +newtype Prelude = Prelude { getPrelude :: Maybe FilePath } + -- | Solver configuration data Config = Config @@ -439,7 +443,7 @@ data Config = -- ^ solver executable file name , arguments :: ![String] -- ^ default command-line arguments to solver - , preludeFile :: !(Maybe FilePath) + , prelude :: !Prelude -- ^ prelude of definitions to initialize solver , logFile :: !(Maybe FilePath) -- ^ optional log file name @@ -458,17 +462,19 @@ defaultConfig = [ "-smt2" -- use SMT-LIB2 format , "-in" -- read from standard input ] - , preludeFile = Nothing + , prelude = Prelude Nothing , logFile = Nothing , timeOut = TimeOut (Limit 40) , resetInterval = ResetInterval 100 } initSolver :: Config -> SMT () -initSolver Config { timeOut, preludeFile } = do +initSolver Config { timeOut, prelude } = do setTimeOut timeOut Foldable.traverse_ loadFile preludeFile join $ SMT (Reader.asks userInit) + where + preludeFile = getPrelude prelude {- | Initialize a new solverHandle with the given 'Config'. From 3bfadfbe1407fd52d866650426196e8bab084a10 Mon Sep 17 00:00:00 2001 From: ana-pantilie Date: Fri, 23 Oct 2020 14:21:08 +0300 Subject: [PATCH 10/13] kore-repl Main: use KoreSolverOptions --- kore/app/repl/Main.hs | 66 ++++++------------------------------------- 1 file changed, 8 insertions(+), 58 deletions(-) diff --git a/kore/app/repl/Main.hs b/kore/app/repl/Main.hs index 702bd507b3..e19ddbe50d 100644 --- a/kore/app/repl/Main.hs +++ b/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,18 +70,11 @@ data KoreModule = KoreModule , moduleName :: !ModuleName } --- | SMT Timeout and (optionally) a custom prelude path. -data SmtOptions = SmtOptions - { timeOut :: !SMT.TimeOut - , resetInterval :: !SMT.ResetInterval - , 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 @@ -98,7 +88,7 @@ parseKoreReplOptions startTime = KoreReplOptions <$> parseMainModule <*> parseKoreProveOptions - <*> parseSmtOptions + <*> parseKoreSolverOptions <*> parseReplMode <*> parseScriptModeOutput <*> parseReplScript @@ -117,29 +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 - ) - <*> option readSMTResetInterval - ( metavar "SMT_RESET_INTERVAL" - <> long "smt-reset-interval" - <> help "Reset the solver after this number of queries" - <> value defaultResetInterval - ) - <*> optional - ( strOption - ( metavar "SMT_PRELUDE" - <> long "smt-prelude" - <> help "Path to the SMT prelude file" - ) - ) - parseReplMode :: Parser ReplMode parseReplMode = flag @@ -170,23 +137,6 @@ parseKoreReplOptions startTime = ) ) - SMT.Config { timeOut = defaultTimeOut } = SMT.defaultConfig - SMT.Config { resetInterval = defaultResetInterval } = SMT.defaultConfig - - readPositiveInteger ctor optionName = do - readInt <- auto - when (readInt <= 0) err - return . ctor $ readInt - where - err = - readerError - . unwords - $ [optionName, "must be a positive integer."] - - readSMTTimeOut = readPositiveInteger (SMT.TimeOut . Limit) "smt-timeout" - readSMTResetInterval = - readPositiveInteger SMT.ResetInterval "smt-reset-interval" - parseOutputFile :: Parser OutputFile parseOutputFile = OutputFile @@ -247,7 +197,7 @@ mainWithOptions SMT.defaultConfig { SMT.timeOut = smtTimeOut , SMT.resetInterval = smtResetInterval - , SMT.preludeFile = smtPrelude + , SMT.prelude = smtPrelude } when @@ -310,5 +260,5 @@ mainWithOptions smtResetInterval :: SMT.ResetInterval smtResetInterval = resetInterval smtOptions - smtPrelude :: Maybe FilePath + smtPrelude :: SMT.Prelude smtPrelude = prelude smtOptions From d7fdf2bd8b7a933d264b43eacef8eb71e675f6bd Mon Sep 17 00:00:00 2001 From: ana-pantilie Date: Fri, 23 Oct 2020 14:33:08 +0300 Subject: [PATCH 11/13] Clean-up --- kore/app/exec/Main.hs | 14 +-------- kore/src/Options/SMT.hs | 67 +++++++++++++++++++++++++++-------------- kore/src/SMT.hs | 2 +- 3 files changed, 47 insertions(+), 36 deletions(-) diff --git a/kore/app/exec/Main.hs b/kore/app/exec/Main.hs index 84f6d21a8b..1399a72315 100644 --- a/kore/app/exec/Main.hs +++ b/kore/app/exec/Main.hs @@ -167,9 +167,9 @@ import Kore.Unparser import Options.SMT ( KoreSolverOptions (..) , Solver (..) - , defaultSmtPreludeFilePath , parseKoreSolverOptions , unparseKoreSolverOptions + , writeKoreSolverFiles ) import Pretty ( Doc @@ -470,14 +470,6 @@ defaultDefinitionFilePath KoreExecOptions { koreProveOptions } defaultRtsStatisticsFilePath :: FilePath defaultRtsStatisticsFilePath = "rts-statistics.json" -writeKoreSolverFiles :: KoreSolverOptions -> FilePath -> IO () -writeKoreSolverFiles - KoreSolverOptions { prelude = SMT.Prelude smtPrelude } - reportFile - = - Foldable.for_ smtPrelude - $ flip copyFile (reportFile defaultSmtPreludeFilePath) - writeKoreSearchFiles :: FilePath -> KoreSearchOptions -> IO () writeKoreSearchFiles reportFile KoreSearchOptions { searchFileName } = copyFile searchFileName $ reportFile <> "/searchFile.kore" @@ -520,8 +512,6 @@ writeOptionsAndKoreFiles (reportDirectory defaultDefinitionFilePath opts) Foldable.for_ patternFileName $ flip copyFile (reportDirectory "pgm.kore") - Foldable.for_ unwrappedPrelude - $ flip copyFile (reportDirectory defaultSmtPreludeFilePath) writeKoreSolverFiles koreSolverOptions reportDirectory Foldable.for_ koreSearchOptions (writeKoreSearchFiles reportDirectory) @@ -529,8 +519,6 @@ writeOptionsAndKoreFiles (writeKoreMergeFiles reportDirectory) Foldable.for_ koreProveOptions (writeKoreProveFiles reportDirectory) - where - KoreSolverOptions { prelude = SMT.Prelude unwrappedPrelude } = koreSolverOptions exeName :: ExeName exeName = ExeName "kore-exec" diff --git a/kore/src/Options/SMT.hs b/kore/src/Options/SMT.hs index a962f4f135..ea2e907d8c 100644 --- a/kore/src/Options/SMT.hs +++ b/kore/src/Options/SMT.hs @@ -9,11 +9,13 @@ module Options.SMT , parseKoreSolverOptions , unparseKoreSolverOptions , defaultSmtPreludeFilePath + , writeKoreSolverFiles ) where import Prelude.Kore import qualified Data.Char as Char +import qualified Data.Foldable as Foldable import Data.List ( intercalate ) @@ -30,6 +32,12 @@ import Options.Applicative , value ) import qualified Options.Applicative as Options +import System.Directory + ( copyFile + ) +import System.FilePath + ( () + ) import Data.Limit ( Limit (..) @@ -39,6 +47,7 @@ import SMT hiding ( Solver ) +-- | Command line options for the SMT solver. data KoreSolverOptions = KoreSolverOptions { timeOut :: !TimeOut , resetInterval :: !ResetInterval @@ -49,30 +58,37 @@ data KoreSolverOptions = KoreSolverOptions parseKoreSolverOptions :: Parser KoreSolverOptions parseKoreSolverOptions = KoreSolverOptions - <$> option readSMTTimeOut - ( metavar "SMT_TIMEOUT" - <> long "smt-timeout" - <> help "Timeout for calls to the SMT solver, in milliseconds" - <> value defaultTimeOut - ) - <*> option readSMTResetInterval - ( metavar "SMT_RESET_INTERVAL" - <> long "smt-reset-interval" - <> help "Reset the solver after this number of queries" - <> value defaultResetInterval - ) - <*> - (Prelude <$> - optional + <$> parseTimeOut + <*> parseResetInterval + <*> parsePrelude + <*> parseSolver + where + parseTimeOut = + option readTimeOut + ( metavar "SMT_TIMEOUT" + <> long "smt-timeout" + <> help "Timeout for calls to the SMT solver, in milliseconds" + <> value defaultTimeOut + ) + + parseResetInterval = + option readResetInterval + ( metavar "SMT_RESET_INTERVAL" + <> long "smt-reset-interval" + <> help "Reset the solver after this number of queries" + <> value defaultResetInterval + ) + + parsePrelude = + Prelude + <$> optional ( strOption ( metavar "SMT_PRELUDE" <> long "smt-prelude" <> help "Path to the SMT prelude file" ) ) - ) - <*> parseSolver - where + SMT.Config { timeOut = defaultTimeOut } = SMT.defaultConfig SMT.Config { resetInterval = defaultResetInterval } = SMT.defaultConfig @@ -86,8 +102,8 @@ parseKoreSolverOptions = . unwords $ [optionName, "must be a positive integer."] - readSMTTimeOut = readPositiveInteger (SMT.TimeOut . Limit) "smt-timeout" - readSMTResetInterval = + readTimeOut = readPositiveInteger (SMT.TimeOut . Limit) "smt-timeout" + readResetInterval = readPositiveInteger SMT.ResetInterval "smt-reset-interval" unparseKoreSolverOptions :: KoreSolverOptions -> [String] @@ -107,7 +123,7 @@ unparseKoreSolverOptions , pure $ "--smt " <> fmap Char.toLower (show solver) ] --- | Available SMT solvers +-- | Available SMT solvers. data Solver = Z3 | None deriving (Eq, Ord, Show) deriving (Enum, Bounded) @@ -135,6 +151,13 @@ readSum longName options = do unknown opt = "Unknown " ++ longName ++ " '" ++ opt ++ "'. " known = "Known " ++ longName ++ "s are: " ++ knownOptions ++ "." - defaultSmtPreludeFilePath :: FilePath defaultSmtPreludeFilePath = "prelude.smt2" + +writeKoreSolverFiles :: KoreSolverOptions -> FilePath -> IO () +writeKoreSolverFiles + KoreSolverOptions { prelude = Prelude unwrappedPrelude } + reportFile + = + Foldable.for_ unwrappedPrelude + $ flip copyFile (reportFile defaultSmtPreludeFilePath) diff --git a/kore/src/SMT.hs b/kore/src/SMT.hs index 6cd50fa1af..f37f2cfa93 100644 --- a/kore/src/SMT.hs +++ b/kore/src/SMT.hs @@ -433,7 +433,7 @@ newtype ResetInterval = ResetInterval { getResetInterval :: Integer } deriving (Eq, Ord, Read, Show) --- | TODO: docs +-- | Optional filepath for the SMT prelude. newtype Prelude = Prelude { getPrelude :: Maybe FilePath } -- | Solver configuration From 4130ea13cb4d995c977d0e7661914b3ece81c1b3 Mon Sep 17 00:00:00 2001 From: ana-pantilie Date: Fri, 23 Oct 2020 14:36:29 +0300 Subject: [PATCH 12/13] Clean-up --- kore/app/exec/Main.hs | 12 +----------- kore/src/Options/SMT.hs | 15 +++++++++++++++ 2 files changed, 16 insertions(+), 11 deletions(-) diff --git a/kore/app/exec/Main.hs b/kore/app/exec/Main.hs index 1399a72315..b7a032ddc8 100644 --- a/kore/app/exec/Main.hs +++ b/kore/app/exec/Main.hs @@ -167,6 +167,7 @@ import Kore.Unparser import Options.SMT ( KoreSolverOptions (..) , Solver (..) + , ensureSmtPreludeExists , parseKoreSolverOptions , unparseKoreSolverOptions , writeKoreSolverFiles @@ -535,17 +536,6 @@ main = do parserInfoModifiers Foldable.for_ (localOptions options) mainWithOptions --- | Ensure that the SMT prelude file exists, if specified. -ensureSmtPreludeExists :: KoreSolverOptions -> IO () -ensureSmtPreludeExists KoreSolverOptions { prelude = SMT.Prelude smtPrelude } = - Foldable.traverse_ - (\filePath -> - Monad.whenM - (not <$> doesFileExist filePath) - (error $ "SMT prelude file does not exist: " <> filePath) - ) - smtPrelude - mainWithOptions :: KoreExecOptions -> IO () mainWithOptions execOptions = do let KoreExecOptions { koreLogOptions, koreSolverOptions, bugReport } = execOptions diff --git a/kore/src/Options/SMT.hs b/kore/src/Options/SMT.hs index ea2e907d8c..24508c282f 100644 --- a/kore/src/Options/SMT.hs +++ b/kore/src/Options/SMT.hs @@ -10,10 +10,12 @@ module Options.SMT , unparseKoreSolverOptions , defaultSmtPreludeFilePath , writeKoreSolverFiles + , ensureSmtPreludeExists ) where import Prelude.Kore +import Control.Monad.Extra as Monad import qualified Data.Char as Char import qualified Data.Foldable as Foldable import Data.List @@ -34,6 +36,7 @@ import Options.Applicative import qualified Options.Applicative as Options import System.Directory ( copyFile + , doesFileExist ) import System.FilePath ( () @@ -45,6 +48,7 @@ import Data.Limit ) import SMT hiding ( Solver + , not ) -- | Command line options for the SMT solver. @@ -161,3 +165,14 @@ writeKoreSolverFiles = Foldable.for_ unwrappedPrelude $ flip copyFile (reportFile defaultSmtPreludeFilePath) + +-- | Ensure that the SMT prelude file exists, if specified. +ensureSmtPreludeExists :: KoreSolverOptions -> IO () +ensureSmtPreludeExists KoreSolverOptions { prelude = SMT.Prelude smtPrelude } = + Foldable.traverse_ + (\filePath -> + Monad.whenM + (not <$> doesFileExist filePath) + (error $ "SMT prelude file does not exist: " <> filePath) + ) + smtPrelude From 557784635255100cccd62284dde6633c8cf84a12 Mon Sep 17 00:00:00 2001 From: ana-pantilie Date: Fri, 23 Oct 2020 14:41:38 +0300 Subject: [PATCH 13/13] Clean-up --- kore/src/Options/SMT.hs | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/kore/src/Options/SMT.hs b/kore/src/Options/SMT.hs index 24508c282f..9e8205c531 100644 --- a/kore/src/Options/SMT.hs +++ b/kore/src/Options/SMT.hs @@ -123,7 +123,8 @@ unparseKoreSolverOptions [ (\limit -> unwords ["--smt-timeout", show limit]) <$> maybeLimit Nothing Just unwrappedTimeOut , pure $ unwords ["--smt-reset-interval", show resetInterval] - , unwrappedPrelude $> unwords ["--smt-prelude", defaultSmtPreludeFilePath] + , unwrappedPrelude + $> unwords ["--smt-prelude", defaultSmtPreludeFilePath] , pure $ "--smt " <> fmap Char.toLower (show solver) ] @@ -168,11 +169,14 @@ writeKoreSolverFiles -- | Ensure that the SMT prelude file exists, if specified. ensureSmtPreludeExists :: KoreSolverOptions -> IO () -ensureSmtPreludeExists KoreSolverOptions { prelude = SMT.Prelude smtPrelude } = +ensureSmtPreludeExists + KoreSolverOptions + { prelude = SMT.Prelude unwrappedPrelude } + = Foldable.traverse_ (\filePath -> Monad.whenM (not <$> doesFileExist filePath) (error $ "SMT prelude file does not exist: " <> filePath) ) - smtPrelude + unwrappedPrelude