From 13819c4ae33a103b1075e816772a305b16db9157 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 22 Feb 2021 17:19:20 -0600 Subject: Eliminate raw use of output channel and valuation in quantifiers (#5933) This makes all lemmas in quantifiers sent through the inference manager. It begins adding InferenceId values for some of these calls. All uses of Valuation are replaced by calls to QuantifiersState. --- src/theory/quantifiers/ematching/ho_trigger.cpp | 3 ++- src/theory/quantifiers/ematching/ho_trigger.h | 1 + .../quantifiers/ematching/inst_strategy_e_matching.cpp | 3 +++ .../ematching/inst_strategy_e_matching_user.cpp | 11 +++++++++-- src/theory/quantifiers/ematching/trigger.cpp | 16 ++++++++++------ src/theory/quantifiers/ematching/trigger.h | 6 ++++++ 6 files changed, 31 insertions(+), 9 deletions(-) (limited to 'src/theory/quantifiers/ematching') 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& nodes, std::map >& 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& 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 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 */ -- cgit v1.2.3