diff options
Diffstat (limited to 'src/theory/rep_set.cpp')
-rw-r--r-- | src/theory/rep_set.cpp | 46 |
1 files changed, 32 insertions, 14 deletions
diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp index 180c4bbcf..b44cc6779 100644 --- a/src/theory/rep_set.cpp +++ b/src/theory/rep_set.cpp @@ -139,7 +139,6 @@ bool RepSetIterator::initialize(){ //store default domain d_domain.push_back( RepDomain() ); TypeNode tn = d_types[i]; - bool isSet = false; if( tn.isSort() ){ if( !d_rep_set->hasType( tn ) ){ Node var = NodeManager::currentNM()->mkSkolem( "repSet_$$", tn, "is a variable created by the RepSetIterator" ); @@ -147,31 +146,36 @@ bool RepSetIterator::initialize(){ d_rep_set->add( var ); } }else if( tn.isInteger() ){ + bool inc = false; //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; d_enum_type.push_back( ENUM_RANGE ); - isSet = true; }else{ - Trace("fmf-incomplete") << "Incomplete because of integer quantification, no bounds found." << std::endl; - d_incomplete = true; + inc = true; } }else{ - Trace("fmf-incomplete") << "Incomplete because of integer quantification." << std::endl; - d_incomplete = true; + inc = true; } - }else if( tn.isReal() ){ - Trace("fmf-incomplete") << "Incomplete because of infinite type " << tn << std::endl; - d_incomplete = true; - //enumerate if the sort is reasonably small, the upper bound of 128 is chosen arbitrarily for now - }else if( tn.getCardinality().isFinite() && tn.getCardinality().getFiniteCardinality().toUnsignedInt()<=128 ){ + 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; + d_enum_type.push_back( ENUM_RANGE ); + }else{ + 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, the upper bound of 1000 is chosen arbitrarily for now + }else if( tn.getCardinality().isFinite() && tn.getCardinality().getFiniteCardinality().toUnsignedInt()<=1000 ){ d_rep_set->complete( tn ); }else{ - Trace("fmf-incomplete") << "Incomplete because of unknown type " << tn << std::endl; + Trace("fmf-incomplete") << "Incomplete because of quantification of type " << tn << std::endl; d_incomplete = true; } - if( !isSet ){ + if( d_enum_type.size()<=i ){ d_enum_type.push_back( ENUM_DOMAIN_ELEMENTS ); if( d_rep_set->hasType( tn ) ){ for( size_t j=0; j<d_rep_set->d_type_reps[tn].size(); j++ ){ @@ -182,7 +186,7 @@ bool RepSetIterator::initialize(){ } } } - //must set a variable index order + //must set a variable index order based on bounded integers if (d_owner.getKind()==FORALL && d_qe && d_qe->getBoundedIntegers()) { Trace("bound-int-rsi") << "Calculating variable order..." << std::endl; std::vector< int > varOrder; @@ -211,6 +215,7 @@ bool RepSetIterator::initialize(){ Trace("bound-int-rsi") << std::endl; setIndexOrder(indexOrder); } + //now reset the indices for (unsigned i=0; i<d_index.size(); i++) { if (!resetIndex(i, true)){ break; @@ -255,6 +260,19 @@ bool RepSetIterator::resetIndex( int i, bool initial ) { return false; }else{ Trace("bound-int-rsi") << "Can limit bounds of " << d_owner[0][ii] << " to " << l << "..." << u << std::endl; + for( unsigned b=0; b<2; b++ ){ + if( d_bounds[b].find(ii)!=d_bounds[b].end() ){ + Trace("bound-int-rsi") << "May further limit bound(" << b << ") based on " << d_bounds[b][ii] << std::endl; + if( b==0 && d_bounds[b][ii].getConst<Rational>() > l.getConst<Rational>() ){ + l = d_bounds[b][ii]; + }else if( b==1 && d_bounds[b][ii].getConst<Rational>() <= u.getConst<Rational>() ){ + u = NodeManager::currentNM()->mkNode( MINUS, d_bounds[b][ii], + NodeManager::currentNM()->mkConst( Rational(1) ) ); + u = Rewriter::rewrite( u ); + } + } + } + Node range = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MINUS, u, l ) ); Node ra = Rewriter::rewrite( NodeManager::currentNM()->mkNode( LEQ, range, NodeManager::currentNM()->mkConst( Rational( 9999 ) ) ) ); d_domain[ii].clear(); |