Use side conditions when rewriting

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 #-}
 

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)