Add Match utility function. (#4632)

1 files changed, 64 insertions, 0 deletions

diff --git a/test/unit/expr/node_algorithm_black.h b/test/unit/expr/node_algorithm_black.h
index fd36174d4..dea5b1f37 100644
--- a/test/unit/expr/node_algorithm_black.h
+++ b/test/unit/expr/node_algorithm_black.h
@@ -130,4 +130,68 @@ class NodeAlgorithmBlack : public CxxTest::TestSuite
     TS_ASSERT(result[*d_boolTypeNode].find(d_nodeManager->operatorOf(EQUAL))
               != result[*d_boolTypeNode].end());
   }
+
+  void testMatch()
+  {
+    TypeNode integer = d_nodeManager->integerType();
+
+    Node one = d_nodeManager->mkConst(Rational(1));
+    Node two = d_nodeManager->mkConst(Rational(2));
+
+    Node x = d_nodeManager->mkBoundVar(integer);
+    Node a = d_nodeManager->mkSkolem("a", integer);
+
+    Node n1 = d_nodeManager->mkNode(MULT, two, x);
+    std::unordered_map<Node, Node, NodeHashFunction> subs;
+
+    // check reflexivity
+    TS_ASSERT(match(n1, n1, subs));
+    TS_ASSERT_EQUALS(subs.size(), 0);
+
+    Node n2 = d_nodeManager->mkNode(MULT, two, a);
+    subs.clear();
+
+    // check instance
+    TS_ASSERT(match(n1, n2, subs));
+    TS_ASSERT_EQUALS(subs.size(), 1);
+    TS_ASSERT_EQUALS(subs[x], a);
+
+    // should return false for flipped arguments (match is not symmetric)
+    TS_ASSERT(!match(n2, n1, subs));
+
+    n2 = d_nodeManager->mkNode(MULT, one, a);
+
+    // should return false since n2 is not an instance of n1
+    TS_ASSERT(!match(n1, n2, subs));
+
+    n2 = d_nodeManager->mkNode(NONLINEAR_MULT, two, a);
+
+    // should return false for similar operators
+    TS_ASSERT(!match(n1, n2, subs));
+
+    n2 = d_nodeManager->mkNode(MULT, two, a, one);
+
+    // should return false for different number of arguments
+    TS_ASSERT(!match(n1, n2, subs));
+
+    n1 = x;
+    n2 = d_nodeManager->mkConst(true);
+
+    // should return false for different types
+    TS_ASSERT(!match(n1, n2, subs));
+
+    n1 = d_nodeManager->mkNode(MULT, x, x);
+    n2 = d_nodeManager->mkNode(MULT, two, a);
+
+    // should return false for contradictory substitutions
+    TS_ASSERT(!match(n1, n2, subs));
+
+    n2 = d_nodeManager->mkNode(MULT, a, a);
+    subs.clear();
+
+    // implementation: check if the cache works correctly
+    TS_ASSERT(match(n1, n2, subs));
+    TS_ASSERT_EQUALS(subs.size(), 1);
+    TS_ASSERT_EQUALS(subs[x], a);
+  }
 };