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.

5 files changed, 105 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
diff --git a/src/theory/arith/nl_model.cpp b/src/theory/arith/nl_model.cpp
index 929eb4acc..3c1d5f1e9 100644
--- a/src/theory/arith/nl_model.cpp
+++ b/src/theory/arith/nl_model.cpp
@@ -278,6 +278,11 @@ bool NlModel::checkModel(const std::vector<Node>& assertions,
   std::vector<Node> check_assertions;
   for (const Node& a : assertions)
   {
+    // don't have to check tautological literals
+    if (d_tautology.find(a) != d_tautology.end())
+    {
+      continue;
+    }
     if (d_check_model_solved.find(a) == d_check_model_solved.end())
     {
       Node av = a;
@@ -424,6 +429,52 @@ void NlModel::setUsedApproximate() { d_used_approx = true; }
 
 bool NlModel::usedApproximate() const { return d_used_approx; }
 
+void NlModel::addTautology(Node n)
+{
+  // ensure rewritten
+  n = Rewriter::rewrite(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() == AND)
+      {
+        // children of AND are also implied
+        for (const Node& cn : cur)
+        {
+          visit.push_back(cn);
+        }
+      }
+      else
+      {
+        // is this an arithmetic literal?
+        Node atom = cur.getKind() == NOT ? cur[0] : cur;
+        if ((atom.getKind() == EQUAL && atom[0].getType().isReal())
+            || atom.getKind() == LEQ)
+        {
+          // Add to tautological literals if it does not contain
+          // non-linear multiplication. We cannot consider literals
+          // with non-linear multiplication to be tautological since this
+          // model object is responsible for checking whether they hold.
+          // (TODO, cvc4-projects #113: revisit this).
+          if (!expr::hasSubtermKind(NONLINEAR_MULT, atom))
+          {
+            Trace("nl-taut") << "Tautological literal: " << atom << std::endl;
+            d_tautology.insert(cur);
+          }
+        }
+      }
+    }
+  } while (!visit.empty());
+}
+
 bool NlModel::solveEqualitySimple(Node eq,
                                   unsigned d,
                                   std::vector<Node>& lemmas)
diff --git a/src/theory/arith/nl_model.h b/src/theory/arith/nl_model.h
index 354f6f71c..a8746ca2e 100644
--- a/src/theory/arith/nl_model.h
+++ b/src/theory/arith/nl_model.h
@@ -163,6 +163,23 @@ class NlModel
   void setUsedApproximate();
   /** Did we use an approximation during this check? */
   bool usedApproximate() const;
+  /** Set tautology
+   *
+   * This states that formula n is a tautology (satisfied in all models).
+   * We call this on internally generated lemmas. This method computes a
+   * set of literals that are implied by n, that are hence tautological
+   * as well, such as:
+   *   l_pi <= real.pi <= u_pi (pi approximations)
+   *   sin(x) = -1*sin(-x)
+   * where these literals are internally generated for the purposes
+   * of guiding the models of the linear solver.
+   *
+   * TODO (cvc4-projects #113: would be helpful if we could do this even
+   * more aggressively by ignoring all internally generated literals.
+   *
+   * Tautological literals do not need be checked during checkModel.
+   */
+  void addTautology(Node n);
   //------------------------------ end recording model substitutions and bounds
 
   /** print model value, for debugging.
@@ -314,6 +331,8 @@ class NlModel
   std::unordered_map<Node, Node, NodeHashFunction> d_check_model_solved;
   /** did we use an approximation on this call to last-call effort? */
   bool d_used_approx;
+  /** the set of all tautological literals */
+  std::unordered_set<Node, NodeHashFunction> d_tautology;
 }; /* class NlModel */
 
 }  // namespace arith
diff --git a/src/theory/arith/nonlinear_extension.cpp b/src/theory/arith/nonlinear_extension.cpp
index bcf7cae14..94c925131 100644
--- a/src/theory/arith/nonlinear_extension.cpp
+++ b/src/theory/arith/nonlinear_extension.cpp
@@ -559,6 +559,8 @@ void NonlinearExtension::sendLemmas(const std::vector<Node>& out,
     {
       d_lemmas.insert(lem);
     }
+    // also indicate this is a tautology
+    d_model.addTautology(lem);
   }
 }