Add naive support for integer variables. (#4835)

This PR adds naive support for integer reasoning to the CAD-based solver.
Essentially, it checks whether the sampled value is integral. If this is not the case, we "invent" a new interval covering the area between the two neighbouring integers with appropriate border polynomials.

diff --git a/src/theory/arith/nl/cad/cdcac.cpp b/src/theory/arith/nl/cad/cdcac.cpp
index dbdae3e0b5e53f8cde3491743de682ad66ba23ac..907f7a7b68852c214e47c162d84dbac115bffbce 100644 (file)
--- a/src/theory/arith/nl/cad/cdcac.cpp
+++ b/src/theory/arith/nl/cad/cdcac.cpp
@@ -327,6 +327,18 @@ std::vector<CACInterval> CDCAC::getUnsatCover(std::size_t cur_variable)
 
   while (sampleOutside(intervals, sample))
   {
+    if (!checkIntegrality(cur_variable, 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);
+      cleanIntervals(intervals);
+      continue;
+    }
     d_assignment.set(d_variableOrdering[cur_variable], sample);
     Trace("cdcac") << "Sample: " << d_assignment << std::endl;
     if (cur_variable == d_variableOrdering.size() - 1)
@@ -381,6 +393,32 @@ std::vector<CACInterval> CDCAC::getUnsatCover(std::size_t cur_variable)
   return intervals;
 }
 
+bool CDCAC::checkIntegrality(std::size_t cur_variable, const poly::Value& value)
+{
+  Node var = d_constraints.varMapper()(d_variableOrdering[cur_variable]);
+  if (var.getType() != NodeManager::currentNM()->integerType())
+  {
+    // variable is not integral
+    return true;
+  }
+  return poly::represents_integer(value);
+}
+
+CACInterval CDCAC::buildIntegralityInterval(std::size_t cur_variable,
+                                            const poly::Value& value)
+{
+  poly::Variable var = d_variableOrdering[cur_variable];
+  poly::Integer below = poly::floor(value);
+  poly::Integer above = poly::ceil(value);
+  // construct var \in (below, above)
+  return CACInterval{poly::Interval(below, above),
+                     {var - below},
+                     {var - above},
+                     {var - below, var - above},
+                     {},
+                     {}};
+}
+
 }  // namespace cad
 }  // namespace nl
 }  // namespace arith

diff --git a/src/theory/arith/nl/cad/cdcac.h b/src/theory/arith/nl/cad/cdcac.h
index 3ea281cec50f0c71c7440001fdcdba5c818704b9..17fef608f8b44482099286e39fc84a0694fdef33 100644 (file)
--- a/src/theory/arith/nl/cad/cdcac.h
+++ b/src/theory/arith/nl/cad/cdcac.h
@@ -117,6 +117,19 @@ class CDCAC
   std::vector<CACInterval> getUnsatCover(std::size_t cur_variable = 0);
 
  private:
+  /**
+   * Check whether the current sample satisfies the integrality condition of the
+   * current variable. Returns true if the variable is not integral or the
+   * sample is integral.
+   */
+  bool checkIntegrality(std::size_t cur_variable, const poly::Value& value);
+  /**
+   * Constructs an interval that excludes the non-integral region around the
+   * current sample. Assumes !check_integrality(cur_variable, value).
+   */
+  CACInterval buildIntegralityInterval(std::size_t cur_variable,
+                                       const poly::Value& value);
+
   /**
    * The current assignment. When the method terminates with SAT, it contains a
    * model for the input constraints.