Implement --smt-retry-limit option (#3166)

Author: JKTKops

kore/src/Kore/Rewrite/SMT/Evaluator.hs

@@ -22,6 +22,7 @@ import Control.Lens qualified as Lens
 import Control.Monad.Counter qualified as Counter
 import Control.Monad.State.Strict qualified as State
 import Data.Generics.Product.Fields
+import Data.Limit
 import Data.Map.Strict qualified as Map
 import Data.Set qualified as Set
 import Data.Text qualified as Text
@@ -171,6 +172,7 @@ decidePredicate sideCondition predicates =
 
     whenUnknown f Unknown = f
     whenUnknown _ result = return result
+
     query :: MaybeT simplifier Result
     query =
         SMT.withSolver . evalTranslator $ do
@@ -182,9 +184,33 @@ decidePredicate sideCondition predicates =
             traverse_ SMT.assert predicates'
             SMT.check
 
+    retry :: MaybeT simplifier Result
     retry = do
+        SMT.RetryLimit limit <- SMT.askRetryLimit
+        -- Use the same timeout for the first retry, since sometimes z3
+        -- decides it doesn't want to work today and all we need is to
+        -- retry it once.
+        let timeoutScales = takeWithin limit [1 ..]
+        let retryActions = map retryOnceWithScaledTimeout timeoutScales
+        let combineRetries r1 r2 = r1 >>= whenUnknown r2
+        -- This works even if 'retryActions' is infinite, because the second
+        -- argument to 'whenUnknown' will be the 'combineRetries' of all of
+        -- the tail of the list. As soon as a result is not 'Unknown', the
+        -- rest of the fold is discarded.
+        foldr combineRetries (pure Unknown) retryActions
+
+    retryOnceWithScaledTimeout :: Integer -> MaybeT simplifier Result
+    retryOnceWithScaledTimeout scale =
+        -- scale the timeout _inside_ 'retryOnce' so that we override the
+        -- call to 'SMT.reinit'.
+        retryOnce $ SMT.localTimeOut (scaleTimeOut scale) query
+
+    scaleTimeOut _ (SMT.TimeOut Unlimited) = SMT.TimeOut Unlimited
+    scaleTimeOut n (SMT.TimeOut (Limit r)) = SMT.TimeOut (Limit (n * r))
+
+    retryOnce actionToRetry = do
         SMT.reinit
-        result <- query
+        result <- actionToRetry
         debugRetrySolverQuery predicates
         return result
 

kore/src/Options/SMT.hs

@@ -52,6 +52,7 @@ import System.FilePath (
 -- | Command line options for the SMT solver.
 data KoreSolverOptions = KoreSolverOptions
     { timeOut :: !TimeOut
+    , retryLimit :: !RetryLimit
     , rLimit :: !RLimit
     , resetInterval :: !ResetInterval
     , prelude :: !Prelude
@@ -62,6 +63,7 @@ parseKoreSolverOptions :: Parser KoreSolverOptions
 parseKoreSolverOptions =
     KoreSolverOptions
         <$> parseTimeOut
+        <*> parseRetryLimit
         <*> parseRLimit
         <*> parseResetInterval
         <*> parsePrelude
@@ -76,6 +78,15 @@ parseKoreSolverOptions =
                 <> value defaultTimeOut
             )
 
+    parseRetryLimit =
+        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
+            )
+
     parseRLimit =
         option
             readRLimit
@@ -106,12 +117,14 @@ parseKoreSolverOptions =
 
     SMT.Config
         { timeOut = defaultTimeOut
+        , retryLimit = defaultRetryLimit
         , rLimit = defaultRLimit
         , resetInterval = defaultResetInterval
         } =
             SMT.defaultConfig
 
     readTimeOut = readPositiveIntegral (SMT.TimeOut . Limit) "smt-timeout"
+    readRetryLimit = readPositiveIntegral (SMT.RetryLimit . Limit) "smt-retry-limit"
     readRLimit = readPositiveIntegral (SMT.RLimit . Limit) "smt-rlimit"
     readResetInterval =
         readPositiveIntegral SMT.ResetInterval "smt-reset-interval"
@@ -120,6 +133,7 @@ unparseKoreSolverOptions :: KoreSolverOptions -> [String]
 unparseKoreSolverOptions
     KoreSolverOptions
         { timeOut = TimeOut unwrappedTimeOut
+        , retryLimit = RetryLimit unwrappedRetryLimit
         , rLimit = RLimit unwrappedRLimit
         , resetInterval
         , prelude = Prelude unwrappedPrelude
@@ -128,6 +142,8 @@ unparseKoreSolverOptions
         catMaybes
             [ (\limit -> unwords ["--smt-timeout", show limit])
                 <$> maybeLimit Nothing Just unwrappedTimeOut
+            , (\limit -> unwords ["--smt-retry-limit", show limit])
+                <$> maybeLimit Nothing Just unwrappedRetryLimit
             , (\limit -> unwords ["--smt-rlimit", show limit])
                 <$> maybeLimit Nothing Just unwrappedRLimit
             , pure $

kore/src/SMT.hs

@@ -26,9 +26,12 @@ module SMT (
     ackCommand,
     loadFile,
     reinit,
+    askRetryLimit,
+    localTimeOut,
     Config (..),
     defaultConfig,
     TimeOut (..),
+    RetryLimit (..),
     RLimit (..),
     ResetInterval (..),
     Prelude (..),
@@ -216,6 +219,11 @@ reinit :: MonadSMT m => m ()
 reinit = liftSMT reinitSMT
 {-# INLINE reinit #-}
 
+-- | Get the retry limit from the SMT
+askRetryLimit :: MonadSMT m => m RetryLimit
+askRetryLimit = liftSMT askRetryLimitSMT
+{-# INLINE askRetryLimit #-}
+
 -- * Implementation
 
 data SolverSetup = SolverSetup
@@ -376,6 +384,10 @@ instance MonadSMT m => MonadSMT (RWST r () s m)
 newtype TimeOut = TimeOut {getTimeOut :: Limit Integer}
     deriving stock (Eq, Ord, Read, Show)
 
+-- | Retry-limit for SMT queries.
+newtype RetryLimit = RetryLimit {getRetryLimit :: Limit Integer}
+    deriving stock (Eq, Ord, Read, Show)
+
 -- | Resource-limit for SMT queries.
 newtype RLimit = RLimit {getRLimit :: Limit Integer}
     deriving stock (Eq, Ord, Read, Show)
@@ -399,6 +411,8 @@ data Config = Config
       logFile :: !(Maybe FilePath)
     , -- | query time limit
       timeOut :: !TimeOut
+    , -- | query retry limit
+      retryLimit :: !RetryLimit
     , -- | query resource limit
       rLimit :: !RLimit
     , -- | reset solver after this number of queries
@@ -417,6 +431,7 @@ defaultConfig =
         , prelude = Prelude Nothing
         , logFile = Nothing
         , timeOut = TimeOut (Limit 40)
+        , retryLimit = RetryLimit (Limit 1)
         , rLimit = RLimit Unlimited
         , resetInterval = ResetInterval 100
         }
@@ -605,6 +620,29 @@ reinitSMT =
         Nothing -> return ()
         Just solverSetup -> reinitSMT' solverSetup
 
+{- | Run a solver action with an adjusted timeout,
+ and reset the timeout when it's done.
+-}
+localTimeOut :: MonadSMT m => (TimeOut -> TimeOut) -> m a -> m a
+localTimeOut adjust isolated = do
+    originalTimeOut <- liftSMT extractTimeOut
+    setTimeOut $ adjust originalTimeOut
+    isolated <* setTimeOut originalTimeOut
+  where
+    extractTimeOut =
+        SMT $
+            pure . \case
+                Nothing -> TimeOut Unlimited
+                Just setup -> timeOut $ config setup
+
+-- | Get the retry limit for SMT queries.
+askRetryLimitSMT :: SMT RetryLimit
+askRetryLimitSMT =
+    SMT $
+        pure . \case
+            Nothing -> RetryLimit (Limit 0)
+            Just setup -> retryLimit $ config setup
+
 -- --------------------------------
 -- Internal