Infrastructure for tautological literals in nonlinear solver (#3795)

Work towards CVC4/cvc4-projects#113 and #3783.

This PR adds the ability to mark certain literals as being tautological, since they can be assumed to hold in all models. This is important for internally generated literals whose purpose is to guide models generated by the linear solver but should not hinder our ability to answer "sat".

This PR is required for further refactoring of check-model for transcendental functions.

2 files changed, 33 insertions, 0 deletions

diff --git a/src/expr/node_algorithm.cpp b/src/expr/node_algorithm.cpp
index 9619e69d1..595adda55 100644
--- a/src/expr/node_algorithm.cpp
+++ b/src/expr/node_algorithm.cpp
@@ -129,6 +129,32 @@ bool hasSubtermMulti(TNode n, TNode t)
   return false;
 }
 
+bool hasSubtermKind(Kind k, Node n)
+{
+  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.getKind() == k)
+      {
+        return true;
+      }
+      for (const Node& cn : cur)
+      {
+        visit.push_back(cn);
+      }
+    }
+  } while (!visit.empty());
+  return false;
+}
+
 bool hasSubterm(TNode n, const std::vector<Node>& t, bool strict)
 {
   if (t.empty())
diff --git a/src/expr/node_algorithm.h b/src/expr/node_algorithm.h
index 929e1c5ef..e47029284 100644
--- a/src/expr/node_algorithm.h
+++ b/src/expr/node_algorithm.h
@@ -45,6 +45,13 @@ bool hasSubterm(TNode n, TNode t, bool strict = false);
 bool hasSubtermMulti(TNode n, TNode t);
 
 /**
+ * @param k The kind of node to check
+ * @param n The node to search in.
+ * @return true iff there is a term in n that has kind k
+ */
+bool hasSubtermKind(Kind k, Node n);
+
+/**
  * 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