From: Tim King <taking@cs.nyu.edu>
Date: Wed, 27 Jun 2012 20:58:37 +0000 (+0000)
Subject: Adding access to simplex's ArithPriorityQueue to TheoryArith for ArithPriorityQueue... 
X-Git-Tag: cvc5-1.0.0~7958
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8eea9f5ecc02363e3a8705abe45a6be424d70c4d;p=cvc5.git

Adding access to simplex's ArithPriorityQueue to TheoryArith for ArithPriorityQueue::reduce(), ::begin() and ::end().
---

diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h
index a1c69548c..9ba44b102 100644
--- a/src/theory/arith/simplex.h
+++ b/src/theory/arith/simplex.h
@@ -230,6 +230,18 @@ public:
     return d_queue.collectionModeContains(var);
   }
 
+  void reduceQueue(){
+    d_queue.reduce();
+  }
+
+  ArithPriorityQueue::const_iterator queueBegin() const{
+    return d_queue.begin();
+  }
+
+  ArithPriorityQueue::const_iterator queueEnd() const{
+    return d_queue.end();
+  }
+
 private:
 
   /** Reports a conflict to on the output channel. */