diff options
| author | Tim King <taking@cs.nyu.edu> | 2010-06-22 17:25:14 +0000 |
|---|---|---|
| committer | Tim King <taking@cs.nyu.edu> | 2010-06-22 17:25:14 +0000 |
| commit | 452cf36c789006db5e1202cf06fdc9dbd158f775 (patch) | |
| tree | b158c250c88cb292b4b7525de37b579ae3123226 /src/theory | |
| parent | 498bb02fc7d2539d41b778bc42e383ca8dbf6d9e (diff) | |
Made ~Stat() virtual. Added some additional statistics. And added some documentation.
Diffstat (limited to 'src/theory')
| -rw-r--r-- | src/theory/arith/theory_arith.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index c16d8f183..b3b7f58be 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -267,10 +267,10 @@ bool TheoryArith::AssertUpper(TNode n, TNode original){ Debug("arith") << "AssertUpper(" << x_i << " " << c_i << ")"<< std::endl; - if(d_partialModel.aboveUpperBound(x_i, c_i, false) ){ + if(d_partialModel.aboveUpperBound(x_i, c_i, false) ){ // \upperbound(x_i) <= c_i return false; //sat } - if(d_partialModel.belowLowerBound(x_i, c_i, true)){ + if(d_partialModel.belowLowerBound(x_i, c_i, true)){// \lowerbound(x_i) > c_i Node lbc = d_partialModel.getLowerConstraint(x_i); Node conflict = NodeManager::currentNM()->mkNode(AND, lbc, original); Debug("arith") << "AssertUpper conflict " << conflict << endl; |