From 36b5281d3a4d58df5a4e68eca3d41568f1650769 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Sun, 24 Jan 2021 13:13:06 -0600 Subject: [PATCH] Initial cleaning of triggers (#5795) In preparation for splitting trigger.h/cpp into multiple files. This updates the code to conform to guidelines. No major changes, apart from a heuristic related to "pure theory triggers" is deleted and simplified. --- src/options/quantifiers_options.toml | 8 - .../quantifiers/ematching/ho_trigger.cpp | 10 +- src/theory/quantifiers/ematching/ho_trigger.h | 4 +- .../ematching/inst_strategy_e_matching.cpp | 3 +- src/theory/quantifiers/ematching/trigger.cpp | 771 ++++++++++-------- src/theory/quantifiers/ematching/trigger.h | 41 +- 6 files changed, 435 insertions(+), 402 deletions(-) diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 9027e7a94..3499da7de 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -263,14 +263,6 @@ header = "options/quantifiers_options.h" default = "false" help = "purify triggers, e.g. f( x+1 ) becomes f( y ), x mapsto y-1" -[[option]] - name = "pureThTriggers" - category = "regular" - long = "pure-th-triggers" - type = "bool" - default = "false" - help = "use pure theory terms as single triggers" - [[option]] name = "partialTriggers" category = "regular" diff --git a/src/theory/quantifiers/ematching/ho_trigger.cpp b/src/theory/quantifiers/ematching/ho_trigger.cpp index 4672c10c7..cdfb9c85c 100644 --- a/src/theory/quantifiers/ematching/ho_trigger.cpp +++ b/src/theory/quantifiers/ematching/ho_trigger.cpp @@ -186,12 +186,12 @@ void HigherOrderTrigger::collectHoVarApplyTerms( } } -int HigherOrderTrigger::addInstantiations() +uint64_t HigherOrderTrigger::addInstantiations() { // call the base class implementation - int addedFoLemmas = Trigger::addInstantiations(); + uint64_t addedFoLemmas = Trigger::addInstantiations(); // also adds predicate lemms to force app completion - int addedHoLemmas = addHoTypeMatchPredicateLemmas(); + uint64_t addedHoLemmas = addHoTypeMatchPredicateLemmas(); return addedHoLemmas + addedFoLemmas; } @@ -460,14 +460,14 @@ bool HigherOrderTrigger::sendInstantiationArg(InstMatch& m, } } -int HigherOrderTrigger::addHoTypeMatchPredicateLemmas() +uint64_t HigherOrderTrigger::addHoTypeMatchPredicateLemmas() { if (d_ho_var_types.empty()) { return 0; } Trace("ho-quant-trigger") << "addHoTypeMatchPredicateLemmas..." << std::endl; - unsigned numLemmas = 0; + uint64_t numLemmas = 0; // this forces expansion of APPLY_UF terms to curried HO_APPLY chains quantifiers::TermDb* tdb = d_quantEngine->getTermDatabase(); unsigned size = tdb->getNumOperators(); diff --git a/src/theory/quantifiers/ematching/ho_trigger.h b/src/theory/quantifiers/ematching/ho_trigger.h index a369aa7c5..d9636cd65 100644 --- a/src/theory/quantifiers/ematching/ho_trigger.h +++ b/src/theory/quantifiers/ematching/ho_trigger.h @@ -122,7 +122,7 @@ class HigherOrderTrigger : public Trigger * Extends Trigger::addInstantiations to also send * lemmas based on addHoTypeMatchPredicateLemmas. */ - int addInstantiations() override; + uint64_t addInstantiations() override; protected: /** @@ -158,7 +158,7 @@ class HigherOrderTrigger : public Trigger * * TODO: we may eliminate this based on how github issue #1115 is resolved. */ - int addHoTypeMatchPredicateLemmas(); + uint64_t addHoTypeMatchPredicateLemmas(); /** send instantiation * * Sends an instantiation that is equivalent to m via diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp index 513897cc9..7dcb9b797 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp @@ -561,7 +561,8 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ void InstStrategyAutoGenTriggers::addPatternToPool( Node q, Node pat, unsigned num_fv, Node mpat ) { d_pat_to_mpat[pat] = mpat; unsigned num_vars = options::partialTriggers() ? d_num_trigger_vars[q] : q[0].getNumChildren(); - if( num_fv==num_vars && ( options::pureThTriggers() || !Trigger::isPureTheoryTrigger( pat ) ) ){ + if (num_fv == num_vars) + { d_patTerms[0][q].push_back( pat ); d_is_single_trigger[ pat ] = true; }else{ diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp index a111e0221..4d6dd9f58 100644 --- a/src/theory/quantifiers/ematching/trigger.cpp +++ b/src/theory/quantifiers/ematching/trigger.cpp @@ -67,8 +67,10 @@ Trigger::Trigger(QuantifiersEngine* qe, Node q, std::vector& nodes) if( d_nodes.size()==1 ){ if( isSimpleTrigger( d_nodes[0] ) ){ d_mg = new InstMatchGeneratorSimple(q, d_nodes[0], qe); + ++(qe->d_statistics.d_triggers); }else{ d_mg = InstMatchGenerator::mkInstMatchGenerator(q, d_nodes[0], qe); + ++(qe->d_statistics.d_simple_triggers); } }else{ if( options::multiTriggerCache() ){ @@ -76,17 +78,13 @@ Trigger::Trigger(QuantifiersEngine* qe, Node q, std::vector& nodes) }else{ d_mg = InstMatchGenerator::mkInstMatchGeneratorMulti(q, d_nodes, qe); } - } - if( d_nodes.size()==1 ){ - if( isSimpleTrigger( d_nodes[0] ) ){ - ++(qe->d_statistics.d_triggers); - }else{ - ++(qe->d_statistics.d_simple_triggers); - } - }else{ - Trace("multi-trigger") << "Trigger for " << q << ": " << std::endl; - for( unsigned i=0; id_statistics.d_multi_triggers); } @@ -107,23 +105,22 @@ void Trigger::reset( Node eqc ){ d_mg->reset( eqc, d_quantEngine ); } -Node Trigger::getInstPattern(){ +bool Trigger::isMultiTrigger() const { return d_nodes.size() > 1; } + +Node Trigger::getInstPattern() const +{ return NodeManager::currentNM()->mkNode( INST_PATTERN, d_nodes ); } -int Trigger::addInstantiations() +uint64_t Trigger::addInstantiations() { - int addedLemmas = d_mg->addInstantiations(d_quant, d_quantEngine, this); - if( addedLemmas>0 ){ - if (Debug.isOn("inst-trigger")) + uint64_t addedLemmas = d_mg->addInstantiations(d_quant, d_quantEngine, this); + if (Debug.isOn("inst-trigger")) + { + if (addedLemmas > 0) { Debug("inst-trigger") << "Added " << addedLemmas - << " lemmas, trigger was "; - for (unsigned i = 0; i < d_nodes.size(); i++) - { - Debug("inst-trigger") << d_nodes[i] << " "; - } - Debug("inst-trigger") << std::endl; + << " lemmas, trigger was " << d_nodes << std::endl; } } return addedLemmas; @@ -134,7 +131,11 @@ bool Trigger::sendInstantiation(InstMatch& m) return d_quantEngine->getInstantiate()->addInstantiation(d_quant, m); } -bool Trigger::mkTriggerTerms( Node q, std::vector< Node >& nodes, unsigned n_vars, std::vector< Node >& trNodes ) { +bool Trigger::mkTriggerTerms(Node q, + std::vector& nodes, + size_t nvars, + std::vector& trNodes) +{ //only take nodes that contribute variables to the trigger when added std::vector< Node > temp; temp.insert( temp.begin(), nodes.begin(), nodes.end() ); @@ -147,10 +148,12 @@ bool Trigger::mkTriggerTerms( Node q, std::vector< Node >& nodes, unsigned n_var quantifiers::TermUtil::computeInstConstContainsForQuant( q, pat, varContains[pat]); } - for( unsigned i=0; i& vct = varContains[t]; bool foundVar = false; - for( unsigned j=0; j& nodes, unsigned n_var } } if( foundVar ){ - trNodes.push_back( temp[i] ); - for( unsigned j=0; j& vcn = varContains[n]; + for (const Node& v : vcn) + { + if (patterns[v].size() == 1) + { + keepPattern = true; + break; } - if( !keepPattern ){ - //remove from pattern vector - for( unsigned j=0; j& 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--; } + // remove from trigger nodes + trNodes.erase(trNodes.begin() + i, trNodes.begin() + i + 1); + i--; } } return true; } -Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes, bool keepAll, int trOption, unsigned use_n_vars ){ +Trigger* Trigger::mkTrigger(QuantifiersEngine* qe, + Node f, + std::vector& nodes, + bool keepAll, + int trOption, + size_t useNVars) +{ std::vector< Node > trNodes; if( !keepAll ){ - unsigned n_vars = use_n_vars==0 ? f[0].getNumChildren() : use_n_vars; - if( !mkTriggerTerms( f, nodes, n_vars, trNodes ) ){ - return NULL; + 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() ); @@ -229,7 +243,7 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& //just return old trigger return t; }else{ - return NULL; + return nullptr; } } } @@ -255,42 +269,54 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& return t; } -Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, Node n, bool keepAll, int trOption, unsigned use_n_vars ){ +Trigger* Trigger::mkTrigger(QuantifiersEngine* qe, + Node f, + Node n, + bool keepAll, + int trOption, + size_t useNVars) +{ std::vector< Node > nodes; nodes.push_back( n ); - return mkTrigger( qe, f, nodes, keepAll, trOption, use_n_vars ); + return mkTrigger(qe, f, nodes, keepAll, trOption, useNVars); } bool Trigger::isUsable( Node n, Node q ){ - if( quantifiers::TermUtil::getInstConstAttr(n)==q ){ - if( isAtomicTrigger( n ) ){ - for( unsigned i=0; i coeffs; - if (options::purifyTriggers()) + if (quantifiers::TermUtil::getInstConstAttr(n) != q) + { + return true; + } + if (isAtomicTrigger(n)) + { + for (const Node& nc : n) + { + if (!isUsable(nc, q)) { - Node x = getInversionVariable( n ); - if( !x.isNull() ){ - return true; - } + return false; } } - return false; - }else{ return true; } + else if (n.getKind() == INST_CONSTANT) + { + return true; + } + std::map coeffs; + if (options::purifyTriggers()) + { + Node x = getInversionVariable(n); + if (!x.isNull()) + { + return true; + } + } + return false; } Node Trigger::getIsUsableEq( Node q, Node n ) { Assert(isRelationalTrigger(n)); - for( unsigned i=0; i<2; i++) { + for (size_t i = 0; i < 2; i++) + { if( isUsableEqTerms( q, n[i], n[1-i] ) ){ if( i==1 && n.getKind()==EQUAL && !quantifiers::TermUtil::hasInstConstAttr(n[0]) ){ return NodeManager::currentNM()->mkNode( n.getKind(), n[1], n[0] ); @@ -349,8 +375,9 @@ Node Trigger::getIsUsableTrigger( Node n, Node q ) { pol = !pol; n = n[0]; } + NodeManager* nm = NodeManager::currentNM(); if( n.getKind()==INST_CONSTANT ){ - return pol ? n : NodeManager::currentNM()->mkNode( EQUAL, n, NodeManager::currentNM()->mkConst( true ) ).notNode(); + return pol ? n : nm->mkNode(EQUAL, n, nm->mkConst(true)).notNode(); }else if( isRelationalTrigger( n ) ){ Node rtr = getIsUsableEq( q, n ); if( rtr.isNull() && n[0].getType().isReal() ){ @@ -388,11 +415,15 @@ Node Trigger::getIsUsableTrigger( Node n, Node q ) { Trace("relational-trigger") << " return : " << rtr2 << std::endl; return rtr2; } - }else{ - Trace("trigger-debug") << n << " usable : " << ( quantifiers::TermUtil::getInstConstAttr(n)==q ) << " " << isAtomicTrigger( n ) << " " << isUsable( n, q ) << std::endl; - if( isUsableAtomicTrigger( n, q ) ){ - return pol ? n : NodeManager::currentNM()->mkNode( EQUAL, n, NodeManager::currentNM()->mkConst( true ) ).notNode(); - } + return Node::null(); + } + Trace("trigger-debug") << n << " usable : " + << (quantifiers::TermUtil::getInstConstAttr(n) == q) + << " " << isAtomicTrigger(n) << " " << isUsable(n, q) + << std::endl; + if (isUsableAtomicTrigger(n, q)) + { + return pol ? n : nm->mkNode(EQUAL, n, nm->mkConst(true)).notNode(); } return Node::null(); } @@ -437,19 +468,23 @@ bool Trigger::isSimpleTrigger( Node n ){ t = t[0]; } } - if( isAtomicTrigger( t ) ){ - for( unsigned i=0; i >::iterator itv = visited.find( n ); - if( itv==visited.end() ){ - visited[ n ].clear(); - Trace("auto-gen-trigger-debug2") << "Collect pat terms " << n << " " << pol << " " << hasPol << " " << epol << " " << hasEPol << std::endl; - if( n.getKind()!=FORALL && n.getKind()!=INST_CONSTANT ){ - Node nu; - bool nu_single = false; - if( knowIsUsable ){ - nu = n; - }else if( n.getKind()!=NOT && std::find( exclude.begin(), exclude.end(), n )==exclude.end() ){ - nu = getIsUsableTrigger( n, q ); - if( !nu.isNull() && nu!=n ){ - collectPatTerms2( q, nu, visited, tinfo, tstrt, exclude, added, pol, hasPol, epol, hasEPol, true ); - // copy to n - visited[n].insert( visited[n].end(), added.begin(), added.end() ); - return; - } + if (itv != visited.end()) + { + // already visited + for (const Node& t : itv->second) + { + if (std::find(added.begin(), added.end(), t) == added.end()) + { + added.push_back(t); } - if( !nu.isNull() ){ - Assert(nu == n); - Assert(nu.getKind() != NOT); - Trace("auto-gen-trigger-debug2") << "...found usable trigger : " << nu << std::endl; - Node reqEq; - if( nu.getKind()==EQUAL ){ - if( isAtomicTrigger( nu[0] ) && !quantifiers::TermUtil::hasInstConstAttr(nu[1]) ){ - if( hasPol ){ - reqEq = nu[1]; - } - nu = nu[0]; - } + } + return; + } + visited[n].clear(); + Trace("auto-gen-trigger-debug2") + << "Collect pat terms " << n << " " << pol << " " << hasPol << " " << epol + << " " << hasEPol << std::endl; + Kind nk = n.getKind(); + if (nk == FORALL || nk == INST_CONSTANT) + { + // do not traverse beneath quantified formulas + return; + } + Node nu; + bool nu_single = false; + if (knowIsUsable) + { + nu = n; + } + else if (nk != NOT + && std::find(exclude.begin(), exclude.end(), n) == exclude.end()) + { + nu = getIsUsableTrigger(n, q); + if (!nu.isNull() && nu != n) + { + collectPatTerms2(q, + nu, + visited, + tinfo, + tstrt, + exclude, + added, + pol, + hasPol, + epol, + hasEPol, + true); + // copy to n + visited[n].insert(visited[n].end(), added.begin(), added.end()); + return; + } + } + if (!nu.isNull()) + { + Assert(nu == n); + Assert(nu.getKind() != NOT); + Trace("auto-gen-trigger-debug2") + << "...found usable trigger : " << nu << std::endl; + Node reqEq; + if (nu.getKind() == EQUAL) + { + if (isAtomicTrigger(nu[0]) + && !quantifiers::TermUtil::hasInstConstAttr(nu[1])) + { + if (hasPol) + { + reqEq = nu[1]; } - Assert(reqEq.isNull() - || !quantifiers::TermUtil::hasInstConstAttr(reqEq)); - Assert(isUsableTrigger(nu, q)); - //tinfo.find( nu )==tinfo.end() - Trace("auto-gen-trigger-debug2") << "...add usable trigger : " << nu << std::endl; - tinfo[ nu ].init( q, nu, hasEPol ? ( epol ? 1 : -1 ) : 0, reqEq ); - nu_single = tinfo[ nu ].d_fv.size()==q[0].getNumChildren(); + nu = nu[0]; } - Node nrec = nu.isNull() ? n : nu; - std::vector< Node > added2; - for( unsigned i=0; i= tinfo[added2[i]].d_weight) - { - // discard if we added a subterm as a trigger with all - // variables that nu has - Trace("auto-gen-trigger-debug2") - << "......subsumes parent " << tinfo[nu].d_weight << " " - << tinfo[added2[i]].d_weight << "." << std::endl; - rm_nu = true; - } - } - if( std::find( added.begin(), added.end(), added2[i] )==added.end() ){ - added.push_back( added2[i] ); - } - } - } - } - if (rm_nu - && (tstrt == options::TriggerSelMode::MIN - || (tstrt == options::TriggerSelMode::MIN_SINGLE_ALL - && nu_single))) + } + Assert(reqEq.isNull() || !quantifiers::TermUtil::hasInstConstAttr(reqEq)); + Assert(isUsableTrigger(nu, q)); + // tinfo.find( nu )==tinfo.end() + Trace("auto-gen-trigger-debug2") + << "...add usable trigger : " << nu << std::endl; + tinfo[nu].init(q, nu, hasEPol ? (epol ? 1 : -1) : 0, reqEq); + nu_single = tinfo[nu].d_fv.size() == q[0].getNumChildren(); + } + Node nrec = nu.isNull() ? n : nu; + std::vector added2; + for (size_t i = 0, nrecc = nrec.getNumChildren(); i < nrecc; i++) + { + bool newHasPol, newPol; + bool newHasEPol, newEPol; + QuantPhaseReq::getPolarity(nrec, i, hasPol, pol, newHasPol, newPol); + QuantPhaseReq::getEntailPolarity( + nrec, i, hasEPol, epol, newHasEPol, newEPol); + collectPatTerms2(q, + nrec[i], + visited, + tinfo, + tstrt, + exclude, + added2, + newPol, + newHasPol, + newEPol, + newHasEPol); + } + // if this is not a usable trigger, don't worry about caching the results, + // since triggers do not contain non-usable subterms + if (nu.isNull()) + { + return; + } + bool rm_nu = false; + for (size_t i = 0, asize = added2.size(); i < asize; i++) + { + Trace("auto-gen-trigger-debug2") << "..." << nu << " added child " << i + << " : " << added2[i] << std::endl; + Assert(added2[i] != nu); + // if child was not already removed + if (tinfo.find(added2[i]) != tinfo.end()) + { + if (tstrt == options::TriggerSelMode::MAX + || (tstrt == options::TriggerSelMode::MIN_SINGLE_MAX && !nu_single)) + { + // discard all subterms + // do not remove if it has smaller weight + if (tinfo[nu].d_weight <= tinfo[added2[i]].d_weight) { - tinfo.erase( nu ); + Trace("auto-gen-trigger-debug2") << "......remove it." << std::endl; + visited[added2[i]].clear(); + tinfo.erase(added2[i]); } - else + } + else + { + if (tinfo[nu].d_fv.size() == tinfo[added2[i]].d_fv.size()) { - if( std::find( added.begin(), added.end(), nu )==added.end() ){ - added.push_back( nu ); + if (tinfo[nu].d_weight >= tinfo[added2[i]].d_weight) + { + // discard if we added a subterm as a trigger with all + // variables that nu has + Trace("auto-gen-trigger-debug2") + << "......subsumes parent " << tinfo[nu].d_weight << " " + << tinfo[added2[i]].d_weight << "." << std::endl; + rm_nu = true; } } - visited[n].insert( visited[n].end(), added.begin(), added.end() ); - } - } - }else{ - for( unsigned i=0; isecond.size(); ++i ){ - Node t = itv->second[i]; - if( std::find( added.begin(), added.end(), t )==added.end() ){ - added.push_back( t ); + if (std::find(added.begin(), added.end(), added2[i]) == added.end()) + { + added.push_back(added2[i]); + } } } } -} - -bool Trigger::isPureTheoryTrigger( Node n ) { - if( n.getKind()==APPLY_UF || n.getKind()==VARIABLE || n.getKind()==SKOLEM ){ //|| !quantifiers::TermUtil::hasInstConstAttr( n ) ){ - return false; - }else{ - for( unsigned i=0; i& vars, std::vector< Node >& patTerms ) { - if( !n.getType().isBoolean() && n.getKind()==APPLY_UF ){ - if( std::find( patTerms.begin(), patTerms.end(), n )==patTerms.end() ){ - bool hasVar = false; - for( unsigned i=0; i& patTerms, @@ -698,15 +737,16 @@ void Trigger::collectPatTerms(Node q, } std::vector< Node > added; collectPatTerms2( q, n, visited, tinfo, tstrt, exclude, added, true, true, false, true ); - for( std::map< Node, TriggerTermInfo >::iterator it = tinfo.begin(); it != tinfo.end(); ++it ){ - patTerms.push_back( it->first ); + for (const std::pair& t : tinfo) + { + patTerms.push_back(t.first); } } int Trigger::isTriggerInstanceOf(Node n1, Node n2, - std::vector& fv1, - std::vector& fv2) + const std::vector& fv1, + const std::vector& fv2) { Assert(n1 != n2); int status = 0; @@ -726,73 +766,72 @@ int Trigger::isTriggerInstanceOf(Node n1, { cur = visit.back(); visit.pop_back(); - if (visited.find(cur) == visited.end()) + if (visited.find(cur) != visited.end()) { - visited.insert(cur); - cur1 = cur.first; - cur2 = cur.second; - Assert(cur1 != cur2); - // recurse if they have the same operator - if (cur1.hasOperator() && cur2.hasOperator() - && cur1.getNumChildren() == cur2.getNumChildren() - && cur1.getOperator() == cur2.getOperator() - && cur1.getOperator().getKind()!=INST_CONSTANT) + continue; + } + visited.insert(cur); + cur1 = cur.first; + cur2 = cur.second; + Assert(cur1 != cur2); + // recurse if they have the same operator + if (cur1.hasOperator() && cur2.hasOperator() + && cur1.getNumChildren() == cur2.getNumChildren() + && cur1.getOperator() == cur2.getOperator() + && cur1.getOperator().getKind() != INST_CONSTANT) + { + visit.push_back(std::pair(cur1, cur2)); + for (size_t i = 0, size = cur1.getNumChildren(); i < size; i++) { - visit.push_back(std::pair(cur1, cur2)); - for (unsigned i = 0, size = cur1.getNumChildren(); i < size; i++) + if (cur1[i] != cur2[i]) { - if (cur1[i] != cur2[i]) - { - visit.push_back(std::pair(cur1[i], cur2[i])); - } - else if (cur1[i].getKind() == INST_CONSTANT) + visit.push_back(std::pair(cur1[i], cur2[i])); + } + else if (cur1[i].getKind() == INST_CONSTANT) + { + if (subs_vars.find(cur1[i]) != subs_vars.end()) { - if (subs_vars.find(cur1[i]) != subs_vars.end()) - { - return 0; - } - // the variable must map to itself in the substitution - subs_vars.insert(cur1[i]); + return 0; } + // the variable must map to itself in the substitution + subs_vars.insert(cur1[i]); } } - else + continue; + } + bool success = false; + // check if we are in a unifiable instance case + // must be only this case + for (unsigned r = 0; r < 2; r++) + { + if (status == 0 || ((status == 1) == (r == 0))) { - bool success = false; - // check if we are in a unifiable instance case - // must be only this case - for (unsigned r = 0; r < 2; r++) + TNode curi = r == 0 ? cur1 : cur2; + if (curi.getKind() == INST_CONSTANT + && subs_vars.find(curi) == subs_vars.end()) { - if (status == 0 || ((status == 1) == (r == 0))) + TNode curj = r == 0 ? cur2 : cur1; + // RHS must be a simple trigger + if (getTriggerWeight(curj) == 0) { - TNode curi = r == 0 ? cur1 : cur2; - if (curi.getKind() == INST_CONSTANT - && subs_vars.find(curi) == subs_vars.end()) + // must occur in the free variables in the other + const std::vector& free_vars = r == 0 ? fv2 : fv1; + if (std::find(free_vars.begin(), free_vars.end(), curi) + != free_vars.end()) { - TNode curj = r == 0 ? cur2 : cur1; - // RHS must be a simple trigger - if (getTriggerWeight(curj) == 0) - { - // must occur in the free variables in the other - std::vector& free_vars = r == 0 ? fv2 : fv1; - if (std::find(free_vars.begin(), free_vars.end(), curi) - != free_vars.end()) - { - status = r == 0 ? 1 : -1; - subs_vars.insert(curi); - success = true; - break; - } - } + status = r == 0 ? 1 : -1; + subs_vars.insert(curi); + success = true; + break; } } } - if (!success) - { - return 0; - } } } + if (!success) + { + return 0; + } } while (!visit.empty()); return status; } @@ -800,41 +839,43 @@ int Trigger::isTriggerInstanceOf(Node n1, void Trigger::filterTriggerInstances(std::vector& nodes) { std::map > fvs; - for (unsigned i = 0, size = nodes.size(); i < size; i++) + for (size_t i = 0, size = nodes.size(); i < size; i++) { quantifiers::TermUtil::computeInstConstContains(nodes[i], fvs[i]); } std::vector active; active.resize(nodes.size(), true); - for (unsigned i = 0, size = nodes.size(); i < size; i++) + for (size_t i = 0, size = nodes.size(); i < size; i++) { std::vector& fvsi = fvs[i]; - if (active[i]) + if (!active[i]) { - for (unsigned j = i + 1, size2 = nodes.size(); j < size2; j++) + continue; + } + for (size_t j = i + 1, size2 = nodes.size(); j < size2; j++) + { + if (!active[j]) { - if (active[j]) - { - int result = isTriggerInstanceOf(nodes[i], nodes[j], fvsi, fvs[j]); - if (result == 1) - { - Trace("filter-instances") << nodes[j] << " is an instance of " - << nodes[i] << std::endl; - active[i] = false; - break; - } - else if (result == -1) - { - Trace("filter-instances") << nodes[i] << " is an instance of " - << nodes[j] << std::endl; - active[j] = false; - } - } + continue; + } + int result = isTriggerInstanceOf(nodes[i], nodes[j], fvsi, fvs[j]); + if (result == 1) + { + Trace("filter-instances") + << nodes[j] << " is an instance of " << nodes[i] << std::endl; + active[i] = false; + break; + } + else if (result == -1) + { + Trace("filter-instances") + << nodes[i] << " is an instance of " << nodes[j] << std::endl; + active[j] = false; } } } std::vector temp; - for (unsigned i = 0; i < nodes.size(); i++) + for (size_t i = 0, nsize = nodes.size(); i < nsize; i++) { if (active[i]) { @@ -846,14 +887,20 @@ void Trigger::filterTriggerInstances(std::vector& nodes) } Node Trigger::getInversionVariable( Node n ) { - if( n.getKind()==INST_CONSTANT ){ + Kind nk = n.getKind(); + if (nk == INST_CONSTANT) + { return n; - }else if( n.getKind()==PLUS || n.getKind()==MULT ){ + } + else if (nk == PLUS || nk == MULT) + { Node ret; - for( unsigned i=0; i(); - if( r!=Rational(-1) && r!=Rational(1) ){ - Trace("var-trigger-debug") << "No : not integer coefficient " << n << std::endl; - return Node::null(); - } - } - */ } } return ret; - }else{ - Trace("var-trigger-debug") << "No : unsupported operator " << n << "." << std::endl; } + Trace("var-trigger-debug") + << "No : unsupported operator " << n << "." << std::endl; return Node::null(); } Node Trigger::getInversion( Node n, Node x ) { - if( n.getKind()==INST_CONSTANT ){ + Kind nk = n.getKind(); + if (nk == INST_CONSTANT) + { return x; - }else if( n.getKind()==PLUS || n.getKind()==MULT ){ + } + else if (nk == PLUS || nk == MULT) + { + NodeManager* nm = NodeManager::currentNM(); int cindex = -1; bool cindexSet = false; - for( unsigned i=0; imkNode( MINUS, x, n[i] ); - }else if( n.getKind()==MULT ){ - Assert(n[i].isConst()); + for (size_t i = 0, nchild = n.getNumChildren(); i < nchild; i++) + { + Node nc = n[i]; + if (!quantifiers::TermUtil::hasInstConstAttr(nc)) + { + if (nk == PLUS) + { + x = nm->mkNode(MINUS, x, nc); + } + else if (nk == MULT) + { + Assert(nc.isConst()); if( x.getType().isInteger() ){ - Node coeff = NodeManager::currentNM()->mkConst( n[i].getConst().abs() ); - if( !n[i].getConst().abs().isOne() ){ - x = NodeManager::currentNM()->mkNode( INTS_DIVISION_TOTAL, x, coeff ); + Node coeff = nm->mkConst(nc.getConst().abs()); + if (!nc.getConst().abs().isOne()) + { + x = nm->mkNode(INTS_DIVISION_TOTAL, x, coeff); } - if( n[i].getConst().sgn()<0 ){ - x = NodeManager::currentNM()->mkNode( UMINUS, x ); + if (nc.getConst().sgn() < 0) + { + x = nm->mkNode(UMINUS, x); } }else{ - Node coeff = NodeManager::currentNM()->mkConst( Rational(1) / n[i].getConst() ); - x = NodeManager::currentNM()->mkNode( MULT, x, coeff ); + Node coeff = nm->mkConst(Rational(1) / nc.getConst()); + x = nm->mkNode(MULT, x, coeff); } } x = Rewriter::rewrite( x ); @@ -942,6 +996,11 @@ int Trigger::getActiveScore() { return d_mg->getActiveScore( d_quantEngine ); } +void Trigger::debugPrint(const char* c) const +{ + Trace(c) << "TRIGGER( " << d_nodes << " )" << std::endl; +} + }/* CVC4::theory::inst namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/quantifiers/ematching/trigger.h b/src/theory/quantifiers/ematching/trigger.h index 890811c8b..201d4258b 100644 --- a/src/theory/quantifiers/ematching/trigger.h +++ b/src/theory/quantifiers/ematching/trigger.h @@ -187,16 +187,16 @@ class Trigger { * produce instantiations beyond what is produced by the match generator * (for example, see theory/quantifiers/ematching/ho_trigger.h). */ - virtual int addInstantiations(); + virtual uint64_t addInstantiations(); /** Return whether this is a multi-trigger. */ - bool isMultiTrigger() { return d_nodes.size()>1; } + bool isMultiTrigger() const; /** Get instantiation pattern list associated with this trigger. * * An instantiation pattern list is the node representation of a trigger, in * particular, it is the third argument of quantified formulas which have user * (! ... :pattern) attributes. */ - Node getInstPattern(); + Node getInstPattern() const; /* A heuristic value indicating how active this generator is. * * This returns the number of ground terms for the match operators in terms @@ -205,19 +205,7 @@ class Trigger { */ int getActiveScore(); /** print debug information for the trigger */ - void debugPrint(const char* c) - { - Trace(c) << "TRIGGER( "; - for (int i = 0; i < (int)d_nodes.size(); i++) - { - if (i > 0) - { - Trace(c) << ", "; - } - Trace(c) << d_nodes[i]; - } - Trace(c) << " )"; - } + void debugPrint(const char* c) const; /** mkTrigger method * * This makes an instance of a trigger object. @@ -227,8 +215,8 @@ class Trigger { * keepAll: don't remove unneeded patterns; * trOption : policy for dealing with triggers that already exist * (see below) - * use_n_vars : number of variables that should be bound by the trigger - * typically, the number of quantified variables in q. + * useNVars : number of variables that should be bound by the trigger + * typically, the number of quantified variables in q. */ enum{ TR_MAKE_NEW, //make new trigger even if it already may exist @@ -240,14 +228,14 @@ class Trigger { std::vector& nodes, bool keepAll = true, int trOption = TR_MAKE_NEW, - unsigned use_n_vars = 0); + size_t useNVars = 0); /** single trigger version that calls the above function */ static Trigger* mkTrigger(QuantifiersEngine* qe, Node q, Node n, bool keepAll = true, int trOption = TR_MAKE_NEW, - unsigned use_n_vars = 0); + size_t useNVars = 0); /** make trigger terms * * This takes a set of eligible trigger terms and stores a subset of them in @@ -259,7 +247,7 @@ class Trigger { */ static bool mkTriggerTerms(Node q, std::vector& nodes, - unsigned n_vars, + size_t nvars, std::vector& trNodes); /** collect pattern terms * @@ -319,8 +307,6 @@ class Trigger { static bool isRelationalTriggerKind( Kind k ); /** is n a simple trigger (see inst_match_generator.h)? */ static bool isSimpleTrigger( Node n ); - /** is n a pure theory trigger, e.g. head( x )? */ - static bool isPureTheoryTrigger( Node n ); /** get trigger weight * * Intutively, this function classifies how difficult it is to handle the @@ -331,11 +317,6 @@ class Trigger { * Returns 2 otherwise. */ static int getTriggerWeight( Node n ); - /** Returns whether n is a trigger term with a local theory extension - * property from Bansal et al., CAV 2015. - */ - static bool isLocalTheoryExt( Node n, std::vector< Node >& vars, - std::vector< Node >& patTerms ); /** get the variable associated with an inversion for n * * A term n with an inversion variable x has the following property : @@ -422,8 +403,8 @@ class Trigger { */ static int isTriggerInstanceOf(Node n1, Node n2, - std::vector& fv1, - std::vector& fv2); + const std::vector& fv1, + const std::vector& fv2); /** add an instantiation (called by InstMatchGenerator) * -- 2.30.2