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.
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)
{
// 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
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,
{
size_t tagid = static_cast<size_t>(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);
}
// 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
// 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<bool>())
{
if (!n.isConst())
{
// Not constant, print a less severe warning message here.
- Warning()
+ warning()
<< "Warning : SolverEngine::checkModel(): cannot check simplified "
"assertion : "
<< n << std::endl;
}
// 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
}
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
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<size_t>(tag)];
}
{
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))
{
}
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,
#include <memory>
-#include "options/base_options.h"
#include "options/options.h"
#include "proof/method_id.h"
#include "theory/logic_info.h"
class ProofNodeManager;
class Printer;
class ResourceManager;
+namespace options {
+enum class OutputTag;
+}
+using OutputTag = options::OutputTag;
namespace context {
class Context;
* 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--------------------------------------------------------- */
/**
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
#include <memory>
#include "expr/node.h"
-
namespace cvc5 {
class Env;
class Context;
class UserContext;
} // namespace context
+namespace options {
+enum class OutputTag;
+}
+using OutputTag = options::OutputTag;
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;
};
{
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;
}
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<Node> removed;
for (const Node& skip : core)
{
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
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;
{
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 "
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);
{
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<Node, std::map<Node, Node>> sol_map;
// Get solutions and build auxiliary vectors for substituting
QuantifiersEngine* qe = d_smtSolver.getQuantifiersEngine();
std::unordered_map<Node, Node> 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())
{
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);
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())
{
}
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() {
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())
&& 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;
}
}
}
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 ){
<< " * " << 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)
{
continue;
}
- d_env.getOutput(options::OutputTag::INST)
- << "(num-instantiations " << name << " " << i.second << ")"
- << std::endl;
+ output(OutputTag::INST) << "(num-instantiations " << name << " "
+ << i.second << ")" << std::endl;
}
}
}
}
}
- 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
}
}
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;
}
}
// 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;
}
}
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
// 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();
}
}
}
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 ] ]++;
}
}
//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
; EXPECT: true
; EXPECT: false
; EXPECT: 15
-; EXPECT: SimplificationMode::NONE
+; EXPECT: none
(get-option :command-verbosity)
(set-option :command-verbosity (* 1))
; COMMAND-LINE: -vvv --sygus-out=status --check-synth-sol --check-abducts
+; ERROR-SCRUBBER: sed -e 's/.*//g'
; SCRUBBER: sed -e 's/.*//g'
; EXIT: 0
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);
EXPECT_TRUE(std::holds_alternative<OptionInfo::ModeInfo>(info.valueInfo));
auto modeInfo = std::get<OptionInfo::ModeInfo>(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());
}
projects / cvc5.git / commitdiff