Remove MultiOr form Result and push branching into LogicT (#3715)

Co-authored-by: github-actions <github-actions@github.com>

kore/src/Kore/Log/DebugRewriteTrace.hs

@@ -96,7 +96,7 @@ newtype DebugFinalPatterns = DebugFinalPatterns [Pattern VariableName]
 data RewriteResult = RewriteResult
     { ruleId :: UniqueId
     , substitution :: Substitution VariableName
-    , results :: [Pattern VariableName]
+    , result :: Pattern VariableName
     }
     deriving stock (Show)
 
@@ -150,11 +150,11 @@ instance ToJSON DebugFinalPatterns where
             ]
 
 instance ToJSON RewriteResult where
-    toJSON RewriteResult{ruleId, substitution, results} =
+    toJSON RewriteResult{ruleId, substitution, result} =
         object
             [ "rule-id" .= maybe Null toJSON (getUniqueId ruleId)
             , "substitution" .= encodeSubstitution substitution
-            , "results" .= map encodePattern results
+            , "result" .= encodePattern result
             ]
 
 instance ToJSON DebugRewriteTrace where
@@ -243,7 +243,7 @@ debugRewriteTrace initial Result.Results{results = (toList -> results), remainde
         RewriteResult
             { ruleId = from @_ @UniqueId $ extract appliedRule
             , substitution = mapSubstitutionVariables $ Conditional.substitution appliedRule
-            , results = multiOrToList result
+            , result = getRewritingPattern result
             }
 
 rewriteTraceLogger ::

kore/src/Kore/Reachability/Claim.hs

@@ -119,7 +119,6 @@ import Kore.Internal.Symbol (
  )
 import Kore.Internal.TermLike (
     Not (..),
-    Sort,
     TermLike,
     freeVariables,
     isFunctionPattern,
@@ -297,14 +296,13 @@ deriveSeqClaim lensClaimPattern mkClaim claims claim =
                 fmap (snd . Step.refreshRule mempty) $
                     Lens.forOf (field @"left") claimPattern $
                         \config -> Compose $ do
-                            let claimPatSort = ClaimPattern.getClaimPatternSort claimPattern
                             results <-
                                 Step.applyClaimsSequence
                                     mkClaim
                                     config
                                     (Lens.view lensClaimPattern <$> claims)
                                     & lift
-                            deriveResults claimPatSort fromAppliedRule results
+                            deriveResults fromAppliedRule results
   where
     fromAppliedRule =
         AppliedClaim
@@ -1005,9 +1003,8 @@ deriveWith lensClaimPattern mkRule takeStep rewrites claim =
                 fmap (snd . Step.refreshRule mempty) $
                     Lens.forOf (field @"left") claimPattern $
                         \config -> Compose $ do
-                            let claimPatSort = ClaimPattern.getClaimPatternSort claimPattern
                             results <- takeStep rewrites config & lift
-                            deriveResults claimPatSort fromAppliedRule results
+                            deriveResults fromAppliedRule results
   where
     fromAppliedRule =
         AppliedAxiom
@@ -1028,25 +1025,21 @@ deriveSeq' lensRulePattern mkRule =
 
 deriveResults ::
     Step.UnifyingRuleVariable representation ~ RewritingVariableName =>
-    Sort ->
     (Step.UnifiedRule representation -> AppliedRule claim) ->
     Step.Results representation ->
     Strategy.TransitionT
         (AppliedRule claim)
         simplifier
         (ApplyResult (Pattern RewritingVariableName))
--- TODO (thomas.tuegel): Remove claim argument.
-deriveResults sort fromAppliedRule Results{results, remainders} =
+deriveResults fromAppliedRule Results{results, remainders} =
     addResults <|> addRemainders
   where
     addResults = asum (addResult <$> results)
     addRemainders = asum (addRemainder <$> toList remainders)
 
     addResult Result{appliedRule, result} = do
         addRule appliedRule
-        case toList result of
-            [] -> addRewritten (Pattern.bottomOf sort)
-            configs -> asum (addRewritten <$> configs)
+        addRewritten result
 
     addRewritten = pure . ApplyRewritten
     addRemainder = pure . ApplyRemainder

kore/src/Kore/Rewrite.hs

@@ -41,6 +41,7 @@ import Generics.SOP qualified as SOP
 import Kore.Attribute.Axiom qualified as Attribute
 import Kore.Debug
 import Kore.Internal.Pattern (
+    Conditional,
     Pattern,
  )
 import Kore.Log.DecidePredicateUnknown (srcLoc)
@@ -65,6 +66,7 @@ import Kore.Simplify.Pattern qualified as Pattern (
  )
 import Kore.Simplify.Simplify as Simplifier
 import Kore.TopBottom (
+    TopBottom,
     isBottom,
  )
 import Kore.Unparser (
@@ -226,20 +228,27 @@ transitionRule rewriteGroups assumeInitialDefined = transitionRuleWorker
         deriveResults results
 
 deriveResults ::
-    Comonad w =>
-    Result.Results (w (RulePattern variable)) a ->
-    TransitionT (RewriteRule variable, Seq SimplifierTrace) Simplifier (ProgramState a)
+    TopBottom a =>
+    Result.Results
+        ( Conditional
+            var
+            (RulePattern var)
+        )
+        a ->
+    TransitionT (RewriteRule var, Seq SimplifierTrace) Simplifier (ProgramState a)
 deriveResults Result.Results{results, remainders} =
-    if (null results || all (\Result.Result{result} -> null result) results) && null remainders
+    if (null results || all (\Result.Result{result} -> isBottom result) results) && null remainders
         then pure Bottom
         else addResults results <|> addRemainders remainders
   where
     addResults results' = asum (addResult <$> results')
-    addResult Result.Result{appliedRule, result} = do
-        (_, rules :: Seq SimplifierTrace) <- lift get
-        lift $ modify $ \(cache, _rules) -> (cache, mempty)
-        addRule (RewriteRule $ extract appliedRule, rules)
-        asum (pure . Rewritten <$> toList result)
+    addResult Result.Result{appliedRule, result}
+        | isBottom result = empty
+        | otherwise = do
+            (_, simplifyRules :: Seq SimplifierTrace) <- lift get
+            lift $ modify $ \(cache, _rules) -> (cache, mempty)
+            addRule (RewriteRule $ extract appliedRule, simplifyRules)
+            pure $ Rewritten result
     addRemainders remainders' =
         asum (pure . Remaining <$> toList remainders')
 

kore/src/Kore/Rewrite/Result.hs

@@ -45,13 +45,14 @@ import Kore.Simplify.Simplify (
  )
 import Kore.TopBottom (
     TopBottom,
+    isBottom,
  )
 import Prelude.Kore
 
 -- | The result of applying a single rule.
 data Result rule config = Result
     { appliedRule :: !rule
-    , result :: !(MultiOr config)
+    , result :: config
     }
     deriving stock (Eq, Foldable, GHC.Generic, Ord, Show)
 
@@ -61,21 +62,17 @@ mapRule f r@Result{appliedRule} = r{appliedRule = f appliedRule}
 
 -- | Apply a function to the 'result' of a 'Result'.
 mapResult ::
-    Ord config2 =>
-    TopBottom config2 =>
     (config1 -> config2) ->
     Result rule config1 ->
     Result rule config2
-mapResult f = Lens.over (field @"result") (MultiOr.map f)
+mapResult f = Lens.over (field @"result") f
 
 traverseResult ::
-    Ord config2 =>
-    TopBottom config2 =>
     Applicative f =>
     (config1 -> f config2) ->
     Result rule config1 ->
     f (Result rule config2)
-traverseResult f = Lens.traverseOf (field @"result") (MultiOr.traverse f)
+traverseResult f = Lens.traverseOf (field @"result") f
 
 {- | The results of applying many rules.
 
@@ -122,19 +119,21 @@ remainder config = mempty{remainders = MultiOr.singleton config}
 
 -- | Gather all the final configurations from the 'Results'.
 gatherResults ::
-    Ord config =>
+    (Ord config, TopBottom config) =>
     Results rule config ->
     MultiOr config
-gatherResults = foldMap result . results
+gatherResults = from . map result . toList . results
 
 -- | Distribute the 'Result' over a transition rule.
-transitionResult :: Result rule config -> TransitionT rule m config
-transitionResult Result{appliedRule, result} = do
-    Transition.addRule appliedRule
-    asum (return <$> toList result)
+transitionResult :: TopBottom config => Result rule config -> TransitionT rule m config
+transitionResult Result{appliedRule, result}
+    | isBottom result = empty
+    | otherwise = do
+        Transition.addRule appliedRule
+        return result
 
 -- | Distribute the 'Results' over a transition rule.
-transitionResults :: Results rule config -> TransitionT rule m config
+transitionResults :: TopBottom config => Results rule config -> TransitionT rule m config
 transitionResults Results{results, remainders} =
     transitionResultsResults <|> transitionResultsRemainders
   where

kore/src/Kore/Rewrite/RewriteStep.hs

@@ -31,12 +31,6 @@ import Kore.Attribute.UniqueId (
 import Kore.Internal.Condition qualified as Condition
 import Kore.Internal.Conditional qualified as Conditional
 import Kore.Internal.MultiOr qualified as MultiOr
-import Kore.Internal.OrCondition (
-    OrCondition,
- )
-import Kore.Internal.OrPattern (
-    OrPattern,
- )
 import Kore.Internal.OrPattern qualified as OrPattern
 import Kore.Internal.Pattern as Pattern
 import Kore.Internal.SideCondition (SideCondition)
@@ -101,9 +95,6 @@ The rule's 'ensures' clause is applied to the conditions and normalized. The
 substitution is applied to the right-hand side of the rule to produce the final
 configurations.
 
-Because the rule is known to apply, @finalizeAppliedRule@ always returns exactly
-one branch.
-
 See also: 'applyInitialConditions'
 -}
 finalizeAppliedRule ::
@@ -112,31 +103,34 @@ finalizeAppliedRule ::
     -- | Applied rule
     RulePattern RewritingVariableName ->
     -- | Conditions of applied rule
-    OrCondition RewritingVariableName ->
-    LogicT Simplifier (OrPattern RewritingVariableName)
+    Condition RewritingVariableName ->
+    LogicT Simplifier (Pattern RewritingVariableName)
 finalizeAppliedRule
     sideCondition
     renamedRule
-    appliedConditions =
-        MultiOr.gather $
-            finalizeAppliedRuleWorker =<< Logic.scatter appliedConditions
+    appliedCondition = do
+        let avoidVars = freeVariables appliedCondition <> freeVariables ruleRHS
+            finalPattern =
+                Rule.topExistsToImplicitForall avoidVars ruleRHS
+
+        -- `constructConfiguration` may simplify the configuration to bottom
+        -- we want to "catch" this and return a #bottom Pattern
+        catchSimplifiesToBottom (termLikeSort $ term finalPattern)
+            =<< Logic.gather
+                ( -- Combine the initial conditions, the unification conditions, and the
+                  -- axiom ensures clause. The axiom requires clause is included by
+                  -- unifyRule.
+                  constructConfiguration
+                    sideCondition
+                    appliedCondition
+                    finalPattern
+                )
       where
         ruleRHS = Rule.rhs renamedRule
 
-        finalizeAppliedRuleWorker ::
-            Condition RewritingVariableName ->
-            LogicT Simplifier (Pattern RewritingVariableName)
-        finalizeAppliedRuleWorker appliedCondition = do
-            -- Combine the initial conditions, the unification conditions, and the
-            -- axiom ensures clause. The axiom requires clause is included by
-            -- unifyRule.
-            let avoidVars = freeVariables appliedCondition <> freeVariables ruleRHS
-                finalPattern =
-                    Rule.topExistsToImplicitForall avoidVars ruleRHS
-            constructConfiguration
-                sideCondition
-                appliedCondition
-                finalPattern
+        catchSimplifiesToBottom srt = \case
+            [] -> return $ pure $ mkBottom srt
+            xs -> Logic.scatter xs
 
 {- | Combine all the conditions to apply rule and construct the result.
 
@@ -191,27 +185,29 @@ finalizeAppliedClaim ::
     -- | Applied rule
     ClaimPattern ->
     -- | Conditions of applied rule
-    OrCondition RewritingVariableName ->
-    LogicT Simplifier (OrPattern RewritingVariableName)
-finalizeAppliedClaim sideCondition renamedRule appliedConditions =
-    MultiOr.gather $
-        finalizeAppliedRuleWorker =<< Logic.scatter appliedConditions
+    Condition RewritingVariableName ->
+    LogicT Simplifier (Pattern RewritingVariableName)
+finalizeAppliedClaim sideCondition renamedRule appliedCondition =
+    -- `constructConfiguration` may simplify the configuration to bottom
+    -- we want to "catch" this and return a #bottom Pattern
+    catchSimplifiesToBottom (Claim.getClaimPatternSort renamedRule)
+        =<< Logic.gather
+            ( Claim.assertRefreshed renamedRule $ do
+                finalPattern <- Logic.scatter right
+                -- Combine the initial conditions, the unification conditions, and
+                -- the axiom ensures clause. The axiom requires clause is included
+                -- by unifyRule.
+                constructConfiguration
+                    sideCondition
+                    appliedCondition
+                    finalPattern
+            )
   where
     ClaimPattern{right} = renamedRule
 
-    finalizeAppliedRuleWorker ::
-        Condition RewritingVariableName ->
-        LogicT Simplifier (Pattern RewritingVariableName)
-    finalizeAppliedRuleWorker appliedCondition =
-        Claim.assertRefreshed renamedRule $ do
-            finalPattern <- Logic.scatter right
-            -- Combine the initial conditions, the unification conditions, and
-            -- the axiom ensures clause. The axiom requires clause is included
-            -- by unifyRule.
-            constructConfiguration
-                sideCondition
-                appliedCondition
-                finalPattern
+    catchSimplifiesToBottom srt = \case
+        [] -> return $ pure $ mkBottom srt
+        xs -> Logic.scatter xs
 
 type UnifyingRuleWithRepresentation representation rule =
     ( Rule.UnifyingRule representation
@@ -225,8 +221,8 @@ type UnifyingRuleWithRepresentation representation rule =
 
 type FinalizeApplied rule =
     rule ->
-    OrCondition RewritingVariableName ->
-    LogicT Simplifier (OrPattern RewritingVariableName)
+    Condition RewritingVariableName ->
+    LogicT Simplifier (Pattern RewritingVariableName)
 
 finalizeRule ::
     UnifyingRuleWithRepresentation representation rule =>
@@ -257,8 +253,7 @@ finalizeRule
             checkSubstitutionCoverage initial (toRule <$> unifiedRule)
             let renamedRule = Conditional.term unifiedRule
             final <- finalizeApplied renamedRule applied
-            let result =
-                    OrPattern.map (resetResultPattern initialVariables) final
+            let result = resetResultPattern initialVariables final
             return Step.Result{appliedRule = unifiedRule, result}
 
 -- | Finalizes a list of applied rules into 'Results'.