adding match for And (#2435)

* adding match for And

* Format with stylish-haskell

* trigger build

* adding unit tests

* fix merge

* moving matchAnd after matchEqualHeads

Co-authored-by: emarzion <[email protected]>
Co-authored-by: Octavian Mircea Sebe <[email protected]>

Author: emarzion

kore/src/Kore/Step/Axiom/Matcher.hs

@@ -176,6 +176,7 @@ matchOne
 matchOne pair =
     (   matchVariable    pair
     <|> matchEqualHeads  pair
+    <|> matchAnd         pair
     <|> matchExists      pair
     <|> matchForall      pair
     <|> matchApplication pair
@@ -443,6 +444,15 @@ matchDefined (Pair term1 term2)
   | Defined_ def2 <- term2 = push (Pair term1 def2)
   | otherwise = empty
 
+matchAnd
+    :: (MatchingVariable variable, MonadSimplify simplifier)
+    => Pair (TermLike variable)
+    -> MaybeT (MatcherT variable simplifier) ()
+matchAnd (Pair term1 term2)
+    | And_ _ conj1 conj2 <- term1 =
+        push (Pair conj1 term2) >> push (Pair conj2 term2)
+    | otherwise = empty
+
 -- * Implementation
 
 type MatchingVariable variable = InternalVariable variable

kore/test/Test/Kore/Step/Axiom/Matcher.hs

@@ -15,6 +15,7 @@ module Test.Kore.Step.Axiom.Matcher
     , test_matching_Exists
     , test_matching_Forall
     , test_matching_Equals
+    , test_matching_And
     , test_matcherOverloading
     , match
     , MatchResult
@@ -778,6 +779,32 @@ test_matching_Pair =
         [(inject xInt, mkElemVar zInt), (inject yInt, mkElemVar zInt)]
     ]
 
+test_matching_And :: [TestTree]
+test_matching_And =
+    [ matches        "and(x, x) matches x"
+        (mkAnd (mkElemVar xInt) (mkElemVar xInt))
+        (mkElemVar xInt)
+        []
+    , matches        "and(x, y) matches y"
+        (mkAnd (mkElemVar xInt) (mkElemVar yInt))
+        (mkElemVar yInt)
+        [(inject xInt, mkElemVar yInt)]
+    , matches        "and(y, x) matches y"
+        (mkAnd (mkElemVar yInt) (mkElemVar xInt))
+        (mkElemVar yInt)
+        [(inject xInt, mkElemVar yInt)]
+    , matches        "and(x, y) matches z"
+        (mkAnd (mkElemVar xInt) (mkElemVar yInt))
+        (mkElemVar zInt)
+        [(inject xInt, mkElemVar zInt), (inject yInt, mkElemVar zInt)]
+    , doesn'tMatch   "and(x, 1) does not match 2"
+        (mkAnd (mkElemVar xInt) (mkInt 1))
+        (mkInt 2)
+    , doesn'tMatch   "and(1, x) does not match 2"
+        (mkAnd (mkInt 1) (mkElemVar xInt))
+        (mkInt 2)
+    ]
+
 mkPair
     :: TermLike RewritingVariableName
     -> TermLike RewritingVariableName