From 3d44636a3080831bd8ea4c6b2d4f60adf6b37e9d Mon Sep 17 00:00:00 2001 From: Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com> Date: Fri, 19 Jun 2020 21:10:06 -0500 Subject: [PATCH] Add Match utility function. (#4632) --- src/expr/node_algorithm.cpp | 87 +++++++++++++++++++++++++++ src/expr/node_algorithm.h | 31 ++++++++-- test/unit/expr/node_algorithm_black.h | 64 ++++++++++++++++++++ 3 files changed, 178 insertions(+), 4 deletions(-) diff --git a/src/expr/node_algorithm.cpp b/src/expr/node_algorithm.cpp index 4d9788a27..52c5165a6 100644 --- a/src/expr/node_algorithm.cpp +++ b/src/expr/node_algorithm.cpp @@ -634,5 +634,92 @@ void getComponentTypes( } while (!toProcess.empty()); } +bool match(Node x, + Node y, + std::unordered_map& subs) +{ + std::unordered_set, TNodePairHashFunction> visited; + std::unordered_set, TNodePairHashFunction>::iterator + it; + std::unordered_map::iterator subsIt; + + std::vector> stack; + stack.emplace_back(x, y); + std::pair curr; + + while (!stack.empty()) + { + curr = stack.back(); + stack.pop_back(); + if (curr.first == curr.second) + { + // holds trivially + continue; + } + it = visited.find(curr); + if (it != visited.end()) + { + // already processed + continue; + } + visited.insert(curr); + if (curr.first.getNumChildren() == 0) + { + if (!curr.first.getType().isComparableTo(curr.second.getType())) + { + // the two subterms have different types + return false; + } + // if the two subterms are not equal and the first one is a bound + // variable... + if (curr.first.getKind() == kind::BOUND_VARIABLE) + { + // and we have not seen this variable before... + subsIt = subs.find(curr.first); + if (subsIt == subs.cend()) + { + // add the two subterms to `sub` + subs.emplace(curr.first, curr.second); + } + else + { + // if we saw this variable before, make sure that (now and before) it + // maps to the same subterm + if (curr.second != subsIt->second) + { + return false; + } + } + } + else + { + // the two subterms are not equal + return false; + } + } + else + { + // if the two subterms are not equal, make sure that their operators are + // equal + // we compare operators instead of kinds because different terms may have + // the same kind (both `(id x)` and `(square x)` have kind APPLY_UF) + // since many builtin operators like `PLUS` allow arbitrary number of + // arguments, we also need to check if the two subterms have the same + // number of children + if (curr.first.getNumChildren() != curr.second.getNumChildren() + || curr.first.getOperator() != curr.second.getOperator()) + { + return false; + } + // recurse on children + for (size_t i = 0, n = curr.first.getNumChildren(); i < n; ++i) + { + stack.emplace_back(curr.first[i], curr.second[i]); + } + } + } + return true; +} + } // namespace expr } // namespace CVC4 diff --git a/src/expr/node_algorithm.h b/src/expr/node_algorithm.h index b0edd08fa..4fb40c739 100644 --- a/src/expr/node_algorithm.h +++ b/src/expr/node_algorithm.h @@ -157,7 +157,7 @@ void getOperatorsMap( /* * Substitution of Nodes in a capture avoiding way. - * If x occurs free in n and it is substituted by a term t + * If x occurs free in n and it is substituted by a term t * and t includes some variable y that is bound in n, * then using alpha conversion y is replaced with a fresh bound variable * before the substitution. @@ -166,9 +166,9 @@ void getOperatorsMap( Node substituteCaptureAvoiding(TNode n, Node src, Node dest); /** - * Same as substituteCaptureAvoiding above, but with a - * simultaneous substitution of a vector of variables. - * Elements in source will be replaced by their corresponding element in dest. + * Same as substituteCaptureAvoiding above, but with a + * simultaneous substitution of a vector of variables. + * Elements in source will be replaced by their corresponding element in dest. * Both vectors should have the same size. */ Node substituteCaptureAvoiding(TNode n, @@ -185,6 +185,29 @@ Node substituteCaptureAvoiding(TNode n, void getComponentTypes( TypeNode t, std::unordered_set& types); +/** match + * + * Given two terms `n1` and `n2` containing free variables, match returns true + * if `n2` is an instance of `n1`. In which case, `subs` is a mapping from the + * free variables in `n1` to corresponding terms in `n2` such that: + * + * n1 * subs = n2 (where * denotes application of substitution). + * + * For example, given: + * n1 = (+ a (* x 2)) (x denotes a free variable) + * n2 = (+ a (* b 2)) + * a call to match should return `true` with subs = {(x, b)} + * + * @param n1 the term (containing free vars) to compare an instance term + * against + * @param n2 the instance term in question + * @param subs the mapping from free vars in `n1` to terms in `n2` + * @return whether or not `n2` is an instance of `n1` + */ +bool match(Node n1, + Node n2, + std::unordered_map& subs); + } // namespace expr } // namespace CVC4 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 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); + } }; -- 2.30.2