Added printModel() to src/theory/arith/partial_model.cpp. This is a debugging utilit...

diff --git a/src/theory/arith/partial_model.cpp b/src/theory/arith/partial_model.cpp
index 4ac03c9040c2cdfb5c6d099b66166686b883a95f..c5eb0ad1d4ebafd4113ac8ee7ee5cfddd582554c 100644 (file)
--- 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 5a0b662f830cf039182859390013239f1d23b298..01db59855d42f57d45474c281319ae856b8e4944 100644 (file)
--- 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);
 };