The "no-tears-in-competition-mode" commit. Change all (non-driver, non-SAT-solver...

diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp
index b441058953586195bb3afd15486934d063c3c299..ce338b5f3e72389fdacba75aa17352a76a07861f 100644 (file)
--- 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 28fe86c70874a82a34562d282efc92c4e811a22f..1ad6dd39582b5f9a8b676cb7cc28761dc7875a50 100644 (file)
--- 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 73087d4e89a1d745225356b17e4f13ad06fe84ac..ee71dea741cc4547496bd2256e8b19fc1c170e8c 100644 (file)
--- 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 16fd28649c184e87f3b8fa70f9643078c71a07cc..a48a13720289c2e72c53463653a5d49a04cfe5ca 100644 (file)
--- 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 7a8e0fab48b5e35fbcf91a4f73e51b8d6256dd22..97729b1a4b390d9d46b757a74f7d2b124946290e 100644 (file)
--- 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 ddb085632c38f78863e2992b1c9594e2015e231e..e8a17eadd2112aaecff838d0ff8ca77b96b158f2 100644 (file)
--- 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 3f8a6d630b933a792b141286f7c6fb755f8232e0..65c4524ee20c204ec6c7c83370c0c1f8dbd4222a 100644 (file)
--- 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 b68a11abd2ec3f5138eb11403da1ca6234ac8a4e..2856e6a01616d5323d048e1ac89bdd72c302357e 100644 (file)
--- 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 25c7ce7113ea324e910751a16c717071643526c4..1c507eb710b1a8101e48691e5f7d35c1ad939396 100644 (file)
--- 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);
     }