Use new Ceil simplifier (#2653)

* OrPattern: Add fromOrCondition

* OrCondition: Add fromPredicates

* Ceil: Return OrCondition instead of OrPattern

* Equals: Return OrCondition instead of OrPattern

* Add Kore.Step.Simplification.TermLike.simplyOnly

* Test.Kore.Step.Simplification.Predicate: Add Ceil tests

* Add Test.Kore.Step.Simplification.TermLike.simplifyOnly

* Clean up Kore.Step.Simplification.Application

* Clean up Kore.Step.Simplification.Condition

* Clean up Kore.Step.Function.Evaluator

* Add instance Pretty (MultiAnd _)

* Add instance Pretty (Conditional _ (TermLike _))

* Add simplifyTermLikeOnly to MonadSimplify

* Move Ceil simplifier to new Predicate simplifier

* TermLike.simplifyOnly: Do not simplify Rewrites

* Refactor evaluateInj

* Clean up simplifyOnly

* Inj.simplify: Mark terms simplified

* Predicate.simplify: Skip simplified Predicates

* TermLike.simplifyOnly: Skip simplified TermLikes

* Warn when predicates are not simplified

* Kore.Step.Simplification.Condition.simplify: Remove redundant argument

Co-authored-by: rv-jenkins <[email protected]>

Author: ttuegel

kore/kore.cabal

@@ -335,6 +335,7 @@ library
     Kore.Log.DebugSolver
     Kore.Log.DebugSubstitutionSimplifier
     Kore.Log.DebugUnification
+    Kore.Log.DebugUnifyBottom
     Kore.Log.ErrorBottomTotalFunction
     Kore.Log.ErrorDecidePredicateUnknown
     Kore.Log.ErrorException
@@ -360,7 +361,7 @@ library
     Kore.Log.WarnStuckClaimState
     Kore.Log.WarnSymbolSMTRepresentation
     Kore.Log.WarnTrivialClaim
-    Kore.Log.DebugUnifyBottom
+    Kore.Log.WarnUnsimplifiedPredicate
     Kore.ModelChecker.Bounded
     Kore.ModelChecker.Simplification
     Kore.ModelChecker.Step

kore/src/Kore/Internal/Conditional.hs

@@ -346,6 +346,12 @@ instance
             Substitution.singleSubstitutionToPredicate
                 <$> Substitution.unwrap substitution
 
+instance
+    InternalVariable variable =>
+    Pretty (Conditional variable (TermLike variable))
+    where
+    pretty = unparse
+
 instance
     ( InternalVariable variable
     , SQL.Column term

kore/src/Kore/Internal/MultiAnd.hs

@@ -56,11 +56,17 @@ import Kore.Internal.Variable
 import Kore.TopBottom (
     TopBottom (..),
  )
+import Kore.Unparser (
+    unparseAssoc',
+ )
 import qualified Logic
 import Prelude.Kore hiding (
     map,
     traverse,
  )
+import Pretty (
+    Pretty (..),
+ )
 
 -- | 'MultiAnd' is a Matching logic and of its children
 
@@ -97,6 +103,10 @@ instance Debug child => Debug (MultiAnd child)
 
 instance (Debug child, Diff child) => Diff (MultiAnd child)
 
+instance Pretty child => Pretty (MultiAnd child) where
+    pretty = unparseAssoc' "\\and{_}" "\\top{_}()" . (<$>) pretty . getMultiAnd
+    {-# INLINE pretty #-}
+
 instance (Ord child, TopBottom child) => Semigroup (MultiAnd child) where
     (MultiAnd []) <> b = b
     a <> (MultiAnd []) = a

kore/src/Kore/Internal/OrCondition.hs

@@ -9,6 +9,7 @@ module Kore.Internal.OrCondition (
     fromConditions,
     fromCondition,
     fromPredicate,
+    fromPredicates,
     MultiOr.gather,
     MultiOr.observeAllT,
     bottom,
@@ -64,6 +65,12 @@ fromPredicate ::
     OrCondition variable
 fromPredicate = fromCondition . Condition.fromPredicate
 
+fromPredicates ::
+    InternalVariable variable =>
+    [Predicate variable] ->
+    OrCondition variable
+fromPredicates = fromConditions . map Condition.fromPredicate
+
 {- | @\\bottom@
 
 @

kore/src/Kore/Internal/OrPattern.hs

@@ -12,6 +12,7 @@ module Kore.Internal.OrPattern (
     fromPatterns,
     toPatterns,
     fromPattern,
+    fromOrCondition,
     fromTermLike,
     bottom,
     isFalse,
@@ -28,6 +29,7 @@ module Kore.Internal.OrPattern (
     MultiOr.observeAllT,
     MultiOr.map,
     MultiOr.traverse,
+    MultiOr.traverseOr,
 ) where
 
 import Kore.Internal.Condition (
@@ -42,6 +44,9 @@ import Kore.Internal.MultiOr (
     MultiOr,
  )
 import qualified Kore.Internal.MultiOr as MultiOr
+import Kore.Internal.OrCondition (
+    OrCondition,
+ )
 import Kore.Internal.Pattern (
     Pattern,
  )
@@ -69,6 +74,7 @@ import Kore.Variables.Target (
     mkElementTarget,
     targetIfEqual,
  )
+import qualified Logic
 import Prelude.Kore
 
 -- | The disjunction of 'Pattern'.
@@ -120,6 +126,14 @@ fromPatterns = from . toList
 toPatterns :: OrPattern variable -> [Pattern variable]
 toPatterns = from
 
+fromOrCondition ::
+    InternalVariable variable =>
+    Sort ->
+    OrCondition variable ->
+    OrPattern variable
+fromOrCondition sort conditions =
+    MultiOr.observeAll $ Pattern.fromCondition sort <$> Logic.scatter conditions
+
 {- | A "disjunction" of one 'TermLike'.
 
 See also: 'fromPattern'

kore/src/Kore/Log/Registry.hs

@@ -127,6 +127,9 @@ import Kore.Log.WarnSymbolSMTRepresentation (
 import Kore.Log.WarnTrivialClaim (
     WarnTrivialClaim,
  )
+import Kore.Log.WarnUnsimplifiedPredicate (
+    WarnUnsimplifiedPredicate,
+ )
 import Log (
     Entry (..),
     LogMessage,
@@ -202,6 +205,7 @@ entryHelpDocsErr, entryHelpDocsNoErr :: [Pretty.Doc ()]
             , mk $ Proxy @InfoProofDepth
             , mk $ Proxy @InfoExecDepth
             , mk $ Proxy @DebugProven
+            , mk $ Proxy @WarnUnsimplifiedPredicate
             ]
         ,
             [ mk $ Proxy @ErrorBottomTotalFunction

kore/src/Kore/Log/WarnUnsimplifiedPredicate.hs

@@ -0,0 +1,63 @@
+{- |
+Copyright   : (c) Runtime Verification, 2021
+License     : NCSA
+-}
+module Kore.Log.WarnUnsimplifiedPredicate (
+    WarnUnsimplifiedPredicate (..),
+    warnUnsimplifiedPredicate,
+) where
+
+import Kore.Internal.MultiAnd (
+    MultiAnd,
+ )
+import Kore.Internal.MultiOr (
+    MultiOr,
+ )
+import Kore.Internal.Predicate (
+    Predicate,
+ )
+import Kore.Rewriting.RewritingVariable
+import Log
+import Prelude.Kore
+import Pretty (
+    Pretty,
+ )
+import qualified Pretty
+
+data WarnUnsimplifiedPredicate = WarnUnsimplifiedPredicate
+    { limit :: !Int
+    , original :: !(Predicate RewritingVariableName)
+    , output :: !(MultiOr (MultiAnd (Predicate RewritingVariableName)))
+    }
+    deriving stock (Show)
+
+instance Pretty WarnUnsimplifiedPredicate where
+    pretty WarnUnsimplifiedPredicate{original, output, limit} =
+        Pretty.vsep
+            [ Pretty.hsep
+                [ "Predicate not simplified after"
+                , Pretty.pretty limit
+                , "rounds."
+                ]
+            , "Original predicate:"
+            , (Pretty.indent 4) (Pretty.pretty original)
+            , Pretty.hsep
+                [ "Output after"
+                , Pretty.pretty limit
+                , "rounds:"
+                ]
+            , (Pretty.indent 4) (Pretty.pretty output)
+            ]
+
+instance Entry WarnUnsimplifiedPredicate where
+    entrySeverity _ = Warning
+    helpDoc _ = "warn when a predicate is not simplified"
+
+warnUnsimplifiedPredicate ::
+    MonadLog log =>
+    Int ->
+    Predicate RewritingVariableName ->
+    MultiOr (MultiAnd (Predicate RewritingVariableName)) ->
+    log ()
+warnUnsimplifiedPredicate limit original output =
+    logEntry WarnUnsimplifiedPredicate{limit, original, output}

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

@@ -73,9 +73,8 @@ import qualified Pretty
 -- to add memoization to a function evaluator.
 evaluateApplication ::
     forall simplifier.
-    ( MonadSimplify simplifier
-    , MonadThrow simplifier
-    ) =>
+    MonadSimplify simplifier =>
+    MonadThrow simplifier =>
     -- | The predicate from the configuration
     SideCondition RewritingVariableName ->
     -- | Aggregated children predicate and substitution.

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

@@ -62,9 +62,8 @@ predicates ans substitutions, applying functions on the Application(terms),
 then merging everything into an Pattern.
 -}
 simplify ::
-    ( MonadSimplify simplifier
-    , MonadThrow simplifier
-    ) =>
+    MonadSimplify simplifier =>
+    MonadThrow simplifier =>
     SideCondition RewritingVariableName ->
     Application Symbol (OrPattern RewritingVariableName) ->
     simplifier (OrPattern RewritingVariableName)
@@ -86,9 +85,8 @@ simplify sideCondition application = do
         MultiOr.distributeApplication application
 
 makeAndEvaluateApplications ::
-    ( MonadSimplify simplifier
-    , MonadThrow simplifier
-    ) =>
+    MonadSimplify simplifier =>
+    MonadThrow simplifier =>
     SideCondition RewritingVariableName ->
     Symbol ->
     [Pattern RewritingVariableName] ->
@@ -97,9 +95,8 @@ makeAndEvaluateApplications =
     makeAndEvaluateSymbolApplications
 
 makeAndEvaluateSymbolApplications ::
-    ( MonadSimplify simplifier
-    , MonadThrow simplifier
-    ) =>
+    MonadSimplify simplifier =>
+    MonadThrow simplifier =>
     SideCondition RewritingVariableName ->
     Symbol ->
     [Pattern RewritingVariableName] ->
@@ -119,9 +116,8 @@ makeAndEvaluateSymbolApplications sideCondition symbol children = do
  as much as possible inside the current rewrite step.
 -}
 evaluateApplicationFunction ::
-    ( MonadSimplify simplifier
-    , MonadThrow simplifier
-    ) =>
+    MonadSimplify simplifier =>
+    MonadThrow simplifier =>
     -- | The predicate from the configuration
     SideCondition RewritingVariableName ->
     -- | The pattern to be evaluated

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

@@ -87,38 +87,23 @@ A ceil(or) is equal to or(ceil). We also take into account that
 simplify ::
     MonadSimplify simplifier =>
     SideCondition RewritingVariableName ->
-    Ceil Sort (OrPattern RewritingVariableName) ->
-    simplifier (OrPattern RewritingVariableName)
+    Ceil sort (OrPattern RewritingVariableName) ->
+    simplifier (OrCondition RewritingVariableName)
 simplify
     sideCondition
     Ceil{ceilChild = child} =
         simplifyEvaluated sideCondition child
 
 {- | 'simplifyEvaluated' evaluates a ceil given its child, see 'simplify'
 for details.
--}
-
-{- TODO (virgil): Preserve pattern sorts under simplification.
-
-One way to preserve the required sort annotations is to make 'simplifyEvaluated'
-take an argument of type
-
-> CofreeF (Ceil Sort) (Attribute.Pattern variable) (OrPattern variable)
-
-instead of an 'OrPattern' argument. The type of 'makeEvaluate' may
-be changed analogously. The 'Attribute.Pattern' annotation will eventually cache
-information besides the pattern sort, which will make it even more useful to
-carry around.
-
 -}
 simplifyEvaluated ::
     MonadSimplify simplifier =>
     SideCondition RewritingVariableName ->
     OrPattern RewritingVariableName ->
-    simplifier (OrPattern RewritingVariableName)
+    simplifier (OrCondition RewritingVariableName)
 simplifyEvaluated sideCondition child =
-    OrPattern.flatten
-        <$> OrPattern.traverse (makeEvaluate sideCondition) child
+    OrPattern.traverseOr (makeEvaluate sideCondition) child
 
 {- | Evaluates a ceil given its child as an Pattern, see 'simplify'
 for details.
@@ -127,33 +112,18 @@ makeEvaluate ::
     MonadSimplify simplifier =>
     SideCondition RewritingVariableName ->
     Pattern RewritingVariableName ->
-    simplifier (OrPattern RewritingVariableName)
+    simplifier (OrCondition RewritingVariableName)
 makeEvaluate sideCondition child
-    | Pattern.isTop child = return OrPattern.top
-    | Pattern.isBottom child = return OrPattern.bottom
-    | otherwise = makeEvaluateNonBoolCeil sideCondition child
-
-makeEvaluateNonBoolCeil ::
-    MonadSimplify simplifier =>
-    SideCondition RewritingVariableName ->
-    Pattern RewritingVariableName ->
-    simplifier (OrPattern RewritingVariableName)
-makeEvaluateNonBoolCeil sideCondition patt@Conditional{term}
-    | isTop term =
-        return $
-            OrPattern.fromPattern
-                patt{term = mkTop_} -- erase the term's sort.
+    | Pattern.isTop child = return OrCondition.top
+    | Pattern.isBottom child = return OrCondition.bottom
+    | isTop term = return $ OrCondition.fromCondition condition
     | otherwise = do
         termCeil <- makeEvaluateTerm sideCondition term
-        result <-
-            And.simplifyEvaluatedMultiPredicate
-                sideCondition
-                ( MultiAnd.make
-                    [ MultiOr.make [Condition.eraseConditionalTerm patt]
-                    , termCeil
-                    ]
-                )
-        return (OrPattern.map Pattern.fromCondition_ result)
+        And.simplifyEvaluatedMultiPredicate
+            sideCondition
+            (MultiAnd.make [MultiOr.make [condition], termCeil])
+  where
+    (term, condition) = Pattern.splitTerm child
 
 -- TODO: Ceil(function) should be an and of all the function's conditions, both
 -- implicit and explicit.