diff options
Diffstat (limited to 'src/theory/arith/arith_static_learner.cpp')
| -rw-r--r-- | src/theory/arith/arith_static_learner.cpp | 36 |
1 files changed, 17 insertions, 19 deletions
diff --git a/src/theory/arith/arith_static_learner.cpp b/src/theory/arith/arith_static_learner.cpp index e17605ead..810eded82 100644 --- a/src/theory/arith/arith_static_learner.cpp +++ b/src/theory/arith/arith_static_learner.cpp @@ -252,25 +252,23 @@ void ArithStaticLearner::addBound(TNode n) { DeltaRational bound = constant; switch(Kind k = n.getKind()) { - case kind::LT: - bound = DeltaRational(constant, -1); - /* fall through */ - case kind::LEQ: - if (maxFind == d_maxMap.end() || (*maxFind).second > bound) { - d_maxMap.insert(n[0], bound); - Debug("arith::static") << "adding bound " << n << endl; - } - break; - case kind::GT: - bound = DeltaRational(constant, 1); - /* fall through */ - case kind::GEQ: - if (minFind == d_minMap.end() || (*minFind).second < bound) { - d_minMap.insert(n[0], bound); - Debug("arith::static") << "adding bound " << n << endl; - } - break; - default: Unhandled() << k; break; + case kind::LT: bound = DeltaRational(constant, -1); CVC4_FALLTHROUGH; + case kind::LEQ: + if (maxFind == d_maxMap.end() || (*maxFind).second > bound) + { + d_maxMap.insert(n[0], bound); + Debug("arith::static") << "adding bound " << n << endl; + } + break; + case kind::GT: bound = DeltaRational(constant, 1); CVC4_FALLTHROUGH; + case kind::GEQ: + if (minFind == d_minMap.end() || (*minFind).second < bound) + { + d_minMap.insert(n[0], bound); + Debug("arith::static") << "adding bound " << n << endl; + } + break; + default: Unhandled() << k; break; } } |