diff options
| author | Tim King <taking@cs.nyu.edu> | 2011-12-15 22:23:25 +0000 |
|---|---|---|
| committer | Tim King <taking@cs.nyu.edu> | 2011-12-15 22:23:25 +0000 |
| commit | 9f5e56a0460c2668e8c5547d616fb34a58ff6d88 (patch) | |
| tree | 9f033c30d44c1df2ad01b5c14248b28d75a8c267 /src/theory/arith/theory_arith.cpp | |
| parent | f2d98d87361fc1a44e64677586f5c8d4625a4756 (diff) | |
Partial fix to bug 295.
Diffstat (limited to 'src/theory/arith/theory_arith.cpp')
| -rw-r--r-- | src/theory/arith/theory_arith.cpp | 15 |
1 files changed, 6 insertions, 9 deletions
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index a99d86a9c..ca0763a0c 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -595,7 +595,8 @@ Node TheoryArith::assertionCases(TNode assertion){ ArithVar x_i = determineLeftVariable(assertion, simpKind); DeltaRational c_i = determineRightConstant(assertion, simpKind); - Debug("arith::assertions") << "arith assertion(" << assertion + Debug("arith::assertions") << "arith assertion @" << getContext()->getLevel() + <<"(" << assertion << " \\-> " << x_i<<" "<< simpKind <<" "<< c_i << ")" << std::endl; switch(simpKind){ @@ -879,14 +880,10 @@ void TheoryArith::debugPrintModel(){ } Node TheoryArith::explain(TNode n) { - Debug("explain") << "explain @" << getContext()->getLevel() << ": " << n << endl; + Debug("arith::explain") << "explain @" << getContext()->getLevel() << ": " << n << endl; Assert(d_propManager.isPropagated(n)); - if(d_propManager.isFlagged(n)){ - return d_differenceManager.explain(n); - }else{ - return d_propManager.explain(n); - } + return d_propManager.explain(n); } void flattenAnd(Node n, std::vector<TNode>& out){ @@ -923,7 +920,7 @@ void TheoryArith::propagate(Effort e) { TNode atom = (toProp.getKind() == kind::NOT) ? toProp[0] : toProp; - Debug("arith::propagate") << "propagate " << flag << " " << toProp << endl; + Debug("arith::propagate") << "propagate @" << getContext()->getLevel() <<" flag: "<< flag << " " << toProp << endl; if(flag) { //Currently if the flag is set this came from an equality detected by the @@ -938,7 +935,7 @@ void TheoryArith::propagate(Effort e) { }else{ Node exp = d_differenceManager.explain(toProp); Node lp = flattenAnd(exp.andNode(notNormalized)); - Debug("arith::propagate") << "propagate conflict" << lp << endl; + Debug("arith::propagate") << "propagate conflict" << lp << endl; d_out->conflict(lp); propagated = true; |