Retry SMT query once if it fails (#2224)

* Retry SMT query once if it fails

* checkPredicate: only run SMT.check

* decidePredicate: Restart query after first failure

* Clean-up: remove empty

* Clean-up: use MaybeT instance of MonadSMT

* Update kore/src/Kore/Log/ErrorDecidePredicateUnknown.hs

Co-authored-by: Thomas Tuegel <[email protected]>

* Update WarnRetrySolverQuery.hs

Co-authored-by: Thomas Tuegel <[email protected]>

Author: ana-pantilie

kore/src/Kore/Log/ErrorDecidePredicateUnknown.hs

@@ -58,7 +58,7 @@ instance Entry ErrorDecidePredicateUnknown where
 errorDecidePredicateUnknown
     :: InternalVariable variable
     => NonEmpty (Predicate variable)
-    -> log ()
+    -> log a
 errorDecidePredicateUnknown predicates' =
     throw ErrorDecidePredicateUnknown { predicates }
   where

kore/src/Kore/Log/Registry.hs

@@ -101,6 +101,9 @@ import Kore.Log.WarnFunctionWithoutEvaluators
 import Kore.Log.WarnIfLowProductivity
     ( WarnIfLowProductivity
     )
+import Kore.Log.WarnRetrySolverQuery
+    ( WarnRetrySolverQuery
+    )
 import Kore.Log.WarnStuckClaimState
     ( WarnStuckClaimState
     )
@@ -160,6 +163,7 @@ entryHelpDocs :: [Pretty.Doc ()]
     , mk $ Proxy @WarnStuckClaimState
     , mk $ Proxy @WarnIfLowProductivity
     , mk $ Proxy @WarnTrivialClaim
+    , mk $ Proxy @WarnRetrySolverQuery
     , mk $ Proxy @DebugEvaluateCondition
     , mk $ Proxy @ErrorException
     , mk $ Proxy @ErrorRewriteLoop

kore/src/Kore/Log/WarnRetrySolverQuery.hs

@@ -0,0 +1,68 @@
+{- |
+Copyright   : (c) Runtime Verification, 2020
+License     : NCSA
+
+-}
+
+module Kore.Log.WarnRetrySolverQuery
+    ( WarnRetrySolverQuery
+    , warnRetrySolverQuery
+    ) where
+
+import Prelude.Kore
+
+import Kore.Internal.Predicate
+    ( Predicate
+    )
+import qualified Kore.Internal.Predicate as Predicate
+import Kore.Internal.Variable
+    ( InternalVariable
+    , VariableName
+    , toVariableName
+    )
+import Kore.Unparser
+    ( unparse
+    )
+import Log
+import Pretty
+    ( Pretty (..)
+    )
+import qualified Pretty
+
+newtype WarnRetrySolverQuery =
+    WarnRetrySolverQuery
+        { predicates :: NonEmpty (Predicate VariableName) }
+    deriving (Show)
+
+instance Pretty WarnRetrySolverQuery where
+    pretty WarnRetrySolverQuery { predicates } =
+        Pretty.vsep $
+        [ "The SMT solver initially failed to solve the following query:"
+        , Pretty.indent 2 "Decide predicate:"
+        , Pretty.indent 4 (unparse predicate)
+        , Pretty.indent 2 "with side conditions:"
+        ]
+        <> fmap (Pretty.indent 4 . unparse) sideConditions
+        <> ["The SMT solver was reset and the query\
+            \ was tried one more time."
+           ]
+      where
+        predicate :| sideConditions = predicates
+
+instance Entry WarnRetrySolverQuery where
+    entrySeverity _ = Warning
+    helpDoc _ =
+        "warning raised when the solver failed to decide\
+        \ the satisfiability of a formula, indicating that\
+        \ the solver was reset and the formula retried"
+
+warnRetrySolverQuery
+    :: InternalVariable variable
+    => MonadLog log
+    => NonEmpty (Predicate variable)
+    -> log ()
+warnRetrySolverQuery predicates' =
+    logEntry WarnRetrySolverQuery { predicates }
+  where
+    predicates =
+        Predicate.mapVariables (pure toVariableName) <$> predicates'

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

@@ -18,7 +18,8 @@ module Kore.Step.SMT.Evaluator
 import Prelude.Kore
 
 import Control.Error
-    ( hoistMaybe
+    ( MaybeT
+    , hoistMaybe
     , runMaybeT
     )
 import qualified Control.Lens as Lens
@@ -65,6 +66,9 @@ import Kore.Log.DebugEvaluateCondition
 import Kore.Log.ErrorDecidePredicateUnknown
     ( errorDecidePredicateUnknown
     )
+import Kore.Log.WarnRetrySolverQuery
+    ( warnRetrySolverQuery
+    )
 import Kore.Step.Simplification.Simplify as Simplifier
 import Kore.Step.SMT.Translate
 import Kore.TopBottom
@@ -172,19 +176,37 @@ decidePredicate
     => NonEmpty (Predicate variable)
     -> simplifier (Maybe Bool)
 decidePredicate predicates =
-    whileDebugEvaluateCondition predicates
-    $ SMT.withSolver $ runMaybeT $ evalTranslator $ do
-        tools <- Simplifier.askMetadataTools
-        predicates' <- traverse (translatePredicate tools) predicates
-        Foldable.traverse_ SMT.assert predicates'
-        result <- SMT.check
-        debugEvaluateConditionResult result
-        case result of
-            Unsat -> return False
-            Sat -> empty
-            Unknown -> do
-                errorDecidePredicateUnknown predicates
-                empty
+    whileDebugEvaluateCondition predicates go
+  where
+    go =
+        do
+            result <- query >>= whenUnknown retry
+            debugEvaluateConditionResult result
+            case result of
+                Unsat -> return False
+                Sat -> empty
+                Unknown ->
+                    errorDecidePredicateUnknown predicates
+        & runMaybeT
+
+    whenUnknown f Unknown = f
+    whenUnknown _ result  = return result
+
+    -- | Run the SMT query once.
+    query :: MaybeT simplifier Result
+    query =
+        SMT.withSolver $ evalTranslator $ do
+            tools <- Simplifier.askMetadataTools
+            predicates' <- traverse (translatePredicate tools) predicates
+            Foldable.traverse_ SMT.assert predicates'
+            SMT.check
+
+    -- | Re-run the SMT query.
+    retry = do
+        SMT.reinit
+        result <- query
+        warnRetrySolverQuery predicates
+        return result
 
 translatePredicate
     :: forall variable m.