Skip to content

Commit 089670b

Browse files
ana-pantilieana-pantilie
authored
kore-exec: Add option --solver-reset-interval (#2220)
1 parent a911cea commit 089670b

File tree

4 files changed

+262
-124
lines changed

4 files changed

+262
-124
lines changed

‎kore/app/exec/Main.hs‎

Lines changed: 32 additions & 71 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,7 @@ module Main (main) where
22

33
import Prelude.Kore
44

5+
import qualified Control.Lens as Lens
56
import Control.Monad.Catch
67
( MonadMask
78
, SomeException
@@ -10,11 +11,13 @@ import Control.Monad.Catch
1011
, throwM
1112
)
1213
import Control.Monad.Extra as Monad
13-
import qualified Data.Char as Char
1414
import Data.Default
1515
( def
1616
)
1717
import qualified Data.Foldable as Foldable
18+
import Data.Generics.Product
19+
( field
20+
)
1821
import Data.Limit
1922
( Limit (..)
2023
, maybeLimit
@@ -35,6 +38,7 @@ import qualified Data.Text.IO as Text
3538
( putStrLn
3639
, readFile
3740
)
41+
import qualified GHC.Generics as GHC
3842
import Options.Applicative
3943
( InfoMod
4044
, Parser
@@ -160,6 +164,14 @@ import qualified Kore.Syntax.Definition as Definition.DoNotUse
160164
import Kore.Unparser
161165
( unparse
162166
)
167+
import Options.SMT
168+
( KoreSolverOptions (..)
169+
, Solver (..)
170+
, ensureSmtPreludeExists
171+
, parseKoreSolverOptions
172+
, unparseKoreSolverOptions
173+
, writeKoreSolverFiles
174+
)
163175
import Pretty
164176
( Doc
165177
, Pretty (..)
@@ -172,7 +184,6 @@ import Prof
172184
)
173185
import SMT
174186
( MonadSMT
175-
, TimeOut (..)
176187
)
177188
import qualified SMT
178189
import Stats
@@ -192,7 +203,7 @@ data KoreSearchOptions =
192203
-- ^ The maximum bound on the number of search matches
193204
, searchType :: !SearchType
194205
-- ^ The type of search to perform
195-
}
206+
} deriving (GHC.Generic)
196207

197208
parseKoreSearchOptions :: Parser KoreSearchOptions
198209
parseKoreSearchOptions =
@@ -262,23 +273,6 @@ applyKoreSearchOptions koreSearchOptions@(Just koreSearchOpts) koreExecOpts =
262273
ONE -> Limit 1
263274
_ -> Unlimited
264275

265-
-- | Available SMT solvers
266-
data Solver = Z3 | None
267-
deriving (Eq, Ord, Show)
268-
deriving (Enum, Bounded)
269-
270-
parseSolver :: Parser Solver
271-
parseSolver =
272-
option (snd <$> readSum longName options)
273-
$ metavar "SOLVER"
274-
<> long longName
275-
<> help ("SMT solver for checking constraints: " <> knownOptions)
276-
<> value Z3
277-
where
278-
longName = "smt"
279-
knownOptions = intercalate ", " (map fst options)
280-
options = [ (map Char.toLower $ show s, s) | s <- [minBound .. maxBound] ]
281-
282276
-- | Main options record
283277
data KoreExecOptions = KoreExecOptions
284278
{ definitionFileName :: !FilePath
@@ -289,19 +283,17 @@ data KoreExecOptions = KoreExecOptions
289283
-- ^ Name for file to contain the output pattern
290284
, mainModuleName :: !ModuleName
291285
-- ^ The name of the main module in the definition
292-
, smtTimeOut :: !SMT.TimeOut
293-
, smtPrelude :: !(Maybe FilePath)
294-
, smtSolver :: !Solver
295286
, breadthLimit :: !(Limit Natural)
296287
, depthLimit :: !(Limit Natural)
297288
, strategy :: !(String, [RewriteRule RewritingVariableName] -> Strategy (Prim (RewriteRule RewritingVariableName)))
289+
, koreSolverOptions :: !KoreSolverOptions
298290
, koreLogOptions :: !KoreLogOptions
299291
, koreSearchOptions :: !(Maybe KoreSearchOptions)
300292
, koreProveOptions :: !(Maybe KoreProveOptions)
301293
, koreMergeOptions :: !(Maybe KoreMergeOptions)
302294
, rtsStatistics :: !(Maybe FilePath)
303295
, bugReport :: !BugReport
304-
}
296+
} deriving (GHC.Generic)
305297

306298
-- | Command Line Argument Parser
307299
parseKoreExecOptions :: TimeSpec -> Parser KoreExecOptions
@@ -332,35 +324,17 @@ parseKoreExecOptions startTime =
332324
)
333325
)
334326
<*> parseMainModuleName
335-
<*> option readSMTTimeOut
336-
( metavar "SMT_TIMEOUT"
337-
<> long "smt-timeout"
338-
<> help "Timeout for calls to the SMT solver, in milliseconds"
339-
<> value defaultTimeOut
340-
)
341-
<*> optional
342-
( strOption
343-
( metavar "SMT_PRELUDE"
344-
<> long "smt-prelude"
345-
<> help "Path to the SMT prelude file"
346-
)
347-
)
348-
<*> parseSolver
349327
<*> parseBreadthLimit
350328
<*> parseDepthLimit
351329
<*> parseStrategy
330+
<*> parseKoreSolverOptions
352331
<*> parseKoreLogOptions (ExeName "kore-exec") startTime
353332
<*> pure Nothing
354333
<*> optional parseKoreProveOptions
355334
<*> optional parseKoreMergeOptions
356335
<*> optional parseRtsStatistics
357336
<*> parseBugReport
358-
SMT.Config { timeOut = defaultTimeOut } = SMT.defaultConfig
359-
readSMTTimeOut = do
360-
i <- auto
361-
if i <= 0
362-
then readerError "smt-timeout must be a positive integer."
363-
else return $ SMT.TimeOut $ Limit i
337+
364338
parseBreadthLimit = Limit <$> breadth <|> pure Unlimited
365339
parseDepthLimit = Limit <$> depth <|> pure Unlimited
366340
parseStrategy =
@@ -375,6 +349,7 @@ parseKoreExecOptions startTime =
375349
[ ("any", priorityAnyStrategy)
376350
, ("all", priorityAllStrategy)
377351
]
352+
378353
breadth =
379354
option auto
380355
( metavar "BREADTH"
@@ -387,6 +362,7 @@ parseKoreExecOptions startTime =
387362
<> long "depth"
388363
<> help "Execute up to DEPTH steps."
389364
)
365+
390366
parseMainModuleName =
391367
GlobalMain.parseModuleName
392368
"MODULE"
@@ -446,12 +422,10 @@ koreExecSh
446422
patternFileName
447423
outputFileName
448424
mainModuleName
449-
(TimeOut timeout)
450-
smtPrelude
451-
smtSolver
452425
breadthLimit
453426
depthLimit
454427
strategy
428+
koreSolverOptions
455429
koreLogOptions
456430
koreSearchOptions
457431
koreProveOptions
@@ -474,10 +448,6 @@ koreExecSh
474448
, patternFileName $> "--pattern pgm.kore"
475449
, outputFileName $> "--output result.kore"
476450
, pure $ "--module " <> unpack (getModuleName mainModuleName)
477-
, (\limit -> unwords ["--smt-timeout", show limit])
478-
<$> maybeLimit Nothing Just timeout
479-
, smtPrelude $> unwords ["--smt-prelude", defaultSmtPreludeFilePath]
480-
, pure $ "--smt " <> fmap Char.toLower (show smtSolver)
481451
, (\limit -> unwords ["--breadth", show limit])
482452
<$> maybeLimit Nothing Just breadthLimit
483453
, (\limit -> unwords ["--depth", show limit])
@@ -486,6 +456,7 @@ koreExecSh
486456
, rtsStatistics $>
487457
unwords ["--rts-statistics", defaultRtsStatisticsFilePath]
488458
]
459+
, unparseKoreSolverOptions koreSolverOptions
489460
, unparseKoreLogOptions koreLogOptions
490461
, maybe mempty unparseKoreSearchOptions koreSearchOptions
491462
, maybe mempty unparseKoreProveOptions koreProveOptions
@@ -497,9 +468,6 @@ defaultDefinitionFilePath KoreExecOptions { koreProveOptions }
497468
| isJust koreProveOptions = "vdefinition.kore"
498469
| otherwise = "definition.kore"
499470

500-
defaultSmtPreludeFilePath :: FilePath
501-
defaultSmtPreludeFilePath = "prelude.smt2"
502-
503471
defaultRtsStatisticsFilePath :: FilePath
504472
defaultRtsStatisticsFilePath = "rts-statistics.json"
505473

@@ -527,7 +495,7 @@ writeOptionsAndKoreFiles
527495
opts@KoreExecOptions
528496
{ definitionFileName
529497
, patternFileName
530-
, smtPrelude
498+
, koreSolverOptions
531499
, koreSearchOptions
532500
, koreProveOptions
533501
, koreMergeOptions
@@ -545,8 +513,7 @@ writeOptionsAndKoreFiles
545513
(reportDirectory </> defaultDefinitionFilePath opts)
546514
Foldable.for_ patternFileName
547515
$ flip copyFile (reportDirectory </> "pgm.kore")
548-
Foldable.for_ smtPrelude
549-
$ flip copyFile (reportDirectory </> defaultSmtPreludeFilePath)
516+
writeKoreSolverFiles koreSolverOptions reportDirectory
550517
Foldable.for_ koreSearchOptions
551518
(writeKoreSearchFiles reportDirectory)
552519
Foldable.for_ koreMergeOptions
@@ -569,18 +536,10 @@ main = do
569536
parserInfoModifiers
570537
Foldable.for_ (localOptions options) mainWithOptions
571538

572-
-- | Ensure that the SMT prelude file exists, if specified.
573-
ensureSmtPreludeExists :: Maybe FilePath -> IO ()
574-
ensureSmtPreludeExists =
575-
Foldable.traverse_ $ \filePath ->
576-
Monad.whenM
577-
(not <$> doesFileExist filePath)
578-
(error $ "SMT prelude file does not exist: " <> filePath)
579-
580539
mainWithOptions :: KoreExecOptions -> IO ()
581540
mainWithOptions execOptions = do
582-
let KoreExecOptions { koreLogOptions, bugReport, smtPrelude } = execOptions
583-
ensureSmtPreludeExists smtPrelude
541+
let KoreExecOptions { koreLogOptions, koreSolverOptions, bugReport } = execOptions
542+
ensureSmtPreludeExists koreSolverOptions
584543
exitCode <-
585544
withBugReport Main.exeName bugReport $ \tmpDir -> do
586545
writeOptionsAndKoreFiles tmpDir execOptions
@@ -841,7 +800,7 @@ execute
841800
-> Main r
842801
execute options mainModule worker =
843802
clockSomethingIO "Executing"
844-
$ case smtSolver of
803+
$ case solver of
845804
Z3 -> withZ3
846805
None -> withoutSMT
847806
where
@@ -854,11 +813,13 @@ execute options mainModule worker =
854813
)
855814
worker
856815
withoutSMT = SMT.runNoSMT worker
857-
KoreExecOptions { smtTimeOut, smtPrelude, smtSolver } = options
816+
KoreSolverOptions { timeOut, resetInterval, prelude, solver } =
817+
Lens.view (field @"koreSolverOptions") options
858818
config =
859819
SMT.defaultConfig
860-
{ SMT.timeOut = smtTimeOut
861-
, SMT.preludeFile = smtPrelude
820+
{ SMT.timeOut = timeOut
821+
, SMT.resetInterval = resetInterval
822+
, SMT.prelude = prelude
862823
}
863824

864825
loadPattern :: LoadedModule -> Maybe FilePath -> Main (TermLike VariableName)

‎kore/app/repl/Main.hs‎

Lines changed: 12 additions & 42 deletions
Original file line numberDiff line numberDiff line change
@@ -11,29 +11,22 @@ import Options.Applicative
1111
( InfoMod
1212
, Parser
1313
, argument
14-
, auto
1514
, flag
1615
, fullDesc
1716
, header
1817
, help
1918
, long
2019
, metavar
21-
, option
2220
, progDesc
23-
, readerError
2421
, short
2522
, str
2623
, strOption
27-
, value
2824
)
2925
import System.Exit
3026
( exitFailure
3127
, exitWith
3228
)
3329

34-
import Data.Limit
35-
( Limit (..)
36-
)
3730
import Kore.BugReport
3831
import Kore.Exec
3932
( proveWithRepl
@@ -58,6 +51,10 @@ import Kore.Step.SMT.Lemma
5851
import Kore.Syntax.Module
5952
( ModuleName (..)
6053
)
54+
import Options.SMT
55+
( KoreSolverOptions (..)
56+
, parseKoreSolverOptions
57+
)
6158
import qualified SMT
6259
import System.Clock
6360
( Clock (Monotonic)
@@ -73,17 +70,11 @@ data KoreModule = KoreModule
7370
, moduleName :: !ModuleName
7471
}
7572

76-
-- | SMT Timeout and (optionally) a custom prelude path.
77-
data SmtOptions = SmtOptions
78-
{ timeOut :: !SMT.TimeOut
79-
, prelude :: !(Maybe FilePath)
80-
}
81-
8273
-- | Options for the kore repl.
8374
data KoreReplOptions = KoreReplOptions
8475
{ definitionModule :: !KoreModule
8576
, proveOptions :: !KoreProveOptions
86-
, smtOptions :: !SmtOptions
77+
, smtOptions :: !KoreSolverOptions
8778
, replMode :: !ReplMode
8879
, scriptModeOutput :: !ScriptModeOutput
8980
, replScript :: !ReplScript
@@ -97,7 +88,7 @@ parseKoreReplOptions startTime =
9788
KoreReplOptions
9889
<$> parseMainModule
9990
<*> parseKoreProveOptions
100-
<*> parseSmtOptions
91+
<*> parseKoreSolverOptions
10192
<*> parseReplMode
10293
<*> parseScriptModeOutput
10394
<*> parseReplScript
@@ -116,23 +107,6 @@ parseKoreReplOptions startTime =
116107
"module"
117108
"Kore main module name."
118109

119-
parseSmtOptions :: Parser SmtOptions
120-
parseSmtOptions =
121-
SmtOptions
122-
<$> option readSMTTimeOut
123-
( metavar "SMT_TIMEOUT"
124-
<> long "smt-timeout"
125-
<> help "Timeout for calls to the SMT solver, in miliseconds"
126-
<> value defaultTimeOut
127-
)
128-
<*> optional
129-
( strOption
130-
( metavar "SMT_PRELUDE"
131-
<> long "smt-prelude"
132-
<> help "Path to the SMT prelude file"
133-
)
134-
)
135-
136110
parseReplMode :: Parser ReplMode
137111
parseReplMode =
138112
flag
@@ -163,14 +137,6 @@ parseKoreReplOptions startTime =
163137
)
164138
)
165139

166-
SMT.Config { timeOut = defaultTimeOut } = SMT.defaultConfig
167-
168-
readSMTTimeOut = do
169-
i <- auto
170-
if i <= 0
171-
then readerError "smt-timeout must be a positive integer."
172-
else return $ SMT.TimeOut $ Limit i
173-
174140
parseOutputFile :: Parser OutputFile
175141
parseOutputFile =
176142
OutputFile
@@ -230,7 +196,8 @@ mainWithOptions
230196
smtConfig =
231197
SMT.defaultConfig
232198
{ SMT.timeOut = smtTimeOut
233-
, SMT.preludeFile = smtPrelude
199+
, SMT.resetInterval = smtResetInterval
200+
, SMT.prelude = smtPrelude
234201
}
235202

236203
when
@@ -290,5 +257,8 @@ mainWithOptions
290257
smtTimeOut :: SMT.TimeOut
291258
smtTimeOut = timeOut smtOptions
292259

293-
smtPrelude :: Maybe FilePath
260+
smtResetInterval :: SMT.ResetInterval
261+
smtResetInterval = resetInterval smtOptions
262+
263+
smtPrelude :: SMT.Prelude
294264
smtPrelude = prelude smtOptions

0 commit comments

Comments
 (0)