1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Tim King, Morgan Deters |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
7 |
|
* Copyright (c) 2009-2021 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. |
11 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* An enumerator for datatypes. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "cvc5_private.h" |
17 |
|
|
18 |
|
#ifndef CVC5__THEORY__DATATYPES__TYPE_ENUMERATOR_H |
19 |
|
#define CVC5__THEORY__DATATYPES__TYPE_ENUMERATOR_H |
20 |
|
|
21 |
|
#include "expr/dtype.h" |
22 |
|
#include "expr/kind.h" |
23 |
|
#include "expr/type_node.h" |
24 |
|
#include "expr/uninterpreted_constant.h" |
25 |
|
#include "options/quantifiers_options.h" |
26 |
|
#include "theory/type_enumerator.h" |
27 |
|
|
28 |
|
namespace cvc5 { |
29 |
|
namespace theory { |
30 |
|
namespace datatypes { |
31 |
|
|
32 |
|
|
33 |
180912 |
class DatatypesEnumerator : public TypeEnumeratorBase<DatatypesEnumerator> { |
34 |
|
/** type properties */ |
35 |
|
TypeEnumeratorProperties * d_tep; |
36 |
|
/** The datatype we're enumerating */ |
37 |
|
const DType& 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 term to consider in the enumeration */ |
45 |
|
Node d_zeroTerm; |
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; |
62 |
|
/** child */ |
63 |
|
bool d_child_enum; |
64 |
|
|
65 |
153 |
bool hasCyclesDt(const DType& dt) |
66 |
|
{ |
67 |
459 |
return dt.isRecursiveSingleton(d_type) |
68 |
612 |
|| dt.getCardinalityClass(d_type) == CardinalityClass::INFINITE; |
69 |
|
} |
70 |
|
bool hasCycles( TypeNode tn ){ |
71 |
|
if( tn.isDatatype() ){ |
72 |
|
const DType& dt = tn.getDType(); |
73 |
|
return hasCyclesDt( dt ); |
74 |
|
}else{ |
75 |
|
return false; |
76 |
|
} |
77 |
|
} |
78 |
|
|
79 |
|
Node getTermEnum( TypeNode tn, unsigned i ); |
80 |
|
|
81 |
|
bool increment( unsigned index ); |
82 |
|
|
83 |
|
Node getCurrentTerm( unsigned index ); |
84 |
|
|
85 |
|
void init(); |
86 |
|
|
87 |
|
public: |
88 |
84975 |
DatatypesEnumerator(TypeNode type, TypeEnumeratorProperties* tep = nullptr) |
89 |
84975 |
: TypeEnumeratorBase<DatatypesEnumerator>(type), |
90 |
|
d_tep(tep), |
91 |
84975 |
d_datatype(type.getDType()), |
92 |
|
d_type(type), |
93 |
|
d_ctor(0), |
94 |
169950 |
d_zeroTermActive(false) |
95 |
|
{ |
96 |
84975 |
d_child_enum = false; |
97 |
84975 |
init(); |
98 |
84975 |
} |
99 |
74 |
DatatypesEnumerator(TypeNode type, |
100 |
|
bool childEnum, |
101 |
|
TypeEnumeratorProperties* tep = nullptr) |
102 |
74 |
: TypeEnumeratorBase<DatatypesEnumerator>(type), |
103 |
|
d_tep(tep), |
104 |
74 |
d_datatype(type.getDType()), |
105 |
|
d_type(type), |
106 |
|
d_ctor(0), |
107 |
148 |
d_zeroTermActive(false) |
108 |
|
{ |
109 |
74 |
d_child_enum = childEnum; |
110 |
74 |
init(); |
111 |
74 |
} |
112 |
5407 |
DatatypesEnumerator(const DatatypesEnumerator& de) |
113 |
16221 |
: TypeEnumeratorBase<DatatypesEnumerator>(de.getType()), |
114 |
5407 |
d_tep(de.d_tep), |
115 |
5407 |
d_datatype(de.d_datatype), |
116 |
|
d_type(de.d_type), |
117 |
5407 |
d_ctor(de.d_ctor), |
118 |
|
d_zeroTerm(de.d_zeroTerm), |
119 |
32442 |
d_zeroTermActive(de.d_zeroTermActive) |
120 |
|
{ |
121 |
5724 |
for( std::map< TypeNode, unsigned >::const_iterator it = de.d_te_index.begin(); it != de.d_te_index.end(); ++it ){ |
122 |
317 |
d_te_index[it->first] = it->second; |
123 |
|
} |
124 |
5724 |
for( std::map< TypeNode, std::vector< Node > >::const_iterator it = de.d_terms.begin(); it != de.d_terms.end(); ++it ){ |
125 |
317 |
d_terms[it->first].insert( d_terms[it->first].end(), it->second.begin(), it->second.end() ); |
126 |
|
} |
127 |
30328 |
for( unsigned i=0; i<de.d_sel_types.size(); i++ ){ |
128 |
24921 |
d_sel_types.push_back( std::vector< TypeNode >() ); |
129 |
24921 |
d_sel_types[i].insert( d_sel_types[i].end(), de.d_sel_types[i].begin(), de.d_sel_types[i].end() ); |
130 |
|
} |
131 |
30328 |
for( unsigned i=0; i<de.d_sel_index.size(); i++ ){ |
132 |
24921 |
d_sel_index.push_back( std::vector< unsigned >() ); |
133 |
24921 |
d_sel_index[i].insert( d_sel_index[i].end(), de.d_sel_index[i].begin(), de.d_sel_index[i].end() ); |
134 |
|
} |
135 |
|
|
136 |
5407 |
d_children.insert( d_children.end(), de.d_children.begin(), de.d_children.end() ); |
137 |
5407 |
d_sel_sum.insert( d_sel_sum.end(), de.d_sel_sum.begin(), de.d_sel_sum.end() ); |
138 |
5407 |
d_size_limit = de.d_size_limit; |
139 |
5407 |
d_has_debruijn = de.d_has_debruijn; |
140 |
5407 |
d_child_enum = de.d_child_enum; |
141 |
5407 |
} |
142 |
|
|
143 |
216756 |
Node operator*() override |
144 |
|
{ |
145 |
216756 |
Debug("dt-enum-debug") << ": get term " << this << std::endl; |
146 |
216756 |
if (d_zeroTermActive) |
147 |
|
{ |
148 |
171257 |
return d_zeroTerm; |
149 |
|
} |
150 |
45499 |
else if (d_ctor < d_has_debruijn + d_datatype.getNumConstructors()) |
151 |
|
{ |
152 |
44549 |
return getCurrentTerm( d_ctor ); |
153 |
|
} |
154 |
950 |
throw NoMoreValuesException(getType()); |
155 |
|
} |
156 |
|
|
157 |
|
DatatypesEnumerator& operator++() override; |
158 |
|
|
159 |
318249 |
bool isFinished() override |
160 |
|
{ |
161 |
318249 |
return d_ctor >= d_has_debruijn+d_datatype.getNumConstructors(); |
162 |
|
} |
163 |
|
|
164 |
|
};/* DatatypesEnumerator */ |
165 |
|
|
166 |
|
} // namespace datatypes |
167 |
|
} // namespace theory |
168 |
|
} // namespace cvc5 |
169 |
|
|
170 |
|
#endif /* CVC5__THEORY__DATATYPES__TYPE_ENUMERATOR_H */ |