src/theory/rep_set.cpp

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