The "no-tears-in-competition-mode" commit. Change all (non-driver, non-SAT-solver) uses of std::cout to the Message stream, and all uses of std::cerr to the Warning stream.

5 files changed, 15 insertions, 15 deletions

diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp
index b44105895..ce338b5f3 100644
--- a/src/theory/arith/constraint.cpp
+++ b/src/theory/arith/constraint.cpp
@@ -128,7 +128,7 @@ std::ostream& operator<<(std::ostream& o, const ValueCollection& vc){
 }
 
 void ConstraintValue::debugPrint() const {
-  cout << *this << endl;
+  Message() << *this << endl;
 }
 
 void ValueCollection::push_into(std::vector<Constraint>& vec) const {
diff --git a/src/theory/arith/dio_solver.cpp b/src/theory/arith/dio_solver.cpp
index 28fe86c70..1ad6dd395 100644
--- a/src/theory/arith/dio_solver.cpp
+++ b/src/theory/arith/dio_solver.cpp
@@ -776,8 +776,8 @@ void DioSolver::debugPrintTrail(DioSolver::TrailIndex i) const{
   const SumPair& eq = d_trail[i].d_eq;
   const Polynomial& proof = d_trail[i].d_proof;
 
-  cout << "d_trail["<<i<<"].d_eq = " << eq.getNode() << endl;
-  cout << "d_trail["<<i<<"].d_proof = " << proof.getNode() << endl;
+  Message() << "d_trail["<<i<<"].d_eq = " << eq.getNode() << endl;
+  Message() << "d_trail["<<i<<"].d_proof = " << proof.getNode() << endl;
 }
 
 void DioSolver::subAndReduceCurrentFByIndex(DioSolver::SubIndex subIndex){
diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp
index 73087d4e8..ee71dea74 100644
--- a/src/theory/arith/simplex.cpp
+++ b/src/theory/arith/simplex.cpp
@@ -287,11 +287,11 @@ Result::Sat SimplexDecisionProcedure::findModel(bool exactResult){
 
     if(verbose && numDifferencePivots > 0){
       if(result ==  Result::UNSAT){
-        cout << "diff order found unsat" << endl;
+        Message() << "diff order found unsat" << endl;
       }else if(d_queue.empty()){
-        cout << "diff order found model" << endl;
+        Message() << "diff order found model" << endl;
       }else{
-        cout << "diff order missed" << endl;
+        Message() << "diff order missed" << endl;
       }
     }
   }
@@ -316,11 +316,11 @@ Result::Sat SimplexDecisionProcedure::findModel(bool exactResult){
       }
       if(verbose){
         if(result ==  Result::UNSAT){
-          cout << "bland found unsat" << endl;
+          Message() << "bland found unsat" << endl;
         }else if(d_queue.empty()){
-          cout << "bland found model" << endl;
+          Message() << "bland found model" << endl;
         }else{
-          cout << "bland order missed" << endl;
+          Message() << "bland order missed" << endl;
         }
       }
     }else{
@@ -335,11 +335,11 @@ Result::Sat SimplexDecisionProcedure::findModel(bool exactResult){
 
       if(verbose){
         if(result ==  Result::UNSAT){
-          cout << "restricted var order found unsat" << endl;
+          Message() << "restricted var order found unsat" << endl;
         }else if(d_queue.empty()){
-          cout << "restricted var order found model" << endl;
+          Message() << "restricted var order found model" << endl;
         }else{
-          cout << "restricted var order missed" << endl;
+          Message() << "restricted var order missed" << endl;
         }
       }
     }
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 16fd28649..a48a13720 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -1723,7 +1723,7 @@ void TheoryArith::propagate(Effort e) {
 
     if(c->negationHasProof()){
       Node conflict = ConstraintValue::explainConflict(c, c->getNegation());
-      cout << "tears " << conflict << endl;
+      Message() << "tears " << conflict << endl;
       Debug("arith::prop") << "propagate conflict" << conflict << endl;
       d_out->conflict(conflict);
       return;
@@ -1950,7 +1950,7 @@ bool TheoryArith::entireStateIsConsistent(){
     ArithVar var = d_arithvarNodeMap.asArithVar(*i);
     if(!d_partialModel.assignmentIsConsistent(var)){
       d_partialModel.printModel(var);
-      cerr << "Assignment is not consistent for " << var << *i << endl;
+      Warning() << "Assignment is not consistent for " << var << *i << endl;
       return false;
     }
   }
diff --git a/src/theory/arith/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h
index 7a8e0fab4..97729b1a4 100644
--- a/src/theory/arith/theory_arith_type_rules.h
+++ b/src/theory/arith/theory_arith_type_rules.h
@@ -76,7 +76,7 @@ public:
     if( check ) {
       TypeNode lhsType = n[0].getType(check);
       if (!lhsType.isReal()) {
-        std::cout << lhsType << " : " << n[0] << std::endl;
+        Message() << lhsType << " : " << n[0] << std::endl;
         throw TypeCheckingExceptionPrivate(n, "expecting an arithmetic term on the left-hand-side");
       }
       TypeNode rhsType = n[1].getType(check);