From: Morgan Deters <mdeters@gmail.com>
Date: Thu, 14 Jun 2012 14:32:51 +0000 (+0000)
Subject: The "no-tears-in-competition-mode" commit.  Change all (non-driver, non-SAT-solver... 
X-Git-Tag: cvc5-1.0.0~8021
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=de6c0b0929f23fd3d01ae4c8bd3b93d4f484b7c7;p=cvc5.git

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

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);
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index ddb085632..e8a17eadd 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -114,7 +114,7 @@ void TermDb::addTerm( Node n, std::vector< Node >& added, bool withinQuant ){
               for( int i=0; i<(int)d_ith->d_op_triggers[op].size(); i++ ){
                 addedLemmas += d_ith->d_op_triggers[op][i]->addTerm( n );
               }
-              //std::cout << "Terms, added lemmas: " << addedLemmas << std::endl;
+              //Message() << "Terms, added lemmas: " << addedLemmas << std::endl;
               d_quantEngine->flushLemmas( &d_quantEngine->getTheoryEngine()->getTheory( THEORY_QUANTIFIERS )->getOutputChannel() );
             }
           }
diff --git a/src/theory/substitutions.cpp b/src/theory/substitutions.cpp
index 3f8a6d630..65c4524ee 100644
--- a/src/theory/substitutions.cpp
+++ b/src/theory/substitutions.cpp
@@ -289,7 +289,7 @@ void SubstitutionMap::print(ostream& out) const {
 }
 
 void SubstitutionMap::debugPrint() const {
-  print(std::cout);
+  print(Message.getStream());
 }
 
 }/* CVC4::theory namespace */
diff --git a/src/theory/uf/theory_uf_type_rules.h b/src/theory/uf/theory_uf_type_rules.h
index b68a11abd..2856e6a01 100644
--- a/src/theory/uf/theory_uf_type_rules.h
+++ b/src/theory/uf/theory_uf_type_rules.h
@@ -46,8 +46,8 @@ public:
         TypeNode currentArgumentType = *argument_type_it;
         if(!currentArgument.isSubtypeOf(currentArgumentType)) {
           std::stringstream ss;
-          ss << Expr::setlanguage(language::toOutputLanguage(Options::current()->inputLanguage))
-             << "argument types is not a subtype of the function's argument type:\n"
+          ss << Expr::setlanguage(Options::current()->outputLanguage)
+             << "argument type is not a subtype of the function's argument type:\n"
              << "argument:  " << *argument_it << "\n"
              << "has type:  " << (*argument_it).getType() << "\n"
              << "not subtype: " << *argument_type_it;
diff --git a/src/theory/unconstrained_simplifier.cpp b/src/theory/unconstrained_simplifier.cpp
index 25c7ce711..1c507eb71 100644
--- a/src/theory/unconstrained_simplifier.cpp
+++ b/src/theory/unconstrained_simplifier.cpp
@@ -692,7 +692,7 @@ void UnconstrainedSimplifier::processAssertions(vector<Node>& assertions)
 
   if (!d_unconstrained.empty()) {
     processUnconstrained();
-    //    d_substitutions.print(std::cout);
+    //    d_substitutions.print(Message.getStream());
     for (it = assertions.begin(); it != iend; ++it) {
       (*it) = d_substitutions.apply(*it);
     }