From 1dc23a88520ac3053f15bc16df2e302bbed49765 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 25 Jan 2021 10:29:39 -0600 Subject: [PATCH] Split inst match generator into multiple files (#5805) No code changes on this PR, only move + format. --- src/CMakeLists.txt | 8 + .../ematching/inst_match_generator.cpp | 615 +----------------- .../ematching/inst_match_generator.h | 244 ------- .../ematching/inst_match_generator_multi.cpp | 333 ++++++++++ .../ematching/inst_match_generator_multi.h | 113 ++++ .../inst_match_generator_multi_linear.cpp | 176 +++++ .../inst_match_generator_multi_linear.h | 91 +++ .../ematching/inst_match_generator_simple.cpp | 193 ++++++ .../ematching/inst_match_generator_simple.h | 110 ++++ src/theory/quantifiers/ematching/trigger.cpp | 3 + .../ematching/var_match_generator.cpp | 78 +++ .../ematching/var_match_generator.h | 60 ++ 12 files changed, 1171 insertions(+), 853 deletions(-) create mode 100644 src/theory/quantifiers/ematching/inst_match_generator_multi.cpp create mode 100644 src/theory/quantifiers/ematching/inst_match_generator_multi.h create mode 100644 src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp create mode 100644 src/theory/quantifiers/ematching/inst_match_generator_multi_linear.h create mode 100644 src/theory/quantifiers/ematching/inst_match_generator_simple.cpp create mode 100644 src/theory/quantifiers/ematching/inst_match_generator_simple.h create mode 100644 src/theory/quantifiers/ematching/var_match_generator.cpp create mode 100644 src/theory/quantifiers/ematching/var_match_generator.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 60e79fbe3..53420d395 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -658,6 +658,12 @@ libcvc4_add_sources( theory/quantifiers/ematching/ho_trigger.h theory/quantifiers/ematching/inst_match_generator.cpp theory/quantifiers/ematching/inst_match_generator.h + theory/quantifiers/ematching/inst_match_generator_multi.cpp + theory/quantifiers/ematching/inst_match_generator_multi.h + theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp + theory/quantifiers/ematching/inst_match_generator_multi_linear.h + theory/quantifiers/ematching/inst_match_generator_simple.cpp + theory/quantifiers/ematching/inst_match_generator_simple.h theory/quantifiers/ematching/inst_strategy.h theory/quantifiers/ematching/inst_strategy_e_matching.cpp theory/quantifiers/ematching/inst_strategy_e_matching.h @@ -669,6 +675,8 @@ libcvc4_add_sources( theory/quantifiers/ematching/trigger.h theory/quantifiers/ematching/trigger_trie.cpp theory/quantifiers/ematching/trigger_trie.h + theory/quantifiers/ematching/var_match_generator.cpp + theory/quantifiers/ematching/var_match_generator.h theory/quantifiers/equality_infer.cpp theory/quantifiers/equality_infer.h theory/quantifiers/equality_query.cpp diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp index c8e821dd7..91da843b3 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp @@ -9,16 +9,19 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** [[ Add lengthier description here ]] - ** \todo document this file + ** \brief Implementation of inst match generator class **/ + #include "theory/quantifiers/ematching/inst_match_generator.h" -#include "options/datatypes_options.h" #include "options/quantifiers_options.h" #include "theory/datatypes/theory_datatypes_utils.h" #include "theory/quantifiers/ematching/candidate_generator.h" +#include "theory/quantifiers/ematching/inst_match_generator_multi.h" +#include "theory/quantifiers/ematching/inst_match_generator_multi_linear.h" +#include "theory/quantifiers/ematching/inst_match_generator_simple.h" #include "theory/quantifiers/ematching/trigger.h" +#include "theory/quantifiers/ematching/var_match_generator.h" #include "theory/quantifiers/instantiate.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" @@ -656,612 +659,6 @@ InstMatchGenerator* InstMatchGenerator::getInstMatchGenerator(Node q, Node n) return new InstMatchGenerator(n); } -VarMatchGeneratorTermSubs::VarMatchGeneratorTermSubs( Node var, Node subs ) : - InstMatchGenerator(), d_var( var ), d_subs( subs ), d_rm_prev( false ){ - d_children_types.push_back(d_var.getAttribute(InstVarNumAttribute())); - d_var_type = d_var.getType(); -} - -int VarMatchGeneratorTermSubs::getNextMatch(Node q, - InstMatch& m, - QuantifiersEngine* qe, - Trigger* tparent) -{ - int ret_val = -1; - if( !d_eq_class.isNull() ){ - Trace("var-trigger-matching") << "Matching " << d_eq_class << " against " << d_var << " in " << d_subs << std::endl; - TNode tvar = d_var; - Node s = d_subs.substitute(tvar, d_eq_class); - s = Rewriter::rewrite( s ); - Trace("var-trigger-matching") << "...got " << s << ", " << s.getKind() << std::endl; - d_eq_class = Node::null(); - //if( s.getType().isSubtypeOf( d_var_type ) ){ - d_rm_prev = m.get(d_children_types[0]).isNull(); - if (!m.set(qe->getEqualityQuery(), d_children_types[0], s)) - { - return -1; - }else{ - ret_val = continueNextMatch(q, m, qe, tparent); - if( ret_val>0 ){ - return ret_val; - } - } - } - if( d_rm_prev ){ - m.d_vals[d_children_types[0]] = Node::null(); - d_rm_prev = false; - } - return -1; -} - -InstMatchGeneratorMultiLinear::InstMatchGeneratorMultiLinear( Node q, std::vector< Node >& pats, QuantifiersEngine* qe ) { - //order patterns to maximize eager matching failures - std::map< Node, std::vector< Node > > var_contains; - for (const Node& pat : pats) - { - quantifiers::TermUtil::computeInstConstContainsForQuant( - q, pat, var_contains[pat]); - } - std::map< Node, std::vector< Node > > var_to_node; - for (std::pair >& vc : var_contains) - { - for (const Node& n : vc.second) - { - var_to_node[n].push_back(vc.first); - } - } - std::vector< Node > pats_ordered; - std::vector< bool > pats_ordered_independent; - std::map< Node, bool > var_bound; - size_t patsSize = pats.size(); - while (pats_ordered.size() < patsSize) - { - // score is lexographic ( bound vars, shared vars ) - int score_max_1 = -1; - int score_max_2 = -1; - unsigned score_index = 0; - bool set_score_index = false; - for (size_t i = 0; i < patsSize; i++) - { - Node p = pats[i]; - if( std::find( pats_ordered.begin(), pats_ordered.end(), p )==pats_ordered.end() ){ - int score_1 = 0; - int score_2 = 0; - for( unsigned j=0; j1 ){ - score_2++; - } - } - if (!set_score_index || score_1 > score_max_1 - || (score_1 == score_max_1 && score_2 > score_max_2)) - { - score_index = i; - set_score_index = true; - score_max_1 = score_1; - score_max_2 = score_2; - } - } - } - Assert(set_score_index); - //update the variable bounds - Node mp = pats[score_index]; - std::vector& vcm = var_contains[mp]; - for (const Node& vc : vcm) - { - var_bound[vc] = true; - } - pats_ordered.push_back( mp ); - pats_ordered_independent.push_back( score_max_1==0 ); - } - - Trace("multi-trigger-linear") << "Make children for linear multi trigger." << std::endl; - for (size_t i = 0, poSize = pats_ordered.size(); i < poSize; i++) - { - Node po = pats_ordered[i]; - Trace("multi-trigger-linear") << "...make for " << po << std::endl; - InstMatchGenerator* cimg = getInstMatchGenerator(q, po); - Assert(cimg != nullptr); - d_children.push_back( cimg ); - // this could be improved - if (i == 0) - { - cimg->setIndependent(); - } - } -} - -int InstMatchGeneratorMultiLinear::resetChildren( QuantifiersEngine* qe ){ - for (InstMatchGenerator* c : d_children) - { - if (!c->reset(Node::null(), qe)) - { - return -2; - } - } - return 1; -} - -bool InstMatchGeneratorMultiLinear::reset( Node eqc, QuantifiersEngine* qe ) { - Assert(eqc.isNull()); - if( options::multiTriggerLinear() ){ - return true; - } - return resetChildren(qe) > 0; -} - -int InstMatchGeneratorMultiLinear::getNextMatch(Node q, - InstMatch& m, - QuantifiersEngine* qe, - Trigger* tparent) -{ - Trace("multi-trigger-linear-debug") << "InstMatchGeneratorMultiLinear::getNextMatch : reset " << std::endl; - if( options::multiTriggerLinear() ){ - //reset everyone - int rc_ret = resetChildren( qe ); - if( rc_ret<0 ){ - return rc_ret; - } - } - Trace("multi-trigger-linear-debug") << "InstMatchGeneratorMultiLinear::getNextMatch : continue match " << std::endl; - Assert(d_next != nullptr); - int ret_val = continueNextMatch(q, m, qe, tparent); - if( ret_val>0 ){ - Trace("multi-trigger-linear") << "Successful multi-trigger instantiation." << std::endl; - if( options::multiTriggerLinear() ){ - // now, restrict everyone - for (size_t i = 0, csize = d_children.size(); i < csize; i++) - { - Node mi = d_children[i]->getCurrentMatch(); - Trace("multi-trigger-linear") << " child " << i << " match : " << mi << std::endl; - d_children[i]->excludeMatch( mi ); - } - } - } - return ret_val; -} - - -/** constructors */ -InstMatchGeneratorMulti::InstMatchGeneratorMulti(Node q, - std::vector& pats, - QuantifiersEngine* qe) - : d_quant(q) -{ - Trace("multi-trigger-cache") << "Making smart multi-trigger for " << q << std::endl; - std::map< Node, std::vector< Node > > var_contains; - for (const Node& pat : pats) - { - quantifiers::TermUtil::computeInstConstContainsForQuant( - q, pat, var_contains[pat]); - } - //convert to indicies - for (std::pair >& vc : var_contains) - { - Trace("multi-trigger-cache") << "Pattern " << vc.first << " contains: "; - for (const Node& vcn : vc.second) - { - Trace("multi-trigger-cache") << vcn << " "; - uint64_t index = vcn.getAttribute(InstVarNumAttribute()); - d_var_contains[vc.first].push_back(index); - d_var_to_node[index].push_back(vc.first); - } - Trace("multi-trigger-cache") << std::endl; - } - size_t patsSize = pats.size(); - for (size_t i = 0; i < patsSize; i++) - { - Node n = pats[i]; - //make the match generator - InstMatchGenerator* img = - InstMatchGenerator::mkInstMatchGenerator(q, n, qe); - img->setActiveAdd(false); - d_children.push_back(img); - //compute unique/shared variables - std::vector unique_vars; - std::map shared_vars; - unsigned numSharedVars = 0; - std::vector& vctn = d_var_contains[n]; - for (size_t j = 0, vctnSize = vctn.size(); j < vctnSize; j++) - { - if (d_var_to_node[vctn[j]].size() == 1) - { - Trace("multi-trigger-cache") - << "Var " << vctn[j] << " is unique to " << pats[i] << std::endl; - unique_vars.push_back(vctn[j]); - }else{ - shared_vars[vctn[j]] = true; - numSharedVars++; - } - } - //we use the latest shared variables, then unique variables - std::vector vars; - size_t index = i == 0 ? pats.size() - 1 : (i - 1); - while( numSharedVars>0 && index!=i ){ - for (std::pair& sv : shared_vars) - { - if (sv.second) - { - std::vector& vctni = d_var_contains[pats[index]]; - if (std::find(vctni.begin(), vctni.end(), sv.first) != vctni.end()) - { - vars.push_back(sv.first); - shared_vars[sv.first] = false; - numSharedVars--; - } - } - } - index = index == 0 ? patsSize - 1 : (index - 1); - } - vars.insert( vars.end(), unique_vars.begin(), unique_vars.end() ); - if (Trace.isOn("multi-trigger-cache")) - { - Trace("multi-trigger-cache") << " Index[" << i << "]: "; - for (uint64_t v : vars) - { - Trace("multi-trigger-cache") << v << " "; - } - Trace("multi-trigger-cache") << std::endl; - } - //make ordered inst match trie - d_imtio[i] = new InstMatchTrie::ImtIndexOrder; - d_imtio[i]->d_order.insert( d_imtio[i]->d_order.begin(), vars.begin(), vars.end() ); - d_children_trie.push_back( InstMatchTrieOrdered( d_imtio[i] ) ); - } -} - -InstMatchGeneratorMulti::~InstMatchGeneratorMulti() -{ - for (size_t i = 0, csize = d_children.size(); i < csize; i++) - { - delete d_children[i]; - } - for (std::pair& i : d_imtio) - { - delete i.second; - } -} - -/** reset instantiation round (call this whenever equivalence classes have changed) */ -void InstMatchGeneratorMulti::resetInstantiationRound( QuantifiersEngine* qe ){ - for (InstMatchGenerator* c : d_children) - { - c->resetInstantiationRound(qe); - } -} - -/** reset, eqc is the equivalence class to search in (any if eqc=null) */ -bool InstMatchGeneratorMulti::reset( Node eqc, QuantifiersEngine* qe ){ - for (InstMatchGenerator* c : d_children) - { - if (!c->reset(eqc, qe)) - { - // do not return false here - } - } - return true; -} - -uint64_t InstMatchGeneratorMulti::addInstantiations(Node q, - QuantifiersEngine* qe, - Trigger* tparent) -{ - uint64_t addedLemmas = 0; - Trace("multi-trigger-cache") << "Process smart multi trigger" << std::endl; - for (size_t i = 0, csize = d_children.size(); i < csize; i++) - { - Trace("multi-trigger-cache") << "Calculate matches " << i << std::endl; - std::vector< InstMatch > newMatches; - InstMatch m( q ); - while (d_children[i]->getNextMatch(q, m, qe, tparent) > 0) - { - //m.makeRepresentative( qe ); - newMatches.push_back( InstMatch( &m ) ); - m.clear(); - } - Trace("multi-trigger-cache") << "Made " << newMatches.size() << " new matches for index " << i << std::endl; - for (size_t j = 0, nmatches = newMatches.size(); j < nmatches; j++) - { - Trace("multi-trigger-cache2") << "...processing " << j << " / " << newMatches.size() << ", #lemmas = " << addedLemmas << std::endl; - processNewMatch(qe, tparent, newMatches[j], i, addedLemmas); - if( qe->inConflict() ){ - return addedLemmas; - } - } - } - return addedLemmas; -} - -void InstMatchGeneratorMulti::processNewMatch(QuantifiersEngine* qe, - Trigger* tparent, - InstMatch& m, - size_t fromChildIndex, - uint64_t& addedLemmas) -{ - //see if these produce new matches - d_children_trie[fromChildIndex].addInstMatch(qe, d_quant, m); - //possibly only do the following if we know that new matches will be produced? - //the issue is that instantiations are filtered in quantifiers engine, and so there is no guarentee that - // we can safely skip the following lines, even when we have already produced this match. - Trace("multi-trigger-cache-debug") << "Child " << fromChildIndex << " produced match " << m << std::endl; - //process new instantiations - size_t childIndex = (fromChildIndex + 1) % d_children.size(); - processNewInstantiations(qe, - tparent, - m, - addedLemmas, - d_children_trie[childIndex].getTrie(), - 0, - childIndex, - fromChildIndex, - true); -} - -void InstMatchGeneratorMulti::processNewInstantiations(QuantifiersEngine* qe, - Trigger* tparent, - InstMatch& m, - uint64_t& addedLemmas, - InstMatchTrie* tr, - size_t trieIndex, - size_t childIndex, - size_t endChildIndex, - bool modEq) -{ - Assert(!qe->inConflict()); - if( childIndex==endChildIndex ){ - // m is an instantiation - if (sendInstantiation(tparent, m)) - { - addedLemmas++; - Trace("multi-trigger-cache-debug") << "-> Produced instantiation " << m - << std::endl; - } - return; - } - InstMatchTrie::ImtIndexOrder* iio = d_children_trie[childIndex].getOrdering(); - if (trieIndex < iio->d_order.size()) - { - size_t curr_index = iio->d_order[trieIndex]; - // Node curr_ic = qe->getTermUtil()->getInstantiationConstant( d_quant, - // curr_index ); - Node n = m.get( curr_index ); - if( n.isNull() ){ - // add to InstMatch - for (std::pair& d : tr->d_data) - { - InstMatch mn(&m); - mn.setValue(curr_index, d.first); - processNewInstantiations(qe, - tparent, - mn, - addedLemmas, - &(d.second), - trieIndex + 1, - childIndex, - endChildIndex, - modEq); - if (qe->inConflict()) - { - break; - } - } - } - // shared and set variable, try to merge - std::map::iterator it = tr->d_data.find(n); - if (it != tr->d_data.end()) - { - processNewInstantiations(qe, - tparent, - m, - addedLemmas, - &(it->second), - trieIndex + 1, - childIndex, - endChildIndex, - modEq); - } - if (!modEq) - { - return; - } - eq::EqualityEngine* ee = qe->getEqualityQuery()->getEngine(); - // check modulo equality for other possible instantiations - if (!ee->hasTerm(n)) - { - return; - } - eq::EqClassIterator eqc(ee->getRepresentative(n), ee); - while (!eqc.isFinished()) - { - Node en = (*eqc); - if (en != n) - { - std::map::iterator itc = tr->d_data.find(en); - if (itc != tr->d_data.end()) - { - processNewInstantiations(qe, - tparent, - m, - addedLemmas, - &(itc->second), - trieIndex + 1, - childIndex, - endChildIndex, - modEq); - if (qe->inConflict()) - { - break; - } - } - } - ++eqc; - } - }else{ - size_t newChildIndex = (childIndex + 1) % d_children.size(); - processNewInstantiations(qe, - tparent, - m, - addedLemmas, - d_children_trie[newChildIndex].getTrie(), - 0, - newChildIndex, - endChildIndex, - modEq); - } -} - -InstMatchGeneratorSimple::InstMatchGeneratorSimple(Node q, - Node pat, - QuantifiersEngine* qe) - : d_quant(q), d_match_pattern(pat) -{ - if( d_match_pattern.getKind()==NOT ){ - d_match_pattern = d_match_pattern[0]; - d_pol = false; - }else{ - d_pol = true; - } - if( d_match_pattern.getKind()==EQUAL ){ - d_eqc = d_match_pattern[1]; - d_match_pattern = d_match_pattern[0]; - Assert(!quantifiers::TermUtil::hasInstConstAttr(d_eqc)); - } - Assert(Trigger::isSimpleTrigger(d_match_pattern)); - for (size_t i = 0, nchild = d_match_pattern.getNumChildren(); i < nchild; i++) - { - if( d_match_pattern[i].getKind()==INST_CONSTANT ){ - if( !options::cegqi() || quantifiers::TermUtil::getInstConstAttr(d_match_pattern[i])==q ){ - d_var_num[i] = d_match_pattern[i].getAttribute(InstVarNumAttribute()); - }else{ - d_var_num[i] = -1; - } - } - d_match_pattern_arg_types.push_back( d_match_pattern[i].getType() ); - } - d_op = qe->getTermDatabase()->getMatchOperator( d_match_pattern ); -} - -void InstMatchGeneratorSimple::resetInstantiationRound( QuantifiersEngine* qe ) { - -} -uint64_t InstMatchGeneratorSimple::addInstantiations(Node q, - QuantifiersEngine* qe, - Trigger* tparent) -{ - uint64_t addedLemmas = 0; - TNodeTrie* tat; - if( d_eqc.isNull() ){ - tat = qe->getTermDatabase()->getTermArgTrie( d_op ); - }else{ - if( d_pol ){ - tat = qe->getTermDatabase()->getTermArgTrie( d_eqc, d_op ); - }else{ - //iterate over all classes except r - tat = qe->getTermDatabase()->getTermArgTrie( Node::null(), d_op ); - if (tat && !qe->inConflict()) - { - Node r = qe->getEqualityQuery()->getRepresentative(d_eqc); - for (std::pair& t : tat->d_data) - { - if (t.first != r) - { - InstMatch m( q ); - addInstantiations(m, qe, addedLemmas, 0, &(t.second)); - if( qe->inConflict() ){ - break; - } - } - } - } - tat = nullptr; - } - } - Debug("simple-trigger-debug") << "Adding instantiations based on " << tat << " from " << d_op << " " << d_eqc << std::endl; - if (tat && !qe->inConflict()) - { - InstMatch m( q ); - addInstantiations( m, qe, addedLemmas, 0, tat ); - } - return addedLemmas; -} - -void InstMatchGeneratorSimple::addInstantiations(InstMatch& m, - QuantifiersEngine* qe, - uint64_t& addedLemmas, - size_t argIndex, - TNodeTrie* tat) -{ - Debug("simple-trigger-debug") << "Add inst " << argIndex << " " << d_match_pattern << std::endl; - if (argIndex == d_match_pattern.getNumChildren()) - { - Assert(!tat->d_data.empty()); - TNode t = tat->getData(); - Debug("simple-trigger") << "Actual term is " << t << std::endl; - //convert to actual used terms - for (const std::pair& v : d_var_num) - { - if (v.second >= 0) - { - Assert(v.first < t.getNumChildren()); - Debug("simple-trigger") - << "...set " << v.second << " " << t[v.first] << std::endl; - m.setValue(v.second, t[v.first]); - } - } - // we do not need the trigger parent for simple triggers (no post-processing - // required) - if (qe->getInstantiate()->addInstantiation(d_quant, m)) - { - addedLemmas++; - Debug("simple-trigger") << "-> Produced instantiation " << m << std::endl; - } - return; - } - if (d_match_pattern[argIndex].getKind() == INST_CONSTANT) - { - int v = d_var_num[argIndex]; - if (v != -1) - { - for (std::pair& tt : tat->d_data) - { - Node t = tt.first; - Node prev = m.get(v); - // using representatives, just check if equal - Assert(t.getType().isComparableTo(d_match_pattern_arg_types[argIndex])); - if (prev.isNull() || prev == t) - { - m.setValue(v, t); - addInstantiations(m, qe, addedLemmas, argIndex + 1, &(tt.second)); - m.setValue(v, prev); - if (qe->inConflict()) - { - break; - } - } - } - return; - } - // inst constant from another quantified formula, treat as ground term TODO: - // remove this? - } - Node r = qe->getEqualityQuery()->getRepresentative(d_match_pattern[argIndex]); - std::map::iterator it = tat->d_data.find(r); - if (it != tat->d_data.end()) - { - addInstantiations(m, qe, addedLemmas, argIndex + 1, &(it->second)); - } -} - -int InstMatchGeneratorSimple::getActiveScore( QuantifiersEngine * qe ) { - Node f = qe->getTermDatabase()->getMatchOperator( d_match_pattern ); - size_t ngt = qe->getTermDatabase()->getNumGroundTerms(f); - Trace("trigger-active-sel-debug") << "Number of ground terms for (simple) " << f << " is " << ngt << std::endl; - return static_cast(ngt); -} - - }/* CVC4::theory::inst namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/quantifiers/ematching/inst_match_generator.h b/src/theory/quantifiers/ematching/inst_match_generator.h index 99816c040..f03d1cf20 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator.h +++ b/src/theory/quantifiers/ematching/inst_match_generator.h @@ -416,250 +416,6 @@ class InstMatchGenerator : public IMGenerator { static InstMatchGenerator* getInstMatchGenerator(Node q, Node n); };/* class InstMatchGenerator */ -/** match generator for purified terms -* This handles the special case of invertible terms like x+1 (see -* Trigger::getTermInversionVariable). -*/ -class VarMatchGeneratorTermSubs : public InstMatchGenerator { -public: - VarMatchGeneratorTermSubs( Node var, Node subs ); - - /** Reset */ - bool reset(Node eqc, QuantifiersEngine* qe) override - { - d_eq_class = eqc; - return true; - } - /** Get the next match. */ - int getNextMatch(Node q, - InstMatch& m, - QuantifiersEngine* qe, - Trigger* tparent) override; - - private: - /** variable we are matching (x in the example x+1). */ - Node d_var; - /** cache of d_var.getType() */ - TypeNode d_var_type; - /** The substitution for what we match (x-1 in the example x+1). */ - Node d_subs; - /** stores whether we have written a value for d_var in the current match. */ - bool d_rm_prev; -}; - -/** InstMatchGeneratorMultiLinear class -* -* This is the default implementation of multi-triggers. -* -* Handling multi-triggers using this class is done by constructing a linked -* list of InstMatchGenerator classes (see mkInstMatchGeneratorMulti), with one -* InstMatchGeneratorMultiLinear at the head and a list of trailing -* InstMatchGenerators. -* -* CVC4 employs techniques that ensure that the number of instantiations -* is worst-case polynomial wrt the number of ground terms, where this class -* lifts this policy to multi-triggers. In particular consider -* -* multi-trigger : { f( x1 ), f( x2 ), f( x3 ), f( x4 ) } -* -* For this multi-trigger, we insist that for each i=1...4, and each ground term -* t, there is at most 1 instantiation added as a result of matching -* ( f( x1 ), f( x2 ), f( x3 ), f( x4 ) ) -* against ground terms of the form -* ( s_1, s_2, s_3, s_4 ) where t = s_i for i=1,...,4. -* Meaning we add instantiations for the multi-trigger -* ( f( x1 ), f( x2 ), f( x3 ), f( x4 ) ) based on matching pairwise against: -* ( f( c_i11 ), f( c_i21 ), f( c_i31 ), f( c_i41 ) ) -* ( f( c_i12 ), f( c_i22 ), f( c_i32 ), f( c_i42 ) ) -* ( f( c_i13 ), f( c_i23 ), f( c_i33 ), f( c_i43 ) ) -* Where we require c_i{jk} != c_i{jl} for each i=1...4, k != l. -* -* For example, we disallow adding instantiations based on matching against both -* ( f( c_1 ), f( c_2 ), f( c_4 ), f( c_6 ) ) and -* ( f( c_1 ), f( c_3 ), f( c_5 ), f( c_7 ) ) -* against ( f( x1 ), f( x2 ), f( x3 ), f( x4 ) ), since f( c_1 ) is matched -* against f( x1 ) twice. -* -* This policy can be disabled by --no-multi-trigger-linear. -* -*/ -class InstMatchGeneratorMultiLinear : public InstMatchGenerator { - friend class InstMatchGenerator; - - public: - /** Reset. */ - bool reset(Node eqc, QuantifiersEngine* qe) override; - /** Get the next match. */ - int getNextMatch(Node q, - InstMatch& m, - QuantifiersEngine* qe, - Trigger* tparent) override; - - protected: - /** reset the children of this generator */ - int resetChildren(QuantifiersEngine* qe); - /** constructor */ - InstMatchGeneratorMultiLinear(Node q, - std::vector& pats, - QuantifiersEngine* qe); -};/* class InstMatchGeneratorMulti */ - -/** InstMatchGeneratorMulti -* -* This is an earlier implementation of multi-triggers -* that is enabled by --multi-trigger-cache. -* This generator takes the product of instantiations -* found by single trigger matching, and does -* not have the guarantee that the number of -* instantiations is polynomial wrt the number of -* ground terms. -*/ -class InstMatchGeneratorMulti : public IMGenerator { - public: - /** constructors */ - InstMatchGeneratorMulti(Node q, - std::vector& pats, - QuantifiersEngine* qe); - /** destructor */ - ~InstMatchGeneratorMulti() override; - - /** Reset instantiation round. */ - void resetInstantiationRound(QuantifiersEngine* qe) override; - /** Reset. */ - bool reset(Node eqc, QuantifiersEngine* qe) override; - /** Add instantiations. */ - uint64_t addInstantiations(Node q, - QuantifiersEngine* qe, - Trigger* tparent) override; - - private: - /** process new match - * - * Called during addInstantiations(...). - * Indicates we produced a match m for child fromChildIndex - * addedLemmas is how many instantiations we succesfully send - * via IMGenerator::sendInstantiation(...) calls. - */ - void processNewMatch(QuantifiersEngine* qe, - Trigger* tparent, - InstMatch& m, - size_t fromChildIndex, - uint64_t& addedLemmas); - /** helper for process new match - * tr is the inst match trie (term index) we are currently traversing. - * trieIndex is depth we are in trie tr. - * childIndex is the index of the term in the multi trigger we are currently - * processing. - * endChildIndex is the index of the term in the multi trigger that generated - * a new term, and hence we will end when the product - * computed by this function returns to. - * modEq is whether we are matching modulo equality. - */ - void processNewInstantiations(QuantifiersEngine* qe, - Trigger* tparent, - InstMatch& m, - uint64_t& addedLemmas, - InstMatchTrie* tr, - size_t trieIndex, - size_t childIndex, - size_t endChildIndex, - bool modEq); - /** Map from pattern nodes to indices of variables they contain. */ - std::map > d_var_contains; - /** Map from variable indices to pattern nodes that contain them. */ - std::map > d_var_to_node; - /** quantified formula we are producing matches for */ - Node d_quant; - /** children generators - * These are inst match generators for each term in the multi trigger. - */ - std::vector< InstMatchGenerator* > d_children; - /** variable orderings - * Stores a heuristically determined variable ordering (unique - * variables first) for each term in the multi trigger. - */ - std::map d_imtio; - /** inst match tries for each child node - * This data structure stores all InstMatch objects generated - * by matching for each term in the multi trigger. - */ - std::vector< InstMatchTrieOrdered > d_children_trie; -};/* class InstMatchGeneratorMulti */ - -/** InstMatchGeneratorSimple class -* -* This is the default generator class for simple single triggers. -* For example, { f( x, a ) }, { f( x, x ) } and { f( x, y ) } are simple single -* triggers. In practice, around 70-90% of triggers are simple single triggers. -* -* Notice that simple triggers also can have an attached polarity. -* For example, { P( x ) = false }, { f( x, y ) = a } and { ~f( a, x ) = b } are -* simple single triggers. -* -* The implementation traverses the term indices in TermDatabase for adding -* instantiations, which is more efficient than the techniques required for -* handling non-simple single triggers. -* -* In contrast to other instantiation generators, it does not call -* IMGenerator::sendInstantiation and for performance reasons instead calls -* qe->getInstantiate()->addInstantiation(...) directly. -*/ -class InstMatchGeneratorSimple : public IMGenerator { - public: - /** constructors */ - InstMatchGeneratorSimple(Node q, Node pat, QuantifiersEngine* qe); - - /** Reset instantiation round. */ - void resetInstantiationRound(QuantifiersEngine* qe) override; - /** Add instantiations. */ - uint64_t addInstantiations(Node q, - QuantifiersEngine* qe, - Trigger* tparent) override; - /** Get active score. */ - int getActiveScore(QuantifiersEngine* qe) override; - - private: - /** quantified formula for the trigger term */ - Node d_quant; - /** the trigger term */ - Node d_match_pattern; - /** equivalence class polarity information - * - * This stores the required polarity/equivalence class with this trigger. - * If d_eqc is non-null, we only produce matches { x->t } such that - * our context does not entail - * ( d_match_pattern*{ x->t } = d_eqc) if d_pol = true, or - * ( d_match_pattern*{ x->t } != d_eqc) if d_pol = false. - * where * denotes application of substitution. - */ - bool d_pol; - Node d_eqc; - /** Match pattern arg types. - * Cached values of d_match_pattern[i].getType(). - */ - std::vector< TypeNode > d_match_pattern_arg_types; - /** The match operator d_match_pattern (see TermDb::getMatchOperator). */ - Node d_op; - /** - * Map from child number of d_match_pattern to variable index, or -1 if the - * child is not a variable. - */ - std::map d_var_num; - /** add instantiations, helper function. - * - * m is the current match we are building, - * addedLemmas is the number of lemmas we have added via calls to - * qe->getInstantiate()->aaddInstantiation(...), - * argIndex is the argument index in d_match_pattern we are currently - * matching, - * tat is the term index we are currently traversing. - */ - void addInstantiations(InstMatch& m, - QuantifiersEngine* qe, - uint64_t& addedLemmas, - size_t argIndex, - TNodeTrie* tat); -};/* class InstMatchGeneratorSimple */ } } } diff --git a/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp b/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp new file mode 100644 index 000000000..b4a7457a3 --- /dev/null +++ b/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp @@ -0,0 +1,333 @@ +/********************* */ +/*! \file inst_match_generator_multi.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief multi inst match generator class + **/ + +#include "theory/quantifiers/ematching/inst_match_generator_multi.h" + +#include "theory/quantifiers_engine.h" + +using namespace CVC4::kind; + +namespace CVC4 { +namespace theory { +namespace inst { + +InstMatchGeneratorMulti::InstMatchGeneratorMulti(Node q, + std::vector& pats, + QuantifiersEngine* qe) + : d_quant(q) +{ + Trace("multi-trigger-cache") + << "Making smart multi-trigger for " << q << std::endl; + std::map > var_contains; + for (const Node& pat : pats) + { + quantifiers::TermUtil::computeInstConstContainsForQuant( + q, pat, var_contains[pat]); + } + // convert to indicies + for (std::pair >& vc : var_contains) + { + Trace("multi-trigger-cache") << "Pattern " << vc.first << " contains: "; + for (const Node& vcn : vc.second) + { + Trace("multi-trigger-cache") << vcn << " "; + uint64_t index = vcn.getAttribute(InstVarNumAttribute()); + d_var_contains[vc.first].push_back(index); + d_var_to_node[index].push_back(vc.first); + } + Trace("multi-trigger-cache") << std::endl; + } + size_t patsSize = pats.size(); + for (size_t i = 0; i < patsSize; i++) + { + Node n = pats[i]; + // make the match generator + InstMatchGenerator* img = + InstMatchGenerator::mkInstMatchGenerator(q, n, qe); + img->setActiveAdd(false); + d_children.push_back(img); + // compute unique/shared variables + std::vector unique_vars; + std::map shared_vars; + unsigned numSharedVars = 0; + std::vector& vctn = d_var_contains[n]; + for (size_t j = 0, vctnSize = vctn.size(); j < vctnSize; j++) + { + if (d_var_to_node[vctn[j]].size() == 1) + { + Trace("multi-trigger-cache") + << "Var " << vctn[j] << " is unique to " << pats[i] << std::endl; + unique_vars.push_back(vctn[j]); + } + else + { + shared_vars[vctn[j]] = true; + numSharedVars++; + } + } + // we use the latest shared variables, then unique variables + std::vector vars; + size_t index = i == 0 ? pats.size() - 1 : (i - 1); + while (numSharedVars > 0 && index != i) + { + for (std::pair& sv : shared_vars) + { + if (sv.second) + { + std::vector& vctni = d_var_contains[pats[index]]; + if (std::find(vctni.begin(), vctni.end(), sv.first) != vctni.end()) + { + vars.push_back(sv.first); + shared_vars[sv.first] = false; + numSharedVars--; + } + } + } + index = index == 0 ? patsSize - 1 : (index - 1); + } + vars.insert(vars.end(), unique_vars.begin(), unique_vars.end()); + if (Trace.isOn("multi-trigger-cache")) + { + Trace("multi-trigger-cache") << " Index[" << i << "]: "; + for (uint64_t v : vars) + { + Trace("multi-trigger-cache") << v << " "; + } + Trace("multi-trigger-cache") << std::endl; + } + // make ordered inst match trie + d_imtio[i] = new InstMatchTrie::ImtIndexOrder; + d_imtio[i]->d_order.insert( + d_imtio[i]->d_order.begin(), vars.begin(), vars.end()); + d_children_trie.push_back(InstMatchTrieOrdered(d_imtio[i])); + } +} + +InstMatchGeneratorMulti::~InstMatchGeneratorMulti() +{ + for (size_t i = 0, csize = d_children.size(); i < csize; i++) + { + delete d_children[i]; + } + for (std::pair& i : d_imtio) + { + delete i.second; + } +} + +/** reset instantiation round (call this whenever equivalence classes have + * changed) */ +void InstMatchGeneratorMulti::resetInstantiationRound(QuantifiersEngine* qe) +{ + for (InstMatchGenerator* c : d_children) + { + c->resetInstantiationRound(qe); + } +} + +/** reset, eqc is the equivalence class to search in (any if eqc=null) */ +bool InstMatchGeneratorMulti::reset(Node eqc, QuantifiersEngine* qe) +{ + for (InstMatchGenerator* c : d_children) + { + if (!c->reset(eqc, qe)) + { + // do not return false here + } + } + return true; +} + +uint64_t InstMatchGeneratorMulti::addInstantiations(Node q, + QuantifiersEngine* qe, + Trigger* tparent) +{ + uint64_t addedLemmas = 0; + Trace("multi-trigger-cache") << "Process smart multi trigger" << std::endl; + for (size_t i = 0, csize = d_children.size(); i < csize; i++) + { + Trace("multi-trigger-cache") << "Calculate matches " << i << std::endl; + std::vector newMatches; + InstMatch m(q); + while (d_children[i]->getNextMatch(q, m, qe, tparent) > 0) + { + // m.makeRepresentative( qe ); + newMatches.push_back(InstMatch(&m)); + m.clear(); + } + Trace("multi-trigger-cache") << "Made " << newMatches.size() + << " new matches for index " << i << std::endl; + for (size_t j = 0, nmatches = newMatches.size(); j < nmatches; j++) + { + Trace("multi-trigger-cache2") + << "...processing " << j << " / " << newMatches.size() + << ", #lemmas = " << addedLemmas << std::endl; + processNewMatch(qe, tparent, newMatches[j], i, addedLemmas); + if (qe->inConflict()) + { + return addedLemmas; + } + } + } + return addedLemmas; +} + +void InstMatchGeneratorMulti::processNewMatch(QuantifiersEngine* qe, + Trigger* tparent, + InstMatch& m, + size_t fromChildIndex, + uint64_t& addedLemmas) +{ + // see if these produce new matches + d_children_trie[fromChildIndex].addInstMatch(qe, d_quant, m); + // possibly only do the following if we know that new matches will be + // produced? the issue is that instantiations are filtered in quantifiers + // engine, and so there is no guarentee that + // we can safely skip the following lines, even when we have already produced + // this match. + Trace("multi-trigger-cache-debug") + << "Child " << fromChildIndex << " produced match " << m << std::endl; + // process new instantiations + size_t childIndex = (fromChildIndex + 1) % d_children.size(); + processNewInstantiations(qe, + tparent, + m, + addedLemmas, + d_children_trie[childIndex].getTrie(), + 0, + childIndex, + fromChildIndex, + true); +} + +void InstMatchGeneratorMulti::processNewInstantiations(QuantifiersEngine* qe, + Trigger* tparent, + InstMatch& m, + uint64_t& addedLemmas, + InstMatchTrie* tr, + size_t trieIndex, + size_t childIndex, + size_t endChildIndex, + bool modEq) +{ + Assert(!qe->inConflict()); + if (childIndex == endChildIndex) + { + // m is an instantiation + if (sendInstantiation(tparent, m)) + { + addedLemmas++; + Trace("multi-trigger-cache-debug") + << "-> Produced instantiation " << m << std::endl; + } + return; + } + InstMatchTrie::ImtIndexOrder* iio = d_children_trie[childIndex].getOrdering(); + if (trieIndex < iio->d_order.size()) + { + size_t curr_index = iio->d_order[trieIndex]; + // Node curr_ic = qe->getTermUtil()->getInstantiationConstant( d_quant, + // curr_index ); + Node n = m.get(curr_index); + if (n.isNull()) + { + // add to InstMatch + for (std::pair& d : tr->d_data) + { + InstMatch mn(&m); + mn.setValue(curr_index, d.first); + processNewInstantiations(qe, + tparent, + mn, + addedLemmas, + &(d.second), + trieIndex + 1, + childIndex, + endChildIndex, + modEq); + if (qe->inConflict()) + { + break; + } + } + } + // shared and set variable, try to merge + std::map::iterator it = tr->d_data.find(n); + if (it != tr->d_data.end()) + { + processNewInstantiations(qe, + tparent, + m, + addedLemmas, + &(it->second), + trieIndex + 1, + childIndex, + endChildIndex, + modEq); + } + if (!modEq) + { + return; + } + eq::EqualityEngine* ee = qe->getEqualityQuery()->getEngine(); + // check modulo equality for other possible instantiations + if (!ee->hasTerm(n)) + { + return; + } + eq::EqClassIterator eqc(ee->getRepresentative(n), ee); + while (!eqc.isFinished()) + { + Node en = (*eqc); + if (en != n) + { + std::map::iterator itc = tr->d_data.find(en); + if (itc != tr->d_data.end()) + { + processNewInstantiations(qe, + tparent, + m, + addedLemmas, + &(itc->second), + trieIndex + 1, + childIndex, + endChildIndex, + modEq); + if (qe->inConflict()) + { + break; + } + } + } + ++eqc; + } + } + else + { + size_t newChildIndex = (childIndex + 1) % d_children.size(); + processNewInstantiations(qe, + tparent, + m, + addedLemmas, + d_children_trie[newChildIndex].getTrie(), + 0, + newChildIndex, + endChildIndex, + modEq); + } +} + +} // namespace inst +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/quantifiers/ematching/inst_match_generator_multi.h b/src/theory/quantifiers/ematching/inst_match_generator_multi.h new file mode 100644 index 000000000..b68d362cc --- /dev/null +++ b/src/theory/quantifiers/ematching/inst_match_generator_multi.h @@ -0,0 +1,113 @@ +/********************* */ +/*! \file inst_match_generator_multi.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds, Morgan Deters, Tim King + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief multi inst match generator class + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_MULTI_H +#define CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_MULTI_H + +#include +#include +#include "expr/node_trie.h" +#include "theory/quantifiers/ematching/inst_match_generator.h" + +namespace CVC4 { +namespace theory { +namespace inst { + +/** InstMatchGeneratorMulti + * + * This is an earlier implementation of multi-triggers that is enabled by + * --multi-trigger-cache. This generator takes the product of instantiations + * found by single trigger matching, and does not have the guarantee that the + * number of instantiations is polynomial wrt the number of ground terms. + */ +class InstMatchGeneratorMulti : public IMGenerator +{ + public: + /** constructors */ + InstMatchGeneratorMulti(Node q, + std::vector& pats, + QuantifiersEngine* qe); + /** destructor */ + ~InstMatchGeneratorMulti() override; + + /** Reset instantiation round. */ + void resetInstantiationRound(QuantifiersEngine* qe) override; + /** Reset. */ + bool reset(Node eqc, QuantifiersEngine* qe) override; + /** Add instantiations. */ + uint64_t addInstantiations(Node q, + QuantifiersEngine* qe, + Trigger* tparent) override; + + private: + /** process new match + * + * Called during addInstantiations(...). + * Indicates we produced a match m for child fromChildIndex + * addedLemmas is how many instantiations we succesfully send + * via IMGenerator::sendInstantiation(...) calls. + */ + void processNewMatch(QuantifiersEngine* qe, + Trigger* tparent, + InstMatch& m, + size_t fromChildIndex, + uint64_t& addedLemmas); + /** helper for process new match + * tr is the inst match trie (term index) we are currently traversing. + * trieIndex is depth we are in trie tr. + * childIndex is the index of the term in the multi trigger we are currently + * processing. + * endChildIndex is the index of the term in the multi trigger that generated + * a new term, and hence we will end when the product + * computed by this function returns to. + * modEq is whether we are matching modulo equality. + */ + void processNewInstantiations(QuantifiersEngine* qe, + Trigger* tparent, + InstMatch& m, + uint64_t& addedLemmas, + InstMatchTrie* tr, + size_t trieIndex, + size_t childIndex, + size_t endChildIndex, + bool modEq); + /** Map from pattern nodes to indices of variables they contain. */ + std::map > d_var_contains; + /** Map from variable indices to pattern nodes that contain them. */ + std::map > d_var_to_node; + /** quantified formula we are producing matches for */ + Node d_quant; + /** children generators + * These are inst match generators for each term in the multi trigger. + */ + std::vector d_children; + /** variable orderings + * Stores a heuristically determined variable ordering (unique + * variables first) for each term in the multi trigger. + */ + std::map d_imtio; + /** inst match tries for each child node + * This data structure stores all InstMatch objects generated + * by matching for each term in the multi trigger. + */ + std::vector d_children_trie; +}; + +} // namespace inst +} // namespace theory +} // namespace CVC4 + +#endif diff --git a/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp b/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp new file mode 100644 index 000000000..1eb9ccdad --- /dev/null +++ b/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp @@ -0,0 +1,176 @@ +/********************* */ +/*! \file inst_match_generator_multi_linear.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Implementation of multi-linear inst match generator class + **/ +#include "theory/quantifiers/ematching/inst_match_generator_multi_linear.h" + +#include "theory/quantifiers_engine.h" + +using namespace CVC4::kind; + +namespace CVC4 { +namespace theory { +namespace inst { + +InstMatchGeneratorMultiLinear::InstMatchGeneratorMultiLinear( + Node q, std::vector& pats, QuantifiersEngine* qe) +{ + // order patterns to maximize eager matching failures + std::map > var_contains; + for (const Node& pat : pats) + { + quantifiers::TermUtil::computeInstConstContainsForQuant( + q, pat, var_contains[pat]); + } + std::map > var_to_node; + for (std::pair >& vc : var_contains) + { + for (const Node& n : vc.second) + { + var_to_node[n].push_back(vc.first); + } + } + std::vector pats_ordered; + std::vector pats_ordered_independent; + std::map var_bound; + size_t patsSize = pats.size(); + while (pats_ordered.size() < patsSize) + { + // score is lexographic ( bound vars, shared vars ) + int score_max_1 = -1; + int score_max_2 = -1; + unsigned score_index = 0; + bool set_score_index = false; + for (size_t i = 0; i < patsSize; i++) + { + Node p = pats[i]; + if (std::find(pats_ordered.begin(), pats_ordered.end(), p) + == pats_ordered.end()) + { + int score_1 = 0; + int score_2 = 0; + for (unsigned j = 0; j < var_contains[p].size(); j++) + { + Node v = var_contains[p][j]; + if (var_bound.find(v) != var_bound.end()) + { + score_1++; + } + else if (var_to_node[v].size() > 1) + { + score_2++; + } + } + if (!set_score_index || score_1 > score_max_1 + || (score_1 == score_max_1 && score_2 > score_max_2)) + { + score_index = i; + set_score_index = true; + score_max_1 = score_1; + score_max_2 = score_2; + } + } + } + Assert(set_score_index); + // update the variable bounds + Node mp = pats[score_index]; + std::vector& vcm = var_contains[mp]; + for (const Node& vc : vcm) + { + var_bound[vc] = true; + } + pats_ordered.push_back(mp); + pats_ordered_independent.push_back(score_max_1 == 0); + } + + Trace("multi-trigger-linear") + << "Make children for linear multi trigger." << std::endl; + for (size_t i = 0, poSize = pats_ordered.size(); i < poSize; i++) + { + Node po = pats_ordered[i]; + Trace("multi-trigger-linear") << "...make for " << po << std::endl; + InstMatchGenerator* cimg = getInstMatchGenerator(q, po); + Assert(cimg != nullptr); + d_children.push_back(cimg); + // this could be improved + if (i == 0) + { + cimg->setIndependent(); + } + } +} + +int InstMatchGeneratorMultiLinear::resetChildren(QuantifiersEngine* qe) +{ + for (InstMatchGenerator* c : d_children) + { + if (!c->reset(Node::null(), qe)) + { + return -2; + } + } + return 1; +} + +bool InstMatchGeneratorMultiLinear::reset(Node eqc, QuantifiersEngine* qe) +{ + Assert(eqc.isNull()); + if (options::multiTriggerLinear()) + { + return true; + } + return resetChildren(qe) > 0; +} + +int InstMatchGeneratorMultiLinear::getNextMatch(Node q, + InstMatch& m, + QuantifiersEngine* qe, + Trigger* tparent) +{ + Trace("multi-trigger-linear-debug") + << "InstMatchGeneratorMultiLinear::getNextMatch : reset " << std::endl; + if (options::multiTriggerLinear()) + { + // reset everyone + int rc_ret = resetChildren(qe); + if (rc_ret < 0) + { + return rc_ret; + } + } + Trace("multi-trigger-linear-debug") + << "InstMatchGeneratorMultiLinear::getNextMatch : continue match " + << std::endl; + Assert(d_next != nullptr); + int ret_val = continueNextMatch(q, m, qe, tparent); + if (ret_val > 0) + { + Trace("multi-trigger-linear") + << "Successful multi-trigger instantiation." << std::endl; + if (options::multiTriggerLinear()) + { + // now, restrict everyone + for (size_t i = 0, csize = d_children.size(); i < csize; i++) + { + Node mi = d_children[i]->getCurrentMatch(); + Trace("multi-trigger-linear") + << " child " << i << " match : " << mi << std::endl; + d_children[i]->excludeMatch(mi); + } + } + } + return ret_val; +} + +} // namespace inst +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.h b/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.h new file mode 100644 index 000000000..245b3d794 --- /dev/null +++ b/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.h @@ -0,0 +1,91 @@ +/********************* */ +/*! \file inst_match_generator_multi_linear.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief multi-linear inst match generator class + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_MULTI_LINEAR_H +#define CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_MULTI_LINEAR_H + +#include + +#include "expr/node.h" +#include "theory/quantifiers/ematching/inst_match_generator.h" + +namespace CVC4 { +namespace theory { +namespace inst { + +/** InstMatchGeneratorMultiLinear class + * + * This is the default implementation of multi-triggers. + * + * Handling multi-triggers using this class is done by constructing a linked + * list of InstMatchGenerator classes (see mkInstMatchGeneratorMulti), with one + * InstMatchGeneratorMultiLinear at the head and a list of trailing + * InstMatchGenerators. + * + * CVC4 employs techniques that ensure that the number of instantiations + * is worst-case polynomial wrt the number of ground terms, where this class + * lifts this policy to multi-triggers. In particular consider + * + * multi-trigger : { f( x1 ), f( x2 ), f( x3 ), f( x4 ) } + * + * For this multi-trigger, we insist that for each i=1...4, and each ground term + * t, there is at most 1 instantiation added as a result of matching + * ( f( x1 ), f( x2 ), f( x3 ), f( x4 ) ) + * against ground terms of the form + * ( s_1, s_2, s_3, s_4 ) where t = s_i for i=1,...,4. + * Meaning we add instantiations for the multi-trigger + * ( f( x1 ), f( x2 ), f( x3 ), f( x4 ) ) based on matching pairwise against: + * ( f( c_i11 ), f( c_i21 ), f( c_i31 ), f( c_i41 ) ) + * ( f( c_i12 ), f( c_i22 ), f( c_i32 ), f( c_i42 ) ) + * ( f( c_i13 ), f( c_i23 ), f( c_i33 ), f( c_i43 ) ) + * Where we require c_i{jk} != c_i{jl} for each i=1...4, k != l. + * + * For example, we disallow adding instantiations based on matching against both + * ( f( c_1 ), f( c_2 ), f( c_4 ), f( c_6 ) ) and + * ( f( c_1 ), f( c_3 ), f( c_5 ), f( c_7 ) ) + * against ( f( x1 ), f( x2 ), f( x3 ), f( x4 ) ), since f( c_1 ) is matched + * against f( x1 ) twice. + * + * This policy can be disabled by --no-multi-trigger-linear. + * + */ +class InstMatchGeneratorMultiLinear : public InstMatchGenerator +{ + friend class InstMatchGenerator; + + public: + /** Reset. */ + bool reset(Node eqc, QuantifiersEngine* qe) override; + /** Get the next match. */ + int getNextMatch(Node q, + InstMatch& m, + QuantifiersEngine* qe, + Trigger* tparent) override; + + protected: + /** reset the children of this generator */ + int resetChildren(QuantifiersEngine* qe); + /** constructor */ + InstMatchGeneratorMultiLinear(Node q, + std::vector& pats, + QuantifiersEngine* qe); +}; + +} // namespace inst +} // namespace theory +} // namespace CVC4 + +#endif diff --git a/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp b/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp new file mode 100644 index 000000000..995888ba2 --- /dev/null +++ b/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp @@ -0,0 +1,193 @@ +/********************* */ +/*! \file inst_match_generator_simple.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds, Morgan Deters, Mathias Preiner + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief simple inst match generator class + **/ +#include "theory/quantifiers/ematching/inst_match_generator_simple.h" + +#include "theory/quantifiers_engine.h" + +using namespace CVC4::kind; + +namespace CVC4 { +namespace theory { +namespace inst { + +InstMatchGeneratorSimple::InstMatchGeneratorSimple(Node q, + Node pat, + QuantifiersEngine* qe) + : d_quant(q), d_match_pattern(pat) +{ + if (d_match_pattern.getKind() == NOT) + { + d_match_pattern = d_match_pattern[0]; + d_pol = false; + } + else + { + d_pol = true; + } + if (d_match_pattern.getKind() == EQUAL) + { + d_eqc = d_match_pattern[1]; + d_match_pattern = d_match_pattern[0]; + Assert(!quantifiers::TermUtil::hasInstConstAttr(d_eqc)); + } + Assert(Trigger::isSimpleTrigger(d_match_pattern)); + for (size_t i = 0, nchild = d_match_pattern.getNumChildren(); i < nchild; i++) + { + if (d_match_pattern[i].getKind() == INST_CONSTANT) + { + if (!options::cegqi() + || quantifiers::TermUtil::getInstConstAttr(d_match_pattern[i]) == q) + { + d_var_num[i] = d_match_pattern[i].getAttribute(InstVarNumAttribute()); + } + else + { + d_var_num[i] = -1; + } + } + d_match_pattern_arg_types.push_back(d_match_pattern[i].getType()); + } + d_op = qe->getTermDatabase()->getMatchOperator(d_match_pattern); +} + +void InstMatchGeneratorSimple::resetInstantiationRound(QuantifiersEngine* qe) {} +uint64_t InstMatchGeneratorSimple::addInstantiations(Node q, + QuantifiersEngine* qe, + Trigger* tparent) +{ + uint64_t addedLemmas = 0; + TNodeTrie* tat; + if (d_eqc.isNull()) + { + tat = qe->getTermDatabase()->getTermArgTrie(d_op); + } + else + { + if (d_pol) + { + tat = qe->getTermDatabase()->getTermArgTrie(d_eqc, d_op); + } + else + { + // iterate over all classes except r + tat = qe->getTermDatabase()->getTermArgTrie(Node::null(), d_op); + if (tat && !qe->inConflict()) + { + Node r = qe->getEqualityQuery()->getRepresentative(d_eqc); + for (std::pair& t : tat->d_data) + { + if (t.first != r) + { + InstMatch m(q); + addInstantiations(m, qe, addedLemmas, 0, &(t.second)); + if (qe->inConflict()) + { + break; + } + } + } + } + tat = nullptr; + } + } + Debug("simple-trigger-debug") + << "Adding instantiations based on " << tat << " from " << d_op << " " + << d_eqc << std::endl; + if (tat && !qe->inConflict()) + { + InstMatch m(q); + addInstantiations(m, qe, addedLemmas, 0, tat); + } + return addedLemmas; +} + +void InstMatchGeneratorSimple::addInstantiations(InstMatch& m, + QuantifiersEngine* qe, + uint64_t& addedLemmas, + size_t argIndex, + TNodeTrie* tat) +{ + Debug("simple-trigger-debug") + << "Add inst " << argIndex << " " << d_match_pattern << std::endl; + if (argIndex == d_match_pattern.getNumChildren()) + { + Assert(!tat->d_data.empty()); + TNode t = tat->getData(); + Debug("simple-trigger") << "Actual term is " << t << std::endl; + // convert to actual used terms + for (const std::pair& v : d_var_num) + { + if (v.second >= 0) + { + Assert(v.first < t.getNumChildren()); + Debug("simple-trigger") + << "...set " << v.second << " " << t[v.first] << std::endl; + m.setValue(v.second, t[v.first]); + } + } + // we do not need the trigger parent for simple triggers (no post-processing + // required) + if (qe->getInstantiate()->addInstantiation(d_quant, m)) + { + addedLemmas++; + Debug("simple-trigger") << "-> Produced instantiation " << m << std::endl; + } + return; + } + if (d_match_pattern[argIndex].getKind() == INST_CONSTANT) + { + int v = d_var_num[argIndex]; + if (v != -1) + { + for (std::pair& tt : tat->d_data) + { + Node t = tt.first; + Node prev = m.get(v); + // using representatives, just check if equal + Assert(t.getType().isComparableTo(d_match_pattern_arg_types[argIndex])); + if (prev.isNull() || prev == t) + { + m.setValue(v, t); + addInstantiations(m, qe, addedLemmas, argIndex + 1, &(tt.second)); + m.setValue(v, prev); + if (qe->inConflict()) + { + break; + } + } + } + return; + } + // inst constant from another quantified formula, treat as ground term? + } + Node r = qe->getEqualityQuery()->getRepresentative(d_match_pattern[argIndex]); + std::map::iterator it = tat->d_data.find(r); + if (it != tat->d_data.end()) + { + addInstantiations(m, qe, addedLemmas, argIndex + 1, &(it->second)); + } +} + +int InstMatchGeneratorSimple::getActiveScore(QuantifiersEngine* qe) +{ + Node f = qe->getTermDatabase()->getMatchOperator(d_match_pattern); + size_t ngt = qe->getTermDatabase()->getNumGroundTerms(f); + Trace("trigger-active-sel-debug") << "Number of ground terms for (simple) " + << f << " is " << ngt << std::endl; + return static_cast(ngt); +} + +} // namespace inst +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/quantifiers/ematching/inst_match_generator_simple.h b/src/theory/quantifiers/ematching/inst_match_generator_simple.h new file mode 100644 index 000000000..243050772 --- /dev/null +++ b/src/theory/quantifiers/ematching/inst_match_generator_simple.h @@ -0,0 +1,110 @@ +/********************* */ +/*! \file inst_match_generator_simple.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds, Morgan Deters, Tim King + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief simple inst match generator class + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_SIMPLE_H +#define CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_SIMPLE_H + +#include +#include + +#include "expr/node_trie.h" +#include "theory/quantifiers/ematching/inst_match_generator.h" + +namespace CVC4 { +namespace theory { +namespace inst { + +/** InstMatchGeneratorSimple class + * + * This is the default generator class for simple single triggers. + * For example, { f( x, a ) }, { f( x, x ) } and { f( x, y ) } are simple single + * triggers. In practice, around 70-90% of triggers are simple single triggers. + * + * Notice that simple triggers also can have an attached polarity. + * For example, { P( x ) = false }, { f( x, y ) = a } and { ~f( a, x ) = b } are + * simple single triggers. + * + * The implementation traverses the term indices in TermDatabase for adding + * instantiations, which is more efficient than the techniques required for + * handling non-simple single triggers. + * + * In contrast to other instantiation generators, it does not call + * IMGenerator::sendInstantiation and for performance reasons instead calls + * qe->getInstantiate()->addInstantiation(...) directly. + */ +class InstMatchGeneratorSimple : public IMGenerator +{ + public: + /** constructors */ + InstMatchGeneratorSimple(Node q, Node pat, QuantifiersEngine* qe); + + /** Reset instantiation round. */ + void resetInstantiationRound(QuantifiersEngine* qe) override; + /** Add instantiations. */ + uint64_t addInstantiations(Node q, + QuantifiersEngine* qe, + Trigger* tparent) override; + /** Get active score. */ + int getActiveScore(QuantifiersEngine* qe) override; + + private: + /** quantified formula for the trigger term */ + Node d_quant; + /** the trigger term */ + Node d_match_pattern; + /** equivalence class polarity information + * + * This stores the required polarity/equivalence class with this trigger. + * If d_eqc is non-null, we only produce matches { x->t } such that + * our context does not entail + * ( d_match_pattern*{ x->t } = d_eqc) if d_pol = true, or + * ( d_match_pattern*{ x->t } != d_eqc) if d_pol = false. + * where * denotes application of substitution. + */ + bool d_pol; + Node d_eqc; + /** Match pattern arg types. + * Cached values of d_match_pattern[i].getType(). + */ + std::vector d_match_pattern_arg_types; + /** The match operator d_match_pattern (see TermDb::getMatchOperator). */ + Node d_op; + /** + * Map from child number of d_match_pattern to variable index, or -1 if the + * child is not a variable. + */ + std::map d_var_num; + /** add instantiations, helper function. + * + * m is the current match we are building, + * addedLemmas is the number of lemmas we have added via calls to + * qe->getInstantiate()->aaddInstantiation(...), + * argIndex is the argument index in d_match_pattern we are currently + * matching, + * tat is the term index we are currently traversing. + */ + void addInstantiations(InstMatch& m, + QuantifiersEngine* qe, + uint64_t& addedLemmas, + size_t argIndex, + TNodeTrie* tat); +}; + +} // namespace inst +} // namespace theory +} // namespace CVC4 + +#endif diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp index 4d6dd9f58..34f413b71 100644 --- a/src/theory/quantifiers/ematching/trigger.cpp +++ b/src/theory/quantifiers/ematching/trigger.cpp @@ -19,6 +19,9 @@ #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" +#include "theory/quantifiers/ematching/inst_match_generator_simple.h" #include "theory/quantifiers/instantiate.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/term_database.h" diff --git a/src/theory/quantifiers/ematching/var_match_generator.cpp b/src/theory/quantifiers/ematching/var_match_generator.cpp new file mode 100644 index 000000000..0553c1745 --- /dev/null +++ b/src/theory/quantifiers/ematching/var_match_generator.cpp @@ -0,0 +1,78 @@ +/********************* */ +/*! \file var_match_generator.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds, Morgan Deters, Mathias Preiner + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Implementation of variable match generator class + **/ +#include "theory/quantifiers/ematching/var_match_generator.h" + +#include "theory/quantifiers_engine.h" + +using namespace CVC4::kind; + +namespace CVC4 { +namespace theory { +namespace inst { + +VarMatchGeneratorTermSubs::VarMatchGeneratorTermSubs(Node var, Node subs) + : InstMatchGenerator(), d_var(var), d_subs(subs), d_rm_prev(false) +{ + d_children_types.push_back(d_var.getAttribute(InstVarNumAttribute())); + d_var_type = d_var.getType(); +} + +bool VarMatchGeneratorTermSubs::reset(Node eqc, QuantifiersEngine* qe) +{ + d_eq_class = eqc; + return true; +} + +int VarMatchGeneratorTermSubs::getNextMatch(Node q, + InstMatch& m, + QuantifiersEngine* qe, + Trigger* tparent) +{ + int ret_val = -1; + if (!d_eq_class.isNull()) + { + Trace("var-trigger-matching") << "Matching " << d_eq_class << " against " + << d_var << " in " << d_subs << std::endl; + TNode tvar = d_var; + Node s = d_subs.substitute(tvar, d_eq_class); + s = Rewriter::rewrite(s); + Trace("var-trigger-matching") + << "...got " << s << ", " << s.getKind() << std::endl; + d_eq_class = Node::null(); + // if( s.getType().isSubtypeOf( d_var_type ) ){ + d_rm_prev = m.get(d_children_types[0]).isNull(); + if (!m.set(qe->getEqualityQuery(), d_children_types[0], s)) + { + return -1; + } + else + { + ret_val = continueNextMatch(q, m, qe, tparent); + if (ret_val > 0) + { + return ret_val; + } + } + } + if (d_rm_prev) + { + m.d_vals[d_children_types[0]] = Node::null(); + d_rm_prev = false; + } + return -1; +} + +} // namespace inst +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/quantifiers/ematching/var_match_generator.h b/src/theory/quantifiers/ematching/var_match_generator.h new file mode 100644 index 000000000..c1030e11d --- /dev/null +++ b/src/theory/quantifiers/ematching/var_match_generator.h @@ -0,0 +1,60 @@ +/********************* */ +/*! \file var_match_generator.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds, Morgan Deters, Tim King + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief variable match generator class + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__QUANTIFIERS__VAR_MATCH_GENERATOR_H +#define CVC4__THEORY__QUANTIFIERS__VAR_MATCH_GENERATOR_H + +#include +#include "expr/node.h" +#include "theory/quantifiers/ematching/inst_match_generator.h" + +namespace CVC4 { +namespace theory { +namespace inst { + +/** match generator for purified terms + * This handles the special case of invertible terms like x+1 (see + * Trigger::getTermInversionVariable). + */ +class VarMatchGeneratorTermSubs : public InstMatchGenerator +{ + public: + VarMatchGeneratorTermSubs(Node var, Node subs); + + /** Reset */ + bool reset(Node eqc, QuantifiersEngine* qe) override; + /** Get the next match. */ + int getNextMatch(Node q, + InstMatch& m, + QuantifiersEngine* qe, + Trigger* tparent) override; + + private: + /** variable we are matching (x in the example x+1). */ + Node d_var; + /** cache of d_var.getType() */ + TypeNode d_var_type; + /** The substitution for what we match (x-1 in the example x+1). */ + Node d_subs; + /** stores whether we have written a value for d_var in the current match. */ + bool d_rm_prev; +}; + +} // namespace inst +} // namespace theory +} // namespace CVC4 + +#endif -- 2.30.2