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