1 /********************* */ 2 /*! \file type_enumerator.h 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-2019 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 An enumerator for datatypes 13 ** 14 ** An enumerator for datatypes. 15 **/ 16 17 #include "cvc4_private.h" 18 19 #ifndef __CVC4__THEORY__DATATYPES__TYPE_ENUMERATOR_H 20 #define __CVC4__THEORY__DATATYPES__TYPE_ENUMERATOR_H 21 22 #include "theory/type_enumerator.h" 23 #include "expr/type_node.h" 24 #include "expr/type.h" 25 #include "expr/kind.h" 26 #include "options/quantifiers_options.h" 27 28 namespace CVC4 { 29 namespace theory { 30 namespace datatypes { 31 32 33 class DatatypesEnumerator : public TypeEnumeratorBase<DatatypesEnumerator> { 34 /** type properties */ 35 TypeEnumeratorProperties * d_tep; 36 /** The datatype we're enumerating */ 37 const Datatype& d_datatype; 38 /** extra cons */ 39 unsigned d_has_debruijn; 40 /** type */ 41 TypeNode d_type; 42 /** The datatype constructor we're currently enumerating */ 43 unsigned d_ctor; 44 /** The "first" constructor to consider; it's non-recursive */ 45 unsigned d_zeroCtor; 46 /** list of type enumerators (one for each type in a selector argument) */ 47 std::map< TypeNode, unsigned > d_te_index; 48 std::vector< TypeEnumerator > d_children; 49 //std::vector< DatatypesEnumerator > d_dt_children; 50 /** terms produced for types */ 51 std::map< TypeNode, std::vector< Node > > d_terms; 52 /** arg type of each selector, for each constructor */ 53 std::vector< std::vector< TypeNode > > d_sel_types; 54 /** current index for each argument, for each constructor */ 55 std::vector< std::vector< unsigned > > d_sel_index; 56 /** current sum of argument indicies for each constructor */ 57 std::vector< int > d_sel_sum; 58 /** current bound on the number of times we can iterate argument enumerators */ 59 unsigned d_size_limit; 60 /** child */ 61 bool d_child_enum; 62 hasCyclesDt(const Datatype & dt)63 bool hasCyclesDt( const Datatype& dt ) { 64 return dt.isRecursiveSingleton( d_type.toType() ) || !dt.isFinite( d_type.toType() ); 65 } hasCycles(TypeNode tn)66 bool hasCycles( TypeNode tn ){ 67 if( tn.isDatatype() ){ 68 const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); 69 return hasCyclesDt( dt ); 70 }else{ 71 return false; 72 } 73 } 74 75 Node getTermEnum( TypeNode tn, unsigned i ); 76 77 bool increment( unsigned index ); 78 79 Node getCurrentTerm( unsigned index ); 80 81 void init(); 82 83 public: 84 DatatypesEnumerator(TypeNode type, TypeEnumeratorProperties* tep = nullptr) 85 : TypeEnumeratorBase<DatatypesEnumerator>(type), 86 d_tep(tep), 87 d_datatype(DatatypeType(type.toType()).getDatatype()), 88 d_type(type) 89 { 90 d_child_enum = false; 91 init(); 92 } 93 DatatypesEnumerator(TypeNode type, 94 bool childEnum, 95 TypeEnumeratorProperties* tep = nullptr) 96 : TypeEnumeratorBase<DatatypesEnumerator>(type), 97 d_tep(tep), 98 d_datatype(DatatypeType(type.toType()).getDatatype()), 99 d_type(type) 100 { 101 d_child_enum = childEnum; 102 init(); 103 } DatatypesEnumerator(const DatatypesEnumerator & de)104 DatatypesEnumerator(const DatatypesEnumerator& de) : 105 TypeEnumeratorBase<DatatypesEnumerator>(de.getType()), 106 d_tep(de.d_tep), 107 d_datatype(de.d_datatype), 108 d_type(de.d_type), 109 d_ctor(de.d_ctor), 110 d_zeroCtor(de.d_zeroCtor) { 111 112 for( std::map< TypeNode, unsigned >::const_iterator it = de.d_te_index.begin(); it != de.d_te_index.end(); ++it ){ 113 d_te_index[it->first] = it->second; 114 } 115 for( std::map< TypeNode, std::vector< Node > >::const_iterator it = de.d_terms.begin(); it != de.d_terms.end(); ++it ){ 116 d_terms[it->first].insert( d_terms[it->first].end(), it->second.begin(), it->second.end() ); 117 } 118 for( unsigned i=0; i<de.d_sel_types.size(); i++ ){ 119 d_sel_types.push_back( std::vector< TypeNode >() ); 120 d_sel_types[i].insert( d_sel_types[i].end(), de.d_sel_types[i].begin(), de.d_sel_types[i].end() ); 121 } 122 for( unsigned i=0; i<de.d_sel_index.size(); i++ ){ 123 d_sel_index.push_back( std::vector< unsigned >() ); 124 d_sel_index[i].insert( d_sel_index[i].end(), de.d_sel_index[i].begin(), de.d_sel_index[i].end() ); 125 } 126 127 d_children.insert( d_children.end(), de.d_children.begin(), de.d_children.end() ); 128 d_sel_sum.insert( d_sel_sum.end(), de.d_sel_sum.begin(), de.d_sel_sum.end() ); 129 d_size_limit = de.d_size_limit; 130 d_has_debruijn = de.d_has_debruijn; 131 d_child_enum = de.d_child_enum; 132 } 133 134 Node operator*() override 135 { 136 Debug("dt-enum-debug") << ": get term " << this << std::endl; 137 if(d_ctor < d_has_debruijn + d_datatype.getNumConstructors()) { 138 return getCurrentTerm( d_ctor ); 139 } else { 140 throw NoMoreValuesException(getType()); 141 } 142 } 143 144 DatatypesEnumerator& operator++() override 145 { 146 Debug("dt-enum-debug") << ": increment " << this << std::endl; 147 unsigned prevSize = d_size_limit; 148 while(d_ctor < d_has_debruijn+d_datatype.getNumConstructors()) { 149 //increment at index 150 while( increment( d_ctor ) ){ 151 Node n = getCurrentTerm( d_ctor ); 152 if( !n.isNull() ){ 153 return *this; 154 } 155 } 156 // Here, we need to step from the current constructor to the next one 157 158 // Find the next constructor (only complicated by the notion of the "zero" constructor 159 d_ctor = (d_ctor == d_zeroCtor) ? 0 : d_ctor + 1; 160 if(d_ctor == d_zeroCtor) { 161 ++d_ctor; 162 } 163 if( d_ctor>=d_has_debruijn+d_datatype.getNumConstructors() ){ 164 //try next size limit as long as new terms were generated at last size, or other cases 165 if( prevSize==d_size_limit || ( d_size_limit==0 && d_datatype.isCodatatype() ) || !d_datatype.isInterpretedFinite( d_type.toType() ) ){ 166 d_size_limit++; 167 d_ctor = d_zeroCtor; 168 for( unsigned i=0; i<d_sel_sum.size(); i++ ){ 169 d_sel_sum[i] = -1; 170 } 171 } 172 } 173 } 174 return *this; 175 } 176 isFinished()177 bool isFinished() override 178 { 179 return d_ctor >= d_has_debruijn+d_datatype.getNumConstructors(); 180 } 181 182 };/* DatatypesEnumerator */ 183 184 }/* CVC4::theory::datatypes namespace */ 185 }/* CVC4::theory namespace */ 186 }/* CVC4 namespace */ 187 188 #endif /* __CVC4__THEORY__DATATYPES__TYPE_ENUMERATOR_H */ 189