diff options
author | Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com> | 2020-06-19 21:10:06 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-06-19 21:10:06 -0500 |
commit | 3d44636a3080831bd8ea4c6b2d4f60adf6b37e9d (patch) | |
tree | e690b3b98e5eb5e7464c526b1e834d9988f59e53 /test | |
parent | 15e7da5ae8752621a128c05ef189893bad91dd88 (diff) |
Add Match utility function. (#4632)
Diffstat (limited to 'test')
-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); + } }; |