diff options
author | Gereon Kremer <nafur42@gmail.com> | 2021-11-04 12:15:28 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-11-04 19:15:28 +0000 |
commit | 67559f3b3e42dc1937f809e56ee57daa4bd8bd89 (patch) | |
tree | 037d2a4202c2adef7940bbd1230875247f173bc6 /src/theory | |
parent | e1f69a43e9ee7e4a63f3c4a1881001bc650c9df7 (diff) |
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.
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/datatypes/theory_datatypes.cpp | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/alpha_equivalence.cpp | 6 | ||||
-rw-r--r-- | src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp | 5 | ||||
-rw-r--r-- | src/theory/quantifiers/ematching/trigger.cpp | 7 | ||||
-rw-r--r-- | src/theory/quantifiers/instantiate.cpp | 7 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/synth_conjecture.cpp | 15 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus_sampler.cpp | 9 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 2 | ||||
-rw-r--r-- | src/theory/uf/cardinality_extension.cpp | 2 |
9 files changed, 25 insertions, 32 deletions
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<const Node, uint32_t>& 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 |