diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-07-31 03:20:17 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-07-31 03:20:24 -0500 |
commit | ec16b410a725e4a7659c41f87327cdd1ef7b59e1 (patch) | |
tree | 04698754f0370b5991b0a7c2b4a36a5662e0352d /src | |
parent | 1307691a6306e84efb4e194755bb111fa0843dd4 (diff) |
Minor improvement for enumerative instantiation.
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/quantifiers/inst_strategy_e_matching.cpp | 42 |
1 files changed, 27 insertions, 15 deletions
diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp index 582b6ba7c..b4821cfd6 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp @@ -682,13 +682,36 @@ bool FullSaturation::process( Node f, bool fullEffort ){ std::vector< unsigned > maxs; std::vector< bool > max_zero; bool has_zero = false; + std::map< TypeNode, std::vector< Node > > term_db_list; + std::vector< TypeNode > ftypes; + // iterate over substitutions for variables for(unsigned i=0; i<f[0].getNumChildren(); i++ ){ + TypeNode tn = f[0][i].getType(); + ftypes.push_back( tn ); unsigned ts; if( r==0 ){ ts = rd->getRDomain( f, i )->d_terms.size(); }else{ - ts = d_quantEngine->getTermDatabase()->getNumTypeGroundTerms( f[0][i].getType() ); + ts = d_quantEngine->getTermDatabase()->getNumTypeGroundTerms( tn ); + std::map< TypeNode, std::vector< Node > >::iterator ittd = term_db_list.find( tn ); + if( ittd==term_db_list.end() ){ + std::map< Node, Node > reps_found; + for( unsigned j=0; j<ts; j++ ){ + Node gt = d_quantEngine->getTermDatabase()->getTypeGroundTerm( ftypes[i], j ); + if( !options::cbqi() || !quantifiers::TermDb::hasInstConstAttr( gt ) ){ + Node r = d_quantEngine->getEqualityQuery()->getRepresentative( gt ); + if( reps_found.find( r )==reps_found.end() ){ + reps_found[r] = gt; + term_db_list[tn].push_back( gt ); + } + } + } + ts = term_db_list[tn].size(); + }else{ + ts = ittd->second.size(); + } } + // consider a default value if at full effort max_zero.push_back( fullEffort && ts==0 ); ts = ( fullEffort && ts==0 ) ? 1 : ts; Trace("inst-alg-rd") << "Variable " << i << " has " << ts << " in relevant domain." << std::endl; @@ -703,11 +726,6 @@ bool FullSaturation::process( Node f, bool fullEffort ){ } } if( !has_zero ){ - std::vector< TypeNode > ftypes; - for( unsigned i=0; i<f[0].getNumChildren(); i++ ){ - ftypes.push_back( f[0][i].getType() ); - } - Trace("inst-alg-rd") << "Will do " << final_max_i << " stages of instantiation." << std::endl; unsigned max_i = 0; bool success; @@ -722,13 +740,6 @@ bool FullSaturation::process( Node f, bool fullEffort ){ }else{ Assert( index==(int)(childIndex.size())-1 ); unsigned nv = childIndex[index]+1; - if( options::cbqi() && r==1 && !max_zero[index] ){ - //skip inst constant nodes - while( nv<maxs[index] && nv<=max_i && - quantifiers::TermDb::hasInstConstAttr( d_quantEngine->getTermDatabase()->getTypeGroundTerm( ftypes[index], nv ) ) ){ - nv++; - } - } if( nv<maxs[index] && nv<=max_i ){ childIndex[index] = nv; index++; @@ -756,8 +767,9 @@ bool FullSaturation::process( Node f, bool fullEffort ){ terms.push_back( rd->getRDomain( f, i )->d_terms[childIndex[i]] ); Trace("inst-alg-rd") << " " << rd->getRDomain( f, i )->d_terms[childIndex[i]] << std::endl; }else{ - terms.push_back( d_quantEngine->getTermDatabase()->getTypeGroundTerm( ftypes[i], childIndex[i] ) ); - Trace("inst-alg-rd") << " " << d_quantEngine->getTermDatabase()->getTypeGroundTerm( ftypes[i], childIndex[i] ) << std::endl; + Assert( childIndex[i]<term_db_list[ftypes[i]].size() ); + terms.push_back( term_db_list[ftypes[i]][childIndex[i]] ); + Trace("inst-alg-rd") << " " << term_db_list[ftypes[i]][childIndex[i]] << std::endl; } } if( d_quantEngine->addInstantiation( f, terms ) ){ |