Booster flag to disable simplification before fall-back request (#3825)

Logs are showing that the simplification performed before fall-back
execute requests is often not productive. This PR provides a server flag
to switch it off and save the overhead.

OTOH, the simplification may prune spurious branches, saving a
`Branching` re-execution in `kore-rpc` in some cases. Therefore the
default behaviour is still to simplify before fallback requests.

Author: jberthold

booster/tools/booster/Proxy.hs

@@ -69,6 +69,7 @@ data ProxyConfig = ProxyConfig
     , boosterState :: MVar.MVar Booster.ServerState
     , fallbackReasons :: [HaltReason]
     , simplifyAtEnd :: Bool
+    , simplifyBeforeFallback :: Bool
     , customLogLevels :: ![Log.LogLevel]
     }
 
@@ -353,7 +354,10 @@ respondEither cfg@ProxyConfig{statsVar, boosterState} booster kore req = case re
                         "Booster " <> show boosterResult.reason <> " at " <> show boosterResult.depth
                     -- simplify Booster's state with Kore's simplifier
                     Log.logInfoNS "proxy" . Text.pack $ "Simplifying booster state and falling back to Kore "
-                    simplifyResult <- simplifyExecuteState logSettings r._module def boosterResult.state
+                    simplifyResult <-
+                        if cfg.simplifyBeforeFallback
+                            then simplifyExecuteState logSettings r._module def boosterResult.state
+                            else pure $ Right (boosterResult.state, Nothing)
                     case simplifyResult of
                         Left logsOnly -> do
                             -- state was simplified to \bottom, return vacuous

booster/tools/booster/Server.hs

@@ -112,6 +112,7 @@ main = do
                     , boosterSMT
                     , fallbackReasons
                     , simplifyAtEnd
+                    , simplifyBeforeFallback
                     }
             } = options
         (logLevel, customLevels) = adjustLogLevels logLevels
@@ -220,6 +221,7 @@ main = do
                                 , boosterState
                                 , fallbackReasons
                                 , simplifyAtEnd
+                                , simplifyBeforeFallback
                                 , customLogLevels = customLevels
                                 }
                         server =
@@ -286,6 +288,8 @@ data ProxyOptions = ProxyOptions
     -- ^ halt reasons to re-execute (fallback) to double-check the result
     , simplifyAtEnd :: Bool
     -- ^ whether to run a post-exec simplification
+    , simplifyBeforeFallback :: Bool
+    -- ^ whether to run a simplification before fall-back execute requests
     }
 
 parserInfoModifiers :: InfoMod options
@@ -334,6 +338,12 @@ clProxyOptionsParser =
                 ( long "no-post-exec-simplify"
                     <> help "disable post-exec simplification"
                 )
+            <*> flag
+                True
+                False
+                ( long "no-fallback-simplify"
+                    <> help "disable simplification before fallback requests"
+                )
 
     reasonReader :: String -> Either String HaltReason
     reasonReader = \case