diff --git a/kore/src/Kore/Step/RewriteStep.hs b/kore/src/Kore/Step/RewriteStep.hs index 6a1fb3421a..b88a72ebe1 100644 --- a/kore/src/Kore/Step/RewriteStep.hs +++ b/kore/src/Kore/Step/RewriteStep.hs @@ -38,8 +38,6 @@ import Kore.Internal.OrPattern import qualified Kore.Internal.OrPattern as OrPattern import Kore.Internal.Pattern as Pattern import qualified Kore.Internal.SideCondition as SideCondition - ( topTODO - ) import qualified Kore.Internal.Substitution as Substitution import Kore.Internal.TermLike as TermLike import Kore.Log.DebugAppliedRewriteRules @@ -59,6 +57,7 @@ import Kore.Step.RulePattern import qualified Kore.Step.RulePattern as Rule import Kore.Step.Simplification.Simplify ( MonadSimplify + , simplifyCondition ) import Kore.Step.Step ( Result @@ -69,7 +68,6 @@ import Kore.Step.Step , applyRemainder , assertFunctionLikeResults , mkRewritingPattern - , simplifyPredicate , unifyRules ) @@ -112,8 +110,13 @@ finalizeAppliedRule renamedRule appliedConditions = Conditional { predicate = ensures } = finalPattern ensuresCondition = Condition.fromPredicate ensures finalCondition <- - simplifyPredicate - SideCondition.topTODO (Just appliedCondition) ensuresCondition + do + partial <- + simplifyCondition + (SideCondition.fromCondition appliedCondition) + ensuresCondition + simplifyCondition SideCondition.top + (appliedCondition <> partial) & Branch.alternate -- Apply the normalized substitution to the right-hand side of the -- axiom. @@ -136,10 +139,7 @@ finalizeRule initialVariables initial unifiedRule = Branch.gather $ do let initialCondition = Conditional.withoutTerm initial let unificationCondition = Conditional.withoutTerm unifiedRule - applied <- applyInitialConditions - SideCondition.topTODO - (Just initialCondition) - unificationCondition + applied <- applyInitialConditions initialCondition unificationCondition checkSubstitutionCoverage initial (RewriteRule <$> unifiedRule) let renamedRule = Conditional.term unifiedRule final <- finalizeAppliedRule renamedRule applied @@ -161,9 +161,7 @@ finalizeRulesParallel initialVariables initial unifiedRules = do & fmap Foldable.fold let unifications = MultiOr.make (Conditional.withoutTerm <$> unifiedRules) remainder = Condition.fromPredicate (Remainder.remainder' unifications) - remainders' <- - applyRemainder SideCondition.topTODO initial remainder - & Branch.gather + remainders' <- applyRemainder initial remainder & Branch.gather return Step.Results { results = Seq.fromList results , remainders = @@ -176,9 +174,7 @@ finalizeRulesSequence initialVariables initial unifiedRules = do State.runStateT (traverse finalizeRuleSequence' unifiedRules) (Conditional.withoutTerm initial) - remainders' <- - applyRemainder SideCondition.topTODO initial remainder - & Branch.gather + remainders' <- applyRemainder initial remainder & Branch.gather return Step.Results { results = Seq.fromList $ Foldable.fold results , remainders = @@ -211,10 +207,9 @@ applyRulesWithFinalizer -- ^ Configuration being rewritten -> simplifier (Results RulePattern Variable) applyRulesWithFinalizer finalize unificationProcedure rules initial = do - let sideCondition = SideCondition.topTODO - initialVariables = freeVariables sideCondition <> freeVariables initial - results <- unifyRules unificationProcedure sideCondition initial rules + results <- unifyRules unificationProcedure initial rules debugAppliedRewriteRules initial results + let initialVariables = freeVariables initial finalize initialVariables initial results {-# INLINE applyRulesWithFinalizer #-} diff --git a/kore/src/Kore/Step/Step.hs b/kore/src/Kore/Step/Step.hs index b1f2daa8e3..e72af89d1f 100644 --- a/kore/src/Kore/Step/Step.hs +++ b/kore/src/Kore/Step/Step.hs @@ -16,7 +16,6 @@ module Kore.Step.Step , unifyRule , applyInitialConditions , applyRemainder - , simplifyPredicate , toConfigurationVariablesCondition , assertFunctionLikeResults , checkFunctionLike @@ -67,9 +66,6 @@ import Kore.Internal.SideCondition ( SideCondition ) import qualified Kore.Internal.SideCondition as SideCondition - ( andCondition - , mapVariables - ) import qualified Kore.Internal.Substitution as Substitution import Kore.Internal.TermLike ( InternalVariable @@ -114,16 +110,15 @@ unifyRules :: MonadSimplify simplifier => UnifyingRule rule => UnificationProcedure simplifier - -> SideCondition RewritingVariable -> Pattern RewritingVariable -- ^ Initial configuration -> [rule RewritingVariable] -- ^ Rule -> simplifier [UnifiedRule rule RewritingVariable] -unifyRules unificationProcedure sideCondition initial rules = +unifyRules unificationProcedure initial rules = Branch.gather $ do rule <- Branch.scatter rules - unifyRule unificationProcedure sideCondition initial rule + unifyRule unificationProcedure initial rule {- | Attempt to unify a rule with the initial configuration. @@ -143,27 +138,25 @@ unifyRule => MonadSimplify simplifier => UnifyingRule rule => UnificationProcedure simplifier - -> SideCondition variable - -- ^ Top level condition. -> Pattern variable -- ^ Initial configuration -> rule variable -- ^ Rule -> BranchT simplifier (UnifiedRule rule variable) -unifyRule unificationProcedure sideCondition initial rule = do +unifyRule unificationProcedure initial rule = do let (initialTerm, initialCondition) = Pattern.splitTerm initial - mergedSideCondition = - sideCondition `SideCondition.andCondition` initialCondition + sideCondition = SideCondition.fromCondition initialCondition -- Unify the left-hand side of the rule with the term of the initial -- configuration. let ruleLeft = matchingPattern rule - unification <- - unifyTermLikes mergedSideCondition initialTerm ruleLeft + unification <- unifyTermLikes sideCondition initialTerm ruleLeft -- Combine the unification solution with the rule's requirement clause, let ruleRequires = precondition rule requires' = Condition.fromPredicate ruleRequires unification' <- - simplifyPredicate mergedSideCondition Nothing (unification <> requires') + Simplifier.simplifyCondition + sideCondition + (unification <> requires') return (rule `Conditional.withCondition` unification') where unifyTermLikes = runUnificationProcedure unificationProcedure @@ -235,25 +228,32 @@ checkFunctionLike unifiedRules pat The rule is considered to apply if the result is not @\\bottom@. +@applyInitialConditions@ assumes that the unification solution includes the +@requires@ clause, and that their conjunction has already been simplified with +respect to the initial condition. + -} applyInitialConditions :: forall simplifier variable . InternalVariable variable => MonadSimplify simplifier - => SideCondition variable - -- ^ Top-level conditions - -> Maybe (Condition variable) + => Condition variable -- ^ Initial conditions -> Condition variable -- ^ Unification conditions -> BranchT simplifier (OrCondition variable) -- TODO(virgil): This should take advantage of the BranchT and not return -- an OrCondition. -applyInitialConditions sideCondition initial unification = do - -- Combine the initial conditions and the unification conditions. - -- The axiom requires clause is included in the unification conditions. +applyInitialConditions initial unification = do + -- Combine the initial conditions and the unification conditions. The axiom + -- requires clause is already included in the unification conditions, and + -- the conjunction has already been simplified with respect to the initial + -- conditions. applied <- - simplifyPredicate sideCondition initial unification + -- Add the simplified unification solution to the initial conditions. We + -- must preserve the initial conditions here, so it cannot be used as + -- the side condition! + Simplifier.simplifyCondition SideCondition.top (initial <> unification) & MultiOr.gather evaluated <- SMT.Evaluator.filterMultiOr applied -- If 'evaluated' is \bottom, the rule is considered to not apply and @@ -277,46 +277,22 @@ applyRemainder :: forall simplifier variable . InternalVariable variable => MonadSimplify simplifier - => SideCondition variable - -- ^ Top level condition - -> Pattern variable + => Pattern variable -- ^ Initial configuration -> Condition variable -- ^ Remainder -> BranchT simplifier (Pattern variable) -applyRemainder sideCondition initial remainder = do - let (initialTerm, initialCondition) = Pattern.splitTerm initial - normalizedCondition <- - simplifyPredicate sideCondition (Just initialCondition) remainder - return normalizedCondition { Conditional.term = initialTerm } - --- | Simplifies the predicate obtained upon matching/unification. -simplifyPredicate - :: forall simplifier variable term - . InternalVariable variable - => MonadSimplify simplifier - => SideCondition variable - -> Maybe (Condition variable) - -> Conditional variable term - -> BranchT simplifier (Conditional variable term) -simplifyPredicate sideCondition (Just initialCondition) conditional = do - partialResult <- +applyRemainder initial 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.andCondition` initialCondition) - conditional - -- TODO (virgil): Consider using different simplifyPredicate implementations - -- for rewrite rules and equational rules. - -- Right now this double simplification both allows using the same code for - -- both kinds of rules, and allows using the strongest background condition - -- for simplifying the `conditional`. However, it's not obvious that - -- using the strongest background condition actually helps in our - -- use cases, so we may be able to do something better for equations. - Simplifier.simplifyCondition - sideCondition - ( partialResult - `Pattern.andCondition` initialCondition - ) -simplifyPredicate sideCondition Nothing conditional = + (SideCondition.fromCondition $ Pattern.withoutTerm initial) + remainder + -- Add the simplified remainder to the initial conditions. We must preserve + -- the initial conditions here! Simplifier.simplifyCondition - sideCondition - conditional + SideCondition.topTODO + (Pattern.andCondition initial partial) diff --git a/kore/test/Test/Kore/Step/RewriteStep.hs b/kore/test/Test/Kore/Step/RewriteStep.hs index 1b4cca679d..66d9d384b2 100644 --- a/kore/test/Test/Kore/Step/RewriteStep.hs +++ b/kore/test/Test/Kore/Step/RewriteStep.hs @@ -54,9 +54,6 @@ import Kore.Internal.Predicate as Predicate , makeTruePredicate , makeTruePredicate_ ) -import qualified Kore.Internal.SideCondition as SideCondition - ( top - ) import qualified Kore.Internal.Substitution as Substitution import Kore.Internal.TermLike import Kore.Rewriting.RewritingVariable @@ -91,7 +88,7 @@ applyInitialConditions -> Condition Variable -> IO [OrCondition Variable] applyInitialConditions initial unification = - Step.applyInitialConditions SideCondition.top (Just initial) unification + Step.applyInitialConditions initial unification & runSimplifier Mock.env . Branch.gather test_applyInitialConditions :: [TestTree] @@ -153,11 +150,7 @@ unifyRule [Conditional Variable (RulePattern Variable)] ) unifyRule initial rule = - Step.unifyRule - Unification.unificationProcedure - SideCondition.top - initial - rule + Step.unifyRule Unification.unificationProcedure initial rule & runExceptT . Branch.gather & runSimplifier Mock.env @@ -850,8 +843,11 @@ test_applyRewriteRulesParallel = , predicate = makeNotPredicate $ makeAndPredicate - (makeCeilPredicate_ Mock.cg) - (makeEqualsPredicate_ (mkElemVar Mock.x) Mock.a) + (makeCeilPredicate Mock.testSort Mock.cg) + (makeEqualsPredicate Mock.testSort + (mkElemVar Mock.x) + Mock.a + ) , substitution = mempty } ] @@ -895,11 +891,15 @@ test_applyRewriteRulesParallel = (mkElemVar Mock.x) Mock.cg , predicate = - makeAndPredicate (makeCeilPredicate_ Mock.cf) - $ makeNotPredicate - $ makeAndPredicate - (makeCeilPredicate_ Mock.cg) - (makeEqualsPredicate_ (mkElemVar Mock.x) Mock.a) + makeAndPredicate + (makeCeilPredicate Mock.testSort Mock.cf) + (makeNotPredicate $ makeAndPredicate + (makeCeilPredicate Mock.testSort Mock.cg) + (makeEqualsPredicate Mock.testSort + (mkElemVar Mock.x) + Mock.a + ) + ) , substitution = mempty } ] @@ -937,7 +937,7 @@ test_applyRewriteRulesParallel = remainders = MultiOr.singleton Conditional { term = Mock.functionalConstr10 (mkElemVar Mock.x) - , predicate = makeNotPredicate requirementUnsorted + , predicate = makeNotPredicate requirement , substitution = mempty } initial = pure (Mock.functionalConstr10 (mkElemVar Mock.x)) @@ -945,8 +945,6 @@ test_applyRewriteRulesParallel = makeEqualsPredicate Mock.testSort (Mock.f (mkElemVar Mock.x)) Mock.b - requirementUnsorted = - makeEqualsPredicate_ (Mock.f (mkElemVar Mock.x)) Mock.b Right actual <- applyRewriteRulesParallel initial [axiomSignum] checkResults results actual checkRemainders remainders actual @@ -980,8 +978,11 @@ test_applyRewriteRulesParallel = { predicate = makeNotPredicate $ makeAndPredicate - (makeCeilPredicate_ Mock.cg) - (makeEqualsPredicate_ (mkElemVar Mock.x) Mock.a) + (makeCeilPredicate Mock.testSort Mock.cg) + (makeEqualsPredicate Mock.testSort + (mkElemVar Mock.x) + Mock.a + ) } ] initialTerm = Mock.functionalConstr20 (mkElemVar Mock.x) Mock.cg @@ -1016,10 +1017,6 @@ test_applyRewriteRulesParallel = makeAndPredicate (makeCeilPredicate Mock.testSort Mock.cf) (makeCeilPredicate_ Mock.cg) - definedBranchesUnsorted = - makeAndPredicate - (makeCeilPredicate_ Mock.cf) - (makeCeilPredicate_ Mock.cg) results = OrPattern.fromPatterns [ Conditional @@ -1044,19 +1041,19 @@ test_applyRewriteRulesParallel = [ initial { predicate = Predicate.makeAndPredicate - (Predicate.makeNotPredicate - $ Predicate.makeAndPredicate - definedBranchesUnsorted - $ Predicate.makeEqualsPredicate_ + (makeNotPredicate $ makeAndPredicate + definedBranches + (Predicate.makeEqualsPredicate Mock.testSort (mkElemVar Mock.x) Mock.a + ) ) - (Predicate.makeNotPredicate - $ Predicate.makeAndPredicate - definedBranchesUnsorted - $ Predicate.makeEqualsPredicate_ + (makeNotPredicate $ makeAndPredicate + definedBranches + (Predicate.makeEqualsPredicate Mock.testSort (mkElemVar Mock.x) Mock.b + ) ) } ] @@ -1094,10 +1091,12 @@ test_applyRewriteRulesParallel = OrPattern.fromPatterns [ initial { predicate = - makeNotPredicate - $ makeAndPredicate - (makeCeilPredicate_ Mock.cg) - (makeEqualsPredicate_ (mkElemVar Mock.x) Mock.a) + makeNotPredicate $ makeAndPredicate + (makeCeilPredicate Mock.testSort Mock.cg) + (makeEqualsPredicate Mock.testSort + (mkElemVar Mock.x) + Mock.a + ) } ] initialTerm = Mock.functionalConstr20 (mkElemVar Mock.x) Mock.cg