diff options
author | Tim King <taking@cs.nyu.edu> | 2010-05-28 22:06:58 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2010-05-28 22:06:58 +0000 |
commit | ff066aebdc624a835c00414dd8ef56f70ad3aab2 (patch) | |
tree | e14425012ea18388ba74645bade7b990efce24c1 /src/theory/arith | |
parent | 6aa071ef292d999828aa2f53e25179959404bea5 (diff) |
Added printModel() to src/theory/arith/partial_model.cpp. This is a debugging utility that prints out the lower bound, upper bound, assignment, and the constraints that were asserted that caused the lower bound and upperbound to be asserted.
Diffstat (limited to 'src/theory/arith')
-rw-r--r-- | src/theory/arith/partial_model.cpp | 23 | ||||
-rw-r--r-- | src/theory/arith/partial_model.h | 2 |
2 files changed, 25 insertions, 0 deletions
diff --git a/src/theory/arith/partial_model.cpp b/src/theory/arith/partial_model.cpp index 4ac03c904..c5eb0ad1d 100644 --- a/src/theory/arith/partial_model.cpp +++ b/src/theory/arith/partial_model.cpp @@ -223,3 +223,26 @@ void ArithPartialModel::stopRecordingAssignments(bool revert){ } } +void ArithPartialModel::printModel(TNode x){ + + Debug("model") << "model" << x << ":"<< getAssignment(x) << " "; + + CDDRationalMap::iterator i = d_LowerBoundMap.find(x); + if(i != d_LowerBoundMap.end()){ + DeltaRational l = (*i).second; + Debug("model") << l << " "; + Debug("model") << getLowerConstraint(x) << " "; + }else{ + Debug("model") << "no lb "; + } + + i = d_UpperBoundMap.find(x); + if(i != d_UpperBoundMap.end()){ + DeltaRational u = (*i).second; + Debug("model") << u << " "; + Debug("model") << getUpperConstraint(x) << " "; + }else{ + Debug("model") << "no ub "; + } + Debug("model") << endl; +} diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h index 5a0b662f8..01db59855 100644 --- a/src/theory/arith/partial_model.h +++ b/src/theory/arith/partial_model.h @@ -142,6 +142,8 @@ public: bool strictlyBelowUpperBound(TNode x); bool strictlyAboveLowerBound(TNode x); bool assignmentIsConsistent(TNode x); + + void printModel(TNode x); }; |