diff options
Diffstat (limited to 'src/theory/quantifiers/ematching/trigger.cpp')
| -rw-r--r-- | src/theory/quantifiers/ematching/trigger.cpp | 176 |
1 files changed, 6 insertions, 170 deletions
diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp index c93e1a99b..c739623bc 100644 --- a/src/theory/quantifiers/ematching/trigger.cpp +++ b/src/theory/quantifiers/ematching/trigger.cpp @@ -17,7 +17,6 @@ #include "expr/skolem_manager.h" #include "options/quantifiers_options.h" #include "theory/quantifiers/ematching/candidate_generator.h" -#include "theory/quantifiers/ematching/ho_trigger.h" #include "theory/quantifiers/ematching/inst_match_generator.h" #include "theory/quantifiers/ematching/inst_match_generator_multi.h" #include "theory/quantifiers/ematching/inst_match_generator_multi_linear.h" @@ -31,7 +30,6 @@ #include "theory/quantifiers/quantifiers_registry.h" #include "theory/quantifiers/quantifiers_state.h" #include "theory/quantifiers/term_util.h" -#include "theory/quantifiers_engine.h" #include "theory/valuation.h" using namespace CVC4::kind; @@ -42,19 +40,13 @@ namespace quantifiers { namespace inst { /** trigger class constructor */ -Trigger::Trigger(QuantifiersEngine* qe, - QuantifiersState& qs, +Trigger::Trigger(QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr, Node q, std::vector<Node>& nodes) - : d_quantEngine(qe), - d_qstate(qs), - d_qim(qim), - d_qreg(qr), - d_treg(tr), - d_quant(q) + : 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. @@ -74,14 +66,15 @@ Trigger::Trigger(QuantifiersEngine* qe, Trace("trigger") << " " << n << std::endl; } } + QuantifiersStatistics& stats = qs.getStats(); if( d_nodes.size()==1 ){ if (TriggerTermInfo::isSimpleTrigger(d_nodes[0])) { d_mg = new InstMatchGeneratorSimple(this, q, d_nodes[0]); - ++(qe->d_statistics.d_triggers); + ++(stats.d_triggers); }else{ d_mg = InstMatchGenerator::mkInstMatchGenerator(this, q, d_nodes[0]); - ++(qe->d_statistics.d_simple_triggers); + ++(stats.d_simple_triggers); } }else{ if( options::multiTriggerCache() ){ @@ -97,7 +90,7 @@ Trigger::Trigger(QuantifiersEngine* qe, Trace("multi-trigger") << " " << nc << std::endl; } } - ++(qe->d_statistics.d_multi_triggers); + ++(stats.d_multi_triggers); } Trace("trigger-debug") << "Finished making trigger." << std::endl; @@ -162,163 +155,6 @@ bool Trigger::sendInstantiation(InstMatch& m, InferenceId id) return sendInstantiation(m.d_vals, id); } -bool Trigger::mkTriggerTerms(Node q, - std::vector<Node>& nodes, - size_t nvars, - std::vector<Node>& trNodes) -{ - //only take nodes that contribute variables to the trigger when added - std::vector< Node > temp; - temp.insert( temp.begin(), nodes.begin(), nodes.end() ); - std::map< Node, bool > vars; - std::map< Node, std::vector< Node > > patterns; - size_t varCount = 0; - std::map< Node, std::vector< Node > > varContains; - for (const Node& pat : temp) - { - TermUtil::computeInstConstContainsForQuant(q, pat, varContains[pat]); - } - for (const Node& t : temp) - { - const std::vector<Node>& vct = varContains[t]; - bool foundVar = false; - for (const Node& v : vct) - { - Assert(TermUtil::getInstConstAttr(v) == q); - if( vars.find( v )==vars.end() ){ - varCount++; - vars[ v ] = true; - foundVar = true; - } - } - if( foundVar ){ - trNodes.push_back(t); - for (const Node& v : vct) - { - patterns[v].push_back(t); - } - } - if (varCount == nvars) - { - break; - } - } - if (varCount < nvars) - { - Trace("trigger-debug") << "Don't consider trigger since it does not contain specified number of variables." << std::endl; - Trace("trigger-debug") << nodes << std::endl; - //do not generate multi-trigger if it does not contain all variables - return false; - } - // now, minimize the trigger - for (size_t i = 0, tsize = trNodes.size(); i < tsize; i++) - { - bool keepPattern = false; - Node n = trNodes[i]; - const std::vector<Node>& vcn = varContains[n]; - for (const Node& v : vcn) - { - if (patterns[v].size() == 1) - { - keepPattern = true; - break; - } - } - if (!keepPattern) - { - // remove from pattern vector - for (const Node& v : vcn) - { - std::vector<Node>& pv = patterns[v]; - for (size_t k = 0, pvsize = pv.size(); k < pvsize; k++) - { - if (pv[k] == n) - { - pv.erase(pv.begin() + k, pv.begin() + k + 1); - break; - } - } - } - // remove from trigger nodes - trNodes.erase(trNodes.begin() + i, trNodes.begin() + i + 1); - i--; - } - } - return true; -} - -Trigger* Trigger::mkTrigger(QuantifiersEngine* qe, - QuantifiersState& qs, - QuantifiersInferenceManager& qim, - QuantifiersRegistry& qr, - TermRegistry& tr, - Node f, - std::vector<Node>& nodes, - bool keepAll, - int trOption, - size_t useNVars) -{ - std::vector< Node > trNodes; - if( !keepAll ){ - size_t nvars = useNVars == 0 ? f[0].getNumChildren() : useNVars; - if (!mkTriggerTerms(f, nodes, nvars, trNodes)) - { - return nullptr; - } - }else{ - trNodes.insert( trNodes.begin(), nodes.begin(), nodes.end() ); - } - - //check for duplicate? - if( trOption!=TR_MAKE_NEW ){ - Trigger* t = qe->getTriggerDatabase()->getTrigger( trNodes ); - if( t ){ - if( trOption==TR_GET_OLD ){ - //just return old trigger - return t; - }else{ - return nullptr; - } - } - } - - // check if higher-order - Trace("trigger-debug") << "Collect higher-order variable triggers..." - << std::endl; - std::map<Node, std::vector<Node> > ho_apps; - HigherOrderTrigger::collectHoVarApplyTerms(f, trNodes, ho_apps); - Trace("trigger-debug") << "...got " << ho_apps.size() - << " higher-order applications." << std::endl; - Trigger* t; - if (!ho_apps.empty()) - { - t = new HigherOrderTrigger(qe, qs, qim, qr, tr, f, trNodes, ho_apps); - } - else - { - t = new Trigger(qe, qs, qim, qr, tr, f, trNodes); - } - - qe->getTriggerDatabase()->addTrigger( trNodes, t ); - return t; -} - -Trigger* Trigger::mkTrigger(QuantifiersEngine* qe, - QuantifiersState& qs, - QuantifiersInferenceManager& qim, - QuantifiersRegistry& qr, - TermRegistry& tr, - Node f, - Node n, - bool keepAll, - int trOption, - size_t useNVars) -{ - std::vector< Node > nodes; - nodes.push_back( n ); - return mkTrigger(qe, qs, qim, qr, tr, f, nodes, keepAll, trOption, useNVars); -} - int Trigger::getActiveScore() { return d_mg->getActiveScore(); } Node Trigger::ensureGroundTermPreprocessed(Valuation& val, |