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.

diff --git a/src/expr/node_algorithm.cpp b/src/expr/node_algorithm.cpp
index 9619e69d1fbd765e0d5222e1ef95fcce10479d3d..595adda55c21edc0fbdfd8b185862160345af1aa 100644 (file)
--- 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 929e1c5ef2c12c7ec8b9a84646f3debea92f0d9f..e47029284b99f427c5beaf8e6d392a6159f21d84 100644 (file)
--- a/src/expr/node_algorithm.h
+++ b/src/expr/node_algorithm.h
@@ -44,6 +44,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

diff --git a/src/theory/arith/nl_model.cpp b/src/theory/arith/nl_model.cpp
index 929eb4acc71c7ba05e012bf518069b9f53cabde2..3c1d5f1e97592e88e5fbc737713eb0b30dcea750 100644 (file)
--- 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 354f6f71c7ef35146bcbfbdbc0aa61a4092abe73..a8746ca2e6b827c284e9cb029c12e7b85ba2e654 100644 (file)
--- 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 bcf7cae141541f4db9f4bcc633ccda1bf3969240..94c92513157fe793158c0b1a8ff16e5d82fc5a0a 100644 (file)
--- 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);
   }
 }