Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/datatypes/type_enumerator.cpp	Lines:	168	168	100.0 %
Date:	2021-09-29	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	41942	Node DatatypesEnumerator::getTermEnum( TypeNode tn, unsigned i ){
28	83884	Node ret;
29	41942	if( i<d_terms[tn].size() ){
30	34801	ret = d_terms[tn][i];
31		}else{
32	7141	Debug("dt-enum-debug") << "get term enum " << tn << " " << i << std::endl;
33	7141	std::map< TypeNode, unsigned >::iterator it = d_te_index.find( tn );
34		unsigned tei;
35	7141	if( it==d_te_index.end() ){
36		//initialize child enumerator for type
37	2281	tei = d_children.size();
38	2281	d_te_index[tn] = tei;
39	2281	if( tn.isDatatype() && d_has_debruijn ){
40		//must indicate that this is a child enumerator (do not normalize constants for it)
41	62	DatatypesEnumerator * dte = new DatatypesEnumerator( tn, true, d_tep );
42	62	d_children.push_back( TypeEnumerator( dte ) );
43		}else{
44	2219	d_children.push_back( TypeEnumerator( tn, d_tep ) );
45		}
46	2281	d_terms[tn].push_back( *d_children[tei] );
47		}else{
48	4860	tei = it->second;
49		}
50		//enumerate terms until index is reached
51	13985	while( i>=d_terms[tn].size() ){
52	4860	++d_children[tei];
53	4860	if( d_children[tei].isFinished() ){
54	1438	Debug("dt-enum-debug") << "...fail term enum " << tn << " " << i << std::endl;
55	1438	return Node::null();
56		}
57	3422	d_terms[tn].push_back( *d_children[tei] );
58		}
59	5703	Debug("dt-enum-debug") << "...return term enum " << tn << " " << i << " : " << d_terms[tn][i] << std::endl;
60	5703	ret = d_terms[tn][i];
61		}
62	40504	return ret;
63		}
64
65	18921	bool DatatypesEnumerator::increment( unsigned index ){
66	18921	Debug("dt-enum") << "Incrementing " << d_type << " " << d_ctor << " at size " << d_sel_sum[index] << "/" << d_size_limit << std::endl;
67	18921	if( d_sel_sum[index]==-1 ){
68		//first time
69	10961	d_sel_sum[index] = 0;
70		//special case: no children to iterate
71	10961	if( index>=d_has_debruijn && d_sel_types[index].empty() ){
72	4662	Debug("dt-enum") << "...success (nc) = " << (d_size_limit==0) << std::endl;
73	4662	return d_size_limit==0;
74		}else{
75	6299	Debug("dt-enum") << "...success" << std::endl;
76	6299	return true;
77		}
78		}else{
79	7960	unsigned i = 0;
80	12778	while( i < d_sel_index[index].size() ){
81		//increment if the sum of iterations on arguments is less than the limit
82	3588	if( d_sel_sum[index]<(int)d_size_limit ){
83		//also check if child enumerator has enough terms
84	1934	if( !getTermEnum( d_sel_types[index][i], d_sel_index[index][i]+1 ).isNull() ){
85	1179	Debug("dt-enum") << "...success increment child " << i << std::endl;
86	1179	d_sel_index[index][i]++;
87	1179	d_sel_sum[index]++;
88	1179	return true;
89		}
90		}
91	2409	Debug("dt-enum") << "......failed increment child " << i << std::endl;
92		//reset child, iterate next
93	2409	d_sel_sum[index] -= d_sel_index[index][i];
94	2409	d_sel_index[index][i] = 0;
95	2409	i++;
96		}
97	6781	Debug("dt-enum") << "...failure." << std::endl;
98	6781	return false;
99		}
100		}
101
102	27620	Node DatatypesEnumerator::getCurrentTerm(unsigned index)
103		{
104	55240	Debug("dt-enum-debug") << "Get current term at " << index << " " << d_type
105	27620	<< std::endl;
106	55240	Node ret;
107	27620	if (index < d_has_debruijn)
108		{
109	1737	if (d_child_enum)
110		{
111	2688	ret = NodeManager::currentNM()->mkConst(
112	2688	UninterpretedConstant(d_type, d_size_limit));
113		}
114		else
115		{
116		// no top-level variables
117	393	return Node::null();
118		}
119		}
120		else
121		{
122	51766	Debug("dt-enum-debug")
123	25883	<< "Look at constructor " << (index - d_has_debruijn) << std::endl;
124	25883	const DTypeConstructor& ctor = d_datatype[index - d_has_debruijn];
125	25883	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	51083	Node lc;
129	25883	if (ctor.getNumArgs() > 0)
130		{
131	22130	Assert(index < d_sel_types.size());
132	22130	Assert(ctor.getNumArgs() - 1 < d_sel_types[index].size());
133	22130	lc = getTermEnum(d_sel_types[index][ctor.getNumArgs() - 1],
134	22130	d_size_limit - d_sel_sum[index]);
135	22130	if (lc.isNull())
136		{
137	683	Debug("dt-enum-debug") << "Current infeasible." << std::endl;
138	683	return Node::null();
139		}
140		}
141	25200	Debug("dt-enum-debug") << "Get constructor..." << std::endl;
142	50400	NodeBuilder b(kind::APPLY_CONSTRUCTOR);
143	25200	if (d_datatype.isParametric())
144		{
145	222	NodeManager* nm = NodeManager::currentNM();
146	444	TypeNode typ = ctor.getSpecializedConstructorType(d_type);
147	1110	b << nm->mkNode(kind::APPLY_TYPE_ASCRIPTION,
148	444	nm->mkConst(AscriptionType(typ)),
149	888	ctor.getConstructor());
150		}
151		else
152		{
153	24978	b << ctor.getConstructor();
154		}
155	25200	Debug("dt-enum-debug") << "Get arguments..." << std::endl;
156	25200	if (ctor.getNumArgs() > 0)
157		{
158	21447	Assert(index < d_sel_types.size());
159	21447	Assert(index < d_sel_index.size());
160	21447	Assert(d_sel_types[index].size() == ctor.getNumArgs());
161	21447	Assert(d_sel_index[index].size() == ctor.getNumArgs() - 1);
162	39325	for (int i = 0; i < (int)(ctor.getNumArgs() - 1); i++)
163		{
164	35756	Node c = getTermEnum(d_sel_types[index][i], d_sel_index[index][i]);
165	17878	Assert(!c.isNull());
166	17878	b << c;
167		}
168	21447	b << lc;
169		}
170	50400	Node nnn = Node(b);
171	25200	Debug("dt-enum-debug") << "Return... " << nnn << std::endl;
172	25200	ret = nnn;
173		}
174
175	26544	if (!d_child_enum && d_has_debruijn)
176		{
177	879	Node nret = DatatypesRewriter::normalizeCodatatypeConstant(ret);
178	601	if (nret != ret)
179		{
180	323	if (nret.isNull())
181		{
182	259	Trace("dt-enum-nn") << "Invalid constant : " << ret << std::endl;
183		}
184		else
185		{
186	64	Trace("dt-enum-nn") << "Non-normal constant : " << ret << std::endl;
187	64	Trace("dt-enum-nn") << " ...normal form is : " << nret << std::endl;
188		}
189	323	return Node::null();
190		}
191		}
192
193	26221	return ret;
194		}
195
196	109133	void DatatypesEnumerator::init()
197		{
198	218266	Debug("dt-enum") << "datatype is datatype? " << d_type.isDatatype()
199	109133	<< std::endl;
200	109133	Debug("dt-enum") << "datatype is kind " << d_type.getKind() << std::endl;
201	109133	Debug("dt-enum") << "datatype is " << d_type << std::endl;
202	218266	Debug("dt-enum") << "properties : " << d_datatype.isCodatatype() << " "
203	109133	<< d_datatype.isRecursiveSingleton(d_type);
204	218266	Debug("dt-enum") << " " << d_datatype.getCardinalityClass(d_type)
205	109133	<< 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	109133	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	109133	d_zeroTermActive = !d_zeroTerm.isNull();
220	109133	if (d_datatype.isCodatatype() && hasCyclesDt(d_datatype))
221		{
222		// start with uninterpreted constant
223	98	d_has_debruijn = 1;
224	98	d_sel_types.push_back(std::vector<TypeNode>());
225	98	d_sel_index.push_back(std::vector<unsigned>());
226	98	d_sel_sum.push_back(-1);
227		}
228		else
229		{
230		// find the "zero" term via mkGroundTerm
231	109035	Debug("dt-enum-debug") << "make ground term..." << std::endl;
232	109035	Debug("dt-enum-debug") << "done : " << d_zeroTerm << std::endl;
233	109035	Assert(d_zeroTerm.getKind() == kind::APPLY_CONSTRUCTOR);
234	109035	d_has_debruijn = 0;
235		}
236	109133	Debug("dt-enum") << "zero term : " << d_zeroTerm << std::endl;
237	109133	d_ctor = 0;
238	772113	for (unsigned i = 0, ncons = d_datatype.getNumConstructors(); i < ncons; ++i)
239		{
240	662980	d_sel_types.push_back(std::vector<TypeNode>());
241	662980	d_sel_index.push_back(std::vector<unsigned>());
242	662980	d_sel_sum.push_back(-1);
243	662980	const DTypeConstructor& ctor = d_datatype[i];
244	1325960	TypeNode typ;
245	662980	if (d_datatype.isParametric())
246		{
247	136	typ = ctor.getSpecializedConstructorType(d_type);
248		}
249	1425074	for (unsigned a = 0; a < ctor.getNumArgs(); ++a)
250		{
251	1524188	TypeNode tn;
252	762094	if (d_datatype.isParametric())
253		{
254	167	tn = typ[a];
255		}
256		else
257		{
258	761927	tn = ctor[a].getSelector().getType()[1];
259		}
260	762094	d_sel_types.back().push_back(tn);
261	762094	d_sel_index.back().push_back(0);
262		}
263	662980	if (!d_sel_index.back().empty())
264		{
265	367346	d_sel_index.back().pop_back();
266		}
267		}
268	109133	d_size_limit = 0;
269	109133	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	109133	AlwaysAssert(!isFinished());
279	109133	}
280
281	7328	DatatypesEnumerator& DatatypesEnumerator::operator++()
282		{
283	7328	Debug("dt-enum-debug") << ": increment " << this << std::endl;
284	7328	if (d_zeroTermActive)
285		{
286	1705	d_zeroTermActive = false;
287		}
288	7328	unsigned prevSize = d_size_limit;
289	26906	while (d_ctor < d_has_debruijn + d_datatype.getNumConstructors())
290		{
291		// increment at index
292	21673	while (increment(d_ctor))
293		{
294	11884	Node n = getCurrentTerm(d_ctor);
295	9132	if (!n.isNull())
296		{
297	7733	if (n == d_zeroTerm)
298		{
299	1353	d_zeroTerm = Node::null();
300		}
301		else
302		{
303	6380	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	9789	d_ctor = d_ctor + 1;
311	9789	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	8294	if (prevSize == d_size_limit
316	859	\|\| (d_size_limit == 0 && d_datatype.isCodatatype())
317	9153	\|\| d_datatype.getCardinalityClass(d_type)
318		== CardinalityClass::INFINITE)
319		{
320	3608	d_size_limit++;
321	3608	d_ctor = 0;
322	11896	for (unsigned i = 0; i < d_sel_sum.size(); i++)
323		{
324	8288	d_sel_sum[i] = -1;
325		}
326		}
327		}
328		}
329	948	return *this;
330	22746	}