} while (!toProcess.empty());
}
+bool match(Node x,
+ Node y,
+ std::unordered_map<Node, Node, NodeHashFunction>& subs)
+{
+ std::unordered_set<std::pair<TNode, TNode>, TNodePairHashFunction> visited;
+ std::unordered_set<std::pair<TNode, TNode>, TNodePairHashFunction>::iterator
+ it;
+ std::unordered_map<Node, Node, NodeHashFunction>::iterator subsIt;
+
+ std::vector<std::pair<TNode, TNode>> stack;
+ stack.emplace_back(x, y);
+ std::pair<TNode, TNode> 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
/*
* 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.
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,
void getComponentTypes(
TypeNode t, std::unordered_set<TypeNode, TypeNodeHashFunction>& 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<Node, Node, NodeHashFunction>& subs);
+
} // namespace expr
} // namespace CVC4
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);
+ }
};
projects / cvc5.git / commitdiff