From 0d0c1cdbce4fb46ad5c7d4bc620b712ea014722e Mon Sep 17 00:00:00 2001
From: Gereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Date: Fri, 4 Sep 2020 16:59:49 +0200
Subject: 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.
---
 src/theory/arith/nl/cad_solver.cpp | 40 +++++++++++++-------------------------
 1 file changed, 14 insertions(+), 26 deletions(-)

(limited to 'src/theory/arith/nl/cad_solver.cpp')

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."
-- 
cgit v1.2.3