src/theory/rep_set.cpp

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