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.

diff --git a/src/theory/arith/nl/cad/cdcac.cpp b/src/theory/arith/nl/cad/cdcac.cpp
index e17e946cdd2926dc8354752d07d797362f729daa..d076438f59f1995f534ebd3758ae86fb60818ca3 100644 (file)
--- 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 1b01d0bf67deb77d0aa0508c7b3c24b53603476b..f9294fdf18e1082cabbc5e8e5a22c2f1350f77da 100644 (file)
--- 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.
@@ -163,6 +163,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.