And simplification: substitute function applications for constructors

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

@@ -64,9 +64,15 @@ 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 Equals_
     , pattern Exists_
     , pattern Forall_
     , pattern Mu_
@@ -96,6 +102,7 @@ import Kore.Unparser
     ( unparse
     )
 import Logic
+import Pair
 import qualified Pretty
 
 {- | Simplify a conjunction of 'OrPattern'.
@@ -259,14 +266,21 @@ simplifyConjunctionByAssumption (Foldable.toList -> andPredicates) =
         :: Predicate variable
         -> StateT (HashMap (TermLike variable) (TermLike variable)) Changed ()
     assume predicate1 =
-        State.modify' insert
+        State.modify' (assumeEqualTerms . assumePredicate)
       where
-        insert =
+        assumePredicate =
             case termLike of
-                -- Infer that the predicate is \bottom.
-                Not_ _ notChild -> HashMap.insert notChild (mkBottom sort)
-                -- Infer that the predicate is \top.
-                _               -> HashMap.insert termLike (mkTop    sort)
+                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
 
@@ -327,6 +341,29 @@ simplifyConjunctionByAssumption (Foldable.toList -> andPredicates) =
           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. @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
+
 applyAndIdempotenceAndFindContradictions
     :: InternalVariable variable
     => TermLike variable

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

@@ -552,6 +552,43 @@ test_andSimplification =
                     , substitution = mempty
                     }
         assertEqual "" (MultiOr.make [expect]) actual
+    , testGroup "Local function evaluation" $
+        let f = Mock.f (mkElemVar Mock.x)
+            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 =
+                testCase name $ do
+                    let equals1 = mkLocalDefn eitherC1 & Condition.fromPredicate
+                        equals2 = mkLocalDefn 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)
+            ]
+    , 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/issue-2095/Makefile

@@ -0,0 +1,3 @@
+include $(CURDIR)/../include.mk
+
+test-%.sh.out: $(TEST_DIR)/test-%-*