diff options
author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2020-08-12 17:01:58 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-08-12 10:01:58 -0500 |
commit | 3f77b4ac0d4ff8ab69e2f2932e9ced088bd339ed (patch) | |
tree | 2d1448d22d06afef93e3a0afb763d6ed20f14a43 | |
parent | a852ea2c368a81c37eadccc02b3d36aec1a55c12 (diff) |
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.
-rw-r--r-- | src/theory/arith/nl/cad/cdcac.cpp | 38 | ||||
-rw-r--r-- | src/theory/arith/nl/cad/cdcac.h | 13 |
2 files changed, 51 insertions, 0 deletions
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 @@ -118,6 +118,19 @@ class CDCAC 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. */ |