Finer-grained inference of substitutions in incremental mode (#2403)

2 files changed, 52 insertions, 3 deletions

diff --git a/src/expr/node_algorithm.cpp b/src/expr/node_algorithm.cpp
index 5443a3a2a..9240e4a8e 100644
--- a/src/expr/node_algorithm.cpp
+++ b/src/expr/node_algorithm.cpp
@@ -166,5 +166,41 @@ bool hasFreeVar(TNode n)
   return false;
 }
 
+void getSymbols(TNode n, std::unordered_set<Node, NodeHashFunction>& syms)
+{
+  std::unordered_set<TNode, TNodeHashFunction> visited;
+  getSymbols(n, syms);
+}
+
+void getSymbols(TNode n,
+                std::unordered_set<Node, NodeHashFunction>& syms,
+                std::unordered_set<TNode, TNodeHashFunction>& visited)
+{
+  std::vector<TNode> visit;
+  TNode cur;
+  visit.push_back(n);
+  do
+  {
+    cur = visit.back();
+    visit.pop_back();
+    if (visited.find(cur) == visited.end())
+    {
+      visited.insert(cur);
+      if (cur.isVar() && cur.getKind() != kind::BOUND_VARIABLE)
+      {
+        syms.insert(cur);
+      }
+      if (cur.hasOperator())
+      {
+        visit.push_back(cur.getOperator());
+      }
+      for (TNode cn : cur)
+      {
+        visit.push_back(cn);
+      }
+    }
+  } while (!visit.empty());
+}
+
 }  // namespace expr
 }  // namespace CVC4
diff --git a/src/expr/node_algorithm.h b/src/expr/node_algorithm.h
index 61e81c4c2..7453bc292 100644
--- a/src/expr/node_algorithm.h
+++ b/src/expr/node_algorithm.h
@@ -39,20 +39,33 @@ namespace expr {
 bool hasSubterm(TNode n, TNode t, bool strict = false);
 
 /**
- * Returns true iff the node n contains a bound variable. This bound
- * variable may or may not be free.
+ * 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
  * @return true iff this node contains a bound variable
  */
 bool hasBoundVar(TNode n);
 
 /**
- * Returns true iff the node n contains a free variable.
+ * Returns true iff the node n contains a free variable, that is, a node
+ * of kind BOUND_VARIABLE that is not bound in n.
  * @param n The node under investigation
  * @return true iff this node contains a free variable.
  */
 bool hasFreeVar(TNode n);
 
+/**
+ * For term n, this function collects the symbols that occur as a subterms
+ * of n. A symbol is a variable that does not have kind BOUND_VARIABLE.
+ * @param n The node under investigation
+ * @param syms The set which the symbols of n are added to
+ */
+void getSymbols(TNode n, std::unordered_set<Node, NodeHashFunction>& syms);
+/** Same as above, with a visited cache */
+void getSymbols(TNode n,
+                std::unordered_set<Node, NodeHashFunction>& syms,
+                std::unordered_set<TNode, TNodeHashFunction>& visited);
+
 }  // namespace expr
 }  // namespace CVC4