Remove old TermLike simplifier

kore/src/Kore/Builtin/AssociativeCommutative.hs

@@ -1076,7 +1076,8 @@ unifyEqualsNormalizedAc
             TermLike RewritingVariableName ->
             unifier (Pattern RewritingVariableName)
         simplify term =
-            lowerLogicT $ simplifyConditionalTerm SideCondition.topTODO term
+            simplifyPatternScatter SideCondition.topTODO (Pattern.fromTermLike term)
+                & lowerLogicT
 
         simplifyPair ::
             ( TermLike RewritingVariableName
@@ -1119,11 +1120,13 @@ unifyEqualsNormalizedAc
                     `andCondition` simplifiedValueCondition
                 )
           where
+            -- TODO: can this be rewritten?
             simplifyTermLike' ::
                 TermLike RewritingVariableName ->
                 unifier (Pattern RewritingVariableName)
             simplifyTermLike' term =
-                lowerLogicT $ simplifyConditionalTerm SideCondition.topTODO term
+                simplifyPatternScatter SideCondition.topTODO (Pattern.fromTermLike term)
+                    & lowerLogicT
 
 buildResultFromUnifiers ::
     forall normalized unifier variable.

kore/src/Kore/Internal/OrPattern.hs

@@ -5,6 +5,7 @@ License     : BSD-3-Clause
 module Kore.Internal.OrPattern (
     OrPattern,
     coerceSort,
+    markSimplified,
     isSimplified,
     hasSimplifiedChildren,
     hasSimplifiedChildrenIgnoreConditions,
@@ -81,6 +82,12 @@ import Prelude.Kore
 -- | The disjunction of 'Pattern'.
 type OrPattern variable = MultiOr (Pattern variable)
 
+markSimplified ::
+    InternalVariable variable =>
+    OrPattern variable ->
+    OrPattern variable
+markSimplified = MultiOr.map Pattern.markSimplified
+
 isSimplified :: SideCondition.Representation -> OrPattern variable -> Bool
 isSimplified sideCondition = all (Pattern.isSimplified sideCondition)
 

kore/src/Kore/Internal/SideCondition.hs

@@ -281,6 +281,23 @@ addAssumptions predicates sideCondition =
             predicates <> assumedTrue sideCondition
         }
 
+areIncludedIn ::
+    Eq variable =>
+    Foldable f =>
+    f (Predicate variable) ->
+    SideCondition variable ->
+    Bool
+areIncludedIn predicates sideCondition =
+    all (flip isIncludedIn sideCondition) predicates
+
+isIncludedIn ::
+    Eq variable =>
+    Predicate variable ->
+    SideCondition variable ->
+    Bool
+isIncludedIn predicate SideCondition{assumedTrue} =
+    predicate `elem` assumedTrue
+
 {- | Assumes a 'Condition' to be true in the context of another
 'SideCondition' and recalculates the term replacements table
 from the combined predicate.
@@ -292,19 +309,22 @@ addConditionWithReplacements ::
     SideCondition variable
 addConditionWithReplacements
     (from @(Condition _) @(MultiAnd _) -> newCondition)
-    sideCondition =
-        let combinedConditions = oldCondition <> newCondition
-            (assumedTrue, assumptions) =
-                simplifyConjunctionByAssumption combinedConditions
-                    & extract
-            Assumptions replacementsTermLike replacementsPredicate = assumptions
-         in SideCondition
-                { assumedTrue
-                , replacementsTermLike
-                , replacementsPredicate
-                , definedTerms
-                , simplifiedFunctions
-                }
+    sideCondition
+        | newCondition `areIncludedIn` sideCondition =
+            sideCondition
+        | otherwise =
+            let combinedConditions = oldCondition <> newCondition
+                (assumedTrue, assumptions) =
+                    simplifyConjunctionByAssumption combinedConditions
+                        & extract
+                Assumptions replacementsTermLike replacementsPredicate = assumptions
+             in SideCondition
+                    { assumedTrue
+                    , replacementsTermLike
+                    , replacementsPredicate
+                    , definedTerms
+                    , simplifiedFunctions
+                    }
       where
         SideCondition
             { assumedTrue = oldCondition

kore/src/Kore/Rewrite/Function/Evaluator.hs

@@ -271,7 +271,7 @@ maybeEvaluatePattern
             | toSimplify == unchangedPatt =
                 return (OrPattern.fromPattern unchangedPatt)
             | otherwise =
-                reevaluateFunctions sideCondition toSimplify
+                simplifyPattern sideCondition toSimplify
 
 evaluateSortInjection ::
     InternalVariable variable =>
@@ -323,22 +323,6 @@ sortInjectionSorts symbol =
                 , "should have two sort parameters."
                 ]
 
-{- | 'reevaluateFunctions' re-evaluates functions after a user-defined function
-was evaluated.
--}
-reevaluateFunctions ::
-    MonadSimplify simplifier =>
-    SideCondition RewritingVariableName ->
-    -- | Function evaluation result.
-    Pattern RewritingVariableName ->
-    simplifier (OrPattern RewritingVariableName)
-reevaluateFunctions sideCondition rewriting = do
-    let (rewritingTerm, rewritingCondition) = Pattern.splitTerm rewriting
-    OrPattern.observeAllT $ do
-        simplifiedTerm <- simplifyConditionalTerm sideCondition rewritingTerm
-        simplifyCondition sideCondition $
-            Pattern.andCondition simplifiedTerm rewritingCondition
-
 -- | Ands the given condition-substitution to the given function evaluation.
 mergeWithConditionAndSubstitution ::
     MonadSimplify simplifier =>

kore/src/Kore/Simplify/Data.hs

@@ -48,9 +48,8 @@ import Kore.IndexedModule.MetadataTools (
 import qualified Kore.IndexedModule.MetadataToolsBuilder as MetadataTools
 import qualified Kore.IndexedModule.OverloadGraph as OverloadGraph
 import qualified Kore.IndexedModule.SortGraph as SortGraph
-import Kore.Internal.TermLike (
-    TermLike,
- )
+import Kore.Internal.Pattern (Pattern)
+import qualified Kore.Internal.Pattern as Pattern
 import qualified Kore.Rewrite.Axiom.EvaluationStrategy as Axiom.EvaluationStrategy
 import Kore.Rewrite.Axiom.Identifier (
     matchAxiomIdentifier,
@@ -66,6 +65,7 @@ import Kore.Rewrite.RewritingVariable (
 import qualified Kore.Simplify.Condition as Condition
 import Kore.Simplify.InjSimplifier
 import Kore.Simplify.OverloadSimplifier
+import qualified Kore.Simplify.Pattern as Pattern
 import Kore.Simplify.Simplify
 import qualified Kore.Simplify.SubstitutionSimplifier as SubstitutionSimplifier
 import qualified Kore.Simplify.TermLike as TermLike
@@ -117,10 +117,10 @@ instance (MonadMask prof, MonadProf prof) => MonadProf (SimplifierT prof) where
 
 traceProfSimplify ::
     MonadProf prof =>
-    TermLike RewritingVariableName ->
+    Pattern RewritingVariableName ->
     prof a ->
     prof a
-traceProfSimplify termLike =
+traceProfSimplify (Pattern.toTermLike -> termLike) =
     maybe id traceProf ident
   where
     ident =
@@ -137,14 +137,12 @@ instance
     askMetadataTools = asks metadataTools
     {-# INLINE askMetadataTools #-}
 
-    simplifyTermLike sideCondition termLike =
-        traceProfSimplify termLike (TermLike.simplify sideCondition termLike)
-    {-# INLINE simplifyTermLike #-}
+    simplifyPattern sideCondition patt =
+        traceProfSimplify patt (Pattern.makeEvaluate sideCondition patt)
+    {-# INLINE simplifyPattern #-}
 
-    simplifyTermLikeOnly sideCondition termLike =
-        (traceProfSimplify termLike)
-            (TermLike.simplifyOnly sideCondition termLike)
-    {-# INLINE simplifyTermLikeOnly #-}
+    simplifyTerm = TermLike.simplify
+    {-# INLINE simplifyTerm #-}
 
     simplifyCondition topCondition conditional = do
         ConditionSimplifier simplify <- asks simplifierCondition

kore/src/Kore/Simplify/Exists.hs

@@ -70,9 +70,6 @@ import Kore.Rewrite.RewritingVariable (
 import qualified Kore.Simplify.AndPredicates as And (
     simplifyEvaluatedMultiPredicate,
  )
-import qualified Kore.Simplify.Pattern as Pattern (
-    makeEvaluate,
- )
 import Kore.Simplify.Simplify
 import Kore.Substitute
 import qualified Kore.TopBottom as TopBottom
@@ -308,7 +305,8 @@ makeEvaluateBoundLeft sideCondition variable boundTerm normalized =
                             Conditional.predicate normalized
                     }
         orPattern <-
-            lift $ Pattern.makeEvaluate sideCondition substituted
+            simplifyPattern sideCondition substituted
+                & lift
         Logic.scatter (toList orPattern)
   where
     someVariableName = inject (variableName variable)

kore/src/Kore/Simplify/Pattern.hs

@@ -46,9 +46,10 @@ import Kore.Rewrite.RewritingVariable (
 import Kore.Simplify.Simplify (
     MonadSimplify,
     simplifyCondition,
-    simplifyConditionalTerm,
+    simplifyTerm,
  )
 import Kore.Substitute
+import qualified Logic
 import Prelude.Kore
 
 -- | Simplifies the 'Pattern' and removes the exists quantifiers at the top.
@@ -110,21 +111,35 @@ This should only be used when it's certain that the
 the 'Pattern'.
 -}
 makeEvaluate ::
+    forall simplifier.
     MonadSimplify simplifier =>
     SideCondition RewritingVariableName ->
     Pattern RewritingVariableName ->
     simplifier (OrPattern RewritingVariableName)
-makeEvaluate sideCondition pattern' =
-    OrPattern.observeAllT $ do
-        withSimplifiedCondition <- simplifyCondition sideCondition pattern'
-        let (term, simplifiedCondition) =
-                Conditional.splitTerm withSimplifiedCondition
-            term' = substitute (toMap $ substitution simplifiedCondition) term
-            termSideCondition =
-                SideCondition.addConditionWithReplacements
-                    simplifiedCondition
-                    sideCondition
-        simplifiedTerm <- simplifyConditionalTerm termSideCondition term'
-        let simplifiedPattern =
-                Conditional.andCondition simplifiedTerm simplifiedCondition
-        simplifyCondition sideCondition simplifiedPattern
+makeEvaluate sideCondition =
+    loop . OrPattern.fromPattern
+  where
+    loop input = do
+        output <-
+            OrPattern.traverse worker input
+                & fmap OrPattern.flatten
+        if input == output
+            then pure output
+            else loop output
+
+    worker pattern' =
+        OrPattern.observeAllT $ do
+            withSimplifiedCondition <- simplifyCondition sideCondition pattern'
+            let (term, simplifiedCondition) =
+                    Conditional.splitTerm withSimplifiedCondition
+                term' = substitute (toMap $ substitution simplifiedCondition) term
+                termSideCondition =
+                    SideCondition.addConditionWithReplacements
+                        simplifiedCondition
+                        sideCondition
+            simplifiedTerm <-
+                simplifyTerm termSideCondition term'
+                    >>= Logic.scatter
+            let simplifiedPattern =
+                    Conditional.andCondition simplifiedTerm simplifiedCondition
+            simplifyCondition sideCondition simplifiedPattern

kore/src/Kore/Simplify/Predicate.hs

@@ -133,14 +133,14 @@ simplify sideCondition original =
     replacePredicate = SideCondition.replacePredicate sideCondition
 
     -- If the child 'TermLike' is a term representing a predicate,
-    -- 'simplifyTermLikeOnly' will not attempt to simplify it, so
+    -- 'simplifyTerm' will not attempt to simplify it, so
     -- it should be transformed into a 'Predicate' and simplified
     -- accordingly.
-    simplifyTerm term
+    simplifyTerm' term
         | Right predicate <- Predicate.makePredicate term =
             toOrPattern (termLikeSort term) <$> worker predicate
         | otherwise =
-            simplifyTermLikeOnly sideCondition term
+            simplifyTerm sideCondition term
 
     repr = SideCondition.toRepresentation sideCondition
 
@@ -167,10 +167,10 @@ simplify sideCondition original =
                 ImpliesF impliesF -> simplifyImplies =<< traverse worker impliesF
                 IffF iffF -> simplifyIff =<< traverse worker iffF
                 CeilF ceilF ->
-                    simplifyCeil sideCondition =<< traverse simplifyTerm ceilF
+                    simplifyCeil sideCondition =<< traverse simplifyTerm' ceilF
                 FloorF floorF@(Floor _ _ child) ->
                     simplifyFloor (termLikeSort child) sideCondition
-                        =<< traverse simplifyTerm floorF
+                        =<< traverse simplifyTerm' floorF
                 ExistsF existsF ->
                     traverse worker (Exists.refreshExists avoid existsF)
                         >>= simplifyExists sideCondition
@@ -179,9 +179,9 @@ simplify sideCondition original =
                         >>= simplifyForall sideCondition
                 EqualsF equalsF@(Equals _ _ term _) ->
                     simplifyEquals sideCondition (termLikeSort term)
-                        =<< traverse simplifyTerm equalsF
+                        =<< traverse simplifyTerm' equalsF
                 InF inF ->
-                    simplifyIn sideCondition =<< traverse simplifyTerm inF
+                    simplifyIn sideCondition =<< traverse simplifyTerm' inF
       where
         _ :< predicateF = Recursive.project predicate
         ~avoid = freeVariableNames sideCondition

kore/src/Kore/Simplify/Rule.hs

@@ -20,6 +20,7 @@ import Kore.Internal.Predicate (
     pattern PredicateTrue,
  )
 import qualified Kore.Internal.Predicate as Predicate
+import qualified Kore.Internal.SideCondition as SideCondition
 import qualified Kore.Internal.Substitution as Substitution
 import Kore.Internal.TermLike (
     TermLike,
@@ -34,7 +35,6 @@ import Kore.Rewrite.RewritingVariable (
     RewritingVariableName,
  )
 import Kore.Rewrite.RulePattern
-import qualified Kore.Simplify.Pattern as Pattern
 import Kore.Simplify.Simplify (
     MonadSimplify,
  )
@@ -64,7 +64,7 @@ simplifyRulePattern ::
     simplifier (RulePattern RewritingVariableName)
 simplifyRulePattern rule = do
     let RulePattern{left} = rule
-    simplifiedLeft <- simplifyPattern left
+    simplifiedLeft <- simplifyPattern' left
     case OrPattern.toPatterns simplifiedLeft of
         [Conditional{term, predicate, substitution}]
             | PredicateTrue <- predicate -> do
@@ -109,7 +109,7 @@ simplifyClaimPattern ::
     simplifier ClaimPattern
 simplifyClaimPattern claim = do
     let ClaimPattern{left} = claim
-    simplifiedLeft <- simplifyPattern (Pattern.term left)
+    simplifiedLeft <- simplifyPattern' (Pattern.term left)
     case OrPattern.toPatterns simplifiedLeft of
         [Conditional{term, predicate, substitution}]
             | PredicateTrue <- predicate ->
@@ -132,10 +132,12 @@ simplifyClaimPattern claim = do
             return claim
 
 -- | Simplify a 'TermLike' using only matching logic rules.
-simplifyPattern ::
+simplifyPattern' ::
     MonadSimplify simplifier =>
     TermLike RewritingVariableName ->
     simplifier (OrPattern RewritingVariableName)
-simplifyPattern termLike =
+simplifyPattern' termLike =
     Simplifier.localSimplifierAxioms (const mempty) $
-        Pattern.simplify (Pattern.fromTermLike termLike)
+        Simplifier.simplifyPattern
+            SideCondition.top
+            (Pattern.fromTermLike termLike)