Revert 'Eliminate top level existentials in side-condtions'

kore/src/Kore/Reachability/Claim.hs

@@ -773,7 +773,7 @@ checkSimpleImplication inLeft inRight existentials =
         rhsBottom <-
             fmap isBottom . liftSimplifier $
                 SMT.Evaluator.filterMultiOr $srcLoc
-                    =<< Pattern.simplify right
+                    =<< Exists.makeEvaluate SideCondition.top existentials right
 
         case (trivial, rhsBottom) of
             (True, _) -> pure (claimToCheck, Implied Nothing)

kore/src/Kore/Simplify/Condition.hs

@@ -16,16 +16,9 @@ import Control.Monad.State.Strict (
     StateT,
  )
 import Control.Monad.State.Strict qualified as State
-import Data.Functor.Foldable qualified as Recursive
 import Data.Generics.Product (
     field,
  )
-import Data.Set (
-    Set,
- )
-import Kore.Attribute.Pattern.FreeVariables (
-    freeVariableNames,
- )
 import Kore.Internal.Condition qualified as Condition
 import Kore.Internal.Conditional qualified as Conditional
 import Kore.Internal.MultiAnd (
@@ -60,8 +53,6 @@ import Kore.Simplify.SubstitutionSimplifier (
     SubstitutionSimplifier (..),
  )
 import Kore.Substitute
-import Kore.Syntax.Exists qualified as Exists
-import Kore.Syntax.Variable (SomeVariableName)
 import Kore.TopBottom qualified as TopBottom
 import Logic
 import Prelude.Kore
@@ -188,40 +179,15 @@ simplifyPredicates sideCondition original = do
     let predicates =
             SideCondition.simplifyConjunctionByAssumption original
                 & fst . extract
-    simplifiedPredicates <- do
-        let eliminatedExists =
-                map
-                    ( simplifyPredicateExistElim $
-                        -- TODO (sam): this is quite conservative and we may not need to
-                        -- avoid names here, but there doesn't seem to be a negative
-                        -- impact on performance, so best leave this in for now.
-                        freeVariableNames original
-                            <> freeVariableNames sideCondition
-                    )
-                    $ toList predicates
+    simplifiedPredicates <-
         simplifyPredicatesWithAssumptions
             sideCondition
-            eliminatedExists
+            (toList predicates)
     let simplified = foldMap mkCondition simplifiedPredicates
     if original == simplifiedPredicates
         then return (Condition.markSimplified simplified)
         else simplifyPredicates sideCondition simplifiedPredicates
 
-{- | Simplify an existential predicate by removing the existential binder and refreshing
-all occurrences of the name within the child term
--}
-simplifyPredicateExistElim ::
-    Set (SomeVariableName RewritingVariableName) ->
-    Predicate RewritingVariableName ->
-    Predicate RewritingVariableName
-simplifyPredicateExistElim avoid predicate = case predicateF of
-    Predicate.ExistsF existsF ->
-        let existsF'@Exists.Exists{existsChild} = Exists.refreshExists avoid existsF
-         in simplifyPredicateExistElim (avoid <> freeVariableNames existsF') existsChild
-    _ -> predicate
-  where
-    _ :< predicateF = Recursive.project predicate
-
 {- | Simplify a conjunction of predicates by simplifying each one
 under the assumption that the others are true.
 -}

kore/test/Test/Kore/Simplify/Pattern.hs

@@ -48,13 +48,16 @@ test_Pattern_simplify =
         "\\or(a, a)"
     , bottomLike `becomes` OrPattern.bottom $
         "\\and(a, \\bottom)"
-    , testCase "Removes top level exist quantifier whilst simplifying" $ do
+    , testCase "Replaces and terms under independent quantifiers" $ do
         let expect =
                 Pattern.fromTermAndPredicate
                     (Mock.constr10 fOfX)
                     ( makeAndPredicate
                         (makeCeilPredicate fOfX)
-                        (makeCeilPredicate fOfY)
+                        ( makeExistsPredicate
+                            Mock.yConfig
+                            (makeCeilPredicate fOfY)
+                        )
                     )
         actual <-
             simplify
@@ -114,7 +117,10 @@ test_Pattern_simplify =
                     (Mock.constr10 fOfX)
                     ( makeAndPredicate
                         (makeCeilPredicate fOfX)
-                        (fromCeil_ $ Mock.f (mkElemVar x'))
+                        ( makeExistsPredicate
+                            x'
+                            (fromCeil_ $ Mock.f (mkElemVar x'))
+                        )
                     )
                     & OrPattern.fromPattern
         actual <-

kore/test/Test/Kore/Unification/UnifierT.hs

@@ -60,12 +60,9 @@ test_simplifyCondition =
         actual <- normalize Condition.bottomCondition
         assertEqual "Expected empty result" expect actual
         assertNormalizedPredicatesMulti actual
-    , testCase
-        ( "∃ y z. x = σ(y, z) normalized to a substitution x = σ(y, z) "
-            <> "(top-level exists get removed, and y,z must be fresh in the context)"
-        )
-        $ do
-            assertNormalized existsSubst
+    , testCase "∃ y z. x = σ(y, z)" $ do
+        let expect = Condition.fromPredicate existsPredicate
+        assertNormalized expect
     , testCase "¬∃ y z. x = σ(y, z)" $ do
         let expect =
                 Condition.fromPredicate $
@@ -96,10 +93,6 @@ test_simplifyCondition =
         assertEqual "Expected \\top" expect actual
     ]
   where
-    existsSubst =
-        Condition.fromSubstitution $
-            Substitution.unsafeWrap
-                [(inject Mock.xConfig, (Mock.sigma (mkElemVar Mock.yConfig) (mkElemVar Mock.zConfig)))]
     existsPredicate =
         Predicate.makeMultipleExists [Mock.yConfig, Mock.zConfig] $
             Predicate.makeEqualsPredicate