src/theory/rep_set.cpp

   1 /*********************                                                        */
   2 /*! \file rep_set.cpp
   3  ** \verbatim
   4  ** Original author: Andrew Reynolds
   5  ** Major contributors: Morgan Deters
   6  ** Minor contributors (to current version): none
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-2013  New York University and The University of Iowa
   9  ** See the file COPYING in the top-level source directory for licensing
  10  ** 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
  19 using namespace std;
  20 using namespace CVC4;
  21 using namespace CVC4::kind;
  22 using namespace CVC4::context;
  23 using namespace CVC4::theory;
  24
  25 void RepSet::clear(){
  26   d_type_reps.clear();
  27   d_type_complete.clear();
  28   d_tmap.clear();
  29 }
  30
  31 int RepSet::getNumRepresentatives( TypeNode tn ) const{
  32   std::map< TypeNode, std::vector< Node > >::const_iterator it = d_type_reps.find( tn );
  33   if( it!=d_type_reps.end() ){
  34     return (int)it->second.size();
  35   }else{
  36     return 0;
  37   }
  38 }
  39
  40 void RepSet::add( Node n ){
  41   TypeNode t = n.getType();
  42   d_tmap[ n ] = (int)d_type_reps[t].size();
  43   d_type_reps[t].push_back( n );
  44 }
  45
  46 int RepSet::getIndexFor( Node n ) const {
  47   std::map< Node, int >::const_iterator it = d_tmap.find( n );
  48   if( it!=d_tmap.end() ){
  49     return it->second;
  50   }else{
  51     return -1;
  52   }
  53 }
  54
  55 void RepSet::complete( TypeNode t ){
  56   if( d_type_complete.find( t )==d_type_complete.end() ){
  57     d_type_complete[t] = true;
  58     TypeEnumerator te(t);
  59     while( !te.isFinished() ){
  60       Node n = *te;
  61       if( std::find( d_type_reps[t].begin(), d_type_reps[t].end(), n )==d_type_reps[t].end() ){
  62         add( n );
  63       }
  64       ++te;
  65     }
  66     for( size_t i=0; i<d_type_reps[t].size(); i++ ){
  67       Trace("reps-complete") << d_type_reps[t][i] << " ";
  68     }
  69     Trace("reps-complete") << std::endl;
  70   }
  71 }
  72
  73 void RepSet::toStream(std::ostream& out){
  74 #if 0
  75   for( std::map< TypeNode, std::vector< Node > >::iterator it = d_type_reps.begin(); it != d_type_reps.end(); ++it ){
  76     out << it->first << " : " << std::endl;
  77     for( int i=0; i<(int)it->second.size(); i++ ){
  78       out << "   " << i << ": " << it->second[i] << std::endl;
  79     }
  80   }
  81 #else
  82   for( std::map< TypeNode, std::vector< Node > >::iterator it = d_type_reps.begin(); it != d_type_reps.end(); ++it ){
  83     if( !it->first.isFunction() && !it->first.isPredicate() ){
  84       out << "(" << it->first << " " << it->second.size();
  85       out << " (";
  86       for( int i=0; i<(int)it->second.size(); i++ ){
  87         if( i>0 ){ out << " "; }
  88         out << it->second[i];
  89       }
  90       out << ")";
  91       out << ")" << std::endl;
  92     }
  93   }
  94 #endif
  95 }
  96
  97
  98 RepSetIterator::RepSetIterator( QuantifiersEngine * qe, RepSet* rs ) : d_qe(qe), d_rep_set( rs ){
  99   d_incomplete = false;
 100 }
 101
 102 int RepSetIterator::domainSize( int i ) {
 103   Assert(i>=0);
 104   if( d_enum_type[i]==ENUM_DOMAIN_ELEMENTS ){
 105     return d_domain[i].size();
 106   }else{
 107     return d_domain[i][0];
 108   }
 109 }
 110
 111 bool RepSetIterator::setQuantifier( Node f ){
 112   Trace("rsi") << "Make rsi for " << f << std::endl;
 113   Assert( d_types.empty() );
 114   //store indicies
 115   for( size_t i=0; i<f[0].getNumChildren(); i++ ){
 116     d_types.push_back( f[0][i].getType() );
 117   }
 118   d_owner = f;
 119   return initialize();
 120 }
 121
 122 bool RepSetIterator::setFunctionDomain( Node op ){
 123   Trace("rsi") << "Make rsi for " << op << std::endl;
 124   Assert( d_types.empty() );
 125   TypeNode tn = op.getType();
 126   for( size_t i=0; i<tn.getNumChildren()-1; i++ ){
 127     d_types.push_back( tn[i] );
 128   }
 129   d_owner = op;
 130   return initialize();
 131 }
 132
 133 bool RepSetIterator::initialize(){
 134   for( size_t i=0; i<d_types.size(); i++ ){
 135     d_index.push_back( 0 );
 136     //store default index order
 137     d_index_order.push_back( i );
 138     d_var_order[i] = i;
 139     //store default domain
 140     d_domain.push_back( RepDomain() );
 141     TypeNode tn = d_types[i];
 142     bool isSet = false;
 143     if( tn.isSort() ){
 144       if( !d_rep_set->hasType( tn ) ){
 145         Node var = NodeManager::currentNM()->mkSkolem( "repSet_$$", tn, "is a variable created by the RepSetIterator" );
 146         Trace("mkVar") << "RepSetIterator:: Make variable " << var << " : " << tn << std::endl;
 147         d_rep_set->add( var );
 148       }
 149     }else if( tn.isInteger() ){
 150       //check if it is bound
 151       if( d_owner.getKind()==FORALL && d_qe && d_qe->getBoundedIntegers() ){
 152         if( d_qe->getBoundedIntegers()->isBoundVar( d_owner, d_owner[0][i] ) ){
 153           Trace("bound-int-rsi") << "Rep set iterator: variable #" << i << " is bounded integer." << std::endl;
 154           d_enum_type.push_back( ENUM_RANGE );
 155           isSet = true;
 156         }else{
 157           Trace("fmf-incomplete") << "Incomplete because of integer quantification, no bounds found." << std::endl;
 158           d_incomplete = true;
 159         }
 160       }else{
 161         Trace("fmf-incomplete") << "Incomplete because of integer quantification." << std::endl;
 162         d_incomplete = true;
 163       }
 164     }else if( tn.isReal() ){
 165       Trace("fmf-incomplete") << "Incomplete because of infinite type " << tn << std::endl;
 166       d_incomplete = true;
 167     //enumerate if the sort is reasonably small, the upper bound of 128 is chosen arbitrarily for now
 168     }else if( tn.getCardinality().isFinite() && tn.getCardinality().getFiniteCardinality().toUnsignedInt()<=128 ){
 169       d_rep_set->complete( tn );
 170     }else{
 171       Trace("fmf-incomplete") << "Incomplete because of unknown type " << tn << std::endl;
 172       d_incomplete = true;
 173     }
 174     if( !isSet ){
 175       d_enum_type.push_back( ENUM_DOMAIN_ELEMENTS );
 176       if( d_rep_set->hasType( tn ) ){
 177         for( size_t j=0; j<d_rep_set->d_type_reps[tn].size(); j++ ){
 178           d_domain[i].push_back( j );
 179         }
 180       }else{
 181         return false;
 182       }
 183     }
 184   }
 185   //must set a variable index order
 186   if (d_owner.getKind()==FORALL && d_qe && d_qe->getBoundedIntegers()) {
 187     Trace("bound-int-rsi") << "Calculating variable order..." << std::endl;
 188     std::vector< int > varOrder;
 189     for( unsigned i=0; i<d_qe->getBoundedIntegers()->getNumBoundVars(d_owner); i++ ){
 190       varOrder.push_back(d_qe->getBoundedIntegers()->getBoundVarNum(d_owner,i));
 191     }
 192     for( unsigned i=0; i<d_owner[0].getNumChildren(); i++) {
 193       if( !d_qe->getBoundedIntegers()->isBoundVar(d_owner, d_owner[0][i])) {
 194         varOrder.push_back(i);
 195       }
 196     }
 197     Trace("bound-int-rsi") << "Variable order : ";
 198     for( unsigned i=0; i<varOrder.size(); i++) {
 199       Trace("bound-int-rsi") << varOrder[i] << " ";
 200     }
 201     Trace("bound-int-rsi") << std::endl;
 202     std::vector< int > indexOrder;
 203     indexOrder.resize(varOrder.size());
 204     for( unsigned i=0; i<varOrder.size(); i++){
 205       indexOrder[varOrder[i]] = i;
 206     }
 207     Trace("bound-int-rsi") << "Will use index order : ";
 208     for( unsigned i=0; i<indexOrder.size(); i++) {
 209       Trace("bound-int-rsi") << indexOrder[i] << " ";
 210     }
 211     Trace("bound-int-rsi") << std::endl;
 212     setIndexOrder(indexOrder);
 213   }
 214   for (unsigned i=0; i<d_index.size(); i++) {
 215     if (!resetIndex(i, true)){
 216       break;
 217     }
 218   }
 219   return true;
 220 }
 221
 222 void RepSetIterator::setIndexOrder( std::vector< int >& indexOrder ){
 223   d_index_order.clear();
 224   d_index_order.insert( d_index_order.begin(), indexOrder.begin(), indexOrder.end() );
 225   //make the d_var_order mapping
 226   for( int i=0; i<(int)d_index_order.size(); i++ ){
 227     d_var_order[d_index_order[i]] = i;
 228   }
 229 }
 230 /*
 231 void RepSetIterator::setDomain( std::vector< RepDomain >& domain ){
 232   d_domain.clear();
 233   d_domain.insert( d_domain.begin(), domain.begin(), domain.end() );
 234   //we are done if a domain is empty
 235   for( int i=0; i<(int)d_domain.size(); i++ ){
 236     if( d_domain[i].empty() ){
 237       d_index.clear();
 238     }
 239   }
 240 }
 241 */
 242 bool RepSetIterator::resetIndex( int i, bool initial ) {
 243   d_index[i] = 0;
 244   int ii = d_index_order[i];
 245   Trace("bound-int-rsi") << "Reset " << i << " " << ii << " " << initial << std::endl;
 246   //determine the current range
 247   if( d_enum_type[ii]==ENUM_RANGE ){
 248     if( initial || !d_qe->getBoundedIntegers()->isGroundRange( d_owner, d_owner[0][ii] ) ){
 249       Trace("bound-int-rsi") << "Getting range of " << d_owner[0][ii] << std::endl;
 250       Node l, u;
 251       d_qe->getBoundedIntegers()->getBoundValues( d_owner, d_owner[0][ii], this, l, u );
 252       if( l.isNull() || u.isNull() ){
 253         //failed, abort the iterator
 254         d_index.clear();
 255         return false;
 256       }else{
 257         Trace("bound-int-rsi") << "Can limit bounds of " << d_owner[0][ii] << " to " << l << "..." << u << std::endl;
 258         Node range = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MINUS, u, l ) );
 259         Node ra = Rewriter::rewrite( NodeManager::currentNM()->mkNode( LEQ, range, NodeManager::currentNM()->mkConst( Rational( 9999 ) ) ) );
 260         d_domain[ii].clear();
 261         d_lower_bounds[ii] = l;
 262         if( ra==NodeManager::currentNM()->mkConst(true) ){
 263           long rr = range.getConst<Rational>().getNumerator().getLong()+1;
 264           Trace("bound-int-rsi")  << "Actual bound range is " << rr << std::endl;
 265           d_domain[ii].push_back( (int)rr );
 266         }else{
 267           Trace("fmf-incomplete") << "Incomplete because of integer quantification, bounds are too big for " << d_owner[0][ii] << "." << std::endl;
 268           d_incomplete = true;
 269           d_domain[ii].push_back( 0 );
 270         }
 271       }
 272     }else{
 273       Trace("bound-int-rsi") << d_owner[0][ii] << " has ground range, skip." << std::endl;
 274     }
 275   }
 276   return true;
 277 }
 278
 279 int RepSetIterator::increment2( int counter ){
 280   Assert( !isFinished() );
 281 #ifdef DISABLE_EVAL_SKIP_MULTIPLE
 282   counter = (int)d_index.size()-1;
 283 #endif
 284   //increment d_index
 285   if( counter>=0){
 286     Trace("rsi-debug") << "domain size of " << counter << " is " << domainSize(counter) << std::endl;
 287   }
 288   while( counter>=0 && d_index[counter]>=(int)(domainSize(counter)-1) ){
 289     counter--;
 290     if( counter>=0){
 291       Trace("rsi-debug") << "domain size of " << counter << " is " << domainSize(counter) << std::endl;
 292     }
 293   }
 294   if( counter==-1 ){
 295     d_index.clear();
 296   }else{
 297     d_index[counter]++;
 298     bool emptyDomain = false;
 299     for( int i=(int)d_index.size()-1; i>counter; i-- ){
 300       if (!resetIndex(i)){
 301         break;
 302       }else if( domainSize(i)<=0 ){
 303         emptyDomain = true;
 304       }
 305     }
 306     if( emptyDomain ){
 307       Trace("rsi-debug") << "This is an empty domain, increment again." << std::endl;
 308       return increment();
 309     }
 310   }
 311   return counter;
 312 }
 313
 314 int RepSetIterator::increment(){
 315   if( !isFinished() ){
 316     return increment2( (int)d_index.size()-1 );
 317   }else{
 318     return -1;
 319   }
 320 }
 321
 322 bool RepSetIterator::isFinished(){
 323   return d_index.empty();
 324 }
 325
 326 Node RepSetIterator::getTerm( int i ){
 327   int index = d_index_order[i];
 328   if( d_enum_type[index]==ENUM_DOMAIN_ELEMENTS ){
 329     TypeNode tn = d_types[index];
 330     Assert( d_rep_set->d_type_reps.find( tn )!=d_rep_set->d_type_reps.end() );
 331     return d_rep_set->d_type_reps[tn][d_domain[index][d_index[index]]];
 332   }else{
 333     Trace("rsi-debug") << index << " " << d_lower_bounds[index] << " " << d_index[index] << std::endl;
 334     Node t = NodeManager::currentNM()->mkNode(PLUS, d_lower_bounds[index],
 335                                                     NodeManager::currentNM()->mkConst( Rational(d_index[index]) ) );
 336     t = Rewriter::rewrite( t );
 337     return t;
 338   }
 339 }
 340
 341 void RepSetIterator::debugPrint( const char* c ){
 342   for( int i=0; i<(int)d_index.size(); i++ ){
 343     Debug( c ) << i << " : " << d_index[i] << " : " << getTerm( i ) << std::endl;
 344   }
 345 }
 346
 347 void RepSetIterator::debugPrintSmall( const char* c ){
 348   Debug( c ) << "RI: ";
 349   for( int i=0; i<(int)d_index.size(); i++ ){
 350     Debug( c ) << d_index[i] << ": " << getTerm( i ) << " ";
 351   }
 352   Debug( c ) << std::endl;
 353 }