diff options
Diffstat (limited to 'test/unit/expr')
-rw-r--r-- | test/unit/expr/node_algorithm_black.h | 64 |
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); + } }; |