Move simplifyConjunctionByAssumption to Condition simplifier (#2170)

* WIP move simplifyConjunctionByAssumption to Pattern simplifier

* Refactor + fix

* Refactor

* Remove Changed

* Test.Integration.sortMatching: reorder ands

* Test.Integration.map-like simplification: reorder ands

* Integration test issue-2095: renegerate golden

* Test.Simplification.Equals: fix tests add pattern simplifier checks as well

* Move local function evaluation tests to Test.Simplification.Pattern

* Move tests from Simplification.And to Simplification.Pattern

* Remove tests

* Check for equivalence of claims in Test.Simplify.Rule

* Add a Proven branch to tests in OnePathStrategy. Is this right?

* Add definedness condition to stuck configuration. Is this right?

* Pattern.simplify: clean-up

* Update kore/src/Kore/Step/Simplification/Pattern.hs

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

* Update kore/src/Kore/Step/ClaimPattern.hs

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

* lensPredicate: move to Internal.MultiAnd

* Address review comment: move ClaimPattern.areEquivalent to test suite

* MultiAnd: sorted version of toPredicate

* Use Pattern simplifier in checkImplication and in applyRemainder

* Step.applyRemainder: simplifyCondition and then simplifyConjunctions

* simplifyConjunctions: move to condition simplifier

* simplifyConjunctions: set simplified based on whether the predicate changed

* test-issue-2095: regenerate golden

* Condition.simplify: simplify conjunctions at the end, continue if predicate changed

* Revert "Test.Integration.sortMatching: reorder ands"

This reverts commit 2521e12.

* Revert "Test.Integration.map-like simplification: reorder ands"

This reverts commit e63d5ee.

* test-issue-2095: regenerate golden

* Update kore/src/Kore/Reachability/Claim.hs

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

* Address review comments

* Address review comment

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

Author: ana-pantilie

kore/src/Kore/Internal/MultiAnd.hs

@@ -16,6 +16,7 @@ module Kore.Internal.MultiAnd
     , top
     , make
     , toPredicate
+    , toPredicateSorted
     , fromPredicate
     , fromTermLike
     , singleton
@@ -44,10 +45,12 @@ import Kore.Internal.Predicate
     ( Predicate
     , getMultiAndPredicate
     , makeAndPredicate
+    , makeTruePredicate
     , makeTruePredicate_
     )
 import Kore.Internal.TermLike
-    ( TermLike
+    ( Sort
+    , TermLike
     , TermLikeF (..)
     )
 import Kore.Internal.Variable
@@ -207,6 +210,16 @@ toPredicate (MultiAnd predicates) =
         [] -> makeTruePredicate_
         _  -> foldr1 makeAndPredicate predicates
 
+toPredicateSorted
+    :: InternalVariable variable
+    => Sort
+    -> MultiAnd (Predicate variable)
+    -> Predicate variable
+toPredicateSorted sort (MultiAnd predicates) =
+    case predicates of
+        [] -> makeTruePredicate sort
+        _  -> foldr1 makeAndPredicate predicates
+
 fromPredicate
     :: Ord variable
     => Predicate variable

kore/src/Kore/Reachability/Claim.hs

@@ -162,6 +162,9 @@ import Logic
     , MonadLogic
     )
 import qualified Logic
+import Pretty
+    ( Pretty (..)
+    )
 import qualified Pretty
 
 class Claim claim where
@@ -410,6 +413,19 @@ data CheckImplicationResult a
     deriving anyclass (SOP.Generic, SOP.HasDatatypeInfo)
     deriving anyclass (Debug, Diff)
 
+instance Pretty a => Pretty (CheckImplicationResult a) where
+    pretty Implied = "implied"
+    pretty (NotImplied a) =
+        Pretty.vsep
+            [ "not implied:"
+            , Pretty.indent 4 $ pretty a
+            ]
+    pretty (NotImpliedStuck a) =
+        Pretty.vsep
+            [ "stuck:"
+            , Pretty.indent 4 $ pretty a
+            ]
+
 -- | Remove the destination of the claim.
 checkImplication'
     :: forall claim m
@@ -513,6 +529,8 @@ checkImplicationWorker (ClaimPattern.refreshExistentials -> claimPattern) =
         stuck <-
             simplifyConditionsWithSmt sideCondition configs'
             >>= Logic.scatter
+            >>= Pattern.simplify sideCondition
+            >>= Logic.scatter
         pure (examine anyUnified stuck)
     & elseImplied
   where

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

@@ -16,40 +16,22 @@ import Prelude.Kore
 import Control.Error
     ( runMaybeT
     )
-import Control.Monad.State.Strict
-    ( StateT
-    , evalStateT
-    )
-import qualified Control.Monad.State.Strict as State
 import Data.Bifunctor
     ( bimap
     )
 import qualified Data.Foldable as Foldable
-import qualified Data.Functor.Foldable as Recursive
-import Data.HashMap.Strict
-    ( HashMap
-    )
-import qualified Data.HashMap.Strict as HashMap
 import Data.List
     ( foldl1'
-    , sortOn
     )
 import Data.Set
     ( Set
     )
 import qualified Data.Set as Set
-import Data.Traversable
-    ( for
-    )
 import Kore.Internal.MultiAnd
     ( MultiAnd
     )
 import qualified Kore.Internal.MultiAnd as MultiAnd
 
-import Changed
-import Kore.Attribute.Synthetic
-    ( synthesize
-    )
 import qualified Kore.Internal.Conditional as Conditional
 import Kore.Internal.OrPattern
     ( OrPattern
@@ -58,36 +40,19 @@ import qualified Kore.Internal.OrPattern as OrPattern
 import Kore.Internal.Pattern as Pattern
 import Kore.Internal.Predicate
     ( Predicate
-    , makePredicate
     )
 import qualified Kore.Internal.Predicate as Predicate
 import Kore.Internal.SideCondition
     ( SideCondition
     )
-import Kore.Internal.Symbol
-    ( isConstructor
-    , isFunction
-    )
 import Kore.Internal.TermLike
     ( And (..)
     , pattern And_
-    , pattern App_
-    , pattern Builtin_
-    , pattern Equals_
-    , pattern Exists_
-    , pattern Forall_
-    , pattern Inj_
-    , pattern Mu_
     , pattern Not_
-    , pattern Nu_
     , TermLike
-    , Variable (..)
     , mkAnd
-    , mkBottom
     , mkBottom_
     , mkNot
-    , mkTop
-    , termLikeSort
     )
 import qualified Kore.Internal.TermLike as TermLike
 import Kore.Step.Simplification.AndTerms
@@ -100,12 +65,7 @@ import Kore.Unification.UnifierT
     ( UnifierT (..)
     , runUnifierT
     )
-import Kore.Unparser
-    ( unparse
-    )
 import Logic
-import Pair
-import qualified Pretty
 
 {- | Simplify a conjunction of 'OrPattern'.
 
@@ -200,182 +160,22 @@ makeEvaluateNonBool notSimplifier sideCondition patterns = do
         from @_ @(Condition _) substitutions
         & Substitution.normalize sideCondition
     let substitution = Pattern.substitution normalized
-        predicates :: Changed (MultiAnd (Predicate variable))
+        predicates :: MultiAnd (Predicate variable)
         predicates =
             mconcat
                 [ MultiAnd.fromPredicate (predicate unified)
                 , MultiAnd.fromPredicate (predicate normalized)
                 , foldMap (from @(Predicate _) . predicate) patterns
                 ]
-            & simplifyConjunctionByAssumption
         term =
             applyAndIdempotenceAndFindContradictions
                 (Conditional.term unified)
-    case predicates of
-        Unchanged unchanged ->
-            Pattern.withCondition term (from substitution <> from predicate)
+    let predicate =
+            MultiAnd.toPredicate predicates
+            & Predicate.setSimplified simplified
+        simplified = foldMap Predicate.simplifiedAttribute predicates
+     in Pattern.withCondition term (from substitution <> from predicate)
             & return
-          where
-            predicate =
-                MultiAnd.toPredicate unchanged
-                & Predicate.setSimplified simplified
-            simplified = foldMap Predicate.simplifiedAttribute unchanged
-        Changed changed ->
-            Pattern.withCondition term (from substitution <> from predicate)
-            & simplifyCondition sideCondition
-          where
-            predicate = MultiAnd.toPredicate changed
-
-{- | Simplify the conjunction of 'Predicate' clauses by assuming each is true.
-
-The conjunction is simplified by the identity:
-
-@
-A ∧ P(A) = A ∧ P(⊤)
-@
-
- -}
-simplifyConjunctionByAssumption
-    :: forall variable
-    .  InternalVariable variable
-    => MultiAnd (Predicate variable)
-    -> Changed (MultiAnd (Predicate variable))
-simplifyConjunctionByAssumption (Foldable.toList -> andPredicates) =
-    fmap MultiAnd.make
-    $ flip evalStateT HashMap.empty
-    $ for (sortBySize andPredicates)
-    $ \predicate' -> do
-        let original = Predicate.unwrapPredicate predicate'
-        result <- applyAssumptions original
-        assume result
-        return result
-  where
-    -- Sorting by size ensures that every clause is considered before any clause
-    -- which could contain it, because the containing clause is necessarily
-    -- larger.
-    sortBySize :: [Predicate variable] -> [Predicate variable]
-    sortBySize = sortOn (size . from)
-
-    size :: TermLike variable -> Int
-    size =
-        Recursive.fold $ \(_ :< termLikeF) ->
-            case termLikeF of
-                TermLike.EvaluatedF evaluated -> TermLike.getEvaluated evaluated
-                TermLike.DefinedF defined -> TermLike.getDefined defined
-                _ -> 1 + Foldable.sum termLikeF
-
-    assume
-        :: Predicate variable
-        -> StateT (HashMap (TermLike variable) (TermLike variable)) Changed ()
-    assume predicate1 =
-        State.modify' (assumeEqualTerms . assumePredicate)
-      where
-        assumePredicate =
-            case termLike of
-                Not_ _ notChild ->
-                    -- Infer that the predicate is \bottom.
-                    HashMap.insert notChild (mkBottom sort)
-                _ ->
-                    -- Infer that the predicate is \top.
-                    HashMap.insert termLike (mkTop sort)
-        assumeEqualTerms =
-            case retractLocalFunction termLike of
-                Just (Pair term1 term2) -> HashMap.insert term1 term2
-                _ -> id
-
-        termLike = Predicate.unwrapPredicate predicate1
-        sort = termLikeSort termLike
-
-    applyAssumptions
-        ::  TermLike variable
-        ->  StateT (HashMap (TermLike variable) (TermLike variable)) Changed
-                (Predicate variable)
-    applyAssumptions replaceIn = do
-        assumptions <- State.get
-        lift $ fmap
-            (unsafeMakePredicate assumptions replaceIn)
-            (applyAssumptionsWorker assumptions replaceIn)
-
-    unsafeMakePredicate replacements original result =
-        case makePredicate result of
-            -- TODO (ttuegel): https://github.com/kframework/kore/issues/1442
-            -- should make it impossible to have an error here.
-            Left err ->
-                (error . show . Pretty.vsep . map (either id (Pretty.indent 4)))
-                [ Left "Replacing"
-                , Right (Pretty.vsep (unparse <$> HashMap.keys replacements))
-                , Left "in"
-                , Right (unparse original)
-                , Right (Pretty.pretty err)
-                ]
-            Right p -> p
-
-    applyAssumptionsWorker
-        :: HashMap (TermLike variable) (TermLike variable)
-        -> TermLike variable
-        -> Changed (TermLike variable)
-    applyAssumptionsWorker assumptions original
-      | Just result <- HashMap.lookup original assumptions = Changed result
-
-      | HashMap.null assumptions' = Unchanged original
-
-      | otherwise =
-        traverse (applyAssumptionsWorker assumptions') replaceIn
-        & getChanged
-        -- The next line ensures that if the result is Unchanged, any allocation
-        -- performed while computing that result is collected.
-        & maybe (Unchanged original) (Changed . synthesize)
-
-      where
-        _ :< replaceIn = Recursive.project original
-
-        assumptions'
-          | Exists_ _ var _ <- original = restrictAssumptions (inject var)
-          | Forall_ _ var _ <- original = restrictAssumptions (inject var)
-          | Mu_       var _ <- original = restrictAssumptions (inject var)
-          | Nu_       var _ <- original = restrictAssumptions (inject var)
-          | otherwise = assumptions
-
-        restrictAssumptions Variable { variableName } =
-            HashMap.filterWithKey
-                (\termLike _ -> wouldNotCapture termLike)
-                assumptions
-          where
-            wouldNotCapture = not . TermLike.hasFreeVariable variableName
-
-{- | Get a local function definition from a 'TermLike'.
-
-A local function definition is a predicate that we can use to evaluate a
-function locally (based on the side conditions) when none of the functions
-global definitions (axioms) apply. We are looking for a 'TermLike' of the form
-
-@
-\equals(f(...), C(...))
-@
-
-where @f@ is a function and @C@ is a constructor, sort injection or builtin.
-@retractLocalFunction@ will match an @\equals@ predicate with its arguments
-in either order, but the function pattern is always returned first in the
-'Pair'.
-
- -}
-retractLocalFunction
-    :: TermLike variable
-    -> Maybe (Pair (TermLike variable))
-retractLocalFunction =
-    \case
-        Equals_ _ _ term1 term2 -> go term1 term2 <|> go term2 term1
-        _ -> Nothing
-  where
-    go term1@(App_ symbol1 _) term2
-      | isFunction symbol1 =
-        case term2 of
-            App_ symbol2 _
-              | isConstructor symbol2 -> Just (Pair term1 term2)
-            Inj_ _     -> Just (Pair term1 term2)
-            Builtin_ _ -> Just (Pair term1 term2)
-            _          -> Nothing
-    go _ _ = Nothing
 
 applyAndIdempotenceAndFindContradictions
     :: InternalVariable variable