1 /********************* */
2 /*! \file type_enumerator.h
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
12 ** \brief An enumerator for datatypes
14 ** An enumerator for datatypes.
17 #include "cvc4_private.h"
19 #ifndef CVC4__THEORY__DATATYPES__TYPE_ENUMERATOR_H
20 #define CVC4__THEORY__DATATYPES__TYPE_ENUMERATOR_H
22 #include "expr/dtype.h"
23 #include "expr/kind.h"
24 #include "expr/type_node.h"
25 #include "options/quantifiers_options.h"
26 #include "theory/type_enumerator.h"
33 class DatatypesEnumerator
: public TypeEnumeratorBase
<DatatypesEnumerator
> {
34 /** type properties */
35 TypeEnumeratorProperties
* d_tep
;
36 /** The datatype we're enumerating */
37 const DType
& d_datatype
;
39 unsigned d_has_debruijn
;
42 /** The datatype constructor we're currently enumerating */
44 /** The first term to consider in the enumeration */
46 /** Whether we are currently considering the above term */
47 bool d_zeroTermActive
;
48 /** list of type enumerators (one for each type in a selector argument) */
49 std::map
< TypeNode
, unsigned > d_te_index
;
50 std::vector
< TypeEnumerator
> d_children
;
51 //std::vector< DatatypesEnumerator > d_dt_children;
52 /** terms produced for types */
53 std::map
< TypeNode
, std::vector
< Node
> > d_terms
;
54 /** arg type of each selector, for each constructor */
55 std::vector
< std::vector
< TypeNode
> > d_sel_types
;
56 /** current index for each argument, for each constructor */
57 std::vector
< std::vector
< unsigned > > d_sel_index
;
58 /** current sum of argument indicies for each constructor */
59 std::vector
< int > d_sel_sum
;
60 /** current bound on the number of times we can iterate argument enumerators */
61 unsigned d_size_limit
;
65 bool hasCyclesDt(const DType
& dt
)
67 return dt
.isRecursiveSingleton(d_type
) || !dt
.isFinite(d_type
);
69 bool hasCycles( TypeNode tn
){
70 if( tn
.isDatatype() ){
71 const DType
& dt
= tn
.getDType();
72 return hasCyclesDt( dt
);
78 Node
getTermEnum( TypeNode tn
, unsigned i
);
80 bool increment( unsigned index
);
82 Node
getCurrentTerm( unsigned index
);
87 DatatypesEnumerator(TypeNode type
, TypeEnumeratorProperties
* tep
= nullptr)
88 : TypeEnumeratorBase
<DatatypesEnumerator
>(type
),
90 d_datatype(type
.getDType()),
93 d_zeroTermActive(false)
98 DatatypesEnumerator(TypeNode type
,
100 TypeEnumeratorProperties
* tep
= nullptr)
101 : TypeEnumeratorBase
<DatatypesEnumerator
>(type
),
103 d_datatype(type
.getDType()),
106 d_zeroTermActive(false)
108 d_child_enum
= childEnum
;
111 DatatypesEnumerator(const DatatypesEnumerator
& de
)
112 : TypeEnumeratorBase
<DatatypesEnumerator
>(de
.getType()),
114 d_datatype(de
.d_datatype
),
117 d_zeroTerm(de
.d_zeroTerm
),
118 d_zeroTermActive(de
.d_zeroTermActive
)
120 for( std::map
< TypeNode
, unsigned >::const_iterator it
= de
.d_te_index
.begin(); it
!= de
.d_te_index
.end(); ++it
){
121 d_te_index
[it
->first
] = it
->second
;
123 for( std::map
< TypeNode
, std::vector
< Node
> >::const_iterator it
= de
.d_terms
.begin(); it
!= de
.d_terms
.end(); ++it
){
124 d_terms
[it
->first
].insert( d_terms
[it
->first
].end(), it
->second
.begin(), it
->second
.end() );
126 for( unsigned i
=0; i
<de
.d_sel_types
.size(); i
++ ){
127 d_sel_types
.push_back( std::vector
< TypeNode
>() );
128 d_sel_types
[i
].insert( d_sel_types
[i
].end(), de
.d_sel_types
[i
].begin(), de
.d_sel_types
[i
].end() );
130 for( unsigned i
=0; i
<de
.d_sel_index
.size(); i
++ ){
131 d_sel_index
.push_back( std::vector
< unsigned >() );
132 d_sel_index
[i
].insert( d_sel_index
[i
].end(), de
.d_sel_index
[i
].begin(), de
.d_sel_index
[i
].end() );
135 d_children
.insert( d_children
.end(), de
.d_children
.begin(), de
.d_children
.end() );
136 d_sel_sum
.insert( d_sel_sum
.end(), de
.d_sel_sum
.begin(), de
.d_sel_sum
.end() );
137 d_size_limit
= de
.d_size_limit
;
138 d_has_debruijn
= de
.d_has_debruijn
;
139 d_child_enum
= de
.d_child_enum
;
142 Node
operator*() override
144 Debug("dt-enum-debug") << ": get term " << this << std::endl
;
145 if (d_zeroTermActive
)
149 else if (d_ctor
< d_has_debruijn
+ d_datatype
.getNumConstructors())
151 return getCurrentTerm( d_ctor
);
153 throw NoMoreValuesException(getType());
156 DatatypesEnumerator
& operator++() override
;
158 bool isFinished() override
160 return d_ctor
>= d_has_debruijn
+d_datatype
.getNumConstructors();
163 };/* DatatypesEnumerator */
165 }/* CVC4::theory::datatypes namespace */
166 }/* CVC4::theory namespace */
167 }/* CVC4 namespace */
169 #endif /* CVC4__THEORY__DATATYPES__TYPE_ENUMERATOR_H */