From d5638ce2fc70625c2b0bbc013b37d96fb5306568 Mon Sep 17 00:00:00 2001
From: Tim King <taking@cs.nyu.edu>
Date: Tue, 7 May 2013 14:35:22 -0400
Subject: [PATCH] Improving arithmetic debugging output.

---
 src/theory/arith/partial_model.h          |  5 +++
 src/theory/arith/theory_arith_private.cpp | 37 +++++++++++++++--------
 src/theory/arith/theory_arith_private.h   |  4 +--
 3 files changed, 31 insertions(+), 15 deletions(-)

diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h
index 953c8c0d3..deafb559a 100644
--- a/src/theory/arith/partial_model.h
+++ b/src/theory/arith/partial_model.h
@@ -204,6 +204,11 @@ private:
   bool isSlack(ArithVar x) const {
     return d_vars[x].d_slack;
   }
+
+  bool integralAssignment(ArithVar x) const {
+    return getAssignment(x).isIntegral();
+  }
+
  private:
 
   typedef std::pair<ArithVar, Constraint> AVCPair;
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 9c43ca962..d911ecf77 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -1721,7 +1721,7 @@ void TheoryArithPrivate::check(Theory::Effort effortLevel){
 
 
   if(Debug.isOn("arith::print_assertions")) {
-    debugPrintAssertions();
+    debugPrintAssertions(Debug("arith::print_assertions"));
   }
 
   bool emmittedConflictOrSplit = false;
@@ -1922,7 +1922,9 @@ void TheoryArithPrivate::check(Theory::Effort effortLevel){
   }
 
   if(Debug.isOn("paranoid:check_tableau")){ d_linEq.debugCheckTableau(); }
-  if(Debug.isOn("arith::print_model")) { debugPrintModel(); }
+  if(Debug.isOn("arith::print_model")) {
+    debugPrintModel(Debug("arith::print_model"));
+  }
   Debug("arith") << "TheoryArithPrivate::check end" << std::endl;
 }
 
@@ -2043,37 +2045,38 @@ bool TheoryArithPrivate::splitDisequalities(){
  * Should be guarded by at least Debug.isOn("arith::print_assertions").
  * Prints to Debug("arith::print_assertions")
  */
-void TheoryArithPrivate::debugPrintAssertions() {
-  Debug("arith::print_assertions") << "Assertions:" << endl;
+void TheoryArithPrivate::debugPrintAssertions(std::ostream& out) const {
+  out << "Assertions:" << endl;
   for (var_iterator vi = var_begin(), vend = var_end(); vi != vend; ++vi){
     ArithVar i = *vi;
     if (d_partialModel.hasLowerBound(i)) {
       Constraint lConstr = d_partialModel.getLowerBoundConstraint(i);
-      Debug("arith::print_assertions") << lConstr << endl;
+      out << lConstr << endl;
     }
 
     if (d_partialModel.hasUpperBound(i)) {
       Constraint uConstr = d_partialModel.getUpperBoundConstraint(i);
-      Debug("arith::print_assertions") << uConstr << endl;
+      out << uConstr << endl;
     }
   }
   context::CDQueue<Constraint>::const_iterator it = d_diseqQueue.begin();
   context::CDQueue<Constraint>::const_iterator it_end = d_diseqQueue.end();
   for(; it != it_end; ++ it) {
-    Debug("arith::print_assertions") << *it << endl;
+    out << *it << endl;
   }
 }
 
-void TheoryArithPrivate::debugPrintModel(){
-  Debug("arith::print_model") << "Model:" << endl;
+void TheoryArithPrivate::debugPrintModel(std::ostream& out) const{
+  out << "Model:" << endl;
   for (var_iterator vi = var_begin(), vend = var_end(); vi != vend; ++vi){
     ArithVar i = *vi;
     if(d_partialModel.hasNode(i)){
-      Debug("arith::print_model") << d_partialModel.asNode(i) << " : " <<
+      out << d_partialModel.asNode(i) << " : " <<
         d_partialModel.getAssignment(i);
-      if(d_tableau.isBasic(i))
-        Debug("arith::print_model") << " (basic)";
-      Debug("arith::print_model") << endl;
+      if(d_tableau.isBasic(i)){
+        out << " (basic)";
+      }
+      out << endl;
     }
   }
 }
@@ -2406,6 +2409,14 @@ bool TheoryArithPrivate::entireStateIsConsistent(const string& s){
       }
       Warning() << endl;
       result = false;
+    }else if(d_partialModel.isInteger(var) && !d_partialModel.integralAssignment(var)){
+      d_partialModel.printModel(var);
+      Warning() << s << ":" << "Assignment is not integer for integer variable " << var << d_partialModel.asNode(var);
+      if(d_tableau.isBasic(var)){
+        Warning() << " (basic)";
+      }
+      Warning() << endl;
+      result = false;
     }
   }
   return result;
diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h
index c8f49ab01..2ea3bb68e 100644
--- a/src/theory/arith/theory_arith_private.h
+++ b/src/theory/arith/theory_arith_private.h
@@ -534,9 +534,9 @@ private:
                  std::vector<ArithVar>& variables);
 
   /** Routine for debugging. Print the assertions the theory is aware of. */
-  void debugPrintAssertions();
+  void debugPrintAssertions(std::ostream& out) const;
   /** Debugging only routine. Prints the model. */
-  void debugPrintModel();
+  void debugPrintModel(std::ostream& out) const;
 
   inline LogicInfo getLogicInfo() const { return d_containing.getLogicInfo(); }
   inline bool done() const { return d_containing.done(); }
-- 
2.30.2