Factor out remainder simplification into a function

runtimeverification · Jun 19, 2024 · a392207 · a392207
1 parent 0cf4ca8
commit a392207
Show file tree

Hide file tree

Showing 2 changed files with 49 additions and 28 deletions.
diff --git 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
@@ -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