(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...

diff --git a/src/theory/arith/nl/cad/cdcac.cpp b/src/theory/arith/nl/cad/cdcac.cpp
index 9c58a0007c1066913f84a5dab40f1bdc7551cdad..0dcf7f7a7bf3f6dccc622d1b54b630a6a528e334 100644 (file)
--- a/src/theory/arith/nl/cad/cdcac.cpp
+++ b/src/theory/arith/nl/cad/cdcac.cpp
@@ -344,15 +344,16 @@ CACInterval CDCAC::intervalFromCharacterization(
   }
 }
 
-std::vector<CACInterval> CDCAC::getUnsatCover(std::size_t cur_variable)
+std::vector<CACInterval> CDCAC::getUnsatCover(std::size_t curVariable,
+                                              bool returnFirstInterval)
 {
   Trace("cdcac") << "Looking for unsat cover for "
-                 << d_variableOrdering[cur_variable] << std::endl;
-  std::vector<CACInterval> intervals = getUnsatIntervals(cur_variable);
+                 << d_variableOrdering[curVariable] << std::endl;
+  std::vector<CACInterval> intervals = getUnsatIntervals(curVariable);
 
   if (Trace.isOn("cdcac"))
   {
-    Trace("cdcac") << "Unsat intervals for " << d_variableOrdering[cur_variable]
+    Trace("cdcac") << "Unsat intervals for " << d_variableOrdering[curVariable]
                    << ":" << std::endl;
     for (const auto& i : intervals)
     {
@@ -362,30 +363,30 @@ std::vector<CACInterval> CDCAC::getUnsatCover(std::size_t cur_variable)
   }
   poly::Value sample;
 
-  while (sampleOutsideWithInitial(intervals, sample, cur_variable))
+  while (sampleOutsideWithInitial(intervals, sample, curVariable))
   {
-    if (!checkIntegrality(cur_variable, sample))
+    if (!checkIntegrality(curVariable, sample))
     {
       // the variable is integral, but the sample is not.
       Trace("cdcac") << "Used " << sample << " for integer variable "
-                     << d_variableOrdering[cur_variable] << std::endl;
-      auto new_interval = buildIntegralityInterval(cur_variable, sample);
-      Trace("cdcac") << "Adding integrality interval "
-                     << new_interval.d_interval << std::endl;
-      intervals.emplace_back(new_interval);
+                     << d_variableOrdering[curVariable] << std::endl;
+      auto newInterval = buildIntegralityInterval(curVariable, sample);
+      Trace("cdcac") << "Adding integrality interval " << newInterval.d_interval
+                     << std::endl;
+      intervals.emplace_back(newInterval);
       cleanIntervals(intervals);
       continue;
     }
-    d_assignment.set(d_variableOrdering[cur_variable], sample);
+    d_assignment.set(d_variableOrdering[curVariable], sample);
     Trace("cdcac") << "Sample: " << d_assignment << std::endl;
-    if (cur_variable == d_variableOrdering.size() - 1)
+    if (curVariable == d_variableOrdering.size() - 1)
     {
       // We have a full assignment. SAT!
       Trace("cdcac") << "Found full assignment: " << d_assignment << std::endl;
       return {};
     }
     // Recurse to next variable
-    auto cov = getUnsatCover(cur_variable + 1);
+    auto cov = getUnsatCover(curVariable + 1);
     if (cov.empty())
     {
       // Found SAT!
@@ -396,12 +397,17 @@ std::vector<CACInterval> CDCAC::getUnsatCover(std::size_t cur_variable)
     auto characterization = constructCharacterization(cov);
     Trace("cdcac") << "Characterization: " << characterization << std::endl;
 
-    d_assignment.unset(d_variableOrdering[cur_variable]);
+    d_assignment.unset(d_variableOrdering[curVariable]);
+
+    auto newInterval =
+        intervalFromCharacterization(characterization, curVariable, sample);
+    newInterval.d_origins = collectConstraints(cov);
+    intervals.emplace_back(newInterval);
 
-    auto new_interval =
-        intervalFromCharacterization(characterization, cur_variable, sample);
-    new_interval.d_origins = collectConstraints(cov);
-    intervals.emplace_back(new_interval);
+    if (returnFirstInterval)
+    {
+      return intervals;
+    }
 
     Trace("cdcac") << "Added " << intervals.back().d_interval << std::endl;
     Trace("cdcac") << "\tlower:   " << intervals.back().d_lowerPolys
@@ -421,7 +427,7 @@ std::vector<CACInterval> CDCAC::getUnsatCover(std::size_t cur_variable)
   if (Trace.isOn("cdcac"))
   {
     Trace("cdcac") << "Returning intervals for "
-                   << d_variableOrdering[cur_variable] << ":" << std::endl;
+                   << d_variableOrdering[curVariable] << ":" << std::endl;
     for (const auto& i : intervals)
     {
       Trace("cdcac") << "-> " << i.d_interval << std::endl;

diff --git a/src/theory/arith/nl/cad/cdcac.h b/src/theory/arith/nl/cad/cdcac.h
index 3434b23e6e8c9865ae89db6a3ad0647b67ba4287..a6049ad618da27c1a8dcd99a64d60248ce847f0c 100644 (file)
--- a/src/theory/arith/nl/cad/cdcac.h
+++ b/src/theory/arith/nl/cad/cdcac.h
@@ -131,8 +131,15 @@ class CDCAC
    * be obtained from d_assignment. If the covering is not empty, the result is
    * UNSAT and an infeasible subset can be extracted from the returned covering.
    * Implements Algorithm 2.
+   * @param curVariable The id of the variable (within d_variableOrdering) to
+   * be considered. This argument is used to manage the recursion internally and
+   * should always be zero if called externally.
+   * @param returnFirstInterval If true, the function returns after the first
+   * interval obtained from a recursive call. The result is not (necessarily) an
+   * unsat cover, but merely a list of infeasible intervals.
    */
-  std::vector<CACInterval> getUnsatCover(std::size_t cur_variable = 0);
+  std::vector<CACInterval> getUnsatCover(std::size_t curVariable = 0,
+                                         bool returnFirstInterval = false);
 
  private:
   /**

diff --git a/src/theory/arith/nl/cad_solver.cpp b/src/theory/arith/nl/cad_solver.cpp
index a2fc1e1f1721c55d5c97197c4cf29736d6c74605..bb1ef9911969f3a45f8cba5c0a320a818b701d98 100644 (file)
--- 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

diff --git a/src/theory/arith/nl/cad_solver.h b/src/theory/arith/nl/cad_solver.h
index 9fb243897fd9a05022138bdb11b31878a7e695e1..6f6c0d43cedd306320d1e16b1dfead4f91b0080e 100644 (file)
--- a/src/theory/arith/nl/cad_solver.h
+++ b/src/theory/arith/nl/cad_solver.h
@@ -54,6 +54,14 @@ class CadSolver
    */
   std::vector<NlLemma> checkFull();
 
+  /**
+   * Perform a partial check, returning either {} or a list of lemmas.
+   * If the result is empty, the input is satisfiable and a model is available
+   * for construct_model_if_available. Otherwise, the lemmas exclude some part
+   * of the search space.
+   */
+  std::vector<NlLemma> checkPartial();
+
   /**
    * If a model is available (indicated by the last call to check_full() or
    * check_partial()) this method puts a satisfying assignment in d_model,

diff --git a/src/theory/arith/nl/poly_conversion.cpp b/src/theory/arith/nl/poly_conversion.cpp
index 8345fc5a115f0481270a471517e58e670e81cc95..e3bf4712d473430a689bb33f7a5175625a849d4b 100644 (file)
--- a/src/theory/arith/nl/poly_conversion.cpp
+++ b/src/theory/arith/nl/poly_conversion.cpp
@@ -360,17 +360,18 @@ Node excluding_interval_to_lemma(const Node& variable,
     if (is_algebraic_number(lv))
     {
       return nm->mkNode(
-          Kind::AND,
+          Kind::OR,
           nm->mkNode(
-              Kind::GT, variable, nm->mkConst(poly_utils::toRationalBelow(lv))),
-          nm->mkNode(Kind::LT,
+              Kind::LT, variable, nm->mkConst(poly_utils::toRationalBelow(lv))),
+          nm->mkNode(Kind::GT,
                      variable,
                      nm->mkConst(poly_utils::toRationalAbove(lv))));
     }
     else
     {
-      return nm->mkNode(
-          Kind::EQUAL, variable, nm->mkConst(poly_utils::toRationalBelow(lv)));
+      return nm->mkNode(Kind::DISTINCT,
+                        variable,
+                        nm->mkConst(poly_utils::toRationalBelow(lv)));
     }
   }
   if (li)
@@ -384,7 +385,7 @@ Node excluding_interval_to_lemma(const Node& variable,
         Kind::LT, variable, nm->mkConst(poly_utils::toRationalBelow(lv)));
   }
   return nm->mkNode(
-      Kind::AND,
+      Kind::OR,
       nm->mkNode(
           Kind::GT, variable, nm->mkConst(poly_utils::toRationalAbove(uv))),
       nm->mkNode(