diff options
Diffstat (limited to 'src/theory/arith')
-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 |
4 files changed, 12 insertions, 13 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: |