From 7ecea69cb996bddb7d2dc54b6442fb6c437ba9de Mon Sep 17 00:00:00 2001 From: ana-pantilie <45069775+ana-pantilie@users.noreply.github.com> Date: Thu, 29 Oct 2020 11:49:22 +0200 Subject: [PATCH] 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 * Update WarnRetrySolverQuery.hs Co-authored-by: Thomas Tuegel --- .../Kore/Log/ErrorDecidePredicateUnknown.hs | 2 +- kore/src/Kore/Log/Registry.hs | 4 ++ kore/src/Kore/Log/WarnRetrySolverQuery.hs | 68 +++++++++++++++++++ kore/src/Kore/Step/SMT/Evaluator.hs | 50 ++++++++++---- 4 files changed, 109 insertions(+), 15 deletions(-) create mode 100644 kore/src/Kore/Log/WarnRetrySolverQuery.hs diff --git a/kore/src/Kore/Log/ErrorDecidePredicateUnknown.hs b/kore/src/Kore/Log/ErrorDecidePredicateUnknown.hs index 6089596358..29d7e1a888 100644 --- a/kore/src/Kore/Log/ErrorDecidePredicateUnknown.hs +++ b/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 diff --git a/kore/src/Kore/Log/Registry.hs b/kore/src/Kore/Log/Registry.hs index 55dae5e863..1766a1a68a 100644 --- a/kore/src/Kore/Log/Registry.hs +++ b/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 diff --git a/kore/src/Kore/Log/WarnRetrySolverQuery.hs b/kore/src/Kore/Log/WarnRetrySolverQuery.hs new file mode 100644 index 0000000000..b412e7d8a3 --- /dev/null +++ b/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' diff --git a/kore/src/Kore/Step/SMT/Evaluator.hs b/kore/src/Kore/Step/SMT/Evaluator.hs index 6071592ea5..fd935197d8 100644 --- a/kore/src/Kore/Step/SMT/Evaluator.hs +++ b/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.