Use arith::InferenceManager for CAD lemmas (#5015)

This makes the CAD solver use the new arith::InferenceManager instead of the previously used lemma collection scheme.

3 files changed, 28 insertions, 36 deletions

diff --git a/src/theory/arith/nl/cad_solver.cpp b/src/theory/arith/nl/cad_solver.cpp
index 473e067b7..416de1c5a 100644
--- a/src/theory/arith/nl/cad_solver.cpp
+++ b/src/theory/arith/nl/cad_solver.cpp
@@ -28,8 +28,8 @@ namespace theory {
 namespace arith {
 namespace nl {
 
-CadSolver::CadSolver(TheoryArith& containing, NlModel& model)
-    : d_foundSatisfiability(false), d_containing(containing), d_model(model)
+CadSolver::CadSolver(InferenceManager& im, NlModel& model)
+    : d_foundSatisfiability(false), d_im(im), d_model(model)
 {
   d_ranVariable =
       NodeManager::currentNM()->mkSkolem("__z",
@@ -66,10 +66,9 @@ void CadSolver::initLastCall(const std::vector<Node>& assertions)
 #endif
 }
 
-std::vector<NlLemma> CadSolver::checkFull()
+void CadSolver::checkFull()
 {
 #ifdef CVC4_POLY_IMP
-  std::vector<NlLemma> lems;
   auto covering = d_CAC.getUnsatCover();
   if (covering.empty())
   {
@@ -81,23 +80,11 @@ std::vector<NlLemma> CadSolver::checkFull()
     d_foundSatisfiability = false;
     auto mis = collectConstraints(covering);
     Trace("nl-cad") << "Collected MIS: " << mis << std::endl;
-    auto* nm = NodeManager::currentNM();
-    for (auto& n : mis)
-    {
-      n = n.negate();
-    }
     Assert(!mis.empty()) << "Infeasible subset can not be empty";
-    if (mis.size() == 1)
-    {
-      lems.emplace_back(mis.front(), InferenceId::NL_CAD_CONFLICT);
-    }
-    else
-    {
-      lems.emplace_back(nm->mkNode(Kind::OR, mis), InferenceId::NL_CAD_CONFLICT);
-    }
-    Trace("nl-cad") << "UNSAT with MIS: " << lems.back().d_node << std::endl;
+    Trace("nl-cad") << "UNSAT with MIS: " << mis << std::endl;
+    d_im.addConflict(NodeManager::currentNM()->mkAnd(mis),
+                     InferenceId::NL_CAD_CONFLICT);
   }
-  return lems;
 #else
   Warning() << "Tried to use CadSolver but libpoly is not available. Compile "
                "with --poly."
@@ -106,10 +93,9 @@ std::vector<NlLemma> CadSolver::checkFull()
 #endif
 }
 
-std::vector<NlLemma> CadSolver::checkPartial()
+void CadSolver::checkPartial()
 {
 #ifdef CVC4_POLY_IMP
-  std::vector<NlLemma> lems;
   auto covering = d_CAC.getUnsatCover(0, true);
   if (covering.empty())
   {
@@ -135,14 +121,16 @@ std::vector<NlLemma> CadSolver::checkPartial()
       }
       Node conclusion =
           excluding_interval_to_lemma(first_var, interval.d_interval, false);
-      if (!conclusion.isNull()) {
+      if (!conclusion.isNull())
+      {
         Node lemma = nm->mkNode(Kind::IMPLIES, premise, conclusion);
-        Trace("nl-cad") << "Excluding " << first_var << " -> " << interval.d_interval << " using " << lemma << std::endl;
-        lems.emplace_back(lemma, InferenceId::NL_CAD_EXCLUDED_INTERVAL);
-       }
+        Trace("nl-cad") << "Excluding " << first_var << " -> "
+                        << interval.d_interval << " using " << lemma
+                        << std::endl;
+        d_im.addPendingArithLemma(lemma, InferenceId::NL_CAD_EXCLUDED_INTERVAL);
+      }
     }
   }
-  return lems;
 #else
   Warning() << "Tried to use CadSolver but libpoly is not available. Compile "
                "with --poly."
diff --git a/src/theory/arith/nl/cad_solver.h b/src/theory/arith/nl/cad_solver.h
index 6f6c0d43c..615cdb03a 100644
--- a/src/theory/arith/nl/cad_solver.h
+++ b/src/theory/arith/nl/cad_solver.h
@@ -18,9 +18,9 @@
 #include <vector>
 
 #include "expr/node.h"
+#include "theory/arith/inference_manager.h"
 #include "theory/arith/nl/cad/cdcac.h"
 #include "theory/arith/nl/nl_model.h"
-#include "theory/arith/theory_arith.h"
 
 namespace CVC4 {
 namespace theory {
@@ -34,7 +34,7 @@ namespace nl {
 class CadSolver
 {
  public:
-  CadSolver(TheoryArith& containing, NlModel& model);
+  CadSolver(InferenceManager& im, NlModel& model);
   ~CadSolver();
 
   /**
@@ -52,7 +52,7 @@ class CadSolver
    * for construct_model_if_available. Otherwise, the single lemma can be used
    * as an infeasible subset.
    */
-  std::vector<NlLemma> checkFull();
+  void checkFull();
 
   /**
    * Perform a partial check, returning either {} or a list of lemmas.
@@ -60,7 +60,7 @@ class CadSolver
    * for construct_model_if_available. Otherwise, the lemmas exclude some part
    * of the search space.
    */
-  std::vector<NlLemma> checkPartial();
+  void checkPartial();
 
   /**
    * If a model is available (indicated by the last call to check_full() or
@@ -88,8 +88,8 @@ class CadSolver
    */
   bool d_foundSatisfiability;
 
-  /** The theory of arithmetic containing this extension.*/
-  TheoryArith& d_containing;
+  /** The inference manager we are pushing conflicts and lemmas to. */
+  InferenceManager& d_im;
   /** Reference to the non-linear model object */
   NlModel& d_model;
 }; /* class CadSolver */
diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp
index 537dd604c..3bf547ceb 100644
--- a/src/theory/arith/nl/nonlinear_extension.cpp
+++ b/src/theory/arith/nl/nonlinear_extension.cpp
@@ -46,7 +46,7 @@ NonlinearExtension::NonlinearExtension(TheoryArith& containing,
       d_model(containing.getSatContext()),
       d_trSlv(d_model),
       d_nlSlv(containing, d_model),
-      d_cadSlv(containing, d_model),
+      d_cadSlv(d_im, d_model),
       d_iandSlv(containing, d_model),
       d_builtModel(containing.getSatContext(), false)
 {
@@ -557,12 +557,16 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
   }
   if (options::nlCad())
   {
-    lemmas = d_cadSlv.checkFull();
-    if (lemmas.empty())
+    d_cadSlv.checkFull();
+    if (!d_im.hasUsed())
     {
       Trace("nl-cad") << "nl-cad found SAT!" << std::endl;
     }
-    filterLemmas(lemmas, wlems);
+    else
+    {
+      // checkFull() only adds a single conflict
+      return 1;
+    }
   }
   // run the full refinement in the IAND solver
   lemmas = d_iandSlv.checkFullRefine();