diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-07-02 13:40:26 -0500 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-07-02 13:40:26 -0500 |
commit | f4d9d607c3a63a1b3842e291f06a621f71b0e966 (patch) | |
tree | 2b92548449e9aee333a2615cbe4e8f64eedb76f7 /src/theory/rep_set.cpp | |
parent | a23c5715ce7cd279d83e75b232fd24b5c53032ba (diff) |
Minor fixes for bounded integers, rewrite engine.
Diffstat (limited to 'src/theory/rep_set.cpp')
-rw-r--r-- | src/theory/rep_set.cpp | 32 |
1 files changed, 17 insertions, 15 deletions
diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp index b44cc6779..647ef965a 100644 --- a/src/theory/rep_set.cpp +++ b/src/theory/rep_set.cpp @@ -250,29 +250,31 @@ bool RepSetIterator::resetIndex( int i, bool initial ) { Trace("bound-int-rsi") << "Reset " << i << " " << ii << " " << initial << std::endl; //determine the current range if( d_enum_type[ii]==ENUM_RANGE ){ - if( initial || !d_qe->getBoundedIntegers()->isGroundRange( d_owner, d_owner[0][ii] ) ){ + if( initial || ( d_qe->getBoundedIntegers() && !d_qe->getBoundedIntegers()->isGroundRange( d_owner, d_owner[0][ii] ) ) ){ Trace("bound-int-rsi") << "Getting range of " << d_owner[0][ii] << std::endl; Node l, u; - d_qe->getBoundedIntegers()->getBoundValues( d_owner, d_owner[0][ii], this, l, u ); + if( d_qe->getBoundedIntegers() && d_qe->getBoundedIntegers()->isBoundVar( d_owner, d_owner[0][ii] ) ){ + d_qe->getBoundedIntegers()->getBoundValues( d_owner, d_owner[0][ii], this, l, u ); + } + 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 && (l.isNull() || d_bounds[b][ii].getConst<Rational>() > l.getConst<Rational>()) ){ + l = d_bounds[b][ii]; + }else if( b==1 && (u.isNull() || 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 ); + } + } + } + if( l.isNull() || u.isNull() ){ //failed, abort the iterator d_index.clear(); 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(); |