From: Andrew Reynolds Date: Tue, 23 Oct 2012 23:40:29 +0000 (+0000) Subject: more major cleanup of quantifiers code, separating rewrite-rules-specific code from... X-Git-Tag: cvc5-1.0.0~7681 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=304404e3709ff7e95156c87f65a3e2647d9f3441;p=cvc5.git more major cleanup of quantifiers code, separating rewrite-rules-specific code from quantifiers-specific code --- diff --git a/src/theory/quantifiers/Makefile.am b/src/theory/quantifiers/Makefile.am index 57b99c59b..ed60e77a9 100644 --- a/src/theory/quantifiers/Makefile.am +++ b/src/theory/quantifiers/Makefile.am @@ -40,7 +40,9 @@ libquantifiers_la_SOURCES = \ inst_gen.h \ inst_gen.cpp \ quant_util.h \ - quant_util.cpp + quant_util.cpp \ + inst_match_generator.h \ + inst_match_generator.cpp EXTRA_DIST = \ kinds \ diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h index c8fcb7c44..3779579fd 100644 --- a/src/theory/quantifiers/first_order_model.h +++ b/src/theory/quantifiers/first_order_model.h @@ -24,13 +24,6 @@ namespace CVC4 { namespace theory { -struct ModelBasisAttributeId {}; -typedef expr::Attribute ModelBasisAttribute; -//for APPLY_UF terms, 1 : term has direct child with model basis attribute, -// 0 : term has no direct child with model basis attribute. -struct ModelBasisArgAttributeId {}; -typedef expr::Attribute ModelBasisArgAttribute; - class QuantifiersEngine; namespace quantifiers{ 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() ); - 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 & vars){ - if(d_match_pattern.isNull()) return true; - - typedef std::vector > tstack; - tstack stack(1,std::make_pair(t0,d_match_pattern)); // t * pat - - while(!stack.empty()){ - const std::pair 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 */ diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h index a0db1336f..426adc02d 100644 --- a/src/theory/quantifiers/inst_match.h +++ b/src/theory/quantifiers/inst_match.h @@ -20,81 +20,19 @@ #include "util/hash.h" #include -#include #include #include "context/cdlist.h" -#include "theory/quantifiers/candidate_generator.h" - -//#define USE_EFFICIENT_E_MATCHING +#include "expr/node.h" namespace CVC4 { namespace theory { -/** Attribute true for nodes that should not be used for matching */ -struct NoMatchAttributeId {}; -/** use the special for boolean flag */ -typedef expr::Attribute< NoMatchAttributeId, - bool, - expr::attr::NullCleanupStrategy, - true // context dependent - > NoMatchAttribute; - -// attribute for "contains instantiation constants from" -struct InstConstantAttributeId {}; -typedef expr::Attribute InstConstantAttribute; - -struct InstLevelAttributeId {}; -typedef expr::Attribute InstLevelAttribute; - -struct InstVarNumAttributeId {}; -typedef expr::Attribute InstVarNumAttribute; - -// Attribute that tell if a node have been asserted in this branch -struct AvailableInTermDbId {}; -/** use the special for boolean flag */ -typedef expr::Attribute AvailableInTermDb; - - class QuantifiersEngine; -namespace quantifiers{ - class TermArgTrie; -} - -namespace uf{ - class InstantiatorTheoryUf; - class TheoryUF; -}/* CVC4::theory::uf namespace */ +class EqualityQuery; namespace inst { -class EqualityQuery { -public: - EqualityQuery(){} - virtual ~EqualityQuery(){}; - /** contains term */ - virtual bool hasTerm( Node a ) = 0; - /** get the representative of the equivalence class of a */ - virtual Node getRepresentative( Node a ) = 0; - /** returns true if a and b are equal in the current context */ - virtual bool areEqual( Node a, Node b ) = 0; - /** returns true is a and b are disequal in the current context */ - virtual bool areDisequal( Node a, Node b ) = 0; - /** getInternalRepresentative gets the current best representative in the equivalence class of a, based on some criteria. - If cbqi is active, this will return a term in the equivalence class of "a" that does - not contain instantiation constants, if such a term exists. - */ - virtual Node getInternalRepresentative( Node a ) = 0; - /** get the equality engine associated with this query */ - virtual eq::EqualityEngine* getEngine() = 0; - /** get the equivalence class of a */ - virtual void getEquivalenceClass( Node a, std::vector< Node >& eqc ) = 0; -};/* class EqualityQuery */ - /** basic class defining an instantiation */ class InstMatch { /* map from variable to ground terms */ @@ -230,176 +168,9 @@ public: } };/* class InstMatchTrieOrdered */ -/** base class for producing InstMatch objects */ -class IMGenerator { -public: - /** reset instantiation round (call this at beginning of instantiation round) */ - virtual void resetInstantiationRound( QuantifiersEngine* qe ) = 0; - /** reset, eqc is the equivalence class to search in (any if eqc=null) */ - virtual void reset( Node eqc, QuantifiersEngine* qe ) = 0; - /** get the next match. must call reset( eqc ) before this function. */ - virtual bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ) = 0; - /** return true if whatever Node is substituted for the variables the - given Node can't match the pattern */ - virtual bool nonunifiable( TNode t, const std::vector & vars) = 0; - /** add instantiations directly */ - virtual int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ) = 0; - /** add ground term t, called when t is added to term db */ - virtual int addTerm( Node f, Node t, QuantifiersEngine* qe ) = 0; -};/* class IMGenerator */ - - -class InstMatchGenerator : public IMGenerator { -private: - /** candidate generator */ - CandidateGenerator* d_cg; - /** policy to use for matching */ - int d_matchPolicy; - /** children generators */ - std::vector< InstMatchGenerator* > d_children; - std::vector< int > d_children_index; - /** partial vector */ - std::vector< InstMatch > d_partial; - /** eq class */ - Node d_eq_class; - /** for arithmetic matching */ - std::map< Node, Node > d_arith_coeffs; - /** initialize pattern */ - void initializePatterns( std::vector< Node >& pats, QuantifiersEngine* qe ); - void initializePattern( Node pat, QuantifiersEngine* qe ); -public: - enum { - //options for producing matches - MATCH_GEN_DEFAULT = 0, - MATCH_GEN_EFFICIENT_E_MATCH, //generate matches via Efficient E-matching for SMT solvers - //others (internally used) - MATCH_GEN_INTERNAL_ARITHMETIC, - MATCH_GEN_INTERNAL_ERROR, - }; -private: - /** get the next match. must call d_cg->reset( ... ) before using. - only valid for use where !d_match_pattern.isNull(). - */ - bool getNextMatch2( InstMatch& m, QuantifiersEngine* qe, bool saveMatched = false ); - /** for arithmetic */ - bool getMatchArithmetic( Node t, InstMatch& m, QuantifiersEngine* qe ); -public: - /** get the match against ground term or formula t. - d_match_pattern and t should have the same shape. - only valid for use where !d_match_pattern.isNull(). - */ - bool getMatch( Node t, InstMatch& m, QuantifiersEngine* qe ); - - /** constructors */ - InstMatchGenerator( Node pat, QuantifiersEngine* qe, int matchOption = 0 ); - InstMatchGenerator( std::vector< Node >& pats, QuantifiersEngine* qe, int matchOption = 0 ); - /** destructor */ - ~InstMatchGenerator(){} - /** The pattern we are producing matches for. - If null, this is a multi trigger that is merging matches from d_children. - */ - Node d_pattern; - /** match pattern */ - Node d_match_pattern; -public: - /** reset instantiation round (call this whenever equivalence classes have changed) */ - void resetInstantiationRound( QuantifiersEngine* qe ); - /** reset, eqc is the equivalence class to search in (any if eqc=null) */ - void reset( Node eqc, QuantifiersEngine* qe ); - /** get the next match. must call reset( eqc ) before this function. */ - bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ); - /** return true if whatever Node is substituted for the variables the - given Node can't match the pattern */ - bool nonunifiable( TNode t, const std::vector & vars); - /** add instantiations */ - int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ); - /** add ground term t */ - int addTerm( Node f, Node t, QuantifiersEngine* qe ); -};/* class InstMatchGenerator */ - -/** smart multi-trigger implementation */ -class InstMatchGeneratorMulti : public IMGenerator { -private: - /** indexed trie */ - typedef std::pair< std::pair< int, int >, InstMatchTrie* > IndexedTrie; - /** process new match */ - void processNewMatch( QuantifiersEngine* qe, InstMatch& m, int fromChildIndex, int& addedLemmas ); - /** process new instantiations */ - void processNewInstantiations( QuantifiersEngine* qe, InstMatch& m, int& addedLemmas, InstMatchTrie* tr, - std::vector< IndexedTrie >& unique_var_tries, - int trieIndex, int childIndex, int endChildIndex, bool modEq ); - /** process new instantiations 2 */ - void processNewInstantiations2( QuantifiersEngine* qe, InstMatch& m, int& addedLemmas, - std::vector< IndexedTrie >& unique_var_tries, - int uvtIndex, InstMatchTrie* tr = NULL, int trieIndex = 0 ); -private: - /** var contains (variable indices) for each pattern node */ - std::map< Node, std::vector< int > > d_var_contains; - /** variable indices contained to pattern nodes */ - std::map< int, std::vector< Node > > d_var_to_node; - /** quantifier to use */ - Node d_f; - /** policy to use for matching */ - int d_matchPolicy; - /** children generators */ - std::vector< InstMatchGenerator* > d_children; - /** inst match tries for each child */ - std::vector< InstMatchTrieOrdered > d_children_trie; - /** calculate matches */ - void calculateMatches( QuantifiersEngine* qe ); -public: - /** constructors */ - InstMatchGeneratorMulti( Node f, std::vector< Node >& pats, QuantifiersEngine* qe, int matchOption = 0 ); - /** destructor */ - ~InstMatchGeneratorMulti(){} - /** reset instantiation round (call this whenever equivalence classes have changed) */ - void resetInstantiationRound( QuantifiersEngine* qe ); - /** reset, eqc is the equivalence class to search in (any if eqc=null) */ - void reset( Node eqc, QuantifiersEngine* qe ); - /** get the next match. must call reset( eqc ) before this function. (not implemented) */ - bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ) { return false; } - /** return true if whatever Node is substituted for the variables the - given Node can't match the pattern */ - bool nonunifiable( TNode t, const std::vector & vars) { return true; } - /** add instantiations */ - int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ); - /** add ground term t */ - int addTerm( Node f, Node t, QuantifiersEngine* qe ); -};/* class InstMatchGeneratorMulti */ - -/** smart (single)-trigger implementation */ -class InstMatchGeneratorSimple : public IMGenerator { -private: - /** quantifier for match term */ - Node d_f; - /** match term */ - Node d_match_pattern; - /** add instantiations */ - void addInstantiations( InstMatch& m, QuantifiersEngine* qe, int& addedLemmas, int argIndex, quantifiers::TermArgTrie* tat ); -public: - /** constructors */ - InstMatchGeneratorSimple( Node f, Node pat ) : d_f( f ), d_match_pattern( pat ){} - /** destructor */ - ~InstMatchGeneratorSimple(){} - /** reset instantiation round (call this whenever equivalence classes have changed) */ - void resetInstantiationRound( QuantifiersEngine* qe ) {} - /** reset, eqc is the equivalence class to search in (any if eqc=null) */ - void reset( Node eqc, QuantifiersEngine* qe ) {} - /** get the next match. must call reset( eqc ) before this function. (not implemented) */ - bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ) { return false; } - /** return true if whatever Node is substituted for the variables the - given Node can't match the pattern */ - bool nonunifiable( TNode t, const std::vector & vars) { return true; } - /** add instantiations */ - int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ); - /** add ground term t, possibly add instantiations */ - int addTerm( Node f, Node t, QuantifiersEngine* qe ); -};/* class InstMatchGeneratorSimple */ - }/* CVC4::theory::inst namespace */ typedef CVC4::theory::inst::InstMatch InstMatch; -typedef CVC4::theory::inst::EqualityQuery EqualityQuery; }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp new file mode 100755 index 000000000..acd733e22 --- /dev/null +++ b/src/theory/quantifiers/inst_match_generator.cpp @@ -0,0 +1,664 @@ +/********************* */ +/*! \file inst_match_generator.cpp +** \verbatim +** Original author: ajreynol +** Major contributors: bobot +** Minor contributors (to current version): barrett, mdeters +** This file is part of the CVC4 prototype. +** Copyright (c) 2009-2012 New York University and The University of Iowa +** See the file COPYING in the top-level source directory for licensing +** information.\endverbatim +** +** \brief Implementation of inst match generator class +**/ + +#include "theory/quantifiers/inst_match_generator.h" +#include "theory/quantifiers/trigger.h" +#include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/candidate_generator.h" +#include "theory/quantifiers_engine.h" + +using namespace std; +using namespace CVC4; +using namespace CVC4::kind; +using namespace CVC4::context; +using namespace CVC4::theory; + +namespace CVC4 { +namespace theory { +namespace inst { + + +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() ); + 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; + } +} + + + +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 */ +}/* CVC4 namespace */ diff --git a/src/theory/quantifiers/inst_match_generator.h b/src/theory/quantifiers/inst_match_generator.h new file mode 100755 index 000000000..af65e809b --- /dev/null +++ b/src/theory/quantifiers/inst_match_generator.h @@ -0,0 +1,192 @@ +/********************* */ +/*! \file inst_match_generator.h + ** \verbatim + ** Original author: ajreynol + ** Major contributors: bobot + ** Minor contributors (to current version): mdeters + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief inst match generator class + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_H +#define __CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_H + +#include "theory/quantifiers/inst_match.h" +#include + +namespace CVC4 { +namespace theory { + +class QuantifiersEngine; +namespace quantifiers{ + class TermArgTrie; +} + +namespace inst { + +/** base class for producing InstMatch objects */ +class IMGenerator { +public: + /** reset instantiation round (call this at beginning of instantiation round) */ + virtual void resetInstantiationRound( QuantifiersEngine* qe ) = 0; + /** reset, eqc is the equivalence class to search in (any if eqc=null) */ + virtual void reset( Node eqc, QuantifiersEngine* qe ) = 0; + /** get the next match. must call reset( eqc ) before this function. */ + virtual bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ) = 0; + /** add instantiations directly */ + virtual int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ) = 0; + /** add ground term t, called when t is added to term db */ + virtual int addTerm( Node f, Node t, QuantifiersEngine* qe ) = 0; +};/* class IMGenerator */ + +class CandidateGenerator; + +class InstMatchGenerator : public IMGenerator { +private: + /** candidate generator */ + CandidateGenerator* d_cg; + /** policy to use for matching */ + int d_matchPolicy; + /** children generators */ + std::vector< InstMatchGenerator* > d_children; + std::vector< int > d_children_index; + /** partial vector */ + std::vector< InstMatch > d_partial; + /** eq class */ + Node d_eq_class; + /** for arithmetic matching */ + std::map< Node, Node > d_arith_coeffs; + /** initialize pattern */ + void initializePatterns( std::vector< Node >& pats, QuantifiersEngine* qe ); + void initializePattern( Node pat, QuantifiersEngine* qe ); +public: + enum { + //options for producing matches + MATCH_GEN_DEFAULT = 0, + MATCH_GEN_EFFICIENT_E_MATCH, //generate matches via Efficient E-matching for SMT solvers + //others (internally used) + MATCH_GEN_INTERNAL_ARITHMETIC, + MATCH_GEN_INTERNAL_ERROR, + }; +private: + /** get the next match. must call d_cg->reset( ... ) before using. + only valid for use where !d_match_pattern.isNull(). + */ + bool getNextMatch2( InstMatch& m, QuantifiersEngine* qe, bool saveMatched = false ); + /** for arithmetic */ + bool getMatchArithmetic( Node t, InstMatch& m, QuantifiersEngine* qe ); +public: + /** get the match against ground term or formula t. + d_match_pattern and t should have the same shape. + only valid for use where !d_match_pattern.isNull(). + */ + bool getMatch( Node t, InstMatch& m, QuantifiersEngine* qe ); + + /** constructors */ + InstMatchGenerator( Node pat, QuantifiersEngine* qe, int matchOption = 0 ); + InstMatchGenerator( std::vector< Node >& pats, QuantifiersEngine* qe, int matchOption = 0 ); + /** destructor */ + ~InstMatchGenerator(){} + /** The pattern we are producing matches for. + If null, this is a multi trigger that is merging matches from d_children. + */ + Node d_pattern; + /** match pattern */ + Node d_match_pattern; +public: + /** reset instantiation round (call this whenever equivalence classes have changed) */ + void resetInstantiationRound( QuantifiersEngine* qe ); + /** reset, eqc is the equivalence class to search in (any if eqc=null) */ + void reset( Node eqc, QuantifiersEngine* qe ); + /** get the next match. must call reset( eqc ) before this function. */ + bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ); + /** add instantiations */ + int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ); + /** add ground term t */ + int addTerm( Node f, Node t, QuantifiersEngine* qe ); +};/* class InstMatchGenerator */ + +/** smart multi-trigger implementation */ +class InstMatchGeneratorMulti : public IMGenerator { +private: + /** indexed trie */ + typedef std::pair< std::pair< int, int >, InstMatchTrie* > IndexedTrie; + /** process new match */ + void processNewMatch( QuantifiersEngine* qe, InstMatch& m, int fromChildIndex, int& addedLemmas ); + /** process new instantiations */ + void processNewInstantiations( QuantifiersEngine* qe, InstMatch& m, int& addedLemmas, InstMatchTrie* tr, + std::vector< IndexedTrie >& unique_var_tries, + int trieIndex, int childIndex, int endChildIndex, bool modEq ); + /** process new instantiations 2 */ + void processNewInstantiations2( QuantifiersEngine* qe, InstMatch& m, int& addedLemmas, + std::vector< IndexedTrie >& unique_var_tries, + int uvtIndex, InstMatchTrie* tr = NULL, int trieIndex = 0 ); +private: + /** var contains (variable indices) for each pattern node */ + std::map< Node, std::vector< int > > d_var_contains; + /** variable indices contained to pattern nodes */ + std::map< int, std::vector< Node > > d_var_to_node; + /** quantifier to use */ + Node d_f; + /** policy to use for matching */ + int d_matchPolicy; + /** children generators */ + std::vector< InstMatchGenerator* > d_children; + /** inst match tries for each child */ + std::vector< InstMatchTrieOrdered > d_children_trie; + /** calculate matches */ + void calculateMatches( QuantifiersEngine* qe ); +public: + /** constructors */ + InstMatchGeneratorMulti( Node f, std::vector< Node >& pats, QuantifiersEngine* qe, int matchOption = 0 ); + /** destructor */ + ~InstMatchGeneratorMulti(){} + /** reset instantiation round (call this whenever equivalence classes have changed) */ + void resetInstantiationRound( QuantifiersEngine* qe ); + /** reset, eqc is the equivalence class to search in (any if eqc=null) */ + void reset( Node eqc, QuantifiersEngine* qe ); + /** get the next match. must call reset( eqc ) before this function. (not implemented) */ + bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ) { return false; } + /** add instantiations */ + int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ); + /** add ground term t */ + int addTerm( Node f, Node t, QuantifiersEngine* qe ); +};/* class InstMatchGeneratorMulti */ + +/** smart (single)-trigger implementation */ +class InstMatchGeneratorSimple : public IMGenerator { +private: + /** quantifier for match term */ + Node d_f; + /** match term */ + Node d_match_pattern; + /** add instantiations */ + void addInstantiations( InstMatch& m, QuantifiersEngine* qe, int& addedLemmas, int argIndex, quantifiers::TermArgTrie* tat ); +public: + /** constructors */ + InstMatchGeneratorSimple( Node f, Node pat ) : d_f( f ), d_match_pattern( pat ){} + /** destructor */ + ~InstMatchGeneratorSimple(){} + /** reset instantiation round (call this whenever equivalence classes have changed) */ + void resetInstantiationRound( QuantifiersEngine* qe ) {} + /** reset, eqc is the equivalence class to search in (any if eqc=null) */ + void reset( Node eqc, QuantifiersEngine* qe ) {} + /** get the next match. must call reset( eqc ) before this function. (not implemented) */ + bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ) { return false; } + /** add instantiations */ + int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ); + /** add ground term t, possibly add instantiations */ + int addTerm( Node f, Node t, QuantifiersEngine* qe ); +};/* class InstMatchGeneratorSimple */ + +} +} +} + +#endif diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp index f61083029..598b50957 100644 --- a/src/theory/quantifiers/model_builder.cpp +++ b/src/theory/quantifiers/model_builder.cpp @@ -243,10 +243,12 @@ void ModelEngineBuilder::analyzeModel( FirstOrderModel* fm ){ } //for calculating terms that we don't need to consider if( !n.getAttribute(NoMatchAttribute()) || n.getAttribute(ModelBasisArgAttribute())==1 ){ - //need to consider if it is not congruent modulo model basis - if( !tabt.addTerm( d_qe, n ) ){ - BasisNoMatchAttribute bnma; - n.setAttribute(bnma,true); + if( !n.getAttribute(BasisNoMatchAttribute()) ){ + //need to consider if it is not congruent modulo model basis + if( !tabt.addTerm( d_qe, n ) ){ + BasisNoMatchAttribute bnma; + n.setAttribute(bnma,true); + } } } } @@ -263,6 +265,17 @@ void ModelEngineBuilder::analyzeModel( FirstOrderModel* fm ){ } } +bool ModelEngineBuilder::hasConstantDefinition( Node n ){ + Node lit = n.getKind()==NOT ? n[0] : n; + if( lit.getKind()==APPLY_UF ){ + Node op = lit.getOperator(); + if( !d_uf_prefs[op].d_const_val.isNull() ){ + return true; + } + } + return false; +} + bool ModelEngineBuilder::optUseModel() { return options::fmfModelBasedInst(); } @@ -305,8 +318,8 @@ bool ModelEngineBuilder::isQuantifierActive( Node f ){ bool ModelEngineBuilder::isTermActive( Node n ){ return !n.getAttribute(NoMatchAttribute()) || //it is not congruent to another active term ( n.getAttribute(ModelBasisArgAttribute())==1 && !n.getAttribute(BasisNoMatchAttribute()) ); //or it has model basis arguments - //and is not congruent to another - //active term + //and is not congruent modulo model basis + //to another active term } @@ -347,7 +360,7 @@ void ModelEngineBuilderDefault::analyzeQuantifier( FirstOrderModel* fm, Node f ) isConst = false; if( gn.getKind()==APPLY_UF ){ uf_terms.push_back( gn ); - isConst = !d_uf_prefs[gn.getOperator()].d_const_val.isNull(); + isConst = hasConstantDefinition( gn ); }else if( gn.getKind()==EQUAL ){ isConst = true; for( int j=0; j<2; j++ ){ @@ -355,7 +368,7 @@ void ModelEngineBuilderDefault::analyzeQuantifier( FirstOrderModel* fm, Node f ) if( n[j].getKind()==APPLY_UF && fm->d_uf_model_tree.find( gn[j].getOperator() )!=fm->d_uf_model_tree.end() ){ uf_terms.push_back( gn[j] ); - isConst = isConst && !d_uf_prefs[ gn[j].getOperator() ].d_const_val.isNull(); + isConst = isConst && hasConstantDefinition( gn[j] ); }else{ isConst = false; } @@ -456,10 +469,8 @@ int ModelEngineBuilderDefault::doInstGen( FirstOrderModel* fm, Node f ){ std::vector< Node > tr_terms; if( lit.getKind()==APPLY_UF ){ //only match predicates that are contrary to this one, use literal matching - std::vector< Node > children; - children.push_back( lit ); - children.push_back( !phase ? fm->d_true : fm->d_false ); - Node eq = d_qe->getTermDatabase()->mkNodeInstConstant( IFF, children, f ); + Node eq = NodeManager::currentNM()->mkNode( IFF, lit, !phase ? fm->d_true : fm->d_false ); + d_qe->getTermDatabase()->setInstantiationConstantAttr( eq, f ); tr_terms.push_back( eq ); }else if( lit.getKind()==EQUAL ){ //collect trigger terms @@ -595,10 +606,16 @@ void ModelEngineBuilderInstGen::analyzeQuantifier( FirstOrderModel* fm, Node f ) d_quant_selection_formula[f] = s; Node gs = d_qe->getTermDatabase()->getModelBasis( f, s ); setSelectedTerms( gs ); + //quick check if it is constant sat + if( hasConstantDefinition( s ) ){ + d_quant_sat[f] = true; + } } //analyze sub quantifiers - for( size_t i=0; i0 ){ - Trace("inst-gen") << " -> children added lemmas" << std::endl; - return addedLemmas; - }else{ - Trace("inst-gen-debug") << "Calculate inst-gen instantiations..." << std::endl; - //get all possible values of selection formula - InstGenProcess igp( d_quant_selection_formula[f] ); - igp.calculateMatches( d_qe, f ); - Trace("inst-gen-debug") << "Add inst-gen instantiations (" << igp.getNumMatches() << ")..." << std::endl; - for( int i=0; id_true ){ - InstMatch m; - igp.getMatch( d_qe->getEqualityQuery(), i, m ); - //we only consider matches that are non-empty - // matches that are empty should trigger other instances that are non-empty - if( !m.empty() ){ - Trace("inst-gen-debug") << "Get in terms of parent..." << std::endl; - //translate to be in terms match in terms of fp - InstMatch mp; - getParentQuantifierMatch( mp, fp, m, f ); - - //if this is a partial instantion - if( !m.isComplete( f ) ){ - //if the instantiation does not yet exist - if( d_sub_quant_inst_trie[fp].addInstMatch( d_qe, fp, mp, true ) ){ - //get the partial instantiation pf - Node pf = d_qe->getInstantiation( fp, mp ); - Trace("inst-gen-pi") << "Partial instantiation of " << f << std::endl; - Trace("inst-gen-pi") << " " << pf << std::endl; - d_sub_quants[ f ].push_back( pf ); - d_sub_quant_inst[ pf ] = InstMatch( &mp ); - d_sub_quant_parent[ pf ] = fp; - mp.add( d_quant_basis_match[ fp ] ); - d_quant_basis_match[ pf ] = InstMatch( &mp ); - addedLemmas += initializeQuantifier( pf, fp ); - Trace("inst-gen-pi") << "Done adding partial instantiation" << std::endl; - } - }else{ - if( d_qe->addInstantiation( fp, mp ) ){ - addedLemmas++; + if( d_quant_sat.find( f )==d_quant_sat.end() ){ + //we wish to add all known exceptions to our selection literal for f. this will help to refine our current model. + //This step is advantageous over exhaustive instantiation, since we are adding instantiations that involve model basis terms, + // effectively acting as partial instantiations instead of pointwise instantiations. + if( !d_quant_selection_formula[f].isNull() ){ + //first, try on sub quantifiers + for( size_t i=0; i0 ){ + Trace("inst-gen") << " -> children added lemmas" << std::endl; + return addedLemmas; + }else{ + Trace("inst-gen-debug") << "Calculate inst-gen instantiations..." << std::endl; + //get all possible values of selection formula + InstGenProcess igp( d_quant_selection_formula[f] ); + igp.calculateMatches( d_qe, f ); + Trace("inst-gen-debug") << "Add inst-gen instantiations (" << igp.getNumMatches() << ")..." << std::endl; + for( int i=0; id_true ){ + InstMatch m; + igp.getMatch( d_qe->getEqualityQuery(), i, m ); + //we only consider matches that are non-empty + // matches that are empty should trigger other instances that are non-empty + if( !m.empty() ){ + Trace("inst-gen-debug") << "Get in terms of parent..." << std::endl; + //translate to be in terms match in terms of fp + InstMatch mp; + getParentQuantifierMatch( mp, fp, m, f ); + + //if this is a partial instantion + if( !m.isComplete( f ) ){ + //if the instantiation does not yet exist + if( d_sub_quant_inst_trie[fp].addInstMatch( d_qe, fp, mp, true ) ){ + //get the partial instantiation pf + Node pf = d_qe->getInstantiation( fp, mp ); + Trace("inst-gen-pi") << "Partial instantiation of " << f << std::endl; + Trace("inst-gen-pi") << " " << pf << std::endl; + d_sub_quants[ f ].push_back( pf ); + d_sub_quant_inst[ pf ] = InstMatch( &mp ); + d_sub_quant_parent[ pf ] = fp; + mp.add( d_quant_basis_match[ fp ] ); + d_quant_basis_match[ pf ] = InstMatch( &mp ); + addedLemmas += initializeQuantifier( pf, fp ); + Trace("inst-gen-pi") << "Done adding partial instantiation" << std::endl; + } + }else{ + if( d_qe->addInstantiation( fp, mp ) ){ + addedLemmas++; + } } } } } - } - if( addedLemmas==0 ){ - //all sub quantifiers must be satisfied as well - bool subQuantSat = true; - for( size_t i=0; i added lemmas = " << addedLemmas << std::endl; - if( d_quant_sat.find( f )!=d_quant_sat.end() ){ if( fp!=f ) Trace("inst-gen") << " "; - Trace("inst-gen") << " -> *** it is satisfied" << std::endl; + Trace("inst-gen") << " -> added lemmas = " << addedLemmas << std::endl; + if( d_quant_sat.find( f )!=d_quant_sat.end() ){ + if( fp!=f ) Trace("inst-gen") << " "; + Trace("inst-gen") << " -> *** it is satisfied" << std::endl; + } } } } @@ -697,24 +716,52 @@ Node ModelEngineBuilderInstGen::getSelectionFormula( Node fn, Node n, bool polar ret = getSelectionFormula( fn[0], n[0], !polarity, useOption ); }else if( n.getKind()==OR || n.getKind()==IMPLIES || n.getKind()==AND ){ //whether we only need to find one or all - bool posPol = (( n.getKind()==OR || n.getKind()==IMPLIES ) && polarity ) || ( n.getKind()==AND && !polarity ); + bool favorPol = ( n.getKind()!=AND && polarity ) || ( n.getKind()==AND && !polarity ); std::vector< Node > children; - bool retSet = false; for( int i=0; i<(int)n.getNumChildren(); i++ ){ Node fnc = ( i==0 && fn.getKind()==IMPLIES ) ? fn[i].negate() : fn[i]; Node nc = ( i==0 && n.getKind()==IMPLIES ) ? n[i].negate() : n[i]; Node nn = getSelectionFormula( fnc, nc, polarity, useOption ); - if( nn.isNull()!=posPol ){ //TODO: may want to weaken selection formula - ret = nn; - retSet = true; + if( nn.isNull() && !favorPol ){ + //cannot make selection formula + children.clear(); break; } - if( std::find( children.begin(), children.end(), nn )==children.end() ){ - children.push_back( nn ); + if( !nn.isNull() ){ + if( favorPol ){ //temporary + return nn; // + } // + if( std::find( children.begin(), children.end(), nn )==children.end() ){ + children.push_back( nn ); + } } } - if( !retSet && !posPol ){ - ret = NodeManager::currentNM()->mkNode( AND, children ); + if( !children.empty() ){ + if( favorPol ){ + //filter which formulas we wish to keep, make disjunction + Node min_lit; + int min_score = -1; + for( size_t i=0; imkNode( AND, children ); + } + }else{ + ret = Node::null(); } }else if( n.getKind()==ITE ){ Node nn; @@ -771,6 +818,24 @@ Node ModelEngineBuilderInstGen::getSelectionFormula( Node fn, Node n, bool polar return ret; } +int ModelEngineBuilderInstGen::getSelectionFormulaScore( Node fn ){ + if( fn.getType().isBoolean() ){ + if( fn.getKind()==APPLY_UF ){ + Node op = fn.getOperator(); + //return total number of terms + return d_qe->getTermDatabase()->d_op_count[op]; + }else{ + int score = 0; + for( size_t i=0; i #include @@ -71,6 +72,30 @@ public: std::map< Node, Node > d_phase_reqs_equality_term; }; + +class EqualityQuery { +public: + EqualityQuery(){} + virtual ~EqualityQuery(){}; + /** contains term */ + virtual bool hasTerm( Node a ) = 0; + /** get the representative of the equivalence class of a */ + virtual Node getRepresentative( Node a ) = 0; + /** returns true if a and b are equal in the current context */ + virtual bool areEqual( Node a, Node b ) = 0; + /** returns true is a and b are disequal in the current context */ + virtual bool areDisequal( Node a, Node b ) = 0; + /** getInternalRepresentative gets the current best representative in the equivalence class of a, based on some criteria. + If cbqi is active, this will return a term in the equivalence class of "a" that does + not contain instantiation constants, if such a term exists. + */ + virtual Node getInternalRepresentative( Node a ) = 0; + /** get the equality engine associated with this query */ + virtual eq::EqualityEngine* getEngine() = 0; + /** get the equivalence class of a */ + virtual void getEquivalenceClass( Node a, std::vector< Node >& eqc ) = 0; +};/* class EqualityQuery */ + } } diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 3b2778061..43548f021 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -45,33 +45,6 @@ bool TermArgTrie::addTerm2( QuantifiersEngine* qe, Node n, int argIndex ){ } } -Trigger* TrTrie::getTrigger2( std::vector< Node >& nodes ){ - if( nodes.empty() ){ - return d_tr; - }else{ - Node n = nodes.back(); - nodes.pop_back(); - if( d_children.find( n )!=d_children.end() ){ - return d_children[n]->getTrigger2( nodes ); - }else{ - return NULL; - } - } -} - -void TrTrie::addTrigger2( std::vector< Node >& nodes, Trigger* t ){ - if( nodes.empty() ){ - d_tr = t; - }else{ - Node n = nodes.back(); - nodes.pop_back(); - if( d_children.find( n )==d_children.end() ){ - d_children[n] = new TrTrie; - } - d_children[n]->addTrigger2( nodes, t ); - } -} - void TermDb::addTermEfficient( Node n, std::set< Node >& added){ static AvailableInTermDb aitdi; if (inst::Trigger::isAtomicTrigger( n ) && !n.getAttribute(aitdi)){ @@ -106,14 +79,14 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){ d_op_map[op].push_back( n ); added.insert( n ); - uf::InstantiatorTheoryUf* d_ith = (uf::InstantiatorTheoryUf*)d_quantEngine->getInstantiator( THEORY_UF ); for( int i=0; i<(int)n.getNumChildren(); i++ ){ addTerm( n[i], added, withinQuant ); if( options::efficientEMatching() ){ + uf::InstantiatorTheoryUf* ith = (uf::InstantiatorTheoryUf*)d_quantEngine->getInstantiator( THEORY_UF ); if( d_parents[n[i]][op].empty() ){ //must add parent to equivalence class info - Node nir = d_ith->getRepresentative( n[i] ); - uf::EqClassInfo* eci_nir = d_ith->getEquivalenceClassInfo( nir ); + Node nir = ith->getRepresentative( n[i] ); + uf::EqClassInfo* eci_nir = ith->getEquivalenceClassInfo( nir ); if( eci_nir ){ eci_nir->d_pfuns[ op ] = true; } @@ -126,9 +99,10 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){ } if( options::eagerInstQuant() ){ if( !n.hasAttribute(InstLevelAttribute()) && n.getAttribute(InstLevelAttribute())==0 ){ + uf::InstantiatorTheoryUf* ith = (uf::InstantiatorTheoryUf*)d_quantEngine->getInstantiator( THEORY_UF ); int addedLemmas = 0; - for( int i=0; i<(int)d_ith->d_op_triggers[op].size(); i++ ){ - addedLemmas += d_ith->d_op_triggers[op][i]->addTerm( n ); + for( int i=0; i<(int)ith->d_op_triggers[op].size(); i++ ){ + addedLemmas += ith->d_op_triggers[op][i]->addTerm( n ); } //Message() << "Terms, added lemmas: " << addedLemmas << std::endl; d_quantEngine->flushLemmas( &d_quantEngine->getTheoryEngine()->theoryOf( THEORY_QUANTIFIERS )->getOutputChannel() ); @@ -157,6 +131,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){ int alreadyCongruentCount = 0; //rebuild d_func/pred_map_trie for each operation, this will calculate all congruent terms for( std::map< Node, std::vector< Node > >::iterator it = d_op_map.begin(); it != d_op_map.end(); ++it ){ + d_op_count[ it->first ] = 0; if( !it->second.empty() ){ if( it->second[0].getType().isBoolean() ){ d_pred_map_trie[ 0 ][ it->first ].d_data.clear(); @@ -174,6 +149,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){ congruentCount++; }else{ nonCongruentCount++; + d_op_count[ it->first ]++; } }else{ congruentCount++; @@ -200,6 +176,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){ congruentCount++; }else{ nonCongruentCount++; + d_op_count[ op ]++; } }else{ alreadyCongruentCount++; @@ -360,12 +337,6 @@ Node TermDb::convertNodeToPattern( Node n, Node f, const std::vector & var return n2; } -Node TermDb::mkNodeInstConstant( Kind k, std::vector< Node >& children, Node f ){ - Node n = NodeManager::currentNM()->mkNode( k, children ); - setInstantiationConstantAttr( n, f ); - return n; -} - Node TermDb::getSkolemizedBody( Node f ){ @@ -379,24 +350,10 @@ Node TermDb::getSkolemizedBody( Node f ){ } d_skolem_body[ f ] = f[ 1 ].substitute( vars.begin(), vars.end(), d_skolem_constants[ f ].begin(), d_skolem_constants[ f ].end() ); - if( f.hasAttribute(InstLevelAttribute()) ){ - setInstantiationLevelAttr( d_skolem_body[ f ], f.getAttribute(InstLevelAttribute()) ); - } } return d_skolem_body[ f ]; } - -void TermDb::setInstantiationLevelAttr( Node n, uint64_t level ){ - if( !n.hasAttribute(InstLevelAttribute()) ){ - InstLevelAttribute ila; - n.setAttribute(ila,level); - } - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - setInstantiationLevelAttr( n[i], level ); - } -} - Node TermDb::getFreeVariableForInstConstant( Node n ){ TypeNode tn = n.getType(); if( d_free_vars.find( tn )==d_free_vars.end() ){ diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index bcd6b833d..e1786d44c 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -24,6 +24,42 @@ namespace CVC4 { namespace theory { +/** Attribute true for nodes that should not be used for matching */ +struct NoMatchAttributeId {}; +/** use the special for boolean flag */ +typedef expr::Attribute< NoMatchAttributeId, + bool, + expr::attr::NullCleanupStrategy, + true // context dependent + > NoMatchAttribute; + +// attribute for "contains instantiation constants from" +struct InstConstantAttributeId {}; +typedef expr::Attribute InstConstantAttribute; + +struct InstLevelAttributeId {}; +typedef expr::Attribute InstLevelAttribute; + +struct InstVarNumAttributeId {}; +typedef expr::Attribute InstVarNumAttribute; + +// Attribute that tell if a node have been asserted in this branch +struct AvailableInTermDbId {}; +/** use the special for boolean flag */ +typedef expr::Attribute AvailableInTermDb; + +struct ModelBasisAttributeId {}; +typedef expr::Attribute ModelBasisAttribute; +//for APPLY_UF terms, 1 : term has direct child with model basis attribute, +// 0 : term has no direct child with model basis attribute. +struct ModelBasisArgAttributeId {}; +typedef expr::Attribute ModelBasisArgAttribute; + + class QuantifiersEngine; namespace inst{ @@ -43,45 +79,21 @@ public: };/* class TermArgTrie */ -/** a trie of triggers */ -class TrTrie { -private: - inst::Trigger* getTrigger2( std::vector< Node >& nodes ); - void addTrigger2( std::vector< Node >& nodes, inst::Trigger* t ); -public: - TrTrie() : d_tr( NULL ){} - inst::Trigger* d_tr; - std::map< TNode, TrTrie* > d_children; - inst::Trigger* getTrigger( std::vector< Node >& nodes ){ - std::vector< Node > temp; - temp.insert( temp.begin(), nodes.begin(), nodes.end() ); - std::sort( temp.begin(), temp.end() ); - return getTrigger2( temp ); - } - void addTrigger( std::vector< Node >& nodes, inst::Trigger* t ){ - std::vector< Node > temp; - temp.insert( temp.begin(), nodes.begin(), nodes.end() ); - std::sort( temp.begin(), temp.end() ); - return addTrigger2( temp, t ); - } -};/* class inst::Trigger::TrTrie */ - - class TermDb { friend class ::CVC4::theory::QuantifiersEngine; friend class ::CVC4::theory::inst::Trigger; private: /** reference to the quantifiers engine */ QuantifiersEngine* d_quantEngine; - /** calculated no match terms */ - bool d_matching_active; /** terms processed */ std::hash_set< Node, NodeHashFunction > d_processed; public: - TermDb( QuantifiersEngine* qe ) : d_quantEngine( qe ), d_matching_active( true ){} + TermDb( QuantifiersEngine* qe ) : d_quantEngine( qe ){} ~TermDb(){} /** map from APPLY_UF operators to ground terms for that operator */ std::map< Node, std::vector< Node > > d_op_map; + /** count number of APPLY_UF terms per operator */ + std::map< Node, int > d_op_count; /** map from APPLY_UF functions to trie */ std::map< Node, TermArgTrie > d_func_map_trie; /** map from APPLY_UF predicates to trie */ @@ -92,10 +104,6 @@ public: void addTerm( Node n, std::set< Node >& added, bool withinQuant = false ); /** reset (calculate which terms are active) */ void reset( Theory::Effort effort ); - /** set active */ - void setMatchingActive( bool a ) { d_matching_active = a; } - /** get active */ - bool getMatchingActive() { return d_matching_active; } private: /** for efficient e-matching */ void addTermEfficient( Node n, std::set< Node >& added); @@ -168,10 +176,6 @@ public: Node convertNodeToPattern( Node n, Node f, const std::vector & vars, const std::vector & nvars); - /** get iff term */ - Node getInstConstantIffTerm( Node n, bool pol ); - /** make node, validating the inst constant attribute */ - Node mkNodeInstConstant( Kind k, std::vector< Node >& children, Node f ); /** set instantiation constant attr */ void setInstantiationConstantAttr( Node n, Node f ); @@ -194,8 +198,6 @@ private: public: /** get free variable for instantiation constant */ Node getFreeVariableForInstConstant( Node n ); - /** set instantiation level attr */ - void setInstantiationLevelAttr( Node n, uint64_t level ); //for triggers private: @@ -212,14 +214,6 @@ public: void getVarContains( Node f, std::vector< Node >& pats, std::map< Node, std::vector< Node > >& varContains ); /** get var contains for node n */ void getVarContainsNode( Node f, Node n, std::vector< Node >& varContains ); -private: - /** all triggers will be stored in this trie */ - TrTrie d_tr_trie; -public: - /** get trigger */ - inst::Trigger* getTrigger( std::vector< Node >& nodes ){ return d_tr_trie.getTrigger( nodes ); } - /** add trigger */ - void addTrigger( std::vector< Node >& nodes, inst::Trigger* t ){ d_tr_trie.addTrigger( nodes, t ); } };/* class TermDb */ }/* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index 90a673715..c64a75ec4 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -20,6 +20,7 @@ #include "theory/uf/equality_engine.h" #include "theory/quantifiers/options.h" #include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/inst_match_generator.h" using namespace std; using namespace CVC4; @@ -97,6 +98,10 @@ int Trigger::addTerm( Node t ){ return d_mg->addTerm( d_f, t, d_quantEngine ); } +//bool Trigger::nonunifiable( TNode t, const std::vector & vars){ +// return d_mg->nonunifiable(t,vars); +//} + int Trigger::addInstantiations( InstMatch& baseMatch ){ int addedLemmas = d_mg->addInstantiations( d_f, baseMatch, d_quantEngine ); if( addedLemmas>0 ){ @@ -183,7 +188,7 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& // Notice() << "Trigger new old = " << trNew << " " << trOld << std::endl; //} }else{ - Trigger* t = qe->getTermDatabase()->getTrigger( trNodes ); + Trigger* t = qe->getTriggerDatabase()->getTrigger( trNodes ); if( t ){ if( trOption==TR_GET_OLD ){ //just return old trigger @@ -194,7 +199,7 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& } } Trigger* t = new Trigger( qe, f, trNodes, matchOption, smartTriggers ); - qe->getTermDatabase()->addTrigger( trNodes, t ); + qe->getTriggerDatabase()->addTrigger( trNodes, t ); return t; } Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, Node n, int matchOption, bool keepAll, int trOption, bool smartTriggers ){ @@ -470,3 +475,30 @@ bool Trigger::getPatternArithmetic( Node f, Node n, std::map< Node, Node >& coef } return false; } + +Trigger* TriggerTrie::getTrigger2( std::vector< Node >& nodes ){ + if( nodes.empty() ){ + return d_tr; + }else{ + Node n = nodes.back(); + nodes.pop_back(); + if( d_children.find( n )!=d_children.end() ){ + return d_children[n]->getTrigger2( nodes ); + }else{ + return NULL; + } + } +} + +void TriggerTrie::addTrigger2( std::vector< Node >& nodes, Trigger* t ){ + if( nodes.empty() ){ + d_tr = t; + }else{ + Node n = nodes.back(); + nodes.pop_back(); + if( d_children.find( n )==d_children.end() ){ + d_children[n] = new TriggerTrie; + } + d_children[n]->addTrigger2( nodes, t ); + } +} diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h index 945b5db2a..267debb02 100644 --- a/src/theory/quantifiers/trigger.h +++ b/src/theory/quantifiers/trigger.h @@ -18,11 +18,19 @@ #define __CVC4__THEORY__QUANTIFIERS__TRIGGER_H #include "theory/quantifiers/inst_match.h" +#include "expr/node.h" +#include "util/hash.h" +#include namespace CVC4 { namespace theory { + +class QuantifiersEngine; + namespace inst { +class IMGenerator; + //a collect of nodes representing a trigger class Trigger { private: @@ -56,11 +64,6 @@ public: bool getMatch( Node t, InstMatch& m); /** add ground term t, called when t is added to the TermDb */ int addTerm( Node t ); - /** return true if whatever Node is subsituted for the variables the - given Node can't match the pattern */ - bool nonunifiable( TNode t, const std::vector & vars){ - return d_mg->nonunifiable(t,vars); - } /** return whether this is a multi-trigger */ bool isMultiTrigger() { return d_nodes.size()>1; } public: @@ -127,6 +130,30 @@ inline std::ostream& operator<<(std::ostream& out, const Trigger & tr) { return out; } + +/** a trie of triggers */ +class TriggerTrie { +private: + inst::Trigger* getTrigger2( std::vector< Node >& nodes ); + void addTrigger2( std::vector< Node >& nodes, inst::Trigger* t ); +public: + TriggerTrie() : d_tr( NULL ){} + inst::Trigger* d_tr; + std::map< TNode, TriggerTrie* > d_children; + inst::Trigger* getTrigger( std::vector< Node >& nodes ){ + std::vector< Node > temp; + temp.insert( temp.begin(), nodes.begin(), nodes.end() ); + std::sort( temp.begin(), temp.end() ); + return getTrigger2( temp ); + } + void addTrigger( std::vector< Node >& nodes, inst::Trigger* t ){ + std::vector< Node > temp; + temp.insert( temp.begin(), nodes.begin(), nodes.end() ); + std::sort( temp.begin(), temp.end() ); + return addTrigger2( temp, t ); + } +};/* class inst::Trigger::Trigger */ + }/* CVC4::theory::inst namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 4e933a511..a44a3ff1f 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -25,7 +25,6 @@ #include "theory/quantifiers/instantiation_engine.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/term_database.h" -#include "theory/rewriterules/rr_candidate_generator.h" using namespace std; using namespace CVC4; @@ -39,6 +38,7 @@ d_te( te ), d_quant_rel( false ){ //currently do not care about relevance d_eq_query = new EqualityQueryQuantifiersEngine( this ); d_term_db = new quantifiers::TermDb( this ); + d_tr_trie = new inst::TriggerTrie; d_hasAddedLemma = false; //the model object @@ -124,18 +124,6 @@ void QuantifiersEngine::check( Theory::Effort e ){ } } -std::vector QuantifiersEngine::createInstVariable( std::vector & vars ){ - std::vector inst_constant; - inst_constant.reserve(vars.size()); - for( std::vector::const_iterator v = vars.begin(); - v != vars.end(); ++v ){ - //make instantiation constants - Node ic = NodeManager::currentNM()->mkInstConstant( (*v).getType() ); - inst_constant.push_back( ic ); - }; - return inst_constant; -} - void QuantifiersEngine::registerQuantifier( Node f ){ if( std::find( d_quants.begin(), d_quants.end(), f )==d_quants.end() ){ d_quants.push_back( f ); @@ -227,6 +215,61 @@ void QuantifiersEngine::computeTermVector( Node f, InstMatch& m, std::vector< No } } +bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms ){ + Assert( f.getKind()==FORALL ); + Assert( !f.hasAttribute(InstConstantAttribute()) ); + Assert( vars.size()==terms.size() ); + Node body = getInstantiation( f, vars, terms ); + //make the lemma + NodeBuilder<> nb(kind::OR); + nb << f.notNode() << body; + Node lem = nb; + //check for duplication + if( addLemma( lem ) ){ + Trace("inst") << "*** Instantiate " << f << " with " << std::endl; + uint64_t maxInstLevel = 0; + for( int i=0; i<(int)terms.size(); i++ ){ + if( terms[i].hasAttribute(InstConstantAttribute()) ){ + Debug("inst")<< "***& Bad Instantiate " << f << " with " << std::endl; + for( int i=0; i<(int)terms.size(); i++ ){ + Debug("inst") << " " << terms[i] << std::endl; + } + Unreachable("Bad instantiation"); + }else{ + Trace("inst") << " " << terms[i]; + //Debug("inst-engine") << " " << terms[i].getAttribute(InstLevelAttribute()); + Trace("inst") << std::endl; + if( terms[i].hasAttribute(InstLevelAttribute()) ){ + if( terms[i].getAttribute(InstLevelAttribute())>maxInstLevel ){ + maxInstLevel = terms[i].getAttribute(InstLevelAttribute()); + } + }else{ + setInstantiationLevelAttr( terms[i], 0 ); + } + } + } + Trace("inst-debug") << "*** Lemma is " << lem << std::endl; + setInstantiationLevelAttr( body, maxInstLevel+1 ); + ++(d_statistics.d_instantiations); + d_statistics.d_total_inst_var += (int)terms.size(); + d_statistics.d_max_instantiation_level.maxAssign( maxInstLevel+1 ); + return true; + }else{ + ++(d_statistics.d_inst_duplicate); + return false; + } +} + +void QuantifiersEngine::setInstantiationLevelAttr( Node n, uint64_t level ){ + if( !n.hasAttribute(InstLevelAttribute()) ){ + InstLevelAttribute ila; + n.setAttribute(ila,level); + } + for( int i=0; i<(int)n.getNumChildren(); i++ ){ + setInstantiationLevelAttr( n[i], level ); + } +} + Node QuantifiersEngine::getInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms ){ Node body = f[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() ); //process partial instantiation if necessary @@ -272,51 +315,6 @@ bool QuantifiersEngine::addLemma( Node lem ){ } } -bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms ){ - Assert( f.getKind()==FORALL ); - Assert( !f.hasAttribute(InstConstantAttribute()) ); - Assert( vars.size()==terms.size() ); - Node body = getInstantiation( f, vars, terms ); - //make the lemma - NodeBuilder<> nb(kind::OR); - nb << f.notNode() << body; - Node lem = nb; - //check for duplication - if( addLemma( lem ) ){ - Trace("inst") << "*** Instantiate " << f << " with " << std::endl; - uint64_t maxInstLevel = 0; - for( int i=0; i<(int)terms.size(); i++ ){ - if( terms[i].hasAttribute(InstConstantAttribute()) ){ - Debug("inst")<< "***& Bad Instantiate " << f << " with " << std::endl; - for( int i=0; i<(int)terms.size(); i++ ){ - Debug("inst") << " " << terms[i] << std::endl; - } - Unreachable("Bad instantiation"); - }else{ - Trace("inst") << " " << terms[i]; - //Debug("inst-engine") << " " << terms[i].getAttribute(InstLevelAttribute()); - Trace("inst") << std::endl; - if( terms[i].hasAttribute(InstLevelAttribute()) ){ - if( terms[i].getAttribute(InstLevelAttribute())>maxInstLevel ){ - maxInstLevel = terms[i].getAttribute(InstLevelAttribute()); - } - }else{ - d_term_db->setInstantiationLevelAttr( terms[i], 0 ); - } - } - } - Trace("inst-debug") << "*** Lemma is " << lem << std::endl; - d_term_db->setInstantiationLevelAttr( body, maxInstLevel+1 ); - ++(d_statistics.d_instantiations); - d_statistics.d_total_inst_var += (int)terms.size(); - d_statistics.d_max_instantiation_level.maxAssign( maxInstLevel+1 ); - return true; - }else{ - ++(d_statistics.d_inst_duplicate); - return false; - } -} - bool QuantifiersEngine::addInstantiation( Node f, InstMatch& m, bool modEq, bool modInst, bool mkRep ){ //make sure there are values for each variable we are instantiating m.makeComplete( f, this ); @@ -395,10 +393,8 @@ void QuantifiersEngine::getPhaseReqTerms( Node f, std::vector< Node >& nodes ){ bool nodeChanged = false; if( d_phase_reqs[f]->isPhaseReq( nodes[i] ) ){ bool preq = d_phase_reqs[f]->getPhaseReq( nodes[i] ); - std::vector< Node > children; - children.push_back( nodes[i] ); - children.push_back( NodeManager::currentNM()->mkConst(preq) ); - nodes[i] = d_term_db->mkNodeInstConstant( IFF, children, f ); + nodes[i] = NodeManager::currentNM()->mkNode( IFF, nodes[i], NodeManager::currentNM()->mkConst(preq) ); + d_term_db->setInstantiationConstantAttr( nodes[i], f ); nodeChanged = true; } //else if( qe->isPhaseReqEquality( f, trNodes[i] ) ){ @@ -416,6 +412,56 @@ void QuantifiersEngine::getPhaseReqTerms( Node f, std::vector< Node >& nodes ){ d_statistics.d_lit_phase_nreq += (int)nodes.size(); } } +/* +EqualityQuery* QuantifiersEngine::getEqualityQuery(TypeNode t) { + // Should use skeleton (in order to have the type and the kind + // or any needed other information) instead of only the type + + // TheoryId id = Theory::theoryOf(t); + // inst::EqualityQuery* eq = d_eq_query_arr[id]; + // if(eq == NULL) return d_eq_query_arr[theory::THEORY_UF]; + // else return eq; + + // hack because the generic one is too slow + // TheoryId id = Theory::theoryOf(t); + // if( true || id == theory::THEORY_UF){ + // uf::InstantiatorTheoryUf* ith = static_cast( getInstantiator( theory::THEORY_UF )); + // return new uf::EqualityQueryInstantiatorTheoryUf(ith); + // } + // inst::EqualityQuery* eq = d_eq_query_arr[id]; + // if(eq == NULL) return d_eq_query_arr[theory::THEORY_UF]; + // else return eq; + + + //Currently we use the generic EqualityQuery + return getEqualityQuery(); +} + + +rrinst::CandidateGenerator* QuantifiersEngine::getRRCanGenClasses() { + return new GenericCandidateGeneratorClasses(this); +} + +rrinst::CandidateGenerator* QuantifiersEngine::getRRCanGenClass() { + return new GenericCandidateGeneratorClass(this); +} + +rrinst::CandidateGenerator* QuantifiersEngine::getRRCanGenClasses(TypeNode t) { + // TheoryId id = Theory::theoryOf(t); + // rrinst::CandidateGenerator* eq = getInstantiator(id)->getRRCanGenClasses(); + // if(eq == NULL) return getInstantiator(id)->getRRCanGenClasses(); + // else return eq; + return getRRCanGenClasses(); +} + +rrinst::CandidateGenerator* QuantifiersEngine::getRRCanGenClass(TypeNode t) { + // TheoryId id = Theory::theoryOf(t); + // rrinst::CandidateGenerator* eq = getInstantiator(id)->getRRCanGenClass(); + // if(eq == NULL) return getInstantiator(id)->getRRCanGenClass(); + // else return eq; + return getRRCanGenClass(); +} +*/ QuantifiersEngine::Statistics::Statistics(): d_num_quant("QuantifiersEngine::Num_Quantifiers", 0), @@ -602,52 +648,3 @@ void EqualityQueryQuantifiersEngine::getEquivalenceClass( Node a, std::vector< N eqc.push_back( a ); } } - -inst::EqualityQuery* QuantifiersEngine::getEqualityQuery(TypeNode t) { - /** Should use skeleton (in order to have the type and the kind - or any needed other information) instead of only the type */ - - // TheoryId id = Theory::theoryOf(t); - // inst::EqualityQuery* eq = d_eq_query_arr[id]; - // if(eq == NULL) return d_eq_query_arr[theory::THEORY_UF]; - // else return eq; - - /** hack because the generic one is too slow */ - // TheoryId id = Theory::theoryOf(t); - // if( true || id == theory::THEORY_UF){ - // uf::InstantiatorTheoryUf* ith = static_cast( getInstantiator( theory::THEORY_UF )); - // return new uf::EqualityQueryInstantiatorTheoryUf(ith); - // } - // inst::EqualityQuery* eq = d_eq_query_arr[id]; - // if(eq == NULL) return d_eq_query_arr[theory::THEORY_UF]; - // else return eq; - - - //Currently we use the generic EqualityQuery - return getEqualityQuery(); -} - - -rrinst::CandidateGenerator* QuantifiersEngine::getRRCanGenClasses() { - return new GenericCandidateGeneratorClasses(this); -} - -rrinst::CandidateGenerator* QuantifiersEngine::getRRCanGenClass() { - return new GenericCandidateGeneratorClass(this); -} - -rrinst::CandidateGenerator* QuantifiersEngine::getRRCanGenClasses(TypeNode t) { - // TheoryId id = Theory::theoryOf(t); - // rrinst::CandidateGenerator* eq = getInstantiator(id)->getRRCanGenClasses(); - // if(eq == NULL) return getInstantiator(id)->getRRCanGenClasses(); - // else return eq; - return getRRCanGenClasses(); -} - -rrinst::CandidateGenerator* QuantifiersEngine::getRRCanGenClass(TypeNode t) { - // TheoryId id = Theory::theoryOf(t); - // rrinst::CandidateGenerator* eq = getInstantiator(id)->getRRCanGenClass(); - // if(eq == NULL) return getInstantiator(id)->getRRCanGenClass(); - // else return eq; - return getRRCanGenClass(); -} diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index be8830710..18635a823 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -62,6 +62,9 @@ namespace quantifiers { class FirstOrderModel; }/* CVC4::theory::quantifiers */ +namespace inst { + class TriggerTrie; +}/* CVC4::theory::inst */ class QuantifiersEngine { friend class quantifiers::InstantiationEngine; @@ -84,20 +87,20 @@ private: /** phase requirements for each quantifier for each instantiation literal */ std::map< Node, QuantPhaseReq* > d_phase_reqs; private: - /** list of all quantifiers (pre-rewrite) */ + /** list of all quantifiers seen */ std::vector< Node > d_quants; - /** lemmas produced */ + /** list of all lemmas produced */ std::map< Node, bool > d_lemmas_produced; /** lemmas waiting */ std::vector< Node > d_lemmas_waiting; /** has added lemma this round */ bool d_hasAddedLemma; - /** inst matches produced for each quantifier */ + /** list of all instantiations produced for each quantifier */ std::map< Node, inst::InstMatchTrie > d_inst_match_trie; - /** owner of quantifiers */ - std::map< Node, Theory* > d_owner; /** term database */ quantifiers::TermDb* d_term_db; + /** all triggers will be stored in this trie */ + inst::TriggerTrie* d_tr_trie; /** extended model object */ quantifiers::FirstOrderModel* d_model; private: @@ -111,15 +114,7 @@ public: TheoryEngine* getTheoryEngine() { return d_te; } /** get equality query object for the given type. The default is the generic one */ - inst::EqualityQuery* getEqualityQuery(TypeNode t); - inst::EqualityQuery* getEqualityQuery() { return d_eq_query; } - /** get equality query object for the given type. The default is the - one of UF */ - rrinst::CandidateGenerator* getRRCanGenClasses(TypeNode t); - rrinst::CandidateGenerator* getRRCanGenClass(TypeNode t); - /* generic candidate generator */ - rrinst::CandidateGenerator* getRRCanGenClasses(); - rrinst::CandidateGenerator* getRRCanGenClass(); + EqualityQuery* getEqualityQuery() { return d_eq_query; } /** get instantiation engine */ quantifiers::InstantiationEngine* getInstantiationEngine() { return d_inst_engine; } /** get model engine */ @@ -151,14 +146,13 @@ public: Node getNextDecisionRequest(); /** reset instantiation round */ void resetInstantiationRound( Theory::Effort level ); - - //create inst variable - std::vector createInstVariable( std::vector & vars ); private: /** compute term vector */ void computeTermVector( Node f, InstMatch& m, std::vector< Node >& vars, std::vector< Node >& terms ); /** instantiate f with arguments terms */ bool addInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms ); + /** set instantiation level attr */ + void setInstantiationLevelAttr( Node n, uint64_t level ); public: /** get instantiation */ Node getInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms ); @@ -190,6 +184,8 @@ public: quantifiers::FirstOrderModel* getModel() { return d_model; } /** get term database */ quantifiers::TermDb* getTermDatabase() { return d_term_db; } + /** get trigger database */ + inst::TriggerTrie* getTriggerDatabase() { return d_tr_trie; } /** add term to database */ void addTermToDatabase( Node n, bool withinQuant = false ); public: diff --git a/src/theory/rewriterules/rr_inst_match.cpp b/src/theory/rewriterules/rr_inst_match.cpp index 572ccfad2..af4cdeb50 100644 --- a/src/theory/rewriterules/rr_inst_match.cpp +++ b/src/theory/rewriterules/rr_inst_match.cpp @@ -23,6 +23,7 @@ #include "theory/rewriterules/rr_trigger.h" #include "theory/rewriterules/rr_inst_match_impl.h" #include "theory/rewriterules/rr_candidate_generator.h" +#include "theory/quantifiers/candidate_generator.h" using namespace CVC4; using namespace CVC4::kind; @@ -140,7 +141,8 @@ ApplyMatcher::ApplyMatcher( Node pat, QuantifiersEngine* qe): d_pattern(pat){ //set-up d_variables, d_constants, d_childrens for( size_t i=0; i< d_pattern.getNumChildren(); ++i ){ - EqualityQuery* q = qe->getEqualityQuery(d_pattern[i].getType()); + //EqualityQuery* q = qe->getEqualityQuery(d_pattern[i].getType()); + EqualityQuery* q = qe->getEqualityQuery(); Assert( q != NULL ); if( d_pattern[i].hasAttribute(InstConstantAttribute()) ){ if( d_pattern[i].getKind()==INST_CONSTANT ){ @@ -327,7 +329,8 @@ class VarMatcher: public Matcher{ EqualityQuery* d_q; public: VarMatcher(Node var, QuantifiersEngine* qe): d_var(var), d_binded(false){ - d_q = qe->getEqualityQuery(var.getType()); + //d_q = qe->getEqualityQuery(var.getType()); + d_q = qe->getEqualityQuery(); } void resetInstantiationRound( QuantifiersEngine* qe ){}; bool reset( TNode n, InstMatch& m, QuantifiersEngine* qe ){ @@ -600,9 +603,9 @@ private: public: void mkCandidateGenerator(){ if(classes) - d_cg = d_qe->getRRCanGenClasses(); + d_cg = new GenericCandidateGeneratorClasses(d_qe); else - d_cg = d_qe->getRRCanGenClass(); + d_cg = new GenericCandidateGeneratorClass(d_qe); } GenericCandidateGeneratorClasses(QuantifiersEngine* qe): diff --git a/src/theory/rewriterules/rr_inst_match.h b/src/theory/rewriterules/rr_inst_match.h index 14873b501..63728a95b 100644 --- a/src/theory/rewriterules/rr_inst_match.h +++ b/src/theory/rewriterules/rr_inst_match.h @@ -30,6 +30,7 @@ #include "context/cdlist.h" #include "theory/quantifiers/inst_match.h" +#include "theory/quantifiers/term_database.h" #include "expr/node_manager.h" #include "expr/node_builder.h" @@ -55,7 +56,7 @@ public: Node cand = cg->getNextCandidate(); //....... }while( !cand.isNull() ); - + eqc is the equivalence class you are searching in */ virtual void reset( TNode eqc ) = 0; diff --git a/src/theory/rewriterules/rr_inst_match_impl.h b/src/theory/rewriterules/rr_inst_match_impl.h index 43161a9e5..388d1a702 100644 --- a/src/theory/rewriterules/rr_inst_match_impl.h +++ b/src/theory/rewriterules/rr_inst_match_impl.h @@ -31,7 +31,7 @@ template InstMatchTrie2Gen::InstMatchTrie2Gen(context::Context* c, QuantifiersEngine* qe): d_context(c), d_mods(c) { d_eQ = qe->getEqualityQuery(); - d_cG = qe->getRRCanGenClass(); + d_cG = new GenericCandidateGeneratorClass(qe); }; /** add match m for quantifier f starting at index, take into account equalities q, return true if successful */ diff --git a/src/theory/rewriterules/theory_rewriterules.h b/src/theory/rewriterules/theory_rewriterules.h index 5e06bfd0b..4a27b4559 100644 --- a/src/theory/rewriterules/theory_rewriterules.h +++ b/src/theory/rewriterules/theory_rewriterules.h @@ -263,6 +263,9 @@ private: rewriter::Subst & pvars, rewriter::Subst & vars); + //create inst variable + std::vector createInstVariable( std::vector & vars ); + /** statistics class */ class Statistics { public: diff --git a/src/theory/rewriterules/theory_rewriterules_rules.cpp b/src/theory/rewriterules/theory_rewriterules_rules.cpp index cc01a01ff..20e5fa084 100644 --- a/src/theory/rewriterules/theory_rewriterules_rules.cpp +++ b/src/theory/rewriterules/theory_rewriterules_rules.cpp @@ -151,8 +151,7 @@ void TheoryRewriteRules::addRewriteRule(const Node r) vars.push_back(*v); }; /* Instantiation version */ - std::vector inst_constants = - getQuantifiersEngine()->createInstVariable(vars); + std::vector inst_constants = createInstVariable(vars); /* Body/Remove_term/Guards/Triggers */ Node body = r[2][1]; TNode new_terms = r[2][1]; @@ -377,6 +376,18 @@ bool TheoryRewriteRules::addRewritePattern(TNode pattern, TNode body, } +std::vector TheoryRewriteRules::createInstVariable( std::vector & vars ){ + std::vector inst_constant; + inst_constant.reserve(vars.size()); + for( std::vector::const_iterator v = vars.begin(); + v != vars.end(); ++v ){ + //make instantiation constants + Node ic = NodeManager::currentNM()->mkInstConstant( (*v).getType() ); + inst_constant.push_back( ic ); + }; + return inst_constant; +} + }/* CVC4::theory::rewriterules namespace */ }/* CVC4::theory namespace */ diff --git a/src/theory/uf/theory_uf_instantiator.cpp b/src/theory/uf/theory_uf_instantiator.cpp index 24da83786..eceb4715b 100644 --- a/src/theory/uf/theory_uf_instantiator.cpp +++ b/src/theory/uf/theory_uf_instantiator.cpp @@ -20,6 +20,7 @@ #include "theory/quantifiers/options.h" #include "theory/rewriterules/options.h" #include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/candidate_generator.h" using namespace std; using namespace CVC4; @@ -771,7 +772,7 @@ void InstantiatorTheoryUf::registerEfficientHandler( EfficientHandler& handler, //take all terms from the uf term db and add to candidate generator if( pats[0].getKind() == kind::INST_CONSTANT ){ TypeNode ty = pats[0].getType(); - rrinst::CandidateGenerator* cg = d_quantEngine->getRRCanGenClasses(ty); + rrinst::CandidateGenerator* cg = new GenericCandidateGeneratorClasses(d_quantEngine); cg->reset(Node::null()); TNode c; SetNode ele; diff --git a/src/theory/uf/theory_uf_instantiator.h b/src/theory/uf/theory_uf_instantiator.h index 13a35d8a3..501ef9a6d 100644 --- a/src/theory/uf/theory_uf_instantiator.h +++ b/src/theory/uf/theory_uf_instantiator.h @@ -26,6 +26,7 @@ #include "util/statistics_registry.h" #include "theory/uf/theory_uf.h" #include "theory/quantifiers/trigger.h" +#include "theory/quantifiers/inst_match_generator.h" #include "util/ntuple.h" #include "context/cdqueue.h"