diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-06-16 18:06:27 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-06-16 18:06:27 +0200 |
commit | 7a36dd1e29c6d0160f949d5f805044768fb549d1 (patch) | |
tree | bb2fea5fac3879868895c2c1dfaf0f969d94dd1d /src/theory/rep_set.cpp | |
parent | 9b32405be875e7d20289d8eabbe85d036a31f301 (diff) |
Avoid completion for large finite types. Fix bug for --fmf-fun.
Diffstat (limited to 'src/theory/rep_set.cpp')
-rw-r--r-- | src/theory/rep_set.cpp | 27 |
1 files changed, 21 insertions, 6 deletions
diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp index 454fe8971..eb05564e5 100644 --- a/src/theory/rep_set.cpp +++ b/src/theory/rep_set.cpp @@ -15,6 +15,7 @@ #include "theory/rep_set.h" #include "theory/type_enumerator.h" #include "theory/quantifiers/bounded_integers.h" +#include "theory/quantifiers/term_database.h" using namespace std; using namespace CVC4; @@ -86,8 +87,15 @@ int RepSet::getIndexFor( Node n ) const { } } -void RepSet::complete( TypeNode t ){ - if( d_type_complete.find( t )==d_type_complete.end() ){ +bool RepSet::complete( TypeNode t ){ + std::map< TypeNode, bool >::iterator it = d_type_complete.find( t ); + if( it==d_type_complete.end() ){ + //remove all previous + for( unsigned i=0; i<d_type_reps[t].size(); i++ ){ + d_tmap.erase( d_type_reps[t][i] ); + } + d_type_reps[t].clear(); + //now complete the type d_type_complete[t] = true; TypeEnumerator te(t); while( !te.isFinished() ){ @@ -101,6 +109,9 @@ void RepSet::complete( TypeNode t ){ Trace("reps-complete") << d_type_reps[t][i] << " "; } Trace("reps-complete") << std::endl; + return true; + }else{ + return it->second; } } @@ -165,6 +176,7 @@ bool RepSetIterator::setFunctionDomain( Node op ){ } bool RepSetIterator::initialize(){ + Trace("rsi") << "Initialize rep set iterator..." << std::endl; for( size_t i=0; i<d_types.size(); i++ ){ d_index.push_back( 0 ); //store default index order @@ -173,6 +185,7 @@ bool RepSetIterator::initialize(){ //store default domain d_domain.push_back( RepDomain() ); TypeNode tn = d_types[i]; + Trace("rsi") << "Var #" << i << " is type " << tn << "..." << std::endl; if( tn.isSort() ){ if( !d_rep_set->hasType( tn ) ){ Node var = NodeManager::currentNM()->mkSkolem( "repSet", tn, "is a variable created by the RepSetIterator" ); @@ -184,7 +197,7 @@ bool RepSetIterator::initialize(){ //check if it is bound if( d_owner.getKind()==FORALL && d_qe && d_qe->getBoundedIntegers() ){ if( d_qe->getBoundedIntegers()->isBoundVar( d_owner, d_owner[0][i] ) ){ - Trace("bound-int-rsi") << "Rep set iterator: variable #" << i << " is bounded integer." << std::endl; + Trace("rsi") << " variable is bounded integer." << std::endl; d_enum_type.push_back( ENUM_RANGE ); }else{ inc = true; @@ -195,18 +208,20 @@ bool RepSetIterator::initialize(){ if( inc ){ //check if it is otherwise bound if( d_bounds[0].find(i)!=d_bounds[0].end() && d_bounds[1].find(i)!=d_bounds[1].end() ){ - Trace("bound-int-rsi") << "Rep set iterator: variable #" << i << " is bounded." << std::endl; + Trace("rsi") << " variable is bounded." << std::endl; d_enum_type.push_back( ENUM_RANGE ); }else{ + Trace("rsi") << " variable cannot be bounded." << std::endl; Trace("fmf-incomplete") << "Incomplete because of integer quantification of " << d_owner[0][i] << "." << std::endl; d_incomplete = true; } } //enumerate if the sort is reasonably small, not an Array, the upper bound of 1000 is chosen arbitrarily for now - }else if( !tn.isArray() && tn.getCardinality().isFinite() && !tn.getCardinality().isLargeFinite() && - tn.getCardinality().getFiniteCardinality().toUnsignedInt()<=1000 ){ + }else if( d_qe->getTermDatabase()->mayComplete( tn ) ){ + Trace("rsi") << " do complete, since cardinality is small (" << tn.getCardinality() << ")..." << std::endl; d_rep_set->complete( tn ); }else{ + Trace("rsi") << " variable cannot be bounded." << std::endl; Trace("fmf-incomplete") << "Incomplete because of quantification of type " << tn << std::endl; d_incomplete = true; } |