diff options
author | Dejan Jovanović <dejan@cs.nyu.edu> | 2013-03-22 17:25:48 -0400 |
---|---|---|
committer | Dejan Jovanović <dejan@cs.nyu.edu> | 2013-03-22 17:25:48 -0400 |
commit | 17921b8fabea67fffd7d6a2a4b476dba06f3cb0c (patch) | |
tree | ca3bb4f24393615584ea45e84539726c610f86d1 /src | |
parent | 36816ad2537a2e6163037e9592c513b9a69aa9dc (diff) |
compiles with
export CXXFLAGS='-std=gnu++0x' before configure
fails all regressions in the parser
Diffstat (limited to 'src')
-rw-r--r-- | src/decision/relevancy.cpp | 5 | ||||
-rw-r--r-- | src/decision/relevancy.h | 7 | ||||
-rw-r--r-- | src/smt/boolean_terms.cpp | 2 | ||||
-rw-r--r-- | src/util/dense_map.h | 6 |
4 files changed, 13 insertions, 7 deletions
diff --git a/src/decision/relevancy.cpp b/src/decision/relevancy.cpp index 31963eee0..ecd31a4cc 100644 --- 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 bfd30ddde..23d980a1b 100644 --- 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 35184e42e..429bb5605 100644 --- 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 222a761c3..b7d690811 100644 --- 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); } |