From b7f117e4703065ebcce3616215e6882dc132ead7 Mon Sep 17 00:00:00 2001 From: ana-pantilie Date: Fri, 23 Oct 2020 19:12:39 +0300 Subject: [PATCH 1/7] Retry SMT query once if it fails --- kore/src/Kore/Log/Registry.hs | 4 ++ kore/src/Kore/Log/WarnRetrySolverQuery.hs | 68 +++++++++++++++++++++++ kore/src/Kore/Step/SMT/Evaluator.hs | 20 ++++++- 3 files changed, 91 insertions(+), 1 deletion(-) create mode 100644 kore/src/Kore/Log/WarnRetrySolverQuery.hs 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..ac35598b92 --- /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 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 will be reset and the query\ + \ will be 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 will be 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..079393c8ca 100644 --- a/kore/src/Kore/Step/SMT/Evaluator.hs +++ b/kore/src/Kore/Step/SMT/Evaluator.hs @@ -65,6 +65,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 @@ -174,12 +177,27 @@ decidePredicate decidePredicate predicates = whileDebugEvaluateCondition predicates $ SMT.withSolver $ runMaybeT $ evalTranslator $ do + result <- checkPredicate + -- for testing: + -- retryCheckPredicateOnce + case result of + Unsat -> return False + Sat -> empty + Unknown -> retryCheckPredicateOnce + where + checkPredicate = do tools <- Simplifier.askMetadataTools predicates' <- traverse (translatePredicate tools) predicates Foldable.traverse_ SMT.assert predicates' result <- SMT.check debugEvaluateConditionResult result - case result of + return result + + retryCheckPredicateOnce = do + SMT.reinit + warnRetrySolverQuery predicates + retriedResult <- checkPredicate + case retriedResult of Unsat -> return False Sat -> empty Unknown -> do From f4ca11d50553e586b022c27842a8346524e088e4 Mon Sep 17 00:00:00 2001 From: ana-pantilie Date: Fri, 23 Oct 2020 19:24:01 +0300 Subject: [PATCH 2/7] checkPredicate: only run SMT.check --- kore/src/Kore/Step/SMT/Evaluator.hs | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/kore/src/Kore/Step/SMT/Evaluator.hs b/kore/src/Kore/Step/SMT/Evaluator.hs index 079393c8ca..077900380d 100644 --- a/kore/src/Kore/Step/SMT/Evaluator.hs +++ b/kore/src/Kore/Step/SMT/Evaluator.hs @@ -177,18 +177,18 @@ decidePredicate decidePredicate predicates = whileDebugEvaluateCondition predicates $ SMT.withSolver $ runMaybeT $ evalTranslator $ do + tools <- Simplifier.askMetadataTools + predicates' <- traverse (translatePredicate tools) predicates + Foldable.traverse_ SMT.assert predicates' result <- checkPredicate - -- for testing: - -- retryCheckPredicateOnce + -- TODO: for testing, remember to remove + let result = Unknown case result of Unsat -> return False Sat -> empty Unknown -> retryCheckPredicateOnce where checkPredicate = do - tools <- Simplifier.askMetadataTools - predicates' <- traverse (translatePredicate tools) predicates - Foldable.traverse_ SMT.assert predicates' result <- SMT.check debugEvaluateConditionResult result return result From ee8702a81ff7aaedb1f9525c17b1f459a7ea54e4 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Tue, 27 Oct 2020 05:47:52 -0500 Subject: [PATCH 3/7] decidePredicate: Restart query after first failure --- kore/src/Kore/Step/SMT/Evaluator.hs | 57 ++++++++++++++++------------- 1 file changed, 32 insertions(+), 25 deletions(-) diff --git a/kore/src/Kore/Step/SMT/Evaluator.hs b/kore/src/Kore/Step/SMT/Evaluator.hs index 077900380d..0b15377d97 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 (MaybeT) + , hoistMaybe , runMaybeT ) import qualified Control.Lens as Lens @@ -175,34 +176,40 @@ 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 <- checkPredicate - -- TODO: for testing, remember to remove - let result = Unknown - case result of - Unsat -> return False - Sat -> empty - Unknown -> retryCheckPredicateOnce + whileDebugEvaluateCondition predicates go where - checkPredicate = do - result <- SMT.check - debugEvaluateConditionResult result - return result + go = + do + result <- query >>= whenUnknown retry + debugEvaluateConditionResult result + case result of + Unsat -> return False + Sat -> empty + Unknown -> do + -- TODO: Remove empty + errorDecidePredicateUnknown predicates + empty + & runMaybeT + + whenUnknown f Unknown = f + whenUnknown _ result = return result - retryCheckPredicateOnce = do + -- | Run the SMT query once. + query :: MaybeT simplifier Result + query = + -- TODO: instance MonadSMT smt => MonadSMT (MaybeT smt) + MaybeT $ SMT.withSolver $ runMaybeT $ 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 - retriedResult <- checkPredicate - case retriedResult of - Unsat -> return False - Sat -> empty - Unknown -> do - errorDecidePredicateUnknown predicates - empty + return result translatePredicate :: forall variable m. From 9f4537ddc3a9691f8f1eb6f46a0cc2c6ab8187e9 Mon Sep 17 00:00:00 2001 From: ana-pantilie Date: Wed, 28 Oct 2020 10:44:09 +0200 Subject: [PATCH 4/7] Clean-up: remove empty --- kore/src/Kore/Log/ErrorDecidePredicateUnknown.hs | 2 +- kore/src/Kore/Step/SMT/Evaluator.hs | 4 +--- 2 files changed, 2 insertions(+), 4 deletions(-) diff --git a/kore/src/Kore/Log/ErrorDecidePredicateUnknown.hs b/kore/src/Kore/Log/ErrorDecidePredicateUnknown.hs index 6089596358..7af039bfb4 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 Bool errorDecidePredicateUnknown predicates' = throw ErrorDecidePredicateUnknown { predicates } where diff --git a/kore/src/Kore/Step/SMT/Evaluator.hs b/kore/src/Kore/Step/SMT/Evaluator.hs index 0b15377d97..244a57df75 100644 --- a/kore/src/Kore/Step/SMT/Evaluator.hs +++ b/kore/src/Kore/Step/SMT/Evaluator.hs @@ -185,10 +185,8 @@ decidePredicate predicates = case result of Unsat -> return False Sat -> empty - Unknown -> do - -- TODO: Remove empty + Unknown -> errorDecidePredicateUnknown predicates - empty & runMaybeT whenUnknown f Unknown = f From 97047ab44eff2f091768e59a66f2fcc27e95359e Mon Sep 17 00:00:00 2001 From: ana-pantilie Date: Wed, 28 Oct 2020 10:49:51 +0200 Subject: [PATCH 5/7] Clean-up: use MaybeT instance of MonadSMT --- kore/src/Kore/Step/SMT/Evaluator.hs | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/kore/src/Kore/Step/SMT/Evaluator.hs b/kore/src/Kore/Step/SMT/Evaluator.hs index 244a57df75..fd935197d8 100644 --- a/kore/src/Kore/Step/SMT/Evaluator.hs +++ b/kore/src/Kore/Step/SMT/Evaluator.hs @@ -18,7 +18,7 @@ module Kore.Step.SMT.Evaluator import Prelude.Kore import Control.Error - ( MaybeT (MaybeT) + ( MaybeT , hoistMaybe , runMaybeT ) @@ -195,8 +195,7 @@ decidePredicate predicates = -- | Run the SMT query once. query :: MaybeT simplifier Result query = - -- TODO: instance MonadSMT smt => MonadSMT (MaybeT smt) - MaybeT $ SMT.withSolver $ runMaybeT $ evalTranslator $ do + SMT.withSolver $ evalTranslator $ do tools <- Simplifier.askMetadataTools predicates' <- traverse (translatePredicate tools) predicates Foldable.traverse_ SMT.assert predicates' From 4d22fccb6af6c2769e7f5ddb1112ea93b3bbe807 Mon Sep 17 00:00:00 2001 From: ana-pantilie <45069775+ana-pantilie@users.noreply.github.com> Date: Thu, 29 Oct 2020 10:46:29 +0200 Subject: [PATCH 6/7] Update kore/src/Kore/Log/ErrorDecidePredicateUnknown.hs Co-authored-by: Thomas Tuegel --- kore/src/Kore/Log/ErrorDecidePredicateUnknown.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kore/src/Kore/Log/ErrorDecidePredicateUnknown.hs b/kore/src/Kore/Log/ErrorDecidePredicateUnknown.hs index 7af039bfb4..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 Bool + -> log a errorDecidePredicateUnknown predicates' = throw ErrorDecidePredicateUnknown { predicates } where From 69a8b2bc1f9d4c2fc593a03efc52b45e7a61a58d Mon Sep 17 00:00:00 2001 From: ana-pantilie <45069775+ana-pantilie@users.noreply.github.com> Date: Thu, 29 Oct 2020 10:53:06 +0200 Subject: [PATCH 7/7] Update WarnRetrySolverQuery.hs --- kore/src/Kore/Log/WarnRetrySolverQuery.hs | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/kore/src/Kore/Log/WarnRetrySolverQuery.hs b/kore/src/Kore/Log/WarnRetrySolverQuery.hs index ac35598b92..b412e7d8a3 100644 --- a/kore/src/Kore/Log/WarnRetrySolverQuery.hs +++ b/kore/src/Kore/Log/WarnRetrySolverQuery.hs @@ -37,14 +37,14 @@ newtype WarnRetrySolverQuery = instance Pretty WarnRetrySolverQuery where pretty WarnRetrySolverQuery { predicates } = Pretty.vsep $ - [ "The SMT solver failed to solve the following query:" + [ "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 will be reset and the query\ - \ will be tried one more time." + <> ["The SMT solver was reset and the query\ + \ was tried one more time." ] where predicate :| sideConditions = predicates @@ -54,7 +54,7 @@ instance Entry WarnRetrySolverQuery where helpDoc _ = "warning raised when the solver failed to decide\ \ the satisfiability of a formula, indicating that\ - \ the solver will be reset and the formula retried" + \ the solver was reset and the formula retried" warnRetrySolverQuery :: InternalVariable variable