diff options
author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2021-02-22 15:44:44 +0100 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-02-22 15:44:44 +0100 |
commit | c0fa8343a5055b0923a97356f8179a9d81a3acd1 (patch) | |
tree | ec09ded333c005dce47e5dd4b855ccd38a8cae67 | |
parent | 0fc7cca0af4885b9636b9bc8c3b4773cbd2b929f (diff) |
add pruneRedundantIntervals (#5950)
Adds a simple helper for CAD to prune redundant intervals. It is just a wrapper for cleanIntervals right now, but will be responsible to making sure the CAD proof is pruned as well.
-rw-r--r-- | src/theory/arith/nl/cad/cdcac.cpp | 14 | ||||
-rw-r--r-- | src/theory/arith/nl/cad/cdcac.h | 9 |
2 files changed, 17 insertions, 6 deletions
diff --git a/src/theory/arith/nl/cad/cdcac.cpp b/src/theory/arith/nl/cad/cdcac.cpp index e17e946cd..d076438f5 100644 --- a/src/theory/arith/nl/cad/cdcac.cpp +++ b/src/theory/arith/nl/cad/cdcac.cpp @@ -93,8 +93,7 @@ const std::vector<poly::Variable>& CDCAC::getVariableOrdering() const return d_variableOrdering; } -std::vector<CACInterval> CDCAC::getUnsatIntervals( - std::size_t cur_variable) const +std::vector<CACInterval> CDCAC::getUnsatIntervals(std::size_t cur_variable) { std::vector<CACInterval> res; for (const auto& c : d_constraints.getConstraints()) @@ -123,7 +122,7 @@ std::vector<CACInterval> CDCAC::getUnsatIntervals( res.emplace_back(CACInterval{i, l, u, m, d, {n}}); } } - cleanIntervals(res); + pruneRedundantIntervals(res); return res; } @@ -363,7 +362,7 @@ std::vector<CACInterval> CDCAC::getUnsatCover(std::size_t curVariable, Trace("cdcac") << "Adding integrality interval " << newInterval.d_interval << std::endl; intervals.emplace_back(newInterval); - cleanIntervals(intervals); + pruneRedundantIntervals(intervals); continue; } d_assignment.set(d_variableOrdering[curVariable], sample); @@ -410,7 +409,7 @@ std::vector<CACInterval> CDCAC::getUnsatCover(std::size_t curVariable, Trace("cdcac") << "\torigins: " << intervals.back().d_origins << std::endl; // Remove redundant intervals - cleanIntervals(intervals); + pruneRedundantIntervals(intervals); } if (Trace.isOn("cdcac")) @@ -469,6 +468,11 @@ bool CDCAC::hasRootBelow(const poly::Polynomial& p, }); } +void CDCAC::pruneRedundantIntervals(std::vector<CACInterval>& intervals) +{ + cleanIntervals(intervals); +} + } // 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 1b01d0bf6..f9294fdf1 100644 --- a/src/theory/arith/nl/cad/cdcac.h +++ b/src/theory/arith/nl/cad/cdcac.h @@ -87,7 +87,7 @@ class CDCAC * Combines unsatisfiable regions from d_constraints evaluated over * d_assignment. Implements Algorithm 2. */ - std::vector<CACInterval> getUnsatIntervals(std::size_t cur_variable) const; + std::vector<CACInterval> getUnsatIntervals(std::size_t cur_variable); /** * Sample outside of the set of intervals. @@ -164,6 +164,13 @@ class CDCAC bool hasRootBelow(const poly::Polynomial& p, const poly::Value& val) const; /** + * Sort intervals according to section 4.4.1. and removes fully redundant + * intervals as in 4.5. 1. by calling out to cleanIntervals. + * Additionally makes sure to prune proofs for removed intervals. + */ + void pruneRedundantIntervals(std::vector<CACInterval>& intervals); + + /** * The current assignment. When the method terminates with SAT, it contains a * model for the input constraints. */ |