Connect the relevance manager to TheoryEngine and use it in non-linear arithmetic (#4930)

This PR activates the use of the relevance manager in TheoryEngine and makes use of it (via Valuation) in the non-linear extension in arith. It removes a deprecated hack (addTautology) for doing this.

This addresses CVC4/cvc4-projects#113.

Note that the best method for relevance is interleaving, where roughly you gain on SMT-LIB:

QF_NIA: +484-53 unsat +792-440 sat
QF_NRA: +32-19 unsat +57-23 sat
However, this PR does not (yet) enable this method by default.

Note that more work is necessary to determine which lemmas require NEEDS_JUSTIFY, this PR identifies 2 cases of lemmas that need justification (skolemization and strings reductions). Regardless, the use of the relevance manager is limited to non-linear arithmetic for now, which is only able to answer "sat" when only arithmetic is present in assertions.

4 files changed, 54 insertions, 76 deletions

diff --git a/src/theory/arith/nl/nl_model.cpp b/src/theory/arith/nl/nl_model.cpp
index daa36f972..cc10d6659 100644
--- a/src/theory/arith/nl/nl_model.cpp
+++ b/src/theory/arith/nl/nl_model.cpp
@@ -16,6 +16,7 @@
 
 #include "expr/node_algorithm.h"
 #include "options/arith_options.h"
+#include "options/theory_options.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/arith/arith_utilities.h"
 #include "theory/rewriter.h"
@@ -279,11 +280,6 @@ 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;
@@ -455,52 +451,6 @@ 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<NlLemma>& lemmas)
diff --git a/src/theory/arith/nl/nl_model.h b/src/theory/arith/nl/nl_model.h
index 1e6f6c8f3..dcbd9cce7 100644
--- a/src/theory/arith/nl/nl_model.h
+++ b/src/theory/arith/nl/nl_model.h
@@ -166,22 +166,6 @@ class NlModel
   void setUsedApproximate();
   /** Did we use an approximation during this check? */
   bool usedApproximate() const;
-  /**
-   * 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
 
   /**
@@ -334,8 +318,6 @@ 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 nl
diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp
index 9dbb95d93..fb5b6eec8 100644
--- a/src/theory/arith/nl/nonlinear_extension.cpp
+++ b/src/theory/arith/nl/nonlinear_extension.cpp
@@ -38,6 +38,7 @@ NonlinearExtension::NonlinearExtension(TheoryArith& containing,
       d_containing(containing),
       d_ee(ee),
       d_needsLastCall(false),
+      d_checkCounter(0),
       d_extTheory(&containing),
       d_model(containing.getSatContext()),
       d_trSlv(d_model),
@@ -182,8 +183,6 @@ void NonlinearExtension::sendLemmas(const std::vector<NlLemma>& out)
       d_lemmas.insert(lem);
     }
     d_stats.d_inferences << nlem.d_id;
-    // also indicate this is a tautology
-    d_model.addTautology(lem);
   }
 }
 
@@ -192,6 +191,22 @@ void NonlinearExtension::processSideEffect(const NlLemma& se)
   d_trSlv.processSideEffect(se);
 }
 
+void NonlinearExtension::computeRelevantAssertions(
+    const std::vector<Node>& assertions, std::vector<Node>& keep)
+{
+  Trace("nl-ext-rlv") << "Compute relevant assertions..." << std::endl;
+  Valuation v = d_containing.getValuation();
+  for (const Node& a : assertions)
+  {
+    if (v.isRelevant(a))
+    {
+      keep.push_back(a);
+    }
+  }
+  Trace("nl-ext-rlv") << "...keep " << keep.size() << "/" << assertions.size()
+                      << " assertions" << std::endl;
+}
+
 unsigned NonlinearExtension::filterLemma(NlLemma lem, std::vector<NlLemma>& out)
 {
   Trace("nl-ext-lemma-debug")
@@ -251,6 +266,16 @@ unsigned NonlinearExtension::filterLemmas(std::vector<NlLemma>& lemmas,
 void NonlinearExtension::getAssertions(std::vector<Node>& assertions)
 {
   Trace("nl-ext") << "Getting assertions..." << std::endl;
+  bool useRelevance = false;
+  if (options::nlRlvMode() == options::NlRlvMode::INTERLEAVE)
+  {
+    useRelevance = (d_checkCounter % 2);
+  }
+  else if (options::nlRlvMode() == options::NlRlvMode::ALWAYS)
+  {
+    useRelevance = true;
+  }
+  Valuation v = d_containing.getValuation();
   NodeManager* nm = NodeManager::currentNM();
   // get the assertions
   std::map<Node, Rational> init_bounds[2];
@@ -264,6 +289,11 @@ void NonlinearExtension::getAssertions(std::vector<Node>& assertions)
     nassertions++;
     const Assertion& assertion = *it;
     Node lit = assertion.d_assertion;
+    if (useRelevance && !v.isRelevant(lit))
+    {
+      // not relevant, skip
+      continue;
+    }
     init_assertions.insert(lit);
     // check for concrete bounds
     bool pol = lit.getKind() != NOT;
@@ -390,7 +420,6 @@ std::vector<Node> NonlinearExtension::checkModelEval(
 }
 
 bool NonlinearExtension::checkModel(const std::vector<Node>& assertions,
-                                    const std::vector<Node>& false_asserts,
                                     std::vector<NlLemma>& lemmas,
                                     std::vector<Node>& gs)
 {
@@ -398,7 +427,17 @@ bool NonlinearExtension::checkModel(const std::vector<Node>& assertions,
 
   // get the presubstitution
   Trace("nl-ext-cm-debug") << "  apply pre-substitution..." << std::endl;
-  std::vector<Node> passertions = assertions;
+  std::vector<Node> passertions;
+  if (options::nlRlvMode() != options::NlRlvMode::NONE)
+  {
+    // only keep the relevant assertions (those required for showing input
+    // is satisfied)
+    computeRelevantAssertions(assertions, passertions);
+  }
+  else
+  {
+    passertions = assertions;
+  }
   if (options::nlExt())
   {
     // preprocess the assertions with the trancendental solver
@@ -681,6 +720,7 @@ void NonlinearExtension::check(Theory::Effort e)
 bool NonlinearExtension::modelBasedRefinement(std::vector<NlLemma>& mlems)
 {
   ++(d_stats.d_mbrRuns);
+  d_checkCounter++;
 
   // get the assertions
   std::vector<Node> assertions;
@@ -786,7 +826,7 @@ bool NonlinearExtension::modelBasedRefinement(std::vector<NlLemma>& mlems)
       // error bounds on the Taylor approximation of transcendental functions.
       std::vector<NlLemma> lemmas;
       std::vector<Node> gs;
-      if (checkModel(assertions, false_asserts, lemmas, gs))
+      if (checkModel(assertions, lemmas, gs))
       {
         complete_status = 1;
       }
diff --git a/src/theory/arith/nl/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h
index 6fb8dbbfa..ee58a9e2e 100644
--- a/src/theory/arith/nl/nonlinear_extension.h
+++ b/src/theory/arith/nl/nonlinear_extension.h
@@ -254,11 +254,12 @@ class NonlinearExtension
    * ensureLiteral respectively.
    */
   bool checkModel(const std::vector<Node>& assertions,
-                  const std::vector<Node>& false_asserts,
                   std::vector<NlLemma>& lemmas,
                   std::vector<Node>& gs);
   //---------------------------end check model
-
+  /** compute relevant assertions */
+  void computeRelevantAssertions(const std::vector<Node>& assertions,
+                                 std::vector<Node>& keep);
   /**
    * Potentially adds lemmas to the set out and clears lemmas. Returns
    * the number of lemmas added to out. We do not add lemmas that have already
@@ -293,6 +294,11 @@ class NonlinearExtension
   NlStats d_stats;
   // needs last call effort
   bool d_needsLastCall;
+  /**
+   * The number of times we have the called main check method
+   * (modelBasedRefinement). This counter is used for interleaving strategies.
+   */
+  unsigned d_checkCounter;
   /** Extended theory, responsible for context-dependent simplification. */
   ExtTheory d_extTheory;
   /** The non-linear model object