Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/datatypes/type_enumerator.cpp	Lines:	168	168	100.0 %
Date:	2021-08-14	Branches:	389	798	48.7 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Morgan Deters, Andres Noetzli
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * Enumerators for datatypes.
 */

#include "theory/datatypes/type_enumerator.h"

#include "expr/ascription_type.h"
#include "expr/dtype_cons.h"
#include "theory/datatypes/datatypes_rewriter.h"
#include "theory/datatypes/theory_datatypes_utils.h"

using namespace cvc5;
using namespace theory;
using namespace datatypes;

Node DatatypesEnumerator::getTermEnum( TypeNode tn, unsigned i ){
   Node ret;
   if( i<d_terms[tn].size() ){
     ret = d_terms[tn][i];
   }else{
     Debug("dt-enum-debug") << "get term enum " << tn << " " << i << std::endl;
     std::map< TypeNode, unsigned >::iterator it = d_te_index.find( tn );
     unsigned tei;
     if( it==d_te_index.end() ){
       //initialize child enumerator for type
       tei = d_children.size();
       d_te_index[tn] = tei;
       if( tn.isDatatype() && d_has_debruijn ){
         //must indicate that this is a child enumerator (do not normalize constants for it)
         DatatypesEnumerator * dte = new DatatypesEnumerator( tn, true, d_tep );
         d_children.push_back( TypeEnumerator( dte ) );
       }else{
         d_children.push_back( TypeEnumerator( tn, d_tep ) );
       }
       d_terms[tn].push_back( *d_children[tei] );
     }else{
       tei = it->second;
     }
     //enumerate terms until index is reached
     while( i>=d_terms[tn].size() ){
       ++d_children[tei];
       if( d_children[tei].isFinished() ){
         Debug("dt-enum-debug") << "...fail term enum " << tn << " " << i << std::endl;
         return Node::null();
       }
       d_terms[tn].push_back( *d_children[tei] );
     }
     Debug("dt-enum-debug") << "...return term enum " << tn << " " << i << " : " << d_terms[tn][i] << std::endl;
     ret = d_terms[tn][i];
   }
   return ret;
 }

 bool DatatypesEnumerator::increment( unsigned index ){
   Debug("dt-enum") << "Incrementing " << d_type << " " << d_ctor << " at size " << d_sel_sum[index] << "/" << d_size_limit << std::endl;
   if( d_sel_sum[index]==-1 ){
     //first time
     d_sel_sum[index] = 0;
     //special case: no children to iterate
     if( index>=d_has_debruijn && d_sel_types[index].empty() ){
       Debug("dt-enum") << "...success (nc) = " << (d_size_limit==0) << std::endl;
       return d_size_limit==0;
     }else{
       Debug("dt-enum") << "...success" << std::endl;
       return true;
     }
   }else{
     unsigned i = 0;
     while( i < d_sel_index[index].size() ){
       //increment if the sum of iterations on arguments is less than the limit
       if( d_sel_sum[index]<(int)d_size_limit ){
         //also check if child enumerator has enough terms
         if( !getTermEnum( d_sel_types[index][i], d_sel_index[index][i]+1 ).isNull() ){
           Debug("dt-enum") << "...success increment child " << i << std::endl;
           d_sel_index[index][i]++;
           d_sel_sum[index]++;
           return true;
         }
       }
       Debug("dt-enum") << "......failed increment child " << i << std::endl;
       //reset child, iterate next
       d_sel_sum[index] -= d_sel_index[index][i];
       d_sel_index[index][i] = 0;
       i++;
     }
     Debug("dt-enum") << "...failure." << std::endl;
     return false;
   }
 }

 Node DatatypesEnumerator::getCurrentTerm(unsigned index)
 {
   Debug("dt-enum-debug") << "Get current term at " << index << " " << d_type
                          << std::endl;
   Node ret;
   if (index < d_has_debruijn)
   {
     if (d_child_enum)
     {
       ret = NodeManager::currentNM()->mkConst(
           UninterpretedConstant(d_type, d_size_limit));
     }
     else
     {
       // no top-level variables
       return Node::null();
     }
   }
   else
   {
     Debug("dt-enum-debug")
         << "Look at constructor " << (index - d_has_debruijn) << std::endl;
     const DTypeConstructor& ctor = d_datatype[index - d_has_debruijn];
     Debug("dt-enum-debug") << "Check last term..." << std::endl;
     // we first check if the last argument (which is forced to make sum of
     // iterated arguments equal to d_size_limit) is defined
     Node lc;
     if (ctor.getNumArgs() > 0)
     {
       Assert(index < d_sel_types.size());
       Assert(ctor.getNumArgs() - 1 < d_sel_types[index].size());
       lc = getTermEnum(d_sel_types[index][ctor.getNumArgs() - 1],
                        d_size_limit - d_sel_sum[index]);
       if (lc.isNull())
       {
         Debug("dt-enum-debug") << "Current infeasible." << std::endl;
         return Node::null();
       }
     }
     Debug("dt-enum-debug") << "Get constructor..." << std::endl;
     NodeBuilder b(kind::APPLY_CONSTRUCTOR);
     if (d_datatype.isParametric())
     {
       NodeManager* nm = NodeManager::currentNM();
       TypeNode typ = ctor.getSpecializedConstructorType(d_type);
       b << nm->mkNode(kind::APPLY_TYPE_ASCRIPTION,
                       nm->mkConst(AscriptionType(typ)),
                       ctor.getConstructor());
     }
     else
     {
       b << ctor.getConstructor();
     }
     Debug("dt-enum-debug") << "Get arguments..." << std::endl;
     if (ctor.getNumArgs() > 0)
     {
       Assert(index < d_sel_types.size());
       Assert(index < d_sel_index.size());
       Assert(d_sel_types[index].size() == ctor.getNumArgs());
       Assert(d_sel_index[index].size() == ctor.getNumArgs() - 1);
       for (int i = 0; i < (int)(ctor.getNumArgs() - 1); i++)
       {
         Node c = getTermEnum(d_sel_types[index][i], d_sel_index[index][i]);
         Assert(!c.isNull());
         b << c;
       }
       b << lc;
     }
     Node nnn = Node(b);
     Debug("dt-enum-debug") << "Return... " << nnn << std::endl;
     ret = nnn;
   }

   if (!d_child_enum && d_has_debruijn)
   {
     Node nret = DatatypesRewriter::normalizeCodatatypeConstant(ret);
     if (nret != ret)
     {
       if (nret.isNull())
       {
         Trace("dt-enum-nn") << "Invalid constant : " << ret << std::endl;
       }
       else
       {
         Trace("dt-enum-nn") << "Non-normal constant : " << ret << std::endl;
         Trace("dt-enum-nn") << "  ...normal form is : " << nret << std::endl;
       }
       return Node::null();
     }
   }

   return ret;
 }

 void DatatypesEnumerator::init()
 {
   Debug("dt-enum") << "datatype is datatype? " << d_type.isDatatype()
                    << std::endl;
   Debug("dt-enum") << "datatype is kind " << d_type.getKind() << std::endl;
   Debug("dt-enum") << "datatype is " << d_type << std::endl;
   Debug("dt-enum") << "properties : " << d_datatype.isCodatatype() << " "
                    << d_datatype.isRecursiveSingleton(d_type);
   Debug("dt-enum") << " " << d_datatype.getCardinalityClass(d_type)
                    << std::endl;
   // Start with the ground term constructed via mkGroundValue, which does
   // a traversal over the structure of the datatype to find a finite term.
   // Notice that mkGroundValue may be dependent upon extracting the first
   // value of type enumerators for *other non-datatype* subfield types of
   // this datatype. Since datatypes can not be embedded in non-datatype
   // types (e.g. (Array D D) cannot be a subfield type of datatype D), this
   // call is guaranteed to avoid infinite recursion. It is important that we
   // start with this term, since it has the same shape as the one returned by
   // TypeNode::mkGroundTerm for d_type, which avoids debug check model
   // failures.
   d_zeroTerm = d_datatype.mkGroundValue(d_type);
   // Only use the zero term if it was successfully constructed. This may
   // fail for codatatype types whose only values are infinite.
   d_zeroTermActive = !d_zeroTerm.isNull();
   if (d_datatype.isCodatatype() && hasCyclesDt(d_datatype))
   {
     // start with uninterpreted constant
     d_has_debruijn = 1;
     d_sel_types.push_back(std::vector<TypeNode>());
     d_sel_index.push_back(std::vector<unsigned>());
     d_sel_sum.push_back(-1);
   }
   else
   {
     // find the "zero" term via mkGroundTerm
     Debug("dt-enum-debug") << "make ground term..." << std::endl;
     Debug("dt-enum-debug") << "done : " << d_zeroTerm << std::endl;
     Assert(d_zeroTerm.getKind() == kind::APPLY_CONSTRUCTOR);
     d_has_debruijn = 0;
   }
   Debug("dt-enum") << "zero term : " << d_zeroTerm << std::endl;
   d_ctor = 0;
   for (unsigned i = 0, ncons = d_datatype.getNumConstructors(); i < ncons; ++i)
   {
     d_sel_types.push_back(std::vector<TypeNode>());
     d_sel_index.push_back(std::vector<unsigned>());
     d_sel_sum.push_back(-1);
     const DTypeConstructor& ctor = d_datatype[i];
     TypeNode typ;
     if (d_datatype.isParametric())
     {
       typ = ctor.getSpecializedConstructorType(d_type);
     }
     for (unsigned a = 0; a < ctor.getNumArgs(); ++a)
     {
       TypeNode tn;
       if (d_datatype.isParametric())
       {
         tn = typ[a];
       }
       else
       {
         tn = ctor[a].getSelector().getType()[1];
       }
       d_sel_types.back().push_back(tn);
       d_sel_index.back().push_back(0);
     }
     if (!d_sel_index.back().empty())
     {
       d_sel_index.back().pop_back();
     }
   }
   d_size_limit = 0;
   if (!d_zeroTermActive)
   {
     // Set up initial conditions (should always succeed). Here, we are calling
     // the increment function of this class, which ensures a term is ready to
     // read via a dereference of this class. We use the same method for
     // setting up the first term, if it is not already set up
     // (d_zeroTermActive) using the increment function, for uniformity.
     ++*this;
   }
   AlwaysAssert(!isFinished());
 }

 DatatypesEnumerator& DatatypesEnumerator::operator++()
 {
   Debug("dt-enum-debug") << ": increment " << this << std::endl;
   if (d_zeroTermActive)
   {
     d_zeroTermActive = false;
   }
   unsigned prevSize = d_size_limit;
   while (d_ctor < d_has_debruijn + d_datatype.getNumConstructors())
   {
     // increment at index
     while (increment(d_ctor))
     {
       Node n = getCurrentTerm(d_ctor);
       if (!n.isNull())
       {
         if (n == d_zeroTerm)
         {
           d_zeroTerm = Node::null();
         }
         else
         {
           return *this;
         }
       }
     }
     // Here, we need to step from the current constructor to the next one

     // Go to the next constructor
     d_ctor = d_ctor + 1;
     if (d_ctor >= d_has_debruijn + d_datatype.getNumConstructors())
     {
       // try next size limit as long as new terms were generated at last size,
       // or other cases
       if (prevSize == d_size_limit
           || (d_size_limit == 0 && d_datatype.isCodatatype())
           || d_datatype.getCardinalityClass(d_type)
                  == CardinalityClass::INFINITE)
       {
         d_size_limit++;
         d_ctor = 0;
         for (unsigned i = 0; i < d_sel_sum.size(); i++)
         {
           d_sel_sum[i] = -1;
         }
       }
     }
   }
   return *this;
 }


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Morgan Deters, Andres Noetzli
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		* Enumerators for datatypes.
14		*/
15
16		#include "theory/datatypes/type_enumerator.h"
17
18		#include "expr/ascription_type.h"
19		#include "expr/dtype_cons.h"
20		#include "theory/datatypes/datatypes_rewriter.h"
21		#include "theory/datatypes/theory_datatypes_utils.h"
22
23		using namespace cvc5;
24		using namespace theory;
25		using namespace datatypes;
26
27	111689	Node DatatypesEnumerator::getTermEnum( TypeNode tn, unsigned i ){
28	223378	Node ret;
29	111689	if( i<d_terms[tn].size() ){
30	98023	ret = d_terms[tn][i];
31		}else{
32	13666	Debug("dt-enum-debug") << "get term enum " << tn << " " << i << std::endl;
33	13666	std::map< TypeNode, unsigned >::iterator it = d_te_index.find( tn );
34		unsigned tei;
35	13666	if( it==d_te_index.end() ){
36		//initialize child enumerator for type
37	4001	tei = d_children.size();
38	4001	d_te_index[tn] = tei;
39	4001	if( tn.isDatatype() && d_has_debruijn ){
40		//must indicate that this is a child enumerator (do not normalize constants for it)
41	74	DatatypesEnumerator * dte = new DatatypesEnumerator( tn, true, d_tep );
42	74	d_children.push_back( TypeEnumerator( dte ) );
43		}else{
44	3927	d_children.push_back( TypeEnumerator( tn, d_tep ) );
45		}
46	4001	d_terms[tn].push_back( *d_children[tei] );
47		}else{
48	9665	tei = it->second;
49		}
50		//enumerate terms until index is reached
51	29628	while( i>=d_terms[tn].size() ){
52	9665	++d_children[tei];
53	9665	if( d_children[tei].isFinished() ){
54	1684	Debug("dt-enum-debug") << "...fail term enum " << tn << " " << i << std::endl;
55	1684	return Node::null();
56		}
57	7981	d_terms[tn].push_back( *d_children[tei] );
58		}
59	11982	Debug("dt-enum-debug") << "...return term enum " << tn << " " << i << " : " << d_terms[tn][i] << std::endl;
60	11982	ret = d_terms[tn][i];
61		}
62	110005	return ret;
63		}
64
65	38311	bool DatatypesEnumerator::increment( unsigned index ){
66	38311	Debug("dt-enum") << "Incrementing " << d_type << " " << d_ctor << " at size " << d_sel_sum[index] << "/" << d_size_limit << std::endl;
67	38311	if( d_sel_sum[index]==-1 ){
68		//first time
69	21556	d_sel_sum[index] = 0;
70		//special case: no children to iterate
71	21556	if( index>=d_has_debruijn && d_sel_types[index].empty() ){
72	8685	Debug("dt-enum") << "...success (nc) = " << (d_size_limit==0) << std::endl;
73	8685	return d_size_limit==0;
74		}else{
75	12871	Debug("dt-enum") << "...success" << std::endl;
76	12871	return true;
77		}
78		}else{
79	16755	unsigned i = 0;
80	28105	while( i < d_sel_index[index].size() ){
81		//increment if the sum of iterations on arguments is less than the limit
82	9457	if( d_sel_sum[index]<(int)d_size_limit ){
83		//also check if child enumerator has enough terms
84	4777	if( !getTermEnum( d_sel_types[index][i], d_sel_index[index][i]+1 ).isNull() ){
85	3782	Debug("dt-enum") << "...success increment child " << i << std::endl;
86	3782	d_sel_index[index][i]++;
87	3782	d_sel_sum[index]++;
88	3782	return true;
89		}
90		}
91	5675	Debug("dt-enum") << "......failed increment child " << i << std::endl;
92		//reset child, iterate next
93	5675	d_sel_sum[index] -= d_sel_index[index][i];
94	5675	d_sel_index[index][i] = 0;
95	5675	i++;
96		}
97	12973	Debug("dt-enum") << "...failure." << std::endl;
98	12973	return false;
99		}
100		}
101
102	63428	Node DatatypesEnumerator::getCurrentTerm(unsigned index)
103		{
104	126856	Debug("dt-enum-debug") << "Get current term at " << index << " " << d_type
105	63428	<< std::endl;
106	126856	Node ret;
107	63428	if (index < d_has_debruijn)
108		{
109	2319	if (d_child_enum)
110		{
111	3600	ret = NodeManager::currentNM()->mkConst(
112	3600	UninterpretedConstant(d_type, d_size_limit));
113		}
114		else
115		{
116		// no top-level variables
117	519	return Node::null();
118		}
119		}
120		else
121		{
122	122218	Debug("dt-enum-debug")
123	61109	<< "Look at constructor " << (index - d_has_debruijn) << std::endl;
124	61109	const DTypeConstructor& ctor = d_datatype[index - d_has_debruijn];
125	61109	Debug("dt-enum-debug") << "Check last term..." << std::endl;
126		// we first check if the last argument (which is forced to make sum of
127		// iterated arguments equal to d_size_limit) is defined
128	121529	Node lc;
129	61109	if (ctor.getNumArgs() > 0)
130		{
131	56724	Assert(index < d_sel_types.size());
132	56724	Assert(ctor.getNumArgs() - 1 < d_sel_types[index].size());
133	56724	lc = getTermEnum(d_sel_types[index][ctor.getNumArgs() - 1],
134	56724	d_size_limit - d_sel_sum[index]);
135	56724	if (lc.isNull())
136		{
137	689	Debug("dt-enum-debug") << "Current infeasible." << std::endl;
138	689	return Node::null();
139		}
140		}
141	60420	Debug("dt-enum-debug") << "Get constructor..." << std::endl;
142	120840	NodeBuilder b(kind::APPLY_CONSTRUCTOR);
143	60420	if (d_datatype.isParametric())
144		{
145	260	NodeManager* nm = NodeManager::currentNM();
146	520	TypeNode typ = ctor.getSpecializedConstructorType(d_type);
147	1300	b << nm->mkNode(kind::APPLY_TYPE_ASCRIPTION,
148	520	nm->mkConst(AscriptionType(typ)),
149	1040	ctor.getConstructor());
150		}
151		else
152		{
153	60160	b << ctor.getConstructor();
154		}
155	60420	Debug("dt-enum-debug") << "Get arguments..." << std::endl;
156	60420	if (ctor.getNumArgs() > 0)
157		{
158	56035	Assert(index < d_sel_types.size());
159	56035	Assert(index < d_sel_index.size());
160	56035	Assert(d_sel_types[index].size() == ctor.getNumArgs());
161	56035	Assert(d_sel_index[index].size() == ctor.getNumArgs() - 1);
162	106223	for (int i = 0; i < (int)(ctor.getNumArgs() - 1); i++)
163		{
164	100376	Node c = getTermEnum(d_sel_types[index][i], d_sel_index[index][i]);
165	50188	Assert(!c.isNull());
166	50188	b << c;
167		}
168	56035	b << lc;
169		}
170	120840	Node nnn = Node(b);
171	60420	Debug("dt-enum-debug") << "Return... " << nnn << std::endl;
172	60420	ret = nnn;
173		}
174
175	62220	if (!d_child_enum && d_has_debruijn)
176		{
177	1095	Node nret = DatatypesRewriter::normalizeCodatatypeConstant(ret);
178	765	if (nret != ret)
179		{
180	435	if (nret.isNull())
181		{
182	353	Trace("dt-enum-nn") << "Invalid constant : " << ret << std::endl;
183		}
184		else
185		{
186	82	Trace("dt-enum-nn") << "Non-normal constant : " << ret << std::endl;
187	82	Trace("dt-enum-nn") << " ...normal form is : " << nret << std::endl;
188		}
189	435	return Node::null();
190		}
191		}
192
193	61785	return ret;
194		}
195
196	85049	void DatatypesEnumerator::init()
197		{
198	170098	Debug("dt-enum") << "datatype is datatype? " << d_type.isDatatype()
199	85049	<< std::endl;
200	85049	Debug("dt-enum") << "datatype is kind " << d_type.getKind() << std::endl;
201	85049	Debug("dt-enum") << "datatype is " << d_type << std::endl;
202	170098	Debug("dt-enum") << "properties : " << d_datatype.isCodatatype() << " "
203	85049	<< d_datatype.isRecursiveSingleton(d_type);
204	170098	Debug("dt-enum") << " " << d_datatype.getCardinalityClass(d_type)
205	85049	<< std::endl;
206		// Start with the ground term constructed via mkGroundValue, which does
207		// a traversal over the structure of the datatype to find a finite term.
208		// Notice that mkGroundValue may be dependent upon extracting the first
209		// value of type enumerators for other non-datatype subfield types of
210		// this datatype. Since datatypes can not be embedded in non-datatype
211		// types (e.g. (Array D D) cannot be a subfield type of datatype D), this
212		// call is guaranteed to avoid infinite recursion. It is important that we
213		// start with this term, since it has the same shape as the one returned by
214		// TypeNode::mkGroundTerm for d_type, which avoids debug check model
215		// failures.
216	85049	d_zeroTerm = d_datatype.mkGroundValue(d_type);
217		// Only use the zero term if it was successfully constructed. This may
218		// fail for codatatype types whose only values are infinite.
219	85049	d_zeroTermActive = !d_zeroTerm.isNull();
220	85049	if (d_datatype.isCodatatype() && hasCyclesDt(d_datatype))
221		{
222		// start with uninterpreted constant
223	153	d_has_debruijn = 1;
224	153	d_sel_types.push_back(std::vector<TypeNode>());
225	153	d_sel_index.push_back(std::vector<unsigned>());
226	153	d_sel_sum.push_back(-1);
227		}
228		else
229		{
230		// find the "zero" term via mkGroundTerm
231	84896	Debug("dt-enum-debug") << "make ground term..." << std::endl;
232	84896	Debug("dt-enum-debug") << "done : " << d_zeroTerm << std::endl;
233	84896	Assert(d_zeroTerm.getKind() == kind::APPLY_CONSTRUCTOR);
234	84896	d_has_debruijn = 0;
235		}
236	85049	Debug("dt-enum") << "zero term : " << d_zeroTerm << std::endl;
237	85049	d_ctor = 0;
238	598374	for (unsigned i = 0, ncons = d_datatype.getNumConstructors(); i < ncons; ++i)
239		{
240	513325	d_sel_types.push_back(std::vector<TypeNode>());
241	513325	d_sel_index.push_back(std::vector<unsigned>());
242	513325	d_sel_sum.push_back(-1);
243	513325	const DTypeConstructor& ctor = d_datatype[i];
244	1026650	TypeNode typ;
245	513325	if (d_datatype.isParametric())
246		{
247	148	typ = ctor.getSpecializedConstructorType(d_type);
248		}
249	1120928	for (unsigned a = 0; a < ctor.getNumArgs(); ++a)
250		{
251	1215206	TypeNode tn;
252	607603	if (d_datatype.isParametric())
253		{
254	177	tn = typ[a];
255		}
256		else
257		{
258	607426	tn = ctor[a].getSelector().getType()[1];
259		}
260	607603	d_sel_types.back().push_back(tn);
261	607603	d_sel_index.back().push_back(0);
262		}
263	513325	if (!d_sel_index.back().empty())
264		{
265	298347	d_sel_index.back().pop_back();
266		}
267		}
268	85049	d_size_limit = 0;
269	85049	if (!d_zeroTermActive)
270		{
271		// Set up initial conditions (should always succeed). Here, we are calling
272		// the increment function of this class, which ensures a term is ready to
273		// read via a dereference of this class. We use the same method for
274		// setting up the first term, if it is not already set up
275		// (d_zeroTermActive) using the increment function, for uniformity.
276	6	++*this;
277		}
278	85049	AlwaysAssert(!isFinished());
279	85049	}
280
281	16256	DatatypesEnumerator& DatatypesEnumerator::operator++()
282		{
283	16256	Debug("dt-enum-debug") << ": increment " << this << std::endl;
284	16256	if (d_zeroTermActive)
285		{
286	2685	d_zeroTermActive = false;
287		}
288	16256	unsigned prevSize = d_size_limit;
289	55120	while (d_ctor < d_has_debruijn + d_datatype.getNumConstructors())
290		{
291		// increment at index
292	41909	while (increment(d_ctor))
293		{
294	22477	Node n = getCurrentTerm(d_ctor);
295	18879	if (!n.isNull())
296		{
297	17236	if (n == d_zeroTerm)
298		{
299	1955	d_zeroTerm = Node::null();
300		}
301		else
302		{
303	15281	return *this;
304		}
305		}
306		}
307		// Here, we need to step from the current constructor to the next one
308
309		// Go to the next constructor
310	19432	d_ctor = d_ctor + 1;
311	19432	if (d_ctor >= d_has_debruijn + d_datatype.getNumConstructors())
312		{
313		// try next size limit as long as new terms were generated at last size,
314		// or other cases
315	16316	if (prevSize == d_size_limit
316	999	\|\| (d_size_limit == 0 && d_datatype.isCodatatype())
317	17315	\|\| d_datatype.getCardinalityClass(d_type)
318		== CardinalityClass::INFINITE)
319		{
320	7591	d_size_limit++;
321	7591	d_ctor = 0;
322	25111	for (unsigned i = 0; i < d_sel_sum.size(); i++)
323		{
324	17520	d_sel_sum[i] = -1;
325		}
326		}
327		}
328		}
329	975	return *this;
330	29340	}