compiles with

export CXXFLAGS='-std=gnu++0x' before configure
fails all regressions in the parser

diff --git a/src/decision/relevancy.cpp b/src/decision/relevancy.cpp
index 31963eee0e98d3c0cab2079380d407a68a228c17..ecd31a4cc26b1e07247c1504ee5c3448dc78a84d 100644 (file)
--- a/src/decision/relevancy.cpp
+++ b/src/decision/relevancy.cpp
@@ -28,6 +28,11 @@
 
 // Relevancy stuff
 
+const double Relevancy::secondsPerDecision = 0.001;
+const double Relevancy::secondsPerExpense = 1e-7;
+const double Relevancy::EPS = 1e-9;
+
+
 void Relevancy::setJustified(TNode n)
 {
   Debug("decision") << " marking [" << n.getId() << "]"<< n << "as justified" << std::endl;

diff --git a/src/decision/relevancy.h b/src/decision/relevancy.h
index bfd30ddde42d48f72fadf5bd2bb04241bd763fb6..23d980a1b38a4a7c6fe89ce695a072c1538827b8 100644 (file)
--- a/src/decision/relevancy.h
+++ b/src/decision/relevancy.h
@@ -109,9 +109,10 @@ class Relevancy : public RelevancyStrategy {
   bool d_multipleBacktrace;
   //bool d_computeRelevancy;     // are we in a mode where we compute relevancy?
 
-  static const double secondsPerDecision = 0.001;
-  static const double secondsPerExpense = 1e-7;
-  static const double EPS = 1e-9;
+  static const double secondsPerDecision;
+  static const double secondsPerExpense;
+  static const double EPS;
+
   /** Maximum time this algorithm should spent as part of whole algorithm */
   double d_maxTimeAsPercentageOfTotalTime;
 

diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp
index 35184e42e08dc8b1b5693543325aef817a30dfe0..429bb560591a1cb527cbede4fcf172b56fad4528 100644 (file)
--- a/src/smt/boolean_terms.cpp
+++ b/src/smt/boolean_terms.cpp
@@ -137,7 +137,7 @@ static void collectVarsInTermContext(TNode n, std::set<TNode>& vars, std::set<TN
 Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, bool boolParent, std::map<TNode, Node>& quantBoolVars) throw() {
   Debug("boolean-terms") << "rewriteBooleanTermsRec: " << top << " - boolParent=" << boolParent << endl;
 
-  BooleanTermCache::iterator i = d_booleanTermCache.find(make_pair<Node, bool>(top, boolParent));
+  BooleanTermCache::iterator i = d_booleanTermCache.find(std::pair<Node, bool>(top, boolParent));
   if(i != d_booleanTermCache.end()) {
     return (*i).second.isNull() ? Node(top) : (*i).second;
   }

diff --git a/src/util/dense_map.h b/src/util/dense_map.h
index 222a761c3ffa216412ba6e6646b404398425c223..b7d6908119e8f23d9130015107b7686e5e809eb1 100644 (file)
--- a/src/util/dense_map.h
+++ b/src/util/dense_map.h
@@ -98,7 +98,7 @@ public:
       return false;
     }else{
       Assert(x <  allocated());
-      return d_posVector[x] != POSITION_SENTINEL;
+      return d_posVector[x] != +POSITION_SENTINEL;
     }
   }
 
@@ -160,7 +160,7 @@ public:
   void pop_back() {
     Assert(!empty());
     Key atBack = back();
-    d_posVector[atBack] = POSITION_SENTINEL;
+    d_posVector[atBack] = +POSITION_SENTINEL;
     d_image[atBack] = T();
     d_list.pop_back();
   }
@@ -195,7 +195,7 @@ public:
 
   void increaseSize(Key max){
     Assert(max >= allocated());
-    d_posVector.resize(max+1, POSITION_SENTINEL);
+    d_posVector.resize(max+1, +POSITION_SENTINEL);
     d_image.resize(max+1);
   }