Rename macro Message to CVC4Message. (#5576)

diff --git a/src/base/output.h b/src/base/output.h
index e23f6278336aa0984688a67fda3dbfdbeb7585a3..96cb9f8acb32e296af9b91bf5a668920e329cc2b 100644 (file)
--- a/src/base/output.h
+++ b/src/base/output.h
@@ -404,7 +404,8 @@ extern DumpOutC DumpOutChannel CVC4_PUBLIC;
 #  define Debug ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::DebugChannel
 #  define Warning ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::WarningChannel
 #  define WarningOnce ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::WarningChannel
-#  define Message ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::MessageChannel
+#define CVC4Message \
+  ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::MessageChannel
 #  define Notice ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::NoticeChannel
 #  define Chat ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::ChatChannel
 #  define Trace ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::TraceChannel
@@ -419,7 +420,9 @@ extern DumpOutC DumpOutChannel CVC4_PUBLIC;
 #  endif /* CVC4_DEBUG && CVC4_TRACING */
 #  define Warning (! ::CVC4::WarningChannel.isOn()) ? ::CVC4::nullCvc4Stream : ::CVC4::WarningChannel
 #  define WarningOnce (! ::CVC4::WarningChannel.isOn() || ! ::CVC4::WarningChannel.warnOnce(__FILE__,__LINE__)) ? ::CVC4::nullCvc4Stream : ::CVC4::WarningChannel
-#  define Message (! ::CVC4::MessageChannel.isOn()) ? ::CVC4::nullCvc4Stream : ::CVC4::MessageChannel
+#define CVC4Message                                         \
+  (!::CVC4::MessageChannel.isOn()) ? ::CVC4::nullCvc4Stream \
+                                   : ::CVC4::MessageChannel
 #  define Notice (! ::CVC4::NoticeChannel.isOn()) ? ::CVC4::nullCvc4Stream : ::CVC4::NoticeChannel
 #  define Chat (! ::CVC4::ChatChannel.isOn()) ? ::CVC4::nullCvc4Stream : ::CVC4::ChatChannel
 #  ifdef CVC4_TRACING

diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index ab2c8a218cee63a746684efee2f8ccddd68ed2c5..9b0fc81be0a25def35308fa2430aaec57b8e688d 100644 (file)
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -216,16 +216,17 @@ int runCvc4(int argc, char* argv[], Options& opts) {
       InteractiveShell shell(pExecutor->getSolver(),
                              pExecutor->getSymbolManager());
       if(opts.getInteractivePrompt()) {
-        Message() << Configuration::getPackageName()
-                  << " " << Configuration::getVersionString();
+        CVC4Message() << Configuration::getPackageName() << " "
+                      << Configuration::getVersionString();
         if(Configuration::isGitBuild()) {
-          Message() << " [" << Configuration::getGitId() << "]";
+          CVC4Message() << " [" << Configuration::getGitId() << "]";
         }
-        Message() << (Configuration::isDebugBuild() ? " DEBUG" : "")
-                  << " assertions:"
-                  << (Configuration::isAssertionBuild() ? "on" : "off")
-                  << endl << endl;
-        Message() << Configuration::copyright() << endl;
+        CVC4Message() << (Configuration::isDebugBuild() ? " DEBUG" : "")
+                      << " assertions:"
+                      << (Configuration::isAssertionBuild() ? "on" : "off")
+                      << endl
+                      << endl;
+        CVC4Message() << Configuration::copyright() << endl;
       }
 
       while(true) {

diff --git a/src/parser/antlr_tracing.h b/src/parser/antlr_tracing.h
index 03e77224b30d2ae3541f2e1cb3afb469c3a88d64..b8a18aba854c582ac0f740b7bd07247419e60183 100644 (file)
--- a/src/parser/antlr_tracing.h
+++ b/src/parser/antlr_tracing.h
@@ -53,7 +53,7 @@ static struct __Cvc4System {
   struct JavaPrinter {
     template <class T>
     JavaPrinter operator+(const T& t) const {
-      Message() << t;
+      CVC4Message() << t;
       return JavaPrinter();
     }
   };/* struct JavaPrinter */
@@ -66,7 +66,7 @@ static struct __Cvc4System {
      * to the call-by-value semantics of C.  All that's left to
      * do is print the newline.
      */
-    void println(JavaPrinter) { Message() << std::endl; }
+    void println(JavaPrinter) { CVC4Message() << std::endl; }
   } out;
 } System;
 

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 30edf86cd81368036a61d6fe4f0c98334fb041da..f174ed4706a5eaccd3cb1bd4aa75e0595ea387d4 100644 (file)
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -799,24 +799,24 @@ mainCommand[std::unique_ptr<CVC4::Command>* cmd]
   | DBG_TOK
     ( ( str[s] | IDENTIFIER { s = AntlrInput::tokenText($IDENTIFIER); } )
       { Debug.on(s); Trace.on(s); }
-    | { Message() << "Please specify what to debug." << std::endl; }
+    | { CVC4Message() << "Please specify what to debug." << std::endl; }
     )
 
   | TRACE_TOK
     ( ( str[s] | IDENTIFIER { s = AntlrInput::tokenText($IDENTIFIER); } )
       { Trace.on(s); }
-    | { Message() << "Please specify something to trace." << std::endl; }
+    | { CVC4Message() << "Please specify something to trace." << std::endl; }
     )
   | UNTRACE_TOK
     ( ( str[s] | IDENTIFIER { s = AntlrInput::tokenText($IDENTIFIER); } )
       { Trace.off(s); }
-    | { Message() << "Please specify something to untrace." << std::endl; }
+    | { CVC4Message() << "Please specify something to untrace." << std::endl; }
     )
 
   | HELP_TOK
     ( ( str[s] | IDENTIFIER { s = AntlrInput::tokenText($IDENTIFIER); } )
-      { Message() << "No help available for `" << s << "'." << std::endl; }
-  |   { Message() << "Please use --help at the command line for help."
+      { CVC4Message() << "No help available for `" << s << "'." << std::endl; }
+  |   { CVC4Message() << "Please use --help at the command line for help."
                 << std::endl; }
             )
 

diff --git a/src/preprocessing/passes/unconstrained_simplifier.cpp b/src/preprocessing/passes/unconstrained_simplifier.cpp
index a4e7ac7032bee9a9a913b6ba207970a5d7a89188..51434e3695c41be644fd94323f2f53a006b93d17 100644 (file)
--- a/src/preprocessing/passes/unconstrained_simplifier.cpp
+++ b/src/preprocessing/passes/unconstrained_simplifier.cpp
@@ -853,7 +853,7 @@ PreprocessingPassResult UnconstrainedSimplifier::applyInternal(
   if (!d_unconstrained.empty())
   {
     processUnconstrained();
-    //    d_substitutions.print(Message.getStream());
+    //    d_substitutions.print(CVC4Message.getStream());
     for (size_t i = 0, asize = assertions.size(); i < asize; ++i)
     {
       Node a = assertions[i];

diff --git a/src/smt/managed_ostreams.cpp b/src/smt/managed_ostreams.cpp
index c49de7372b6d8e1eafa420f30dc4cb8b7a9365f8..27a90cb56dabb5a350ae9beae296a6f89561c399 100644 (file)
--- a/src/smt/managed_ostreams.cpp
+++ b/src/smt/managed_ostreams.cpp
@@ -122,8 +122,9 @@ ManagedDiagnosticOutputChannel::~ManagedDiagnosticOutputChannel() {
   if(Warning.getStreamPointer() == getManagedOstream()){
     Warning.setStream(&null_os);
   }
-  if(Message.getStreamPointer() == getManagedOstream()){
-    Message.setStream(&null_os);
+  if (CVC4Message.getStreamPointer() == getManagedOstream())
+  {
+    CVC4Message.setStream(&null_os);
   }
   if(Notice.getStreamPointer() == getManagedOstream()){
     Notice.setStream(&null_os);

diff --git a/src/smt/options_manager.cpp b/src/smt/options_manager.cpp
index 81e13c446d4319c6d7cc484d9b9e761cccf2682c..e028068ee962d11f47ba183536372cf58aa54f51 100644 (file)
--- a/src/smt/options_manager.cpp
+++ b/src/smt/options_manager.cpp
@@ -76,7 +76,7 @@ void OptionsManager::notifySetOption(const std::string& key)
     Trace.getStream() << expr::ExprSetDepth(depth);
     Notice.getStream() << expr::ExprSetDepth(depth);
     Chat.getStream() << expr::ExprSetDepth(depth);
-    Message.getStream() << expr::ExprSetDepth(depth);
+    CVC4Message.getStream() << expr::ExprSetDepth(depth);
     Warning.getStream() << expr::ExprSetDepth(depth);
     // intentionally exclude Dump stream from this list
   }
@@ -87,7 +87,7 @@ void OptionsManager::notifySetOption(const std::string& key)
     Trace.getStream() << expr::ExprDag(dag);
     Notice.getStream() << expr::ExprDag(dag);
     Chat.getStream() << expr::ExprDag(dag);
-    Message.getStream() << expr::ExprDag(dag);
+    CVC4Message.getStream() << expr::ExprDag(dag);
     Warning.getStream() << expr::ExprDag(dag);
     Dump.getStream() << expr::ExprDag(dag);
   }
@@ -103,7 +103,7 @@ void OptionsManager::notifySetOption(const std::string& key)
     Trace.getStream() << Command::printsuccess(value);
     Notice.getStream() << Command::printsuccess(value);
     Chat.getStream() << Command::printsuccess(value);
-    Message.getStream() << Command::printsuccess(value);
+    CVC4Message.getStream() << Command::printsuccess(value);
     Warning.getStream() << Command::printsuccess(value);
     *options::out() << Command::printsuccess(value);
   }

diff --git a/src/smt/update_ostream.h b/src/smt/update_ostream.h
index e2a482e30bf6fd36907d0a12268d3d174c28e458..fd33beec75b9127aab537d425c991d343a94713e 100644 (file)
--- a/src/smt/update_ostream.h
+++ b/src/smt/update_ostream.h
@@ -94,8 +94,8 @@ class WarningOstreamUpdate : public OstreamUpdate {
 
 class MessageOstreamUpdate : public OstreamUpdate {
  public:
-  std::ostream& get() override { return Message.getStream(); }
-  void set(std::ostream* setTo) override { Message.setStream(setTo); }
+  std::ostream& get() override { return CVC4Message.getStream(); }
+  void set(std::ostream* setTo) override { CVC4Message.setStream(setTo); }
 };  /* class MessageOstreamUpdate */
 
 class NoticeOstreamUpdate : public OstreamUpdate {

diff --git a/src/theory/arith/approx_simplex.cpp b/src/theory/arith/approx_simplex.cpp
index 7c89a9e393e786c3fef2ccf7d5a1503cd37d4dd7..2432e6945fc1f61961944f60e7154ac5532f1ccc 100644 (file)
--- a/src/theory/arith/approx_simplex.cpp
+++ b/src/theory/arith/approx_simplex.cpp
@@ -630,9 +630,10 @@ ApproxGLPK::ApproxGLPK(const ArithVariables& v, TreeLog& l, ApproximateStatistic
   for(ArithVariables::var_iterator vi = d_vars.var_begin(), vi_end = d_vars.var_end(); vi != vi_end; ++vi){
     ArithVar v = *vi;
 
-    if(s_verbosity >= 2){
-      //Message() << v  << " ";
-      //d_vars.printModel(v, Message());
+    if (s_verbosity >= 2)
+    {
+      // CVC4Message() << v  << " ";
+      // d_vars.printModel(v, CVC4Message());
     }
 
     int type;
@@ -763,9 +764,10 @@ ArithRatPairVec ApproxGLPK::heuristicOptCoeffs() const{
   for(ArithVariables::var_iterator vi = d_vars.var_begin(), vi_end = d_vars.var_end(); vi != vi_end; ++vi){
     ArithVar v = *vi;
 
-    if(s_verbosity >= 2){
-      Message() << v  << " ";
-      d_vars.printModel(v, Message());
+    if (s_verbosity >= 2)
+    {
+      CVC4Message() << v << " ";
+      d_vars.printModel(v, CVC4Message());
     }
 
     int type;
@@ -865,9 +867,11 @@ ArithRatPairVec ApproxGLPK::heuristicOptCoeffs() const{
 
       int dir = guessDir(r);
       if(len >= rowLengthReq){
-        if(s_verbosity >= 1){
-          Message() << "high row " << r << " " << len << " " << avgRowLength << " " << dir<< endl;
-          d_vars.printModel(r, Message());
+        if (s_verbosity >= 1)
+        {
+          CVC4Message() << "high row " << r << " " << len << " " << avgRowLength
+                        << " " << dir << endl;
+          d_vars.printModel(r, CVC4Message());
         }
         ret.push_back(ArithRatPair(r, Rational(dir)));
       }
@@ -885,9 +889,11 @@ ArithRatPairVec ApproxGLPK::heuristicOptCoeffs() const{
       double ubScore = double(bc.upperBoundCount()) / maxCount;
       double lbScore = double(bc.lowerBoundCount()) / maxCount;
       if(ubScore  >= .9 || lbScore >= .9){
-        if(s_verbosity >= 1){
-          Message() << "high col " << c << " " << bc << " " << ubScore << " " << lbScore << " " << dir << endl;
-          d_vars.printModel(c, Message());
+        if (s_verbosity >= 1)
+        {
+          CVC4Message() << "high col " << c << " " << bc << " " << ubScore
+                        << " " << lbScore << " " << dir << endl;
+          d_vars.printModel(c, CVC4Message());
         }
         ret.push_back(ArithRatPair(c, Rational(c)));
       }
@@ -1009,22 +1015,26 @@ ApproximateSimplex::Solution ApproxGLPK::extractSolution(bool mip) const
 
     int status = isAux ? glp_get_row_stat(prob, glpk_index)
       : glp_get_col_stat(prob, glpk_index);
-    if(s_verbosity >= 2){
-      Message() << "assignment " << vi << endl;
+    if (s_verbosity >= 2)
+    {
+      CVC4Message() << "assignment " << vi << endl;
     }
 
     bool useDefaultAssignment = false;
 
     switch(status){
     case GLP_BS:
-      //Message() << "basic" << endl;
+      // CVC4Message() << "basic" << endl;
       newBasis.add(vi);
       useDefaultAssignment = true;
       break;
     case GLP_NL:
     case GLP_NS:
       if(!mip){
-        if(s_verbosity >= 2){ Message() << "non-basic lb" << endl; }
+        if (s_verbosity >= 2)
+        {
+          CVC4Message() << "non-basic lb" << endl;
+        }
         newValues.set(vi, d_vars.getLowerBound(vi));
       }else{// intentionally fall through otherwise
         useDefaultAssignment = true;
@@ -1032,7 +1042,10 @@ ApproximateSimplex::Solution ApproxGLPK::extractSolution(bool mip) const
       break;
     case GLP_NU:
       if(!mip){
-        if(s_verbosity >= 2){ Message() << "non-basic ub" << endl; }
+        if (s_verbosity >= 2)
+        {
+          CVC4Message() << "non-basic ub" << endl;
+        }
         newValues.set(vi, d_vars.getUpperBound(vi));
       }else {// intentionally fall through otherwise
         useDefaultAssignment = true;
@@ -1046,7 +1059,10 @@ ApproximateSimplex::Solution ApproxGLPK::extractSolution(bool mip) const
     }
 
     if(useDefaultAssignment){
-      if(s_verbosity >= 2){ Message() << "non-basic other" << endl; }
+      if (s_verbosity >= 2)
+      {
+        CVC4Message() << "non-basic other" << endl;
+      }
 
       double newAssign;
       if(mip){
@@ -1058,24 +1074,35 @@ ApproximateSimplex::Solution ApproxGLPK::extractSolution(bool mip) const
       }
       const DeltaRational& oldAssign = d_vars.getAssignment(vi);
 
-
-      if(d_vars.hasLowerBound(vi) &&
-         roughlyEqual(newAssign, d_vars.getLowerBound(vi).approx(SMALL_FIXED_DELTA))){
-        //Message() << "  to lb" << endl;
+      if (d_vars.hasLowerBound(vi)
+          && roughlyEqual(newAssign,
+                          d_vars.getLowerBound(vi).approx(SMALL_FIXED_DELTA)))
+      {
+        // CVC4Message() << "  to lb" << endl;
 
         newValues.set(vi, d_vars.getLowerBound(vi));
-      }else if(d_vars.hasUpperBound(vi) &&
-               roughlyEqual(newAssign, d_vars.getUpperBound(vi).approx(SMALL_FIXED_DELTA))){
+      }
+      else if (d_vars.hasUpperBound(vi)
+               && roughlyEqual(
+                   newAssign,
+                   d_vars.getUpperBound(vi).approx(SMALL_FIXED_DELTA)))
+      {
         newValues.set(vi, d_vars.getUpperBound(vi));
-        // Message() << "  to ub" << endl;
-      }else{
-
+        // CVC4Message() << "  to ub" << endl;
+      }
+      else
+      {
         double rounded = round(newAssign);
-        if(roughlyEqual(newAssign, rounded)){
-          // Message() << "roughly equal " << rounded << " " << newAssign << " " << oldAssign << endl;
+        if (roughlyEqual(newAssign, rounded))
+        {
+          // CVC4Message() << "roughly equal " << rounded << " " << newAssign <<
+          // " " << oldAssign << endl;
           newAssign = rounded;
-        }else{
-          // Message() << "not roughly equal " << rounded << " " << newAssign << " " << oldAssign << endl;
+        }
+        else
+        {
+          // CVC4Message() << "not roughly equal " << rounded << " " <<
+          // newAssign << " " << oldAssign << endl;
         }
 
         DeltaRational proposal;
@@ -1089,20 +1116,29 @@ ApproximateSimplex::Solution ApproxGLPK::extractSolution(bool mip) const
           proposal = d_vars.getAssignment(vi);
         }
 
-        if(roughlyEqual(newAssign, oldAssign.approx(SMALL_FIXED_DELTA))){
-          // Message() << "  to prev value" << newAssign << " " << oldAssign << endl;
+        if (roughlyEqual(newAssign, oldAssign.approx(SMALL_FIXED_DELTA)))
+        {
+          // CVC4Message() << "  to prev value" << newAssign << " " << oldAssign
+          // << endl;
           proposal = d_vars.getAssignment(vi);
         }
 
-
-        if(d_vars.strictlyLessThanLowerBound(vi, proposal)){
-          //Message() << "  round to lb " << d_vars.getLowerBound(vi) << endl;
+        if (d_vars.strictlyLessThanLowerBound(vi, proposal))
+        {
+          // CVC4Message() << "  round to lb " << d_vars.getLowerBound(vi) <<
+          // endl;
           proposal = d_vars.getLowerBound(vi);
-        }else if(d_vars.strictlyGreaterThanUpperBound(vi, proposal)){
-          //Message() << "  round to ub " << d_vars.getUpperBound(vi) << endl;
+        }
+        else if (d_vars.strictlyGreaterThanUpperBound(vi, proposal))
+        {
+          // CVC4Message() << "  round to ub " << d_vars.getUpperBound(vi) <<
+          // endl;
           proposal = d_vars.getUpperBound(vi);
-        }else{
-          //Message() << "  use proposal" << proposal << " " << oldAssign  << endl;
+        }
+        else
+        {
+          // CVC4Message() << "  use proposal" << proposal << " " << oldAssign
+          // << endl;
         }
         newValues.set(vi, proposal);
       }

diff --git a/src/theory/arith/attempt_solution_simplex.cpp b/src/theory/arith/attempt_solution_simplex.cpp
index b8e08add8f10b34167f28fdf5e6e24d854e0d59b..22802b5583b9061ba0f1d256b872a47f103723ec 100644 (file)
--- a/src/theory/arith/attempt_solution_simplex.cpp
+++ b/src/theory/arith/attempt_solution_simplex.cpp
@@ -122,12 +122,12 @@ Result::Sat AttemptSolutionSDP::attempt(const ApproximateSimplex::Solution& sol)
     Assert(toAdd != ARITHVAR_SENTINEL);
 
     Trace("arith::forceNewBasis") << toRemove << " " << toAdd << endl;
-    //Message() << toRemove << " " << toAdd << endl;
+    // CVC4Message() << toRemove << " " << toAdd << endl;
 
     d_linEq.pivotAndUpdate(toRemove, toAdd, newValues[toRemove]);
 
     Trace("arith::forceNewBasis") << needsToBeAdded.size() << "to go" << endl;
-    //Message() << needsToBeAdded.size() << "to go" << endl;
+    // CVC4Message() << needsToBeAdded.size() << "to go" << endl;
     needsToBeAdded.remove(toAdd);
 
     bool conflict = processSignals();

diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp
index b0be108f72ee13780217f3ed3f072554f37feb0e..03d9c50e94d1c0a854aa765323329998704498a8 100644 (file)
--- a/src/theory/arith/constraint.cpp
+++ b/src/theory/arith/constraint.cpp
@@ -179,10 +179,7 @@ std::ostream& operator<<(std::ostream& o, const ConstraintCPVec& v){
   return o;
 }
 
-void Constraint::debugPrint() const {
-  Message() << *this << endl;
-}
-
+void Constraint::debugPrint() const { CVC4Message() << *this << endl; }
 
 ValueCollection::ValueCollection()
   : d_lowerBound(NullConstraint),

diff --git a/src/theory/arith/dio_solver.cpp b/src/theory/arith/dio_solver.cpp
index 15d6b9f50c26ef153161e3ba0f67a16525ddf2cc..15faf58bffbb382a912db225158e6b88542f8575 100644 (file)
--- a/src/theory/arith/dio_solver.cpp
+++ b/src/theory/arith/dio_solver.cpp
@@ -784,8 +784,8 @@ void DioSolver::debugPrintTrail(DioSolver::TrailIndex i) const{
   const SumPair& eq = d_trail[i].d_eq;
   const Polynomial& proof = d_trail[i].d_proof;
 
-  Message() << "d_trail["<<i<<"].d_eq = " << eq.getNode() << endl;
-  Message() << "d_trail["<<i<<"].d_proof = " << proof.getNode() << endl;
+  CVC4Message() << "d_trail[" << i << "].d_eq = " << eq.getNode() << endl;
+  CVC4Message() << "d_trail[" << i << "].d_proof = " << proof.getNode() << endl;
 }
 
 void DioSolver::subAndReduceCurrentFByIndex(DioSolver::SubIndex subIndex){

diff --git a/src/theory/arith/dual_simplex.cpp b/src/theory/arith/dual_simplex.cpp
index 3d6e92283899e06a5ee0cc6e9124230d78908536..4ac3034ff6013ef42f48bce0d5eeda1fecfd1f8b 100644 (file)
--- a/src/theory/arith/dual_simplex.cpp
+++ b/src/theory/arith/dual_simplex.cpp
@@ -107,13 +107,19 @@ Result::Sat DualSimplexDecisionProcedure::dualFindModel(bool exactResult){
       }
     }
 
-    if(verbose && numDifferencePivots > 0){
-      if(result ==  Result::UNSAT){
-        Message() << "diff order found unsat" << endl;
-      }else if(d_errorSet.errorEmpty()){
-        Message() << "diff order found model" << endl;
-      }else{
-        Message() << "diff order missed" << endl;
+    if (verbose && numDifferencePivots > 0)
+    {
+      if (result == Result::UNSAT)
+      {
+        CVC4Message() << "diff order found unsat" << endl;
+      }
+      else if (d_errorSet.errorEmpty())
+      {
+        CVC4Message() << "diff order found model" << endl;
+      }
+      else
+      {
+        CVC4Message() << "diff order missed" << endl;
       }
     }
   }
@@ -133,13 +139,19 @@ Result::Sat DualSimplexDecisionProcedure::dualFindModel(bool exactResult){
       if(searchForFeasibleSolution(options::arithStandardCheckVarOrderPivots())){
         result = Result::UNSAT;
       }
-      if(verbose){
-        if(result ==  Result::UNSAT){
-          Message() << "restricted var order found unsat" << endl;
-        }else if(d_errorSet.errorEmpty()){
-          Message() << "restricted var order found model" << endl;
-        }else{
-          Message() << "restricted var order missed" << endl;
+      if (verbose)
+      {
+        if (result == Result::UNSAT)
+        {
+          CVC4Message() << "restricted var order found unsat" << endl;
+        }
+        else if (d_errorSet.errorEmpty())
+        {
+          CVC4Message() << "restricted var order found model" << endl;
+        }
+        else
+        {
+          CVC4Message() << "restricted var order missed" << endl;
         }
       }
     }

diff --git a/src/theory/arith/fc_simplex.cpp b/src/theory/arith/fc_simplex.cpp
index 7b482b3146e869c963459267afc9db5182be69f1..33f01eba14bd1ddffb3d736836aa8edb2dbea28c 100644 (file)
--- 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));

diff --git a/src/theory/arith/linear_equality.cpp b/src/theory/arith/linear_equality.cpp
index 32d2714e8e9106d6d16596c3ad20ced77f81e1d2..765061e8d8eb177b9d8b9147871a70185a9075c7 100644 (file)
--- a/src/theory/arith/linear_equality.cpp
+++ b/src/theory/arith/linear_equality.cpp
@@ -184,12 +184,12 @@ void LinearEqualityModule::forceNewBasis(const DenseSet& newBasis){
     Assert(toAdd != ARITHVAR_SENTINEL);
 
     Trace("arith::forceNewBasis") << toRemove << " " << toAdd << endl;
-    Message() << toRemove << " " << toAdd << endl;
+    CVC4Message() << toRemove << " " << toAdd << endl;
     d_tableau.pivot(toRemove, toAdd, d_trackCallback);
     d_basicVariableUpdates(toAdd);
 
     Trace("arith::forceNewBasis") << needsToBeAdded.size() << "to go" << endl;
-    Message() << needsToBeAdded.size() << "to go" << endl;
+    CVC4Message() << needsToBeAdded.size() << "to go" << endl;
     needsToBeAdded.remove(toAdd);
   }
 }

diff --git a/src/theory/arith/soi_simplex.cpp b/src/theory/arith/soi_simplex.cpp
index ecac3d7498d6827394da136f6370236a79d0d82c..3f2fca50f114ebcb2a03b665d52bf47af61d6f5c 100644 (file)
--- a/src/theory/arith/soi_simplex.cpp
+++ b/src/theory/arith/soi_simplex.cpp
@@ -121,7 +121,10 @@ Result::Sat SumOfInfeasibilitiesSPD::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("soi::findModel") << "fcFindModel("<< instance <<") early conflict" << endl;
     Assert(d_conflictVariables.empty());
     return Result::UNSAT;
@@ -152,17 +155,27 @@ Result::Sat SumOfInfeasibilitiesSPD::findModel(bool exactResult){
 
     if(result ==  Result::UNSAT){
       ++(d_statistics.d_soiFoundUnsat);
-      if(verbose){ Message() << "fc found unsat";}
+      if (verbose)
+      {
+        CVC4Message() << "fc found unsat";
+      }
     }else if(d_errorSet.errorEmpty()){
       ++(d_statistics.d_soiFoundSat);
-      if(verbose){ Message() << "fc found model"; }
+      if (verbose)
+      {
+        CVC4Message() << "fc found model";
+      }
     }else{
       ++(d_statistics.d_soiMissed);
-      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());
@@ -373,12 +386,10 @@ void SumOfInfeasibilitiesSPD::updateAndSignal(const UpdateInfo& selected, Witnes
     }
     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;
     }
   }
 
@@ -424,9 +435,10 @@ void SumOfInfeasibilitiesSPD::updateAndSignal(const UpdateInfo& selected, Witnes
     }
   }
 
-  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")); }
 
@@ -982,8 +994,9 @@ Result::Sat SumOfInfeasibilitiesSPD::sumOfInfeasibilities(){
 
     Assert(d_errorSize == d_errorSet.errorSize());
 
-    if(verbose){
-      debugSOI(w,  Message(), instance);
+    if (verbose)
+    {
+      debugSOI(w, CVC4Message(), instance);
     }
     Assert(debugSOI(w, Debug("dualLike"), instance));
   }

diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 153b8e379c515c45527cf4ce8a7be804e4105756..74f2bdbd3d2b560d441d10b0a58c88dd9f37caa0 100644 (file)
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -3193,7 +3193,6 @@ bool TheoryArithPrivate::solveRealRelaxation(Theory::Effort effortLevel){
 //           int maxDepth =
 //             d_likelyIntegerInfeasible ? 1 : options::arithMaxBranchDepth();
 
-
 //           if(d_likelyIntegerInfeasible){
 //             d_qflraStatus = d_attemptSolSimplex.attempt(relaxSolution);
 //           }else{
@@ -3203,7 +3202,7 @@ bool TheoryArithPrivate::solveRealRelaxation(Theory::Effort effortLevel){
 //               mipRes = approxSolver->solveMIP(true);
 //             }
 //             d_errorSet.reduceToSignals();
-//             //Message() << "here" << endl;
+//             //CVC4Message() << "here" << endl;
 //             if(mipRes == ApproximateSimplex::ApproxSat){
 //               mipSolution = approxSolver->extractMIP();
 //               d_qflraStatus = d_attemptSolSimplex.attempt(mipSolution);
@@ -3219,13 +3218,15 @@ bool TheoryArithPrivate::solveRealRelaxation(Theory::Effort effortLevel){
 //             }
 //           }
 //           options::arithStandardCheckVarOrderPivots.set(pass2Limit);
-//           if(d_qflraStatus != Result::UNSAT){ d_qflraStatus = simplex.findModel(false); }
-//           //Message() << "done" << endl;
+//           if(d_qflraStatus != Result::UNSAT){ d_qflraStatus =
+//           simplex.findModel(false); }
+//           //CVC4Message() << "done" << endl;
 //         }
 //         break;
 //       case ApproximateSimplex::ApproxUnsat:
 //         {
-//           ApproximateSimplex::Solution sol = approxSolver->extractRelaxation();
+//           ApproximateSimplex::Solution sol =
+//           approxSolver->extractRelaxation();
 
 //           d_qflraStatus = d_attemptSolSimplex.attempt(sol);
 //           options::arithStandardCheckVarOrderPivots.set(pass2Limit);
@@ -3245,13 +3246,13 @@ bool TheoryArithPrivate::solveRealRelaxation(Theory::Effort effortLevel){
 //   }else{
 
 //     if(d_qflraStatus == Result::SAT_UNKNOWN){
-//       //Message() << "got sat unknown" << endl;
+//       //CVC4Message() << "got sat unknown" << endl;
 //       vector<ArithVar> toCut = cutAllBounded();
 //       if(toCut.size() > 0){
 //         //branchVector(toCut);
 //         emmittedConflictOrSplit = true;
 //       }else{
-//         //Message() << "splitting" << endl;
+//         //CVC4Message() << "splitting" << endl;
 
 //         d_qflraStatus = simplex.findModel(noPivotLimit);
 //       }

diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp
index 683dde688247d0a5747245a596956d5237e6611f..173803a7f08a3af2e8ff3158e79a084924269951 100644 (file)
--- a/src/theory/quantifiers/fmf/full_model_check.cpp
+++ b/src/theory/quantifiers/fmf/full_model_check.cpp
@@ -668,8 +668,8 @@ int FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, i
           Node ev = d_quant_models[f].evaluate(fmfmc, inst);
           if (ev == d_true)
           {
-            Message() << "WARNING: instantiation was true! " << f << " "
-                      << mcond[i] << std::endl;
+            CVC4Message() << "WARNING: instantiation was true! " << f << " "
+                          << mcond[i] << std::endl;
             AlwaysAssert(false);
           }
           else

diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp
index 0f5ada5491323505311842f9442dde89bd852714..6d9c82ac3f49a4c8c58971e42c46335fbdaef1df 100644 (file)
--- a/src/theory/quantifiers/quantifiers_attributes.cpp
+++ b/src/theory/quantifiers/quantifiers_attributes.cpp
@@ -176,7 +176,8 @@ void QuantAttributes::computeAttributes( Node q ) {
   {
     Node f = qa.d_fundef_f;
     if( d_fun_defs.find( f )!=d_fun_defs.end() ){
-      Message() << "Cannot define function " << f << " more than once." << std::endl;
+      CVC4Message() << "Cannot define function " << f << " more than once."
+                    << std::endl;
       AlwaysAssert(false);
     }
     d_fun_defs[f] = true;

diff --git a/src/theory/substitutions.cpp b/src/theory/substitutions.cpp
index 664fcd1b3716e92de4f862df6f238d006df7a28d..4c610ccfc79450f38f41539b9805d423d5fdae91 100644 (file)
--- a/src/theory/substitutions.cpp
+++ b/src/theory/substitutions.cpp
@@ -210,9 +210,7 @@ void SubstitutionMap::print(ostream& out) const {
   }
 }
 
-void SubstitutionMap::debugPrint() const {
-  print(Message.getStream());
-}
+void SubstitutionMap::debugPrint() const { print(CVC4Message.getStream()); }
 
 }/* CVC4::theory namespace */
 

diff --git a/src/theory/uf/cardinality_extension.cpp b/src/theory/uf/cardinality_extension.cpp
index b51e40a6c36eadcbd2f4571dc44f00ce12060095..ddf81c2e8625c525834e662fafd94e35491cb0c9 100644 (file)
--- a/src/theory/uf/cardinality_extension.cpp
+++ b/src/theory/uf/cardinality_extension.cpp
@@ -1014,8 +1014,9 @@ int SortModel::addSplit(Region* r)
       }else{
         Trace("uf-ss-warn") << "Split on unknown literal : " << ss << std::endl;
       }
-      if( ss==b_t ){
-        Message() << "Bad split " << s << std::endl;
+      if (ss == b_t)
+      {
+        CVC4Message() << "Bad split " << s << std::endl;
         AlwaysAssert(false);
       }
     }
@@ -1420,8 +1421,8 @@ void CardinalityExtension::assertNode(Node n, bool isDecision)
           for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
             if( !it->second->hasCardinalityAsserted() ){
               Trace("uf-ss-warn") << "WARNING: Assert " << n << " as a decision before cardinality for " << it->first << "." << std::endl;
-              //Message() << "Error: constraint asserted before cardinality for " << it->first << std::endl;
-              //Unimplemented();
+              // CVC4Message() << "Error: constraint asserted before cardinality
+              // for " << it->first << std::endl; Unimplemented();
             }
           }
         }

diff --git a/test/unit/util/output_black.h b/test/unit/util/output_black.h
index 5d6098060ff7c6a57b8980244509edd6745c75a0..00580de63da96a0df314ce2c8a677535c4406f0f 100644 (file)
--- a/test/unit/util/output_black.h
+++ b/test/unit/util/output_black.h
@@ -61,7 +61,7 @@ class OutputBlack : public CxxTest::TestSuite {
     Debug.on("foo");
     Debug("foo") << "testing3";
 
-    Message() << "a message";
+    CVC4Message() << "a message";
     Warning() << "bad warning!";
     Chat() << "chatty";
     Notice() << "note";
@@ -136,7 +136,7 @@ class OutputBlack : public CxxTest::TestSuite {
     TS_ASSERT( !( Debug.isOn("foo") ) );
     TS_ASSERT( !( Trace.isOn("foo") ) );
     TS_ASSERT( !( Warning.isOn() ) );
-    TS_ASSERT( !( Message.isOn() ) );
+    TS_ASSERT(!(CVC4Message.isOn()));
     TS_ASSERT( !( Notice.isOn() ) );
     TS_ASSERT( !( Chat.isOn() ) );
 
@@ -147,7 +147,7 @@ class OutputBlack : public CxxTest::TestSuite {
     cout << "warning" << std::endl;
     Warning() << failure() << endl;
     cout << "message" << std::endl;
-    Message() << failure() << endl;
+    CVC4Message() << failure() << endl;
     cout << "notice" << std::endl;
     Notice() << failure() << endl;
     cout << "chat" << std::endl;
@@ -185,7 +185,7 @@ class OutputBlack : public CxxTest::TestSuite {
     TS_ASSERT_EQUALS(d_chatStream.str(), string());
     d_chatStream.str("");
 
-    Message() << "baz foo";
+    CVC4Message() << "baz foo";
     TS_ASSERT_EQUALS(d_messageStream.str(), string());
     d_messageStream.str("");
 
@@ -229,7 +229,7 @@ class OutputBlack : public CxxTest::TestSuite {
     TS_ASSERT_EQUALS(d_chatStream.str(), string("baz foo"));
     d_chatStream.str("");
 
-    Message() << "baz foo";
+    CVC4Message() << "baz foo";
     TS_ASSERT_EQUALS(d_messageStream.str(), string("baz foo"));
     d_messageStream.str("");