No code changes on this PR, only move + format.
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
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
** 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"
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<const Node, std::vector<Node> >& 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; 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<Node>& 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<Node>& 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<const Node, std::vector<Node> >& 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<uint64_t> unique_vars;
- std::map<uint64_t, bool> shared_vars;
- unsigned numSharedVars = 0;
- std::vector<uint64_t>& 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<uint64_t> vars;
- size_t index = i == 0 ? pats.size() - 1 : (i - 1);
- while( numSharedVars>0 && index!=i ){
- for (std::pair<const uint64_t, bool>& sv : shared_vars)
- {
- if (sv.second)
- {
- std::vector<uint64_t>& 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<const size_t, InstMatchTrie::ImtIndexOrder*>& 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<const Node, InstMatchTrie>& 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<Node, InstMatchTrie>::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<Node, InstMatchTrie>::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<const TNode, TNodeTrie>& 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<unsigned, int>& 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<const TNode, TNodeTrie>& 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<TNode, TNodeTrie>::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<int>(ngt);
-}
-
-
}/* CVC4::theory::inst namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
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<Node>& 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<Node>& 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<Node, std::vector<uint64_t> > d_var_contains;
- /** Map from variable indices to pattern nodes that contain them. */
- std::map<uint64_t, std::vector<Node> > 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<size_t, InstMatchTrie::ImtIndexOrder*> 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<size_t, int> 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 */
}
}
}
--- /dev/null
+/********************* */
+/*! \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<Node>& 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<const Node, std::vector<Node> >& 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<uint64_t> unique_vars;
+ std::map<uint64_t, bool> shared_vars;
+ unsigned numSharedVars = 0;
+ std::vector<uint64_t>& 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<uint64_t> vars;
+ size_t index = i == 0 ? pats.size() - 1 : (i - 1);
+ while (numSharedVars > 0 && index != i)
+ {
+ for (std::pair<const uint64_t, bool>& sv : shared_vars)
+ {
+ if (sv.second)
+ {
+ std::vector<uint64_t>& 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<const size_t, InstMatchTrie::ImtIndexOrder*>& 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<const Node, InstMatchTrie>& 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<Node, InstMatchTrie>::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<Node, InstMatchTrie>::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
--- /dev/null
+/********************* */
+/*! \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 <map>
+#include <vector>
+#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<Node>& 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<Node, std::vector<uint64_t> > d_var_contains;
+ /** Map from variable indices to pattern nodes that contain them. */
+ std::map<uint64_t, std::vector<Node> > 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<size_t, InstMatchTrie::ImtIndexOrder*> 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;
+};
+
+} // namespace inst
+} // namespace theory
+} // namespace CVC4
+
+#endif
--- /dev/null
+/********************* */
+/*! \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<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<const Node, std::vector<Node> >& 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; 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<Node>& 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
--- /dev/null
+/********************* */
+/*! \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 <vector>
+
+#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<Node>& pats,
+ QuantifiersEngine* qe);
+};
+
+} // namespace inst
+} // namespace theory
+} // namespace CVC4
+
+#endif
--- /dev/null
+/********************* */
+/*! \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<const TNode, TNodeTrie>& 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<unsigned, int>& 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<const TNode, TNodeTrie>& 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<TNode, TNodeTrie>::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<int>(ngt);
+}
+
+} // namespace inst
+} // namespace theory
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \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 <map>
+#include <vector>
+
+#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<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<size_t, int> 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
#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"
--- /dev/null
+/********************* */
+/*! \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
--- /dev/null
+/********************* */
+/*! \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 <map>
+#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
projects / cvc5.git / commitdiff