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