From bf682b92e2bddcd490604f8a65c440b9c4c2f2f9 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Tue, 4 Apr 2017 12:54:26 -0500 Subject: [PATCH] Enable multi-trigger-linear by default, add option. --- src/options/quantifiers_options | 4 +- .../quantifiers/inst_match_generator.cpp | 64 ++++++++++++------- src/theory/quantifiers/inst_match_generator.h | 2 + src/theory/quantifiers/trigger.cpp | 6 +- .../quaternion_ds1_symm_0428.fof.smt2 | 2 +- 5 files changed, 49 insertions(+), 29 deletions(-) diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index e8586a898..cd6333225 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -91,7 +91,9 @@ option multiTriggerWhenSingle --multi-trigger-when-single bool :default false select multi triggers when single triggers exist option multiTriggerPriority --multi-trigger-priority bool :default false only try multi triggers if single triggers give no instantiations -option multiTriggerLinear --multi-trigger-linear bool :default false +option multiTriggerCache --multi-trigger-cache bool :default false + caching version of multi triggers +option multiTriggerLinear --multi-trigger-linear bool :default true implementation of multi triggers where maximum number of instantiations is linear wrt number of ground terms option triggerSelMode --trigger-sel CVC4::theory::quantifiers::TriggerSelMode :default CVC4::theory::quantifiers::TRIGGER_SEL_MIN :read-write :include "options/quantifiers_modes.h" :handler stringToTriggerSelMode selection mode for triggers diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp index a54c5cd92..889fe667e 100644 --- a/src/theory/quantifiers/inst_match_generator.cpp +++ b/src/theory/quantifiers/inst_match_generator.cpp @@ -610,17 +610,31 @@ InstMatchGeneratorMultiLinear::~InstMatchGeneratorMultiLinear() throw() { } +int InstMatchGeneratorMultiLinear::resetChildren( QuantifiersEngine* qe ){ + for( unsigned i=0; ireset( Node::null(), qe ) ){ + return -2; + } + } + return 1; +} + bool InstMatchGeneratorMultiLinear::reset( Node eqc, QuantifiersEngine* qe ) { Assert( eqc.isNull() ); - return true; + if( options::multiTriggerLinear() ){ + return true; + }else{ + return resetChildren( qe )>0; + } } int InstMatchGeneratorMultiLinear::getNextMatch( Node q, InstMatch& m, QuantifiersEngine* qe ) { Trace("multi-trigger-linear-debug") << "InstMatchGeneratorMultiLinear::getNextMatch : reset " << std::endl; - //reset everyone - for( unsigned i=0; ireset( Node::null(), qe ) ){ - return -2; + if( options::multiTriggerLinear() ){ + //reset everyone + int rc_ret = resetChildren( qe ); + if( rc_ret<0 ){ + return rc_ret; } } Trace("multi-trigger-linear-debug") << "InstMatchGeneratorMultiLinear::getNextMatch : continue match " << std::endl; @@ -628,11 +642,13 @@ int InstMatchGeneratorMultiLinear::getNextMatch( Node q, InstMatch& m, Quantifie int ret_val = continueNextMatch( q, m, qe ); if( ret_val>0 ){ Trace("multi-trigger-linear") << "Successful multi-trigger instantiation." << std::endl; - // now, restrict everyone - for( unsigned i=0; id_curr_matched; - Trace("multi-trigger-linear") << " child " << i << " match : " << mi << std::endl; - d_children[i]->excludeMatch( mi ); + if( options::multiTriggerLinear() ){ + // now, restrict everyone + for( unsigned i=0; id_curr_matched; + Trace("multi-trigger-linear") << " child " << i << " match : " << mi << std::endl; + d_children[i]->excludeMatch( mi ); + } } } return ret_val; @@ -642,19 +658,19 @@ int InstMatchGeneratorMultiLinear::getNextMatch( Node q, InstMatch& m, Quantifie /** constructors */ InstMatchGeneratorMulti::InstMatchGeneratorMulti( Node q, std::vector< Node >& pats, QuantifiersEngine* qe ) : d_f( q ){ - Trace("smart-multi-trigger") << "Making smart multi-trigger for " << q << std::endl; + Trace("multi-trigger-cache") << "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 ){ - Trace("smart-multi-trigger") << "Pattern " << it->first << " contains: "; + Trace("multi-trigger-cache") << "Pattern " << it->first << " contains: "; for( int i=0; i<(int)it->second.size(); i++ ){ - Trace("smart-multi-trigger") << it->second[i] << " "; + Trace("multi-trigger-cache") << 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 ); } - Trace("smart-multi-trigger") << std::endl; + Trace("multi-trigger-cache") << std::endl; } for( unsigned i=0; id_order.insert( d_imtio[i]->d_order.begin(), vars.begin(), vars.end() ); @@ -730,9 +746,9 @@ bool InstMatchGeneratorMulti::reset( Node eqc, QuantifiersEngine* qe ){ int InstMatchGeneratorMulti::addInstantiations( Node q, InstMatch& baseMatch, QuantifiersEngine* qe ){ int addedLemmas = 0; - Trace("smart-multi-trigger") << "Process smart multi trigger" << std::endl; + Trace("multi-trigger-cache") << "Process smart multi trigger" << std::endl; for( unsigned i=0; i newMatches; InstMatch m( q ); while( d_children[i]->getNextMatch( q, m, qe )>0 ){ @@ -740,9 +756,9 @@ int InstMatchGeneratorMulti::addInstantiations( Node q, InstMatch& baseMatch, Qu newMatches.push_back( InstMatch( &m ) ); m.clear(); } - Trace("smart-multi-trigger") << "Made " << newMatches.size() << " new matches for index " << i << std::endl; + Trace("multi-trigger-cache") << "Made " << newMatches.size() << " new matches for index " << i << std::endl; for( unsigned j=0; j unique_var_tries; @@ -860,7 +876,7 @@ void InstMatchGeneratorMulti::processNewInstantiations2( QuantifiersEngine* qe, //m is an instantiation if( qe->addInstantiation( d_f, m ) ){ addedLemmas++; - Trace("smart-multi-trigger-debug") << "-> Produced instantiation " << m << std::endl; + Trace("multi-trigger-cache-debug") << "-> Produced instantiation " << m << std::endl; } } } diff --git a/src/theory/quantifiers/inst_match_generator.h b/src/theory/quantifiers/inst_match_generator.h index f6f23dfb3..910cde131 100644 --- a/src/theory/quantifiers/inst_match_generator.h +++ b/src/theory/quantifiers/inst_match_generator.h @@ -177,6 +177,8 @@ public: /** smart multi-trigger implementation */ class InstMatchGeneratorMultiLinear : public InstMatchGenerator { +private: + int resetChildren( QuantifiersEngine* qe ); public: /** constructors */ InstMatchGeneratorMultiLinear( Node q, std::vector< Node >& pats, QuantifiersEngine* qe ); diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index d4d6cfb00..f2a4e6d17 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -58,11 +58,11 @@ Trigger::Trigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes ) d_mg->setActiveAdd(true); } }else{ - if( options::multiTriggerLinear() ){ + if( options::multiTriggerCache() ){ + d_mg = new InstMatchGeneratorMulti( f, d_nodes, qe ); + }else{ d_mg = InstMatchGenerator::mkInstMatchGeneratorMulti( f, d_nodes, qe ); d_mg->setActiveAdd(true); - }else{ - d_mg = new InstMatchGeneratorMulti( f, d_nodes, qe ); } //d_mg = InstMatchGenerator::mkInstMatchGenerator( d_nodes, qe ); //d_mg->setActiveAdd(); diff --git a/test/regress/regress0/quantifiers/quaternion_ds1_symm_0428.fof.smt2 b/test/regress/regress0/quantifiers/quaternion_ds1_symm_0428.fof.smt2 index 9b0216e58..e7be953ce 100644 --- a/test/regress/regress0/quantifiers/quaternion_ds1_symm_0428.fof.smt2 +++ b/test/regress/regress0/quantifiers/quaternion_ds1_symm_0428.fof.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --full-saturate-quant +; COMMAND-LINE: --full-saturate-quant --multi-trigger-cache ; EXPECT: unsat (set-logic AUFLIRA) (set-info :status unsat) -- 2.30.2