(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, 8 insertions, 1 deletions

diff --git a/src/theory/arith/nl/cad/cdcac.h b/src/theory/arith/nl/cad/cdcac.h
index 3434b23e6..a6049ad61 100644
--- 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:
   /**