Simplify the remainder predicate before checking its satisfiability

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
@@ -74,6 +75,7 @@ import Kore.Rewrite.Step (
     applyInitialConditions,
     applyRemainder,
     assertFunctionLikeResults,
+    simplifyRemainder,
     unifyRules,
  )
 import Kore.Simplify.Ceil (
@@ -305,11 +307,21 @@ 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
+
+            -- Simplify the remainder predicate under the side condition and the initial conditions.
+            simplifiedRemainderCondition <-
+                simplifyRemainder
+                    sideCondition
+                    (Conditional.withoutTerm initial)
+                    (Conditional.fromPredicate remainderPredicate)
+
+            -- check simplified remainder to make sure it is actually satisfiable.
             SMT.evalPredicate
                 (ErrorDecidePredicateUnknown $srcLoc Nothing)
-                remainderPredicate
-                Nothing
+                ( 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
@@ -327,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 remainderPredicate)
+                            applyRemainder sideCondition initial simplifiedRemainderCondition
                                 & Logic.observeAllT
                                 & fmap (fmap assertRemainderPattern >>> OrPattern.fromPatterns)
                         return

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
@@ -324,20 +361,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