diff options
22 files changed, 230 insertions, 147 deletions
diff --git a/src/base/output.h b/src/base/output.h index e23f62783..96cb9f8ac 100644 --- 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 ab2c8a218..9b0fc81be 100644 --- 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 03e77224b..b8a18aba8 100644 --- 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 30edf86cd..f174ed470 100644 --- 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 a4e7ac703..51434e369 100644 --- 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 c49de7372..27a90cb56 100644 --- 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 81e13c446..e028068ee 100644 --- 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 e2a482e30..fd33beec7 100644 --- 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 7c89a9e39..2432e6945 100644 --- 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 b8e08add8..22802b558 100644 --- 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 b0be108f7..03d9c50e9 100644 --- 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 15d6b9f50..15faf58bf 100644 --- 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 3d6e92283..4ac3034ff 100644 --- 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 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)); diff --git a/src/theory/arith/linear_equality.cpp b/src/theory/arith/linear_equality.cpp index 32d2714e8..765061e8d 100644 --- 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 ecac3d749..3f2fca50f 100644 --- 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 153b8e379..74f2bdbd3 100644 --- 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 683dde688..173803a7f 100644 --- 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 0f5ada549..6d9c82ac3 100644 --- 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 664fcd1b3..4c610ccfc 100644 --- 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 b51e40a6c..ddf81c2e8 100644 --- 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 5d6098060..00580de63 100644 --- 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(""); |