From ff066aebdc624a835c00414dd8ef56f70ad3aab2 Mon Sep 17 00:00:00 2001
From: Tim King <taking@cs.nyu.edu>
Date: Fri, 28 May 2010 22:06:58 +0000
Subject: [PATCH] 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.

---
 src/theory/arith/partial_model.cpp | 23 +++++++++++++++++++++++
 src/theory/arith/partial_model.h   |  2 ++
 2 files changed, 25 insertions(+)

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