From 1909b36e01578099d7a773e561b4bec15c067580 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Fri, 5 Nov 2021 17:27:08 -0700 Subject: [PATCH] Remove `Notice()` in favor of new `verbose()` (#7588) This PR removes the remaining usages of the Notice() macros and uses verbose() instead. --- src/api/__pycache__/parsekinds.cpython-39.pyc | Bin 0 -> 4484 bytes src/base/output.cpp | 1 - src/base/output.h | 23 --- src/main/driver_unified.cpp | 1 - src/main/interactive_shell.cpp | 34 +++-- src/main/interactive_shell.h | 5 +- src/options/options_handler.cpp | 10 -- src/proof/proof_checker.cpp | 14 +- src/proof/proof_node_manager.cpp | 5 +- src/prop/minisat/minisat.cpp | 49 +++--- src/prop/minisat/minisat.h | 7 +- src/prop/prop_engine.cpp | 3 +- src/prop/sat_solver_factory.cpp | 4 +- src/prop/sat_solver_factory.h | 3 +- src/smt/check_models.cpp | 4 +- src/smt/set_defaults.cpp | 139 +++++++++--------- src/smt/set_defaults.h | 5 +- src/smt/solver_engine.cpp | 2 +- src/theory/strings/skolem_cache.cpp | 3 +- test/unit/theory/theory_arith_cad_white.cpp | 2 +- test/unit/util/output_black.cpp | 17 --- 21 files changed, 152 insertions(+), 179 deletions(-) create mode 100644 src/api/__pycache__/parsekinds.cpython-39.pyc diff --git a/src/api/__pycache__/parsekinds.cpython-39.pyc b/src/api/__pycache__/parsekinds.cpython-39.pyc new file mode 100644 index 0000000000000000000000000000000000000000..34d010ce4ea1b1b43af2c337e2fffe03b8ca7219 GIT binary patch literal 4484 zcmZu!&u<&Y72cU$QY(s7(3GfUXMEgatwCBG!fep!t8 zBf|AvG3t+sieHhAEM2qwF)`*>Mb*C~F8SkP+`lX?`x9cqpA?f~N?iFf_ov>s#I$(f z6HC1CocmYA)lI8*t@A}?Yd6ZgEL2fjdr_+$%a%-Z=6w()B3lnsCY5)%8-=@-HZ?L& z?@Di11_JN5qgZ<3)9|g?Oog*SJDLsK?OA%!+{5ttZUxq5-+1N)hk=q_x^0Zyd^y_o z?%wp;f!0zbUXTdyFp6U@+DTF+D`X<`gbZU065eB}52Z}J^I@cZ^JSTcX!~Z}ThU$^ zz($;`u;_ zIjeL=WpdCme(3PoS(IBHervWY(Fxw7f=`A0rqUaxU~bUxBgWvEl-Us{gS zKu5_=JB<<@(!7H|2aWeovY$an%V&r@mo~*ymLrZR0|lR0h&1Al=cqvZ@vI2MAI~v? z_~Tg>W1@;DB9DlU=VJqr3mI&m|ESJU7ErP~5ZZcfb*(1rJ-MKky+hIw46-CRWLa1+ zY&Vv3t2Uy@LS8bl$w$qjDbg@^5eS{`$s`{?uQf9rgnPLgB?b*yJ{<=dF=;-I({QgD zrY%AmLg8dG-u}C#reXT5KD(Q?;5@%KXJJ$w%H=sG>z7h>UG49(!rOQs>GW_{9 z>y#g}0>*f2pIRr5=BI4Ydd`lyuun=|w2qlBpNyPZi`K`}zv9RCu|pQRcGscN`|otg zy-x6oZCQOctt5s)){pcq{5rS3a>tWFxLf#?HtK=Xl!T*OL@vU(Tn1SL(mKdwrEiGn z3HmssV5wbD9|peD??pUcuY*_Gkq+XhBh94Spb_oGl1PiF%uIZkD&f5y2qw#FgBE{K_gcYTVGDiwoDK_%nHQ&rQiTCld5$MM->73d?KlXfH^eF+OaNth zeNgw!3*9~$6?*fJhIS4rhMUqvdh!{;4j3KU`||4A+}29t{q?n##ujL=aDHX$(bB@!+D3D3ak1x8+Jra%XikX1 zDd*PLS3hcQF0C5%Le*%_wcGL0ri=}*503aY51A3?9vTSY=F--KmBz!(fmg(-D*f{3-_D2z0))NTX5{Z$Q7K5-k}Gn*(G(JPVr z$JJv-N9@%4Bj0y63*H3{S1y2F<2kS2&Dr7C38Qi^jxr4*Yv138x&NYAo!f&vQJgu$ zHuZZTdfdqOQ8^!_h@oq4KGK7;qSPqo4>$9Y0e)V}urZxGPjG4G)t;6~N%9hoRx7KO z46Ef1q0283HZq^5JGq_6Z>)E0U^&0UOvME;Gr?w9g-@_?K1^~0+CwBqKBQtuPNUKV ztzEYS-{aYLevTZiXkP`f{SLkrPOtAr=qnZNqED2MaeJItV&s&aFyRszethHD?%H@a z3Nl1Zt#*0We%pd37cM>b@dhMV={)R*c|*3+r@d^9u88aix6CucbLM(IzijB(32=u# zP)X)JIRM{K0;lCO-M6JEGdN?jomZBgwSjSBL!IJK21*yiG3z}((B4j}z3*qAe}!M? z#*iwm{BJ6nPapiR>DMCtw?0{bf2A(ptftD@U0aMGUIk?i$K4raJfwYiPA&W=+_RD?Uzfnz> zVe_|LO#TFyVV7OA-bQ|A?4yNw|4J6sUr5pgNtTkbNz81rCvbLarOs#lIBxW!93Xv2 zV+p?1GKM#Cw;{o*o4g6Ryd*-V02g_-7kK1x4-}rHy56^jjGD4(Br<~1HZ)=bokWH* z%K~sc0HOgU5Vb<0H;lMe5UR9q%Rn;gHyc|95X;~J*CdS~vHZ&X>e|8w&4slG50-G< z%rCva(oj=~hq_E+0wOPi?0~g=a#(k%v6$QKw2d@~5*}5D@Jq(>*MU?mHeKYPe}G>0 z3WViW7?MU-W&jdOmAQ6>SJ)H^-tjVXcxPr1P=jWM;8cb+Duyclhl)02@thN!P8f0^ zt^p7L>|f^CJEzvMtxH`S0l(k1k%QYOWnDUDzXy0oBU{{`=~^cvU5rxe`!m`#y29k< zqs-d>g8H9~s(*KFT>+#tbjFO%pZfO33VSDJw&c6IYWhFx_g4q|G211Y4Vjn&%i~@9 z9>8~U8TARgEp-XxlU?VYg_)*|r5OO&YL4#DU@iRQ$|;g%^VQ%qa-58<+H~%uh+OU{ zd^wuKpYz75x()y2BfXI4&NfnF^%lKzml_WrG!a)dNlklgVLs{i^D+zI!F>2Dx_BTf3y!y3oJG^SJt>0)L+ z2i3b6>Dvnn^FH5PQ1{VN^fjiwM}lmt_ek6$@eYap#uR=0sudEH2&k7y(2BloskwWv gaMXQbgzQxaXSC{I#TS1Y?2pp>JC4m6|FT^EKW~e53;+NC literal 0 HcmV?d00001 diff --git a/src/base/output.cpp b/src/base/output.cpp index 2b77a3b2a..f9946c4a8 100644 --- a/src/base/output.cpp +++ b/src/base/output.cpp @@ -32,7 +32,6 @@ const int Cvc5ostream::s_indentIosIndex = std::ios_base::xalloc(); DebugC DebugChannel(&std::cout); WarningC WarningChannel(&std::cerr); MessageC MessageChannel(&std::cout); -NoticeC NoticeChannel(&null_os); TraceC TraceChannel(&std::cout); std::ostream DumpOutC::dump_cout(std::cout.rdbuf()); // copy cout stream buffer DumpOutC DumpOutChannel(&DumpOutC::dump_cout); diff --git a/src/base/output.h b/src/base/output.h index 2783f4bc6..dad354ad4 100644 --- a/src/base/output.h +++ b/src/base/output.h @@ -280,23 +280,6 @@ public: bool isOn() const { return d_os != &null_os; } }; /* class MessageC */ -/** The notice output class */ -class NoticeC -{ - std::ostream* d_os; - -public: - explicit NoticeC(std::ostream* os) : d_os(os) {} - - Cvc5ostream operator()() const { return Cvc5ostream(d_os); } - - std::ostream& setStream(std::ostream* os) { d_os = os; return *d_os; } - std::ostream& getStream() const { return *d_os; } - std::ostream* getStreamPointer() const { return d_os; } - - bool isOn() const { return d_os != &null_os; } -}; /* class NoticeC */ - /** The trace output class */ class TraceC { @@ -387,8 +370,6 @@ extern DebugC DebugChannel CVC5_EXPORT; extern WarningC WarningChannel CVC5_EXPORT; /** The message output singleton */ extern MessageC MessageChannel CVC5_EXPORT; -/** The notice output singleton */ -extern NoticeC NoticeChannel CVC5_EXPORT; /** The trace output singleton */ extern TraceC TraceChannel CVC5_EXPORT; /** The dump output singleton */ @@ -403,8 +384,6 @@ extern DumpOutC DumpOutChannel CVC5_EXPORT; ::cvc5::__cvc5_true() ? ::cvc5::nullStream : ::cvc5::WarningChannel #define CVC5Message \ ::cvc5::__cvc5_true() ? ::cvc5::nullStream : ::cvc5::MessageChannel -#define Notice \ - ::cvc5::__cvc5_true() ? ::cvc5::nullStream : ::cvc5::NoticeChannel #define Trace ::cvc5::__cvc5_true() ? ::cvc5::nullStream : ::cvc5::TraceChannel #define DumpOut \ ::cvc5::__cvc5_true() ? ::cvc5::nullStream : ::cvc5::DumpOutChannel @@ -425,8 +404,6 @@ extern DumpOutC DumpOutChannel CVC5_EXPORT; : ::cvc5::WarningChannel #define CVC5Message \ (!::cvc5::MessageChannel.isOn()) ? ::cvc5::nullStream : ::cvc5::MessageChannel -#define Notice \ - (!::cvc5::NoticeChannel.isOn()) ? ::cvc5::nullStream : ::cvc5::NoticeChannel #ifdef CVC5_TRACING #define Trace ::cvc5::TraceChannel #else /* CVC5_TRACING */ diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index 893a77cd9..e7f0a90b9 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -159,7 +159,6 @@ int runCvc5(int argc, char* argv[], std::unique_ptr& solver) if(Configuration::isMuzzledBuild()) { DebugChannel.setStream(&cvc5::null_os); TraceChannel.setStream(&cvc5::null_os); - NoticeChannel.setStream(&cvc5::null_os); MessageChannel.setStream(&cvc5::null_os); WarningChannel.setStream(&cvc5::null_os); } diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp index c178a637c..1a0795ddc 100644 --- a/src/main/interactive_shell.cpp +++ b/src/main/interactive_shell.cpp @@ -89,7 +89,7 @@ InteractiveShell::InteractiveShell(api::Solver* solver, { ParserBuilder parserBuilder(solver, sm, true); /* Create parser with bogus input. */ - d_parser = parserBuilder.build(); + d_parser.reset(parserBuilder.build()); if (d_solver->getOptionInfo("force-logic").setByUser) { LogicInfo tmp(d_solver->getOption("force-logic")); @@ -129,13 +129,16 @@ InteractiveShell::InteractiveShell(api::Solver* solver, d_usingEditline = true; int err = ::read_history(d_historyFilename.c_str()); ::stifle_history(s_historyLimit); - if(Notice.isOn()) { + if (d_solver->getOptionInfo("verbosity").intValue() >= 1) + { if(err == 0) { - Notice() << "Read " << ::history_length << " lines of history from " - << d_historyFilename << std::endl; + d_solver->getDriverOptions().err() + << "Read " << ::history_length << " lines of history from " + << d_historyFilename << std::endl; } else { - Notice() << "Could not read history from " << d_historyFilename - << ": " << strerror(err) << std::endl; + d_solver->getDriverOptions().err() + << "Could not read history from " << d_historyFilename << ": " + << strerror(err) << std::endl; } } } @@ -151,15 +154,20 @@ InteractiveShell::InteractiveShell(api::Solver* solver, InteractiveShell::~InteractiveShell() { #if HAVE_LIBEDITLINE int err = ::write_history(d_historyFilename.c_str()); - if(err == 0) { - Notice() << "Wrote " << ::history_length << " lines of history to " - << d_historyFilename << std::endl; - } else { - Notice() << "Could not write history to " << d_historyFilename - << ": " << strerror(err) << std::endl; + if (d_solver->getOptionInfo("verbosity").intValue() >= 1) + { + if (err == 0) + { + d_solver->getDriverOptions().err() + << "Wrote " << ::history_length << " lines of history to " + << d_historyFilename << std::endl; + } else { + d_solver->getDriverOptions().err() + << "Could not write history to " << d_historyFilename << ": " + << strerror(err) << std::endl; + } } #endif /* HAVE_LIBEDITLINE */ - delete d_parser; } Command* InteractiveShell::readCommand() diff --git a/src/main/interactive_shell.h b/src/main/interactive_shell.h index 6029d6b0e..401f7a1c9 100644 --- a/src/main/interactive_shell.h +++ b/src/main/interactive_shell.h @@ -17,6 +17,7 @@ #define CVC5__INTERACTIVE_SHELL_H #include +#include #include namespace cvc5 { @@ -55,13 +56,13 @@ class InteractiveShell /** * Return the internal parser being used. */ - parser::Parser* getParser() { return d_parser; } + parser::Parser* getParser() { return d_parser.get(); } private: api::Solver* d_solver; std::istream& d_in; std::ostream& d_out; - parser::Parser* d_parser; + std::unique_ptr d_parser; bool d_quit; bool d_usingEditline; diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index 060b7eeba..5adce0a4f 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -75,7 +75,6 @@ void OptionsHandler::setErrStream(const std::string& flag, const ManagedErr& me) Debug.setStream(me); Warning.setStream(me); CVC5Message.setStream(me); - Notice.setStream(me); Trace.setStream(me); } @@ -134,15 +133,9 @@ void OptionsHandler::setVerbosity(const std::string& flag, int value) if(Configuration::isMuzzledBuild()) { DebugChannel.setStream(&cvc5::null_os); TraceChannel.setStream(&cvc5::null_os); - NoticeChannel.setStream(&cvc5::null_os); MessageChannel.setStream(&cvc5::null_os); WarningChannel.setStream(&cvc5::null_os); } else { - if(value < 1) { - NoticeChannel.setStream(&cvc5::null_os); - } else { - NoticeChannel.setStream(&std::cout); - } if(value < 0) { MessageChannel.setStream(&cvc5::null_os); WarningChannel.setStream(&cvc5::null_os); @@ -269,7 +262,6 @@ void OptionsHandler::setPrintSuccess(const std::string& flag, bool value) { Debug.getStream() << Command::printsuccess(value); Trace.getStream() << Command::printsuccess(value); - Notice.getStream() << Command::printsuccess(value); CVC5Message.getStream() << Command::printsuccess(value); Warning.getStream() << Command::printsuccess(value); *d_options->base.out << Command::printsuccess(value); @@ -352,7 +344,6 @@ void OptionsHandler::setDefaultExprDepth(const std::string& flag, int depth) { Debug.getStream() << expr::ExprSetDepth(depth); Trace.getStream() << expr::ExprSetDepth(depth); - Notice.getStream() << expr::ExprSetDepth(depth); CVC5Message.getStream() << expr::ExprSetDepth(depth); Warning.getStream() << expr::ExprSetDepth(depth); } @@ -361,7 +352,6 @@ void OptionsHandler::setDefaultDagThresh(const std::string& flag, int dag) { Debug.getStream() << expr::ExprDag(dag); Trace.getStream() << expr::ExprDag(dag); - Notice.getStream() << expr::ExprDag(dag); CVC5Message.getStream() << expr::ExprDag(dag); Warning.getStream() << expr::ExprDag(dag); } diff --git a/src/proof/proof_checker.cpp b/src/proof/proof_checker.cpp index 28a09fc9c..c178ccebf 100644 --- a/src/proof/proof_checker.cpp +++ b/src/proof/proof_checker.cpp @@ -207,7 +207,7 @@ Node ProofChecker::checkInternal(PfRule id, { if (useTrustedChecker) { - Notice() << "ProofChecker::check: trusting PfRule " << id << std::endl; + out << "ProofChecker::check: trusting PfRule " << id << std::endl; // trusted checker return expected; } @@ -275,8 +275,9 @@ void ProofChecker::registerChecker(PfRule id, ProofRuleChecker* psc) if (it != d_checker.end()) { // checker is already provided - Notice() << "ProofChecker::registerChecker: checker already exists for " - << id << std::endl; + Trace("pfcheck") + << "ProofChecker::registerChecker: checker already exists for " << id + << std::endl; return; } d_checker[id] = psc; @@ -293,9 +294,10 @@ void ProofChecker::registerTrustedChecker(PfRule id, // overwrites if already there if (d_plevel.find(id) != d_plevel.end()) { - Notice() << "ProofChecker::registerTrustedRule: already provided pedantic " - "level for " - << id << std::endl; + Trace("proof-pedantic") + << "ProofChecker::registerTrustedRule: already provided pedantic " + "level for " + << id << std::endl; } d_plevel[id] = plevel; } diff --git a/src/proof/proof_node_manager.cpp b/src/proof/proof_node_manager.cpp index 8b4b332a1..72c39c59f 100644 --- a/src/proof/proof_node_manager.cpp +++ b/src/proof/proof_node_manager.cpp @@ -237,8 +237,9 @@ std::shared_ptr ProofNodeManager::mkScope( { if (acu.find(a) == acu.end()) { - Notice() << "ProofNodeManager::mkScope: assumption " << a - << " does not match a free assumption in proof" << std::endl; + Trace("pnm") << "ProofNodeManager::mkScope: assumption " << a + << " does not match a free assumption in proof" + << std::endl; } } } diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp index e193bfb28..a681aa4f1 100644 --- a/src/prop/minisat/minisat.cpp +++ b/src/prop/minisat/minisat.cpp @@ -30,8 +30,12 @@ namespace prop { //// DPllMinisatSatSolver -MinisatSatSolver::MinisatSatSolver(StatisticsRegistry& registry) - : d_minisat(NULL), d_context(NULL), d_assumptions(), d_statistics(registry) +MinisatSatSolver::MinisatSatSolver(Env& env, StatisticsRegistry& registry) + : EnvObj(env), + d_minisat(NULL), + d_context(NULL), + d_assumptions(), + d_statistics(registry) {} MinisatSatSolver::~MinisatSatSolver() @@ -108,20 +112,22 @@ void MinisatSatSolver::initialize(context::Context* context, { d_context = context; - if (options::decisionMode() != options::DecisionMode::INTERNAL) + if (options().decision.decisionMode != options::DecisionMode::INTERNAL) { - Notice() << "minisat: Incremental solving is forced on (to avoid variable elimination)" - << " unless using internal decision strategy." << std::endl; + verbose(1) << "minisat: Incremental solving is forced on (to avoid " + "variable elimination)" + << " unless using internal decision strategy." << std::endl; } // Create the solver - d_minisat = new Minisat::SimpSolver( - theoryProxy, - d_context, - userContext, - pnm, - options::incrementalSolving() - || options::decisionMode() != options::DecisionMode::INTERNAL); + d_minisat = + new Minisat::SimpSolver(theoryProxy, + d_context, + userContext, + pnm, + options().base.incrementalSolving + || options().decision.decisionMode + != options::DecisionMode::INTERNAL); d_statistics.init(d_minisat); } @@ -132,20 +138,21 @@ void MinisatSatSolver::setupOptions() { // Copy options from cvc5 options structure into minisat, as appropriate // Set up the verbosity - d_minisat->verbosity = (options::verbosity() > 0) ? 1 : -1; + d_minisat->verbosity = (options().base.verbosity > 0) ? 1 : -1; // Set up the random decision parameters - d_minisat->random_var_freq = options::satRandomFreq(); + d_minisat->random_var_freq = options().prop.satRandomFreq; // If 0, we use whatever we like (here, the Minisat default seed) - if(options::satRandomSeed() != 0) { - d_minisat->random_seed = double(options::satRandomSeed()); + if (options().prop.satRandomSeed != 0) + { + d_minisat->random_seed = double(options().prop.satRandomSeed); } // Give access to all possible options in the sat solver - d_minisat->var_decay = options::satVarDecay(); - d_minisat->clause_decay = options::satClauseDecay(); - d_minisat->restart_first = options::satRestartFirst(); - d_minisat->restart_inc = options::satRestartInc(); + d_minisat->var_decay = options().prop.satVarDecay; + d_minisat->clause_decay = options().prop.satClauseDecay; + d_minisat->restart_first = options().prop.satRestartFirst; + d_minisat->restart_inc = options().prop.satRestartInc; } ClauseId MinisatSatSolver::addClause(SatClause& clause, bool removable) { @@ -159,7 +166,7 @@ ClauseId MinisatSatSolver::addClause(SatClause& clause, bool removable) { } d_minisat->addClause(minisat_clause, removable, clause_id); // FIXME: to be deleted when we kill old proof code for unsat cores - Assert(!options::unsatCores() || options::produceProofs() + Assert(!options().smt.unsatCores || options().smt.produceProofs || clause_id != ClauseIdError); return clause_id; } diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h index 984cc6479..ef2cca6f0 100644 --- a/src/prop/minisat/minisat.h +++ b/src/prop/minisat/minisat.h @@ -17,8 +17,9 @@ #pragma once -#include "prop/sat_solver.h" #include "prop/minisat/simp/SimpSolver.h" +#include "prop/sat_solver.h" +#include "smt/env_obj.h" #include "util/statistics_registry.h" namespace cvc5 { @@ -32,10 +33,10 @@ void toSatClause(const typename Solver::TClause& minisat_cl, namespace prop { -class MinisatSatSolver : public CDCLTSatSolverInterface +class MinisatSatSolver : public CDCLTSatSolverInterface, protected EnvObj { public: - MinisatSatSolver(StatisticsRegistry& registry); + MinisatSatSolver(Env& env, StatisticsRegistry& registry); ~MinisatSatSolver() override; static SatVariable toSatVariable(Minisat::Var var); diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 0e911a495..eeca414e2 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -99,7 +99,8 @@ PropEngine::PropEngine(TheoryEngine* te, Env& env) d_decisionEngine.reset(new decision::DecisionEngineEmpty(env)); } - d_satSolver = SatSolverFactory::createCDCLTMinisat(smtStatisticsRegistry()); + d_satSolver = + SatSolverFactory::createCDCLTMinisat(d_env, smtStatisticsRegistry()); // CNF stream and theory proxy required pointers to each other, make the // theory proxy first diff --git a/src/prop/sat_solver_factory.cpp b/src/prop/sat_solver_factory.cpp index 7852fc4e7..dfd660ace 100644 --- a/src/prop/sat_solver_factory.cpp +++ b/src/prop/sat_solver_factory.cpp @@ -24,9 +24,9 @@ namespace cvc5 { namespace prop { MinisatSatSolver* SatSolverFactory::createCDCLTMinisat( - StatisticsRegistry& registry) + Env& env, StatisticsRegistry& registry) { - return new MinisatSatSolver(registry); + return new MinisatSatSolver(env, registry); } SatSolver* SatSolverFactory::createCryptoMinisat(StatisticsRegistry& registry, diff --git a/src/prop/sat_solver_factory.h b/src/prop/sat_solver_factory.h index c997a1ab8..fce8e31e2 100644 --- a/src/prop/sat_solver_factory.h +++ b/src/prop/sat_solver_factory.h @@ -32,7 +32,8 @@ namespace prop { class SatSolverFactory { public: - static MinisatSatSolver* createCDCLTMinisat(StatisticsRegistry& registry); + static MinisatSatSolver* createCDCLTMinisat(Env& env, + StatisticsRegistry& registry); static SatSolver* createCryptoMinisat(StatisticsRegistry& registry, const std::string& name = ""); diff --git a/src/smt/check_models.cpp b/src/smt/check_models.cpp index d7f654fc6..7d546eae7 100644 --- a/src/smt/check_models.cpp +++ b/src/smt/check_models.cpp @@ -36,10 +36,10 @@ void CheckModels::checkModel(TheoryModel* m, const context::CDList& al, bool hardFailure) { - // Throughout, we use Notice() to give diagnostic output. + // Throughout, we use verbose(1) to give diagnostic output. // // If this function is running, the user gave --check-model (or equivalent), - // and if Notice() is on, the user gave --verbose (or equivalent). + // and if verbose(1) is on, the user gave --verbose (or equivalent). // check-model is not guaranteed to succeed if approximate values were used. // Thus, we intentionally abort here. diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index 195f9e76d..895e41c96 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -46,8 +46,8 @@ using namespace cvc5::theory; namespace cvc5 { namespace smt { -SetDefaults::SetDefaults(bool isInternalSubsolver) - : d_isInternalSubsolver(isInternalSubsolver) +SetDefaults::SetDefaults(Env& env, bool isInternalSubsolver) + : EnvObj(env), d_isInternalSubsolver(isInternalSubsolver) { } @@ -100,7 +100,7 @@ void SetDefaults::setDefaultsPre(Options& opts) { if (opts.smt.unsatCoresModeWasSetByUser) { - Notice() + verbose(1) << "Overriding OFF unsat-core mode since cores were requested.\n"; } opts.smt.unsatCoresMode = options::UnsatCoresMode::ASSUMPTIONS; @@ -116,8 +116,8 @@ void SetDefaults::setDefaultsPre(Options& opts) { if (opts.smt.unsatCoresModeWasSetByUser) { - Notice() << "Forcing full-proof mode for unsat cores mode since proofs " - "were requested.\n"; + verbose(1) << "Forcing full-proof mode for unsat cores mode since proofs " + "were requested.\n"; } // enable unsat cores, because they are available as a consequence of proofs opts.smt.unsatCores = true; @@ -129,7 +129,7 @@ void SetDefaults::setDefaultsPre(Options& opts) { if (opts.smt.produceProofsWasSetByUser) { - Notice() + verbose(1) << "Forcing proof production since new unsat cores were requested.\n"; } opts.smt.produceProofs = true; @@ -158,8 +158,8 @@ void SetDefaults::setDefaultsPre(Options& opts) { opts.smt.unsatCores = false; opts.smt.unsatCoresMode = options::UnsatCoresMode::OFF; - Notice() << "SolverEngine: turning off produce-proofs due to " - << reasonNoProofs.str() << "." << std::endl; + verbose(1) << "SolverEngine: turning off produce-proofs due to " + << reasonNoProofs.str() << "." << std::endl; opts.smt.produceProofs = false; opts.smt.checkProofs = false; } @@ -207,7 +207,7 @@ void SetDefaults::finalizeLogic(LogicInfo& logic, Options& opts) const "for the combination of bit-vectors with arrays or uinterpreted " "functions. Try --bitblast=lazy")); } - Notice() + verbose(1) << "SolverEngine: setting bit-blast mode to lazy to support model" << "generation" << std::endl; opts.bv.bitblastMode = options::BitblastMode::LAZY; @@ -266,8 +266,8 @@ void SetDefaults::finalizeLogic(LogicInfo& logic, Options& opts) const throw OptionException(std::string( "Ackermannization currently does not support model generation.")); } - Notice() << "SolverEngine: turn off ackermannization to support model" - << "generation" << std::endl; + verbose(1) << "SolverEngine: turn off ackermannization to support model" + << "generation" << std::endl; opts.smt.ackermann = false; } @@ -377,8 +377,8 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const || opts.smt.produceProofs) && !opts.smt.produceAssertions) { - Notice() << "SolverEngine: turning on produce-assertions to support " - << "option requiring assertions." << std::endl; + verbose(1) << "SolverEngine: turning on produce-assertions to support " + << "option requiring assertions." << std::endl; opts.smt.produceAssertions = true; } @@ -465,7 +465,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const "bool-to-bv != off not supported with CBQI BV for quantified " "logics"); } - Notice() + verbose(1) << "SolverEngine: turning off bool-to-bitvector to support CBQI BV" << std::endl; opts.bv.boolToBitvector = options::BoolToBVMode::OFF; @@ -477,7 +477,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const && (opts.smt.produceAssignments || opts.quantifiers.sygusRewSynthCheck || usesSygus(opts))) { - Notice() << "SolverEngine: turning on produce-models" << std::endl; + verbose(1) << "SolverEngine: turning on produce-models" << std::endl; opts.smt.produceModels = true; } @@ -582,8 +582,8 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const throw OptionException( "bool-to-bv=all not supported for non-bitvector logics."); } - Notice() << "SolverEngine: turning off bool-to-bv for non-bv logic: " - << logic.getLogicString() << std::endl; + verbose(1) << "SolverEngine: turning off bool-to-bv for non-bv logic: " + << logic.getLogicString() << std::endl; opts.bv.boolToBitvector = options::BoolToBVMode::OFF; } @@ -759,8 +759,8 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const ss << "Cannot use " << sOptNoModel << " with model generation."; throw OptionException(ss.str()); } - Notice() << "SolverEngine: turning off produce-models to support " - << sOptNoModel << std::endl; + verbose(1) << "SolverEngine: turning off produce-models to support " + << sOptNoModel << std::endl; opts.smt.produceModels = false; } if (opts.smt.produceAssignments) @@ -772,8 +772,8 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const << " with model generation (produce-assignments)."; throw OptionException(ss.str()); } - Notice() << "SolverEngine: turning off produce-assignments to support " - << sOptNoModel << std::endl; + verbose(1) << "SolverEngine: turning off produce-assignments to support " + << sOptNoModel << std::endl; opts.smt.produceAssignments = false; } if (opts.smt.checkModels) @@ -785,8 +785,8 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const << " with model generation (check-models)."; throw OptionException(ss.str()); } - Notice() << "SolverEngine: turning off check-models to support " - << sOptNoModel << std::endl; + verbose(1) << "SolverEngine: turning off check-models to support " + << sOptNoModel << std::endl; opts.smt.checkModels = false; } } @@ -840,8 +840,8 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const } else { - Notice() << "Cannot use --nl-cad without configuring with --poly." - << std::endl; + verbose(1) << "Cannot use --nl-cad without configuring with --poly." + << std::endl; opts.arith.nlCad = false; opts.arith.nlExt = options::NlExtMode::FULL; } @@ -903,7 +903,7 @@ bool SetDefaults::incompatibleWithProofs(Options& opts, // options that are automatically set to support proofs if (opts.bv.bvAssertInput) { - Notice() + verbose(1) << "Disabling bv-assert-input since it is incompatible with proofs." << std::endl; opts.bv.bvAssertInput = false; @@ -913,8 +913,8 @@ bool SetDefaults::incompatibleWithProofs(Options& opts, if (opts.bv.bvSolver != options::BVSolver::BITBLAST_INTERNAL && !opts.bv.bvSolverWasSetByUser) { - Notice() << "Forcing internal bit-vector solver due to proof production." - << std::endl; + verbose(1) << "Forcing internal bit-vector solver due to proof production." + << std::endl; opts.bv.bvSolver = options::BVSolver::BITBLAST_INTERNAL; } return false; @@ -963,9 +963,9 @@ bool SetDefaults::incompatibleWithIncremental(const LogicInfo& logic, reason << "unconstrained simplification"; return true; } - Notice() << "SolverEngine: turning off unconstrained simplification to " - "support incremental solving" - << std::endl; + verbose(1) << "SolverEngine: turning off unconstrained simplification to " + "support incremental solving" + << std::endl; opts.smt.unconstrainedSimp = false; } if (opts.bv.bitblastMode == options::BitblastMode::EAGER @@ -982,9 +982,9 @@ bool SetDefaults::incompatibleWithIncremental(const LogicInfo& logic, reason << "sygus inference"; return true; } - Notice() << "SolverEngine: turning off sygus inference to support " - "incremental solving" - << std::endl; + verbose(1) << "SolverEngine: turning off sygus inference to support " + "incremental solving" + << std::endl; opts.quantifiers.sygusInference = false; } if (opts.quantifiers.sygusInst) @@ -994,9 +994,9 @@ bool SetDefaults::incompatibleWithIncremental(const LogicInfo& logic, reason << "sygus inst"; return true; } - Notice() << "SolverEngine: turning off sygus inst to support " - "incremental solving" - << std::endl; + verbose(1) << "SolverEngine: turning off sygus inst to support " + "incremental solving" + << std::endl; opts.quantifiers.sygusInst = false; } if (opts.smt.solveIntAsBV > 0) @@ -1025,9 +1025,9 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts, reason << "simplification"; return true; } - Notice() << "SolverEngine: turning off simplification to support unsat " - "cores" - << std::endl; + verbose(1) << "SolverEngine: turning off simplification to support unsat " + "cores" + << std::endl; opts.smt.simplificationMode = options::SimplificationMode::NONE; } @@ -1038,8 +1038,8 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts, reason << "learned rewrites"; return true; } - Notice() << "SolverEngine: turning off learned rewrites to support " - "unsat cores\n"; + verbose(1) << "SolverEngine: turning off learned rewrites to support " + "unsat cores\n"; opts.smt.learnedRewrite = false; } @@ -1050,8 +1050,8 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts, reason << "pseudoboolean rewrites"; return true; } - Notice() << "SolverEngine: turning off pseudoboolean rewrites to support " - "unsat cores\n"; + verbose(1) << "SolverEngine: turning off pseudoboolean rewrites to support " + "unsat cores\n"; opts.arith.pbRewrites = false; } @@ -1062,8 +1062,8 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts, reason << "sort inference"; return true; } - Notice() << "SolverEngine: turning off sort inference to support unsat " - "cores\n"; + verbose(1) << "SolverEngine: turning off sort inference to support unsat " + "cores\n"; opts.smt.sortInference = false; } @@ -1074,8 +1074,8 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts, reason << "pre-skolemization"; return true; } - Notice() << "SolverEngine: turning off pre-skolemization to support " - "unsat cores\n"; + verbose(1) << "SolverEngine: turning off pre-skolemization to support " + "unsat cores\n"; opts.quantifiers.preSkolemQuant = false; } @@ -1086,8 +1086,8 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts, reason << "bv-to-bool"; return true; } - Notice() << "SolverEngine: turning off bitvector-to-bool to support " - "unsat cores\n"; + verbose(1) << "SolverEngine: turning off bitvector-to-bool to support " + "unsat cores\n"; opts.bv.bitvectorToBool = false; } @@ -1098,7 +1098,8 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts, reason << "bool-to-bv != off"; return true; } - Notice() << "SolverEngine: turning off bool-to-bv to support unsat cores\n"; + verbose(1) + << "SolverEngine: turning off bool-to-bv to support unsat cores\n"; opts.bv.boolToBitvector = options::BoolToBVMode::OFF; } @@ -1109,7 +1110,7 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts, reason << "bv-intro-pow2"; return true; } - Notice() + verbose(1) << "SolverEngine: turning off bv-intro-pow2 to support unsat cores"; opts.bv.bvIntroducePow2 = false; } @@ -1121,7 +1122,7 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts, reason << "repeat-simp"; return true; } - Notice() + verbose(1) << "SolverEngine: turning off repeat-simp to support unsat cores\n"; opts.smt.repeatSimp = false; } @@ -1133,8 +1134,8 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts, reason << "global-negate"; return true; } - Notice() << "SolverEngine: turning off global-negate to support unsat " - "cores\n"; + verbose(1) << "SolverEngine: turning off global-negate to support unsat " + "cores\n"; opts.quantifiers.globalNegate = false; } @@ -1150,9 +1151,9 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts, reason << "unconstrained simplification"; return true; } - Notice() << "SolverEngine: turning off unconstrained simplification to " - "support unsat cores" - << std::endl; + verbose(1) << "SolverEngine: turning off unconstrained simplification to " + "support unsat cores" + << std::endl; opts.smt.unconstrainedSimp = false; } return false; @@ -1197,7 +1198,7 @@ void SetDefaults::widenLogic(LogicInfo& logic, const Options& opts) const needsUf = true; if (!logic.isTheoryEnabled(THEORY_ARITH) || logic.isDifferenceLogic()) { - Notice() + verbose(1) << "Enabling linear integer arithmetic because strings are enabled" << std::endl; log.enableTheory(THEORY_ARITH); @@ -1206,8 +1207,8 @@ void SetDefaults::widenLogic(LogicInfo& logic, const Options& opts) const } else if (!logic.areIntegersUsed()) { - Notice() << "Enabling integer arithmetic because strings are enabled" - << std::endl; + verbose(1) << "Enabling integer arithmetic because strings are enabled" + << std::endl; log.enableIntegers(); } logic = log; @@ -1218,8 +1219,8 @@ void SetDefaults::widenLogic(LogicInfo& logic, const Options& opts) const { // if pre-skolem nested is explictly set, then we require UF. If it is // not explicitly set, it is disabled below if UF is not present. - Notice() << "Enabling UF because preSkolemQuantNested requires it." - << std::endl; + verbose(1) << "Enabling UF because preSkolemQuantNested requires it." + << std::endl; needsUf = true; } if (needsUf @@ -1245,8 +1246,8 @@ void SetDefaults::widenLogic(LogicInfo& logic, const Options& opts) const LogicInfo log(logic.getUnlockedCopy()); if (!needsUf) { - Notice() << "Enabling UF because " << logic << " requires it." - << std::endl; + verbose(1) << "Enabling UF because " << logic << " requires it." + << std::endl; } log.enableTheory(THEORY_UF); logic = log; @@ -1259,8 +1260,8 @@ void SetDefaults::widenLogic(LogicInfo& logic, const Options& opts) const { // enable integers LogicInfo log(logic.getUnlockedCopy()); - Notice() << "Enabling integers because arithMLTrick requires it." - << std::endl; + verbose(1) << "Enabling integers because arithMLTrick requires it." + << std::endl; log.enableIntegers(); logic = log; logic.lock(); @@ -1288,8 +1289,8 @@ void SetDefaults::setDefaultsQuantifiers(const LogicInfo& logic, if (opts.quantifiers.instMaxLevel != -1) { - Notice() << "SolverEngine: turning off cbqi to support instMaxLevel" - << std::endl; + verbose(1) << "SolverEngine: turning off cbqi to support instMaxLevel" + << std::endl; opts.quantifiers.cegqi = false; } diff --git a/src/smt/set_defaults.h b/src/smt/set_defaults.h index 31e2c3e41..24b39e205 100644 --- a/src/smt/set_defaults.h +++ b/src/smt/set_defaults.h @@ -17,6 +17,7 @@ #define CVC5__SMT__SET_DEFAULTS_H #include "options/options.h" +#include "smt/env_obj.h" #include "theory/logic_info.h" namespace cvc5 { @@ -26,14 +27,14 @@ namespace smt { * Class responsible for setting default options, which includes managing * implied options and dependencies between the options and the logic. */ -class SetDefaults +class SetDefaults : protected EnvObj { public: /** * @param isInternalSubsolver Whether we are setting the options for an * internal subsolver (see SolverEngine::isInternalSubsolver). */ - SetDefaults(bool isInternalSubsolver); + SetDefaults(Env& env, bool isInternalSubsolver); /** * The purpose of this method is to set the default options and update the * logic info for an SMT engine. diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp index 12a86d569..6dc40ac8b 100644 --- a/src/smt/solver_engine.cpp +++ b/src/smt/solver_engine.cpp @@ -179,7 +179,7 @@ void SolverEngine::finishInit() // Call finish init on the set defaults module. This inializes the logic // and the best default options based on our heuristics. - SetDefaults sdefaults(d_isInternalSubsolver); + SetDefaults sdefaults(*d_env, d_isInternalSubsolver); sdefaults.setDefaults(d_env->d_logic, getOptions()); if (d_env->getOptions().smt.produceProofs) diff --git a/src/theory/strings/skolem_cache.cpp b/src/theory/strings/skolem_cache.cpp index fc68ddfc4..dd4093e30 100644 --- a/src/theory/strings/skolem_cache.cpp +++ b/src/theory/strings/skolem_cache.cpp @@ -133,7 +133,8 @@ Node SkolemCache::mkTypedSkolemCached( break; default: { - Notice() << "Don't know how to handle Skolem ID " << id << std::endl; + Trace("skolem-cache") + << "Don't know how to handle Skolem ID " << id << std::endl; Node v = nm->mkBoundVar(tn); Node cond = nm->mkConst(true); sk = sm->mkSkolem(v, cond, c, "string skolem"); diff --git a/test/unit/theory/theory_arith_cad_white.cpp b/test/unit/theory/theory_arith_cad_white.cpp index 4d6bade95..719b76cab 100644 --- a/test/unit/theory/theory_arith_cad_white.cpp +++ b/test/unit/theory/theory_arith_cad_white.cpp @@ -349,7 +349,7 @@ void test_delta(const std::vector& a) std::cout << "Collected MIS: " << mis << std::endl; Assert(!mis.empty()) << "Infeasible subset can not be empty"; Node lem = NodeManager::currentNM()->mkAnd(mis).negate(); - Notice() << "UNSAT with MIS: " << lem << std::endl; + std::cout << "UNSAT with MIS: " << lem << std::endl; } } diff --git a/test/unit/util/output_black.cpp b/test/unit/util/output_black.cpp index e1d803227..72067c496 100644 --- a/test/unit/util/output_black.cpp +++ b/test/unit/util/output_black.cpp @@ -30,13 +30,11 @@ class TestUtilBlackOutput : public TestInternal TestInternal::SetUp(); DebugChannel.setStream(&d_debugStream); TraceChannel.setStream(&d_traceStream); - NoticeChannel.setStream(&d_noticeStream); MessageChannel.setStream(&d_messageStream); WarningChannel.setStream(&d_warningStream); d_debugStream.str(""); d_traceStream.str(""); - d_noticeStream.str(""); d_messageStream.str(""); d_warningStream.str(""); } @@ -52,7 +50,6 @@ class TestUtilBlackOutput : public TestInternal } std::stringstream d_debugStream; std::stringstream d_traceStream; - std::stringstream d_noticeStream; std::stringstream d_messageStream; std::stringstream d_warningStream; }; @@ -68,7 +65,6 @@ TEST_F(TestUtilBlackOutput, output) CVC5Message() << "a message"; Warning() << "bad warning!"; - Notice() << "note"; Trace.on("foo"); Trace("foo") << "tracing1"; @@ -82,7 +78,6 @@ TEST_F(TestUtilBlackOutput, output) ASSERT_EQ(d_debugStream.str(), ""); ASSERT_EQ(d_messageStream.str(), ""); ASSERT_EQ(d_warningStream.str(), ""); - ASSERT_EQ(d_noticeStream.str(), ""); ASSERT_EQ(d_traceStream.str(), ""); #else /* CVC5_MUZZLE */ @@ -95,7 +90,6 @@ TEST_F(TestUtilBlackOutput, output) ASSERT_EQ(d_messageStream.str(), "a message"); ASSERT_EQ(d_warningStream.str(), "bad warning!"); - ASSERT_EQ(d_noticeStream.str(), "note"); #ifdef CVC5_TRACING ASSERT_EQ(d_traceStream.str(), "tracing1tracing3"); @@ -131,7 +125,6 @@ TEST_F(TestUtilBlackOutput, evaluation_off_when_it_is_supposed_to_be) ASSERT_FALSE(Trace.isOn("foo")); ASSERT_FALSE(Warning.isOn()); ASSERT_FALSE(CVC5Message.isOn()); - ASSERT_FALSE(Notice.isOn()); cout << "debug" << std::endl; Debug("foo") << failure() << std::endl; @@ -141,8 +134,6 @@ TEST_F(TestUtilBlackOutput, evaluation_off_when_it_is_supposed_to_be) Warning() << failure() << std::endl; cout << "message" << std::endl; CVC5Message() << failure() << std::endl; - cout << "notice" << std::endl; - Notice() << failure() << std::endl; #endif } @@ -176,10 +167,6 @@ TEST_F(TestUtilBlackOutput, simple_print) ASSERT_EQ(d_messageStream.str(), std::string()); d_messageStream.str(""); - Notice() << "baz foo"; - ASSERT_EQ(d_noticeStream.str(), std::string()); - d_noticeStream.str(""); - #else /* CVC5_MUZZLE */ Debug.off("yo"); @@ -216,10 +203,6 @@ TEST_F(TestUtilBlackOutput, simple_print) ASSERT_EQ(d_messageStream.str(), std::string("baz foo")); d_messageStream.str(""); - Notice() << "baz foo"; - ASSERT_EQ(d_noticeStream.str(), std::string("baz foo")); - d_noticeStream.str(""); - #endif /* CVC5_MUZZLE */ } } // namespace test -- 2.30.2