2 files changed, 114 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