diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-05-02 09:16:30 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-05-02 09:16:36 -0500 |
commit | f65b945119341ae8afa69bd0b7dc005c9fcc768b (patch) | |
tree | c264125578d3b8edd752740701789f7b1e4e26bb /src/theory/quantifiers | |
parent | 53c301aa808218abe725014e01bddc19fe11a116 (diff) |
Clean up issues related to compiled scc in LFSC. Refactor --partial-trigger, do not combine quantifier prefixes with annotations. Eliminate use of context-dependent attributes in quantifiers.
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/ambqi_builder.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/candidate_generator.cpp | 10 | ||||
-rw-r--r-- | src/theory/quantifiers/candidate_generator.h | 16 | ||||
-rw-r--r-- | src/theory/quantifiers/conjecture_generator.cpp | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/full_model_check.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/inst_match_generator.cpp | 8 | ||||
-rw-r--r-- | src/theory/quantifiers/inst_match_generator.h | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/inst_strategy_e_matching.cpp | 100 | ||||
-rw-r--r-- | src/theory/quantifiers/inst_strategy_e_matching.h | 5 | ||||
-rw-r--r-- | src/theory/quantifiers/model_builder.cpp | 17 | ||||
-rw-r--r-- | src/theory/quantifiers/model_builder.h | 11 | ||||
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.cpp | 24 | ||||
-rw-r--r-- | src/theory/quantifiers/relevant_domain.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/rewrite_engine.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 47 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.h | 16 | ||||
-rw-r--r-- | src/theory/quantifiers/trigger.cpp | 147 | ||||
-rw-r--r-- | src/theory/quantifiers/trigger.h | 18 |
18 files changed, 225 insertions, 208 deletions
diff --git a/src/theory/quantifiers/ambqi_builder.cpp b/src/theory/quantifiers/ambqi_builder.cpp index 5192da7de..97116dee4 100644 --- a/src/theory/quantifiers/ambqi_builder.cpp +++ b/src/theory/quantifiers/ambqi_builder.cpp @@ -787,7 +787,7 @@ void AbsMbqiBuilder::processBuildModel(TheoryModel* m, bool fullModel) { Trace("ambqi-model-debug") << "Initial terms: " << std::endl; for( size_t i=0; i<fm->d_uf_terms[f].size(); i++ ){ Node n = fm->d_uf_terms[f][i]; - if( !n.getAttribute(NoMatchAttribute()) ){ + if( d_qe->getTermDatabase()->isTermActive( n ) ){ Trace("ambqi-model-debug") << " " << n << " -> " << fm->getRepresentativeId( n ) << std::endl; fapps.push_back( n ); } diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp index 43f5ee2fd..a0d9bda0f 100644 --- a/src/theory/quantifiers/candidate_generator.cpp +++ b/src/theory/quantifiers/candidate_generator.cpp @@ -28,7 +28,7 @@ using namespace CVC4::theory; using namespace CVC4::theory::inst; bool CandidateGenerator::isLegalCandidate( Node n ){ - return ( !n.getAttribute(NoMatchAttribute()) && ( !options::cbqi() || !quantifiers::TermDb::hasInstConstAttr(n) ) ); + return d_qe->getTermDatabase()->isTermActive( n ) && ( !options::cbqi() || !quantifiers::TermDb::hasInstConstAttr(n) ); } void CandidateGeneratorQueue::addCandidate( Node n ) { @@ -59,7 +59,7 @@ Node CandidateGeneratorQueue::getNextCandidate(){ } CandidateGeneratorQE::CandidateGeneratorQE( QuantifiersEngine* qe, Node pat ) : - d_qe( qe ), d_term_iter( -1 ){ +CandidateGenerator( qe ), d_term_iter( -1 ){ d_op = qe->getTermDatabase()->getMatchOperator( pat ); Assert( !d_op.isNull() ); d_op_arity = pat.getNumChildren(); @@ -186,7 +186,7 @@ Node CandidateGeneratorQE::getNextCandidate(){ } CandidateGeneratorQELitEq::CandidateGeneratorQELitEq( QuantifiersEngine* qe, Node mpat ) : - d_match_pattern( mpat ), d_qe( qe ){ + CandidateGenerator( qe ), d_match_pattern( mpat ){ Assert( mpat.getKind()==EQUAL ); for( unsigned i=0; i<2; i++ ){ if( !quantifiers::TermDb::hasInstConstAttr(mpat[i]) ){ @@ -225,7 +225,7 @@ Node CandidateGeneratorQELitEq::getNextCandidate(){ CandidateGeneratorQELitDeq::CandidateGeneratorQELitDeq( QuantifiersEngine* qe, Node mpat ) : - d_match_pattern( mpat ), d_qe( qe ){ +CandidateGenerator( qe ), d_match_pattern( mpat ){ Assert( d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==IFF ); d_match_pattern_type = d_match_pattern[0].getType(); @@ -259,7 +259,7 @@ Node CandidateGeneratorQELitDeq::getNextCandidate(){ CandidateGeneratorQEAll::CandidateGeneratorQEAll( QuantifiersEngine* qe, Node mpat ) : - d_match_pattern( mpat ), d_qe( qe ){ + CandidateGenerator( qe ), d_match_pattern( mpat ){ d_match_pattern_type = mpat.getType(); Assert( mpat.getKind()==INST_CONSTANT ); d_f = quantifiers::TermDb::getInstConstAttr( mpat ); diff --git a/src/theory/quantifiers/candidate_generator.h b/src/theory/quantifiers/candidate_generator.h index 18ef6a086..4fc6969fc 100644 --- a/src/theory/quantifiers/candidate_generator.h +++ b/src/theory/quantifiers/candidate_generator.h @@ -33,8 +33,10 @@ namespace inst { /** base class for generating candidates for matching */ class CandidateGenerator { +protected: + QuantifiersEngine* d_qe; public: - CandidateGenerator(){} + CandidateGenerator( QuantifiersEngine* qe ) : d_qe( qe ){} virtual ~CandidateGenerator(){} /** Get candidates functions. These set up a context to get all match candidates. @@ -54,7 +56,7 @@ public: virtual void resetInstantiationRound() = 0; public: /** legal candidate */ - static bool isLegalCandidate( Node n ); + bool isLegalCandidate( Node n ); };/* class CandidateGenerator */ /** candidate generator queue (for manual candidate generation) */ @@ -63,7 +65,7 @@ private: std::vector< Node > d_candidates; int d_candidate_index; public: - CandidateGeneratorQueue() : d_candidate_index( 0 ){} + CandidateGeneratorQueue( QuantifiersEngine* qe ) : CandidateGenerator( qe ), d_candidate_index( 0 ){} ~CandidateGeneratorQueue() throw() {} void addCandidate( Node n ); @@ -80,8 +82,6 @@ class CandidateGeneratorQE : public CandidateGenerator private: //operator you are looking for Node d_op; - //instantiator pointer - QuantifiersEngine* d_qe; //the equality class iterator unsigned d_op_arity; std::vector< quantifiers::TermArgTrie* > d_tindex; @@ -122,8 +122,6 @@ private: Node d_match_pattern; Node d_match_gterm; bool d_do_mgt; - //einstantiator pointer - QuantifiersEngine* d_qe; public: CandidateGeneratorQELitEq( QuantifiersEngine* qe, Node mpat ); ~CandidateGeneratorQELitEq() throw() {} @@ -142,8 +140,6 @@ private: Node d_match_pattern; //type of disequality TypeNode d_match_pattern_type; - //einstantiator pointer - QuantifiersEngine* d_qe; public: CandidateGeneratorQELitDeq( QuantifiersEngine* qe, Node mpat ); ~CandidateGeneratorQELitDeq() throw() {} @@ -161,8 +157,6 @@ private: //equality you are trying to match equalities for Node d_match_pattern; TypeNode d_match_pattern_type; - //einstantiator pointer - QuantifiersEngine* d_qe; // quantifier/index for the variable we are matching Node d_f; unsigned d_index; diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index 2cc49ef5a..fa71f0132 100644 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -285,7 +285,7 @@ Node ConjectureGenerator::getFreeVar( TypeNode tn, unsigned i ) { } bool ConjectureGenerator::isHandledTerm( TNode n ){ - return !n.getAttribute(NoMatchAttribute()) && inst::Trigger::isAtomicTrigger( n ) && ( n.getKind()!=APPLY_UF || n.getOperator().getKind()!=SKOLEM ); + return d_quantEngine->getTermDatabase()->isTermActive( n ) && inst::Trigger::isAtomicTrigger( n ) && ( n.getKind()!=APPLY_UF || n.getOperator().getKind()!=SKOLEM ); } Node ConjectureGenerator::getGroundEqc( TNode r ) { @@ -425,7 +425,7 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) { eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee ); while( !eqc_i.isFinished() ){ TNode n = (*eqc_i); - if( getTermDatabase()->hasTermCurrent( n ) && !n.getAttribute(NoMatchAttribute()) && ( n.getKind()!=EQUAL || isFalse ) ){ + if( getTermDatabase()->hasTermCurrent( n ) && getTermDatabase()->isTermActive( n ) && ( n.getKind()!=EQUAL || isFalse ) ){ if( firstTime ){ Trace("sg-gen-eqc") << "e" << d_em[r] << " : { " << std::endl; firstTime = false; diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp index 33c853328..8835d00bc 100644 --- a/src/theory/quantifiers/full_model_check.cpp +++ b/src/theory/quantifiers/full_model_check.cpp @@ -405,7 +405,7 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){ bool needsDefault = true; for( size_t i=0; i<fm->d_uf_terms[op].size(); i++ ){ Node n = fm->d_uf_terms[op][i]; - if( !n.getAttribute(NoMatchAttribute()) ){ + if( d_qe->getTermDatabase()->isTermActive( n ) ){ add_conds.push_back( n ); add_values.push_back( n ); Node r = fm->getUsedRepresentative(n); diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp index bf05de3bb..bd5100a2e 100644 --- a/src/theory/quantifiers/inst_match_generator.cpp +++ b/src/theory/quantifiers/inst_match_generator.cpp @@ -150,7 +150,7 @@ void InstMatchGenerator::initialize( Node q, QuantifiersEngine* qe, std::vector< d_cg = new inst::CandidateGeneratorQELitDeq( qe, d_match_pattern ); } }else{ - d_cg = new CandidateGeneratorQueue; + d_cg = new CandidateGeneratorQueue( qe ); Trace("inst-match-gen-warn") << "(?) Unknown matching pattern is " << d_match_pattern << std::endl; d_matchPolicy = MATCH_GEN_INTERNAL_ERROR; } @@ -697,7 +697,7 @@ int InstMatchGeneratorMulti::addTerm( Node q, Node t, QuantifiersEngine* qe ){ return addedLemmas; } -InstMatchGeneratorSimple::InstMatchGeneratorSimple( Node q, Node pat ) : d_f( q ), d_match_pattern( pat ) { +InstMatchGeneratorSimple::InstMatchGeneratorSimple( Node q, Node pat, QuantifiersEngine* qe ) : d_f( q ), d_match_pattern( pat ) { if( d_match_pattern.getKind()==NOT ){ d_match_pattern = d_match_pattern[0]; d_pol = false; @@ -720,10 +720,11 @@ InstMatchGeneratorSimple::InstMatchGeneratorSimple( Node q, Node pat ) : d_f( q } d_match_pattern_arg_types.push_back( d_match_pattern[i].getType() ); } + d_op = qe->getTermDatabase()->getMatchOperator( d_match_pattern ); } void InstMatchGeneratorSimple::resetInstantiationRound( QuantifiersEngine* qe ) { - d_op = qe->getTermDatabase()->getMatchOperator( d_match_pattern ); + } int InstMatchGeneratorSimple::addInstantiations( Node q, InstMatch& baseMatch, QuantifiersEngine* qe ){ @@ -751,6 +752,7 @@ int InstMatchGeneratorSimple::addInstantiations( Node q, InstMatch& baseMatch, Q tat = NULL; } } + Debug("simple-trigger-debug") << "Adding instantiations based on " << tat << " from " << d_op << " " << d_eqc << std::endl; if( tat ){ InstMatch m( q ); m.add( baseMatch ); diff --git a/src/theory/quantifiers/inst_match_generator.h b/src/theory/quantifiers/inst_match_generator.h index a1d907001..49e3c1ec5 100644 --- a/src/theory/quantifiers/inst_match_generator.h +++ b/src/theory/quantifiers/inst_match_generator.h @@ -224,7 +224,7 @@ private: void addInstantiations( InstMatch& m, QuantifiersEngine* qe, int& addedLemmas, int argIndex, quantifiers::TermArgTrie* tat ); public: /** constructors */ - InstMatchGeneratorSimple( Node q, Node pat ); + InstMatchGeneratorSimple( Node q, Node pat, QuantifiersEngine* qe ); /** destructor */ ~InstMatchGeneratorSimple() throw() {} /** reset instantiation round (call this whenever equivalence classes have changed) */ diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp index 630880690..d58bbcf3a 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp @@ -83,9 +83,8 @@ int InstStrategyUserPatterns::process( Node f, Theory::Effort effort, int e ){ Trace("inst-alg") << "-> User-provided instantiate " << f << "..." << std::endl; if( d_quantEngine->getInstUserPatMode()==USER_PAT_MODE_RESORT ){ - int matchOption = 0; for( unsigned i=0; i<d_user_gen_wait[f].size(); i++ ){ - Trigger * t = Trigger::mkTrigger( d_quantEngine, f, d_user_gen_wait[f][i], matchOption, true, Trigger::TR_RETURN_NULL ); + Trigger * t = Trigger::mkTrigger( d_quantEngine, f, d_user_gen_wait[f][i], true, Trigger::TR_RETURN_NULL ); if( t ){ d_user_gen[f].push_back( t ); } @@ -134,11 +133,10 @@ void InstStrategyUserPatterns::addUserPattern( Node q, Node pat ){ if( usable ){ Trace("user-pat") << "Add user pattern: " << pat << " for " << q << std::endl; //check match option - int matchOption = 0; if( d_quantEngine->getInstUserPatMode()==USER_PAT_MODE_RESORT ){ d_user_gen_wait[q].push_back( nodes ); }else{ - Trigger * t = Trigger::mkTrigger( d_quantEngine, q, nodes, matchOption, true, Trigger::TR_MAKE_NEW ); + Trigger * t = Trigger::mkTrigger( d_quantEngine, q, nodes, true, Trigger::TR_MAKE_NEW ); if( t ){ d_user_gen[q].push_back( t ); }else{ @@ -306,6 +304,23 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ last_weight = curr_w; } } + d_num_trigger_vars[f] = vcMap.size(); + if( d_num_trigger_vars[f]>0 && d_num_trigger_vars[f]<f[0].getNumChildren() ){ + Trace("auto-gen-trigger-partial") << "Quantified formula : " << f << std::endl; + Trace("auto-gen-trigger-partial") << "...does not contain all variables in triggers!!!" << std::endl; + if( options::partialTriggers() ){ + std::vector< Node > vcs[2]; + for( unsigned i=0; i<f[0].getNumChildren(); i++ ){ + Node ic = d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i ); + vcs[ vcMap.find( ic )==vcMap.end() ? 0 : 1 ].push_back( f[0][i] ); + } + for( unsigned i=0; i<2; i++ ){ + d_vc_partition[i][f] = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, vcs[i] ); + } + }else{ + return; + } + } for( unsigned i=0; i<patTermsF.size(); i++ ){ Node pat = patTermsF[i]; if( rmPatTermsF.find( pat )==rmPatTermsF.end() ){ @@ -381,10 +396,9 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ } } //now, generate the trigger... - int matchOption = 0; Trigger* tr = NULL; if( d_is_single_trigger[ patTerms[0] ] ){ - tr = Trigger::mkTrigger( d_quantEngine, f, patTerms[0], matchOption, false, Trigger::TR_RETURN_NULL ); + tr = Trigger::mkTrigger( d_quantEngine, f, patTerms[0], false, Trigger::TR_RETURN_NULL, d_num_trigger_vars[f] ); d_single_trigger_gen[ patTerms[0] ] = true; }else{ //only generate multi trigger if option set, or if no single triggers exist @@ -402,29 +416,14 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ d_made_multi_trigger[f] = true; } //will possibly want to get an old trigger - tr = Trigger::mkTrigger( d_quantEngine, f, patTerms, matchOption, false, Trigger::TR_GET_OLD ); + tr = Trigger::mkTrigger( d_quantEngine, f, patTerms, false, Trigger::TR_GET_OLD, d_num_trigger_vars[f] ); } if( tr ){ - unsigned tindex; - if( tr->isMultiTrigger() ){ - //disable all other multi triggers - for( std::map< Trigger*, bool >::iterator it = d_auto_gen_trigger[1][f].begin(); it != d_auto_gen_trigger[1][f].end(); ++it ){ - d_auto_gen_trigger[1][f][ it->first ] = false; - } - tindex = 1; - }else{ - tindex = 0; - } - //making it during an instantiation round, so must reset - if( d_auto_gen_trigger[tindex][f].find( tr )==d_auto_gen_trigger[tindex][f].end() ){ - tr->resetInstantiationRound(); - tr->reset( Node::null() ); - } - d_auto_gen_trigger[tindex][f][tr] = true; + addTrigger( tr, f ); //if we are generating additional triggers... - if( tindex==0 ){ - int index = 0; - if( index<(int)patTerms.size() ){ + if( !tr->isMultiTrigger() ){ + unsigned index = 0; + if( index<patTerms.size() ){ //Notice() << "check add additional" << std::endl; //check if similar patterns exist, and if so, add them additionally int nqfs_curr = 0; @@ -433,18 +432,13 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ } index++; bool success = true; - while( success && index<(int)patTerms.size() && d_is_single_trigger[ patTerms[index] ] ){ + while( success && index<patTerms.size() && d_is_single_trigger[ patTerms[index] ] ){ success = false; if( !options::relevantTriggers() || d_quantEngine->getQuantifierRelevance()->getNumQuantifiersForSymbol( patTerms[index].getOperator() )<=nqfs_curr ){ d_single_trigger_gen[ patTerms[index] ] = true; - Trigger* tr2 = Trigger::mkTrigger( d_quantEngine, f, patTerms[index], matchOption, false, Trigger::TR_RETURN_NULL ); - if( tr2 ){ - //Notice() << "Add additional trigger " << patTerms[index] << std::endl; - tr2->resetInstantiationRound(); - tr2->reset( Node::null() ); - d_auto_gen_trigger[0][f][tr2] = true; - } + Trigger* tr2 = Trigger::mkTrigger( d_quantEngine, f, patTerms[index], false, Trigger::TR_RETURN_NULL, d_num_trigger_vars[f] ); + addTrigger( tr2, f ); success = true; } index++; @@ -458,7 +452,8 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ } void InstStrategyAutoGenTriggers::addPatternToPool( Node q, Node pat, unsigned num_fv ) { - if( num_fv==q[0].getNumChildren() && ( options::pureThTriggers() || !Trigger::isPureTheoryTrigger( pat ) ) ){ + unsigned num_vars = options::partialTriggers() ? d_num_trigger_vars[q] : q[0].getNumChildren(); + if( num_fv==num_vars && ( options::pureThTriggers() || !Trigger::isPureTheoryTrigger( pat ) ) ){ d_patTerms[0][q].push_back( pat ); d_is_single_trigger[ pat ] = true; }else{ @@ -467,6 +462,38 @@ void InstStrategyAutoGenTriggers::addPatternToPool( Node q, Node pat, unsigned n } } + +void InstStrategyAutoGenTriggers::addTrigger( inst::Trigger * tr, Node q ) { + if( tr ){ + if( d_num_trigger_vars[q]<q[0].getNumChildren() ){ + //partial trigger : generate implication to mark user pattern + Node ipl = NodeManager::currentNM()->mkNode( INST_PATTERN_LIST, d_quantEngine->getTermDatabase()->getVariableNode( tr->getInstPattern(), q ) ); + Node qq = NodeManager::currentNM()->mkNode( FORALL, d_vc_partition[1][q], NodeManager::currentNM()->mkNode( FORALL, d_vc_partition[0][q], q[1] ), ipl ); + Trace("auto-gen-trigger-partial") << "Make partially specified user pattern: " << std::endl; + Trace("auto-gen-trigger-partial") << " " << qq << std::endl; + Node lem = NodeManager::currentNM()->mkNode( OR, q.negate(), qq ); + d_quantEngine->addLemma( lem ); + }else{ + unsigned tindex; + if( tr->isMultiTrigger() ){ + //disable all other multi triggers + for( std::map< Trigger*, bool >::iterator it = d_auto_gen_trigger[1][q].begin(); it != d_auto_gen_trigger[1][q].end(); ++it ){ + d_auto_gen_trigger[1][q][ it->first ] = false; + } + tindex = 1; + }else{ + tindex = 0; + } + //making it during an instantiation round, so must reset + if( d_auto_gen_trigger[tindex][q].find( tr )==d_auto_gen_trigger[tindex][q].end() ){ + tr->resetInstantiationRound(); + tr->reset( Node::null() ); + } + d_auto_gen_trigger[tindex][q][tr] = true; + } + } +} + bool InstStrategyAutoGenTriggers::hasUserPatterns( Node q ) { if( q.getNumChildren()==3 ){ std::map< Node, bool >::iterator it = d_hasUserPatterns.find( q ); @@ -519,8 +546,7 @@ bool InstStrategyLocalTheoryExt::isLocalTheoryExt( Node f ) { Trace("local-t-ext") << " " << patTerms[i] << std::endl; } Trace("local-t-ext") << std::endl; - int matchOption = 0; - Trigger * tr = Trigger::mkTrigger( d_quantEngine, f, patTerms, matchOption, true, Trigger::TR_GET_OLD ); + Trigger * tr = Trigger::mkTrigger( d_quantEngine, f, patTerms, true, Trigger::TR_GET_OLD ); d_lte_trigger[f] = tr; }else{ Trace("local-t-ext") << "No local theory extensions trigger for " << f << "." << std::endl; diff --git a/src/theory/quantifiers/inst_strategy_e_matching.h b/src/theory/quantifiers/inst_strategy_e_matching.h index 028f24b27..97d97b10a 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.h +++ b/src/theory/quantifiers/inst_strategy_e_matching.h @@ -83,6 +83,9 @@ private: std::map< Node, std::map< inst::Trigger*, bool > > d_processed_trigger; //instantiation no patterns std::map< Node, std::vector< Node > > d_user_no_gen; + // number of trigger variables per quantifier + std::map< Node, unsigned > d_num_trigger_vars; + std::map< Node, Node > d_vc_partition[2]; private: /** process functions */ void processResetInstantiationRound( Theory::Effort effort ); @@ -90,7 +93,7 @@ private: /** generate triggers */ void generateTriggers( Node q ); void addPatternToPool( Node q, Node pat, unsigned num_fv ); - //bool addTrigger( inst::Trigger * tr, Node f, unsigned r ); + void addTrigger( inst::Trigger * tr, Node f ); /** has user patterns */ bool hasUserPatterns( Node q ); /** has user patterns */ diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp index 3ae36b1d4..42fd7c354 100644 --- a/src/theory/quantifiers/model_builder.cpp +++ b/src/theory/quantifiers/model_builder.cpp @@ -114,7 +114,7 @@ bool TermArgBasisTrie::addTerm2( FirstOrderModel* fm, Node n, int argIndex ){ QModelBuilderIG::QModelBuilderIG( context::Context* c, QuantifiersEngine* qe ) : -QModelBuilder( c, qe ) { +QModelBuilder( c, qe ), d_basisNoMatch( c ) { } @@ -302,7 +302,7 @@ void QModelBuilderIG::analyzeModel( FirstOrderModel* fm ){ for( size_t i=0; i<fmig->d_uf_terms[op].size(); i++ ){ Node n = fmig->d_uf_terms[op][i]; //for calculating if op is constant - if( !n.getAttribute(NoMatchAttribute()) ){ + if( d_qe->getTermDatabase()->isTermActive( n ) ){ Node v = fmig->getRepresentative( n ); if( i==0 ){ d_uf_prefs[op].d_const_val = v; @@ -312,12 +312,11 @@ void QModelBuilderIG::analyzeModel( FirstOrderModel* fm ){ } } //for calculating terms that we don't need to consider - if( !n.getAttribute(NoMatchAttribute()) || n.getAttribute(ModelBasisArgAttribute())!=0 ){ - if( !n.getAttribute(BasisNoMatchAttribute()) ){ + if( d_qe->getTermDatabase()->isTermActive( n ) || n.getAttribute(ModelBasisArgAttribute())!=0 ){ + if( d_basisNoMatch.find( n )==d_basisNoMatch.end() ){ //need to consider if it is not congruent modulo model basis if( !tabt.addTerm( fmig, n ) ){ - BasisNoMatchAttribute bnma; - n.setAttribute(bnma,true); + d_basisNoMatch[n] = true; } } } @@ -382,8 +381,8 @@ bool QModelBuilderIG::isQuantifierActive( Node f ){ } bool QModelBuilderIG::isTermActive( Node n ){ - return !n.getAttribute(NoMatchAttribute()) || //it is not congruent to another active term - ( n.getAttribute(ModelBasisArgAttribute())!=0 && !n.getAttribute(BasisNoMatchAttribute()) ); //or it has model basis arguments + return d_qe->getTermDatabase()->isTermActive( n ) || //it is not congruent to another active term + ( n.getAttribute(ModelBasisArgAttribute())!=0 && d_basisNoMatch.find( n )==d_basisNoMatch.end() ); //or it has model basis arguments //and is not congruent modulo model basis //to another active term } @@ -667,7 +666,7 @@ int QModelBuilderDefault::doInstGen( FirstOrderModel* fm, Node f ){ //if applicable, try to add exceptions here if( !tr_terms.empty() ){ //make a trigger for these terms, add instantiations - inst::Trigger* tr = inst::Trigger::mkTrigger( d_qe, f, tr_terms, 0, true, inst::Trigger::TR_MAKE_NEW ); + inst::Trigger* tr = inst::Trigger::mkTrigger( d_qe, f, tr_terms, true, inst::Trigger::TR_MAKE_NEW ); //Notice() << "Trigger = " << (*tr) << std::endl; tr->resetInstantiationRound(); tr->reset( Node::null() ); diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h index 906673903..e4f9529a8 100644 --- a/src/theory/quantifiers/model_builder.h +++ b/src/theory/quantifiers/model_builder.h @@ -57,15 +57,6 @@ public: -/** Attribute true for nodes that should not be used when considered for inst-gen basis */ -struct BasisNoMatchAttributeId {}; -/** use the special for boolean flag */ -typedef expr::Attribute< BasisNoMatchAttributeId, - bool, - expr::attr::NullCleanupStrategy, - true // context dependent - > BasisNoMatchAttribute; - class TermArgBasisTrie { private: bool addTerm2( FirstOrderModel* fm, Node n, int argIndex ); @@ -85,7 +76,9 @@ public: */ class QModelBuilderIG : public QModelBuilder { + typedef context::CDHashMap<Node, bool, NodeHashFunction> BoolMap; protected: + BoolMap d_basisNoMatch; //map from operators to model preference data std::map< Node, uf::UfModelPreferenceData > d_uf_prefs; //built model uf diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 5aae4d640..2f7864831 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -185,19 +185,11 @@ RewriteResponse QuantifiersRewriter::preRewrite(TNode in) { if( in.getKind()==kind::EXISTS || in.getKind()==kind::FORALL ){ Trace("quantifiers-rewrite-debug") << "pre-rewriting " << in << std::endl; std::vector< Node > args; - for( int i=0; i<(int)in[0].getNumChildren(); i++ ){ - args.push_back( in[0][i] ); - } - Node body = in[1]; + Node body = in; bool doRewrite = false; - std::vector< Node > ipl; - while( body.getNumChildren()>=2 && body.getKind()==in.getKind() ){ - if( body.getNumChildren()==3 ){ - for( unsigned i=0; i<body[2].getNumChildren(); i++ ){ - ipl.push_back( body[2][i] ); - } - } - for( int i=0; i<(int)body[0].getNumChildren(); i++ ){ + bool firstTime = true; + while( body.getNumChildren()==2 && body.getKind()==body[1].getKind() ){ + for( unsigned i=0; i<body[0].getNumChildren(); i++ ){ args.push_back( body[0][i] ); } body = body[1]; @@ -207,14 +199,6 @@ RewriteResponse QuantifiersRewriter::preRewrite(TNode in) { std::vector< Node > children; children.push_back( NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST,args) ); children.push_back( body ); - if( in.getNumChildren()==3 ){ - for( unsigned i=0; i<in[2].getNumChildren(); i++ ){ - ipl.push_back( in[2][i] ); - } - } - if( !ipl.empty() ){ - children.push_back( NodeManager::currentNM()->mkNode( INST_PATTERN_LIST, ipl ) ); - } Node n = NodeManager::currentNM()->mkNode( in.getKind(), children ); if( in!=n ){ Trace("quantifiers-pre-rewrite") << "*** pre-rewrite " << in << std::endl; diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp index b353fce2f..b4b51fd84 100644 --- a/src/theory/quantifiers/relevant_domain.cpp +++ b/src/theory/quantifiers/relevant_domain.cpp @@ -110,7 +110,7 @@ void RelevantDomain::compute(){ for( unsigned i=0; i<sz; i++ ){ Node n = it->second[i]; //if it is a non-redundant term - if( !n.getAttribute(NoMatchAttribute()) ){ + if( db->isTermActive( n ) ){ for( unsigned j=0; j<n.getNumChildren(); j++ ){ RDomain * rf = getRDomain( op, j ); rf->addTerm( n[j] ); diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp index 5365dbcfa..2c58b8f77 100644 --- a/src/theory/quantifiers/rewrite_engine.cpp +++ b/src/theory/quantifiers/rewrite_engine.cpp @@ -175,7 +175,7 @@ int RewriteEngine::checkRewriteRule( Node f, Theory::Effort e ) { for( unsigned j=0; j<to_remove.size(); j++ ){ Node ns = d_quantEngine->getSubstitute( to_remove[j], inst ); Trace("rewrite-engine-inst-debug") << "Will remove : " << ns << std::endl; - ns.setAttribute(NoMatchAttribute(),true); + d_quantEngine->getTermDatabase()->setTermInactive( ns ); } */ }else{ diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 4dcf0e248..b143286cc 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -84,7 +84,7 @@ void TermArgTrie::debugPrint( const char * c, Node n, unsigned depth ) { } } -TermDb::TermDb( context::Context* c, context::UserContext* u, QuantifiersEngine* qe ) : d_quantEngine( qe ), d_op_id_count( 0 ), d_typ_id_count( 0 ) { +TermDb::TermDb( context::Context* c, context::UserContext* u, QuantifiersEngine* qe ) : d_quantEngine( qe ), d_inactive_map( c ), d_op_id_count( 0 ), d_typ_id_count( 0 ) { d_true = NodeManager::currentNM()->mkConst( true ); d_false = NodeManager::currentNM()->mkConst( false ); d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) ); @@ -178,6 +178,8 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant, bool wi } } } + }else{ + setTermInactive( n ); } rec = true; } @@ -210,7 +212,7 @@ void TermDb::computeUfEqcTerms( TNode f ) { for( unsigned i=0; i<d_op_map[f].size(); i++ ){ TNode n = d_op_map[f][i]; if( hasTermCurrent( n ) ){ - if( !n.getAttribute(NoMatchAttribute()) ){ + if( isTermActive( n ) ){ computeArgReps( n ); TNode r = ee->hasTerm( n ) ? ee->getRepresentative( n ) : n; d_func_map_eqc_trie[f].d_data[r].addTerm( n, d_arg_reps[n] ); @@ -471,6 +473,18 @@ bool TermDb::isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, return isEntailed2( n, subs, subsRep, true, pol, qy ); } +bool TermDb::isTermActive( Node n ) { + return d_inactive_map.find( n )==d_inactive_map.end(); + //return !n.getAttribute(NoMatchAttribute()); +} + +void TermDb::setTermInactive( Node n ) { + d_inactive_map[n] = true; + //Trace("term-db-debug2") << "set no match attribute" << std::endl; + //NoMatchAttribute nma; + //n.setAttribute(nma,true); +} + bool TermDb::hasTermCurrent( Node n, bool useMode ) { if( !useMode ){ return d_has_map.find( n )!=d_has_map.end(); @@ -636,7 +650,7 @@ bool TermDb::reset( Theory::Effort effort ){ Node n = it->second[i]; //to be added to term index, term must be relevant, and exist in EE if( hasTermCurrent( n ) && ee->hasTerm( n ) ){ - if( !n.getAttribute(NoMatchAttribute()) ){ + if( isTermActive( n ) ){ if( options::finiteModelFind() ){ computeModelBasisArgAttribute( n ); } @@ -651,13 +665,11 @@ bool TermDb::reset( Theory::Effort effort ){ } } Trace("term-db-debug") << std::endl; - if( ee->hasTerm( n ) ){ - Trace("term-db-debug") << " and value : " << ee->getRepresentative( n ) << std::endl; - } + Trace("term-db-debug") << " and value : " << ee->getRepresentative( n ) << std::endl; Node at = d_func_map_trie[ it->first ].addOrGetTerm( n, d_arg_reps[n] ); + Trace("term-db-debug2") << "...add term returned " << at << std::endl; if( at!=n && ee->areEqual( at, n ) ){ - NoMatchAttribute nma; - n.setAttribute(nma,true); + setTermInactive( n ); Trace("term-db-debug") << n << " is redundant." << std::endl; congruentCount++; }else{ @@ -846,9 +858,8 @@ void TermDb::makeInstantiationConstantsFor( Node q ){ ic.setAttribute( ivna, i ); InstConstantAttribute ica; ic.setAttribute( ica, q ); - //also set the no-match attribute - NoMatchAttribute nma; - ic.setAttribute(nma,true); + //also set the term inactive + setTermInactive( ic ); } } } @@ -906,11 +917,6 @@ Node TermDb::getInstConstAttr( Node n ) { } InstConstantAttribute ica; n.setAttribute(ica, q); - if( !q.isNull() ){ - //also set the no-match attribute - NoMatchAttribute nma; - n.setAttribute(nma,true); - } } return n.getAttribute(InstConstantAttribute()); } @@ -1019,9 +1025,12 @@ Node TermDb::getCounterexampleLiteral( Node q ){ Node TermDb::getInstConstantNode( Node n, Node q ){ makeInstantiationConstantsFor( q ); - Node n2 = n.substitute( d_vars[q].begin(), d_vars[q].end(), - d_inst_constants[q].begin(), d_inst_constants[q].end() ); - return n2; + return n.substitute( d_vars[q].begin(), d_vars[q].end(), d_inst_constants[q].begin(), d_inst_constants[q].end() ); +} + +Node TermDb::getVariableNode( Node n, Node q ) { + makeInstantiationConstantsFor( q ); + return n.substitute( d_inst_constants[q].begin(), d_inst_constants[q].end(), d_vars[q].begin(), d_vars[q].end() ); } Node TermDb::getInstantiatedNode( Node n, Node q, std::vector< Node >& terms ) { diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 266d9b8fa..004292622 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -47,15 +47,6 @@ typedef expr::Attribute< SygusAttributeId, bool > SygusAttribute; struct SynthesisAttributeId {}; typedef expr::Attribute< SynthesisAttributeId, bool > SynthesisAttribute; -/** 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<InstConstantAttributeId, Node> InstConstantAttribute; @@ -179,6 +170,7 @@ class TermDb : public QuantifiersUtil { friend class ::CVC4::theory::quantifiers::ConjectureGenerator; friend class ::CVC4::theory::quantifiers::TermGenEnv; typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap; + typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap; private: /** reference to the quantifiers engine */ QuantifiersEngine* d_quantEngine; @@ -211,6 +203,8 @@ private: std::map< Node, std::vector< Node > > d_op_map; /** map from type nodes to terms of that type */ std::map< TypeNode, std::vector< Node > > d_type_map; + /** inactive map */ + NodeBoolMap d_inactive_map; /** count number of non-redundant ground terms per operator */ std::map< Node, int > d_op_nonred_count; @@ -266,6 +260,9 @@ public: /** is entailed (incomplete check) */ bool isEntailed( TNode n, bool pol, EqualityQuery * qy = NULL ); bool isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool pol, EqualityQuery * qy = NULL ); + /** is active */ + bool isTermActive( Node n ); + void setTermInactive( Node n ); /** has term */ bool hasTermCurrent( Node n, bool useMode = true ); /** is term eligble for instantiation? */ @@ -327,6 +324,7 @@ public: instantiation. */ Node getInstConstantNode( Node n, Node q ); + Node getVariableNode( Node n, Node q ); /** get substituted node */ Node getInstantiatedNode( Node n, Node q, std::vector< Node >& terms ); diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index 38635b37b..c91194239 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -43,9 +43,8 @@ void TriggerTermInfo::init( Node q, Node n, int reqPol, Node reqPolEq ){ } /** trigger class constructor */ -Trigger::Trigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes, int matchOption ) - : d_quantEngine( qe ), d_f( f ) -{ +Trigger::Trigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes ) + : d_quantEngine( qe ), d_f( f ) { d_nodes.insert( d_nodes.begin(), nodes.begin(), nodes.end() ); Trace("trigger") << "Trigger for " << f << ": " << std::endl; for( unsigned i=0; i<d_nodes.size(); i++ ){ @@ -53,7 +52,7 @@ Trigger::Trigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes, int } if( d_nodes.size()==1 ){ if( isSimpleTrigger( d_nodes[0] ) ){ - d_mg = new InstMatchGeneratorSimple( f, d_nodes[0] ); + d_mg = new InstMatchGeneratorSimple( f, d_nodes[0], qe ); }else{ d_mg = InstMatchGenerator::mkInstMatchGenerator( f, d_nodes[0], qe ); d_mg->setActiveAdd(true); @@ -112,6 +111,10 @@ int Trigger::addTerm( Node t ){ return d_mg->addTerm( d_f, t, d_quantEngine ); } +Node Trigger::getInstPattern(){ + return NodeManager::currentNM()->mkNode( INST_PATTERN, d_nodes ); +} + int Trigger::addInstantiations( InstMatch& baseMatch ){ int addedLemmas = d_mg->addInstantiations( d_f, baseMatch, d_quantEngine ); if( addedLemmas>0 ){ @@ -124,77 +127,85 @@ int Trigger::addInstantiations( InstMatch& baseMatch ){ return addedLemmas; } -Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes, int matchOption, bool keepAll, int trOption ){ - std::vector< Node > trNodes; - if( !keepAll ){ - //only take nodes that contribute variables to the trigger when added - std::vector< Node > temp; - temp.insert( temp.begin(), nodes.begin(), nodes.end() ); - std::map< Node, bool > vars; - std::map< Node, std::vector< Node > > patterns; - size_t varCount = 0; - std::map< Node, std::vector< Node > > varContains; - quantifiers::TermDb::getVarContains( f, temp, varContains ); - for( unsigned i=0; i<temp.size(); i++ ){ - bool foundVar = false; +bool Trigger::mkTriggerTerms( Node q, std::vector< Node >& nodes, unsigned n_vars, std::vector< Node >& trNodes ) { + //only take nodes that contribute variables to the trigger when added + std::vector< Node > temp; + temp.insert( temp.begin(), nodes.begin(), nodes.end() ); + std::map< Node, bool > vars; + std::map< Node, std::vector< Node > > patterns; + size_t varCount = 0; + std::map< Node, std::vector< Node > > varContains; + quantifiers::TermDb::getVarContains( q, temp, varContains ); + for( unsigned i=0; i<temp.size(); i++ ){ + bool foundVar = false; + for( unsigned j=0; j<varContains[ temp[i] ].size(); j++ ){ + Node v = varContains[ temp[i] ][j]; + Assert( quantifiers::TermDb::getInstConstAttr(v)==q ); + if( vars.find( v )==vars.end() ){ + varCount++; + vars[ v ] = true; + foundVar = true; + } + } + if( foundVar ){ + trNodes.push_back( temp[i] ); for( unsigned j=0; j<varContains[ temp[i] ].size(); j++ ){ Node v = varContains[ temp[i] ][j]; - Assert( quantifiers::TermDb::getInstConstAttr(v)==f ); - if( vars.find( v )==vars.end() ){ - varCount++; - vars[ v ] = true; - foundVar = true; - } - } - if( foundVar ){ - trNodes.push_back( temp[i] ); - for( unsigned j=0; j<varContains[ temp[i] ].size(); j++ ){ - Node v = varContains[ temp[i] ][j]; - patterns[ v ].push_back( temp[i] ); - } - } - if( varCount==f[0].getNumChildren() ){ - break; + patterns[ v ].push_back( temp[i] ); } } - if( varCount<f[0].getNumChildren() && !options::partialTriggers() ){ - Trace("trigger-debug") << "Don't consider trigger since it does not contain all variables in " << f << std::endl; - for( unsigned i=0; i<nodes.size(); i++) { - Trace("trigger-debug") << nodes[i] << " "; - } - Trace("trigger-debug") << std::endl; + if( varCount==n_vars ){ + break; + } + } + if( varCount<n_vars ){ + Trace("trigger-debug") << "Don't consider trigger since it does not contain specified number of variables." << std::endl; + for( unsigned i=0; i<nodes.size(); i++) { + Trace("trigger-debug") << nodes[i] << " "; + } + Trace("trigger-debug") << std::endl; - //do not generate multi-trigger if it does not contain all variables - return NULL; - }else{ - //now, minimize the trigger - for( unsigned i=0; i<trNodes.size(); i++ ){ - bool keepPattern = false; - Node n = trNodes[i]; + //do not generate multi-trigger if it does not contain all variables + return false; + }else{ + //now, minimize the trigger + for( unsigned i=0; i<trNodes.size(); i++ ){ + bool keepPattern = false; + Node n = trNodes[i]; + for( unsigned j=0; j<varContains[ n ].size(); j++ ){ + Node v = varContains[ n ][j]; + if( patterns[v].size()==1 ){ + keepPattern = true; + break; + } + } + if( !keepPattern ){ + //remove from pattern vector for( unsigned j=0; j<varContains[ n ].size(); j++ ){ Node v = varContains[ n ][j]; - if( patterns[v].size()==1 ){ - keepPattern = true; - break; - } - } - if( !keepPattern ){ - //remove from pattern vector - for( unsigned j=0; j<varContains[ n ].size(); j++ ){ - Node v = varContains[ n ][j]; - for( unsigned k=0; k<patterns[v].size(); k++ ){ - if( patterns[v][k]==n ){ - patterns[v].erase( patterns[v].begin() + k, patterns[v].begin() + k + 1 ); - break; - } + for( unsigned k=0; k<patterns[v].size(); k++ ){ + if( patterns[v][k]==n ){ + patterns[v].erase( patterns[v].begin() + k, patterns[v].begin() + k + 1 ); + break; } } - //remove from trigger nodes - trNodes.erase( trNodes.begin() + i, trNodes.begin() + i + 1 ); - i--; } + //remove from trigger nodes + trNodes.erase( trNodes.begin() + i, trNodes.begin() + i + 1 ); + i--; } } + } + return true; +} + +Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes, bool keepAll, int trOption, unsigned use_n_vars ){ + std::vector< Node > trNodes; + if( !keepAll ){ + unsigned n_vars = use_n_vars==0 ? f[0].getNumChildren() : use_n_vars; + if( !mkTriggerTerms( f, nodes, n_vars, trNodes ) ){ + return NULL; + } }else{ trNodes.insert( trNodes.begin(), nodes.begin(), nodes.end() ); } @@ -211,15 +222,15 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& } } } - Trigger* t = new Trigger( qe, f, trNodes, matchOption ); + Trigger* t = new Trigger( qe, f, trNodes ); qe->getTriggerDatabase()->addTrigger( trNodes, t ); return t; } -Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, Node n, int matchOption, bool keepAll, int trOption ){ +Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, Node n, bool keepAll, int trOption, unsigned use_n_vars ){ std::vector< Node > nodes; nodes.push_back( n ); - return mkTrigger( qe, f, nodes, matchOption, keepAll, trOption ); + return mkTrigger( qe, f, nodes, keepAll, trOption, use_n_vars ); } bool Trigger::isUsable( Node n, Node q ){ @@ -343,9 +354,7 @@ bool Trigger::isUsableTrigger( Node n, Node q ){ } bool Trigger::isAtomicTrigger( Node n ){ - Kind k = n.getKind(); - return ( k==APPLY_UF && !n.getOperator().getAttribute(NoMatchAttribute()) ) || - ( k!=APPLY_UF && isAtomicTriggerKind( k ) ); + return isAtomicTriggerKind( n.getKind() ); } bool Trigger::isAtomicTriggerKind( Kind k ) { diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h index 41f2a1c38..902f73e75 100644 --- a/src/theory/quantifiers/trigger.h +++ b/src/theory/quantifiers/trigger.h @@ -76,6 +76,8 @@ class Trigger { int addTerm( Node t ); /** return whether this is a multi-trigger */ bool isMultiTrigger() { return d_nodes.size()>1; } + /** get inst pattern list */ + Node getInstPattern(); /** add all available instantiations exhaustively, in any equivalence class if limitInst>0, limitInst is the max # of instantiations to try */ @@ -84,8 +86,6 @@ class Trigger { ie : quantifier engine; f : forall something .... nodes : (multi-)trigger - matchOption : which policy to use for creating matches - (one of InstMatchGenerator::MATCH_GEN_* ) keepAll: don't remove unneeded patterns; trOption : policy for dealing with triggers that already existed (see below) @@ -95,12 +95,12 @@ class Trigger { TR_GET_OLD, //return a previous trigger if it had already been created TR_RETURN_NULL //return null if a duplicate is found }; - static Trigger* mkTrigger( QuantifiersEngine* qe, Node f, - std::vector< Node >& nodes, int matchOption = 0, - bool keepAll = true, int trOption = TR_MAKE_NEW ); - static Trigger* mkTrigger( QuantifiersEngine* qe, Node f, Node n, - int matchOption = 0, bool keepAll = true, - int trOption = TR_MAKE_NEW ); + //nodes input, trNodes output + static bool mkTriggerTerms( Node q, std::vector< Node >& nodes, unsigned n_vars, std::vector< Node >& trNodes ); + static Trigger* mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes, + bool keepAll = true, int trOption = TR_MAKE_NEW, unsigned use_n_vars = 0 ); + static Trigger* mkTrigger( QuantifiersEngine* qe, Node f, Node n, bool keepAll = true, + int trOption = TR_MAKE_NEW, unsigned use_n_vars = 0 ); static void collectPatTerms( Node q, Node n, std::vector< Node >& patTerms, quantifiers::TriggerSelMode tstrt, std::vector< Node >& exclude, std::map< Node, TriggerTermInfo >& tinfo, bool filterInst = false ); @@ -135,7 +135,7 @@ class Trigger { } private: /** trigger constructor */ - Trigger( QuantifiersEngine* ie, Node f, std::vector< Node >& nodes, int matchOption = 0 ); + Trigger( QuantifiersEngine* ie, Node f, std::vector< Node >& nodes ); /** is subterm of trigger usable */ static bool isUsable( Node n, Node q ); |