From: Tim King <taking@cs.nyu.edu>
Date: Fri, 28 May 2010 22:06:58 +0000 (+0000)
Subject: Added printModel() to src/theory/arith/partial_model.cpp.  This is a debugging utilit... 
X-Git-Tag: cvc5-1.0.0~9025
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ff066aebdc624a835c00414dd8ef56f70ad3aab2;p=cvc5.git

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.
---

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