SMT retry logic changes in Kore (#3860)

Fixes #3859 * if a query returns unknown, do not retry with the same timeout, use double the timeout. Scale further timeouts quadratically, rather than linearly. * do not retry when applying simplifications * add context logs for unknown predicates --------- Co-authored-by: rv-jenkins <[email protected]>
runtimeverification · May 20, 2024 · f1d4ba6 · f1d4ba6
1 parent b373660
commit f1d4ba6
Show file tree

Hide file tree

Showing 2 changed files with 30 additions and 7 deletions.
diff --git a/kore/src/Kore/Log/DecidePredicateUnknown.hs b/kore/src/Kore/Log/DecidePredicateUnknown.hs
@@ -32,6 +32,7 @@ import Kore.Internal.Predicate qualified as Predicate
 import Kore.Internal.TermLike qualified as TermLike
 import Kore.Internal.Variable
 import Kore.Syntax.Json qualified as PatternJson
+import Kore.Unparser (unparse)
 import Language.Haskell.TH.Syntax (Exp, Loc (..), Q, qLocation)
 import Log
 import Prelude.Kore
@@ -101,7 +102,23 @@ instance Entry DecidePredicateUnknown where
       where
         prettyHsLoc Loc{loc_module, loc_start = (row, col)} =
             Pretty.pretty loc_module <> ":" <> Pretty.pretty row <> ":" <> Pretty.pretty col
-    oneLineDoc _ = "DecidePredicateUnknown"
+    oneLineDoc (DecidePredicateUnknown{message, predicates}) =
+        Pretty.hsep
+            [ Pretty.brackets "smt"
+            , Pretty.pretty description
+            , unparse
+                ( Predicate.fromPredicate
+                    sortBool
+                    predicate
+                )
+            ]
+      where
+        predicate = Predicate.makeMultipleAndPredicate . toList $ predicates
+        description =
+            "solver returned unknwon with reason "
+                <> message
+                <> " for predicate "
+
     helpDoc _ =
         "error or a warning when the solver cannot decide the satisfiability of a formula"
 
@@ -125,6 +142,10 @@ externaliseDecidePredicateUnknown :: DecidePredicateUnknown -> (Text, PatternJso
 externaliseDecidePredicateUnknown err@DecidePredicateUnknown{message} =
     ( message
     , PatternJson.fromPredicate
-        (TermLike.SortActualSort $ TermLike.SortActual (TermLike.Id "SortBool" TermLike.AstLocationNone) [])
+        sortBool
         (Predicate.makeMultipleAndPredicate . toList $ predicates err)
     )
+
+sortBool :: TermLike.Sort
+sortBool =
+    (TermLike.SortActualSort $ TermLike.SortActual (TermLike.Id "SortBool" TermLike.AstLocationNone) [])
diff --git a/kore/src/Kore/Rewrite/SMT/Evaluator.hs b/kore/src/Kore/Rewrite/SMT/Evaluator.hs
@@ -169,7 +169,11 @@ decidePredicate ::
 decidePredicate onUnknown sideCondition predicates =
     whileDebugEvaluateCondition predicates $
         do
-            result <- query >>= whenUnknown retry
+            result <- case onUnknown of
+                -- do not retry the query on Unknown if the use-case is "soft", i.e. applying simplifications
+                WarnDecidePredicateUnknown _ _ -> query
+                -- if Unknown leads to a hard error, retry the query with scaled timeouts
+                ErrorDecidePredicateUnknown _ _ -> query >>= whenUnknown retry
             debugEvaluateConditionResult result
             case result of
                 Unsat -> return False
@@ -206,10 +210,8 @@ decidePredicate onUnknown sideCondition predicates =
 retryWithScaledTimeout :: MonadSMT m => m Result -> m Result
 retryWithScaledTimeout q = 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 ..]
+    -- the timeout is doubled for every retry
+    let timeoutScales = takeWithin limit . map (2 ^) $ [1 :: Integer ..]
         retryActions = map (retryOnceWithScaledTimeout q) timeoutScales
         combineRetries [] = pure $ Unknown "retry limit is 0"
         combineRetries [r] = r