Add built-in rule for symbolic ==Int (#1894)

Author: andreiburdusa

kore/src/Kore/Builtin/Int.hs

@@ -64,6 +64,7 @@ import Prelude.Kore
 import Control.Error
     ( MaybeT
     )
+import qualified Control.Monad as Monad
 import Data.Bits
     ( complement
     , shift
@@ -97,6 +98,11 @@ import qualified Kore.Builtin.Builtin as Builtin
 import Kore.Builtin.Int.Int
 import qualified Kore.Domain.Builtin as Domain
 import qualified Kore.Error
+import qualified Kore.Internal.Condition as Condition
+import qualified Kore.Internal.Pattern as Pattern
+import Kore.Internal.Predicate
+    ( makeCeilPredicate
+    )
 import Kore.Internal.TermLike as TermLike
 import Kore.Step.Simplification.Simplify
     ( BuiltinAndAxiomSimplifier
@@ -252,7 +258,7 @@ builtinFunctions =
 
     , comparator gtKey (>)
     , comparator geKey (>=)
-    , comparator eqKey (==)
+    , (eqKey, Builtin.functionEvaluator evalEq)
     , comparator leKey (<=)
     , comparator ltKey (<)
     , comparator neKey (/=)
@@ -325,3 +331,32 @@ builtinFunctions =
     log2 n
         | n > 0 = Just (smallInteger (integerLog2# n))
         | otherwise = Nothing
+
+evalEq :: Builtin.Function
+evalEq resultSort arguments@[_intLeft, _intRight] =
+    concrete <|> symbolicReflexivity
+  where
+    concrete = do
+        _intLeft <- expectBuiltinInt eqKey _intLeft
+        _intRight <- expectBuiltinInt eqKey _intRight
+        _intLeft == _intRight
+            & Bool.asPattern resultSort
+            & return
+
+    symbolicReflexivity = do
+        Monad.guard (TermLike.isFunctionPattern _intLeft)
+        -- Do not need to check _intRight because we only return a result
+        -- when _intLeft and _intRight are equal.
+        if _intLeft == _intRight then
+            True & Bool.asPattern resultSort & returnPattern
+        else
+            empty
+
+    mkCeilUnlessDefined termLike
+      | TermLike.isDefinedPattern termLike = Condition.topOf resultSort
+      | otherwise =
+        Condition.fromPredicate (makeCeilPredicate resultSort termLike)
+    returnPattern = return . flip Pattern.andCondition conditions
+    conditions = foldMap mkCeilUnlessDefined arguments
+
+evalEq _ _ = Builtin.wrongArity eqKey

kore/test/Test/Kore/Builtin/Int.hs

@@ -17,6 +17,8 @@ module Test.Kore.Builtin.Int
     , test_unifyAnd_Equal
     , test_unifyAndEqual_Equal
     , test_unifyAnd_Fn
+    , test_reflexivity_symbolic
+    , test_symbolic_eq_not_conclusive
     , hprop_unparse
     --
     , asInternal
@@ -71,6 +73,7 @@ import Kore.Internal.TermLike
 import Test.Kore
     ( elementVariableGen
     , standaloneGen
+    , testId
     )
 import qualified Test.Kore.Builtin.Bool as Test.Bool
 import Test.Kore.Builtin.Builtin
@@ -444,6 +447,28 @@ test_unifyAnd_Fn =
         actual <- evaluateT $ mkAnd dv fnPat
         (===) expect actual
 
+test_reflexivity_symbolic :: TestTree
+test_reflexivity_symbolic =
+    testCaseWithSMT "evaluate symbolic reflexivity for equality" $ do
+        let x = mkElemVar $ "x" `ofSort` intSort
+            expect = Test.Bool.asPattern True
+        actual <- evaluate $ mkApplySymbol eqIntSymbol [x, x]
+        assertEqual' "" expect actual
+  where
+    ofSort :: Text.Text -> Sort -> ElementVariable VariableName
+    ofSort idName sort = mkElementVariable (testId idName) sort
+
+test_symbolic_eq_not_conclusive :: TestTree
+test_symbolic_eq_not_conclusive =
+    testCaseWithSMT "evaluate symbolic equality for different variables" $ do
+        let x = mkElemVar $ "x" `ofSort` intSort
+            y = mkElemVar $ "y" `ofSort` intSort
+            expect = fromTermLike $ mkApplySymbol eqIntSymbol [x, y]
+        actual <- evaluate $ mkApplySymbol eqIntSymbol [x, y]
+        assertEqual' "" expect actual
+  where
+    ofSort :: Text.Text -> Sort -> ElementVariable VariableName
+    ofSort idName sort = mkElementVariable (testId idName) sort
 
 hprop_unparse :: Property
 hprop_unparse = hpropUnparse (asInternal <$> genInteger)