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.

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 8f574dc82be36435ba2aedb94c734c3e1b52af3f..914bc5d0cef20a59787d7d1b35f1e14f6638aaf7 100644 (file)
--- 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 2a98ee36a1522cfa3b9473dffb7d50eb659efc66..d33ef5b42d61d1470809899182ce293588c59113 100644 (file)
--- 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 (file)
index d9b7b34..0000000
--- a/src/options/outputc.cpp
+++ /dev/null
@@ -1,35 +0,0 @@
-#include "options/outputc.h"
-
-#include <iostream>
-
-namespace cvc5 {
-
-OutputC OutputChannel(&std::cout);
-
-Cvc5ostream OutputC::operator()(const options::OutputTag tag) const
-{
-  if (options::outputTagHolder()[static_cast<size_t>(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<size_t>(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 (file)
index 7ad7cea..0000000
--- 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 <iostream>
-
-#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 c77b8cfbacffb2b8b35a6b8c5020b4246257f017..0ffe1c4b95fc87fc1fed1bd02f795be73d38b4d6 100644 (file)
--- 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<size_t>(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<Node>& args,
                    const std::vector<Node>& vals,

diff --git a/src/smt/env.h b/src/smt/env.h
index 2f2fe19ce858f1d3d8caf7e576f153ef7401f817..426749f5cf3a8897ec2f12ff765eebdef428df14 100644 (file)
--- a/src/smt/env.h
+++ b/src/smt/env.h
@@ -21,6 +21,7 @@
 
 #include <memory>
 
+#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 cb4bac254426586a706ebde1ff3ae9139bb83647..a8ab760ce6f1ba826d4b193472a33a4ee61554fa 100644 (file)
--- 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<Node>& nodes,
     std::map<Node, std::vector<Node> >& 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 78b2e6c849b493420f17bab4cb8b6267ee7597da..32633d2330173e2cdd78aa4563e22c4f32dba65d 100644 (file)
--- 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 94da9200ad7757a96769b646c4b305106d4bf10e..644fba6f1b82c979a60dda4512bf1d4fab97165d 100644 (file)
--- 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 5751347103b6a795afaa59cad38ff1d7934cd6c8..da91e1f1ce51029a6a6051a6bba920b25028f876 100644 (file)
--- 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 <vector>
+
 #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 e01a8fee2ad3cee391ef289978235395f434a5b6..8da91ec57ae7a13f55243d0fcbf42a6152c215f7 100644 (file)
--- 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 fd3bb995d29659d91c341e648d37c2cc1274a016..7b074057e07ba2f82c774049aa426adb1efb6e36 100644 (file)
--- 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<Node, bool> 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 a937edf444a7a04c357b1a1ed8e548de259169a8..cdda020ebdfd1bd82a2af76b8430913d902a8cab 100644 (file)
--- 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 064958ce2e9f7af60bee147e3f6db53232ef1a0a..8b52c43333d493873aced1c1a2fb1acdff16763f 100644 (file)
--- 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 62c5c2440efc741ed88a0acc0aff792278d769b5..17023e6b985992ac246fbad282983a4491112293 100644 (file)
--- 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 63aabbfd6ebcb98beb68c4d6c63cb01802fd11d4..b75c523ae44c3582073f2a38546b21e1bdfff733 100644 (file)
--- 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<Node>& 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 944a082c086de51307ee5b094a211595c209d5bb..dd69f682f7779474bd0b0f9510c709ae3df60962 100644 (file)
--- 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 711e6ab21c871b50a4f825ae2f5bafc95c782e45..58f8d5f00f9b8c44f2051fd44ae8d5e02f0a4e67 100644 (file)
--- 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 8dbcde7bf20444c6ecb1d54ca5a77a3a5021a635..6535e1ae76d5c51601ee91c847066d48fd933fb8 100644 (file)
--- a/src/theory/quantifiers/ematching/trigger_database.h
+++ b/src/theory/quantifiers/ematching/trigger_database.h
@@ -21,6 +21,7 @@
 #include <vector>
 
 #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 2a3974d492fd7a49633f7ef2fa4e2da2a1fc2a5a..4d90fe95beecffe82cf089ce3334e0c668119947 100644 (file)
--- 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<const Node, uint32_t>& 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 22ba879d7dd31d74f1b42e420bf83543aef1f04c..ab2a73cb0adf8bcdd22a26d8ecd9e5aaf7a36de4 100644 (file)
--- 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(