diff options
Diffstat (limited to 'src/theory/rep_set.cpp')
-rw-r--r-- | src/theory/rep_set.cpp | 283 |
1 files changed, 153 insertions, 130 deletions
diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp index d7178a8c1..184553ba7 100644 --- a/src/theory/rep_set.cpp +++ b/src/theory/rep_set.cpp @@ -127,19 +127,11 @@ int RepSet::getNumRelevantGroundReps( TypeNode t ) { } void RepSet::toStream(std::ostream& out){ -#if 0 - for( std::map< TypeNode, std::vector< Node > >::iterator it = d_type_reps.begin(); it != d_type_reps.end(); ++it ){ - out << it->first << " : " << std::endl; - for( int i=0; i<(int)it->second.size(); i++ ){ - out << " " << i << ": " << it->second[i] << std::endl; - } - } -#else for( std::map< TypeNode, std::vector< Node > >::iterator it = d_type_reps.begin(); it != d_type_reps.end(); ++it ){ if( !it->first.isFunction() && !it->first.isPredicate() ){ out << "(" << it->first << " " << it->second.size(); out << " ("; - for( int i=0; i<(int)it->second.size(); i++ ){ + for( unsigned i=0; i<it->second.size(); i++ ){ if( i>0 ){ out << " "; } out << it->second[i]; } @@ -147,7 +139,6 @@ void RepSet::toStream(std::ostream& out){ out << ")" << std::endl; } } -#endif } @@ -157,10 +148,11 @@ RepSetIterator::RepSetIterator( QuantifiersEngine * qe, RepSet* rs ) : d_qe(qe), int RepSetIterator::domainSize( int i ) { Assert(i>=0); - if( d_enum_type[i]==ENUM_DOMAIN_ELEMENTS ){ - return d_domain[i].size(); + int v = d_var_order[i]; + if( d_enum_type[v]==ENUM_DOMAIN_ELEMENTS ){ + return d_domain[v].size(); }else{ - return d_domain[i][0]; + return d_domain[v][0]; } } @@ -188,15 +180,15 @@ 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++ ){ + for( unsigned v=0; v<d_types.size(); v++ ){ d_index.push_back( 0 ); //store default index order - d_index_order.push_back( i ); - d_var_order[i] = i; + d_index_order.push_back( v ); + d_var_order[v] = v; //store default domain d_domain.push_back( RepDomain() ); - TypeNode tn = d_types[i]; - Trace("rsi") << "Var #" << i << " is type " << tn << "..." << std::endl; + TypeNode tn = d_types[v]; + Trace("rsi") << "Var #" << v << " is type " << tn << "..." << std::endl; if( tn.isSort() ){ //must ensure uninterpreted type is non-empty. if( !d_rep_set->hasType( tn ) ){ @@ -209,59 +201,59 @@ bool RepSetIterator::initialize(){ Trace("mkVar") << "RepSetIterator:: Make variable " << var << " : " << tn << std::endl; d_rep_set->add( tn, var ); } - }else if( tn.isInteger() ){ - bool inc = false; - //check if it is bound + }else{ + bool inc = true; + //check if it is bound by bounded integer module if( d_owner.getKind()==FORALL && d_qe && d_qe->getBoundedIntegers() ){ - if( d_qe->getBoundedIntegers()->isBoundVar( d_owner, d_owner[0][i] ) ){ + unsigned bvt = d_qe->getBoundedIntegers()->getBoundVarType( d_owner, d_owner[0][v] ); + if( bvt==quantifiers::BoundedIntegers::BOUND_INT_RANGE ){ Trace("rsi") << " variable is bounded integer." << std::endl; - d_enum_type.push_back( ENUM_RANGE ); - }else{ - inc = true; + d_enum_type.push_back( ENUM_INT_RANGE ); + inc = false; + }else if( bvt==quantifiers::BoundedIntegers::BOUND_SET_MEMBER ){ + Trace("rsi") << " variable is bounded by set membership." << std::endl; + d_enum_type.push_back( ENUM_SET_MEMBERS ); + inc = false; } - }else{ - inc = true; } 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() ){ + if( d_bounds[0].find( v )!=d_bounds[0].end() && d_bounds[1].find( v )!=d_bounds[1].end() ){ Trace("rsi") << " variable is bounded." << std::endl; - d_enum_type.push_back( ENUM_RANGE ); + d_enum_type.push_back( ENUM_INT_RANGE ); + }else if( d_qe->getTermDatabase()->mayComplete( tn ) ){ + Trace("rsi") << " do complete, since cardinality is small (" << tn.getCardinality() << ")..." << std::endl; + d_rep_set->complete( tn ); + //must have succeeded + Assert( d_rep_set->hasType( tn ) ); }else{ Trace("rsi") << " variable cannot be bounded." << std::endl; - Trace("fmf-incomplete") << "Incomplete because of integer quantification of " << d_owner[0][i] << "." << std::endl; + Trace("fmf-incomplete") << "Incomplete because of quantification of type " << tn << std::endl; d_incomplete = true; } } - //enumerate if the sort is reasonably small - }else if( d_qe->getTermDatabase()->mayComplete( tn ) ){ - Trace("rsi") << " do complete, since cardinality is small (" << tn.getCardinality() << ")..." << std::endl; - d_rep_set->complete( tn ); - //must have succeeded - Assert( d_rep_set->hasType( 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; } //if we have yet to determine the type of enumeration - if( d_enum_type.size()<=i ){ + if( d_enum_type.size()<=v ){ 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++ ){ - d_domain[i].push_back( j ); + for( unsigned j=0; j<d_rep_set->d_type_reps[tn].size(); j++ ){ + d_domain[v].push_back( j ); } }else{ + Assert( d_incomplete ); return false; } } } //must set a variable index order based on bounded integers - if (d_owner.getKind()==FORALL && d_qe && d_qe->getBoundedIntegers()) { + if( d_owner.getKind()==FORALL && d_qe && d_qe->getBoundedIntegers() ){ Trace("bound-int-rsi") << "Calculating variable order..." << std::endl; std::vector< int > varOrder; - for( unsigned i=0; i<d_qe->getBoundedIntegers()->getNumBoundVars(d_owner); i++ ){ - varOrder.push_back(d_qe->getBoundedIntegers()->getBoundVarNum(d_owner,i)); + for( unsigned i=0; i<d_qe->getBoundedIntegers()->getNumBoundVars( d_owner ); i++ ){ + Node v = d_qe->getBoundedIntegers()->getBoundVar( d_owner, i ); + Trace("bound-int-rsi") << " bound var #" << i << " is " << v << std::endl; + varOrder.push_back( d_qe->getTermDatabase()->getVariableNum( d_owner, v ) ); } for( unsigned i=0; i<d_owner[0].getNumChildren(); i++) { if( !d_qe->getBoundedIntegers()->isBoundVar(d_owner, d_owner[0][i])) { @@ -283,14 +275,10 @@ bool RepSetIterator::initialize(){ Trace("bound-int-rsi") << indexOrder[i] << " "; } Trace("bound-int-rsi") << std::endl; - setIndexOrder(indexOrder); + setIndexOrder( indexOrder ); } //now reset the indices - for (unsigned i=0; i<d_index.size(); i++) { - if (!resetIndex(i, true)){ - break; - } - } + do_reset_increment( -1, true ); return true; } @@ -298,46 +286,40 @@ void RepSetIterator::setIndexOrder( std::vector< int >& indexOrder ){ d_index_order.clear(); d_index_order.insert( d_index_order.begin(), indexOrder.begin(), indexOrder.end() ); //make the d_var_order mapping - for( int i=0; i<(int)d_index_order.size(); i++ ){ + for( unsigned i=0; i<d_index_order.size(); i++ ){ d_var_order[d_index_order[i]] = i; } } -/* -void RepSetIterator::setDomain( std::vector< RepDomain >& domain ){ - d_domain.clear(); - d_domain.insert( d_domain.begin(), domain.begin(), domain.end() ); - //we are done if a domain is empty - for( int i=0; i<(int)d_domain.size(); i++ ){ - if( d_domain[i].empty() ){ - d_index.clear(); - } - } -} -*/ -bool RepSetIterator::resetIndex( int i, bool initial ) { + +int RepSetIterator::resetIndex( int i, bool initial ) { d_index[i] = 0; - int ii = d_index_order[i]; - Trace("bound-int-rsi") << "Reset " << i << " " << ii << " " << initial << std::endl; + int v = d_var_order[i]; + Trace("bound-int-rsi") << "Reset " << i << ", var order = " << v << ", initial = " << initial << std::endl; //determine the current range - if( d_enum_type[ii]==ENUM_RANGE ){ - 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; + if( initial || ( d_owner.getKind()==FORALL && d_qe && d_qe->getBoundedIntegers() && + d_qe->getBoundedIntegers()->isBoundVar( d_owner, d_owner[0][v] ) && + !d_qe->getBoundedIntegers()->isGroundRange( d_owner, d_owner[0][v] ) ) ){ + Trace("bound-int-rsi") << "Getting range of " << d_owner[0][v] << std::endl; + if( d_enum_type[v]==ENUM_INT_RANGE ){ Node actual_l; Node 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 ); + if( d_qe->getBoundedIntegers() ){ + unsigned bvt = d_qe->getBoundedIntegers()->getBoundVarType( d_owner, d_owner[0][v] ); + if( bvt==quantifiers::BoundedIntegers::BOUND_INT_RANGE ){ + d_qe->getBoundedIntegers()->getBoundValues( d_owner, d_owner[0][v], 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>()) ){ + if( d_bounds[b].find(v)!=d_bounds[b].end() ){ + Trace("bound-int-rsi") << "May further limit bound(" << b << ") based on " << d_bounds[b][v] << std::endl; + if( b==0 && (l.isNull() || d_bounds[b][v].getConst<Rational>() > l.getConst<Rational>()) ){ if( !l.isNull() ){ //bound was limited externally, record that the value lower bound is not equal to the term lower bound - actual_l = NodeManager::currentNM()->mkNode( MINUS, d_bounds[b][ii], l ); + actual_l = NodeManager::currentNM()->mkNode( MINUS, d_bounds[b][v], l ); } - 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], + l = d_bounds[b][v]; + }else if( b==1 && (u.isNull() || d_bounds[b][v].getConst<Rational>() <= u.getConst<Rational>()) ){ + u = NodeManager::currentNM()->mkNode( MINUS, d_bounds[b][v], NodeManager::currentNM()->mkConst( Rational(1) ) ); u = Rewriter::rewrite( u ); } @@ -346,73 +328,109 @@ bool RepSetIterator::resetIndex( int i, bool initial ) { if( l.isNull() || u.isNull() ){ //failed, abort the iterator - d_index.clear(); - return false; + return -1; }else{ - Trace("bound-int-rsi") << "Can limit bounds of " << d_owner[0][ii] << " to " << l << "..." << u << std::endl; + Trace("bound-int-rsi") << "Can limit bounds of " << d_owner[0][v] << " to " << l << "..." << u << std::endl; 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(); + d_domain[v].clear(); Node tl = l; Node tu = u; - if( d_qe->getBoundedIntegers() && d_qe->getBoundedIntegers()->isBoundVar( d_owner, d_owner[0][ii] ) ){ - d_qe->getBoundedIntegers()->getBounds( d_owner, d_owner[0][ii], this, tl, tu ); + if( d_qe->getBoundedIntegers() && d_qe->getBoundedIntegers()->isBoundVar( d_owner, d_owner[0][v] ) ){ + d_qe->getBoundedIntegers()->getBounds( d_owner, d_owner[0][v], this, tl, tu ); } - d_lower_bounds[ii] = tl; + d_lower_bounds[v] = tl; if( !actual_l.isNull() ){ //if bound was limited externally, must consider the offset - d_lower_bounds[ii] = Rewriter::rewrite( NodeManager::currentNM()->mkNode( PLUS, tl, actual_l ) ); + d_lower_bounds[v] = Rewriter::rewrite( NodeManager::currentNM()->mkNode( PLUS, tl, actual_l ) ); } - if( ra==NodeManager::currentNM()->mkConst(true) ){ + if( ra==d_qe->getTermDatabase()->d_true ){ long rr = range.getConst<Rational>().getNumerator().getLong()+1; Trace("bound-int-rsi") << "Actual bound range is " << rr << std::endl; - d_domain[ii].push_back( (int)rr ); + d_domain[v].push_back( (int)rr ); + if( rr<=0 ){ + return 0; + } }else{ - Trace("fmf-incomplete") << "Incomplete because of integer quantification, bounds are too big for " << d_owner[0][ii] << "." << std::endl; - d_incomplete = true; - d_domain[ii].push_back( 0 ); + Trace("fmf-incomplete") << "Incomplete because of integer quantification, bounds are too big for " << d_owner[0][v] << "." << std::endl; + return -1; } } - }else{ - Trace("bound-int-rsi") << d_owner[0][ii] << " has ground range, skip." << std::endl; + }else if( d_enum_type[v]==ENUM_SET_MEMBERS ){ + Assert( d_qe->getBoundedIntegers()->getBoundVarType( d_owner, d_owner[0][v] )==quantifiers::BoundedIntegers::BOUND_SET_MEMBER ); + Node srv = d_qe->getBoundedIntegers()->getSetRangeValue( d_owner, d_owner[0][v], this ); + if( srv.isNull() ){ + return -1; + } + Trace("bound-int-rsi") << "Bounded by set membership : " << srv << std::endl; + d_domain[v].clear(); + d_setm_bounds[v].clear(); + if( srv.getKind()!=EMPTYSET ){ + //TODO: need term model, not value model + while( srv.getKind()==UNION ){ + Assert( srv[1].getKind()==kind::SINGLETON ); + d_setm_bounds[v].push_back( srv[1][0] ); + srv = srv[0]; + } + d_setm_bounds[v].push_back( srv[0] ); + d_domain[v].push_back( d_setm_bounds[v].size() ); + }else{ + d_domain[v].push_back( 0 ); + return 0; + } } } - return true; + return 1; } -int RepSetIterator::increment2( int counter ){ +int RepSetIterator::increment2( int i ){ Assert( !isFinished() ); #ifdef DISABLE_EVAL_SKIP_MULTIPLE - counter = (int)d_index.size()-1; + i = (int)d_index.size()-1; #endif //increment d_index - if( counter>=0){ - Trace("rsi-debug") << "domain size of " << counter << " is " << domainSize(counter) << std::endl; + if( i>=0){ + Trace("rsi-debug") << "domain size of " << i << " is " << domainSize(i) << std::endl; } - while( counter>=0 && d_index[counter]>=(int)(domainSize(counter)-1) ){ - counter--; - if( counter>=0){ - Trace("rsi-debug") << "domain size of " << counter << " is " << domainSize(counter) << std::endl; + while( i>=0 && d_index[i]>=(int)(domainSize(i)-1) ){ + i--; + if( i>=0){ + Trace("rsi-debug") << "domain size of " << i << " is " << domainSize(i) << std::endl; } } - if( counter==-1 ){ + if( i==-1 ){ d_index.clear(); + return -1; }else{ - d_index[counter]++; - bool emptyDomain = false; - for( int i=(int)d_index.size()-1; i>counter; i-- ){ - if (!resetIndex(i)){ - break; - }else if( domainSize(i)<=0 ){ - emptyDomain = true; - } + Trace("rsi-debug") << "increment " << i << std::endl; + d_index[i]++; + return do_reset_increment( i ); + } +} + +int RepSetIterator::do_reset_increment( int i, bool initial ) { + bool emptyDomain = false; + for( unsigned ii=(i+1); ii<d_index.size(); ii++ ){ + int ri_res = resetIndex( ii, initial ); + if( ri_res==-1 ){ + //failed + d_index.clear(); + d_incomplete = true; + break; + }else if( ri_res==0 ){ + emptyDomain = true; } + //force next iteration if currently an empty domain if( emptyDomain ){ - Trace("rsi-debug") << "This is an empty domain, increment again." << std::endl; - return increment(); + d_index[ii] = domainSize(ii)-1; } } - return counter; + if( emptyDomain ){ + Trace("rsi-debug") << "This is an empty domain, increment." << std::endl; + return increment(); + }else{ + return i; + } } int RepSetIterator::increment(){ @@ -427,33 +445,38 @@ bool RepSetIterator::isFinished(){ return d_index.empty(); } -Node RepSetIterator::getTerm( int i ){ - Trace("rsi-debug") << "rsi : get term " << i << ", index order = " << d_index_order[i] << std::endl; - //int index = d_index_order[i]; - int index = i; - if( d_enum_type[index]==ENUM_DOMAIN_ELEMENTS ){ - TypeNode tn = d_types[index]; +Node RepSetIterator::getCurrentTerm( int v ){ + Trace("rsi-debug") << "rsi : get term " << v << ", index order = " << d_index_order[v] << std::endl; + int ii = d_index_order[v]; + int curr = d_index[ii]; + if( d_enum_type[v]==ENUM_DOMAIN_ELEMENTS ){ + TypeNode tn = d_types[v]; Assert( d_rep_set->d_type_reps.find( tn )!=d_rep_set->d_type_reps.end() ); - return d_rep_set->d_type_reps[tn][d_domain[index][d_index[index]]]; + Assert( 0<=d_domain[v][curr] && d_domain[v][curr]<(int)d_rep_set->d_type_reps[tn].size() ); + return d_rep_set->d_type_reps[tn][d_domain[v][curr]]; + }else if( d_enum_type[v]==ENUM_SET_MEMBERS ){ + Assert( 0<=curr && curr<(int)d_setm_bounds[v].size() ); + return d_setm_bounds[v][curr]; }else{ - Trace("rsi-debug") << "Get, with offset : " << index << " " << d_lower_bounds[index] << " " << d_index[index] << std::endl; - Node t = NodeManager::currentNM()->mkNode(PLUS, d_lower_bounds[index], - NodeManager::currentNM()->mkConst( Rational(d_index[index]) ) ); + Trace("rsi-debug") << "Get, with offset : " << v << " " << d_lower_bounds[v] << " " << curr << std::endl; + Assert( !d_lower_bounds[v].isNull() ); + Node t = NodeManager::currentNM()->mkNode(PLUS, d_lower_bounds[v], NodeManager::currentNM()->mkConst( Rational(curr) ) ); t = Rewriter::rewrite( t ); return t; } } void RepSetIterator::debugPrint( const char* c ){ - for( int i=0; i<(int)d_index.size(); i++ ){ - Debug( c ) << i << " : " << d_index[i] << " : " << getTerm( i ) << std::endl; + for( unsigned v=0; v<d_index.size(); v++ ){ + Debug( c ) << v << " : " << getCurrentTerm( v ) << std::endl; } } void RepSetIterator::debugPrintSmall( const char* c ){ Debug( c ) << "RI: "; - for( int i=0; i<(int)d_index.size(); i++ ){ - Debug( c ) << d_index[i] << ": " << getTerm( i ) << " "; + for( unsigned v=0; v<d_index.size(); v++ ){ + Debug( c ) << v << ": " << getCurrentTerm( v ) << " "; } Debug( c ) << std::endl; } + |