From 07a47262c405fb37248572d3029883d078273cd7 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Thu, 23 Sep 2021 16:14:08 -0700 Subject: [PATCH] Eliminate Output macro in favor of simple Env functions (#7223) This PR eliminates the Output macro together with the associated output stream (stored in a static variable). It is replaces by a set of simple utility functions of the Env class, and we instead use the output stream from options.base.out. To achieve this, a couple of quantifier classes are now derived from EnvObj. --- src/CMakeLists.txt | 2 - src/api/cpp/cvc5.cpp | 10 ++--- src/options/outputc.cpp | 35 ---------------- src/options/outputc.h | 40 ------------------- src/smt/env.cpp | 21 ++++++++++ src/smt/env.h | 25 ++++++++++++ .../quantifiers/ematching/ho_trigger.cpp | 3 +- src/theory/quantifiers/ematching/ho_trigger.h | 3 +- .../quantifiers/ematching/inst_strategy.cpp | 6 ++- .../quantifiers/ematching/inst_strategy.h | 7 +++- .../ematching/inst_strategy_e_matching.cpp | 11 +++-- .../ematching/inst_strategy_e_matching.h | 3 +- .../inst_strategy_e_matching_user.cpp | 3 +- .../ematching/inst_strategy_e_matching_user.h | 3 +- .../ematching/instantiation_engine.cpp | 7 ++-- src/theory/quantifiers/ematching/trigger.cpp | 14 ++++--- src/theory/quantifiers/ematching/trigger.h | 7 +++- .../ematching/trigger_database.cpp | 10 +++-- .../quantifiers/ematching/trigger_database.h | 6 ++- src/theory/quantifiers/instantiate.cpp | 8 ++-- .../quantifiers/sygus/synth_conjecture.cpp | 10 +++-- 21 files changed, 114 insertions(+), 120 deletions(-) delete mode 100644 src/options/outputc.cpp delete mode 100644 src/options/outputc.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 8f574dc82..914bc5d0c 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -63,8 +63,6 @@ libcvc5_add_sources( options/options_handler.h options/options_listener.h options/options_public.h - options/outputc.cpp - options/outputc.h options/set_language.cpp options/set_language.h preprocessing/assertion_pipeline.cpp diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 2a98ee36a..d33ef5b42 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -60,9 +60,9 @@ #include "options/option_exception.h" #include "options/options.h" #include "options/options_public.h" -#include "options/outputc.h" #include "options/smt_options.h" #include "proof/unsat_core.h" +#include "smt/env.h" #include "smt/model.h" #include "smt/smt_engine.h" #include "smt/smt_mode.h" @@ -7840,12 +7840,12 @@ Statistics Solver::getStatistics() const bool Solver::isOutputOn(const std::string& tag) const { - // `Output(tag)` may raise an `OptionException`, which we do not want to + // `isOutputOn(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 cvc5::OutputChannel.isOn(tag); + return d_smtEngine->getEnv().isOutputOn(tag); } catch (const cvc5::Exception& e) { @@ -7855,12 +7855,12 @@ bool Solver::isOutputOn(const std::string& tag) const std::ostream& Solver::getOutput(const std::string& tag) const { - // `Output(tag)` may raise an `OptionException`, which we do not want to + // `getOutput(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 Output(tag); + return d_smtEngine->getEnv().getOutput(tag); } catch (const cvc5::Exception& e) { diff --git a/src/options/outputc.cpp b/src/options/outputc.cpp deleted file mode 100644 index d9b7b346b..000000000 --- a/src/options/outputc.cpp +++ /dev/null @@ -1,35 +0,0 @@ -#include "options/outputc.h" - -#include - -namespace cvc5 { - -OutputC OutputChannel(&std::cout); - -Cvc5ostream OutputC::operator()(const options::OutputTag tag) const -{ - if (options::outputTagHolder()[static_cast(tag)]) - { - return Cvc5ostream(d_os); - } - else - { - return Cvc5ostream(); - } -} - -Cvc5ostream OutputC::operator()(const std::string& tag) const -{ - return (*this)(options::stringToOutputTag(tag)); -} - -bool OutputC::isOn(const options::OutputTag tag) const -{ - return options::outputTagHolder()[static_cast(tag)]; -} -bool OutputC::isOn(const std::string& tag) const -{ - return (*this).isOn(options::stringToOutputTag(tag)); -} - -} // namespace cvc5 diff --git a/src/options/outputc.h b/src/options/outputc.h deleted file mode 100644 index 7ad7cea76..000000000 --- a/src/options/outputc.h +++ /dev/null @@ -1,40 +0,0 @@ -#include "cvc5_private_library.h" - -#ifndef CVC5__OPTIONS__OUTPUTC_H -#define CVC5__OPTIONS__OUTPUTC_H - -#include - -#include "cvc5_export.h" -#include "base/output.h" -#include "options/base_options.h" - -namespace cvc5 { - -class OutputC -{ - public: - explicit OutputC(std::ostream* os) : d_os(os) {} - - Cvc5ostream operator()(const options::OutputTag tag) const; - Cvc5ostream operator()(const std::string& tag) const; - - bool isOn(const options::OutputTag tag) const; - bool isOn(const std::string& tag) const; - - private: - std::ostream* d_os; - -}; /* class OutputC */ - -extern OutputC OutputChannel CVC5_EXPORT; - -#ifdef CVC5_MUZZLE -#define Output ::cvc5::__cvc5_true() ? ::cvc5::nullStream : ::cvc5::OutputChannel -#else /* CVC5_MUZZLE */ -#define Output ::cvc5::OutputChannel -#endif /* CVC5_MUZZLE */ - -} - -#endif /* CVC5__OPTIONS__OUTPUTC_H */ diff --git a/src/smt/env.cpp b/src/smt/env.cpp index c77b8cfba..0ffe1c4b9 100644 --- a/src/smt/env.cpp +++ b/src/smt/env.cpp @@ -135,6 +135,27 @@ const Printer& Env::getPrinter() std::ostream& Env::getDumpOut() { return *d_options.base.out; } +bool Env::isOutputOn(options::OutputTag tag) const +{ + return d_options.base.outputTagHolder[static_cast(tag)]; +} +bool Env::isOutputOn(const std::string& tag) const +{ + return isOutputOn(options::stringToOutputTag(tag)); +} +std::ostream& Env::getOutput(options::OutputTag tag) const +{ + if (isOutputOn(tag)) + { + return *d_options.base.out; + } + return cvc5::null_os; +} +std::ostream& Env::getOutput(const std::string& tag) const +{ + return getOutput(options::stringToOutputTag(tag)); +} + Node Env::evaluate(TNode n, const std::vector& args, const std::vector& vals, diff --git a/src/smt/env.h b/src/smt/env.h index 2f2fe19ce..426749f5c 100644 --- a/src/smt/env.h +++ b/src/smt/env.h @@ -21,6 +21,7 @@ #include +#include "options/base_options.h" #include "options/options.h" #include "proof/method_id.h" #include "theory/logic_info.h" @@ -139,6 +140,30 @@ class Env */ std::ostream& getDumpOut(); + /** + * 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; + /** + * 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. 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& getOutput(options::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. + */ + std::ostream& getOutput(const std::string& tag) const; + /* Rewrite helpers--------------------------------------------------------- */ /** * Evaluate node n under the substitution args -> vals. For details, see diff --git a/src/theory/quantifiers/ematching/ho_trigger.cpp b/src/theory/quantifiers/ematching/ho_trigger.cpp index cb4bac254..a8ab760ce 100644 --- a/src/theory/quantifiers/ematching/ho_trigger.cpp +++ b/src/theory/quantifiers/ematching/ho_trigger.cpp @@ -35,6 +35,7 @@ namespace quantifiers { namespace inst { HigherOrderTrigger::HigherOrderTrigger( + Env& env, QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, @@ -42,7 +43,7 @@ HigherOrderTrigger::HigherOrderTrigger( Node q, std::vector& nodes, std::map >& ho_apps) - : Trigger(qs, qim, qr, tr, q, nodes), d_ho_var_apps(ho_apps) + : Trigger(env, qs, qim, qr, tr, q, nodes), d_ho_var_apps(ho_apps) { NodeManager* nm = NodeManager::currentNM(); // process the higher-order variable applications diff --git a/src/theory/quantifiers/ematching/ho_trigger.h b/src/theory/quantifiers/ematching/ho_trigger.h index 78b2e6c84..32633d233 100644 --- a/src/theory/quantifiers/ematching/ho_trigger.h +++ b/src/theory/quantifiers/ematching/ho_trigger.h @@ -92,7 +92,8 @@ class Trigger; class HigherOrderTrigger : public Trigger { public: - HigherOrderTrigger(QuantifiersState& qs, + HigherOrderTrigger(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr, diff --git a/src/theory/quantifiers/ematching/inst_strategy.cpp b/src/theory/quantifiers/ematching/inst_strategy.cpp index 94da9200a..644fba6f1 100644 --- a/src/theory/quantifiers/ematching/inst_strategy.cpp +++ b/src/theory/quantifiers/ematching/inst_strategy.cpp @@ -15,18 +15,20 @@ #include "theory/quantifiers/ematching/inst_strategy.h" +#include "smt/env.h" #include "theory/quantifiers/quantifiers_state.h" namespace cvc5 { namespace theory { namespace quantifiers { -InstStrategy::InstStrategy(inst::TriggerDatabase& td, +InstStrategy::InstStrategy(Env& env, + inst::TriggerDatabase& td, QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr) - : d_td(td), d_qstate(qs), d_qim(qim), d_qreg(qr), d_treg(tr) + : EnvObj(env), d_td(td), d_qstate(qs), d_qim(qim), d_qreg(qr), d_treg(tr) { } InstStrategy::~InstStrategy() {} diff --git a/src/theory/quantifiers/ematching/inst_strategy.h b/src/theory/quantifiers/ematching/inst_strategy.h index 575134710..da91e1f1c 100644 --- a/src/theory/quantifiers/ematching/inst_strategy.h +++ b/src/theory/quantifiers/ematching/inst_strategy.h @@ -19,8 +19,10 @@ #define CVC5__THEORY__QUANTIFIERS__INST_STRATEGY_H #include + #include "expr/node.h" #include "options/quantifiers_options.h" +#include "smt/env_obj.h" #include "theory/theory.h" namespace cvc5 { @@ -48,10 +50,11 @@ enum class InstStrategyStatus /** * A base class for instantiation strategies within E-matching. */ -class InstStrategy +class InstStrategy : protected EnvObj { public: - InstStrategy(inst::TriggerDatabase& td, + InstStrategy(Env& env, + inst::TriggerDatabase& td, QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp index e01a8fee2..8da91ec57 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp @@ -16,7 +16,6 @@ #include "theory/quantifiers/ematching/inst_strategy_e_matching.h" #include "options/base_options.h" -#include "options/outputc.h" #include "theory/quantifiers/ematching/pattern_term_selector.h" #include "theory/quantifiers/ematching/trigger_database.h" #include "theory/quantifiers/quant_relevance.h" @@ -65,13 +64,14 @@ struct sortTriggers { }; InstStrategyAutoGenTriggers::InstStrategyAutoGenTriggers( + Env& env, inst::TriggerDatabase& td, QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr, QuantRelevance* qrlv) - : InstStrategy(td, qs, qim, qr, tr), d_quant_rel(qrlv) + : InstStrategy(env, td, qs, qim, qr, tr), d_quant_rel(qrlv) { //how to select trigger terms d_tr_strategy = options::triggerSelMode(); @@ -150,8 +150,11 @@ 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; - Output(options::OutputTag::TRIGGER) - << "(no-trigger " << f << ")" << std::endl; + if (d_env.isOutputOn(options::OutputTag::TRIGGER)) + { + d_env.getOutput(options::OutputTag::TRIGGER) + << "(no-trigger " << f << ")" << std::endl; + } } } if (options::triggerActiveSelMode() != options::TriggerActiveSelMode::ALL) diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.h b/src/theory/quantifiers/ematching/inst_strategy_e_matching.h index fd3bb995d..7b074057e 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.h +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.h @@ -86,7 +86,8 @@ class InstStrategyAutoGenTriggers : public InstStrategy std::map d_hasUserPatterns; public: - InstStrategyAutoGenTriggers(inst::TriggerDatabase& td, + InstStrategyAutoGenTriggers(Env& env, + inst::TriggerDatabase& td, QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp index a937edf44..cdda020eb 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp @@ -27,12 +27,13 @@ namespace theory { namespace quantifiers { InstStrategyUserPatterns::InstStrategyUserPatterns( + Env& env, inst::TriggerDatabase& td, QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr) - : InstStrategy(td, qs, qim, qr, tr) + : InstStrategy(env, td, qs, qim, qr, tr) { } InstStrategyUserPatterns::~InstStrategyUserPatterns() {} diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h index 064958ce2..8b52c4333 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h @@ -35,7 +35,8 @@ namespace quantifiers { class InstStrategyUserPatterns : public InstStrategy { public: - InstStrategyUserPatterns(inst::TriggerDatabase& td, + InstStrategyUserPatterns(Env& env, + inst::TriggerDatabase& td, QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, diff --git a/src/theory/quantifiers/ematching/instantiation_engine.cpp b/src/theory/quantifiers/ematching/instantiation_engine.cpp index 62c5c2440..17023e6b9 100644 --- a/src/theory/quantifiers/ematching/instantiation_engine.cpp +++ b/src/theory/quantifiers/ematching/instantiation_engine.cpp @@ -42,7 +42,7 @@ InstantiationEngine::InstantiationEngine(Env& env, d_isup(), d_i_ag(), d_quants(), - d_trdb(qs, qim, qr, tr), + d_trdb(d_env, qs, qim, qr, tr), d_quant_rel(nullptr) { if (options::relevantTriggers()) @@ -54,13 +54,14 @@ InstantiationEngine::InstantiationEngine(Env& env, // user-provided patterns if (options::userPatternsQuant() != options::UserPatMode::IGNORE) { - d_isup.reset(new InstStrategyUserPatterns(d_trdb, qs, qim, qr, tr)); + d_isup.reset( + new InstStrategyUserPatterns(d_env, d_trdb, qs, qim, qr, tr)); d_instStrategies.push_back(d_isup.get()); } // auto-generated patterns d_i_ag.reset(new InstStrategyAutoGenTriggers( - d_trdb, qs, qim, qr, tr, d_quant_rel.get())); + d_env, d_trdb, qs, qim, qr, tr, d_quant_rel.get())); d_instStrategies.push_back(d_i_ag.get()); } } diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp index 63aabbfd6..b75c523ae 100644 --- a/src/theory/quantifiers/ematching/trigger.cpp +++ b/src/theory/quantifiers/ematching/trigger.cpp @@ -17,8 +17,8 @@ #include "expr/skolem_manager.h" #include "options/base_options.h" -#include "options/outputc.h" #include "options/quantifiers_options.h" +#include "smt/env.h" #include "theory/quantifiers/ematching/candidate_generator.h" #include "theory/quantifiers/ematching/inst_match_generator.h" #include "theory/quantifiers/ematching/inst_match_generator_multi.h" @@ -43,13 +43,14 @@ namespace quantifiers { namespace inst { /** trigger class constructor */ -Trigger::Trigger(QuantifiersState& qs, +Trigger::Trigger(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr, Node q, std::vector& nodes) - : d_qstate(qs), d_qim(qim), d_qreg(qr), d_treg(tr), d_quant(q) + : EnvObj(env), d_qstate(qs), d_qim(qim), d_qreg(qr), d_treg(tr), d_quant(q) { // We must ensure that the ground subterms of the trigger have been // preprocessed. @@ -77,11 +78,12 @@ Trigger::Trigger(QuantifiersState& qs, extNodes.push_back(ns); } d_trNode = NodeManager::currentNM()->mkNode(SEXPR, extNodes); - if (Output.isOn(options::OutputTag::TRIGGER)) + if (d_env.isOutputOn(options::OutputTag::TRIGGER)) { QuantAttributes& qa = d_qreg.getQuantAttributes(); - Output(options::OutputTag::TRIGGER) << "(trigger " << qa.quantToString(q) - << " " << d_trNode << ")" << std::endl; + d_env.getOutput(options::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/ematching/trigger.h b/src/theory/quantifiers/ematching/trigger.h index 944a082c0..dd69f682f 100644 --- a/src/theory/quantifiers/ematching/trigger.h +++ b/src/theory/quantifiers/ematching/trigger.h @@ -19,6 +19,7 @@ #define CVC5__THEORY__QUANTIFIERS__TRIGGER_H #include "expr/node.h" +#include "smt/env_obj.h" #include "theory/inference_id.h" namespace cvc5 { @@ -95,12 +96,14 @@ class InstMatchGenerator; * required to ensure the correctness of instantiation lemmas we generate. * */ -class Trigger { +class Trigger : protected EnvObj +{ friend class IMGenerator; public: /** trigger constructor */ - Trigger(QuantifiersState& qs, + Trigger(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr, diff --git a/src/theory/quantifiers/ematching/trigger_database.cpp b/src/theory/quantifiers/ematching/trigger_database.cpp index 711e6ab21..58f8d5f00 100644 --- a/src/theory/quantifiers/ematching/trigger_database.cpp +++ b/src/theory/quantifiers/ematching/trigger_database.cpp @@ -24,11 +24,12 @@ namespace theory { namespace quantifiers { namespace inst { -TriggerDatabase::TriggerDatabase(QuantifiersState& qs, +TriggerDatabase::TriggerDatabase(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr) - : d_qs(qs), d_qim(qim), d_qreg(qr), d_treg(tr) + : EnvObj(env), d_qs(qs), d_qim(qim), d_qreg(qr), d_treg(tr) { } TriggerDatabase::~TriggerDatabase() {} @@ -78,11 +79,12 @@ Trigger* TriggerDatabase::mkTrigger(Node q, Trigger* t; if (!hoApps.empty()) { - t = new HigherOrderTrigger(d_qs, d_qim, d_qreg, d_treg, q, trNodes, hoApps); + t = new HigherOrderTrigger( + d_env, d_qs, d_qim, d_qreg, d_treg, q, trNodes, hoApps); } else { - t = new Trigger(d_qs, d_qim, d_qreg, d_treg, q, trNodes); + t = new Trigger(d_env, d_qs, d_qim, d_qreg, d_treg, q, trNodes); } d_trie.addTrigger(trNodes, t); return t; diff --git a/src/theory/quantifiers/ematching/trigger_database.h b/src/theory/quantifiers/ematching/trigger_database.h index 8dbcde7bf..6535e1ae7 100644 --- a/src/theory/quantifiers/ematching/trigger_database.h +++ b/src/theory/quantifiers/ematching/trigger_database.h @@ -21,6 +21,7 @@ #include #include "expr/node.h" +#include "smt/env_obj.h" #include "theory/quantifiers/ematching/trigger_trie.h" namespace cvc5 { @@ -37,10 +38,11 @@ namespace inst { /** * A database of triggers, which manages how triggers are constructed. */ -class TriggerDatabase +class TriggerDatabase : protected EnvObj { public: - TriggerDatabase(QuantifiersState& qs, + TriggerDatabase(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr); diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index 2a3974d49..4d90fe95b 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -17,7 +17,6 @@ #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" @@ -696,7 +695,7 @@ void Instantiate::notifyEndRound() << " * " << i.second << " for " << i.first << std::endl; } } - if (Output.isOn(options::OutputTag::INST)) + if (d_env.isOutputOn(options::OutputTag::INST)) { bool req = !options::printInstFull(); for (std::pair& i : d_instDebugTemp) @@ -706,8 +705,9 @@ void Instantiate::notifyEndRound() { continue; } - Output(options::OutputTag::INST) << "(num-instantiations " << name << " " - << i.second << ")" << std::endl; + d_env.getOutput(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 22ba879d7..ab2a73cb0 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -20,7 +20,6 @@ #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" @@ -359,7 +358,7 @@ bool SynthConjecture::doCheck() } } - bool printDebug = Output.isOn(options::OutputTag::SYGUS); + bool printDebug = d_env.isOutputOn(options::OutputTag::SYGUS); if (!constructed_cand) { // get the model value of the relevant terms from the master module @@ -424,8 +423,11 @@ bool SynthConjecture::doCheck() } } Trace("sygus-engine") << std::endl; - Output(options::OutputTag::SYGUS) - << "(sygus-enum" << sygusEnumOut.str() << ")" << std::endl; + if (d_env.isOutputOn(options::OutputTag::SYGUS)) + { + d_env.getOutput(options::OutputTag::SYGUS) + << "(sygus-enum" << sygusEnumOut.str() << ")" << std::endl; + } } Assert(candidate_values.empty()); constructed_cand = d_master->constructCandidates( -- 2.30.2