Simplify side conditions (#2393)

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

Author: ana-pantilie

kore/src/Kore/Attribute/Pattern.hs

@@ -12,8 +12,9 @@ module Kore.Attribute.Pattern
     , mapVariables
     , traverseVariables
     , deleteFreeVariable
-    , isFullySimplified
     , isSimplified
+    , isSimplifiedAnyCondition
+    , isSimplifiedSomeCondition
     , setSimplified
     , simplifiedAttribute
     , constructorLikeAttribute
@@ -63,12 +64,14 @@ import qualified Kore.Attribute.Pattern.FreeVariables as FreeVariables
 import Kore.Attribute.Pattern.Function
 import Kore.Attribute.Pattern.Functional
 import Kore.Attribute.Pattern.Simplified hiding
-    ( isFullySimplified
-    , isSimplified
+    ( isSimplified
+    , isSimplifiedAnyCondition
+    , isSimplifiedSomeCondition
     )
 import qualified Kore.Attribute.Pattern.Simplified as Simplified
-    ( isFullySimplified
-    , isSimplified
+    ( isSimplified
+    , isSimplifiedAnyCondition
+    , isSimplifiedSomeCondition
     )
 import Kore.Attribute.Synthetic
 import Kore.Debug
@@ -156,17 +159,26 @@ isSimplified sideCondition patt@Pattern {simplified} =
     assertSimplifiedConsistency patt
     $ Simplified.isSimplified sideCondition simplified
 
+{- Checks whether the pattern is simplified relative to some side condition.
+-}
+isSimplifiedSomeCondition
+    :: HasCallStack
+    => Pattern variable -> Bool
+isSimplifiedSomeCondition patt@Pattern {simplified} =
+    assertSimplifiedConsistency patt
+    $ Simplified.isSimplifiedSomeCondition simplified
+
 {- Checks whether the pattern is simplified relative to any side condition.
 -}
-isFullySimplified :: HasCallStack => Pattern variable -> Bool
-isFullySimplified patt@Pattern {simplified} =
+isSimplifiedAnyCondition :: HasCallStack => Pattern variable -> Bool
+isSimplifiedAnyCondition patt@Pattern {simplified} =
     assertSimplifiedConsistency patt
-    $ Simplified.isFullySimplified simplified
+    $ Simplified.isSimplifiedAnyCondition simplified
 
 assertSimplifiedConsistency :: HasCallStack => Pattern variable -> a -> a
 assertSimplifiedConsistency Pattern {constructorLike, simplified}
   | isConstructorLike constructorLike
-  , not (Simplified.isFullySimplified simplified) =
+  , not (Simplified.isSimplifiedAnyCondition simplified) =
     error "Inconsistent attributes, constructorLike implies fully simplified."
   | otherwise = id
 

kore/src/Kore/Attribute/Pattern/Simplified.hs

@@ -12,7 +12,8 @@ module Kore.Attribute.Pattern.Simplified
     , pattern Simplified_
     , Type (..)
     , isSimplified
-    , isFullySimplified
+    , isSimplifiedAnyCondition
+    , isSimplifiedSomeCondition
     , simplifiedTo
     , notSimplified
     , fullySimplified
@@ -225,6 +226,11 @@ Simplified_ _ Any `simplifiedTo` s@(Simplified_ Fully Any) = s
 
 s1@(Simplified_ _ _) `simplifiedTo` s2@(Simplified_ Partly _) = s1 <> s2
 
+{- | Is the pattern fully simplified under the given side condition?
+
+See also: 'isSimplifiedAnyCondition', 'isSimplifiedSomeCondition'.
+
+ -}
 isSimplified :: SideCondition.Representation -> Simplified -> Bool
 isSimplified _ (Simplified_ Fully Any) = True
 isSimplified currentCondition (Simplified_ Fully (Condition condition)) =
@@ -233,12 +239,26 @@ isSimplified _ (Simplified_ Fully Unknown) = False
 isSimplified _ (Simplified_ Partly _) = False
 isSimplified _ NotSimplified = False
 
-isFullySimplified :: Simplified -> Bool
-isFullySimplified (Simplified_ Fully Any) = True
-isFullySimplified (Simplified_ Fully (Condition _)) = False
-isFullySimplified (Simplified_ Fully Unknown) = False
-isFullySimplified (Simplified_ Partly _) = False
-isFullySimplified NotSimplified = False
+{- | Is the pattern fully simplified under any side condition?
+
+See also: 'isSimplified', 'isSimplifiedSomeCondition'.
+
+ -}
+isSimplifiedAnyCondition :: Simplified -> Bool
+isSimplifiedAnyCondition (Simplified_ Fully Any) = True
+isSimplifiedAnyCondition (Simplified_ Fully (Condition _)) = False
+isSimplifiedAnyCondition (Simplified_ Fully Unknown) = False
+isSimplifiedAnyCondition (Simplified_ Partly _) = False
+isSimplifiedAnyCondition NotSimplified = False
+
+{- | Is the pattern fully simplified under some side condition?
+
+See also: 'isSimplified', 'isSimplifiedAnyCondition'.
+
+ -}
+isSimplifiedSomeCondition :: Simplified -> Bool
+isSimplifiedSomeCondition (Simplified_ Fully _) = True
+isSimplifiedSomeCondition _ = False
 
 fullySimplified :: Simplified
 fullySimplified = Simplified_ Fully Any

kore/src/Kore/Attribute/PredicatePattern.hs

@@ -11,7 +11,8 @@ module Kore.Attribute.PredicatePattern
     -- simplified is excluded on purpose
     , simplifiedAttribute
     , isSimplified
-    , isFullySimplified
+    , isSimplifiedAnyCondition
+    , isSimplifiedSomeCondition
     , setSimplified
     , mapVariables
     , traverseVariables
@@ -39,12 +40,14 @@ import qualified Kore.Attribute.Pattern.FreeVariables as FreeVariables
     ( freeVariables
     )
 import Kore.Attribute.Pattern.Simplified hiding
-    ( isFullySimplified
-    , isSimplified
+    ( isSimplified
+    , isSimplifiedAnyCondition
+    , isSimplifiedSomeCondition
     )
 import qualified Kore.Attribute.Pattern.Simplified as Simplified
-    ( isFullySimplified
-    , isSimplified
+    ( isSimplified
+    , isSimplifiedAnyCondition
+    , isSimplifiedSomeCondition
     )
 import Kore.Attribute.Synthetic
 import Kore.Debug
@@ -97,12 +100,23 @@ isSimplified
     :: SideCondition.Representation -> PredicatePattern variable -> Bool
 isSimplified sideCondition = Simplified.isSimplified sideCondition . simplifiedAttribute
 
+{- Checks whether the pattern is simplified relative to some side condition.
+-}
+isSimplifiedSomeCondition
+    :: PredicatePattern variable -> Bool
+isSimplifiedSomeCondition =
+    Simplified.isSimplifiedSomeCondition . simplifiedAttribute
+
 {- Checks whether the pattern is simplified relative to any side condition.
 -}
-isFullySimplified :: PredicatePattern variable -> Bool
-isFullySimplified PredicatePattern {simplified} = Simplified.isFullySimplified simplified
+isSimplifiedAnyCondition :: PredicatePattern variable -> Bool
+isSimplifiedAnyCondition PredicatePattern {simplified} =
+    Simplified.isSimplifiedAnyCondition simplified
 
-setSimplified :: Simplified -> PredicatePattern variable -> PredicatePattern variable
+setSimplified
+    :: Simplified
+    -> PredicatePattern variable
+    -> PredicatePattern variable
 setSimplified simplified patt = patt { simplified }
 
 {- | Use the provided mapping to replace all variables in a 'Pattern'.

kore/src/Kore/Equation/Simplification.hs

@@ -37,9 +37,6 @@ import Kore.Internal.Pattern
     )
 import qualified Kore.Internal.Pattern as Pattern
 import qualified Kore.Internal.Predicate as Predicate
-import qualified Kore.Internal.SideCondition as SideCondition
-    ( top
-    )
 import qualified Kore.Internal.Substitution as Substitution
 import qualified Kore.Internal.TermLike as TermLike
 import qualified Kore.Step.Simplification.Pattern as Pattern
@@ -134,4 +131,4 @@ simplifyPattern
     -> simplifier (OrPattern variable)
 simplifyPattern patt =
     Simplifier.localSimplifierAxioms (const mempty)
-    $ Pattern.simplify SideCondition.top patt
+    $ Pattern.simplify patt

kore/src/Kore/Exec.hs

@@ -92,9 +92,6 @@ import Kore.Internal.Predicate
     , makeMultipleOrPredicate
     )
 import qualified Kore.Internal.SideCondition as SideCondition
-    ( top
-    , topTODO
-    )
 import Kore.Internal.TermLike
 import Kore.Log.ErrorRewriteLoop
     ( errorRewriteLoop
@@ -224,8 +221,7 @@ exec depthLimit breadthLimit verifiedModule strategy initialTerm =
         finals <-
             getFinalConfigsOf $ do
                 initialConfig <-
-                    Pattern.simplify SideCondition.top
-                        (Pattern.fromTermLike initialTerm)
+                    Pattern.simplify (Pattern.fromTermLike initialTerm)
                     >>= Logic.scatter
                 let
                     updateQueue = \as ->
@@ -372,8 +368,7 @@ search depthLimit breadthLimit verifiedModule termLike searchPattern searchConfi
         initialized <- initializeAndSimplify verifiedModule
         let Initialized { rewriteRules } = initialized
         simplifiedPatterns <-
-            Pattern.simplify SideCondition.top
-            $ Pattern.fromTermLike termLike
+            Pattern.simplify $ Pattern.fromTermLike termLike
         let
             initialPattern =
                 case toList simplifiedPatterns of
@@ -401,7 +396,7 @@ search depthLimit breadthLimit verifiedModule termLike searchPattern searchConfi
             searchGraph
                 searchConfig
                 (match
-                    SideCondition.topTODO
+                    SideCondition.top
                     (mkRewritingPattern searchPattern)
                 )
                 executionGraph

kore/src/Kore/Internal/OrPattern.hs

@@ -8,6 +8,7 @@ module Kore.Internal.OrPattern
     , coerceSort
     , isSimplified
     , hasSimplifiedChildren
+    , hasSimplifiedChildrenIgnoreConditions
     , forgetSimplified
     , fromPatterns
     , toPatterns
@@ -95,6 +96,18 @@ hasSimplifiedChildren
 hasSimplifiedChildren sideCondition =
     all (Pattern.hasSimplifiedChildren sideCondition)
 
+{- | Checks whether all patterns in the disjunction have simplified children,
+ignoring the conditions used to simplify them.
+
+See also: 'Pattern.hasSimplifiedChildrenIgnoreConditions'
+
+ -}
+hasSimplifiedChildrenIgnoreConditions
+    :: InternalVariable variable
+    => OrPattern variable -> Bool
+hasSimplifiedChildrenIgnoreConditions =
+    all Pattern.hasSimplifiedChildrenIgnoreConditions
+
 forgetSimplified
     :: InternalVariable variable => OrPattern variable -> OrPattern variable
 forgetSimplified = fromPatterns . map Pattern.forgetSimplified . toPatterns

kore/src/Kore/Internal/Pattern.hs

@@ -26,6 +26,7 @@ module Kore.Internal.Pattern
     , Kore.Internal.Pattern.freeElementVariables
     , isSimplified
     , hasSimplifiedChildren
+    , hasSimplifiedChildrenIgnoreConditions
     , forgetSimplified
     , markSimplified
     , simplifiedAttribute
@@ -162,6 +163,20 @@ hasSimplifiedChildren sideCondition patt =
     Conditional { term, predicate, substitution } = patt
     clauses = MultiAnd.fromPredicate predicate
 
+{- | Similar to 'hasSimplifiedChildren', only that it ignores the conditions
+used to simplify the children.
+ -}
+hasSimplifiedChildrenIgnoreConditions
+    :: Ord variable
+    => Pattern variable -> Bool
+hasSimplifiedChildrenIgnoreConditions patt =
+    TermLike.isSimplifiedSomeCondition term
+    && all Predicate.isSimplifiedSomeCondition clauses
+    && Substitution.isSimplifiedSomeCondition substitution
+  where
+    Conditional { term, predicate, substitution } = patt
+    clauses = MultiAnd.fromPredicate predicate
+
 forgetSimplified
     :: InternalVariable variable => Pattern variable -> Pattern variable
 forgetSimplified patt =

kore/src/Kore/Internal/Predicate.hs

@@ -35,6 +35,7 @@ module Kore.Internal.Predicate
     , isPredicate
     , simplifiedAttribute
     , isSimplified
+    , isSimplifiedSomeCondition
     , isFreeOf
     , freeElementVariables
     , hasFreeVariable
@@ -142,6 +143,7 @@ import Kore.Internal.TermLike hiding
     , forgetSimplified
     , hasFreeVariable
     , isSimplified
+    , isSimplifiedSomeCondition
     , mapVariables
     , markSimplified
     , markSimplifiedConditional
@@ -911,9 +913,23 @@ instance HasFreeVariables (Predicate variable) variable where
 simplifiedAttribute :: Predicate variable -> Simplified
 simplifiedAttribute = Attribute.simplifiedAttribute . extractAttributes
 
+{- | Is the 'Predicate' fully simplified under the given side condition?
+
+See also: 'isSimplifiedSomeCondition'.
+
+ -}
 isSimplified :: SideCondition.Representation -> Predicate variable -> Bool
 isSimplified condition = Attribute.isSimplified condition . extractAttributes
 
+{- | Is the 'Predicate' fully simplified under some side condition?
+
+See also: 'isSimplified'.
+
+ -}
+isSimplifiedSomeCondition :: Predicate variable -> Bool
+isSimplifiedSomeCondition =
+    Attribute.isSimplifiedSomeCondition . extractAttributes
+
 cannotSimplifyNotSimplifiedError
     :: (HasCallStack, InternalVariable variable)
     => PredicateF variable (Predicate variable) -> a

kore/src/Kore/Internal/SideCondition/SideCondition.hs

@@ -9,10 +9,14 @@ module Kore.Internal.SideCondition.SideCondition
     ) where
 
 import Prelude.Kore
+import Pretty
+    ( Pretty (..)
+    )
 
 import Data.Hashable
     ( Hashed
     , hashed
+    , unhashed
     )
 
 import Data.Type.Equality
@@ -30,7 +34,7 @@ import Type.Reflection
     )
 
 data Representation where
-    Representation :: Ord a => !(TypeRep a) -> !(Hashed a) -> Representation
+    Representation :: (Ord a, Pretty a) => !(TypeRep a) -> !(Hashed a) -> Representation
 
 instance Eq Representation where
     (==) (Representation typeRep1 hashed1) (Representation typeRep2 hashed2) =
@@ -64,9 +68,12 @@ instance NFData Representation where
     rnf (Representation typeRep1 hashed1) = typeRep1 `seq` hashed1 `seq` ()
     {-# INLINE rnf #-}
 
+instance Pretty Representation where
+    pretty (Representation _ h) = pretty (unhashed h)
+
 -- | Creates a 'Representation'. Should not be used directly.
 -- See 'Kore.Internal.SideCondition.toRepresentation'.
-mkRepresentation :: (Ord a, Hashable a, Typeable a) => a -> Representation
+mkRepresentation :: (Ord a, Hashable a, Typeable a, Pretty a) => a -> Representation
 mkRepresentation = Representation typeRep . hashed
 
 instance Debug Representation where