Fixes to FCSimplex for some versions of compilers

4 files changed, 24 insertions, 14 deletions

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;