/** 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];
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;
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() );
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 ) ){
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;
//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;
//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;
}
}
}
}
//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() ){
}
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;
}
}
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 );
+ }
}
}
}
projects / cvc5.git / commitdiff