diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-30 09:11:52 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-30 09:11:52 -0500 |
commit | 100037d531ff1fd30ed3dd5bed91076c383ad55c (patch) | |
tree | f31d60fd4a902efa45e2db109632c607aee5c575 /src/theory/quantifiers | |
parent | fa5df1aad69f8ad62686b9418070a1baf74b4a77 (diff) |
Minor fixes for trigger selection max.
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/inst_match_generator.cpp | 27 | ||||
-rw-r--r-- | src/theory/quantifiers/trigger.cpp | 85 | ||||
-rw-r--r-- | src/theory/quantifiers/trigger.h | 2 |
3 files changed, 58 insertions, 56 deletions
diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp index 7cf9868bd..661451b68 100644 --- a/src/theory/quantifiers/inst_match_generator.cpp +++ b/src/theory/quantifiers/inst_match_generator.cpp @@ -482,19 +482,19 @@ bool VarMatchGeneratorTermSubs::getNextMatch( Node q, InstMatch& m, QuantifiersE /** constructors */ InstMatchGeneratorMulti::InstMatchGeneratorMulti( Node q, std::vector< Node >& pats, QuantifiersEngine* qe ) : d_f( q ){ - Debug("smart-multi-trigger") << "Making smart multi-trigger for " << q << std::endl; + Trace("smart-multi-trigger") << "Making smart multi-trigger for " << q << std::endl; std::map< Node, std::vector< Node > > var_contains; qe->getTermDatabase()->getVarContains( q, 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: "; + Trace("smart-multi-trigger") << "Pattern " << it->first << " contains: "; for( int i=0; i<(int)it->second.size(); i++ ){ - Debug("smart-multi-trigger") << it->second[i] << " "; + Trace("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; + Trace("smart-multi-trigger") << std::endl; } for( unsigned i=0; i<pats.size(); i++ ){ Node n = pats[i]; @@ -506,7 +506,7 @@ d_f( q ){ int numSharedVars = 0; for( unsigned j=0; j<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; + Trace("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; @@ -530,11 +530,11 @@ d_f( q ){ 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 << "]: "; + Trace("smart-multi-trigger") << " Index[" << i << "]: "; for( unsigned j=0; j<vars.size(); j++ ){ - Debug("smart-multi-trigger") << vars[j] << " "; + Trace("smart-multi-trigger") << vars[j] << " "; } - Debug("smart-multi-trigger") << std::endl; + Trace("smart-multi-trigger") << std::endl; //make ordered inst match trie d_imtio[i] = new InstMatchTrie::ImtIndexOrder; d_imtio[i]->d_order.insert( d_imtio[i]->d_order.begin(), vars.begin(), vars.end() ); @@ -567,9 +567,9 @@ void InstMatchGeneratorMulti::reset( Node eqc, QuantifiersEngine* qe ){ int InstMatchGeneratorMulti::addInstantiations( Node q, InstMatch& baseMatch, QuantifiersEngine* qe ){ int addedLemmas = 0; - Debug("smart-multi-trigger") << "Process smart multi trigger" << std::endl; + Trace("smart-multi-trigger") << "Process smart multi trigger" << std::endl; for( unsigned i=0; i<d_children.size(); i++ ){ - Debug("smart-multi-trigger") << "Calculate matches " << i << std::endl; + Trace("smart-multi-trigger") << "Calculate matches " << i << std::endl; std::vector< InstMatch > newMatches; InstMatch m( q ); while( d_children[i]->getNextMatch( q, m, qe ) ){ @@ -577,8 +577,9 @@ int InstMatchGeneratorMulti::addInstantiations( Node q, InstMatch& baseMatch, Qu newMatches.push_back( InstMatch( &m ) ); m.clear(); } - Debug("smart-multi-trigger") << "Made " << newMatches.size() << " new matches for index " << i << std::endl; + Trace("smart-multi-trigger") << "Made " << newMatches.size() << " new matches for index " << i << std::endl; for( unsigned j=0; j<newMatches.size(); j++ ){ + Trace("smart-multi-trigger2") << "...processing " << j << " / " << newMatches.size() << ", #lemmas = " << addedLemmas << std::endl; processNewMatch( qe, newMatches[j], i, addedLemmas ); if( qe->inConflict() ){ return addedLemmas; @@ -594,7 +595,7 @@ void InstMatchGeneratorMulti::processNewMatch( QuantifiersEngine* qe, InstMatch& //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; + Trace("smart-multi-trigger-debug") << "Child " << fromChildIndex << " produced match " << m << std::endl; //process new instantiations int childIndex = (fromChildIndex+1)%(int)d_children.size(); std::vector< IndexedTrie > unique_var_tries; @@ -696,7 +697,7 @@ void InstMatchGeneratorMulti::processNewInstantiations2( QuantifiersEngine* qe, //m is an instantiation if( qe->addInstantiation( d_f, m ) ){ addedLemmas++; - Debug("smart-multi-trigger") << "-> Produced instantiation " << m << std::endl; + Trace("smart-multi-trigger-debug") << "-> Produced instantiation " << m << std::endl; } } } diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index 1bfc53b41..7072d0499 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -398,16 +398,14 @@ bool Trigger::isSimpleTrigger( Node n ){ } //store triggers in reqPol, indicating their polarity (if any) they must appear to falsify the quantified formula -bool Trigger::collectPatTerms2( Node q, Node n, std::map< Node, Node >& visited, std::map< Node, TriggerTermInfo >& tinfo, +void Trigger::collectPatTerms2( Node q, Node n, std::map< Node, Node >& visited, std::map< Node, TriggerTermInfo >& tinfo, quantifiers::TriggerSelMode tstrt, std::vector< Node >& exclude, std::vector< Node >& added, bool pol, bool hasPol, bool epol, bool hasEPol ){ std::map< Node, Node >::iterator itv = visited.find( n ); if( itv==visited.end() ){ visited[ n ] = Node::null(); Trace("auto-gen-trigger-debug2") << "Collect pat terms " << n << " " << pol << " " << hasPol << " " << epol << " " << hasEPol << std::endl; - bool retVal = false; if( n.getKind()!=FORALL && n.getKind()!=INST_CONSTANT ){ - bool rec = true; Node nu; bool nu_single = false; if( n.getKind()!=NOT && std::find( exclude.begin(), exclude.end(), n )==exclude.end() ){ @@ -426,11 +424,11 @@ bool Trigger::collectPatTerms2( Node q, Node n, std::map< Node, Node >& visited, } Assert( reqEq.isNull() || !quantifiers::TermDb::hasInstConstAttr( reqEq ) ); Assert( isUsableTrigger( nu, q ) ); - //do not add if already excluded + //do not add if already visited bool add = true; if( n!=nu ){ std::map< Node, Node >::iterator itvu = visited.find( nu ); - if( itvu!=visited.end() && itvu->second.isNull() ){ + if( itvu!=visited.end() ){ add = false; } } @@ -439,55 +437,58 @@ bool Trigger::collectPatTerms2( Node q, Node n, std::map< Node, Node >& visited, visited[ nu ] = nu; tinfo[ nu ].init( q, nu, hasEPol ? ( epol ? 1 : -1 ) : 0, reqEq ); nu_single = tinfo[ nu ].d_fv.size()==q[0].getNumChildren(); - retVal = true; - if( tstrt==quantifiers::TRIGGER_SEL_MAX || ( tstrt==quantifiers::TRIGGER_SEL_MIN_SINGLE_MAX && !nu_single ) ){ - rec = false; - } + }else{ + nu = Node::null(); } } } - if( rec ){ - Node nrec = nu.isNull() ? n : nu; - std::vector< Node > added2; - for( unsigned i=0; i<nrec.getNumChildren(); i++ ){ - bool newHasPol, newPol; - bool newHasEPol, newEPol; - QuantPhaseReq::getPolarity( nrec, i, hasPol, pol, newHasPol, newPol ); - QuantPhaseReq::getEntailPolarity( nrec, i, hasEPol, epol, newHasEPol, newEPol ); - if( collectPatTerms2( q, nrec[i], visited, tinfo, tstrt, exclude, added2, newPol, newHasPol, newEPol, newHasEPol ) ){ - retVal = true; - } - } - if( !nu.isNull() ){ - bool rm_nu = false; - //discard if we added a subterm as a trigger with all variables that nu has - for( unsigned i=0; i<added2.size(); i++ ){ - Assert( tinfo.find( added2[i] )!=tinfo.end() ); - if( added2[i]!=nu ){ + Node nrec = nu.isNull() ? n : nu; + std::vector< Node > added2; + for( unsigned i=0; i<nrec.getNumChildren(); i++ ){ + bool newHasPol, newPol; + bool newHasEPol, newEPol; + QuantPhaseReq::getPolarity( nrec, i, hasPol, pol, newHasPol, newPol ); + QuantPhaseReq::getEntailPolarity( nrec, i, hasEPol, epol, newHasEPol, newEPol ); + collectPatTerms2( q, nrec[i], visited, tinfo, tstrt, exclude, added2, newPol, newHasPol, newEPol, newHasEPol ); + } + if( !nu.isNull() ){ + bool rm_nu = false; + for( unsigned i=0; i<added2.size(); i++ ){ + Trace("auto-gen-trigger-debug2") << "..." << nu << " added child " << i << " : " << added2[i] << std::endl; + Assert( added2[i]!=nu ); + // if child was not already removed + if( tinfo.find( added2[i] )!=tinfo.end() ){ + if( tstrt==quantifiers::TRIGGER_SEL_MAX || ( tstrt==quantifiers::TRIGGER_SEL_MIN_SINGLE_MAX && !nu_single ) ){ + //discard all subterms + Trace("auto-gen-trigger-debug2") << "......remove it." << std::endl; + visited[added2[i]] = Node::null(); + tinfo.erase( added2[i] ); + }else{ if( tinfo[ nu ].d_fv.size()==tinfo[ added2[i] ].d_fv.size() ){ + //discard if we added a subterm as a trigger with all variables that nu has + Trace("auto-gen-trigger-debug2") << "......subsumes parent." << std::endl; rm_nu = true; } - added.push_back( added2[i] ); - }else{ - Assert( false ); + if( std::find( added.begin(), added.end(), added2[i] )==added.end() ){ + added.push_back( added2[i] ); + } } } - if( rm_nu && ( tstrt==quantifiers::TRIGGER_SEL_MIN || ( tstrt==quantifiers::TRIGGER_SEL_MIN_SINGLE_ALL && nu_single ) ) ){ - visited[nu] = Node::null(); - tinfo.erase( nu ); - }else{ - added.push_back( nu ); - } + } + if( rm_nu && ( tstrt==quantifiers::TRIGGER_SEL_MIN || ( tstrt==quantifiers::TRIGGER_SEL_MIN_SINGLE_ALL && nu_single ) ) ){ + visited[nu] = Node::null(); + tinfo.erase( nu ); + }else{ + Assert( std::find( added.begin(), added.end(), nu )==added.end() ); + added.push_back( nu ); } } } - return retVal; }else{ - if( itv->second.isNull() ){ - return false; - }else{ - added.push_back( itv->second ); - return true; + if( !itv->second.isNull() ){ + if( std::find( added.begin(), added.end(), itv->second )==added.end() ){ + added.push_back( itv->second ); + } } } } diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h index 631627331..9ff82595f 100644 --- a/src/theory/quantifiers/trigger.h +++ b/src/theory/quantifiers/trigger.h @@ -142,7 +142,7 @@ private: static Node getIsUsableEq( Node q, Node eq ); static bool isUsableEqTerms( Node q, Node n1, Node n2 ); /** collect all APPLY_UF pattern terms for f in n */ - static bool collectPatTerms2( Node q, Node n, std::map< Node, Node >& visited, std::map< Node, TriggerTermInfo >& tinfo, + static void collectPatTerms2( Node q, Node n, std::map< Node, Node >& visited, std::map< Node, TriggerTermInfo >& tinfo, quantifiers::TriggerSelMode tstrt, std::vector< Node >& exclude, std::vector< Node >& added, bool pol, bool hasPol, bool epol, bool hasEPol ); |