diff options
Diffstat (limited to 'src/theory/quantifiers/ematching')
6 files changed, 31 insertions, 9 deletions
diff --git a/src/theory/quantifiers/ematching/ho_trigger.cpp b/src/theory/quantifiers/ematching/ho_trigger.cpp index 875c74aa4..5df350fe5 100644 --- a/src/theory/quantifiers/ematching/ho_trigger.cpp +++ b/src/theory/quantifiers/ematching/ho_trigger.cpp @@ -29,12 +29,13 @@ namespace inst { HigherOrderTrigger::HigherOrderTrigger( QuantifiersEngine* qe, + quantifiers::QuantifiersState& qs, quantifiers::QuantifiersInferenceManager& qim, quantifiers::QuantifiersRegistry& qr, Node q, std::vector<Node>& nodes, std::map<Node, std::vector<Node> >& ho_apps) - : Trigger(qe, qim, qr, q, nodes), d_ho_var_apps(ho_apps) + : Trigger(qe, qs, qim, qr, 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 af7020bfc..b99a8504d 100644 --- a/src/theory/quantifiers/ematching/ho_trigger.h +++ b/src/theory/quantifiers/ematching/ho_trigger.h @@ -93,6 +93,7 @@ class HigherOrderTrigger : public Trigger private: HigherOrderTrigger(QuantifiersEngine* qe, + quantifiers::QuantifiersState& qs, quantifiers::QuantifiersInferenceManager& qim, quantifiers::QuantifiersRegistry& qr, Node q, diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp index 2a1e38c3c..e7635f200 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp @@ -283,6 +283,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ if (d_is_single_trigger[patTerms[0]]) { tr = Trigger::mkTrigger(d_quantEngine, + d_qstate, d_qim, d_qreg, f, @@ -321,6 +322,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ } // will possibly want to get an old trigger tr = Trigger::mkTrigger(d_quantEngine, + d_qstate, d_qim, d_qreg, f, @@ -364,6 +366,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ { d_single_trigger_gen[patTerms[index]] = true; Trigger* tr2 = Trigger::mkTrigger(d_quantEngine, + d_qstate, d_qim, d_qreg, f, 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 ca2f1bdc5..14913bdc1 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp @@ -107,6 +107,7 @@ InstStrategyStatus InstStrategyUserPatterns::process(Node q, for (size_t i = 0, usize = ugw.size(); i < usize; i++) { Trigger* t = Trigger::mkTrigger(d_quantEngine, + d_qstate, d_qim, d_qreg, q, @@ -170,8 +171,14 @@ void InstStrategyUserPatterns::addUserPattern(Node q, Node pat) d_user_gen_wait[q].push_back(nodes); return; } - Trigger* t = Trigger::mkTrigger( - d_quantEngine, d_qim, d_qreg, q, nodes, true, Trigger::TR_MAKE_NEW); + Trigger* t = Trigger::mkTrigger(d_quantEngine, + d_qstate, + d_qim, + d_qreg, + q, + nodes, + true, + Trigger::TR_MAKE_NEW); if (t) { d_user_gen[q].push_back(t); 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() { diff --git a/src/theory/quantifiers/ematching/trigger.h b/src/theory/quantifiers/ematching/trigger.h index 21888ff8f..014cf2185 100644 --- a/src/theory/quantifiers/ematching/trigger.h +++ b/src/theory/quantifiers/ematching/trigger.h @@ -30,6 +30,7 @@ namespace theory { class QuantifiersEngine; namespace quantifiers { +class QuantifiersState; class QuantifiersInferenceManager; class QuantifiersRegistry; } @@ -163,6 +164,7 @@ class Trigger { TR_RETURN_NULL //return null if a duplicate is found }; static Trigger* mkTrigger(QuantifiersEngine* qe, + quantifiers::QuantifiersState& qs, quantifiers::QuantifiersInferenceManager& qim, quantifiers::QuantifiersRegistry& qr, Node q, @@ -172,6 +174,7 @@ class Trigger { size_t useNVars = 0); /** single trigger version that calls the above function */ static Trigger* mkTrigger(QuantifiersEngine* qe, + quantifiers::QuantifiersState& qs, quantifiers::QuantifiersInferenceManager& qim, quantifiers::QuantifiersRegistry& qr, Node q, @@ -196,6 +199,7 @@ class Trigger { protected: /** trigger constructor, intentionally protected (use Trigger::mkTrigger). */ Trigger(QuantifiersEngine* ie, + quantifiers::QuantifiersState& qs, quantifiers::QuantifiersInferenceManager& qim, quantifiers::QuantifiersRegistry& qr, Node q, @@ -245,6 +249,8 @@ class Trigger { std::vector<Node> d_groundTerms; /** The quantifiers engine associated with this trigger. */ QuantifiersEngine* d_quantEngine; + /** Reference to the quantifiers state */ + quantifiers::QuantifiersState& d_qstate; /** Reference to the quantifiers inference manager */ quantifiers::QuantifiersInferenceManager& d_qim; /** The quantifiers registry */ |