diff options
| -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); }; |