Simplification.And.retractLocalFunction: cases for sort inj and builtins (#2166)

* Simplification.And.retractLocalFunction: cases for sort inj and builtins + tests

* Update golden

* Add integration test

* test_andSimplification: remove "Constructor equality" test

The "Constructor equality" test case doesn't make sense because both predicates
under the conjunction should independently be \bottom.

* retractLocalFunction: cleanup

* Revert "Add integration test"

This reverts commit f376a6f.

It's not evident that this integration test checks something useful.

Co-authored-by: Thomas Tuegel <ttuegel@mailbox.org>
Co-authored-by: Thomas Tuegel <thomas.tuegel@runtimeverification.com>

Author: ana-pantilie

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

@@ -72,9 +72,11 @@ 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_
@@ -351,18 +353,29 @@ 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. @retractLocalFunction@ will
-match an @\equals@ predicate with its arguments in either order, but the
-function pattern is always returned first in the 'Pair'.
+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 (Equals_ _ _ term1@(App_ symbol1 _) term2@(App_ symbol2 _))
-  | isConstructor symbol1, isFunction symbol2 = Just (Pair term2 term1)
-  | isConstructor symbol2, isFunction symbol1 = Just (Pair term1 term2)
-retractLocalFunction _ = Nothing
+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

kore/test/Test/Kore/Step/Simplification/And.hs

@@ -554,41 +554,41 @@ test_andSimplification =
         assertEqual "" (MultiOr.make [expect]) actual
     , testGroup "Local function evaluation" $
         let f = Mock.f (mkElemVar Mock.x)
+            fInt = Mock.fInt (mkElemVar Mock.xInt)
             defined = makeCeilPredicate_ f & Condition.fromPredicate
             a = Mock.a
             b = Mock.b
-            mkLocalDefn (Left t)  = makeEqualsPredicate_ t f
-            mkLocalDefn (Right t) = makeEqualsPredicate_ f t
-            test name eitherC1 eitherC2 =
+            injA = Mock.sortInjection10 Mock.a
+            injB = Mock.sortInjection10 Mock.b
+            int2 = Mock.builtinInt 2
+            int3 = Mock.builtinInt 3
+            mkLocalDefn func (Left t)  = makeEqualsPredicate_ t func
+            mkLocalDefn func (Right t) = makeEqualsPredicate_ func t
+            test name func eitherC1 eitherC2 =
                 testCase name $ do
-                    let equals1 = mkLocalDefn eitherC1 & Condition.fromPredicate
-                        equals2 = mkLocalDefn eitherC2 & Condition.fromPredicate
+                    let equals1 = mkLocalDefn func eitherC1 & Condition.fromPredicate
+                        equals2 = mkLocalDefn func eitherC2 & Condition.fromPredicate
                         pattern1 = Pattern.fromCondition_ (defined <> equals1)
                         pattern2 = Pattern.fromCondition_ (defined <> equals2)
                     actual <- evaluatePatterns pattern1 pattern2
                     assertBool "Expected \\bottom" $ isBottom actual
         in
-            [ test "contradiction: f(x) = a ∧ f(x) = b" (Right a) (Right b)
-            , test "contradiction: a = f(x) ∧ f(x) = b" (Left  a) (Right b)
-            , test "contradiction: a = f(x) ∧ b = f(x)" (Left  a) (Left  b)
-            , test "contradiction: f(x) = a ∧ b = f(x)" (Right a) (Left  b)
+            [ -- Constructor at top
+              test "contradiction: f(x) = a ∧ f(x) = b" f (Right a) (Right b)
+            , test "contradiction: a = f(x) ∧ f(x) = b" f (Left  a) (Right b)
+            , test "contradiction: a = f(x) ∧ b = f(x)" f (Left  a) (Left  b)
+            , test "contradiction: f(x) = a ∧ b = f(x)" f (Right a) (Left  b)
+            -- Sort injection at top
+            , test "contradiction: f(x) = injA ∧ f(x) = injB" f (Right injA) (Right injB)
+            , test "contradiction: injA = f(x) ∧ f(x) = injB" f (Left  injA) (Right injB)
+            , test "contradiction: injA = f(x) ∧ injB = f(x)" f (Left  injA) (Left  injB)
+            , test "contradiction: f(x) = injA ∧ injB = f(x)" f (Right injA) (Left  injB)
+            -- Builtin at top
+            , test "contradiction: f(x) = 2 ∧ f(x) = 3" fInt (Right int2) (Right int3)
+            , test "contradiction: 2 = f(x) ∧ f(x) = 3" fInt (Left  int2) (Right int3)
+            , test "contradiction: 2 = f(x) ∧ 3 = f(x)" fInt (Left  int2) (Left  int3)
+            , test "contradiction: f(x) = 2 ∧ 3 = f(x)" fInt (Right int2) (Left  int3)
             ]
-    , testCase "Constructor equality" $ do
-        actual <-
-            evaluatePatterns
-                (makeEqualsPredicate_
-                    Mock.c
-                    Mock.a
-                & Condition.fromPredicate
-                & Pattern.fromCondition_
-                )
-                ( makeEqualsPredicate_
-                    Mock.b
-                    Mock.c
-                & Condition.fromPredicate
-                & Pattern.fromCondition_
-                )
-        assertEqual "" (MultiOr.make []) actual
     ]
   where
     yExpanded = Conditional

test/symbolic-ensures/1.strict.out.golden

@@ -7,12 +7,6 @@
   #Equals
     true
   }
-#And
-  {
-    true
-  #Equals
-    ?X <=Int 3
-  }
 #And
   {
     true