diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-10-23 23:40:29 +0000 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-10-23 23:40:29 +0000 |
commit | 304404e3709ff7e95156c87f65a3e2647d9f3441 (patch) | |
tree | 10fd1c4cc42567c3fac5fd91ad76aef3d49975b5 /src/theory/quantifiers/inst_match.cpp | |
parent | 697dd317af39a896865c99b922e80baac2bb4b23 (diff) |
more major cleanup of quantifiers code, separating rewrite-rules-specific code from quantifiers-specific code
Diffstat (limited to 'src/theory/quantifiers/inst_match.cpp')
-rw-r--r-- | src/theory/quantifiers/inst_match.cpp | 677 |
1 files changed, 2 insertions, 675 deletions
diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp index d00885abf..36f265c30 100644 --- a/src/theory/quantifiers/inst_match.cpp +++ b/src/theory/quantifiers/inst_match.cpp @@ -13,16 +13,9 @@ **/ #include "theory/quantifiers/inst_match.h" -#include "theory/theory_engine.h" -#include "theory/quantifiers_engine.h" -#include "theory/quantifiers/candidate_generator.h" -#include "theory/uf/theory_uf_instantiator.h" -#include "theory/uf/equality_engine.h" -#include "theory/quantifiers/options.h" -#include "theory/quantifiers/model_engine.h" -#include "theory/quantifiers/term_database.h" -#include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/quant_util.h" +#include "theory/quantifiers_engine.h" using namespace std; using namespace CVC4; @@ -216,672 +209,6 @@ bool InstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, b } } -InstMatchGenerator::InstMatchGenerator( Node pat, QuantifiersEngine* qe, int matchPolicy ) : d_matchPolicy( matchPolicy ){ - initializePattern( pat, qe ); -} - -InstMatchGenerator::InstMatchGenerator( std::vector< Node >& pats, QuantifiersEngine* qe, int matchPolicy ) : d_matchPolicy( matchPolicy ){ - if( pats.size()==1 ){ - initializePattern( pats[0], qe ); - }else{ - initializePatterns( pats, qe ); - } -} - -void InstMatchGenerator::initializePatterns( std::vector< Node >& pats, QuantifiersEngine* qe ){ - int childMatchPolicy = d_matchPolicy==MATCH_GEN_EFFICIENT_E_MATCH ? 0 : d_matchPolicy; - for( int i=0; i<(int)pats.size(); i++ ){ - d_children.push_back( new InstMatchGenerator( pats[i], qe, childMatchPolicy ) ); - } - d_pattern = Node::null(); - d_match_pattern = Node::null(); - d_cg = NULL; -} - -void InstMatchGenerator::initializePattern( Node pat, QuantifiersEngine* qe ){ - Debug("inst-match-gen") << "Pattern term is " << pat << std::endl; - Assert( pat.hasAttribute(InstConstantAttribute()) ); - d_pattern = pat; - d_match_pattern = pat; - if( d_match_pattern.getKind()==NOT ){ - //we want to add the children of the NOT - d_match_pattern = d_pattern[0]; - } - if( d_match_pattern.getKind()==IFF || d_match_pattern.getKind()==EQUAL ){ - if( !d_match_pattern[0].hasAttribute(InstConstantAttribute()) ){ - Assert( d_match_pattern[1].hasAttribute(InstConstantAttribute()) ); - //swap sides - d_pattern = NodeManager::currentNM()->mkNode( d_match_pattern.getKind(), d_match_pattern[1], d_match_pattern[0] ); - d_pattern = pat.getKind()==NOT ? d_pattern.notNode() : d_pattern; - if( pat.getKind()!=NOT ){ //TEMPORARY until we do better implementation of disequality matching - d_match_pattern = d_match_pattern[1]; - }else{ - d_match_pattern = d_pattern[0][0]; - } - }else if( !d_match_pattern[1].hasAttribute(InstConstantAttribute()) ){ - Assert( d_match_pattern[0].hasAttribute(InstConstantAttribute()) ); - if( pat.getKind()!=NOT ){ //TEMPORARY until we do better implementation of disequality matching - d_match_pattern = d_match_pattern[0]; - } - } - } - int childMatchPolicy = MATCH_GEN_DEFAULT; - for( int i=0; i<(int)d_match_pattern.getNumChildren(); i++ ){ - if( d_match_pattern[i].hasAttribute(InstConstantAttribute()) ){ - if( d_match_pattern[i].getKind()!=INST_CONSTANT ){ - d_children.push_back( new InstMatchGenerator( d_match_pattern[i], qe, childMatchPolicy ) ); - d_children_index.push_back( i ); - } - } - } - - Debug("inst-match-gen") << "Pattern is " << d_pattern << ", match pattern is " << d_match_pattern << std::endl; - - //create candidate generator - if( d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==IFF ){ - Assert( d_matchPolicy==MATCH_GEN_DEFAULT ); - //we will be producing candidates via literal matching heuristics - if( d_pattern.getKind()!=NOT ){ - //candidates will be all equalities - d_cg = new inst::CandidateGeneratorQELitEq( qe, d_match_pattern ); - }else{ - //candidates will be all disequalities - d_cg = new inst::CandidateGeneratorQELitDeq( qe, d_match_pattern ); - } - }else if( d_pattern.getKind()==EQUAL || d_pattern.getKind()==IFF || d_pattern.getKind()==NOT ){ - Assert( d_matchPolicy==MATCH_GEN_DEFAULT ); - if( d_pattern.getKind()==NOT ){ - Unimplemented("Disequal generator unimplemented"); - }else{ - Assert( Trigger::isAtomicTrigger( d_match_pattern ) ); - //we are matching only in a particular equivalence class - d_cg = new inst::CandidateGeneratorQE( qe, d_match_pattern.getOperator() ); - //store the equivalence class that we will call d_cg->reset( ... ) on - d_eq_class = d_pattern[1]; - } - }else if( Trigger::isAtomicTrigger( d_match_pattern ) ){ - //if( d_matchPolicy==MATCH_GEN_EFFICIENT_E_MATCH ){ - //Warning() << "Currently efficient e matching is not taken into account for quantifiers: " << d_pattern << std::endl; - //} - //we will be scanning lists trying to find d_match_pattern.getOperator() - d_cg = new inst::CandidateGeneratorQE( qe, d_match_pattern.getOperator() ); - }else{ - d_cg = new CandidateGeneratorQueue; - if( !Trigger::getPatternArithmetic( d_match_pattern.getAttribute(InstConstantAttribute()), d_match_pattern, d_arith_coeffs ) ){ - Debug("inst-match-gen") << "(?) Unknown matching pattern is " << d_match_pattern << std::endl; - Warning() << "(?) Unknown matching pattern is " << d_match_pattern << std::endl; - d_matchPolicy = MATCH_GEN_INTERNAL_ERROR; - }else{ - Debug("matching-arith") << "Generated arithmetic pattern for " << d_match_pattern << ": " << std::endl; - for( std::map< Node, Node >::iterator it = d_arith_coeffs.begin(); it != d_arith_coeffs.end(); ++it ){ - Debug("matching-arith") << " " << it->first << " -> " << it->second << std::endl; - } - //we will treat this as match gen internal arithmetic - d_matchPolicy = MATCH_GEN_INTERNAL_ARITHMETIC; - } - } -} - -/** get match (not modulo equality) */ -bool InstMatchGenerator::getMatch( Node t, InstMatch& m, QuantifiersEngine* qe ){ - Debug("matching") << "Matching " << t << " against pattern " << d_match_pattern << " (" - << m.size() << ")" << ", " << d_children.size() << std::endl; - Assert( !d_match_pattern.isNull() ); - if( qe->d_optMatchIgnoreModelBasis && t.getAttribute(ModelBasisAttribute()) ){ - return true; - }else if( d_matchPolicy==MATCH_GEN_INTERNAL_ARITHMETIC ){ - return getMatchArithmetic( t, m, qe ); - }else if( d_matchPolicy==MATCH_GEN_INTERNAL_ERROR ){ - return false; - }else{ - EqualityQuery* q = qe->getEqualityQuery(); - //add m to partial match vector - std::vector< InstMatch > partial; - partial.push_back( InstMatch( &m ) ); - //if t is null - Assert( !t.isNull() ); - Assert( !t.hasAttribute(InstConstantAttribute()) ); - Assert( t.getKind()==d_match_pattern.getKind() ); - Assert( !Trigger::isAtomicTrigger( d_match_pattern ) || t.getOperator()==d_match_pattern.getOperator() ); - //first, check if ground arguments are not equal, or a match is in conflict - for( int i=0; i<(int)d_match_pattern.getNumChildren(); i++ ){ - if( d_match_pattern[i].hasAttribute(InstConstantAttribute()) ){ - if( d_match_pattern[i].getKind()==INST_CONSTANT ){ - if( !partial[0].setMatch( q, d_match_pattern[i], t[i] ) ){ - //match is in conflict - Debug("matching-debug") << "Match in conflict " << t[i] << " and " - << d_match_pattern[i] << " because " - << partial[0].get(d_match_pattern[i]) - << std::endl; - Debug("matching-fail") << "Match fail: " << partial[0].get(d_match_pattern[i]) << " and " << t[i] << std::endl; - return false; - } - } - }else{ - if( !q->areEqual( d_match_pattern[i], t[i] ) ){ - Debug("matching-fail") << "Match fail arg: " << d_match_pattern[i] << " and " << t[i] << std::endl; - //ground arguments are not equal - return false; - } - } - } - //now, fit children into match - //we will be requesting candidates for matching terms for each child - std::vector< Node > reps; - for( int i=0; i<(int)d_children.size(); i++ ){ - Node rep = q->getRepresentative( t[ d_children_index[i] ] ); - reps.push_back( rep ); - d_children[i]->d_cg->reset( rep ); - } - - //combine child matches - int index = 0; - while( index>=0 && index<(int)d_children.size() ){ - partial.push_back( InstMatch( &partial[index] ) ); - if( d_children[index]->getNextMatch2( partial[index+1], qe ) ){ - index++; - }else{ - d_children[index]->d_cg->reset( reps[index] ); - partial.pop_back(); - if( !partial.empty() ){ - partial.pop_back(); - } - index--; - } - } - if( index>=0 ){ - m = partial.back(); - return true; - }else{ - return false; - } - } -} - -bool InstMatchGenerator::getNextMatch2( InstMatch& m, QuantifiersEngine* qe, bool saveMatched ){ - bool success = false; - Node t; - do{ - //get the next candidate term t - t = d_cg->getNextCandidate(); - //if t not null, try to fit it into match m - if( !t.isNull() && t.getType()==d_match_pattern.getType() ){ - success = getMatch( t, m, qe ); - } - }while( !success && !t.isNull() ); - if (saveMatched) m.d_matched = t; - return success; -} - -bool InstMatchGenerator::getMatchArithmetic( Node t, InstMatch& m, QuantifiersEngine* qe ){ - Debug("matching-arith") << "Matching " << t << " " << d_match_pattern << std::endl; - if( !d_arith_coeffs.empty() ){ - NodeBuilder<> tb(kind::PLUS); - Node ic = Node::null(); - for( std::map< Node, Node >::iterator it = d_arith_coeffs.begin(); it != d_arith_coeffs.end(); ++it ){ - Debug("matching-arith") << it->first << " -> " << it->second << std::endl; - if( !it->first.isNull() ){ - if( m.find( it->first )==m.end() ){ - //see if we can choose this to set - if( ic.isNull() && ( it->second.isNull() || !it->first.getType().isInteger() ) ){ - ic = it->first; - } - }else{ - Debug("matching-arith") << "already set " << m.get( it->first ) << std::endl; - Node tm = m.get( it->first ); - if( !it->second.isNull() ){ - tm = NodeManager::currentNM()->mkNode( MULT, it->second, tm ); - } - tb << tm; - } - }else{ - tb << it->second; - } - } - if( !ic.isNull() ){ - Node tm; - if( tb.getNumChildren()==0 ){ - tm = t; - }else{ - tm = tb.getNumChildren()==1 ? tb.getChild( 0 ) : tb; - tm = NodeManager::currentNM()->mkNode( MINUS, t, tm ); - } - if( !d_arith_coeffs[ ic ].isNull() ){ - Assert( !ic.getType().isInteger() ); - Node coeff = NodeManager::currentNM()->mkConst( Rational(1) / d_arith_coeffs[ ic ].getConst<Rational>() ); - tm = NodeManager::currentNM()->mkNode( MULT, coeff, tm ); - } - m.set( ic, Rewriter::rewrite( tm )); - //set the rest to zeros - for( std::map< Node, Node >::iterator it = d_arith_coeffs.begin(); it != d_arith_coeffs.end(); ++it ){ - if( !it->first.isNull() ){ - if( m.find( it->first )==m.end() ){ - m.set( it->first, NodeManager::currentNM()->mkConst( Rational(0) ) ); - } - } - } - Debug("matching-arith") << "Setting " << ic << " to " << tm << std::endl; - return true; - }else{ - return false; - } - }else{ - return false; - } -} - - -/** reset instantiation round */ -void InstMatchGenerator::resetInstantiationRound( QuantifiersEngine* qe ){ - if( d_match_pattern.isNull() ){ - for( int i=0; i<(int)d_children.size(); i++ ){ - d_children[i]->resetInstantiationRound( qe ); - } - }else{ - if( d_cg ){ - d_cg->resetInstantiationRound(); - } - } -} - -void InstMatchGenerator::reset( Node eqc, QuantifiersEngine* qe ){ - if( d_match_pattern.isNull() ){ - for( int i=0; i<(int)d_children.size(); i++ ){ - d_children[i]->reset( eqc, qe ); - } - d_partial.clear(); - }else{ - if( !d_eq_class.isNull() ){ - //we have a specific equivalence class in mind - //we are producing matches for f(E) ~ t, where E is a non-ground vector of terms, and t is a ground term - //just look in equivalence class of the RHS - d_cg->reset( d_eq_class ); - }else{ - d_cg->reset( eqc ); - } - } -} - -bool InstMatchGenerator::getNextMatch( InstMatch& m, QuantifiersEngine* qe ){ - m.d_matched = Node::null(); - if( d_match_pattern.isNull() ){ - int index = (int)d_partial.size(); - while( index>=0 && index<(int)d_children.size() ){ - if( index>0 ){ - d_partial.push_back( InstMatch( &d_partial[index-1] ) ); - }else{ - d_partial.push_back( InstMatch() ); - } - if( d_children[index]->getNextMatch( d_partial[index], qe ) ){ - index++; - }else{ - d_children[index]->reset( Node::null(), qe ); - d_partial.pop_back(); - if( !d_partial.empty() ){ - d_partial.pop_back(); - } - index--; - } - } - if( index>=0 ){ - m = d_partial.back(); - d_partial.pop_back(); - return true; - }else{ - return false; - } - }else{ - bool res = getNextMatch2( m, qe, true ); - Assert(!res || !m.d_matched.isNull()); - return res; - } -} - - - -// Currently the implementation doesn't take into account that -// variable should have the same value given. -// TODO use the d_children way perhaps -// TODO replace by a real dictionnary -// We should create a real substitution? slower more precise -// We don't do that often -bool InstMatchGenerator::nonunifiable( TNode t0, const std::vector<Node> & vars){ - if(d_match_pattern.isNull()) return true; - - typedef std::vector<std::pair<TNode,TNode> > tstack; - tstack stack(1,std::make_pair(t0,d_match_pattern)); // t * pat - - while(!stack.empty()){ - const std::pair<TNode,TNode> p = stack.back(); stack.pop_back(); - const TNode & t = p.first; - const TNode & pat = p.second; - - // t or pat is a variable currently we consider that can match anything - if( find(vars.begin(),vars.end(),t) != vars.end() ) continue; - if( pat.getKind() == INST_CONSTANT ) continue; - - // t and pat are nonunifiable - if( !Trigger::isAtomicTrigger( t ) || !Trigger::isAtomicTrigger( pat ) ) { - if(t == pat) continue; - else return true; - }; - if( t.getOperator() != pat.getOperator() ) return true; - - //put the children on the stack - for( size_t i=0; i < pat.getNumChildren(); i++ ){ - stack.push_back(std::make_pair(t[i],pat[i])); - }; - } - // The heuristic can't find non-unifiability - return false; -} - -int InstMatchGenerator::addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ){ - //now, try to add instantiation for each match produced - int addedLemmas = 0; - InstMatch m; - while( getNextMatch( m, qe ) ){ - //m.makeInternal( d_quantEngine->getEqualityQuery() ); - m.add( baseMatch ); - if( qe->addInstantiation( f, m ) ){ - addedLemmas++; - if( qe->d_optInstLimitActive && qe->d_optInstLimit<=0 ){ - return addedLemmas; - } - } - m.clear(); - } - //return number of lemmas added - return addedLemmas; -} - -int InstMatchGenerator::addTerm( Node f, Node t, QuantifiersEngine* qe ){ - Assert( options::eagerInstQuant() ); - if( !d_match_pattern.isNull() ){ - InstMatch m; - if( getMatch( t, m, qe ) ){ - if( qe->addInstantiation( f, m ) ){ - return 1; - } - } - }else{ - for( int i=0; i<(int)d_children.size(); i++ ){ - d_children[i]->addTerm( f, t, qe ); - } - } - return 0; -} - -/** constructors */ -InstMatchGeneratorMulti::InstMatchGeneratorMulti( Node f, std::vector< Node >& pats, QuantifiersEngine* qe, int matchOption ) : -d_f( f ){ - Debug("smart-multi-trigger") << "Making smart multi-trigger for " << f << std::endl; - std::map< Node, std::vector< Node > > var_contains; - qe->getTermDatabase()->getVarContains( f, pats, var_contains ); - //convert to indicies - for( std::map< Node, std::vector< Node > >::iterator it = var_contains.begin(); it != var_contains.end(); ++it ){ - Debug("smart-multi-trigger") << "Pattern " << it->first << " contains: "; - for( int i=0; i<(int)it->second.size(); i++ ){ - Debug("smart-multi-trigger") << it->second[i] << " "; - int index = it->second[i].getAttribute(InstVarNumAttribute()); - d_var_contains[ it->first ].push_back( index ); - d_var_to_node[ index ].push_back( it->first ); - } - Debug("smart-multi-trigger") << std::endl; - } - for( int i=0; i<(int)pats.size(); i++ ){ - Node n = pats[i]; - //make the match generator - d_children.push_back( new InstMatchGenerator( n, qe, matchOption ) ); - //compute unique/shared variables - std::vector< int > unique_vars; - std::map< int, bool > shared_vars; - int numSharedVars = 0; - for( int j=0; j<(int)d_var_contains[n].size(); j++ ){ - if( d_var_to_node[ d_var_contains[n][j] ].size()==1 ){ - Debug("smart-multi-trigger") << "Var " << d_var_contains[n][j] << " is unique to " << pats[i] << std::endl; - unique_vars.push_back( d_var_contains[n][j] ); - }else{ - shared_vars[ d_var_contains[n][j] ] = true; - numSharedVars++; - } - } - //we use the latest shared variables, then unique variables - std::vector< int > vars; - int index = i==0 ? (int)(pats.size()-1) : (i-1); - while( numSharedVars>0 && index!=i ){ - for( std::map< int, bool >::iterator it = shared_vars.begin(); it != shared_vars.end(); ++it ){ - if( it->second ){ - if( std::find( d_var_contains[ pats[index] ].begin(), d_var_contains[ pats[index] ].end(), it->first )!= - d_var_contains[ pats[index] ].end() ){ - vars.push_back( it->first ); - shared_vars[ it->first ] = false; - numSharedVars--; - } - } - } - index = index==0 ? (int)(pats.size()-1) : (index-1); - } - vars.insert( vars.end(), unique_vars.begin(), unique_vars.end() ); - Debug("smart-multi-trigger") << " Index[" << i << "]: "; - for( int i=0; i<(int)vars.size(); i++ ){ - Debug("smart-multi-trigger") << vars[i] << " "; - } - Debug("smart-multi-trigger") << std::endl; - //make ordered inst match trie - InstMatchTrie::ImtIndexOrder* imtio = new InstMatchTrie::ImtIndexOrder; - imtio->d_order.insert( imtio->d_order.begin(), vars.begin(), vars.end() ); - d_children_trie.push_back( InstMatchTrieOrdered( imtio ) ); - } - -} - -/** reset instantiation round (call this whenever equivalence classes have changed) */ -void InstMatchGeneratorMulti::resetInstantiationRound( QuantifiersEngine* qe ){ - for( int i=0; i<(int)d_children.size(); i++ ){ - d_children[i]->resetInstantiationRound( qe ); - } -} - -/** reset, eqc is the equivalence class to search in (any if eqc=null) */ -void InstMatchGeneratorMulti::reset( Node eqc, QuantifiersEngine* qe ){ - for( int i=0; i<(int)d_children.size(); i++ ){ - d_children[i]->reset( eqc, qe ); - } -} - -int InstMatchGeneratorMulti::addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ){ - int addedLemmas = 0; - Debug("smart-multi-trigger") << "Process smart multi trigger" << std::endl; - for( int i=0; i<(int)d_children.size(); i++ ){ - Debug("smart-multi-trigger") << "Calculate matches " << i << std::endl; - std::vector< InstMatch > newMatches; - InstMatch m; - while( d_children[i]->getNextMatch( m, qe ) ){ - m.makeRepresentative( qe ); - newMatches.push_back( InstMatch( &m ) ); - m.clear(); - } - for( int j=0; j<(int)newMatches.size(); j++ ){ - processNewMatch( qe, newMatches[j], i, addedLemmas ); - } - } - return addedLemmas; -} - -void InstMatchGeneratorMulti::processNewMatch( QuantifiersEngine* qe, InstMatch& m, int fromChildIndex, int& addedLemmas ){ - //see if these produce new matches - d_children_trie[fromChildIndex].addInstMatch( qe, d_f, m, true ); - //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. - Debug("smart-multi-trigger") << "Child " << fromChildIndex << " produced match " << m << std::endl; - //process new instantiations - int childIndex = (fromChildIndex+1)%(int)d_children.size(); - std::vector< IndexedTrie > unique_var_tries; - processNewInstantiations( qe, m, addedLemmas, d_children_trie[childIndex].getTrie(), - unique_var_tries, 0, childIndex, fromChildIndex, true ); -} - -void InstMatchGeneratorMulti::processNewInstantiations( QuantifiersEngine* qe, InstMatch& m, int& addedLemmas, InstMatchTrie* tr, - std::vector< IndexedTrie >& unique_var_tries, - int trieIndex, int childIndex, int endChildIndex, bool modEq ){ - if( childIndex==endChildIndex ){ - //now, process unique variables - processNewInstantiations2( qe, m, addedLemmas, unique_var_tries, 0 ); - }else if( trieIndex<(int)d_children_trie[childIndex].getOrdering()->d_order.size() ){ - int curr_index = d_children_trie[childIndex].getOrdering()->d_order[trieIndex]; - Node curr_ic = qe->getTermDatabase()->getInstantiationConstant( d_f, curr_index ); - if( m.find( curr_ic )==m.end() ){ - //if( d_var_to_node[ curr_index ].size()==1 ){ //FIXME - // //unique variable(s), defer calculation - // unique_var_tries.push_back( IndexedTrie( std::pair< int, int >( childIndex, trieIndex ), tr ) ); - // int newChildIndex = (childIndex+1)%(int)d_children.size(); - // processNewInstantiations( qe, m, d_children_trie[newChildIndex].getTrie(), unique_var_tries, - // 0, newChildIndex, endChildIndex, modEq ); - //}else{ - //shared and non-set variable, add to InstMatch - for( std::map< Node, InstMatchTrie >::iterator it = tr->d_data.begin(); it != tr->d_data.end(); ++it ){ - InstMatch mn( &m ); - mn.set( curr_ic, it->first); - processNewInstantiations( qe, mn, addedLemmas, &(it->second), unique_var_tries, - trieIndex+1, childIndex, endChildIndex, modEq ); - } - //} - }else{ - //shared and set variable, try to merge - Node n = m.get( curr_ic ); - std::map< Node, InstMatchTrie >::iterator it = tr->d_data.find( n ); - if( it!=tr->d_data.end() ){ - processNewInstantiations( qe, m, addedLemmas, &(it->second), unique_var_tries, - trieIndex+1, childIndex, endChildIndex, modEq ); - } - if( modEq ){ - //check modulo equality for other possible instantiations - if( qe->getEqualityQuery()->getEngine()->hasTerm( n ) ){ - eq::EqClassIterator eqc( qe->getEqualityQuery()->getEngine()->getRepresentative( n ), - qe->getEqualityQuery()->getEngine() ); - 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, m, addedLemmas, &(itc->second), unique_var_tries, - trieIndex+1, childIndex, endChildIndex, modEq ); - } - } - ++eqc; - } - } - } - } - }else{ - int newChildIndex = (childIndex+1)%(int)d_children.size(); - processNewInstantiations( qe, m, addedLemmas, d_children_trie[newChildIndex].getTrie(), unique_var_tries, - 0, newChildIndex, endChildIndex, modEq ); - } -} - -void InstMatchGeneratorMulti::processNewInstantiations2( QuantifiersEngine* qe, InstMatch& m, int& addedLemmas, - std::vector< IndexedTrie >& unique_var_tries, - int uvtIndex, InstMatchTrie* tr, int trieIndex ){ - if( uvtIndex<(int)unique_var_tries.size() ){ - int childIndex = unique_var_tries[uvtIndex].first.first; - if( !tr ){ - tr = unique_var_tries[uvtIndex].second; - trieIndex = unique_var_tries[uvtIndex].first.second; - } - if( trieIndex<(int)d_children_trie[childIndex].getOrdering()->d_order.size() ){ - int curr_index = d_children_trie[childIndex].getOrdering()->d_order[trieIndex]; - Node curr_ic = qe->getTermDatabase()->getInstantiationConstant( d_f, curr_index ); - //unique non-set variable, add to InstMatch - for( std::map< Node, InstMatchTrie >::iterator it = tr->d_data.begin(); it != tr->d_data.end(); ++it ){ - InstMatch mn( &m ); - mn.set( curr_ic, it->first); - processNewInstantiations2( qe, mn, addedLemmas, unique_var_tries, uvtIndex, &(it->second), trieIndex+1 ); - } - }else{ - processNewInstantiations2( qe, m, addedLemmas, unique_var_tries, uvtIndex+1 ); - } - }else{ - //m is an instantiation - if( qe->addInstantiation( d_f, m ) ){ - addedLemmas++; - Debug("smart-multi-trigger") << "-> Produced instantiation " << m << std::endl; - } - } -} - -int InstMatchGeneratorMulti::addTerm( Node f, Node t, QuantifiersEngine* qe ){ - Assert( options::eagerInstQuant() ); - int addedLemmas = 0; - for( int i=0; i<(int)d_children.size(); i++ ){ - if( ((InstMatchGenerator*)d_children[i])->d_match_pattern.getOperator()==t.getOperator() ){ - InstMatch m; - //if it produces a match, then process it with the rest - if( ((InstMatchGenerator*)d_children[i])->getMatch( t, m, qe ) ){ - processNewMatch( qe, m, i, addedLemmas ); - } - } - } - return addedLemmas; -} - -int InstMatchGeneratorSimple::addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ){ - InstMatch m; - m.add( baseMatch ); - int addedLemmas = 0; - if( d_match_pattern.getType()==NodeManager::currentNM()->booleanType() ){ - for( int i=0; i<2; i++ ){ - addInstantiations( m, qe, addedLemmas, 0, &(qe->getTermDatabase()->d_pred_map_trie[i][ d_match_pattern.getOperator() ]) ); - } - }else{ - addInstantiations( m, qe, addedLemmas, 0, &(qe->getTermDatabase()->d_func_map_trie[ d_match_pattern.getOperator() ]) ); - } - return addedLemmas; -} - -void InstMatchGeneratorSimple::addInstantiations( InstMatch& m, QuantifiersEngine* qe, int& addedLemmas, int argIndex, quantifiers::TermArgTrie* tat ){ - if( argIndex==(int)d_match_pattern.getNumChildren() ){ - //m is an instantiation - if( qe->addInstantiation( d_f, m ) ){ - addedLemmas++; - Debug("simple-multi-trigger") << "-> Produced instantiation " << m << std::endl; - } - }else{ - if( d_match_pattern[argIndex].getKind()==INST_CONSTANT ){ - Node ic = d_match_pattern[argIndex]; - for( std::map< Node, quantifiers::TermArgTrie >::iterator it = tat->d_data.begin(); it != tat->d_data.end(); ++it ){ - Node t = it->first; - if( m.get( ic ).isNull() || m.get( ic )==t ){ - Node prev = m.get( ic ); - m.set( ic, t); - addInstantiations( m, qe, addedLemmas, argIndex+1, &(it->second) ); - m.set( ic, prev); - } - } - }else{ - Node r = qe->getEqualityQuery()->getRepresentative( d_match_pattern[argIndex] ); - std::map< Node, quantifiers::TermArgTrie >::iterator it = tat->d_data.find( r ); - if( it!=tat->d_data.end() ){ - addInstantiations( m, qe, addedLemmas, argIndex+1, &(it->second) ); - } - } - } -} - -int InstMatchGeneratorSimple::addTerm( Node f, Node t, QuantifiersEngine* qe ){ - Assert( options::eagerInstQuant() ); - InstMatch m; - for( int i=0; i<(int)t.getNumChildren(); i++ ){ - if( d_match_pattern[i].getKind()==INST_CONSTANT ){ - m.set(d_match_pattern[i], t[i]); - }else if( !qe->getEqualityQuery()->areEqual( d_match_pattern[i], t[i] ) ){ - return 0; - } - } - return qe->addInstantiation( f, m ) ? 1 : 0; -} }/* CVC4::theory::inst namespace */ }/* CVC4::theory namespace */ |