This commit adds a priority queue implementation. This is to avoid compilation troubles with libc++.

2 files changed, 29 insertions, 24 deletions

diff --git a/src/theory/arith/error_set.cpp b/src/theory/arith/error_set.cpp
index 6d341ed12..4a63b1a6a 100644
--- a/src/theory/arith/error_set.cpp
+++ b/src/theory/arith/error_set.cpp
@@ -253,11 +253,11 @@ void ErrorSet::update(ErrorInformation& ei){
     case MINIMUM_AMOUNT:
     case MAXIMUM_AMOUNT:
       ei.setAmount(computeDiff(ei.getVariable()));
-      d_focus.modify(ei.getHandle(), ei.getVariable());
+      d_focus.update(ei.getHandle(), ei.getVariable());
       break;
     case  SUM_METRIC:
       ei.setMetric(sumMetric(ei.getVariable()));
-      d_focus.modify(ei.getHandle(), ei.getVariable());
+      d_focus.update(ei.getHandle(), ei.getVariable());
       break;
     case  VAR_ORDER:
       //do nothing
diff --git a/src/theory/arith/error_set.h b/src/theory/arith/error_set.h
index b87282ba0..cff6807c4 100644
--- a/src/theory/arith/error_set.h
+++ b/src/theory/arith/error_set.h
@@ -29,23 +29,24 @@
 #include "theory/arith/callbacks.h"
 
 #include "util/statistics_registry.h"
-
-#if CVC4_GCC_HAS_PB_DS_BUG
-   // Unfortunate bug in some older GCCs (e.g., v4.2):
-   //   http://gcc.gnu.org/bugzilla/show_bug.cgi?id=36612
-   // Requires some header-hacking to work around
-#  define __throw_container_error inline __throw_container_error
-#  define __throw_insert_error inline __throw_insert_error
-#  define __throw_join_error inline __throw_join_error
-#  define __throw_resize_error inline __throw_resize_error
-#  include <ext/pb_ds/exception.hpp>
-#  undef __throw_container_error
-#  undef __throw_insert_error
-#  undef __throw_join_error
-#  undef __throw_resize_error
-#endif /* CVC4_GCC_HAS_PB_DS_BUG */
-
-#include <ext/pb_ds/priority_queue.hpp>
+#include "util/bin_heap.h"
+
+// #if CVC4_GCC_HAS_PB_DS_BUG
+//    // Unfortunate bug in some older GCCs (e.g., v4.2):
+//    //   http://gcc.gnu.org/bugzilla/show_bug.cgi?id=36612
+//    // Requires some header-hacking to work around
+// #  define __throw_container_error inline __throw_container_error
+// #  define __throw_insert_error inline __throw_insert_error
+// #  define __throw_join_error inline __throw_join_error
+// #  define __throw_resize_error inline __throw_resize_error
+// #  include <ext/pb_ds/exception.hpp>
+// #  undef __throw_container_error
+// #  undef __throw_insert_error
+// #  undef __throw_join_error
+// #  undef __throw_resize_error
+// #endif /* CVC4_GCC_HAS_PB_DS_BUG */
+
+// #include <ext/pb_ds/priority_queue.hpp>
 
 #include <vector>
 
@@ -103,12 +104,16 @@ public:
 //
 // typedef FocusSet::handle_type FocusSetHandle;
 
-typedef CVC4_PB_DS_NAMESPACE::priority_queue<
-  ArithVar,
-  ComparatorPivotRule,
-  CVC4_PB_DS_NAMESPACE::pairing_heap_tag> FocusSet;
+// typedef CVC4_PB_DS_NAMESPACE::priority_queue<
+//   ArithVar,
+//   ComparatorPivotRule,
+//   CVC4_PB_DS_NAMESPACE::pairing_heap_tag> FocusSet;
+
+// typedef FocusSet::point_iterator FocusSetHandle;
+
+typedef BinaryHeap<ArithVar, ComparatorPivotRule> FocusSet;
+typedef FocusSet::handle FocusSetHandle;
 
-typedef FocusSet::point_iterator FocusSetHandle;
 
 class ErrorInformation {
 private: