(cad solver) Add a partial check method. (#4904)

This PR extends the CAD-based solver to enable partial checks. Essentially, we only collect the first interval that is excluded for the first variable and return that one as a lemma. This does not leave a lot of choice on "how partial" the check should be, but it is fairly easy to implement and does not add additional overhead.
It also fixes some confusion in excluding_interval_to_lemma...

1 files changed, 43 insertions, 0 deletions

diff --git a/src/theory/arith/nl/cad_solver.cpp b/src/theory/arith/nl/cad_solver.cpp
index a2fc1e1f1..bb1ef9911 100644
--- a/src/theory/arith/nl/cad_solver.cpp
+++ b/src/theory/arith/nl/cad_solver.cpp
@@ -106,6 +106,49 @@ std::vector<NlLemma> CadSolver::checkFull()
 #endif
 }
 
+std::vector<NlLemma> CadSolver::checkPartial()
+{
+#ifdef CVC4_POLY_IMP
+  std::vector<NlLemma> lems;
+  auto covering = d_CAC.getUnsatCover(0, true);
+  if (covering.empty())
+  {
+    d_foundSatisfiability = true;
+    Trace("nl-cad") << "SAT: " << d_CAC.getModel() << std::endl;
+  }
+  else
+  {
+    auto* nm = NodeManager::currentNM();
+    Node first_var =
+        d_CAC.getConstraints().varMapper()(d_CAC.getVariableOrdering()[0]);
+    for (const auto& interval : covering)
+    {
+      Node premise;
+      Assert(!interval.d_origins.empty());
+      if (interval.d_origins.size() == 1)
+      {
+        premise = interval.d_origins[0];
+      }
+      else
+      {
+        premise = nm->mkNode(Kind::AND, interval.d_origins);
+      }
+      Node conclusion =
+          excluding_interval_to_lemma(first_var, interval.d_interval);
+      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, Inference::CAD_EXCLUDED_INTERVAL);
+    }
+  }
+  return lems;
+#else
+  Warning() << "Tried to use CadSolver but libpoly is not available. Compile "
+               "with --poly."
+            << std::endl;
+  return {};
+#endif
+}
+
 bool CadSolver::constructModelIfAvailable(std::vector<Node>& assertions)
 {
 #ifdef CVC4_POLY_IMP