diff options
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/instantiate.cpp | 37 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/synth_conjecture.cpp | 11 |
2 files changed, 20 insertions, 28 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; } } } diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index 4e8d7d46d..b2b69687c 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -20,6 +20,7 @@ #include "expr/skolem_manager.h" #include "options/base_options.h" #include "options/datatypes_options.h" +#include "options/outputc.h" #include "options/quantifiers_options.h" #include "printer/printer.h" #include "smt/logic_exception.h" @@ -384,7 +385,7 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems) } } - bool printDebug = options::debugSygus(); + bool printDebug = Output.isOn(options::OutputTag::SYGUS); if (!constructed_cand) { // get the model value of the relevant terms from the master module @@ -454,12 +455,8 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems) } } Trace("sygus-engine") << std::endl; - if (printDebug) - { - Options& sopts = smt::currentSmtEngine()->getOptions(); - std::ostream& out = *sopts.base.out; - out << "(sygus-enum" << sygusEnumOut.str() << ")" << std::endl; - } + Output(options::OutputTag::SYGUS) + << "(sygus-enum" << sygusEnumOut.str() << ")" << std::endl; } Assert(candidate_values.empty()); constructed_cand = d_master->constructCandidates( |