1 /********************* */
2 /*! \file type_enumerator.cpp
4 ** Top contributors (to current version):
5 ** Andrew Reynolds, Morgan Deters, Andres Noetzli
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 Enumerators for datatypes
14 ** Enumerators for datatypes.
17 #include "theory/datatypes/type_enumerator.h"
18 #include "theory/datatypes/datatypes_rewriter.h"
19 #include "theory/datatypes/theory_datatypes_utils.h"
22 using namespace theory
;
23 using namespace datatypes
;
25 Node
DatatypesEnumerator::getTermEnum( TypeNode tn
, unsigned i
){
27 if( i
<d_terms
[tn
].size() ){
30 Debug("dt-enum-debug") << "get term enum " << tn
<< " " << i
<< std::endl
;
31 std::map
< TypeNode
, unsigned >::iterator it
= d_te_index
.find( tn
);
33 if( it
==d_te_index
.end() ){
34 //initialize child enumerator for type
35 tei
= d_children
.size();
37 if( tn
.isDatatype() && d_has_debruijn
){
38 //must indicate that this is a child enumerator (do not normalize constants for it)
39 DatatypesEnumerator
* dte
= new DatatypesEnumerator( tn
, true, d_tep
);
40 d_children
.push_back( TypeEnumerator( dte
) );
42 d_children
.push_back( TypeEnumerator( tn
, d_tep
) );
44 d_terms
[tn
].push_back( *d_children
[tei
] );
48 //enumerate terms until index is reached
49 while( i
>=d_terms
[tn
].size() ){
51 if( d_children
[tei
].isFinished() ){
52 Debug("dt-enum-debug") << "...fail term enum " << tn
<< " " << i
<< std::endl
;
55 d_terms
[tn
].push_back( *d_children
[tei
] );
57 Debug("dt-enum-debug") << "...return term enum " << tn
<< " " << i
<< " : " << d_terms
[tn
][i
] << std::endl
;
63 bool DatatypesEnumerator::increment( unsigned index
){
64 Debug("dt-enum") << "Incrementing " << d_type
<< " " << d_ctor
<< " at size " << d_sel_sum
[index
] << "/" << d_size_limit
<< std::endl
;
65 if( d_sel_sum
[index
]==-1 ){
68 //special case: no children to iterate
69 if( index
>=d_has_debruijn
&& d_sel_types
[index
].empty() ){
70 Debug("dt-enum") << "...success (nc) = " << (d_size_limit
==0) << std::endl
;
71 return d_size_limit
==0;
73 Debug("dt-enum") << "...success" << std::endl
;
78 while( i
< d_sel_index
[index
].size() ){
79 //increment if the sum of iterations on arguments is less than the limit
80 if( d_sel_sum
[index
]<(int)d_size_limit
){
81 //also check if child enumerator has enough terms
82 if( !getTermEnum( d_sel_types
[index
][i
], d_sel_index
[index
][i
]+1 ).isNull() ){
83 Debug("dt-enum") << "...success increment child " << i
<< std::endl
;
84 d_sel_index
[index
][i
]++;
89 Debug("dt-enum") << "......failed increment child " << i
<< std::endl
;
90 //reset child, iterate next
91 d_sel_sum
[index
] -= d_sel_index
[index
][i
];
92 d_sel_index
[index
][i
] = 0;
95 Debug("dt-enum") << "...failure." << std::endl
;
100 Node
DatatypesEnumerator::getCurrentTerm(unsigned index
)
102 Debug("dt-enum-debug") << "Get current term at " << index
<< " " << d_type
105 if (index
< d_has_debruijn
)
109 ret
= NodeManager::currentNM()->mkConst(
110 UninterpretedConstant(d_type
, d_size_limit
));
114 // no top-level variables
120 Debug("dt-enum-debug")
121 << "Look at constructor " << (index
- d_has_debruijn
) << std::endl
;
122 const DTypeConstructor
& ctor
= d_datatype
[index
- d_has_debruijn
];
123 Debug("dt-enum-debug") << "Check last term..." << std::endl
;
124 // we first check if the last argument (which is forced to make sum of
125 // iterated arguments equal to d_size_limit) is defined
127 if (ctor
.getNumArgs() > 0)
129 Assert(index
< d_sel_types
.size());
130 Assert(ctor
.getNumArgs() - 1 < d_sel_types
[index
].size());
131 lc
= getTermEnum(d_sel_types
[index
][ctor
.getNumArgs() - 1],
132 d_size_limit
- d_sel_sum
[index
]);
135 Debug("dt-enum-debug") << "Current infeasible." << std::endl
;
139 Debug("dt-enum-debug") << "Get constructor..." << std::endl
;
140 NodeBuilder
<> b(kind::APPLY_CONSTRUCTOR
);
141 if (d_datatype
.isParametric())
143 NodeManager
* nm
= NodeManager::currentNM();
144 TypeNode typ
= ctor
.getSpecializedConstructorType(d_type
);
145 b
<< nm
->mkNode(kind::APPLY_TYPE_ASCRIPTION
,
146 nm
->mkConst(AscriptionType(typ
)),
147 ctor
.getConstructor());
151 b
<< ctor
.getConstructor();
153 Debug("dt-enum-debug") << "Get arguments..." << std::endl
;
154 if (ctor
.getNumArgs() > 0)
156 Assert(index
< d_sel_types
.size());
157 Assert(index
< d_sel_index
.size());
158 Assert(d_sel_types
[index
].size() == ctor
.getNumArgs());
159 Assert(d_sel_index
[index
].size() == ctor
.getNumArgs() - 1);
160 for (int i
= 0; i
< (int)(ctor
.getNumArgs() - 1); i
++)
162 Node c
= getTermEnum(d_sel_types
[index
][i
], d_sel_index
[index
][i
]);
169 Debug("dt-enum-debug") << "Return... " << nnn
<< std::endl
;
173 if (!d_child_enum
&& d_has_debruijn
)
175 Node nret
= DatatypesRewriter::normalizeCodatatypeConstant(ret
);
180 Trace("dt-enum-nn") << "Invalid constant : " << ret
<< std::endl
;
184 Trace("dt-enum-nn") << "Non-normal constant : " << ret
<< std::endl
;
185 Trace("dt-enum-nn") << " ...normal form is : " << nret
<< std::endl
;
194 void DatatypesEnumerator::init()
196 Debug("dt-enum") << "datatype is datatype? " << d_type
.isDatatype()
198 Debug("dt-enum") << "datatype is kind " << d_type
.getKind() << std::endl
;
199 Debug("dt-enum") << "datatype is " << d_type
<< std::endl
;
200 Debug("dt-enum") << "properties : " << d_datatype
.isCodatatype() << " "
201 << d_datatype
.isRecursiveSingleton(d_type
);
202 Debug("dt-enum") << " " << d_datatype
.isInterpretedFinite(d_type
)
204 // Start with the ground term constructed via mkGroundValue, which does
205 // a traversal over the structure of the datatype to find a finite term.
206 // Notice that mkGroundValue may be dependent upon extracting the first
207 // value of type enumerators for *other non-datatype* subfield types of
208 // this datatype. Since datatypes can not be embedded in non-datatype
209 // types (e.g. (Array D D) cannot be a subfield type of datatype D), this
210 // call is guaranteed to avoid infinite recursion. It is important that we
211 // start with this term, since it has the same shape as the one returned by
212 // TypeNode::mkGroundTerm for d_type, which avoids debug check model
214 d_zeroTerm
= d_datatype
.mkGroundValue(d_type
);
215 // Only use the zero term if it was successfully constructed. This may
216 // fail for codatatype types whose only values are infinite.
217 d_zeroTermActive
= !d_zeroTerm
.isNull();
218 if (d_datatype
.isCodatatype() && hasCyclesDt(d_datatype
))
220 // start with uninterpreted constant
222 d_sel_types
.push_back(std::vector
<TypeNode
>());
223 d_sel_index
.push_back(std::vector
<unsigned>());
224 d_sel_sum
.push_back(-1);
228 // find the "zero" term via mkGroundTerm
229 Debug("dt-enum-debug") << "make ground term..." << std::endl
;
230 Debug("dt-enum-debug") << "done : " << d_zeroTerm
<< std::endl
;
231 Assert(d_zeroTerm
.getKind() == kind::APPLY_CONSTRUCTOR
);
234 Debug("dt-enum") << "zero term : " << d_zeroTerm
<< std::endl
;
236 for (unsigned i
= 0, ncons
= d_datatype
.getNumConstructors(); i
< ncons
; ++i
)
238 d_sel_types
.push_back(std::vector
<TypeNode
>());
239 d_sel_index
.push_back(std::vector
<unsigned>());
240 d_sel_sum
.push_back(-1);
241 const DTypeConstructor
& ctor
= d_datatype
[i
];
243 if (d_datatype
.isParametric())
245 typ
= ctor
.getSpecializedConstructorType(d_type
);
247 for (unsigned a
= 0; a
< ctor
.getNumArgs(); ++a
)
250 if (d_datatype
.isParametric())
256 tn
= ctor
[a
].getSelector().getType()[1];
258 d_sel_types
.back().push_back(tn
);
259 d_sel_index
.back().push_back(0);
261 if (!d_sel_index
.back().empty())
263 d_sel_index
.back().pop_back();
267 if (!d_zeroTermActive
)
269 // Set up initial conditions (should always succeed). Here, we are calling
270 // the increment function of this class, which ensures a term is ready to
271 // read via a dereference of this class. We use the same method for
272 // setting up the first term, if it is not already set up
273 // (d_zeroTermActive) using the increment function, for uniformity.
276 AlwaysAssert(!isFinished());
279 DatatypesEnumerator
& DatatypesEnumerator::operator++()
281 Debug("dt-enum-debug") << ": increment " << this << std::endl
;
282 if (d_zeroTermActive
)
284 d_zeroTermActive
= false;
286 unsigned prevSize
= d_size_limit
;
287 while (d_ctor
< d_has_debruijn
+ d_datatype
.getNumConstructors())
289 // increment at index
290 while (increment(d_ctor
))
292 Node n
= getCurrentTerm(d_ctor
);
297 d_zeroTerm
= Node::null();
305 // Here, we need to step from the current constructor to the next one
307 // Go to the next constructor
309 if (d_ctor
>= d_has_debruijn
+ d_datatype
.getNumConstructors())
311 // try next size limit as long as new terms were generated at last size,
313 if (prevSize
== d_size_limit
314 || (d_size_limit
== 0 && d_datatype
.isCodatatype())
315 || !d_datatype
.isInterpretedFinite(d_type
))
319 for (unsigned i
= 0; i
< d_sel_sum
.size(); i
++)