diff options
author | Tim King <taking@cs.nyu.edu> | 2012-12-05 19:06:21 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2012-12-05 19:06:21 +0000 |
commit | 7f52115ab0dcba4c8ba9403a5f25b8e8c588911a (patch) | |
tree | 14b74c89069cd6e9b443853ac1f15cca2ce586a1 /src/theory/arith/arith_static_learner.cpp | |
parent | 7efd777609f7fbc20701402ad949971cbc251f8f (diff) |
This commit merges in CDTrailHashMap and CDInsertHashMap. CDHashSet now uses CDInsertHashMap. CDHashSet<TNode> have been changed to CDHashSet<Node>. Switching CnfStream to use CDInsertSet. Switches a few CDHashMaps in arithmetic to use CDTrailHashMap. Documentation changes to CDHashMap.
Diffstat (limited to 'src/theory/arith/arith_static_learner.cpp')
-rw-r--r-- | src/theory/arith/arith_static_learner.cpp | 12 |
1 files changed, 6 insertions, 6 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; |