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