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   for( std::map< TypeNode, std::vector< Node > >::iterator it = d_type_reps.begin(); it != d_type_reps.end(); ++it ){
 131     if( !it->first.isFunction() && !it->first.isPredicate() ){
 132       out << "(" << it->first << " " << it->second.size();
 133       out << " (";
 134       for( unsigned i=0; i<it->second.size(); i++ ){
 135         if( i>0 ){ out << " "; }
 136         out << it->second[i];
 137       }
 138       out << ")";
 139       out << ")" << std::endl;
 140     }
 141   }
 142 }
 143
 144
 145 RepSetIterator::RepSetIterator( QuantifiersEngine * qe, RepSet* rs ) : d_qe(qe), d_rep_set( rs ){
 146   d_incomplete = false;
 147 }
 148
 149 int RepSetIterator::domainSize( int i ) {
 150   Assert(i>=0);
 151   int v = d_var_order[i];
 152   if( d_enum_type[v]==ENUM_DOMAIN_ELEMENTS ){
 153     return d_domain[v].size();
 154   }else{
 155     return d_domain[v][0];
 156   }
 157 }
 158
 159 bool RepSetIterator::setQuantifier( Node f ){
 160   Trace("rsi") << "Make rsi for " << f << std::endl;
 161   Assert( d_types.empty() );
 162   //store indicies
 163   for( size_t i=0; i<f[0].getNumChildren(); i++ ){
 164     d_types.push_back( f[0][i].getType() );
 165   }
 166   d_owner = f;
 167   return initialize();
 168 }
 169
 170 bool RepSetIterator::setFunctionDomain( Node op ){
 171   Trace("rsi") << "Make rsi for " << op << std::endl;
 172   Assert( d_types.empty() );
 173   TypeNode tn = op.getType();
 174   for( size_t i=0; i<tn.getNumChildren()-1; i++ ){
 175     d_types.push_back( tn[i] );
 176   }
 177   d_owner = op;
 178   return initialize();
 179 }
 180
 181 bool RepSetIterator::initialize(){
 182   Trace("rsi") << "Initialize rep set iterator..." << std::endl;
 183   for( unsigned v=0; v<d_types.size(); v++ ){
 184     d_index.push_back( 0 );
 185     //store default index order
 186     d_index_order.push_back( v );
 187     d_var_order[v] = v;
 188     //store default domain
 189     d_domain.push_back( RepDomain() );
 190     TypeNode tn = d_types[v];
 191     Trace("rsi") << "Var #" << v << " is type " << tn << "..." << std::endl;
 192     if( tn.isSort() ){
 193       //must ensure uninterpreted type is non-empty.
 194       if( !d_rep_set->hasType( tn ) ){
 195         //FIXME:
 196         // terms in rep_set are now constants which mapped to terms through TheoryModel
 197         // thus, should introduce a constant and a term.  for now, just a term.
 198
 199         //Node c = d_qe->getTermDatabase()->getEnumerateTerm( tn, 0 );
 200         Node var = d_qe->getModel()->getSomeDomainElement( tn );
 201         Trace("mkVar") << "RepSetIterator:: Make variable " << var << " : " << tn << std::endl;
 202         d_rep_set->add( tn, var );
 203       }
 204     }else{
 205       bool inc = true;
 206       //check if it is bound by bounded integer module
 207       if( d_owner.getKind()==FORALL && d_qe && d_qe->getBoundedIntegers() ){
 208         unsigned bvt = d_qe->getBoundedIntegers()->getBoundVarType( d_owner, d_owner[0][v] );
 209         if( bvt==quantifiers::BoundedIntegers::BOUND_INT_RANGE ){
 210           Trace("rsi") << "  variable is bounded integer." << std::endl;
 211           d_enum_type.push_back( ENUM_INT_RANGE );
 212           inc = false;
 213         }else if( bvt==quantifiers::BoundedIntegers::BOUND_SET_MEMBER ){
 214           Trace("rsi") << "  variable is bounded by set membership." << std::endl;
 215           d_enum_type.push_back( ENUM_SET_MEMBERS );
 216           inc = false;
 217         }
 218       }
 219       if( inc ){
 220         //check if it is otherwise bound
 221         if( d_bounds[0].find( v )!=d_bounds[0].end() && d_bounds[1].find( v )!=d_bounds[1].end() ){
 222           Trace("rsi") << "  variable is bounded." << std::endl;
 223           d_enum_type.push_back( ENUM_INT_RANGE );
 224         }else if( d_qe->getTermDatabase()->mayComplete( tn ) ){
 225           Trace("rsi") << "  do complete, since cardinality is small (" << tn.getCardinality() << ")..." << std::endl;
 226           d_rep_set->complete( tn );
 227           //must have succeeded
 228           Assert( d_rep_set->hasType( tn ) );
 229         }else{
 230           Trace("rsi") << "  variable cannot be bounded." << std::endl;
 231           Trace("fmf-incomplete") << "Incomplete because of quantification of type " << tn << std::endl;
 232           d_incomplete = true;
 233         }
 234       }
 235     }
 236     //if we have yet to determine the type of enumeration
 237     if( d_enum_type.size()<=v ){
 238       d_enum_type.push_back( ENUM_DOMAIN_ELEMENTS );
 239       if( d_rep_set->hasType( tn ) ){
 240         for( unsigned j=0; j<d_rep_set->d_type_reps[tn].size(); j++ ){
 241           d_domain[v].push_back( j );
 242         }
 243       }else{
 244         Assert( d_incomplete );
 245         return false;
 246       }
 247     }
 248   }
 249   //must set a variable index order based on bounded integers
 250   if( d_owner.getKind()==FORALL && d_qe && d_qe->getBoundedIntegers() ){
 251     Trace("bound-int-rsi") << "Calculating variable order..." << std::endl;
 252     std::vector< int > varOrder;
 253     for( unsigned i=0; i<d_qe->getBoundedIntegers()->getNumBoundVars( d_owner ); i++ ){
 254       Node v = d_qe->getBoundedIntegers()->getBoundVar( d_owner, i );
 255       Trace("bound-int-rsi") << "  bound var #" << i << " is " << v << std::endl;
 256       varOrder.push_back( d_qe->getTermDatabase()->getVariableNum( d_owner, v ) );
 257     }
 258     for( unsigned i=0; i<d_owner[0].getNumChildren(); i++) {
 259       if( !d_qe->getBoundedIntegers()->isBoundVar(d_owner, d_owner[0][i])) {
 260         varOrder.push_back(i);
 261       }
 262     }
 263     Trace("bound-int-rsi") << "Variable order : ";
 264     for( unsigned i=0; i<varOrder.size(); i++) {
 265       Trace("bound-int-rsi") << varOrder[i] << " ";
 266     }
 267     Trace("bound-int-rsi") << std::endl;
 268     std::vector< int > indexOrder;
 269     indexOrder.resize(varOrder.size());
 270     for( unsigned i=0; i<varOrder.size(); i++){
 271       indexOrder[varOrder[i]] = i;
 272     }
 273     Trace("bound-int-rsi") << "Will use index order : ";
 274     for( unsigned i=0; i<indexOrder.size(); i++) {
 275       Trace("bound-int-rsi") << indexOrder[i] << " ";
 276     }
 277     Trace("bound-int-rsi") << std::endl;
 278     setIndexOrder( indexOrder );
 279   }
 280   //now reset the indices
 281   do_reset_increment( -1, true );
 282   return true;
 283 }
 284
 285 void RepSetIterator::setIndexOrder( std::vector< int >& indexOrder ){
 286   d_index_order.clear();
 287   d_index_order.insert( d_index_order.begin(), indexOrder.begin(), indexOrder.end() );
 288   //make the d_var_order mapping
 289   for( unsigned i=0; i<d_index_order.size(); i++ ){
 290     d_var_order[d_index_order[i]] = i;
 291   }
 292 }
 293
 294 int RepSetIterator::resetIndex( int i, bool initial ) {
 295   d_index[i] = 0;
 296   int v = d_var_order[i];
 297   Trace("bound-int-rsi") << "Reset " << i << ", var order = " << v << ", initial = " << initial << std::endl;
 298   //determine the current range
 299   if( initial || ( d_owner.getKind()==FORALL && d_qe && d_qe->getBoundedIntegers() &&
 300                    d_qe->getBoundedIntegers()->isBoundVar( d_owner, d_owner[0][v] ) &&
 301                    !d_qe->getBoundedIntegers()->isGroundRange( d_owner, d_owner[0][v] ) ) ){
 302     Trace("bound-int-rsi") << "Getting range of " << d_owner[0][v] << std::endl;
 303     if( d_enum_type[v]==ENUM_INT_RANGE ){
 304       Node actual_l;
 305       Node l, u;
 306       if( d_qe->getBoundedIntegers() ){
 307         unsigned bvt = d_qe->getBoundedIntegers()->getBoundVarType( d_owner, d_owner[0][v] );
 308         if( bvt==quantifiers::BoundedIntegers::BOUND_INT_RANGE ){
 309           d_qe->getBoundedIntegers()->getBoundValues( d_owner, d_owner[0][v], this, l, u );
 310         }
 311       }
 312       for( unsigned b=0; b<2; b++ ){
 313         if( d_bounds[b].find(v)!=d_bounds[b].end() ){
 314           Trace("bound-int-rsi") << "May further limit bound(" << b << ") based on " << d_bounds[b][v] << std::endl;
 315           if( b==0 && (l.isNull() || d_bounds[b][v].getConst<Rational>() > l.getConst<Rational>()) ){
 316             if( !l.isNull() ){
 317               //bound was limited externally, record that the value lower bound is not equal to the term lower bound
 318               actual_l = NodeManager::currentNM()->mkNode( MINUS, d_bounds[b][v], l );
 319             }
 320             l = d_bounds[b][v];
 321           }else if( b==1 && (u.isNull() || d_bounds[b][v].getConst<Rational>() <= u.getConst<Rational>()) ){
 322             u = NodeManager::currentNM()->mkNode( MINUS, d_bounds[b][v],
 323                                                   NodeManager::currentNM()->mkConst( Rational(1) ) );
 324             u = Rewriter::rewrite( u );
 325           }
 326         }
 327       }
 328
 329       if( l.isNull() || u.isNull() ){
 330         //failed, abort the iterator
 331         return -1;
 332       }else{
 333         Trace("bound-int-rsi") << "Can limit bounds of " << d_owner[0][v] << " to " << l << "..." << u << std::endl;
 334         Node range = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MINUS, u, l ) );
 335         Node ra = Rewriter::rewrite( NodeManager::currentNM()->mkNode( LEQ, range, NodeManager::currentNM()->mkConst( Rational( 9999 ) ) ) );
 336         d_domain[v].clear();
 337         Node tl = l;
 338         Node tu = u;
 339         if( d_qe->getBoundedIntegers() && d_qe->getBoundedIntegers()->isBoundVar( d_owner, d_owner[0][v] ) ){
 340           d_qe->getBoundedIntegers()->getBounds( d_owner, d_owner[0][v], this, tl, tu );
 341         }
 342         d_lower_bounds[v] = tl;
 343         if( !actual_l.isNull() ){
 344           //if bound was limited externally, must consider the offset
 345           d_lower_bounds[v] = Rewriter::rewrite( NodeManager::currentNM()->mkNode( PLUS, tl, actual_l ) );
 346         }
 347         if( ra==d_qe->getTermDatabase()->d_true ){
 348           long rr = range.getConst<Rational>().getNumerator().getLong()+1;
 349           Trace("bound-int-rsi")  << "Actual bound range is " << rr << std::endl;
 350           d_domain[v].push_back( (int)rr );
 351           if( rr<=0 ){
 352             return 0;
 353           }
 354         }else{
 355           Trace("fmf-incomplete") << "Incomplete because of integer quantification, bounds are too big for " << d_owner[0][v] << "." << std::endl;
 356           return -1;
 357         }
 358       }
 359     }else if( d_enum_type[v]==ENUM_SET_MEMBERS ){
 360       Assert( d_qe->getBoundedIntegers()->getBoundVarType( d_owner, d_owner[0][v] )==quantifiers::BoundedIntegers::BOUND_SET_MEMBER );
 361       Node srv = d_qe->getBoundedIntegers()->getSetRangeValue( d_owner, d_owner[0][v], this );
 362       if( srv.isNull() ){
 363         return -1;
 364       }
 365       Trace("bound-int-rsi") << "Bounded by set membership : " << srv << std::endl;
 366       d_domain[v].clear();
 367       d_setm_bounds[v].clear();
 368       if( srv.getKind()!=EMPTYSET ){
 369         while( srv.getKind()==UNION ){
 370           Assert( srv[1].getKind()==kind::SINGLETON );
 371           d_setm_bounds[v].push_back( srv[1][0] );
 372           srv = srv[0];
 373         }
 374         Assert( srv.getKind()==kind::SINGLETON );
 375         d_setm_bounds[v].push_back( srv[0] );
 376         d_domain[v].push_back( d_setm_bounds[v].size() );
 377       }else{
 378         d_domain[v].push_back( 0 );
 379         return 0;
 380       }
 381     }
 382   }
 383   return 1;
 384 }
 385
 386 int RepSetIterator::increment2( int i ){
 387   Assert( !isFinished() );
 388 #ifdef DISABLE_EVAL_SKIP_MULTIPLE
 389   i = (int)d_index.size()-1;
 390 #endif
 391   //increment d_index
 392   if( i>=0){
 393     Trace("rsi-debug") << "domain size of " << i << " is " << domainSize(i) << std::endl;
 394   }
 395   while( i>=0 && d_index[i]>=(int)(domainSize(i)-1) ){
 396     i--;
 397     if( i>=0){
 398       Trace("rsi-debug") << "domain size of " << i << " is " << domainSize(i) << std::endl;
 399     }
 400   }
 401   if( i==-1 ){
 402     d_index.clear();
 403     return -1;
 404   }else{
 405     Trace("rsi-debug") << "increment " << i << std::endl;
 406     d_index[i]++;
 407     return do_reset_increment( i );
 408   }
 409 }
 410
 411 int RepSetIterator::do_reset_increment( int i, bool initial ) {
 412   bool emptyDomain = false;
 413   for( unsigned ii=(i+1); ii<d_index.size(); ii++ ){
 414     int ri_res = resetIndex( ii, initial );
 415     if( ri_res==-1 ){
 416       //failed
 417       d_index.clear();
 418       d_incomplete = true;
 419       break;
 420     }else if( ri_res==0 ){
 421       emptyDomain = true;
 422     }
 423     //force next iteration if currently an empty domain
 424     if( emptyDomain ){
 425       d_index[ii] = domainSize(ii)-1;
 426     }
 427   }
 428   if( emptyDomain ){
 429     Trace("rsi-debug") << "This is an empty domain, increment." << std::endl;
 430     return increment();
 431   }else{
 432     return i;
 433   }
 434 }
 435
 436 int RepSetIterator::increment(){
 437   if( !isFinished() ){
 438     return increment2( (int)d_index.size()-1 );
 439   }else{
 440     return -1;
 441   }
 442 }
 443
 444 bool RepSetIterator::isFinished(){
 445   return d_index.empty();
 446 }
 447
 448 Node RepSetIterator::getCurrentTerm( int v ){
 449   Trace("rsi-debug") << "rsi : get term " << v << ", index order = " << d_index_order[v] << std::endl;
 450   int ii = d_index_order[v];
 451   int curr = d_index[ii];
 452   if( d_enum_type[v]==ENUM_DOMAIN_ELEMENTS ){
 453     TypeNode tn = d_types[v];
 454     Assert( d_rep_set->d_type_reps.find( tn )!=d_rep_set->d_type_reps.end() );
 455     Assert( 0<=d_domain[v][curr] && d_domain[v][curr]<(int)d_rep_set->d_type_reps[tn].size() );
 456     return d_rep_set->d_type_reps[tn][d_domain[v][curr]];
 457   }else if( d_enum_type[v]==ENUM_SET_MEMBERS ){
 458     Assert( 0<=curr && curr<(int)d_setm_bounds[v].size() );
 459     return d_setm_bounds[v][curr];
 460   }else{
 461     Trace("rsi-debug") << "Get, with offset : " << v << " " << d_lower_bounds[v] << " " << curr << std::endl;
 462     Assert( !d_lower_bounds[v].isNull() );
 463     Node t = NodeManager::currentNM()->mkNode(PLUS, d_lower_bounds[v], NodeManager::currentNM()->mkConst( Rational(curr) ) );
 464     t = Rewriter::rewrite( t );
 465     return t;
 466   }
 467 }
 468
 469 void RepSetIterator::debugPrint( const char* c ){
 470   for( unsigned v=0; v<d_index.size(); v++ ){
 471     Debug( c ) << v << " : " << getCurrentTerm( v ) << std::endl;
 472   }
 473 }
 474
 475 void RepSetIterator::debugPrintSmall( const char* c ){
 476   Debug( c ) << "RI: ";
 477   for( unsigned v=0; v<d_index.size(); v++ ){
 478     Debug( c ) << v << ": " << getCurrentTerm( v ) << " ";
 479   }
 480   Debug( c ) << std::endl;
 481 }
 482