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 }
  33
  34 bool RepSet::hasRep( TypeNode tn, Node n ) {
  35   std::map< TypeNode, std::vector< Node > >::iterator it = d_type_reps.find( tn );
  36   if( it==d_type_reps.end() ){
  37     return false;
  38   }else{
  39     return std::find( it->second.begin(), it->second.end(), n )!=it->second.end();
  40   }
  41 }
  42
  43 int RepSet::getNumRepresentatives( TypeNode tn ) const{
  44   std::map< TypeNode, std::vector< Node > >::const_iterator it = d_type_reps.find( tn );
  45   if( it!=d_type_reps.end() ){
  46     return (int)it->second.size();
  47   }else{
  48     return 0;
  49   }
  50 }
  51
  52 bool containsStoreAll( Node n, std::vector< Node >& cache ){
  53   if( std::find( cache.begin(), cache.end(), n )==cache.end() ){
  54     cache.push_back( n );
  55     if( n.getKind()==STORE_ALL ){
  56       return true;
  57     }else{
  58       for( unsigned i=0; i<n.getNumChildren(); i++ ){
  59         if( containsStoreAll( n[i], cache ) ){
  60           return true;
  61         }
  62       }
  63     }
  64   }
  65   return false;
  66 }
  67
  68 void RepSet::add( TypeNode tn, Node n ){
  69   //for now, do not add array constants FIXME
  70   if( tn.isArray() ){
  71     std::vector< Node > cache;
  72     if( containsStoreAll( n, cache ) ){
  73       return;
  74     }
  75   }
  76   Trace("rsi-debug") << "Add rep #" << d_type_reps[tn].size() << " for " << tn << " : " << n << std::endl;
  77   Assert( n.getType().isSubtypeOf( tn ) );
  78   d_tmap[ n ] = (int)d_type_reps[tn].size();
  79   d_type_reps[tn].push_back( n );
  80 }
  81
  82 int RepSet::getIndexFor( Node n ) const {
  83   std::map< Node, int >::const_iterator it = d_tmap.find( n );
  84   if( it!=d_tmap.end() ){
  85     return it->second;
  86   }else{
  87     return -1;
  88   }
  89 }
  90
  91 bool RepSet::complete( TypeNode t ){
  92   std::map< TypeNode, bool >::iterator it = d_type_complete.find( t );
  93   if( it==d_type_complete.end() ){
  94     //remove all previous
  95     for( unsigned i=0; i<d_type_reps[t].size(); i++ ){
  96       d_tmap.erase( d_type_reps[t][i] );
  97     }
  98     d_type_reps[t].clear();
  99     //now complete the type
 100     d_type_complete[t] = true;
 101     TypeEnumerator te(t);
 102     while( !te.isFinished() ){
 103       Node n = *te;
 104       if( std::find( d_type_reps[t].begin(), d_type_reps[t].end(), n )==d_type_reps[t].end() ){
 105         add( t, n );
 106       }
 107       ++te;
 108     }
 109     for( size_t i=0; i<d_type_reps[t].size(); i++ ){
 110       Trace("reps-complete") << d_type_reps[t][i] << " ";
 111     }
 112     Trace("reps-complete") << std::endl;
 113     return true;
 114   }else{
 115     return it->second;
 116   }
 117 }
 118
 119 void RepSet::toStream(std::ostream& out){
 120   for( std::map< TypeNode, std::vector< Node > >::iterator it = d_type_reps.begin(); it != d_type_reps.end(); ++it ){
 121     if( !it->first.isFunction() && !it->first.isPredicate() ){
 122       out << "(" << it->first << " " << it->second.size();
 123       out << " (";
 124       for( unsigned i=0; i<it->second.size(); i++ ){
 125         if( i>0 ){ out << " "; }
 126         out << it->second[i];
 127       }
 128       out << ")";
 129       out << ")" << std::endl;
 130     }
 131   }
 132 }
 133
 134
 135 RepSetIterator::RepSetIterator( QuantifiersEngine * qe, RepSet* rs ) : d_qe(qe), d_rep_set( rs ){
 136   d_incomplete = false;
 137 }
 138
 139 int RepSetIterator::domainSize( int i ) {
 140   Assert(i>=0);
 141   int v = d_var_order[i];
 142   return d_domain_elements[v].size();
 143 }
 144
 145 bool RepSetIterator::setQuantifier( Node f, RepBoundExt* rext ){
 146   Trace("rsi") << "Make rsi for " << f << std::endl;
 147   Assert( d_types.empty() );
 148   //store indicies
 149   for( size_t i=0; i<f[0].getNumChildren(); i++ ){
 150     d_types.push_back( f[0][i].getType() );
 151   }
 152   d_owner = f;
 153   return initialize( rext );
 154 }
 155
 156 bool RepSetIterator::setFunctionDomain( Node op, RepBoundExt* rext ){
 157   Trace("rsi") << "Make rsi for " << op << std::endl;
 158   Assert( d_types.empty() );
 159   TypeNode tn = op.getType();
 160   for( size_t i=0; i<tn.getNumChildren()-1; i++ ){
 161     d_types.push_back( tn[i] );
 162   }
 163   d_owner = op;
 164   return initialize( rext );
 165 }
 166
 167 bool RepSetIterator::initialize( RepBoundExt* rext ){
 168   Trace("rsi") << "Initialize rep set iterator..." << std::endl;
 169   for( unsigned v=0; v<d_types.size(); v++ ){
 170     d_index.push_back( 0 );
 171     //store default index order
 172     d_index_order.push_back( v );
 173     d_var_order[v] = v;
 174     //store default domain
 175     //d_domain.push_back( RepDomain() );
 176     d_domain_elements.push_back( std::vector< Node >() );
 177     TypeNode tn = d_types[v];
 178     Trace("rsi") << "Var #" << v << " is type " << tn << "..." << std::endl;
 179     if( tn.isSort() ){
 180       //must ensure uninterpreted type is non-empty.
 181       if( !d_rep_set->hasType( tn ) ){
 182         //FIXME:
 183         // terms in rep_set are now constants which mapped to terms through TheoryModel
 184         // thus, should introduce a constant and a term.  for now, just a term.
 185
 186         //Node c = d_qe->getTermDatabase()->getEnumerateTerm( tn, 0 );
 187         Node var = d_qe->getModel()->getSomeDomainElement( tn );
 188         Trace("mkVar") << "RepSetIterator:: Make variable " << var << " : " << tn << std::endl;
 189         d_rep_set->add( tn, var );
 190       }
 191     }
 192     bool inc = true;
 193     //check if it is externally bound
 194     if( rext && rext->setBound( d_owner, v, tn, d_domain_elements[v] ) ){
 195       d_enum_type.push_back( ENUM_DEFAULT );
 196       inc = false;
 197     //builtin: check if it is bound by bounded integer module
 198     }else if( d_owner.getKind()==FORALL && d_qe && d_qe->getBoundedIntegers() ){
 199       if( d_qe->getBoundedIntegers()->isBoundVar( d_owner, d_owner[0][v] ) ){
 200         unsigned bvt = d_qe->getBoundedIntegers()->getBoundVarType( d_owner, d_owner[0][v] );
 201         if( bvt!=quantifiers::BoundedIntegers::BOUND_FINITE ){
 202           d_enum_type.push_back( ENUM_BOUND_INT );
 203           inc = false;
 204         }else{
 205           //will treat in default way
 206         }
 207       }
 208     }
 209     if( !tn.isSort() ){
 210       if( inc ){
 211         if( d_qe->getTermDatabase()->mayComplete( tn ) ){
 212           Trace("rsi") << "  do complete, since cardinality is small (" << tn.getCardinality() << ")..." << std::endl;
 213           d_rep_set->complete( tn );
 214           //must have succeeded
 215           Assert( d_rep_set->hasType( tn ) );
 216         }else{
 217           Trace("rsi") << "  variable cannot be bounded." << std::endl;
 218           Trace("fmf-incomplete") << "Incomplete because of quantification of type " << tn << std::endl;
 219           d_incomplete = true;
 220         }
 221       }
 222     }
 223
 224     //if we have yet to determine the type of enumeration
 225     if( d_enum_type.size()<=v ){
 226       if( d_rep_set->hasType( tn ) ){
 227         d_enum_type.push_back( ENUM_DEFAULT );
 228         for( unsigned j=0; j<d_rep_set->d_type_reps[tn].size(); j++ ){
 229           //d_domain[v].push_back( j );
 230           d_domain_elements[v].push_back( d_rep_set->d_type_reps[tn][j] );
 231         }
 232       }else{
 233         Assert( d_incomplete );
 234         return false;
 235       }
 236     }
 237   }
 238   //must set a variable index order based on bounded integers
 239   if( d_owner.getKind()==FORALL && d_qe && d_qe->getBoundedIntegers() ){
 240     Trace("bound-int-rsi") << "Calculating variable order..." << std::endl;
 241     std::vector< int > varOrder;
 242     for( unsigned i=0; i<d_qe->getBoundedIntegers()->getNumBoundVars( d_owner ); i++ ){
 243       Node v = d_qe->getBoundedIntegers()->getBoundVar( d_owner, i );
 244       Trace("bound-int-rsi") << "  bound var #" << i << " is " << v << std::endl;
 245       varOrder.push_back( d_qe->getTermDatabase()->getVariableNum( d_owner, v ) );
 246     }
 247     for( unsigned i=0; i<d_owner[0].getNumChildren(); i++) {
 248       if( !d_qe->getBoundedIntegers()->isBoundVar(d_owner, d_owner[0][i])) {
 249         varOrder.push_back(i);
 250       }
 251     }
 252     Trace("bound-int-rsi") << "Variable order : ";
 253     for( unsigned i=0; i<varOrder.size(); i++) {
 254       Trace("bound-int-rsi") << varOrder[i] << " ";
 255     }
 256     Trace("bound-int-rsi") << std::endl;
 257     std::vector< int > indexOrder;
 258     indexOrder.resize(varOrder.size());
 259     for( unsigned i=0; i<varOrder.size(); i++){
 260       indexOrder[varOrder[i]] = i;
 261     }
 262     Trace("bound-int-rsi") << "Will use index order : ";
 263     for( unsigned i=0; i<indexOrder.size(); i++) {
 264       Trace("bound-int-rsi") << indexOrder[i] << " ";
 265     }
 266     Trace("bound-int-rsi") << std::endl;
 267     setIndexOrder( indexOrder );
 268   }
 269   //now reset the indices
 270   do_reset_increment( -1, true );
 271   return true;
 272 }
 273
 274 void RepSetIterator::setIndexOrder( std::vector< int >& indexOrder ){
 275   d_index_order.clear();
 276   d_index_order.insert( d_index_order.begin(), indexOrder.begin(), indexOrder.end() );
 277   //make the d_var_order mapping
 278   for( unsigned i=0; i<d_index_order.size(); i++ ){
 279     d_var_order[d_index_order[i]] = i;
 280   }
 281 }
 282
 283 int RepSetIterator::resetIndex( int i, bool initial ) {
 284   d_index[i] = 0;
 285   int v = d_var_order[i];
 286   Trace("bound-int-rsi") << "Reset " << i << ", var order = " << v << ", initial = " << initial << std::endl;
 287   if( d_enum_type[v]==ENUM_BOUND_INT ){
 288     Assert( d_owner.getKind()==FORALL );
 289     if( !d_qe->getBoundedIntegers()->getBoundElements( this, initial, d_owner, d_owner[0][v], d_domain_elements[v] ) ){
 290       return -1;
 291     }
 292   }
 293   return d_domain_elements[v].empty() ? 0 : 1;
 294 }
 295
 296 int RepSetIterator::increment2( int i ){
 297   Assert( !isFinished() );
 298 #ifdef DISABLE_EVAL_SKIP_MULTIPLE
 299   i = (int)d_index.size()-1;
 300 #endif
 301   //increment d_index
 302   if( i>=0){
 303     Trace("rsi-debug") << "domain size of " << i << " is " << domainSize(i) << std::endl;
 304   }
 305   while( i>=0 && d_index[i]>=(int)(domainSize(i)-1) ){
 306     i--;
 307     if( i>=0){
 308       Trace("rsi-debug") << "domain size of " << i << " is " << domainSize(i) << std::endl;
 309     }
 310   }
 311   if( i==-1 ){
 312     d_index.clear();
 313     return -1;
 314   }else{
 315     Trace("rsi-debug") << "increment " << i << std::endl;
 316     d_index[i]++;
 317     return do_reset_increment( i );
 318   }
 319 }
 320
 321 int RepSetIterator::do_reset_increment( int i, bool initial ) {
 322   bool emptyDomain = false;
 323   for( unsigned ii=(i+1); ii<d_index.size(); ii++ ){
 324     int ri_res = resetIndex( ii, initial );
 325     if( ri_res==-1 ){
 326       //failed
 327       d_index.clear();
 328       d_incomplete = true;
 329       break;
 330     }else if( ri_res==0 ){
 331       emptyDomain = true;
 332     }
 333     //force next iteration if currently an empty domain
 334     if( emptyDomain ){
 335       d_index[ii] = domainSize(ii)-1;
 336     }
 337   }
 338   if( emptyDomain ){
 339     Trace("rsi-debug") << "This is an empty domain, increment." << std::endl;
 340     return increment();
 341   }else{
 342     return i;
 343   }
 344 }
 345
 346 int RepSetIterator::increment(){
 347   if( !isFinished() ){
 348     return increment2( (int)d_index.size()-1 );
 349   }else{
 350     return -1;
 351   }
 352 }
 353
 354 bool RepSetIterator::isFinished(){
 355   return d_index.empty();
 356 }
 357
 358 Node RepSetIterator::getCurrentTerm( int v ){
 359   int ii = d_index_order[v];
 360   int curr = d_index[ii];
 361   Trace("rsi-debug") << "rsi : get term " << v << ", index order = " << d_index_order[v] << std::endl;
 362   Trace("rsi-debug") << "rsi : curr = " << curr << " / " << d_domain_elements[v].size() << std::endl;
 363   Assert( 0<=curr && curr<(int)d_domain_elements[v].size() );
 364   return d_domain_elements[v][curr];
 365 }
 366
 367 void RepSetIterator::debugPrint( const char* c ){
 368   for( unsigned v=0; v<d_index.size(); v++ ){
 369     Debug( c ) << v << " : " << getCurrentTerm( v ) << std::endl;
 370   }
 371 }
 372
 373 void RepSetIterator::debugPrintSmall( const char* c ){
 374   Debug( c ) << "RI: ";
 375   for( unsigned v=0; v<d_index.size(); v++ ){
 376     Debug( c ) << v << ": " << getCurrentTerm( v ) << " ";
 377   }
 378   Debug( c ) << std::endl;
 379 }
 380