Cache simplified functions in SideCondition (#2662)

* WIP: keep and use metadata of simplified functions in SideCondition

* Format with fourmolu

* Cache when doing proof rewrites

* Format with fourmolu

* Move call to cacheSimplified.. at the top

* Format with fourmolu

* Update golden file

* SideCondition.Representation: remove simplifiedFunctions

* Format with fourmolu

* Revert change to integration test

* Clean-up and documentation

* Format with fourmolu

* Add unit tests

* Format with fourmolu

* Revert changes to AllPathClaim

* Factor out recursive call

Co-authored-by: Octavian Mircea Sebe <[email protected]>

Co-authored-by: github-actions <[email protected]>
Co-authored-by: Octavian Mircea Sebe <[email protected]>
Co-authored-by: rv-jenkins <[email protected]>

Author: 4 people

kore/src/Kore/Internal/SideCondition.hs

@@ -25,6 +25,9 @@ module Kore.Internal.SideCondition (
     fromDefinedTerms,
     generateNormalizedAcs,
     simplifyConjunctionByAssumption,
+    cacheSimplifiedFunctions,
+    isSimplifiedFunction,
+    fromSimplifiedFunctions,
 ) where
 
 import Changed
@@ -96,11 +99,13 @@ import Kore.Internal.Predicate (
 import qualified Kore.Internal.Predicate as Predicate
 import Kore.Internal.SideCondition.SideCondition as SideCondition
 import Kore.Internal.Symbol (
+    Symbol,
     isConstructor,
     isFunction,
     isFunctional,
  )
 import Kore.Internal.TermLike (
+    Application,
     Key,
     TermLike,
     pattern App_,
@@ -140,9 +145,12 @@ import qualified SQL
 
 {- | Side condition used in the evaluation context.
 
-It contains a predicate assumed to be true, and a table of term replacements,
-which is used when simplifying terms. The table is constructed from the predicate,
-see 'simplifyConjunctionByAssumption'.
+It contains:
+* a predicate assumed to be true
+* a table of term replacements which is used when simplifying terms
+* a set of terms which are assumed to be defined
+* a set of terms with function application at the top which are known to have been
+  simplified as much as possible during the current rewrite step
 
 Warning! When simplifying a pattern, extra care should be taken that the
 'SideCondition' sent to the simplifier isn't created from the same 'Condition'
@@ -158,6 +166,8 @@ data SideCondition variable = SideCondition
     , replacementsPredicate ::
         !(HashMap (Predicate variable) (Predicate variable))
     , definedTerms :: !(HashSet (TermLike variable))
+    , simplifiedFunctions ::
+        !(HashSet (Application Symbol (TermLike variable)))
     }
     deriving stock (Eq, Ord, Show)
     deriving stock (GHC.Generic)
@@ -170,11 +180,14 @@ instance InternalVariable variable => SQL.Column (SideCondition variable) where
     toColumn = SQL.toColumn . Pretty.renderText . Pretty.layoutOneLine . pretty
 
 instance Ord variable => HasFreeVariables (SideCondition variable) variable where
-    freeVariables sideCondition@(SideCondition _ _ _ _) =
+    freeVariables sideCondition@(SideCondition _ _ _ _ _) =
         freeVariables assumedTrue
             <> foldMap freeVariables definedTerms
       where
-        SideCondition{assumedTrue, definedTerms} = sideCondition
+        SideCondition
+            { assumedTrue
+            , definedTerms
+            } = sideCondition
 
 instance InternalVariable variable => Pretty (SideCondition variable) where
     pretty
@@ -208,7 +221,7 @@ instance InternalVariable variable => Pretty (SideCondition variable) where
                        ]
 
 instance From (SideCondition variable) (MultiAnd (Predicate variable)) where
-    from condition@(SideCondition _ _ _ _) = assumedTrue condition
+    from condition@(SideCondition _ _ _ _ _) = assumedTrue condition
     {-# INLINE from #-}
 
 instance
@@ -234,9 +247,10 @@ assumeTrue ::
 assumeTrue assumedTrue =
     SideCondition
         { assumedTrue
-        , definedTerms = HashSet.empty
         , replacementsTermLike = HashMap.empty
         , replacementsPredicate = HashMap.empty
+        , definedTerms = HashSet.empty
+        , simplifiedFunctions = HashSet.empty
         }
 
 {- | Assumes a single 'Predicate' to be true in the context of another
@@ -272,25 +286,30 @@ from the combined predicate.
 -}
 addConditionWithReplacements ::
     InternalVariable variable =>
-    SideCondition variable ->
     Condition variable ->
+    SideCondition variable ->
     SideCondition variable
 addConditionWithReplacements
-    sideCondition
-    (from @(Condition _) @(MultiAnd _) -> newCondition) =
+    (from @(Condition _) @(MultiAnd _) -> newCondition)
+    sideCondition =
         let combinedConditions = oldCondition <> newCondition
             (assumedTrue, assumptions) =
                 simplifyConjunctionByAssumption combinedConditions
                     & extract
             Assumptions replacementsTermLike replacementsPredicate = assumptions
          in SideCondition
                 { assumedTrue
-                , definedTerms
                 , replacementsTermLike
                 , replacementsPredicate
+                , definedTerms
+                , simplifiedFunctions
                 }
       where
-        SideCondition{assumedTrue = oldCondition, definedTerms} = sideCondition
+        SideCondition
+            { assumedTrue = oldCondition
+            , definedTerms
+            , simplifiedFunctions
+            } = sideCondition
 
 {- | Smart constructor for creating a 'SideCondition' by just constructing
  the replacement table from a conjunction of predicates.
@@ -310,6 +329,7 @@ constructReplacements predicates =
             , replacementsTermLike
             , replacementsPredicate
             , definedTerms = HashSet.empty
+            , simplifiedFunctions = HashSet.empty
             }
 
 {- | Smart constructor for creating a `SideCondition` by assuming
@@ -338,9 +358,10 @@ top :: InternalVariable variable => SideCondition variable
 top =
     SideCondition
         { assumedTrue = MultiAnd.top
-        , definedTerms = mempty
         , replacementsTermLike = mempty
         , replacementsPredicate = mempty
+        , definedTerms = mempty
+        , simplifiedFunctions = mempty
         }
 
 -- TODO(ana.pantilie): Should we look into removing this?
@@ -353,7 +374,7 @@ toPredicate ::
     InternalVariable variable =>
     SideCondition variable ->
     Predicate variable
-toPredicate condition@(SideCondition _ _ _ _) =
+toPredicate condition@(SideCondition _ _ _ _ _) =
     Predicate.makeAndPredicate
         assumedTruePredicate
         definedPredicate
@@ -372,7 +393,7 @@ mapVariables ::
     AdjSomeVariableName (variable1 -> variable2) ->
     SideCondition variable1 ->
     SideCondition variable2
-mapVariables adj condition@(SideCondition _ _ _ _) =
+mapVariables adj condition@(SideCondition _ _ _ _ _) =
     let assumedTrue' =
             MultiAnd.map (Predicate.mapVariables adj) assumedTrue
         replacementsTermLike' =
@@ -381,18 +402,22 @@ mapVariables adj condition@(SideCondition _ _ _ _) =
             mapKeysAndValues (Predicate.mapVariables adj) replacementsPredicate
         definedTerms' =
             HashSet.map (TermLike.mapVariables adj) definedTerms
+        simplifiedFunctions' =
+            (HashSet.map . fmap) (TermLike.mapVariables adj) simplifiedFunctions
      in SideCondition
             { assumedTrue = assumedTrue'
             , replacementsTermLike = replacementsTermLike'
             , replacementsPredicate = replacementsPredicate'
             , definedTerms = definedTerms'
+            , simplifiedFunctions = simplifiedFunctions'
             }
   where
     SideCondition
         { assumedTrue
-        , definedTerms
         , replacementsTermLike
         , replacementsPredicate
+        , definedTerms
+        , simplifiedFunctions
         } = condition
 
 -- | Utility function for mapping on the keys and values of a 'HashMap'.
@@ -414,11 +439,18 @@ fromDefinedTerms ::
 fromDefinedTerms definedTerms =
     top{definedTerms}
 
+{- | Prepares the 'SideCondition' for storing in the term attributes.
+ Any metadata information used only in particular places during execution
+ is erased.
+-}
 toRepresentation ::
     InternalVariable variable =>
     SideCondition variable ->
     SideCondition.Representation
-toRepresentation = mkRepresentation
+toRepresentation sideCondition =
+    let sideCondition' =
+            sideCondition{simplifiedFunctions = HashSet.empty}
+     in mkRepresentation sideCondition'
 
 -- | Looks up the term in the table of replacements.
 replaceTerm ::
@@ -908,3 +940,114 @@ generateNormalizedAcs internalAc =
 isDefinedInternal :: TermLike variable -> Bool
 isDefinedInternal =
     Attribute.isDefined . TermLike.termDefined . TermLike.extractAttributes
+
+fromSimplifiedFunctions ::
+    InternalVariable variable =>
+    HashSet (Application Symbol (TermLike variable)) ->
+    SideCondition variable
+fromSimplifiedFunctions simplifiedFunctions =
+    top{simplifiedFunctions}
+
+{- | Stores all non-constructor function symbols appearing in a term.
+ Inside a rewrite step, this information is used to avoid trying to
+ reevaluate functions which could not be evaluated during the 'Simplify'
+ stage of execution.
+
+ See 'isSimplifiedFunction'.
+-}
+cacheSimplifiedFunctions ::
+    forall variable.
+    InternalVariable variable =>
+    TermLike variable ->
+    SideCondition variable
+cacheSimplifiedFunctions =
+    fromSimplifiedFunctions
+        . extractSimplifiedFunctions
+  where
+    extractSimplifiedFunctions ::
+        TermLike variable ->
+        HashSet (Application Symbol (TermLike variable))
+    extractSimplifiedFunctions (Recursive.project -> _ :< termF) =
+        case termF of
+            TermLike.ApplySymbolF symbolApp ->
+                let symbol = TermLike.applicationSymbolOrAlias symbolApp
+                    children = TermLike.applicationChildren symbolApp
+                    childrenSet = foldMap extractSimplifiedFunctions children
+                 in if isFunction symbol && not (isConstructor symbol)
+                        then HashSet.singleton symbolApp <> childrenSet
+                        else childrenSet
+            TermLike.AndF and' ->
+                foldMap extractSimplifiedFunctions and'
+            TermLike.ApplyAliasF aliasApp ->
+                foldMap extractSimplifiedFunctions aliasApp
+            TermLike.BottomF bottom ->
+                foldMap extractSimplifiedFunctions bottom
+            TermLike.CeilF ceil ->
+                foldMap extractSimplifiedFunctions ceil
+            TermLike.DomainValueF dv ->
+                foldMap extractSimplifiedFunctions dv
+            TermLike.EqualsF equals ->
+                foldMap extractSimplifiedFunctions equals
+            TermLike.ExistsF exists ->
+                foldMap extractSimplifiedFunctions exists
+            TermLike.FloorF floor' ->
+                foldMap extractSimplifiedFunctions floor'
+            TermLike.ForallF forall' ->
+                foldMap extractSimplifiedFunctions forall'
+            TermLike.IffF iff ->
+                foldMap extractSimplifiedFunctions iff
+            TermLike.ImpliesF implies ->
+                foldMap extractSimplifiedFunctions implies
+            TermLike.InF in' ->
+                foldMap extractSimplifiedFunctions in'
+            TermLike.MuF mu ->
+                foldMap extractSimplifiedFunctions mu
+            TermLike.NextF next ->
+                foldMap extractSimplifiedFunctions next
+            TermLike.NotF not' ->
+                foldMap extractSimplifiedFunctions not'
+            TermLike.NuF nu ->
+                foldMap extractSimplifiedFunctions nu
+            TermLike.OrF or' ->
+                foldMap extractSimplifiedFunctions or'
+            TermLike.RewritesF rewrites ->
+                foldMap extractSimplifiedFunctions rewrites
+            TermLike.TopF top' ->
+                foldMap extractSimplifiedFunctions top'
+            TermLike.InhabitantF inh ->
+                foldMap extractSimplifiedFunctions inh
+            TermLike.StringLiteralF stringLit ->
+                foldMap extractSimplifiedFunctions stringLit
+            TermLike.InternalBoolF bool ->
+                foldMap extractSimplifiedFunctions bool
+            TermLike.InternalBytesF bytes ->
+                foldMap extractSimplifiedFunctions bytes
+            TermLike.InternalIntF int ->
+                foldMap extractSimplifiedFunctions int
+            TermLike.InternalStringF string ->
+                foldMap extractSimplifiedFunctions string
+            TermLike.InternalListF list ->
+                foldMap extractSimplifiedFunctions list
+            TermLike.InternalMapF map' ->
+                foldMap extractSimplifiedFunctions map'
+            TermLike.InternalSetF set ->
+                foldMap extractSimplifiedFunctions set
+            TermLike.VariableF var ->
+                foldMap extractSimplifiedFunctions var
+            TermLike.EndiannessF end ->
+                foldMap extractSimplifiedFunctions end
+            TermLike.SignednessF sign ->
+                foldMap extractSimplifiedFunctions sign
+            TermLike.InjF inj ->
+                foldMap extractSimplifiedFunctions inj
+
+{- | Decides whether a function can be further simplified or not.
+ See also 'cacheSimplifiedFunctions'.
+-}
+isSimplifiedFunction ::
+    InternalVariable variable =>
+    Application Symbol (TermLike variable) ->
+    SideCondition variable ->
+    Bool
+isSimplifiedFunction app SideCondition{simplifiedFunctions} =
+    HashSet.member app simplifiedFunctions