From 76a811d9698db0bf0d2cde9be6fb9f7a32099b92 Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Mon, 17 Jun 2024 15:19:10 +0200 Subject: [PATCH 1/7] Consider the side condition when checking remainder Maybe like that?? --- kore/src/Kore/Rewrite/RewriteStep.hs | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/kore/src/Kore/Rewrite/RewriteStep.hs b/kore/src/Kore/Rewrite/RewriteStep.hs index dcc67efbee..a0702a2ef4 100644 --- a/kore/src/Kore/Rewrite/RewriteStep.hs +++ b/kore/src/Kore/Rewrite/RewriteStep.hs @@ -304,12 +304,14 @@ finalizeRulesParallel unifiedRules & fmap fold let unifications = MultiOr.make (Conditional.withoutTerm <$> unifiedRules) + -- TODO here we lose the connection between the rules and the remainders. + -- Perhaps it would make sense to log the remainder of every rule. remainderPredicate = Remainder.remainder' unifications -- evaluate the remainder predicate to make sure it is actually satisfiable SMT.evalPredicate (ErrorDecidePredicateUnknown $srcLoc Nothing) remainderPredicate - Nothing + (Just (SideCondition.addAssumption (predicate initial) sideCondition)) >>= \case -- remainder condition is UNSAT: we prune the remainder branch early to avoid -- jumping into the pit of function evaluation in the configuration under the From 14a9239ead7417f3795bedb1107761edb291372e Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Mon, 17 Jun 2024 17:16:45 +0200 Subject: [PATCH 2/7] Try simplifying the remainder predicate before checking it with SMT --- kore/src/Kore/Rewrite/RewriteStep.hs | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) diff --git a/kore/src/Kore/Rewrite/RewriteStep.hs b/kore/src/Kore/Rewrite/RewriteStep.hs index a0702a2ef4..464dc5d860 100644 --- a/kore/src/Kore/Rewrite/RewriteStep.hs +++ b/kore/src/Kore/Rewrite/RewriteStep.hs @@ -83,6 +83,7 @@ import Kore.Simplify.Simplify ( Simplifier, simplifyCondition, ) +import Kore.Simplify.Simplify qualified as Simplifier import Kore.Substitute import Logic ( LogicT, @@ -307,10 +308,21 @@ finalizeRulesParallel -- TODO here we lose the connection between the rules and the remainders. -- Perhaps it would make sense to log the remainder of every rule. remainderPredicate = Remainder.remainder' unifications + + simplifiedRemainderConditional <- + Logic.observeAllT $ + Simplifier.simplifyCondition + ( sideCondition + & SideCondition.addConditionWithReplacements + (Pattern.withoutTerm initial) + ) + (Condition.fromPredicate remainderPredicate) + let simplifiedRemainderPredicate = Remainder.remainder' $ MultiOr.make simplifiedRemainderConditional + -- evaluate the remainder predicate to make sure it is actually satisfiable SMT.evalPredicate (ErrorDecidePredicateUnknown $srcLoc Nothing) - remainderPredicate + simplifiedRemainderPredicate (Just (SideCondition.addAssumption (predicate initial) sideCondition)) >>= \case -- remainder condition is UNSAT: we prune the remainder branch early to avoid From 51bb03170378bc7cfdd50fbdcdcfb9eab8d214e2 Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Mon, 17 Jun 2024 20:19:28 +0200 Subject: [PATCH 3/7] Don't use initial --- kore/src/Kore/Rewrite/RewriteStep.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kore/src/Kore/Rewrite/RewriteStep.hs b/kore/src/Kore/Rewrite/RewriteStep.hs index 464dc5d860..4a01220334 100644 --- a/kore/src/Kore/Rewrite/RewriteStep.hs +++ b/kore/src/Kore/Rewrite/RewriteStep.hs @@ -323,7 +323,7 @@ finalizeRulesParallel SMT.evalPredicate (ErrorDecidePredicateUnknown $srcLoc Nothing) simplifiedRemainderPredicate - (Just (SideCondition.addAssumption (predicate initial) sideCondition)) + (Just sideCondition) >>= \case -- remainder condition is UNSAT: we prune the remainder branch early to avoid -- jumping into the pit of function evaluation in the configuration under the From 883af2e4c01a465f989a6695adb3f46c775057b4 Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Tue, 18 Jun 2024 08:42:49 +0200 Subject: [PATCH 4/7] Revert to trivial side condition when working with the remainder --- kore/src/Kore/Rewrite/RewriteStep.hs | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/kore/src/Kore/Rewrite/RewriteStep.hs b/kore/src/Kore/Rewrite/RewriteStep.hs index 4a01220334..d8f69e0f5d 100644 --- a/kore/src/Kore/Rewrite/RewriteStep.hs +++ b/kore/src/Kore/Rewrite/RewriteStep.hs @@ -312,10 +312,7 @@ finalizeRulesParallel simplifiedRemainderConditional <- Logic.observeAllT $ Simplifier.simplifyCondition - ( sideCondition - & SideCondition.addConditionWithReplacements - (Pattern.withoutTerm initial) - ) + SideCondition.top (Condition.fromPredicate remainderPredicate) let simplifiedRemainderPredicate = Remainder.remainder' $ MultiOr.make simplifiedRemainderConditional @@ -323,7 +320,7 @@ finalizeRulesParallel SMT.evalPredicate (ErrorDecidePredicateUnknown $srcLoc Nothing) simplifiedRemainderPredicate - (Just sideCondition) + Nothing >>= \case -- remainder condition is UNSAT: we prune the remainder branch early to avoid -- jumping into the pit of function evaluation in the configuration under the From 375b1e1e28fc45a0d617ac405bc992dfbf725ca7 Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Wed, 19 Jun 2024 09:51:58 +0200 Subject: [PATCH 5/7] Do not simplify the remainder, but consider side condition when solving --- kore/src/Kore/Rewrite/RewriteStep.hs | 15 ++------------- 1 file changed, 2 insertions(+), 13 deletions(-) diff --git a/kore/src/Kore/Rewrite/RewriteStep.hs b/kore/src/Kore/Rewrite/RewriteStep.hs index d8f69e0f5d..3ab087573f 100644 --- a/kore/src/Kore/Rewrite/RewriteStep.hs +++ b/kore/src/Kore/Rewrite/RewriteStep.hs @@ -83,7 +83,6 @@ import Kore.Simplify.Simplify ( Simplifier, simplifyCondition, ) -import Kore.Simplify.Simplify qualified as Simplifier import Kore.Substitute import Logic ( LogicT, @@ -305,22 +304,12 @@ finalizeRulesParallel unifiedRules & fmap fold let unifications = MultiOr.make (Conditional.withoutTerm <$> unifiedRules) - -- TODO here we lose the connection between the rules and the remainders. - -- Perhaps it would make sense to log the remainder of every rule. remainderPredicate = Remainder.remainder' unifications - - simplifiedRemainderConditional <- - Logic.observeAllT $ - Simplifier.simplifyCondition - SideCondition.top - (Condition.fromPredicate remainderPredicate) - let simplifiedRemainderPredicate = Remainder.remainder' $ MultiOr.make simplifiedRemainderConditional - -- evaluate the remainder predicate to make sure it is actually satisfiable SMT.evalPredicate (ErrorDecidePredicateUnknown $srcLoc Nothing) - simplifiedRemainderPredicate - Nothing + remainderPredicate + (Just sideCondition) >>= \case -- remainder condition is UNSAT: we prune the remainder branch early to avoid -- jumping into the pit of function evaluation in the configuration under the From 0cf4ca86136b271b11af0e08a59cc0f7be2cc057 Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Wed, 19 Jun 2024 11:12:39 +0200 Subject: [PATCH 6/7] Simplify the remainder before checking its satisfiability --- kore/src/Kore/Rewrite/RewriteStep.hs | 36 ++++++++++++++++++++++++---- kore/src/Kore/Rewrite/Step.hs | 16 ++----------- 2 files changed, 34 insertions(+), 18 deletions(-) diff --git a/kore/src/Kore/Rewrite/RewriteStep.hs b/kore/src/Kore/Rewrite/RewriteStep.hs index 3ab087573f..c4334c5253 100644 --- a/kore/src/Kore/Rewrite/RewriteStep.hs +++ b/kore/src/Kore/Rewrite/RewriteStep.hs @@ -35,6 +35,7 @@ import Kore.Internal.Conditional qualified as Conditional import Kore.Internal.MultiOr qualified as MultiOr import Kore.Internal.OrPattern qualified as OrPattern import Kore.Internal.Pattern as Pattern +import Kore.Internal.Predicate (Predicate) import Kore.Internal.SideCondition (SideCondition) import Kore.Internal.SideCondition qualified as SideCondition import Kore.Internal.Substitution qualified as Substitution @@ -83,6 +84,7 @@ import Kore.Simplify.Simplify ( Simplifier, simplifyCondition, ) +import Kore.Simplify.Simplify qualified as Simplifier import Kore.Substitute import Logic ( LogicT, @@ -305,11 +307,37 @@ finalizeRulesParallel & fmap fold let unifications = MultiOr.make (Conditional.withoutTerm <$> unifiedRules) remainderPredicate = Remainder.remainder' unifications - -- evaluate the remainder predicate to make sure it is actually satisfiable + + let sideConditionWithInitialCondition = + sideCondition + & SideCondition.addConditionWithReplacements + (Pattern.withoutTerm initial) + + -- Simplify the remainder predicate under the side condition and the initial conditions. + -- We must ensure that functions in the remainder are evaluated using the top-level + -- side conditions because we will not re-evaluate them after they are added + -- to the top level. + simplifiedRemainderRaw <- + Simplifier.simplifyCondition + sideConditionWithInitialCondition + (Condition.fromPredicate remainderPredicate) + & Logic.observeAllT + + -- convert to predicate from the list of conditionals produce by the simplifier + -- TODO must gracefully handle the ?impossible? case of more then one simplifier branch + let simplifiedRemainderPredicate = + map + (from @(Condition RewritingVariableName) @(Predicate RewritingVariableName)) + simplifiedRemainderRaw + & \case + [singleResult] -> singleResult + _ -> error "more then one result after simplifying the remainder condition" + + -- check simplified remainder predicate to make sure it is actually satisfiable. SMT.evalPredicate (ErrorDecidePredicateUnknown $srcLoc Nothing) - remainderPredicate - (Just sideCondition) + simplifiedRemainderPredicate + (Just sideConditionWithInitialCondition) >>= \case -- remainder condition is UNSAT: we prune the remainder branch early to avoid -- jumping into the pit of function evaluation in the configuration under the @@ -327,7 +355,7 @@ finalizeRulesParallel -- the remainder branch, i.e. to evaluate the functions in the configuration -- with the remainder in the path condition and rewrite further remainders <- - applyRemainder sideCondition initial (Condition.fromPredicate remainderPredicate) + applyRemainder sideCondition initial (Condition.fromPredicate simplifiedRemainderPredicate) & Logic.observeAllT & fmap (fmap assertRemainderPattern >>> OrPattern.fromPatterns) return diff --git a/kore/src/Kore/Rewrite/Step.hs b/kore/src/Kore/Rewrite/Step.hs index 14dcb746f1..6e78407ce2 100644 --- a/kore/src/Kore/Rewrite/Step.hs +++ b/kore/src/Kore/Rewrite/Step.hs @@ -324,20 +324,8 @@ applyRemainder :: Condition RewritingVariableName -> LogicT Simplifier (Pattern RewritingVariableName) applyRemainder sideCondition initial remainder = inContext "apply-remainder" $ do - -- Simplify the remainder predicate under the initial conditions. We must - -- ensure that functions in the remainder are evaluated using the top-level - -- side conditions because we will not re-evaluate them after they are added - -- to the top level. - partial <- - Simplifier.simplifyCondition - ( sideCondition - & SideCondition.addConditionWithReplacements - (Pattern.withoutTerm initial) - ) - remainder - -- Add the simplified remainder to the initial conditions. We must preserve - -- the initial conditions here! + -- Add the remainder to the initial conditions. Simplifier.simplifyCondition sideCondition - (Pattern.andCondition initial partial) + (Pattern.andCondition initial remainder) <&> Pattern.mapVariables resetConfigVariable From a39220745970edd77d75202417bd502141100818 Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Wed, 19 Jun 2024 11:36:28 +0200 Subject: [PATCH 7/7] Factor out remainder simplification into a function --- kore/src/Kore/Rewrite/RewriteStep.hs | 40 +++++++++------------------- kore/src/Kore/Rewrite/Step.hs | 37 +++++++++++++++++++++++++ 2 files changed, 49 insertions(+), 28 deletions(-) diff --git a/kore/src/Kore/Rewrite/RewriteStep.hs b/kore/src/Kore/Rewrite/RewriteStep.hs index c4334c5253..5b331e9e65 100644 --- a/kore/src/Kore/Rewrite/RewriteStep.hs +++ b/kore/src/Kore/Rewrite/RewriteStep.hs @@ -75,6 +75,7 @@ import Kore.Rewrite.Step ( applyInitialConditions, applyRemainder, assertFunctionLikeResults, + simplifyRemainder, unifyRules, ) import Kore.Simplify.Ceil ( @@ -84,7 +85,6 @@ import Kore.Simplify.Simplify ( Simplifier, simplifyCondition, ) -import Kore.Simplify.Simplify qualified as Simplifier import Kore.Substitute import Logic ( LogicT, @@ -308,36 +308,20 @@ finalizeRulesParallel let unifications = MultiOr.make (Conditional.withoutTerm <$> unifiedRules) remainderPredicate = Remainder.remainder' unifications - let sideConditionWithInitialCondition = - sideCondition - & SideCondition.addConditionWithReplacements - (Pattern.withoutTerm initial) - -- Simplify the remainder predicate under the side condition and the initial conditions. - -- We must ensure that functions in the remainder are evaluated using the top-level - -- side conditions because we will not re-evaluate them after they are added - -- to the top level. - simplifiedRemainderRaw <- - Simplifier.simplifyCondition - sideConditionWithInitialCondition - (Condition.fromPredicate remainderPredicate) - & Logic.observeAllT + simplifiedRemainderCondition <- + simplifyRemainder + sideCondition + (Conditional.withoutTerm initial) + (Conditional.fromPredicate remainderPredicate) - -- convert to predicate from the list of conditionals produce by the simplifier - -- TODO must gracefully handle the ?impossible? case of more then one simplifier branch - let simplifiedRemainderPredicate = - map - (from @(Condition RewritingVariableName) @(Predicate RewritingVariableName)) - simplifiedRemainderRaw - & \case - [singleResult] -> singleResult - _ -> error "more then one result after simplifying the remainder condition" - - -- check simplified remainder predicate to make sure it is actually satisfiable. + -- check simplified remainder to make sure it is actually satisfiable. SMT.evalPredicate (ErrorDecidePredicateUnknown $srcLoc Nothing) - simplifiedRemainderPredicate - (Just sideConditionWithInitialCondition) + ( from @(Conditional RewritingVariableName ()) @(Predicate RewritingVariableName) + simplifiedRemainderCondition + ) + (Just sideCondition) >>= \case -- remainder condition is UNSAT: we prune the remainder branch early to avoid -- jumping into the pit of function evaluation in the configuration under the @@ -355,7 +339,7 @@ finalizeRulesParallel -- the remainder branch, i.e. to evaluate the functions in the configuration -- with the remainder in the path condition and rewrite further remainders <- - applyRemainder sideCondition initial (Condition.fromPredicate simplifiedRemainderPredicate) + applyRemainder sideCondition initial simplifiedRemainderCondition & Logic.observeAllT & fmap (fmap assertRemainderPattern >>> OrPattern.fromPatterns) return diff --git a/kore/src/Kore/Rewrite/Step.hs b/kore/src/Kore/Rewrite/Step.hs index 6e78407ce2..09bee365f4 100644 --- a/kore/src/Kore/Rewrite/Step.hs +++ b/kore/src/Kore/Rewrite/Step.hs @@ -16,6 +16,7 @@ module Kore.Rewrite.Step ( unifyRules, unifyRule, applyInitialConditions, + simplifyRemainder, applyRemainder, assertFunctionLikeResults, checkFunctionLike, @@ -314,6 +315,42 @@ applyInitialConditions sideCondition initial unification = inContext "apply-init -- then the rule is considered to apply with a \bottom result. Logic.scatter evaluated +{- | Simplify the remainder condition in the context of the side condition and the initial condition + +This function assumes that the remainder is a pure boolean predicate, i.e. no configuration pieces/ceils etc. are involved. The simplifier should not branch on such pure predicates. This function will call @error@ if the simplifier returns more then one result. +-} +simplifyRemainder :: + -- | SideCondition containing metadata + SideCondition RewritingVariableName -> + -- | Initial conditions + Condition RewritingVariableName -> + -- | Remainder condition + Condition RewritingVariableName -> + Simplifier (Condition RewritingVariableName) +simplifyRemainder sideCondition initialCondition remainderCondition = inContext "simplify-remainder" $ do + let sideConditionWithInitialCondition = + sideCondition + & SideCondition.addConditionWithReplacements + initialCondition + + -- Simplify the remainder predicate under the side condition and the initial conditions. + -- We must ensure that functions in the remainder are evaluated using the top-level + -- side conditions because we will not re-evaluate them after they are added + -- to the top level. + simplifiedRemainderRaw <- + Simplifier.simplifyCondition + sideConditionWithInitialCondition + remainderCondition + & Logic.observeAllT + + -- convert to predicate from the list of conditionals produce by the simplifier + -- TODO must gracefully handle the ?impossible? case of more then one simplifier branch + let simplifiedRemainder = case simplifiedRemainderRaw of + [singleResult] -> singleResult + _ -> error "more then one result after simplifying the remainder condition" + + pure simplifiedRemainder + -- | Apply the remainder predicate to the given initial configuration. applyRemainder :: -- | SideCondition containing metadata