Skip to content

Commit

Permalink
Add --solver-transcript option to the booster (#228)
Browse files Browse the repository at this point in the history
Fixes #218
  • Loading branch information
goodlyrottenapple authored Jul 11, 2023
1 parent 09692d6 commit c28d5ff
Showing 1 changed file with 5 additions and 0 deletions.
5 changes: 5 additions & 0 deletions tools/booster/Server.hs
Original file line number Diff line number Diff line change
Expand Up @@ -61,6 +61,7 @@ import Kore.Log (
withLogger,
)
import Kore.Log qualified as Log
import Kore.Log.DebugSolver qualified as Log
import Kore.Rewrite.SMT.Lemma (declareSMTLemmas)
import Kore.Syntax.Definition (ModuleName (ModuleName), SentenceAxiom)
import Options.SMT (KoreSolverOptions (..), parseKoreSolverOptions)
Expand All @@ -85,6 +86,7 @@ main = do
}
, koreSolverOptions
, proxyOptions = ProxyOptions{printStats}
, debugSolverOptions
} = options
(logLevel, customLevels) = adjustLogLevels logLevels
levelFilter :: Logger.LogSource -> LogLevel -> Bool
Expand Down Expand Up @@ -113,6 +115,7 @@ main = do
(defaultKoreLogOptions (ExeName "") startTime)
{ Log.logLevel = coLogLevel
, Log.timestampsSwitch = TimestampsDisable
, Log.debugSolverOptions = debugSolverOptions
, Log.logType = LogSomeAction $ LogAction $ \txt -> liftIO $ monadLogger defaultLoc "kore" logLevel $ toLogStr txt
}
srvSettings = serverSettings port "*"
Expand Down Expand Up @@ -171,6 +174,7 @@ data CLProxyOptions = CLProxyOptions
{ clOptions :: CLOptions
, proxyOptions :: ProxyOptions
, koreSolverOptions :: !KoreSolverOptions
, debugSolverOptions :: !Log.DebugSolverOptions
}

newtype ProxyOptions = ProxyOptions
Expand All @@ -189,6 +193,7 @@ clProxyOptionsParser =
<$> clOptionsParser
<*> parseProxyOptions
<*> parseKoreSolverOptions
<*> Log.parseDebugSolverOptions
where
parseProxyOptions =
ProxyOptions
Expand Down

0 comments on commit c28d5ff

Please sign in to comment.