Update to standard implementation of contains term (#3270)

2 files changed, 80 insertions, 6 deletions

diff --git a/src/expr/node_algorithm.cpp b/src/expr/node_algorithm.cpp
index 50ac8297c..59e3d3b03 100644
--- a/src/expr/node_algorithm.cpp
+++ b/src/expr/node_algorithm.cpp
@@ -34,16 +34,26 @@ bool hasSubterm(TNode n, TNode t, bool strict)
 
   toProcess.push_back(n);
 
+  // incrementally iterate and add to toProcess
   for (unsigned i = 0; i < toProcess.size(); ++i)
   {
     TNode current = toProcess[i];
-    if (current.hasOperator() && current.getOperator() == t)
+    for (unsigned j = 0, j_end = current.getNumChildren(); j <= j_end; ++j)
     {
-      return true;
-    }
-    for (unsigned j = 0, j_end = current.getNumChildren(); j < j_end; ++j)
-    {
-      TNode child = current[j];
+      TNode child;
+      // try children then operator
+      if (j < j_end)
+      {
+        child = current[j];
+      }
+      else if (current.hasOperator())
+      {
+        child = current.getOperator();
+      }
+      else
+      {
+        break;
+      }
       if (child == t)
       {
         return true;
@@ -118,6 +128,61 @@ bool hasSubtermMulti(TNode n, TNode t)
   return false;
 }
 
+bool hasSubterm(TNode n, const std::vector<Node>& t, bool strict)
+{
+  if (t.empty())
+  {
+    return false;
+  }
+  if (!strict && std::find(t.begin(), t.end(), n) != t.end())
+  {
+    return true;
+  }
+
+  std::unordered_set<TNode, TNodeHashFunction> visited;
+  std::vector<TNode> toProcess;
+
+  toProcess.push_back(n);
+
+  // incrementally iterate and add to toProcess
+  for (unsigned i = 0; i < toProcess.size(); ++i)
+  {
+    TNode current = toProcess[i];
+    for (unsigned j = 0, j_end = current.getNumChildren(); j <= j_end; ++j)
+    {
+      TNode child;
+      // try children then operator
+      if (j < j_end)
+      {
+        child = current[j];
+      }
+      else if (current.hasOperator())
+      {
+        child = current.getOperator();
+      }
+      else
+      {
+        break;
+      }
+      if (std::find(t.begin(), t.end(), child) != t.end())
+      {
+        return true;
+      }
+      if (visited.find(child) != visited.end())
+      {
+        continue;
+      }
+      else
+      {
+        visited.insert(child);
+        toProcess.push_back(child);
+      }
+    }
+  }
+
+  return false;
+}
+
 struct HasBoundVarTag
 {
 };
diff --git a/src/expr/node_algorithm.h b/src/expr/node_algorithm.h
index 17d7d951b..e5a21d565 100644
--- a/src/expr/node_algorithm.h
+++ b/src/expr/node_algorithm.h
@@ -45,6 +45,15 @@ bool hasSubterm(TNode n, TNode t, bool strict = false);
 bool hasSubtermMulti(TNode n, TNode t);
 
 /**
+ * Check if the node n has a subterm that occurs in t.
+ * @param n The node to search in
+ * @param t The set of subterms to search for
+ * @param strict If true, a term is not considered to be a subterm of itself
+ * @return true iff there is a term in t that is a subterm in n
+ */
+bool hasSubterm(TNode n, const std::vector<Node>& t, bool strict = false);
+
+/**
  * Returns true iff the node n contains a bound variable, that is a node of
  * kind BOUND_VARIABLE. This bound variable may or may not be free.
  * @param n The node under investigation