From: ajreynol Date: Thu, 30 Mar 2017 14:11:52 +0000 (-0500) Subject: Minor fixes for trigger selection max. X-Git-Tag: cvc5-1.0.0~5856 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=100037d531ff1fd30ed3dd5bed91076c383ad55c;p=cvc5.git Minor fixes for trigger selection max. --- 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; id_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 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 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 added2; + for( unsigned i=0; isecond.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 );