Inefficient Equation renaming (#2438)

Co-authored-by: Thomas Tuegel <[email protected]>

Co-authored-by: andreiburdusa <[email protected]>
Co-authored-by: Thomas Tuegel <[email protected]>

Author: andreiburdusa

kore/src/Kore/Equation/Application.hs

@@ -95,6 +95,7 @@ import Kore.Internal.TermLike
 import qualified Kore.Internal.TermLike as TermLike
 import Kore.Rewriting.RewritingVariable
     ( RewritingVariableName
+    , withoutEquationVariables
     )
 import Kore.Step.Axiom.Matcher
     ( MatchResult
@@ -156,6 +157,7 @@ attemptEquation
     -> Equation RewritingVariableName
     -> simplifier (AttemptEquationResult RewritingVariableName)
 attemptEquation sideCondition termLike equation =
+    assertNoEquationVar (freeVariables termLike) $
     whileDebugAttemptEquation' $ runExceptT $ do
         let Equation { left, argument, antiLeft } = equationRenamed
         (equation', predicate) <- matchAndApplyResults left argument antiLeft
@@ -177,25 +179,27 @@ attemptEquation sideCondition termLike equation =
     matchAndApplyResults left' argument' antiLeft'
       | isNothing argument'
       , isNothing antiLeft' = do
-          matchResult <- match left' termLike & whileMatch
-          applyMatchResult equationRenamed matchResult
-              & whileApplyMatchResult
+        matchResult <- match left' termLike & whileMatch
+        applyMatchResult equationRenamed matchResult
+            & whileApplyMatchResult
       | otherwise = do
-          (matchPredicate, matchSubstitution) <-
-              match left' termLike
-              & whileMatch
-          matchResults <-
-              applySubstitutionAndSimplify
-                  argument'
-                  antiLeft'
-                  matchSubstitution
-              & whileMatch
-          (equation', predicate) <-
-              applyAndSelectMatchResult matchResults
-          return
-              ( equation'
-              , makeAndPredicate predicate matchPredicate
-              )
+        (matchPredicate, matchSubstitution) <-
+            match left' termLike
+            & whileMatch
+        matchResults <-
+            applySubstitutionAndSimplify
+                argument'
+                antiLeft'
+                matchSubstitution
+            & whileMatch
+        (equation', predicate) <-
+            applyAndSelectMatchResult matchResults
+        assertNoEquationVar (freeVariables equation' <> freeVariables predicate)
+            $ return
+                ( equation'
+                , makeAndPredicate predicate matchPredicate
+                )
+    assertNoEquationVar = assert . withoutEquationVariables
 
     applyAndSelectMatchResult
         :: [MatchResult RewritingVariableName]

kore/src/Kore/Rewriting/RewritingVariable.hs

@@ -11,6 +11,8 @@ module Kore.Rewriting.RewritingVariable
     , isEquationVariable
     , isConfigVariable
     , isRuleVariable
+    , isSomeEquationVariable
+    , isSomeEquationVariableName
     , isSomeConfigVariable
     , isSomeConfigVariableName
     , isSomeRuleVariable
@@ -34,6 +36,7 @@ module Kore.Rewriting.RewritingVariable
     , resetConfigVariable
     , resetRuleVariable
     , getRewritingVariable
+    , withoutEquationVariables
     -- * Exported for unparsing/testing
     , getRewritingPattern
     , getRewritingTerm
@@ -52,6 +55,7 @@ import Kore.AST.AstWithLocation
     )
 import Kore.Attribute.Pattern.FreeVariables
     ( FreeVariables
+    , toNames
     )
 import qualified Kore.Attribute.Pattern.FreeVariables as FreeVariables
 import Kore.Internal.Pattern as Pattern
@@ -285,6 +289,12 @@ assertRemainderPattern pattern' =
   where
     freeVars = freeVariables pattern' & FreeVariables.toList
 
+isSomeEquationVariable :: SomeVariable RewritingVariableName -> Bool
+isSomeEquationVariable = isSomeEquationVariableName . variableName
+
+isSomeEquationVariableName :: SomeVariableName RewritingVariableName -> Bool
+isSomeEquationVariableName = foldSomeVariableName (pure isEquationVariable)
+
 isSomeConfigVariable :: SomeVariable RewritingVariableName -> Bool
 isSomeConfigVariable = isSomeConfigVariableName . variableName
 
@@ -302,3 +312,8 @@ isElementRuleVariable = isElementRuleVariableName . variableName
 
 isElementRuleVariableName :: ElementVariableName RewritingVariableName -> Bool
 isElementRuleVariableName = any isRuleVariable
+
+withoutEquationVariables
+    :: FreeVariables RewritingVariableName -> Bool
+withoutEquationVariables fv =
+    (not . any isSomeEquationVariableName) (toNames fv)

kore/src/Kore/Step/Simplification/Data.hs

@@ -55,7 +55,7 @@ import Kore.Internal.TermLike
     )
 import Kore.Rewriting.RewritingVariable
     ( RewritingVariableName
-    , mkRuleVariable
+    , mkEquationVariable
     )
 import qualified Kore.Step.Axiom.EvaluationStrategy as Axiom.EvaluationStrategy
 import Kore.Step.Axiom.Identifier
@@ -249,7 +249,7 @@ evalSimplifier verifiedModule simplifier = do
     initialize = do
         equations <-
             Equation.simplifyExtractedEquations
-            $ (Map.map . fmap . Equation.mapVariables $ pure mkRuleVariable)
+            $ (Map.map . fmap . Equation.mapVariables $ pure mkEquationVariable)
             $ Equation.extractEquations verifiedModule'
         let
             builtinEvaluators, userEvaluators, simplifierAxioms