Add Match utility function. (#4632)

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<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
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<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
 
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);
+  }
 };