diff options
author | Dejan Jovanović <dejan@cs.nyu.edu> | 2013-03-23 01:19:06 -0400 |
---|---|---|
committer | Dejan Jovanović <dejan@cs.nyu.edu> | 2013-03-23 01:19:06 -0400 |
commit | 75a37a134bf21e1664ade24b663a79cf1f298266 (patch) | |
tree | 008a5d5f655758b4150001b41ec5d8b55a244c70 | |
parent | f44a81d1b62058fa56af952aa92be965690481e5 (diff) | |
parent | 54b7a17226dd71f25b9f4b0f315ccdb53c1c0292 (diff) |
Merge remote-tracking branch 'dddejan/c++11'
Conflicts:
src/smt/boolean_terms.cpp
-rw-r--r-- | src/decision/relevancy.cpp | 5 | ||||
-rw-r--r-- | src/decision/relevancy.h | 7 | ||||
-rw-r--r-- | src/util/dense_map.h | 6 | ||||
-rw-r--r-- | src/util/hash.h | 2 |
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/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); } diff --git a/src/util/hash.h b/src/util/hash.h index 4d4094143..913358512 100644 --- a/src/util/hash.h +++ b/src/util/hash.h @@ -48,7 +48,7 @@ namespace CVC4 { struct StringHashFunction { size_t operator()(const std::string& str) const { - return std::hash<const char*>()(str.c_str()); + return __gnu_cxx::hash<const char*>()(str.c_str()); } };/* struct StringHashFunction */ |