From: Gereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Date: Wed, 12 Aug 2020 15:01:58 +0000 (+0200)
Subject: Add naive support for integer variables. (#4835)
X-Git-Tag: cvc5-1.0.0~3017
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3f77b4ac0d4ff8ab69e2f2932e9ced088bd339ed;p=cvc5.git

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 dbdae3e0b..907f7a7b6 100644
--- 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 3ea281cec..17fef608f 100644
--- 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.