unifyKequalsEq should apply for both \and and \equals

* unifyKequalsEq should apply for both \and and \equals

* Tests for KEqual unification

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

Author: ana-pantilie

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

@@ -237,7 +237,7 @@ andEqualsFunctions notSimplifier =
     , (BothT,   \_ _ s -> Builtin.Bool.unifyBoolNot s)
     , (EqualsT, \_ _ s -> Builtin.Int.unifyIntEq s notSimplifier)
     , (EqualsT, \_ _ s -> Builtin.String.unifyStringEq s notSimplifier)
-    , (EqualsT, \_ _ s -> Builtin.KEqual.unifyKequalsEq s notSimplifier)
+    , (BothT,   \_ _ s -> Builtin.KEqual.unifyKequalsEq s notSimplifier)
     , (AndT,    \_ _ s -> Builtin.KEqual.unifyIfThenElse s)
     , (BothT,   \_ _ _ -> Builtin.Endianness.unifyEquals)
     , (BothT,   \_ _ _ -> Builtin.Signedness.unifyEquals)

kore/test/Test/Kore/Step/MockSymbols.hs

@@ -64,6 +64,7 @@ import Kore.Attribute.Synthetic
 import qualified Kore.Builtin.Bool as Builtin.Bool
 import qualified Kore.Builtin.Builtin as Builtin
 import qualified Kore.Builtin.Int as Builtin.Int
+import qualified Kore.Builtin.KEqual as Builtin.KEqual
 import qualified Kore.Builtin.List as List
 import qualified Kore.Builtin.Map as Map
 import qualified Kore.Builtin.Set as Set
@@ -281,6 +282,8 @@ elementSetId :: Id
 elementSetId = testId "elementSet"
 unitSetId :: Id
 unitSetId = testId "unitSet"
+keqBoolId :: Id
+keqBoolId = testId "keqBool"
 sigmaId :: Id
 sigmaId = testId "sigma"
 anywhereId :: Id
@@ -660,6 +663,11 @@ unitSetSymbol :: Symbol
 unitSetSymbol =
     symbol unitSetId [] setSort & functional & hook "SET.unit"
 
+keqBoolSymbol :: Symbol
+keqBoolSymbol =
+    symbol keqBoolId [testSort, testSort] boolSort
+    & function & functional & hook "KEQUAL.eq"
+
 opaqueSetSymbol :: Symbol
 opaqueSetSymbol =
     symbol opaqueSetId [testSort] setSort
@@ -1347,6 +1355,13 @@ unitList
     => TermLike variable
 unitList = Internal.mkApplySymbol unitListSymbol []
 
+keqBool
+    :: InternalVariable variable
+    => TermLike variable
+    -> TermLike variable
+    -> TermLike variable
+keqBool t1 t2 = Internal.mkApplySymbol keqBoolSymbol [t1, t2]
+
 sigma
     :: InternalVariable variable
     => HasCallStack
@@ -1463,6 +1478,7 @@ symbols =
     , lessIntSymbol
     , greaterEqIntSymbol
     , tdivIntSymbol
+    , keqBoolSymbol
     , sigmaSymbol
     , anywhereSymbol
     , subsubOverloadSymbol
@@ -2047,4 +2063,8 @@ builtinSimplifiers =
             , builtinEvaluation
                 (Builtin.Int.builtinFunctions Map.! Builtin.Int.geKey)
             )
+        ,   ( AxiomIdentifier.Application keqBoolId
+            , builtinEvaluation
+                (Builtin.KEqual.builtinFunctions Map.! Builtin.KEqual.eqKey)
+            )
         ]

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

@@ -1174,7 +1174,43 @@ test_andTermsSimplification =
             actual <- unify input1 input2
             assertEqual "" expect actual
         ]
+
+    , testGroup "KEquals"
+        [ testCase "Equal unification" $ do
+            let input1 = Mock.keqBool (cf xVar) a
+                input2 = Mock.builtinBool False
+                expected = [Condition.top]
+            Just actual <- simplifyEquals mempty input1 input2
+            assertEqual "" expected actual
+        , testCase "And unification" $ do
+            let input1 = Mock.keqBool (cf xVar) a
+                input2 = Mock.builtinBool False
+                expected = [Pattern.top]
+            actual <- simplify input1 input2
+            assertEqual "" expected actual
+        , testCase "And unification fails if pattern\
+                    \ is not function-like" $ do
+            let input1 = Mock.keqBool (TermLike.mkOr a (cf xVar)) b
+                input2 = Mock.builtinBool False
+                expected =
+                    TermLike.mkAnd input1 input2
+                    & Pattern.fromTermLike
+                    & pure
+            actual <- simplify input1 input2
+            assertEqual "" expected actual
+        , testCase "Equal unification fails if pattern\
+                    \ is not function-like" $ do
+            let input1 = Mock.keqBool (TermLike.mkOr a (cf xVar)) b
+                input2 = Mock.builtinBool False
+            actual <- simplifyEquals mempty input1 input2
+            assertEqual "" Nothing actual
+        ]
     ]
+  where
+    xVar = mkElemVar Mock.x
+    cf = Mock.functionalConstr10
+    a = Mock.a
+    b = Mock.b
 
 mkVariable :: Text -> Variable VariableName
 mkVariable ident =