diff options
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/arith/arith_static_learner.cpp | 12 | ||||
-rw-r--r-- | src/theory/arith/arith_static_learner.h | 8 | ||||
-rw-r--r-- | src/theory/arith/theory_arith.cpp | 2 | ||||
-rw-r--r-- | src/theory/arith/theory_arith.h | 3 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 6 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays.h | 6 | ||||
-rw-r--r-- | src/theory/booleans/circuit_propagator.h | 2 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.h | 4 | ||||
-rw-r--r-- | src/theory/shared_terms_database.h | 2 | ||||
-rw-r--r-- | src/theory/theory_engine.h | 2 |
10 files changed, 24 insertions, 23 deletions
diff --git a/src/theory/arith/arith_static_learner.cpp b/src/theory/arith/arith_static_learner.cpp index 5b8d3befc..9ae7cd1c2 100644 --- a/src/theory/arith/arith_static_learner.cpp +++ b/src/theory/arith/arith_static_learner.cpp @@ -145,8 +145,8 @@ void ArithStaticLearner::process(TNode n, NodeBuilder<>& learned, const TNodeSet break; case CONST_RATIONAL: // Mark constants as minmax - d_minMap[n] = n.getConst<Rational>(); - d_maxMap[n] = n.getConst<Rational>(); + d_minMap.insert(n, n.getConst<Rational>()); + d_maxMap.insert(n, n.getConst<Rational>()); break; case OR: { // Look for things like "x = 0 OR x = 1" (that are defTrue) and @@ -248,7 +248,7 @@ void ArithStaticLearner::iteConstant(TNode n, NodeBuilder<>& learned){ DeltaRational min = std::min(first, second); CDNodeToMinMaxMap::const_iterator minFind = d_minMap.find(n); if (minFind == d_minMap.end() || (*minFind).second < min) { - d_minMap[n] = min; + d_minMap.insert(n, min); Node nGeqMin; if (min.getInfinitesimalPart() == 0) { nGeqMin = NodeBuilder<2>(kind::GEQ) << n << mkRationalNode(min.getNoninfinitesimalPart()); @@ -267,7 +267,7 @@ void ArithStaticLearner::iteConstant(TNode n, NodeBuilder<>& learned){ DeltaRational max = std::max(first, second); CDNodeToMinMaxMap::const_iterator maxFind = d_maxMap.find(n); if (maxFind == d_maxMap.end() || (*maxFind).second > max) { - d_maxMap[n] = max; + d_maxMap.insert(n, max); Node nLeqMax; if (max.getInfinitesimalPart() == 0) { nLeqMax = NodeBuilder<2>(kind::LEQ) << n << mkRationalNode(max.getNoninfinitesimalPart()); @@ -398,7 +398,7 @@ void ArithStaticLearner::addBound(TNode n) { /* fall through */ case kind::LEQ: if (maxFind == d_maxMap.end() || (*maxFind).second > bound) { - d_maxMap[n[0]] = bound; + d_maxMap.insert(n[0], bound); Debug("arith::static") << "adding bound " << n << endl; } break; @@ -407,7 +407,7 @@ void ArithStaticLearner::addBound(TNode n) { /* fall through */ case kind::GEQ: if (minFind == d_minMap.end() || (*minFind).second < bound) { - d_minMap[n[0]] = bound; + d_minMap.insert(n[0], bound); Debug("arith::static") << "adding bound " << n << endl; } break; diff --git a/src/theory/arith/arith_static_learner.h b/src/theory/arith/arith_static_learner.h index b047018e8..0de28c5ab 100644 --- a/src/theory/arith/arith_static_learner.h +++ b/src/theory/arith/arith_static_learner.h @@ -27,7 +27,7 @@ #include "context/context.h" #include "context/cdlist.h" -#include "context/cdhashmap.h" +#include "context/cdtrail_hashmap.h" #include <set> namespace CVC4 { @@ -41,8 +41,7 @@ private: * (=> _ (= x c)) * where c is a constant. */ - //typedef __gnu_cxx::hash_map<Node, std::set<Node>, NodeHashFunction> VarToNodeSetMap; - typedef context::CDHashMap<Node, Node, NodeHashFunction> CDNodeToNodeListMap; + typedef context::CDTrailHashMap<Node, Node, NodeHashFunction> CDNodeToNodeListMap; // The domain is an implicit list OR(x, OR(y, ..., FALSE )) // or FALSE CDNodeToNodeListMap d_miplibTrick; @@ -50,8 +49,7 @@ private: /** * Map from a node to it's minimum and maximum. */ - //typedef __gnu_cxx::hash_map<Node, DeltaRational, NodeHashFunction> NodeToMinMaxMap; - typedef context::CDHashMap<Node, DeltaRational, NodeHashFunction> CDNodeToMinMaxMap; + typedef context::CDTrailHashMap<Node, DeltaRational, NodeHashFunction> CDNodeToMinMaxMap; CDNodeToMinMaxMap d_minMap; CDNodeToMinMaxMap d_maxMap; diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 6ec6c7090..d2814348a 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -1369,7 +1369,7 @@ Constraint TheoryArith::constraintFromFactQueue(){ if(assertion != reAssertion){ Debug("arith::nf") << "getting non-nf assertion " << assertion << " |-> " << reAssertion << endl; Assert(constraint != NullConstraint); - d_assertionsThatDoNotMatchTheirLiterals[assertion] = constraint; + d_assertionsThatDoNotMatchTheirLiterals.insert(assertion, constraint); } } diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index 6a83c501b..b791186cf 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -22,6 +22,7 @@ #include "context/context.h" #include "context/cdlist.h" #include "context/cdhashset.h" +#include "context/cdinsert_hashmap.h" #include "context/cdqueue.h" #include "expr/node.h" @@ -135,7 +136,7 @@ private: * A superset of all of the assertions that currently are not the literal for * their constraint do not match constraint literals. Not just the witnesses. */ - context::CDHashMap<TNode, Constraint, TNodeHashFunction> d_assertionsThatDoNotMatchTheirLiterals; + context::CDInsertHashMap<Node, Constraint, NodeHashFunction> d_assertionsThatDoNotMatchTheirLiterals; /** * (For the moment) the type hierarchy goes as: diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index a05d30517..aabd3a62d 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -537,7 +537,7 @@ EqualityStatus TheoryArrays::getEqualityStatus(TNode a, TNode b) { void TheoryArrays::computeCareGraph() { if (d_sharedArrays.size() > 0) { - context::CDHashSet<TNode, TNodeHashFunction>::iterator it1 = d_sharedArrays.begin(), it2, iend = d_sharedArrays.end(); + CDNodeSet::key_iterator it1 = d_sharedArrays.key_begin(), it2, iend = d_sharedArrays.key_end(); for (; it1 != iend; ++it1) { for (it2 = it1, ++it2; it2 != iend; ++it2) { if ((*it1).getType() != (*it2).getType()) { @@ -1261,7 +1261,7 @@ void TheoryArrays::checkRowLemmas(TNode a, TNode b) void TheoryArrays::queueRowLemma(RowLemmaType lem) { - if (d_conflict || d_RowAlreadyAdded.count(lem) != 0) { + if (d_conflict || d_RowAlreadyAdded.contains(lem)) { return; } TNode a = lem.first; @@ -1407,7 +1407,7 @@ void TheoryArrays::dischargeLemmas() for (unsigned count = 0; count < sz; ++count) { RowLemmaType l = d_RowQueue.front(); d_RowQueue.pop(); - if (d_RowAlreadyAdded.count(l) != 0) { + if (d_RowAlreadyAdded.contains(l)) { continue; } diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index 240cfad9a..172482e71 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -333,8 +333,10 @@ class TheoryArrays : public Theory { context::CDQueue<RowLemmaType> d_RowQueue; context::CDHashSet<RowLemmaType, RowLemmaTypeHashFunction > d_RowAlreadyAdded; - context::CDHashSet<TNode, TNodeHashFunction> d_sharedArrays; - context::CDHashSet<TNode, TNodeHashFunction> d_sharedOther; + typedef context::CDHashSet<Node, NodeHashFunction> CDNodeSet; + + CDNodeSet d_sharedArrays; + CDNodeSet d_sharedOther; context::CDO<bool> d_sharedTerms; context::CDList<TNode> d_reads; std::hash_map<TNode, Node, TNodeHashFunction> d_diseqCache; diff --git a/src/theory/booleans/circuit_propagator.h b/src/theory/booleans/circuit_propagator.h index e62f9b7a1..aec0cff58 100644 --- a/src/theory/booleans/circuit_propagator.h +++ b/src/theory/booleans/circuit_propagator.h @@ -118,7 +118,7 @@ private: /** Nodes that have been attached already (computed forward edges for) */ // All the nodes we've visited so far - context::CDHashSet<TNode, TNodeHashFunction> d_seen; + context::CDHashSet<Node, NodeHashFunction> d_seen; /** * Assignment status of each node. diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index 0c8df3fca..e38f3568c 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -40,8 +40,8 @@ class TheoryBV : public Theory { context::Context* d_context; /** Context dependent set of atoms we already propagated */ - context::CDHashSet<TNode, TNodeHashFunction> d_alreadyPropagatedSet; - context::CDHashSet<TNode, TNodeHashFunction> d_sharedTermsSet; + context::CDHashSet<Node, NodeHashFunction> d_alreadyPropagatedSet; + context::CDHashSet<Node, NodeHashFunction> d_sharedTermsSet; BitblastSolver d_bitblastSolver; EqualitySolver d_equalitySolver; diff --git a/src/theory/shared_terms_database.h b/src/theory/shared_terms_database.h index 655918986..c7036a9ad 100644 --- a/src/theory/shared_terms_database.h +++ b/src/theory/shared_terms_database.h @@ -66,7 +66,7 @@ private: AlreadyNotifiedMap d_alreadyNotifiedMap; /** The registered equalities for propagation */ - typedef context::CDHashSet<TNode, TNodeHashFunction> RegisteredEqualitiesSet; + typedef context::CDHashSet<Node, NodeHashFunction> RegisteredEqualitiesSet; RegisteredEqualitiesSet d_registeredEqualities; private: diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 063943056..27371eac3 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -190,7 +190,7 @@ class TheoryEngine { * context-dependent set of those theory-propagable literals that * have been propagated. */ - context::CDHashSet<TNode, TNodeHashFunction> d_hasPropagated; + context::CDHashSet<Node, NodeHashFunction> d_hasPropagated; /** * Statistics for a particular theory. |