Adding reduce() to the ArithPriorityQueue. This reduces the queue from a superset of the basic variables that violate a bound to the exact set.

2 files changed, 27 insertions, 0 deletions

diff --git a/src/theory/arith/arith_priority_queue.cpp b/src/theory/arith/arith_priority_queue.cpp
index 04ca62571..52b9f4a74 100644
--- a/src/theory/arith/arith_priority_queue.cpp
+++ b/src/theory/arith/arith_priority_queue.cpp
@@ -326,3 +326,23 @@ std::ostream& CVC4::theory::arith::operator<<(std::ostream& out, ArithPriorityQu
 
   return out;
 }
+
+void  ArithPriorityQueue::reduce(){
+  vector<ArithVar> contents;
+
+  if(inCollectionMode()){
+    contents = d_candidates;
+  } else {
+    ArithVar res = ARITHVAR_SENTINEL;
+    while((res = dequeueInconsistentBasicVariable()) != ARITHVAR_SENTINEL){
+      contents.push_back(res);
+    }
+  }
+  clear();
+  for(vector<ArithVar>::const_iterator iter = contents.begin(), end = contents.end(); iter != end; ++iter){
+    ArithVar curr = *iter;
+    if(d_tableau.isBasic(curr)){
+      enqueueIfInconsistent(curr);
+    }
+  }
+}
diff --git a/src/theory/arith/arith_priority_queue.h b/src/theory/arith/arith_priority_queue.h
index fb80e599e..d1fac1e58 100644
--- a/src/theory/arith/arith_priority_queue.h
+++ b/src/theory/arith/arith_priority_queue.h
@@ -217,6 +217,13 @@ public:
   void clear();
 
 
+  /**
+   * Reduces the queue to only contain the subset that is still basic
+   * and inconsistent.
+   *Currently, O(n log n) for an easy obviously correct implementation in all modes..
+   */
+  void reduce();
+
   bool collectionModeContains(ArithVar v) const {
     Assert(inCollectionMode());
     return d_varSet.isMember(v);