diff options
Diffstat (limited to 'src/theory/quantifiers/ematching/trigger.cpp')
| -rw-r--r-- | src/theory/quantifiers/ematching/trigger.cpp | 16 |
1 files changed, 10 insertions, 6 deletions
diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp index d8d3aa098..d57c3356e 100644 --- a/src/theory/quantifiers/ematching/trigger.cpp +++ b/src/theory/quantifiers/ematching/trigger.cpp @@ -25,6 +25,7 @@ #include "theory/quantifiers/instantiate.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/quantifiers_inference_manager.h" +#include "theory/quantifiers/quantifiers_state.h" #include "theory/quantifiers_engine.h" using namespace CVC4::kind; @@ -35,15 +36,16 @@ namespace inst { /** trigger class constructor */ Trigger::Trigger(QuantifiersEngine* qe, + quantifiers::QuantifiersState& qs, quantifiers::QuantifiersInferenceManager& qim, quantifiers::QuantifiersRegistry& qr, Node q, std::vector<Node>& nodes) - : d_quantEngine(qe), d_qim(qim), d_qreg(qr), d_quant(q) + : d_quantEngine(qe), d_qstate(qs), d_qim(qim), d_qreg(qr), d_quant(q) { // We must ensure that the ground subterms of the trigger have been // preprocessed. - Valuation& val = qe->getValuation(); + Valuation& val = d_qstate.getValuation(); for (const Node& n : nodes) { Node np = ensureGroundTermPreprocessed(val, n, d_groundTerms); @@ -114,7 +116,7 @@ uint64_t Trigger::addInstantiations() { // for each ground term t that does not exist in the equality engine, we // add a purification lemma of the form (k = t). - eq::EqualityEngine* ee = d_quantEngine->getState().getEqualityEngine(); + eq::EqualityEngine* ee = d_qstate.getEqualityEngine(); for (const Node& gt : d_groundTerms) { if (!ee->hasTerm(gt)) @@ -233,6 +235,7 @@ bool Trigger::mkTriggerTerms(Node q, } Trigger* Trigger::mkTrigger(QuantifiersEngine* qe, + quantifiers::QuantifiersState& qs, quantifiers::QuantifiersInferenceManager& qim, quantifiers::QuantifiersRegistry& qr, Node f, @@ -275,11 +278,11 @@ Trigger* Trigger::mkTrigger(QuantifiersEngine* qe, Trigger* t; if (!ho_apps.empty()) { - t = new HigherOrderTrigger(qe, qim, qr, f, trNodes, ho_apps); + t = new HigherOrderTrigger(qe, qs, qim, qr, f, trNodes, ho_apps); } else { - t = new Trigger(qe, qim, qr, f, trNodes); + t = new Trigger(qe, qs, qim, qr, f, trNodes); } qe->getTriggerDatabase()->addTrigger( trNodes, t ); @@ -287,6 +290,7 @@ Trigger* Trigger::mkTrigger(QuantifiersEngine* qe, } Trigger* Trigger::mkTrigger(QuantifiersEngine* qe, + quantifiers::QuantifiersState& qs, quantifiers::QuantifiersInferenceManager& qim, quantifiers::QuantifiersRegistry& qr, Node f, @@ -297,7 +301,7 @@ Trigger* Trigger::mkTrigger(QuantifiersEngine* qe, { std::vector< Node > nodes; nodes.push_back( n ); - return mkTrigger(qe, qim, qr, f, nodes, keepAll, trOption, useNVars); + return mkTrigger(qe, qs, qim, qr, f, nodes, keepAll, trOption, useNVars); } int Trigger::getActiveScore() { |