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.

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