5 files changed, 39 insertions, 14 deletions
diff --git a/configure.ac b/configure.ac
index deee4fa68..ca868c0d0 100644
--- a/configure.ac
+++ b/configure.ac
@@ -751,6 +751,21 @@ void foo(int64_t) {}])],
 AC_LANG_POP([C++])
 AC_SUBST([CVC4_NEED_INT64_T_OVERLOADS])
 
+AC_MSG_CHECKING([for the pb_ds namespace])
+AC_LANG_PUSH([C++])
+AC_COMPILE_IFELSE([AC_LANG_SOURCE([
+#include <ext/pb_ds/priority_queue.hpp>
+typedef pb_ds::priority_queue<void, void, void> pq;])],
+  [CVC4_PB_DS_NAMESPACE=pb_ds],
+  [AC_COMPILE_IFELSE([AC_LANG_SOURCE([
+    #include <ext/pb_ds/priority_queue.hpp>
+    typedef __gnu_pbds::priority_queue<void, void, void> pq;])],
+      [CVC4_PB_DS_NAMESPACE=__gnu_pbds],
+      [AC_MSG_ERROR([can't find required priority_queue in either __gnu_pbds or pb_ds namespace])])])
+AC_LANG_POP([C++])
+AC_DEFINE_UNQUOTED(CVC4_PB_DS_NAMESPACE, ${CVC4_PB_DS_NAMESPACE}, [The namespace for pb_ds data structures.])
+AC_MSG_RESULT([$CVC4_PB_DS_NAMESPACE])
+
 # Check for ANTLR runantlr script (defined in config/antlr.m4)
 AC_PROG_ANTLR
 
diff --git a/src/theory/arith/error_set.h b/src/theory/arith/error_set.h
index ce6412573..e616db3b9 100644
--- a/src/theory/arith/error_set.h
+++ b/src/theory/arith/error_set.h
@@ -87,10 +87,10 @@ public:
 //
 // typedef FocusSet::handle_type FocusSetHandle;
 
-typedef  __gnu_pbds::priority_queue<
+typedef CVC4_PB_DS_NAMESPACE::priority_queue<
   ArithVar,
   ComparatorPivotRule,
-  __gnu_pbds::pairing_heap_tag> FocusSet;
+  CVC4_PB_DS_NAMESPACE::pairing_heap_tag> FocusSet;
 
 typedef FocusSet::point_iterator FocusSetHandle;
 
diff --git a/src/theory/arith/fc_simplex.h b/src/theory/arith/fc_simplex.h
index 0dafa83ff..51514bcfb 100644
--- a/src/theory/arith/fc_simplex.h
+++ b/src/theory/arith/fc_simplex.h
@@ -146,9 +146,11 @@ private:
   LinearEqualityModule::UpdatePreferenceFunction selectLeavingFunction(ArithVar x){
     bool useBlands = d_leavingCountSinceImprovement.isKey(x) &&
       d_leavingCountSinceImprovement[x] >= s_maxDegeneratePivotsBeforeBlandsOnEntering;
-    return useBlands ?
-      &LinearEqualityModule::preferWitness<false>:
-      &LinearEqualityModule::preferWitness<true>;
+    if(useBlands) {
+      return &LinearEqualityModule::preferWitness<false>;
+    } else {
+      return &LinearEqualityModule::preferWitness<true>;
+    }
   }
 
   bool debugDualLike(WitnessImprovement w, std::ostream& out,
@@ -183,9 +185,12 @@ private:
   UpdateInfo selectUpdateForPrimal(ArithVar basic, bool useBlands){
     TimerStat::CodeTimer codeTimer(d_statistics.d_selectUpdateForPrimal);
 
-    LinearEqualityModule::UpdatePreferenceFunction upf = useBlands ?
-      &LinearEqualityModule::preferWitness<false>:
-      &LinearEqualityModule::preferWitness<true>;
+    LinearEqualityModule::UpdatePreferenceFunction upf;
+    if(useBlands) {
+      upf = &LinearEqualityModule::preferWitness<false>;
+    } else {
+      upf = &LinearEqualityModule::preferWitness<true>;
+    }
 
     LinearEqualityModule::VarPreferenceFunction bpf = useBlands ?
       &LinearEqualityModule::minVarOrder :
diff --git a/src/theory/arith/soi_simplex.cpp b/src/theory/arith/soi_simplex.cpp
index f19b13fa5..7255d92ef 100644
--- a/src/theory/arith/soi_simplex.cpp
+++ b/src/theory/arith/soi_simplex.cpp
@@ -674,9 +674,12 @@ WitnessImprovement SumOfInfeasibilitiesSPD::soiRound() {
   Assert(d_soiVar != ARITHVAR_SENTINEL);
 
   bool useBlands = degeneratePivotsInARow() >= s_maxDegeneratePivotsBeforeBlandsOnLeaving;
-  LinearEqualityModule::UpdatePreferenceFunction upf = useBlands ?
-    &LinearEqualityModule::preferWitness<false>:
-    &LinearEqualityModule::preferWitness<true>;
+  LinearEqualityModule::UpdatePreferenceFunction upf;
+  if(useBlands) {
+    upf = &LinearEqualityModule::preferWitness<false>;
+  } else {
+    upf = &LinearEqualityModule::preferWitness<true>;
+  }
 
   LinearEqualityModule::VarPreferenceFunction bpf = useBlands ?
     &LinearEqualityModule::minVarOrder :
diff --git a/src/theory/arith/soi_simplex.h b/src/theory/arith/soi_simplex.h
index 1a6becccb..006839a55 100644
--- a/src/theory/arith/soi_simplex.h
+++ b/src/theory/arith/soi_simplex.h
@@ -122,9 +122,11 @@ private:
   LinearEqualityModule::UpdatePreferenceFunction selectLeavingFunction(ArithVar x){
     bool useBlands = d_leavingCountSinceImprovement.isKey(x) &&
       d_leavingCountSinceImprovement[x] >= s_maxDegeneratePivotsBeforeBlandsOnEntering;
-    return useBlands ?
-      &LinearEqualityModule::preferWitness<false>:
-      &LinearEqualityModule::preferWitness<true>;
+    if(useBlands) {
+      return &LinearEqualityModule::preferWitness<false>;
+    } else {
+      return &LinearEqualityModule::preferWitness<true>;
+    }
   }
 
   bool debugSOI(WitnessImprovement w, std::ostream& out, int instance) const;