Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/datatypes/type_enumerator.cpp	Lines:	168	168	100.0 %
Date:	2021-05-22	Branches:	389	800	48.6 %


/******************************************************************************
 * 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 "expr/dtype_cons.h"
#include "theory/datatypes/type_enumerator.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 "expr/dtype_cons.h"
17		#include "theory/datatypes/type_enumerator.h"
18		#include "theory/datatypes/datatypes_rewriter.h"
19		#include "theory/datatypes/theory_datatypes_utils.h"
20
21		using namespace cvc5;
22		using namespace theory;
23		using namespace datatypes;
24
25	220456	Node DatatypesEnumerator::getTermEnum( TypeNode tn, unsigned i ){
26	440912	Node ret;
27	220456	if( i<d_terms[tn].size() ){
28	202727	ret = d_terms[tn][i];
29		}else{
30	17729	Debug("dt-enum-debug") << "get term enum " << tn << " " << i << std::endl;
31	17729	std::map< TypeNode, unsigned >::iterator it = d_te_index.find( tn );
32		unsigned tei;
33	17729	if( it==d_te_index.end() ){
34		//initialize child enumerator for type
35	6185	tei = d_children.size();
36	6185	d_te_index[tn] = tei;
37	6185	if( tn.isDatatype() && d_has_debruijn ){
38		//must indicate that this is a child enumerator (do not normalize constants for it)
39	74	DatatypesEnumerator * dte = new DatatypesEnumerator( tn, true, d_tep );
40	74	d_children.push_back( TypeEnumerator( dte ) );
41		}else{
42	6111	d_children.push_back( TypeEnumerator( tn, d_tep ) );
43		}
44	6185	d_terms[tn].push_back( *d_children[tei] );
45		}else{
46	11544	tei = it->second;
47		}
48		//enumerate terms until index is reached
49	37465	while( i>=d_terms[tn].size() ){
50	11544	++d_children[tei];
51	11544	if( d_children[tei].isFinished() ){
52	1676	Debug("dt-enum-debug") << "...fail term enum " << tn << " " << i << std::endl;
53	1676	return Node::null();
54		}
55	9868	d_terms[tn].push_back( *d_children[tei] );
56		}
57	16053	Debug("dt-enum-debug") << "...return term enum " << tn << " " << i << " : " << d_terms[tn][i] << std::endl;
58	16053	ret = d_terms[tn][i];
59		}
60	218780	return ret;
61		}
62
63	52730	bool DatatypesEnumerator::increment( unsigned index ){
64	52730	Debug("dt-enum") << "Incrementing " << d_type << " " << d_ctor << " at size " << d_sel_sum[index] << "/" << d_size_limit << std::endl;
65	52730	if( d_sel_sum[index]==-1 ){
66		//first time
67	26668	d_sel_sum[index] = 0;
68		//special case: no children to iterate
69	26668	if( index>=d_has_debruijn && d_sel_types[index].empty() ){
70	9357	Debug("dt-enum") << "...success (nc) = " << (d_size_limit==0) << std::endl;
71	9357	return d_size_limit==0;
72		}else{
73	17311	Debug("dt-enum") << "...success" << std::endl;
74	17311	return true;
75		}
76		}else{
77	26062	unsigned i = 0;
78	49308	while( i < d_sel_index[index].size() ){
79		//increment if the sum of iterations on arguments is less than the limit
80	20898	if( d_sel_sum[index]<(int)d_size_limit ){
81		//also check if child enumerator has enough terms
82	10270	if( !getTermEnum( d_sel_types[index][i], d_sel_index[index][i]+1 ).isNull() ){
83	9275	Debug("dt-enum") << "...success increment child " << i << std::endl;
84	9275	d_sel_index[index][i]++;
85	9275	d_sel_sum[index]++;
86	9275	return true;
87		}
88		}
89	11623	Debug("dt-enum") << "......failed increment child " << i << std::endl;
90		//reset child, iterate next
91	11623	d_sel_sum[index] -= d_sel_index[index][i];
92	11623	d_sel_index[index][i] = 0;
93	11623	i++;
94		}
95	16787	Debug("dt-enum") << "...failure." << std::endl;
96	16787	return false;
97		}
98		}
99
100	102681	Node DatatypesEnumerator::getCurrentTerm(unsigned index)
101		{
102	205362	Debug("dt-enum-debug") << "Get current term at " << index << " " << d_type
103	102681	<< std::endl;
104	205362	Node ret;
105	102681	if (index < d_has_debruijn)
106		{
107	2319	if (d_child_enum)
108		{
109	3600	ret = NodeManager::currentNM()->mkConst(
110	3600	UninterpretedConstant(d_type, d_size_limit));
111		}
112		else
113		{
114		// no top-level variables
115	519	return Node::null();
116		}
117		}
118		else
119		{
120	200724	Debug("dt-enum-debug")
121	100362	<< "Look at constructor " << (index - d_has_debruijn) << std::endl;
122	100362	const DTypeConstructor& ctor = d_datatype[index - d_has_debruijn];
123	100362	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
126	200043	Node lc;
127	100362	if (ctor.getNumArgs() > 0)
128		{
129	95665	Assert(index < d_sel_types.size());
130	95665	Assert(ctor.getNumArgs() - 1 < d_sel_types[index].size());
131	95665	lc = getTermEnum(d_sel_types[index][ctor.getNumArgs() - 1],
132	95665	d_size_limit - d_sel_sum[index]);
133	95665	if (lc.isNull())
134		{
135	681	Debug("dt-enum-debug") << "Current infeasible." << std::endl;
136	681	return Node::null();
137		}
138		}
139	99681	Debug("dt-enum-debug") << "Get constructor..." << std::endl;
140	199362	NodeBuilder b(kind::APPLY_CONSTRUCTOR);
141	99681	if (d_datatype.isParametric())
142		{
143	282	NodeManager* nm = NodeManager::currentNM();
144	564	TypeNode typ = ctor.getSpecializedConstructorType(d_type);
145	1410	b << nm->mkNode(kind::APPLY_TYPE_ASCRIPTION,
146	564	nm->mkConst(AscriptionType(typ)),
147	1128	ctor.getConstructor());
148		}
149		else
150		{
151	99399	b << ctor.getConstructor();
152		}
153	99681	Debug("dt-enum-debug") << "Get arguments..." << std::endl;
154	99681	if (ctor.getNumArgs() > 0)
155		{
156	94984	Assert(index < d_sel_types.size());
157	94984	Assert(index < d_sel_index.size());
158	94984	Assert(d_sel_types[index].size() == ctor.getNumArgs());
159	94984	Assert(d_sel_index[index].size() == ctor.getNumArgs() - 1);
160	209505	for (int i = 0; i < (int)(ctor.getNumArgs() - 1); i++)
161		{
162	229042	Node c = getTermEnum(d_sel_types[index][i], d_sel_index[index][i]);
163	114521	Assert(!c.isNull());
164	114521	b << c;
165		}
166	94984	b << lc;
167		}
168	199362	Node nnn = Node(b);
169	99681	Debug("dt-enum-debug") << "Return... " << nnn << std::endl;
170	99681	ret = nnn;
171		}
172
173	101481	if (!d_child_enum && d_has_debruijn)
174		{
175	1095	Node nret = DatatypesRewriter::normalizeCodatatypeConstant(ret);
176	765	if (nret != ret)
177		{
178	435	if (nret.isNull())
179		{
180	353	Trace("dt-enum-nn") << "Invalid constant : " << ret << std::endl;
181		}
182		else
183		{
184	82	Trace("dt-enum-nn") << "Non-normal constant : " << ret << std::endl;
185	82	Trace("dt-enum-nn") << " ...normal form is : " << nret << std::endl;
186		}
187	435	return Node::null();
188		}
189		}
190
191	101046	return ret;
192		}
193
194	95951	void DatatypesEnumerator::init()
195		{
196	191902	Debug("dt-enum") << "datatype is datatype? " << d_type.isDatatype()
197	95951	<< std::endl;
198	95951	Debug("dt-enum") << "datatype is kind " << d_type.getKind() << std::endl;
199	95951	Debug("dt-enum") << "datatype is " << d_type << std::endl;
200	191902	Debug("dt-enum") << "properties : " << d_datatype.isCodatatype() << " "
201	95951	<< d_datatype.isRecursiveSingleton(d_type);
202	191902	Debug("dt-enum") << " " << d_datatype.getCardinalityClass(d_type)
203	95951	<< std::endl;
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
213		// failures.
214	95951	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	95951	d_zeroTermActive = !d_zeroTerm.isNull();
218	95951	if (d_datatype.isCodatatype() && hasCyclesDt(d_datatype))
219		{
220		// start with uninterpreted constant
221	154	d_has_debruijn = 1;
222	154	d_sel_types.push_back(std::vector<TypeNode>());
223	154	d_sel_index.push_back(std::vector<unsigned>());
224	154	d_sel_sum.push_back(-1);
225		}
226		else
227		{
228		// find the "zero" term via mkGroundTerm
229	95797	Debug("dt-enum-debug") << "make ground term..." << std::endl;
230	95797	Debug("dt-enum-debug") << "done : " << d_zeroTerm << std::endl;
231	95797	Assert(d_zeroTerm.getKind() == kind::APPLY_CONSTRUCTOR);
232	95797	d_has_debruijn = 0;
233		}
234	95951	Debug("dt-enum") << "zero term : " << d_zeroTerm << std::endl;
235	95951	d_ctor = 0;
236	687005	for (unsigned i = 0, ncons = d_datatype.getNumConstructors(); i < ncons; ++i)
237		{
238	591054	d_sel_types.push_back(std::vector<TypeNode>());
239	591054	d_sel_index.push_back(std::vector<unsigned>());
240	591054	d_sel_sum.push_back(-1);
241	591054	const DTypeConstructor& ctor = d_datatype[i];
242	1182108	TypeNode typ;
243	591054	if (d_datatype.isParametric())
244		{
245	164	typ = ctor.getSpecializedConstructorType(d_type);
246		}
247	1322812	for (unsigned a = 0; a < ctor.getNumArgs(); ++a)
248		{
249	1463516	TypeNode tn;
250	731758	if (d_datatype.isParametric())
251		{
252	197	tn = typ[a];
253		}
254		else
255		{
256	731561	tn = ctor[a].getSelector().getType()[1];
257		}
258	731758	d_sel_types.back().push_back(tn);
259	731758	d_sel_index.back().push_back(0);
260		}
261	591054	if (!d_sel_index.back().empty())
262		{
263	361540	d_sel_index.back().pop_back();
264		}
265		}
266	95951	d_size_limit = 0;
267	95951	if (!d_zeroTermActive)
268		{
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.
274	6	++*this;
275		}
276	95951	AlwaysAssert(!isFinished());
277	95951	}
278
279	26093	DatatypesEnumerator& DatatypesEnumerator::operator++()
280		{
281	26093	Debug("dt-enum-debug") << ": increment " << this << std::endl;
282	26093	if (d_zeroTermActive)
283		{
284	3597	d_zeroTermActive = false;
285		}
286	26093	unsigned prevSize = d_size_limit;
287	73293	while (d_ctor < d_has_debruijn + d_datatype.getNumConstructors())
288		{
289		// increment at index
290	56710	while (increment(d_ctor))
291		{
292	33110	Node n = getCurrentTerm(d_ctor);
293	29130	if (!n.isNull())
294		{
295	27495	if (n == d_zeroTerm)
296		{
297	2345	d_zeroTerm = Node::null();
298		}
299		else
300		{
301	25150	return *this;
302		}
303		}
304		}
305		// Here, we need to step from the current constructor to the next one
306
307		// Go to the next constructor
308	23600	d_ctor = d_ctor + 1;
309	23600	if (d_ctor >= d_has_debruijn + d_datatype.getNumConstructors())
310		{
311		// try next size limit as long as new terms were generated at last size,
312		// or other cases
313	17700	if (prevSize == d_size_limit
314	967	\|\| (d_size_limit == 0 && d_datatype.isCodatatype())
315	18667	\|\| d_datatype.getCardinalityClass(d_type)
316		== CardinalityClass::INFINITE)
317		{
318	8315	d_size_limit++;
319	8315	d_ctor = 0;
320	29251	for (unsigned i = 0; i < d_sel_sum.size(); i++)
321		{
322	20936	d_sel_sum[i] = -1;
323		}
324		}
325		}
326		}
327	943	return *this;
328	28194	}