summaryrefslogtreecommitdiff
path: root/src/theory/rep_set.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/rep_set.cpp')
-rw-r--r--src/theory/rep_set.cpp283
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;
}
+
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback