src/theory/sets/theory_sets_type_enumerator.h

   1 /*********************                                                        */
   2 /*! \file theory_sets_type_enumerator.h
   3  ** \verbatim
   4  ** Original author: Kshitij Bansal
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): none
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-2014  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 [[ Add one-line brief description here ]]
  13  **
  14  ** [[ Add lengthier description here ]]
  15  ** \todo document this file
  16  **/
  17
  18
  19 #include "cvc4_private.h"
  20
  21 #ifndef __CVC4__THEORY__SETS__TYPE_ENUMERATOR_H
  22 #define __CVC4__THEORY__SETS__TYPE_ENUMERATOR_H
  23
  24 #include "theory/type_enumerator.h"
  25 #include "expr/type_node.h"
  26 #include "expr/kind.h"
  27 #include "theory/rewriter.h"
  28
  29 namespace CVC4 {
  30 namespace theory {
  31 namespace sets {
  32
  33 class SetEnumerator : public TypeEnumeratorBase<SetEnumerator> {
  34   unsigned d_index;
  35   TypeNode d_constituentType;
  36   NodeManager* d_nm;
  37   std::vector<bool> d_indexVec;
  38   std::vector<TypeEnumerator*> d_constituentVec;
  39   bool d_finished;
  40   Node d_setConst;
  41
  42 public:
  43
  44   SetEnumerator(TypeNode type) throw(AssertionException) :
  45     TypeEnumeratorBase<SetEnumerator>(type),
  46     d_index(0),
  47     d_constituentType(type.getSetElementType()),
  48     d_nm(NodeManager::currentNM()),
  49     d_indexVec(),
  50     d_constituentVec(),
  51     d_finished(false),
  52     d_setConst()
  53   {
  54     // d_indexVec.push_back(false);
  55     // d_constituentVec.push_back(new TypeEnumerator(d_constituentType));
  56     d_setConst = d_nm->mkConst(EmptySet(type.toType()));
  57   }
  58
  59   // An set enumerator could be large, and generally you don't want to
  60   // go around copying these things; but a copy ctor is presently required
  61   // by the TypeEnumerator framework.
  62   SetEnumerator(const SetEnumerator& ae) throw() :
  63     TypeEnumeratorBase<SetEnumerator>(ae.d_nm->mkSetType(ae.d_constituentType)),
  64     d_constituentType(ae.d_constituentType),
  65     d_nm(ae.d_nm),
  66     d_indexVec(ae.d_indexVec),
  67     d_constituentVec(),// copied below
  68     d_finished(ae.d_finished),
  69     d_setConst(ae.d_setConst)
  70   {
  71     for(std::vector<TypeEnumerator*>::const_iterator i =
  72           ae.d_constituentVec.begin(), i_end = ae.d_constituentVec.end();
  73         i != i_end;
  74         ++i) {
  75       d_constituentVec.push_back(new TypeEnumerator(**i));
  76     }
  77   }
  78
  79   ~SetEnumerator() {
  80     while (!d_constituentVec.empty()) {
  81       delete d_constituentVec.back();
  82       d_constituentVec.pop_back();
  83     }
  84   }
  85
  86   Node operator*() throw(NoMoreValuesException) {
  87     if (d_finished) {
  88       throw NoMoreValuesException(getType());
  89     }
  90     Node n = d_setConst;
  91
  92     // For now only support only sets of size 1
  93     Assert(d_index == 0 || d_index == 1);
  94
  95     if(d_index == 1) {
  96       n = d_nm->mkNode(kind::SINGLETON, *(*(d_constituentVec[0])));
  97     }
  98
  99     // for (unsigned i = 0; i < d_indexVec.size(); ++i) {
 100     //   n = d_nm->mkNode(kind::STORE, n, d_indexVec[d_indexVec.size() - 1 - i], *(*(d_constituentVec[i])));
 101     // }
 102     Trace("set-type-enum") << "operator * prerewrite: " << n << std::endl;
 103     n = Rewriter::rewrite(n);
 104     Trace("set-type-enum") << "operator * returning: " << n << std::endl;
 105     return n;
 106   }
 107
 108   SetEnumerator& operator++() throw() {
 109     Trace("set-type-enum") << "operator++ called, **this = " << **this << std::endl;
 110
 111     if (d_finished) {
 112       Trace("set-type-enum") << "operator++ finished!" << std::endl;
 113       return *this;
 114     }
 115
 116     // increment by one, at the same time deleting all elements that
 117     // cannot be incremented any further (note: we are keeping a set
 118     // -- no repetitions -- thus some trickery to know what to pop and
 119     // what not to.)
 120     if(d_index > 0) {
 121       Assert(d_index == d_constituentVec.size());
 122
 123       Node last_pre_increment;
 124       last_pre_increment = *(*d_constituentVec.back());
 125
 126       ++(*d_constituentVec.back());
 127
 128       if (d_constituentVec.back()->isFinished()) {
 129         delete d_constituentVec.back();
 130         d_constituentVec.pop_back();
 131
 132         while(!d_constituentVec.empty()) {
 133           Node cur_pre_increment = *(*d_constituentVec.back());
 134           ++(*d_constituentVec.back());
 135           Node cur_post_increment = *(*d_constituentVec.back());
 136           if(last_pre_increment == cur_post_increment) {
 137             delete d_constituentVec.back();
 138             d_constituentVec.pop_back();
 139             last_pre_increment = cur_pre_increment;
 140           } else {
 141             break;
 142           }
 143         }
 144       }
 145     }
 146
 147     if (d_constituentVec.empty()) {
 148       ++d_index;
 149       d_constituentVec.push_back(new TypeEnumerator(d_constituentType));
 150     }
 151
 152     while (d_constituentVec.size() < d_index) {
 153       TypeEnumerator *d_newEnumerator = new TypeEnumerator(*d_constituentVec.back());
 154       ++(*d_newEnumerator);
 155       if( (*d_newEnumerator).isFinished() ) {
 156         Trace("set-type-enum") << "operator++ finished!" << std::endl;
 157         d_finished = true;
 158         return *this;
 159       }
 160       d_constituentVec.push_back(d_newEnumerator);
 161     }
 162
 163     Trace("set-type-enum") << "operator++ returning, **this = " << **this << std::endl;
 164     return *this;
 165   }
 166
 167   bool isFinished() throw() {
 168     Trace("set-type-enum") << "isFinished returning: " << d_finished << std::endl;
 169     return d_finished;
 170   }
 171
 172 };/* class SetEnumerator */
 173
 174 }/* CVC4::theory::sets namespace */
 175 }/* CVC4::theory namespace */
 176 }/* CVC4 namespace */
 177
 178 #endif /* __CVC4__THEORY__SETS__TYPE_ENUMERATOR_H */