projects
/
cvc5.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
| inline |
side by side
(parent:
44ee91e
)
Fix to the context dependent static learning code.
author
Tim King
<taking@cs.nyu.edu>
Mon, 5 Nov 2012 23:52:22 +0000
(23:52 +0000)
committer
Tim King
<taking@cs.nyu.edu>
Mon, 5 Nov 2012 23:52:22 +0000
(23:52 +0000)
src/theory/arith/arith_static_learner.cpp
patch
|
blob
|
history
diff --git
a/src/theory/arith/arith_static_learner.cpp
b/src/theory/arith/arith_static_learner.cpp
index af2f0c9bcc1ff3aa984d11946616451c0019f145..5b8d3befc22bead85275e64b517fd2b745531e78 100644
(file)
--- a/
src/theory/arith/arith_static_learner.cpp
+++ b/
src/theory/arith/arith_static_learner.cpp
@@
-262,8
+262,8
@@
void ArithStaticLearner::iteConstant(TNode n, NodeBuilder<>& learned){
}
if (d_maxMap.find(n[1]) != d_maxMap.end() && d_maxMap.find(n[2]) != d_maxMap.end()) {
- const DeltaRational& first = d_m
in
Map[n[1]];
- const DeltaRational& second = d_m
in
Map[n[2]];
+ const DeltaRational& first = d_m
ax
Map[n[1]];
+ const DeltaRational& second = d_m
ax
Map[n[2]];
DeltaRational max = std::max(first, second);
CDNodeToMinMaxMap::const_iterator maxFind = d_maxMap.find(n);
if (maxFind == d_maxMap.end() || (*maxFind).second > max) {