Rename macro Message to CVC4Message. (#5576)

1 files changed, 38 insertions, 19 deletions

diff --git a/src/theory/arith/fc_simplex.cpp b/src/theory/arith/fc_simplex.cpp
index 7b482b314..33f01eba1 100644
--- a/src/theory/arith/fc_simplex.cpp
+++ b/src/theory/arith/fc_simplex.cpp
@@ -98,7 +98,10 @@ Result::Sat FCSimplexDecisionProcedure::findModel(bool exactResult){
   if(d_errorSet.errorEmpty() && !d_errorSet.moreSignals()){
     Debug("arith::findModel") << "fcFindModel("<< instance <<") trivial" << endl;
     Assert(d_conflictVariables.empty());
-    //if(verbose){ Message() << "fcFindModel("<< instance <<") trivial" << endl; }
+    //if (verbose)
+    //{
+    //  CVC4Message() << "fcFindModel(" << instance << ") trivial" << endl;
+    //}
     return Result::SAT;
   }
 
@@ -110,12 +113,18 @@ Result::Sat FCSimplexDecisionProcedure::findModel(bool exactResult){
 
   if(initialProcessSignals()){
     d_conflictVariables.purge();
-    if(verbose){ Message() << "fcFindModel("<< instance <<") early conflict" << endl; }
+    if (verbose)
+    {
+      CVC4Message() << "fcFindModel(" << instance << ") early conflict" << endl;
+    }
     Debug("arith::findModel") << "fcFindModel("<< instance <<") early conflict" << endl;
     Assert(d_conflictVariables.empty());
     return Result::UNSAT;
   }else if(d_errorSet.errorEmpty()){
-    //if(verbose){ Message() << "fcFindModel("<< instance <<") fixed itself" << endl; }
+    //if (verbose)
+    //{
+    //  CVC4Message() << "fcFindModel(" << instance << ") fixed itself" << endl;
+    //}
     Debug("arith::findModel") << "fcFindModel("<< instance <<") fixed itself" << endl;
     if (verbose) Assert(!d_errorSet.moreSignals());
     Assert(d_conflictVariables.empty());
@@ -142,17 +151,27 @@ Result::Sat FCSimplexDecisionProcedure::findModel(bool exactResult){
 
     if(result ==  Result::UNSAT){
       ++(d_statistics.d_fcFoundUnsat);
-      if(verbose){ Message() << "fc found unsat";}
+      if (verbose)
+      {
+        CVC4Message() << "fc found unsat";
+      }
     }else if(d_errorSet.errorEmpty()){
       ++(d_statistics.d_fcFoundSat);
-      if(verbose){ Message() << "fc found model"; }
+      if (verbose)
+      {
+        CVC4Message() << "fc found model";
+      }
     }else{
       ++(d_statistics.d_fcMissed);
-      if(verbose){ Message() << "fc missed"; }
+      if (verbose)
+      {
+        CVC4Message() << "fc missed";
+      }
     }
   }
-  if(verbose){
-    Message() << "(" << instance << ") pivots " << d_pivots << endl;
+  if (verbose)
+  {
+    CVC4Message() << "(" << instance << ") pivots " << d_pivots << endl;
   }
 
   Assert(!d_errorSet.moreSignals());
@@ -524,12 +543,10 @@ void FCSimplexDecisionProcedure::updateAndSignal(const UpdateInfo& selected, Wit
     }
     if(degenerate(w) && selected.describesPivot()){
       ArithVar leaving = selected.leaving();
-      Message()
-        << "degenerate " << leaving
-        << ", atBounds " << d_linEq.basicsAtBounds(selected)
-        << ", len " << d_tableau.basicRowLength(leaving)
-        << ", bc " << d_linEq.debugBasicAtBoundCount(leaving)
-        << endl;
+      CVC4Message() << "degenerate " << leaving << ", atBounds "
+                    << d_linEq.basicsAtBounds(selected) << ", len "
+                    << d_tableau.basicRowLength(leaving) << ", bc "
+                    << d_linEq.debugBasicAtBoundCount(leaving) << endl;
     }
   }
 
@@ -575,9 +592,10 @@ void FCSimplexDecisionProcedure::updateAndSignal(const UpdateInfo& selected, Wit
     }
   }
 
-  if(verbose){
-    Message() << "conflict variable " << selected << endl;
-    Message() << ss.str();
+  if (verbose)
+  {
+    CVC4Message() << "conflict variable " << selected << endl;
+    CVC4Message() << ss.str();
   }
   if(Debug.isOn("error")){ d_errorSet.debugPrint(Debug("error")); }
 
@@ -791,8 +809,9 @@ Result::Sat FCSimplexDecisionProcedure::dualLike(){
     Assert(d_focusSize == d_errorSet.focusSize());
     Assert(d_errorSize == d_errorSet.errorSize());
 
-    if(verbose){
-      debugDualLike(w,  Message(), instance, prevFocusSize, prevErrorSize);
+    if (verbose)
+    {
+      debugDualLike(w, CVC4Message(), instance, prevFocusSize, prevErrorSize);
     }
     Assert(debugDualLike(
         w, Debug("dualLike"), instance, prevFocusSize, prevErrorSize));