src/theory/rep_set.cpp

   1 /*********************                                                        */
   2 /*! \file rep_set.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Morgan Deters, Tim King
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory) and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief Implementation of representative set
  13  **/
  14
  15 #include "theory/rep_set.h"
  16 #include "theory/type_enumerator.h"
  17 #include "theory/quantifiers/bounded_integers.h"
  18 #include "theory/quantifiers/term_database.h"
  19 #include "theory/quantifiers/first_order_model.h"
  20
  21 using namespace std;
  22 using namespace CVC4;
  23 using namespace CVC4::kind;
  24 using namespace CVC4::context;
  25 using namespace CVC4::theory;
  26
  27 void RepSet::clear(){
  28   d_type_reps.clear();
  29   d_type_complete.clear();
  30   d_tmap.clear();
  31   d_values_to_terms.clear();
  32   d_type_rlv_rep.clear();
  33 }
  34
  35 bool RepSet::hasRep( TypeNode tn, Node n ) {
  36   std::map< TypeNode, std::vector< Node > >::iterator it = d_type_reps.find( tn );
  37   if( it==d_type_reps.end() ){
  38     return false;
  39   }else{
  40     return std::find( it->second.begin(), it->second.end(), n )!=it->second.end();
  41   }
  42 }
  43
  44 int RepSet::getNumRepresentatives( TypeNode tn ) const{
  45   std::map< TypeNode, std::vector< Node > >::const_iterator it = d_type_reps.find( tn );
  46   if( it!=d_type_reps.end() ){
  47     return (int)it->second.size();
  48   }else{
  49     return 0;
  50   }
  51 }
  52
  53 bool containsStoreAll( Node n, std::vector< Node >& cache ){
  54   if( std::find( cache.begin(), cache.end(), n )==cache.end() ){
  55     cache.push_back( n );
  56     if( n.getKind()==STORE_ALL ){
  57       return true;
  58     }else{
  59       for( unsigned i=0; i<n.getNumChildren(); i++ ){
  60         if( containsStoreAll( n[i], cache ) ){
  61           return true;
  62         }
  63       }
  64     }
  65   }
  66   return false;
  67 }
  68
  69 void RepSet::add( TypeNode tn, Node n ){
  70   //for now, do not add array constants FIXME
  71   if( tn.isArray() ){
  72     std::vector< Node > cache;
  73     if( containsStoreAll( n, cache ) ){
  74       return;
  75     }
  76   }
  77   Trace("rsi-debug") << "Add rep #" << d_type_reps[tn].size() << " for " << tn << " : " << n << std::endl;
  78   Assert( n.getType().isSubtypeOf( tn ) );
  79   d_tmap[ n ] = (int)d_type_reps[tn].size();
  80   d_type_reps[tn].push_back( n );
  81 }
  82
  83 int RepSet::getIndexFor( Node n ) const {
  84   std::map< Node, int >::const_iterator it = d_tmap.find( n );
  85   if( it!=d_tmap.end() ){
  86     return it->second;
  87   }else{
  88     return -1;
  89   }
  90 }
  91
  92 bool RepSet::complete( TypeNode t ){
  93   std::map< TypeNode, bool >::iterator it = d_type_complete.find( t );
  94   if( it==d_type_complete.end() ){
  95     //remove all previous
  96     for( unsigned i=0; i<d_type_reps[t].size(); i++ ){
  97       d_tmap.erase( d_type_reps[t][i] );
  98     }
  99     d_type_reps[t].clear();
 100     //now complete the type
 101     d_type_complete[t] = true;
 102     TypeEnumerator te(t);
 103     while( !te.isFinished() ){
 104       Node n = *te;
 105       if( std::find( d_type_reps[t].begin(), d_type_reps[t].end(), n )==d_type_reps[t].end() ){
 106         add( t, n );
 107       }
 108       ++te;
 109     }
 110     for( size_t i=0; i<d_type_reps[t].size(); i++ ){
 111       Trace("reps-complete") << d_type_reps[t][i] << " ";
 112     }
 113     Trace("reps-complete") << std::endl;
 114     return true;
 115   }else{
 116     return it->second;
 117   }
 118 }
 119
 120 int RepSet::getNumRelevantGroundReps( TypeNode t ) {
 121   std::map< TypeNode, int >::iterator it = d_type_rlv_rep.find( t );
 122   if( it==d_type_rlv_rep.end() ){
 123     return 0;
 124   }else{
 125     return it->second;
 126   }
 127 }
 128
 129 void RepSet::toStream(std::ostream& out){
 130 #if 0
 131   for( std::map< TypeNode, std::vector< Node > >::iterator it = d_type_reps.begin(); it != d_type_reps.end(); ++it ){
 132     out << it->first << " : " << std::endl;
 133     for( int i=0; i<(int)it->second.size(); i++ ){
 134       out << "   " << i << ": " << it->second[i] << std::endl;
 135     }
 136   }
 137 #else
 138   for( std::map< TypeNode, std::vector< Node > >::iterator it = d_type_reps.begin(); it != d_type_reps.end(); ++it ){
 139     if( !it->first.isFunction() && !it->first.isPredicate() ){
 140       out << "(" << it->first << " " << it->second.size();
 141       out << " (";
 142       for( int i=0; i<(int)it->second.size(); i++ ){
 143         if( i>0 ){ out << " "; }
 144         out << it->second[i];
 145       }
 146       out << ")";
 147       out << ")" << std::endl;
 148     }
 149   }
 150 #endif
 151 }
 152
 153
 154 RepSetIterator::RepSetIterator( QuantifiersEngine * qe, RepSet* rs ) : d_qe(qe), d_rep_set( rs ){
 155   d_incomplete = false;
 156 }
 157
 158 int RepSetIterator::domainSize( int i ) {
 159   Assert(i>=0);
 160   if( d_enum_type[i]==ENUM_DOMAIN_ELEMENTS ){
 161     return d_domain[i].size();
 162   }else{
 163     return d_domain[i][0];
 164   }
 165 }
 166
 167 bool RepSetIterator::setQuantifier( Node f ){
 168   Trace("rsi") << "Make rsi for " << f << std::endl;
 169   Assert( d_types.empty() );
 170   //store indicies
 171   for( size_t i=0; i<f[0].getNumChildren(); i++ ){
 172     d_types.push_back( f[0][i].getType() );
 173   }
 174   d_owner = f;
 175   return initialize();
 176 }
 177
 178 bool RepSetIterator::setFunctionDomain( Node op ){
 179   Trace("rsi") << "Make rsi for " << op << std::endl;
 180   Assert( d_types.empty() );
 181   TypeNode tn = op.getType();
 182   for( size_t i=0; i<tn.getNumChildren()-1; i++ ){
 183     d_types.push_back( tn[i] );
 184   }
 185   d_owner = op;
 186   return initialize();
 187 }
 188
 189 bool RepSetIterator::initialize(){
 190   Trace("rsi") << "Initialize rep set iterator..." << std::endl;
 191   for( size_t i=0; i<d_types.size(); i++ ){
 192     d_index.push_back( 0 );
 193     //store default index order
 194     d_index_order.push_back( i );
 195     d_var_order[i] = i;
 196     //store default domain
 197     d_domain.push_back( RepDomain() );
 198     TypeNode tn = d_types[i];
 199     Trace("rsi") << "Var #" << i << " is type " << tn << "..." << std::endl;
 200     if( tn.isSort() ){
 201       //must ensure uninterpreted type is non-empty.
 202       if( !d_rep_set->hasType( tn ) ){
 203         //FIXME:
 204         // terms in rep_set are now constants which mapped to terms through TheoryModel
 205         // thus, should introduce a constant and a term.  for now, just a term.
 206
 207         //Node c = d_qe->getTermDatabase()->getEnumerateTerm( tn, 0 );
 208         Node var = d_qe->getModel()->getSomeDomainElement( tn );
 209         Trace("mkVar") << "RepSetIterator:: Make variable " << var << " : " << tn << std::endl;
 210         d_rep_set->add( tn, var );
 211       }
 212     }else if( tn.isInteger() ){
 213       bool inc = false;
 214       //check if it is bound
 215       if( d_owner.getKind()==FORALL && d_qe && d_qe->getBoundedIntegers() ){
 216         if( d_qe->getBoundedIntegers()->isBoundVar( d_owner, d_owner[0][i] ) ){
 217           Trace("rsi") << "  variable is bounded integer." << std::endl;
 218           d_enum_type.push_back( ENUM_RANGE );
 219         }else{
 220           inc = true;
 221         }
 222       }else{
 223         inc = true;
 224       }
 225       if( inc ){
 226         //check if it is otherwise bound
 227         if( d_bounds[0].find(i)!=d_bounds[0].end() && d_bounds[1].find(i)!=d_bounds[1].end() ){
 228           Trace("rsi") << "  variable is bounded." << std::endl;
 229           d_enum_type.push_back( ENUM_RANGE );
 230         }else{
 231           Trace("rsi") << "  variable cannot be bounded." << std::endl;
 232           Trace("fmf-incomplete") << "Incomplete because of integer quantification of " << d_owner[0][i] << "." << std::endl;
 233           d_incomplete = true;
 234         }
 235       }
 236     //enumerate if the sort is reasonably small
 237     }else if( d_qe->getTermDatabase()->mayComplete( tn ) ){
 238       Trace("rsi") << "  do complete, since cardinality is small (" << tn.getCardinality() << ")..." << std::endl;
 239       d_rep_set->complete( tn );
 240       //must have succeeded
 241       Assert( d_rep_set->hasType( tn ) );
 242     }else{
 243       Trace("rsi") << "  variable cannot be bounded." << std::endl;
 244       Trace("fmf-incomplete") << "Incomplete because of quantification of type " << tn << std::endl;
 245       d_incomplete = true;
 246     }
 247     //if we have yet to determine the type of enumeration
 248     if( d_enum_type.size()<=i ){
 249       d_enum_type.push_back( ENUM_DOMAIN_ELEMENTS );
 250       if( d_rep_set->hasType( tn ) ){
 251         for( size_t j=0; j<d_rep_set->d_type_reps[tn].size(); j++ ){
 252           d_domain[i].push_back( j );
 253         }
 254       }else{
 255         return false;
 256       }
 257     }
 258   }
 259   //must set a variable index order based on bounded integers
 260   if (d_owner.getKind()==FORALL && d_qe && d_qe->getBoundedIntegers()) {
 261     Trace("bound-int-rsi") << "Calculating variable order..." << std::endl;
 262     std::vector< int > varOrder;
 263     for( unsigned i=0; i<d_qe->getBoundedIntegers()->getNumBoundVars(d_owner); i++ ){
 264       varOrder.push_back(d_qe->getBoundedIntegers()->getBoundVarNum(d_owner,i));
 265     }
 266     for( unsigned i=0; i<d_owner[0].getNumChildren(); i++) {
 267       if( !d_qe->getBoundedIntegers()->isBoundVar(d_owner, d_owner[0][i])) {
 268         varOrder.push_back(i);
 269       }
 270     }
 271     Trace("bound-int-rsi") << "Variable order : ";
 272     for( unsigned i=0; i<varOrder.size(); i++) {
 273       Trace("bound-int-rsi") << varOrder[i] << " ";
 274     }
 275     Trace("bound-int-rsi") << std::endl;
 276     std::vector< int > indexOrder;
 277     indexOrder.resize(varOrder.size());
 278     for( unsigned i=0; i<varOrder.size(); i++){
 279       indexOrder[varOrder[i]] = i;
 280     }
 281     Trace("bound-int-rsi") << "Will use index order : ";
 282     for( unsigned i=0; i<indexOrder.size(); i++) {
 283       Trace("bound-int-rsi") << indexOrder[i] << " ";
 284     }
 285     Trace("bound-int-rsi") << std::endl;
 286     setIndexOrder(indexOrder);
 287   }
 288   //now reset the indices
 289   for (unsigned i=0; i<d_index.size(); i++) {
 290     if (!resetIndex(i, true)){
 291       break;
 292     }
 293   }
 294   return true;
 295 }
 296
 297 void RepSetIterator::setIndexOrder( std::vector< int >& indexOrder ){
 298   d_index_order.clear();
 299   d_index_order.insert( d_index_order.begin(), indexOrder.begin(), indexOrder.end() );
 300   //make the d_var_order mapping
 301   for( int i=0; i<(int)d_index_order.size(); i++ ){
 302     d_var_order[d_index_order[i]] = i;
 303   }
 304 }
 305 /*
 306 void RepSetIterator::setDomain( std::vector< RepDomain >& domain ){
 307   d_domain.clear();
 308   d_domain.insert( d_domain.begin(), domain.begin(), domain.end() );
 309   //we are done if a domain is empty
 310   for( int i=0; i<(int)d_domain.size(); i++ ){
 311     if( d_domain[i].empty() ){
 312       d_index.clear();
 313     }
 314   }
 315 }
 316 */
 317 bool RepSetIterator::resetIndex( int i, bool initial ) {
 318   d_index[i] = 0;
 319   int ii = d_index_order[i];
 320   Trace("bound-int-rsi") << "Reset " << i << " " << ii << " " << initial << std::endl;
 321   //determine the current range
 322   if( d_enum_type[ii]==ENUM_RANGE ){
 323     if( initial || ( d_qe->getBoundedIntegers() && !d_qe->getBoundedIntegers()->isGroundRange( d_owner, d_owner[0][ii] ) ) ){
 324       Trace("bound-int-rsi") << "Getting range of " << d_owner[0][ii] << std::endl;
 325       Node actual_l;
 326       Node l, u;
 327       if( d_qe->getBoundedIntegers() && d_qe->getBoundedIntegers()->isBoundVar( d_owner, d_owner[0][ii] ) ){
 328         d_qe->getBoundedIntegers()->getBoundValues( d_owner, d_owner[0][ii], this, l, u );
 329       }
 330       for( unsigned b=0; b<2; b++ ){
 331         if( d_bounds[b].find(ii)!=d_bounds[b].end() ){
 332           Trace("bound-int-rsi") << "May further limit bound(" << b << ") based on " << d_bounds[b][ii] << std::endl;
 333           if( b==0 && (l.isNull() || d_bounds[b][ii].getConst<Rational>() > l.getConst<Rational>()) ){
 334             if( !l.isNull() ){
 335               //bound was limited externally, record that the value lower bound is not equal to the term lower bound
 336               actual_l = NodeManager::currentNM()->mkNode( MINUS, d_bounds[b][ii], l );
 337             }
 338             l = d_bounds[b][ii];
 339           }else if( b==1 && (u.isNull() || d_bounds[b][ii].getConst<Rational>() <= u.getConst<Rational>()) ){
 340             u = NodeManager::currentNM()->mkNode( MINUS, d_bounds[b][ii],
 341                                                   NodeManager::currentNM()->mkConst( Rational(1) ) );
 342             u = Rewriter::rewrite( u );
 343           }
 344         }
 345       }
 346
 347       if( l.isNull() || u.isNull() ){
 348         //failed, abort the iterator
 349         d_index.clear();
 350         return false;
 351       }else{
 352         Trace("bound-int-rsi") << "Can limit bounds of " << d_owner[0][ii] << " to " << l << "..." << u << std::endl;
 353         Node range = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MINUS, u, l ) );
 354         Node ra = Rewriter::rewrite( NodeManager::currentNM()->mkNode( LEQ, range, NodeManager::currentNM()->mkConst( Rational( 9999 ) ) ) );
 355         d_domain[ii].clear();
 356         Node tl = l;
 357         Node tu = u;
 358         if( d_qe->getBoundedIntegers() && d_qe->getBoundedIntegers()->isBoundVar( d_owner, d_owner[0][ii] ) ){
 359           d_qe->getBoundedIntegers()->getBounds( d_owner, d_owner[0][ii], this, tl, tu );
 360         }
 361         d_lower_bounds[ii] = tl;
 362         if( !actual_l.isNull() ){
 363           //if bound was limited externally, must consider the offset
 364           d_lower_bounds[ii] = Rewriter::rewrite( NodeManager::currentNM()->mkNode( PLUS, tl, actual_l ) );
 365         }
 366         if( ra==NodeManager::currentNM()->mkConst(true) ){
 367           long rr = range.getConst<Rational>().getNumerator().getLong()+1;
 368           Trace("bound-int-rsi")  << "Actual bound range is " << rr << std::endl;
 369           d_domain[ii].push_back( (int)rr );
 370         }else{
 371           Trace("fmf-incomplete") << "Incomplete because of integer quantification, bounds are too big for " << d_owner[0][ii] << "." << std::endl;
 372           d_incomplete = true;
 373           d_domain[ii].push_back( 0 );
 374         }
 375       }
 376     }else{
 377       Trace("bound-int-rsi") << d_owner[0][ii] << " has ground range, skip." << std::endl;
 378     }
 379   }
 380   return true;
 381 }
 382
 383 int RepSetIterator::increment2( int counter ){
 384   Assert( !isFinished() );
 385 #ifdef DISABLE_EVAL_SKIP_MULTIPLE
 386   counter = (int)d_index.size()-1;
 387 #endif
 388   //increment d_index
 389   if( counter>=0){
 390     Trace("rsi-debug") << "domain size of " << counter << " is " << domainSize(counter) << std::endl;
 391   }
 392   while( counter>=0 && d_index[counter]>=(int)(domainSize(counter)-1) ){
 393     counter--;
 394     if( counter>=0){
 395       Trace("rsi-debug") << "domain size of " << counter << " is " << domainSize(counter) << std::endl;
 396     }
 397   }
 398   if( counter==-1 ){
 399     d_index.clear();
 400   }else{
 401     d_index[counter]++;
 402     bool emptyDomain = false;
 403     for( int i=(int)d_index.size()-1; i>counter; i-- ){
 404       if (!resetIndex(i)){
 405         break;
 406       }else if( domainSize(i)<=0 ){
 407         emptyDomain = true;
 408       }
 409     }
 410     if( emptyDomain ){
 411       Trace("rsi-debug") << "This is an empty domain, increment again." << std::endl;
 412       return increment();
 413     }
 414   }
 415   return counter;
 416 }
 417
 418 int RepSetIterator::increment(){
 419   if( !isFinished() ){
 420     return increment2( (int)d_index.size()-1 );
 421   }else{
 422     return -1;
 423   }
 424 }
 425
 426 bool RepSetIterator::isFinished(){
 427   return d_index.empty();
 428 }
 429
 430 Node RepSetIterator::getTerm( int i ){
 431   Trace("rsi-debug") << "rsi : get term " << i << ", index order = " << d_index_order[i] << std::endl;
 432   //int index = d_index_order[i];
 433   int index = i;
 434   if( d_enum_type[index]==ENUM_DOMAIN_ELEMENTS ){
 435     TypeNode tn = d_types[index];
 436     Assert( d_rep_set->d_type_reps.find( tn )!=d_rep_set->d_type_reps.end() );
 437     return d_rep_set->d_type_reps[tn][d_domain[index][d_index[index]]];
 438   }else{
 439     Trace("rsi-debug") << "Get, with offset : " << index << " " << d_lower_bounds[index] << " " << d_index[index] << std::endl;
 440     Node t = NodeManager::currentNM()->mkNode(PLUS, d_lower_bounds[index],
 441                                                     NodeManager::currentNM()->mkConst( Rational(d_index[index]) ) );
 442     t = Rewriter::rewrite( t );
 443     return t;
 444   }
 445 }
 446
 447 void RepSetIterator::debugPrint( const char* c ){
 448   for( int i=0; i<(int)d_index.size(); i++ ){
 449     Debug( c ) << i << " : " << d_index[i] << " : " << getTerm( i ) << std::endl;
 450   }
 451 }
 452
 453 void RepSetIterator::debugPrintSmall( const char* c ){
 454   Debug( c ) << "RI: ";
 455   for( int i=0; i<(int)d_index.size(); i++ ){
 456     Debug( c ) << d_index[i] << ": " << getTerm( i ) << " ";
 457   }
 458   Debug( c ) << std::endl;
 459 }