From: Gereon Kremer Date: Sat, 6 Nov 2021 00:27:08 +0000 (-0700) Subject: Remove `Notice()` in favor of new `verbose()` (#7588) X-Git-Tag: cvc5-1.0.0~872 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1909b36e01578099d7a773e561b4bec15c067580;p=cvc5.git Remove `Notice()` in favor of new `verbose()` (#7588) This PR removes the remaining usages of the Notice() macros and uses verbose() instead. --- diff --git a/src/api/__pycache__/parsekinds.cpython-39.pyc b/src/api/__pycache__/parsekinds.cpython-39.pyc new file mode 100644 index 000000000..34d010ce4 Binary files /dev/null and b/src/api/__pycache__/parsekinds.cpython-39.pyc differ 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