From 67559f3b3e42dc1937f809e56ee57daa4bd8bd89 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Thu, 4 Nov 2021 12:15:28 -0700 Subject: [PATCH] Start refactoring of `-o` and `-v` (#7449) This PR does the first step in consolidating our various output mechanisms. The goal is to have only three major ways to output information: - verbose(level) prints log-like information to the user via stderr, -v and -q increase and decrease the verbosity, respectively. - output(tag) prints structured information (as s-expressions) to the user via stdout, -o enables individual tags. - Trace(tag) prints log-like information to the developer via stdout, -t enables individual tags. While Debug and Trace (and eventually Dump) will be combined within Trace, all of Warning, Message, Notice and Chat will be combined into verbose. --- src/api/cpp/cvc5.cpp | 4 +-- src/main/command_executor.cpp | 3 +- src/options/mkoptions.py | 5 +-- src/options/options_handler.cpp | 3 +- src/smt/check_models.cpp | 26 +++++++------- src/smt/env.cpp | 23 +++++++++--- src/smt/env.h | 35 ++++++++++++++----- src/smt/env_obj.cpp | 16 +++++++++ src/smt/env_obj.h | 20 ++++++++++- src/smt/quant_elim_solver.cpp | 4 +-- src/smt/solver_engine.cpp | 21 ++++++----- src/smt/sygus_solver.cpp | 35 +++++++++++++------ src/theory/datatypes/theory_datatypes.cpp | 4 +-- src/theory/quantifiers/alpha_equivalence.cpp | 6 ++-- .../ematching/inst_strategy_e_matching.cpp | 5 ++- src/theory/quantifiers/ematching/trigger.cpp | 7 ++-- src/theory/quantifiers/instantiate.cpp | 7 ++-- .../quantifiers/sygus/synth_conjecture.cpp | 15 ++++---- src/theory/quantifiers/sygus_sampler.cpp | 9 ++--- src/theory/theory_engine.cpp | 2 +- src/theory/uf/cardinality_extension.cpp | 2 -- .../regress0/options/set-and-get-options.smt2 | 2 +- test/regress/regress0/sygus/issue5512-vvv.sy | 1 + test/unit/api/java/SolverTest.java | 2 +- test/unit/api/solver_black.cpp | 2 +- 25 files changed, 171 insertions(+), 88 deletions(-) diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 0450ac06a..90f6f0d56 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -7862,12 +7862,12 @@ bool Solver::isOutputOn(const std::string& tag) const std::ostream& Solver::getOutput(const std::string& tag) const { - // `getOutput(tag)` may raise an `OptionException`, which we do not want to + // `output(tag)` may raise an `OptionException`, which we do not want to // forward as such. We thus do not use the standard exception handling macros // here but roll our own. try { - return d_slv->getEnv().getOutput(tag); + return d_slv->getEnv().output(tag); } catch (const cvc5::Exception& e) { diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp index f08d9adde..be3652dd4 100644 --- a/src/main/command_executor.cpp +++ b/src/main/command_executor.cpp @@ -200,8 +200,7 @@ bool solverInvoke(api::Solver* solver, // print output for -o raw-benchmark if (solver->isOutputOn("raw-benchmark")) { - std::ostream& ss = solver->getOutput("raw-benchmark"); - cmd->toStream(ss); + cmd->toStream(solver->getOutput("raw-benchmark")); } // In parse-only mode, we do not invoke any of the commands except define-fun diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py index 0db16e7c6..63ca49c76 100644 --- a/src/options/mkoptions.py +++ b/src/options/mkoptions.py @@ -524,8 +524,9 @@ def generate_module_mode_impl(module): if option.name is None or not option.mode: continue cases = [ - 'case {type}::{enum}: return os << "{type}::{enum}";'.format( - type=option.type, enum=x) for x in option.mode.keys() + 'case {type}::{enum}: return os << "{name}";'.format( + type=option.type, enum=enum, name=info[0]['name']) + for enum,info in option.mode.items() ] res.append( TPL_MODE_STREAM_OPERATOR.format(type=option.type, diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index 2a7331c67..b58063dbb 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -269,8 +269,7 @@ void OptionsHandler::enableOutputTag(const std::string& flag, { size_t tagid = static_cast(stringToOutputTag(optarg)); Assert(d_options->base.outputTagHolder.size() > tagid) - << "Trying to enable an output tag whose value is larger than the bitset " - "that holds it. Maybe someone forgot to update the bitset size?"; + << "Output tag is larger than the bitset that holds it."; d_options->base.outputTagHolder.set(tagid); } diff --git a/src/smt/check_models.cpp b/src/smt/check_models.cpp index 5d16c12ce..13e504835 100644 --- a/src/smt/check_models.cpp +++ b/src/smt/check_models.cpp @@ -64,8 +64,8 @@ void CheckModels::checkModel(TheoryModel* m, // Now go through all our user assertions checking if they're satisfied. for (const Node& assertion : al) { - Notice() << "SolverEngine::checkModel(): checking assertion " << assertion - << std::endl; + verbose(1) << "SolverEngine::checkModel(): checking assertion " << assertion + << std::endl; // Apply any define-funs from the problem. We do not expand theory symbols // like integer division here. Hence, the code below is not able to properly @@ -73,17 +73,19 @@ void CheckModels::checkModel(TheoryModel* m, // is not trustworthy, since the UF introduced by expanding definitions may // not be properly constrained. Node n = sm.apply(assertion, false); - Notice() << "SolverEngine::checkModel(): -- substitutes to " << n - << std::endl; + verbose(1) << "SolverEngine::checkModel(): -- substitutes to " << n + << std::endl; n = rewrite(n); - Notice() << "SolverEngine::checkModel(): -- rewrites to " << n << std::endl; + verbose(1) << "SolverEngine::checkModel(): -- rewrites to " << n + << std::endl; // We look up the value before simplifying. If n contains quantifiers, // this may increases the chance of finding its value before the node is // altered by simplification below. n = m->getValue(n); - Notice() << "SolverEngine::checkModel(): -- get value : " << n << std::endl; + verbose(1) << "SolverEngine::checkModel(): -- get value : " << n + << std::endl; if (n.isConst() && n.getConst()) { @@ -109,7 +111,7 @@ void CheckModels::checkModel(TheoryModel* m, if (!n.isConst()) { // Not constant, print a less severe warning message here. - Warning() + warning() << "Warning : SolverEngine::checkModel(): cannot check simplified " "assertion : " << n << std::endl; @@ -118,8 +120,8 @@ void CheckModels::checkModel(TheoryModel* m, } // Assertions that simplify to false result in an InternalError or // Warning being thrown below (when hardFailure is false). - Notice() << "SolverEngine::checkModel(): *** PROBLEM: EXPECTED `TRUE' ***" - << std::endl; + verbose(1) << "SolverEngine::checkModel(): *** PROBLEM: EXPECTED `TRUE' ***" + << std::endl; std::stringstream ss; ss << "SolverEngine::checkModel(): " << "ERRORS SATISFYING ASSERTIONS WITH MODEL:" << std::endl @@ -134,13 +136,13 @@ void CheckModels::checkModel(TheoryModel* m, } else { - Warning() << ss.str() << std::endl; + warning() << ss.str() << std::endl; } } if (noCheckList.empty()) { - Notice() << "SolverEngine::checkModel(): all assertions checked out OK !" - << std::endl; + verbose(1) << "SolverEngine::checkModel(): all assertions checked out OK !" + << std::endl; return; } // if the noCheckList is non-empty, we could expand definitions on this list diff --git a/src/smt/env.cpp b/src/smt/env.cpp index fd44c274c..dc9efdf91 100644 --- a/src/smt/env.cpp +++ b/src/smt/env.cpp @@ -148,7 +148,7 @@ const Printer& Env::getPrinter() std::ostream& Env::getDumpOut() { return *d_options.base.out; } -bool Env::isOutputOn(options::OutputTag tag) const +bool Env::isOutputOn(OutputTag tag) const { return d_options.base.outputTagHolder[static_cast(tag)]; } @@ -156,7 +156,12 @@ bool Env::isOutputOn(const std::string& tag) const { return isOutputOn(options::stringToOutputTag(tag)); } -std::ostream& Env::getOutput(options::OutputTag tag) const +std::ostream& Env::output(const std::string& tag) const +{ + return output(options::stringToOutputTag(tag)); +} + +std::ostream& Env::output(OutputTag tag) const { if (isOutputOn(tag)) { @@ -164,9 +169,19 @@ std::ostream& Env::getOutput(options::OutputTag tag) const } return cvc5::null_os; } -std::ostream& Env::getOutput(const std::string& tag) const + +bool Env::isVerboseOn(int64_t level) const +{ + return !Configuration::isMuzzledBuild() && d_options.base.verbosity >= level; +} + +std::ostream& Env::verbose(int64_t level) const { - return getOutput(options::stringToOutputTag(tag)); + if (isVerboseOn(level)) + { + return *d_options.base.err; + } + return cvc5::null_os; } Node Env::evaluate(TNode n, diff --git a/src/smt/env.h b/src/smt/env.h index 1974408ad..25f8d0b71 100644 --- a/src/smt/env.h +++ b/src/smt/env.h @@ -21,7 +21,6 @@ #include -#include "options/base_options.h" #include "options/options.h" #include "proof/method_id.h" #include "theory/logic_info.h" @@ -34,6 +33,10 @@ class StatisticsRegistry; class ProofNodeManager; class Printer; class ResourceManager; +namespace options { +enum class OutputTag; +} +using OutputTag = options::OutputTag; namespace context { class Context; @@ -152,25 +155,41 @@ class Env * Check whether the output for the given output tag is enabled. Output tags * are enabled via the `output` option (or `-o` on the command line). */ - bool isOutputOn(options::OutputTag tag) const; + bool isOutputOn(OutputTag tag) const; /** * Check whether the output for the given output tag (as a string) is enabled. * Output tags are enabled via the `output` option (or `-o` on the command * line). */ bool isOutputOn(const std::string& tag) const; + + /** + * Return the output stream for the given output tag (as a string). If the + * output tag is enabled, this returns the output stream from the `out` + * option. Otherwise, a null stream (`cvc5::null_os`) is returned. + */ + std::ostream& output(const std::string& tag) const; + /** * Return the output stream for the given output tag. If the output tag is * enabled, this returns the output stream from the `out` option. Otherwise, - * a null stream (`cvc5::null_os`) is returned. + * a null stream (`cvc5::null_os`) is returned. The user of this method needs + * to make sure that a proper S-expression is printed. */ - std::ostream& getOutput(options::OutputTag tag) const; + std::ostream& output(OutputTag tag) const; + /** - * Return the output stream for the given output tag (as a string). If the - * output tag is enabled, this returns the output stream from the `out` - * option. Otherwise, a null stream (`cvc5::null_os`) is returned. + * Check whether the verbose output for the given verbosity level is enabled. + * The verbosity level is raised (or lowered) with the `-v` (or `-q`) option. + */ + bool isVerboseOn(int64_t level) const; + + /** + * Return the output stream for the given verbosity level. If the verbosity + * level is enabled, this returns the output stream from the `err` option. + * Otherwise, a null stream (`cvc5::null_os`) is returned. */ - std::ostream& getOutput(const std::string& tag) const; + std::ostream& verbose(int64_t level) const; /* Rewrite helpers--------------------------------------------------------- */ /** diff --git a/src/smt/env_obj.cpp b/src/smt/env_obj.cpp index 926bf61ff..8af3bdfd0 100644 --- a/src/smt/env_obj.cpp +++ b/src/smt/env_obj.cpp @@ -70,4 +70,20 @@ StatisticsRegistry& EnvObj::statisticsRegistry() const return d_env.getStatisticsRegistry(); } +bool EnvObj::isOutputOn(OutputTag tag) const { return d_env.isOutputOn(tag); } + +std::ostream& EnvObj::output(OutputTag tag) const { return d_env.output(tag); } + +bool EnvObj::isVerboseOn(int64_t level) const +{ + return d_env.isVerboseOn(level); +} + +std::ostream& EnvObj::verbose(int64_t level) const +{ + return d_env.verbose(level); +} + +std::ostream& EnvObj::warning() const { return verbose(0); } + } // namespace cvc5 diff --git a/src/smt/env_obj.h b/src/smt/env_obj.h index b240b4852..2c88f45b4 100644 --- a/src/smt/env_obj.h +++ b/src/smt/env_obj.h @@ -22,7 +22,6 @@ #include #include "expr/node.h" - namespace cvc5 { class Env; @@ -35,6 +34,10 @@ namespace context { class Context; class UserContext; } // namespace context +namespace options { +enum class OutputTag; +} +using OutputTag = options::OutputTag; class EnvObj { @@ -88,6 +91,21 @@ class EnvObj /** Get the statistics registry via Env. */ StatisticsRegistry& statisticsRegistry() const; + /** Convenience wrapper for Env::isOutputOn(). */ + bool isOutputOn(OutputTag tag) const; + + /** Convenience wrapper for Env::output(). */ + std::ostream& output(OutputTag tag) const; + + /** Convenience wrapper for Env::isVerboseOn(). */ + bool isVerboseOn(int64_t level) const; + + /** Convenience wrapper for Env::verbose(). */ + std::ostream& verbose(int64_t) const; + + /** Convenience wrapper for Env::verbose(0). */ + std::ostream& warning() const; + /** The associated environment. */ Env& d_env; }; diff --git a/src/smt/quant_elim_solver.cpp b/src/smt/quant_elim_solver.cpp index 2ffa0d7c1..919368512 100644 --- a/src/smt/quant_elim_solver.cpp +++ b/src/smt/quant_elim_solver.cpp @@ -79,9 +79,9 @@ Node QuantElimSolver::getQuantifierElimination(Assertions& as, { if (r.asSatisfiabilityResult().isSat() != Result::SAT && doFull) { - Notice() + verbose(1) << "While performing quantifier elimination, unexpected result : " - << r << " for query."; + << r << " for query." << std::endl; // failed, return original return q; } diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp index c7147a676..fddea7649 100644 --- a/src/smt/solver_engine.cpp +++ b/src/smt/solver_engine.cpp @@ -1383,7 +1383,8 @@ std::vector SolverEngine::reduceUnsatCore(const std::vector& core) Assert(options::unsatCores()) << "cannot reduce unsat core if unsat cores are turned off"; - Notice() << "SolverEngine::reduceUnsatCore(): reducing unsat core" << endl; + d_env->verbose(1) << "SolverEngine::reduceUnsatCore(): reducing unsat core" + << std::endl; std::unordered_set removed; for (const Node& skip : core) { @@ -1450,7 +1451,8 @@ void SolverEngine::checkUnsatCore() Assert(d_env->getOptions().smt.unsatCores) << "cannot check unsat core if unsat cores are turned off"; - Notice() << "SolverEngine::checkUnsatCore(): generating unsat core" << endl; + d_env->verbose(1) << "SolverEngine::checkUnsatCore(): generating unsat core" + << std::endl; UnsatCore core = getUnsatCore(); // initialize the core checker @@ -1468,14 +1470,15 @@ void SolverEngine::checkUnsatCore() coreChecker->declareSepHeap(sepLocType, sepDataType); } - Notice() << "SolverEngine::checkUnsatCore(): pushing core assertions" - << std::endl; + d_env->verbose(1) << "SolverEngine::checkUnsatCore(): pushing core assertions" + << std::endl; theory::TrustSubstitutionMap& tls = d_env->getTopLevelSubstitutions(); for (UnsatCore::iterator i = core.begin(); i != core.end(); ++i) { Node assertionAfterExpansion = tls.apply(*i, false); - Notice() << "SolverEngine::checkUnsatCore(): pushing core member " << *i - << ", expanded to " << assertionAfterExpansion << "\n"; + d_env->verbose(1) << "SolverEngine::checkUnsatCore(): pushing core member " + << *i << ", expanded to " << assertionAfterExpansion + << std::endl; coreChecker->assertFormula(assertionAfterExpansion); } Result r; @@ -1487,7 +1490,8 @@ void SolverEngine::checkUnsatCore() { throw; } - Notice() << "SolverEngine::checkUnsatCore(): result is " << r << endl; + d_env->verbose(1) << "SolverEngine::checkUnsatCore(): result is " << r + << std::endl; if (r.asSatisfiabilityResult().isUnknown()) { Warning() << "SolverEngine::checkUnsatCore(): could not check core result " @@ -1511,7 +1515,8 @@ void SolverEngine::checkModel(bool hardFailure) TimerStat::CodeTimer checkModelTimer(d_stats->d_checkModelTime); - Notice() << "SolverEngine::checkModel(): generating model" << endl; + d_env->verbose(1) << "SolverEngine::checkModel(): generating model" + << std::endl; TheoryModel* m = getAvailableModel("check model"); Assert(m != nullptr); diff --git a/src/smt/sygus_solver.cpp b/src/smt/sygus_solver.cpp index 5db9804c6..4c8d3e5bd 100644 --- a/src/smt/sygus_solver.cpp +++ b/src/smt/sygus_solver.cpp @@ -257,8 +257,11 @@ void SygusSolver::checkSynthSolution(Assertions& as) { NodeManager* nm = NodeManager::currentNM(); SkolemManager* sm = nm->getSkolemManager(); - Notice() << "SygusSolver::checkSynthSolution(): checking synthesis solution" - << std::endl; + if (isVerboseOn(1)) + { + verbose(1) << "SyGuS::checkSynthSolution: checking synthesis solution" + << std::endl; + } std::map> sol_map; // Get solutions and build auxiliary vectors for substituting QuantifiersEngine* qe = d_smtSolver.getQuantifiersEngine(); @@ -308,13 +311,19 @@ void SygusSolver::checkSynthSolution(Assertions& as) std::unordered_map cache; for (const Node& assertion : alist) { - Notice() << "SygusSolver::checkSynthSolution(): checking assertion " - << assertion << std::endl; + if (isVerboseOn(1)) + { + verbose(1) << "SyGuS::checkSynthSolution: checking assertion " + << assertion << std::endl; + } Trace("check-synth-sol") << "Retrieving assertion " << assertion << "\n"; // Apply any define-funs from the problem. Node n = d_smtSolver.getPreprocessor()->expandDefinitions(assertion, cache); - Notice() << "SygusSolver::checkSynthSolution(): -- expands to " << n - << std::endl; + if (isVerboseOn(1)) + { + verbose(1) << "SyGuS::checkSynthSolution: -- expands to " << n + << std::endl; + } Trace("check-synth-sol") << "Expanded assertion " << n << "\n"; if (conjs.find(n) == conjs.end()) { @@ -364,8 +373,12 @@ void SygusSolver::checkSynthSolution(Assertions& as) conjBody = conjBody.substitute( vars.begin(), vars.end(), skos.begin(), skos.end()); } - Notice() << "SygusSolver::checkSynthSolution(): -- body substitutes to " - << conjBody << std::endl; + + if (isVerboseOn(1)) + { + verbose(1) << "SyGuS::checkSynthSolution: -- body substitutes to " + << conjBody << std::endl; + } Trace("check-synth-sol") << "Substituted body of assertion to " << conjBody << "\n"; solChecker->assertFormula(conjBody); @@ -381,8 +394,10 @@ void SygusSolver::checkSynthSolution(Assertions& as) solChecker->assertFormula(ar); } Result r = solChecker->checkSat(); - Notice() << "SygusSolver::checkSynthSolution(): result is " << r - << std::endl; + if (isVerboseOn(1)) + { + verbose(1) << "SyGuS::checkSynthSolution: result is " << r << std::endl; + } Trace("check-synth-sol") << "Satsifiability check: " << r << "\n"; if (r.asSatisfiabilityResult().isUnknown()) { diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index fe48aa59d..1c6e3f0cb 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -382,9 +382,7 @@ void TheoryDatatypes::postCheck(Effort level) } Trace("datatypes-check") << "Finished check effort " << level << std::endl; - if( Debug.isOn("datatypes") || Debug.isOn("datatypes-split") ) { - Notice() << "TheoryDatatypes::check(): done" << endl; - } + Debug("datatypes") << "TheoryDatatypes::check(): done" << std::endl; } bool TheoryDatatypes::needsCheckLastEffort() { diff --git a/src/theory/quantifiers/alpha_equivalence.cpp b/src/theory/quantifiers/alpha_equivalence.cpp index f4370c017..0c9a5ba46 100644 --- a/src/theory/quantifiers/alpha_equivalence.cpp +++ b/src/theory/quantifiers/alpha_equivalence.cpp @@ -172,9 +172,9 @@ TrustNode AlphaEquivalence::reduceQuantifier(Node q) lem = ret.eqNode(q); if (q.getNumChildren() == 3) { - Notice() << "Ignoring annotated quantified formula based on alpha " - "equivalence: " - << q << std::endl; + verbose(1) << "Ignoring annotated quantified formula based on alpha " + "equivalence: " + << q << std::endl; } // if successfully computed the substitution above if (isProofEnabled() && !vars.empty()) diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp index fdb0d0db3..f1d80032b 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp @@ -153,10 +153,9 @@ InstStrategyStatus InstStrategyAutoGenTriggers::process(Node f, && d_auto_gen_trigger[1][f].empty() && !QuantAttributes::hasPattern(f)) { Trace("trigger-warn") << "Could not find trigger for " << f << std::endl; - if (d_env.isOutputOn(options::OutputTag::TRIGGER)) + if (isOutputOn(OutputTag::TRIGGER)) { - d_env.getOutput(options::OutputTag::TRIGGER) - << "(no-trigger " << f << ")" << std::endl; + output(OutputTag::TRIGGER) << "(no-trigger " << f << ")" << std::endl; } } } diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp index ff02e5f3e..e267b470d 100644 --- a/src/theory/quantifiers/ematching/trigger.cpp +++ b/src/theory/quantifiers/ematching/trigger.cpp @@ -78,12 +78,11 @@ Trigger::Trigger(Env& env, extNodes.push_back(ns); } d_trNode = NodeManager::currentNM()->mkNode(SEXPR, extNodes); - if (d_env.isOutputOn(options::OutputTag::TRIGGER)) + if (isOutputOn(OutputTag::TRIGGER)) { QuantAttributes& qa = d_qreg.getQuantAttributes(); - d_env.getOutput(options::OutputTag::TRIGGER) - << "(trigger " << qa.quantToString(q) << " " << d_trNode << ")" - << std::endl; + output(OutputTag::TRIGGER) << "(trigger " << qa.quantToString(q) << " " + << d_trNode << ")" << std::endl; } QuantifiersStatistics& stats = qs.getStats(); if( d_nodes.size()==1 ){ diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index 23f789f4e..1af2b3f75 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -706,7 +706,7 @@ void Instantiate::notifyEndRound() << " * " << i.second << " for " << i.first << std::endl; } } - if (d_env.isOutputOn(options::OutputTag::INST)) + if (isOutputOn(OutputTag::INST)) { bool req = !options().printer.printInstFull; for (std::pair& i : d_instDebugTemp) @@ -716,9 +716,8 @@ void Instantiate::notifyEndRound() { continue; } - d_env.getOutput(options::OutputTag::INST) - << "(num-instantiations " << name << " " << i.second << ")" - << std::endl; + output(OutputTag::INST) << "(num-instantiations " << name << " " + << i.second << ")" << std::endl; } } } diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index 6c3f5e70b..1fde43913 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -372,7 +372,7 @@ bool SynthConjecture::doCheck() } } - bool printDebug = d_env.isOutputOn(options::OutputTag::SYGUS); + bool printDebug = isOutputOn(OutputTag::SYGUS); if (!constructed_cand) { // get the model value of the relevant terms from the master module @@ -437,9 +437,9 @@ bool SynthConjecture::doCheck() } } Trace("sygus-engine") << std::endl; - if (d_env.isOutputOn(options::OutputTag::SYGUS)) + if (d_env.isOutputOn(OutputTag::SYGUS)) { - d_env.getOutput(options::OutputTag::SYGUS) + d_env.output(OutputTag::SYGUS) << "(sygus-enum" << sygusEnumOut.str() << ")" << std::endl; } } @@ -518,16 +518,15 @@ bool SynthConjecture::doCheck() // print the candidate solution for debugging if (constructed_cand && printDebug) { - const Options& sopts = options(); - std::ostream& out = *sopts.base.out; + std::ostream& out = output(OutputTag::SYGUS); out << "(sygus-candidate "; Assert(d_quant[0].getNumChildren() == candidate_values.size()); for (size_t i = 0, ncands = candidate_values.size(); i < ncands; i++) { Node v = candidate_values[i]; - std::stringstream ss; - TermDbSygus::toStreamSygus(ss, v); - out << "(" << d_quant[0][i] << " " << ss.str() << ")"; + out << "(" << d_quant[0][i] << " "; + TermDbSygus::toStreamSygus(out, v); + out << ")"; } out << ")" << std::endl; } diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp index 08fab59eb..2fc7f0c29 100644 --- a/src/theory/quantifiers/sygus_sampler.cpp +++ b/src/theory/quantifiers/sygus_sampler.cpp @@ -815,10 +815,11 @@ void SygusSampler::checkEquivalent(Node bv, Node bvr, std::ostream& out) } if (!ptDisequalConst) { - Notice() << "Warning: " << bv << " and " << bvr - << " evaluate to different (non-constant) values on point:" - << std::endl; - Notice() << ptOut.str(); + d_env.verbose(1) + << "Warning: " << bv << " and " << bvr + << " evaluate to different (non-constant) values on point:" + << std::endl; + d_env.verbose(1) << ptOut.str(); return; } // we have detected unsoundness in the rewriter diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 03880bfbb..5aafae367 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1892,7 +1892,7 @@ void TheoryEngine::checkTheoryAssertionsWithModel(bool hardFailure) { // assertions with unevaluable operators, e.g. transcendental // functions. It also may happen for separation logic, where // check-model support is limited. - Warning() << ss.str(); + warning() << ss.str(); } } } diff --git a/src/theory/uf/cardinality_extension.cpp b/src/theory/uf/cardinality_extension.cpp index 650ef1d70..83862e8bb 100644 --- a/src/theory/uf/cardinality_extension.cpp +++ b/src/theory/uf/cardinality_extension.cpp @@ -828,7 +828,6 @@ void SortModel::getDisequalitiesToRegions(int ri, for( DiseqList::iterator it2 = del->begin(); it2 != del->end(); ++it2 ){ if( (*it2).second ){ Assert(isValid(d_regions_map[(*it2).first])); - //Notice() << "Found disequality with " << (*it2).first << ", region = " << d_regions_map[ (*it2).first ] << std::endl; regions_diseq[ d_regions_map[ (*it2).first ] ]++; } } @@ -1046,7 +1045,6 @@ int SortModel::addSplit(Region* r) //Trace("uf-ss-lemma") << d_th->getEqualityEngine()->areEqual( s[0], s[1] ) << " "; //Trace("uf-ss-lemma") << d_th->getEqualityEngine()->areDisequal( s[0], s[1] ) << std::endl; //Trace("uf-ss-lemma") << s[0].getType() << " " << s[1].getType() << std::endl; - //Notice() << "*** Split on " << s << std::endl; //split on the equality s Node lem = NodeManager::currentNM()->mkNode( kind::OR, ss, ss.negate() ); // send lemma, with caching diff --git a/test/regress/regress0/options/set-and-get-options.smt2 b/test/regress/regress0/options/set-and-get-options.smt2 index 6b07dfc1c..24e05ec2a 100644 --- a/test/regress/regress0/options/set-and-get-options.smt2 +++ b/test/regress/regress0/options/set-and-get-options.smt2 @@ -3,7 +3,7 @@ ; EXPECT: true ; EXPECT: false ; EXPECT: 15 -; EXPECT: SimplificationMode::NONE +; EXPECT: none (get-option :command-verbosity) (set-option :command-verbosity (* 1)) diff --git a/test/regress/regress0/sygus/issue5512-vvv.sy b/test/regress/regress0/sygus/issue5512-vvv.sy index 9d37032ac..333c0dd5a 100644 --- a/test/regress/regress0/sygus/issue5512-vvv.sy +++ b/test/regress/regress0/sygus/issue5512-vvv.sy @@ -1,4 +1,5 @@ ; COMMAND-LINE: -vvv --sygus-out=status --check-synth-sol --check-abducts +; ERROR-SCRUBBER: sed -e 's/.*//g' ; SCRUBBER: sed -e 's/.*//g' ; EXIT: 0 diff --git a/test/unit/api/java/SolverTest.java b/test/unit/api/java/SolverTest.java index 4c9ec4c0d..f89ecfffd 100644 --- a/test/unit/api/java/SolverTest.java +++ b/test/unit/api/java/SolverTest.java @@ -1429,7 +1429,7 @@ class SolverTest assertions.add(() -> assertTrue(info.getBaseInfo().getClass() == OptionInfo.ModeInfo.class)); OptionInfo.ModeInfo modeInfo = (OptionInfo.ModeInfo) info.getBaseInfo(); assertions.add(() -> assertEquals("NONE", modeInfo.getDefaultValue())); - assertions.add(() -> assertEquals("OutputTag::NONE", modeInfo.getCurrentValue())); + assertions.add(() -> assertEquals("none", modeInfo.getCurrentValue())); assertions.add(() -> assertTrue(Arrays.asList(modeInfo.getModes()).contains("NONE"))); } assertAll(assertions); diff --git a/test/unit/api/solver_black.cpp b/test/unit/api/solver_black.cpp index 062a2a59e..eca6683ba 100644 --- a/test/unit/api/solver_black.cpp +++ b/test/unit/api/solver_black.cpp @@ -1379,7 +1379,7 @@ TEST_F(TestApiBlackSolver, getOptionInfo) EXPECT_TRUE(std::holds_alternative(info.valueInfo)); auto modeInfo = std::get(info.valueInfo); EXPECT_EQ("NONE", modeInfo.defaultValue); - EXPECT_EQ("OutputTag::NONE", modeInfo.currentValue); + EXPECT_EQ("none", modeInfo.currentValue); EXPECT_TRUE(std::find(modeInfo.modes.begin(), modeInfo.modes.end(), "NONE") != modeInfo.modes.end()); } -- 2.30.2