Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add --kore-fallback-depth <N> to kore-rpc-booster #305

Draft
wants to merge 5 commits into
base: main
Choose a base branch
from
Draft

Add --kore-fallback-depth <N> to kore-rpc-booster #305

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
da3b6a4
Add `--kore-fallback-depth <N>` to `kore-rpc-booster`
geo2a Sep 11, 2023
3ec883c
Merge remote-tracking branch 'origin/main' into georgy/revert-to-kore…
geo2a Sep 14, 2023
322a6e9
Merge branch 'main' into georgy/revert-to-kore-for-depth-N
PetarMax Sep 20, 2023
a0212ec
Merge branch 'main' into georgy/revert-to-kore-for-depth-N
PetarMax Sep 25, 2023
4ec656f
Merge branch 'main' into georgy/revert-to-kore-for-depth-N
PetarMax Oct 4, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 3 additions & 2 deletions tools/booster/Proxy.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -62,10 +62,11 @@ respondEither ::
Log.MonadLogger m =>
MonadIO m =>
Maybe StatsVar ->
Depth ->
Respond (API 'Req) m (API 'Res) ->
Respond (API 'Req) m (API 'Res) ->
Respond (API 'Req) m (API 'Res)
respondEither mbStatsVar booster kore req = case req of
respondEither mbStatsVar koreFallbackDepth booster kore req = case req of
Execute execReq
| isJust execReq.stepTimeout || isJust execReq.movingAverageStepTimeout ->
loggedKore ExecuteM req
Expand Down Expand Up @@ -215,7 +216,7 @@ respondEither mbStatsVar booster kore req = case req of
( Execute
r
{ state = execStateToKoreJson simplifiedBoosterState
, maxDepth = Just $ Depth 1
, maxDepth = Just koreFallbackDepth
}
)
when (isJust mbStatsVar) $
Expand Down
28 changes: 24 additions & 4 deletions tools/booster/Server.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -50,7 +50,7 @@ import Kore.JsonRpc (ServerState (..))
import Kore.JsonRpc qualified as Kore
import Kore.JsonRpc.Error
import Kore.JsonRpc.Server
import Kore.JsonRpc.Types (API, ReqOrRes (Req, Res))
import Kore.JsonRpc.Types (API, Depth (..), ReqOrRes (Req, Res))
import Kore.Log (
ExeName (..),
KoreLogType (LogSomeAction),
Expand All @@ -62,6 +62,7 @@ import Kore.Log (
)
import Kore.Log qualified as Log
import Kore.Log.DebugSolver qualified as Log
import Kore.Parser.ParserUtils (readPositiveIntegral)
import Kore.Rewrite.SMT.Lemma (declareSMTLemmas)
import Kore.Syntax.Definition (ModuleName (ModuleName), SentenceAxiom)
import Options.SMT (KoreSolverOptions (..), parseKoreSolverOptions)
Expand All @@ -85,7 +86,7 @@ main = do
, eventlogEnabledUserEvents
}
, koreSolverOptions
, proxyOptions = ProxyOptions{printStats}
, proxyOptions = ProxyOptions{printStats, koreFallbackDepth}
, debugSolverOptions
} = options
(logLevel, customLevels) = adjustLogLevels logLevels
Expand Down Expand Up @@ -142,7 +143,7 @@ main = do
server =
jsonRpcServer
srvSettings
(const $ Proxy.respondEither statVar boosterRespond koreRespond)
(const $ Proxy.respondEither statVar koreFallbackDepth boosterRespond koreRespond)
[handleErrorCall, handleSomeException]
interruptHandler _ = do
when (logLevel >= LevelInfo) $
Expand Down Expand Up @@ -177,9 +178,11 @@ data CLProxyOptions = CLProxyOptions
, debugSolverOptions :: !Log.DebugSolverOptions
}

newtype ProxyOptions = ProxyOptions
data ProxyOptions = ProxyOptions
{ printStats :: Bool
-- ^ print timing statistics per request and on shutdown
, koreFallbackDepth :: Depth
-- ^ maximum number of rewriting steps to be preformed when falling back to Kore
}

parserInfoModifiers :: InfoMod options
Expand All @@ -201,6 +204,23 @@ clProxyOptionsParser =
( long "print-stats"
<> help "(development) Print timing information per request and on shutdown"
)
<*> option
readKoreFallpackLimit
( long "kore-fallback-depth"
<> help "Maximum number of rewriting steps to be preformed when falling back to Kore"
<> value defaultKoreFallpackLimit
)
where
readKoreFallpackLimit = readPositiveIntegral Depth "kore-fallback-depth"
defaultKoreFallpackLimit = 1

-- option
-- readRetryLimit
-- ( metavar "SMT_RETRY_LIMIT"
-- <> long "smt-retry-limit"
-- <> help "Limit how many times an SMT query can be retried (with scaling timeouts)"
-- <> value defaultRetryLimit
-- )

mkKoreServer :: Log.LoggerEnv IO -> CLOptions -> KoreSolverOptions -> IO KoreServer
mkKoreServer loggerEnv@Log.LoggerEnv{logAction} CLOptions{definitionFile, mainModuleName} koreSolverOptions =
Expand Down