diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2021-07-03 10:44:30 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-07-03 17:44:30 +0000 |
commit | c56eaf4423fbf65663a4e03c8a60ed937c99de7d (patch) | |
tree | c7b4d8d67f09441cac77a8100db49b6bf41e8230 /src/theory/quantifiers/instantiate.cpp | |
parent | de0401e53e4baab30a5e78d5bd51048348b1e1ce (diff) |
Add output tags -o, --output. (#6826)
Output tags are similar to debug/trace tags, but are always enabled
(except for muzzled builds) to provide useful information for users.
Available output tags can be queried via -o help/--output help and are
specified in the base options module via enum values.
Co-authored-by: Gereon Kremer <nafur42@gmail.com>
Diffstat (limited to 'src/theory/quantifiers/instantiate.cpp')
-rw-r--r-- | src/theory/quantifiers/instantiate.cpp | 37 |
1 files changed, 16 insertions, 21 deletions
diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index 157f0f64b..17fd089d6 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -17,6 +17,7 @@ #include "expr/node_algorithm.h" #include "options/base_options.h" +#include "options/outputc.h" #include "options/printer_options.h" #include "options/quantifiers_options.h" #include "options/smt_options.h" @@ -676,33 +677,27 @@ bool Instantiate::isProofEnabled() const { return d_pfInst != nullptr; } void Instantiate::notifyEndRound() { - bool debugInstTrace = Trace.isOn("inst-per-quant-round"); - if (options::debugInst() || debugInstTrace) + // debug information + if (Trace.isOn("inst-per-quant-round")) { - Options& sopts = smt::currentSmtEngine()->getOptions(); - std::ostream& out = *sopts.base.out; - // debug information - if (debugInstTrace) + for (std::pair<const Node, uint32_t>& i : d_instDebugTemp) { - for (std::pair<const Node, uint32_t>& i : d_instDebugTemp) - { - Trace("inst-per-quant-round") - << " * " << i.second << " for " << i.first << std::endl; - } + Trace("inst-per-quant-round") + << " * " << i.second << " for " << i.first << std::endl; } - if (options::debugInst()) + } + if (Output.isOn(options::OutputTag::INST)) + { + bool req = !options::printInstFull(); + for (std::pair<const Node, uint32_t>& i : d_instDebugTemp) { - bool req = !options::printInstFull(); - for (std::pair<const Node, uint32_t>& i : d_instDebugTemp) + Node name; + if (!d_qreg.getNameForQuant(i.first, name, req)) { - Node name; - if (!d_qreg.getNameForQuant(i.first, name, req)) - { - continue; - } - out << "(num-instantiations " << name << " " << i.second << ")" - << std::endl; + continue; } + Output(options::OutputTag::INST) << "(num-instantiations " << name << " " + << i.second << ")" << std::endl; } } } |