diff options
Diffstat (limited to 'src/theory/quantifiers/ematching/trigger.cpp')
| -rw-r--r-- | src/theory/quantifiers/ematching/trigger.cpp | 14 |
1 files changed, 8 insertions, 6 deletions
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<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 ){ |