Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/datatypes/type_enumerator.cpp	Lines:	168	168	100.0 %
Date:	2021-11-07	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/codatatype_bound_variable.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)
     {
       NodeManager* nm = NodeManager::currentNM();
       ret = nm->mkConst(CodatatypeBoundVariable(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/codatatype_bound_variable.h"
20		#include "expr/dtype_cons.h"
21		#include "theory/datatypes/datatypes_rewriter.h"
22		#include "theory/datatypes/theory_datatypes_utils.h"
23
24		using namespace cvc5;
25		using namespace theory;
26		using namespace datatypes;
27
28	119272	Node DatatypesEnumerator::getTermEnum( TypeNode tn, unsigned i ){
29	238544	Node ret;
30	119272	if( i<d_terms[tn].size() ){
31	103248	ret = d_terms[tn][i];
32		}else{
33	16024	Debug("dt-enum-debug") << "get term enum " << tn << " " << i << std::endl;
34	16024	std::map< TypeNode, unsigned >::iterator it = d_te_index.find( tn );
35		unsigned tei;
36	16024	if( it==d_te_index.end() ){
37		//initialize child enumerator for type
38	4056	tei = d_children.size();
39	4056	d_te_index[tn] = tei;
40	4056	if( tn.isDatatype() && d_has_debruijn ){
41		//must indicate that this is a child enumerator (do not normalize constants for it)
42	78	DatatypesEnumerator * dte = new DatatypesEnumerator( tn, true, d_tep );
43	78	d_children.push_back( TypeEnumerator( dte ) );
44		}else{
45	3978	d_children.push_back( TypeEnumerator( tn, d_tep ) );
46		}
47	4056	d_terms[tn].push_back( *d_children[tei] );
48		}else{
49	11968	tei = it->second;
50		}
51		//enumerate terms until index is reached
52	34408	while( i>=d_terms[tn].size() ){
53	11968	++d_children[tei];
54	11968	if( d_children[tei].isFinished() ){
55	2776	Debug("dt-enum-debug") << "...fail term enum " << tn << " " << i << std::endl;
56	2776	return Node::null();
57		}
58	9192	d_terms[tn].push_back( *d_children[tei] );
59		}
60	13248	Debug("dt-enum-debug") << "...return term enum " << tn << " " << i << " : " << d_terms[tn][i] << std::endl;
61	13248	ret = d_terms[tn][i];
62		}
63	116496	return ret;
64		}
65
66	44248	bool DatatypesEnumerator::increment( unsigned index ){
67	44248	Debug("dt-enum") << "Incrementing " << d_type << " " << d_ctor << " at size " << d_sel_sum[index] << "/" << d_size_limit << std::endl;
68	44248	if( d_sel_sum[index]==-1 ){
69		//first time
70	25118	d_sel_sum[index] = 0;
71		//special case: no children to iterate
72	25118	if( index>=d_has_debruijn && d_sel_types[index].empty() ){
73	9889	Debug("dt-enum") << "...success (nc) = " << (d_size_limit==0) << std::endl;
74	9889	return d_size_limit==0;
75		}else{
76	15229	Debug("dt-enum") << "...success" << std::endl;
77	15229	return true;
78		}
79		}else{
80	19130	unsigned i = 0;
81	32738	while( i < d_sel_index[index].size() ){
82		//increment if the sum of iterations on arguments is less than the limit
83	10610	if( d_sel_sum[index]<(int)d_size_limit ){
84		//also check if child enumerator has enough terms
85	5893	if( !getTermEnum( d_sel_types[index][i], d_sel_index[index][i]+1 ).isNull() ){
86	3806	Debug("dt-enum") << "...success increment child " << i << std::endl;
87	3806	d_sel_index[index][i]++;
88	3806	d_sel_sum[index]++;
89	3806	return true;
90		}
91		}
92	6804	Debug("dt-enum") << "......failed increment child " << i << std::endl;
93		//reset child, iterate next
94	6804	d_sel_sum[index] -= d_sel_index[index][i];
95	6804	d_sel_index[index][i] = 0;
96	6804	i++;
97		}
98	15324	Debug("dt-enum") << "...failure." << std::endl;
99	15324	return false;
100		}
101		}
102
103	69658	Node DatatypesEnumerator::getCurrentTerm(unsigned index)
104		{
105	139316	Debug("dt-enum-debug") << "Get current term at " << index << " " << d_type
106	69658	<< std::endl;
107	139316	Node ret;
108	69658	if (index < d_has_debruijn)
109		{
110	5076	if (d_child_enum)
111		{
112	4004	NodeManager* nm = NodeManager::currentNM();
113	4004	ret = nm->mkConst(CodatatypeBoundVariable(d_type, d_size_limit));
114		}
115		else
116		{
117		// no top-level variables
118	1072	return Node::null();
119		}
120		}
121		else
122		{
123	129164	Debug("dt-enum-debug")
124	64582	<< "Look at constructor " << (index - d_has_debruijn) << std::endl;
125	64582	const DTypeConstructor& ctor = d_datatype[index - d_has_debruijn];
126	64582	Debug("dt-enum-debug") << "Check last term..." << std::endl;
127		// we first check if the last argument (which is forced to make sum of
128		// iterated arguments equal to d_size_limit) is defined
129	128475	Node lc;
130	64582	if (ctor.getNumArgs() > 0)
131		{
132	60146	Assert(index < d_sel_types.size());
133	60146	Assert(ctor.getNumArgs() - 1 < d_sel_types[index].size());
134	60146	lc = getTermEnum(d_sel_types[index][ctor.getNumArgs() - 1],
135	60146	d_size_limit - d_sel_sum[index]);
136	60146	if (lc.isNull())
137		{
138	689	Debug("dt-enum-debug") << "Current infeasible." << std::endl;
139	689	return Node::null();
140		}
141		}
142	63893	Debug("dt-enum-debug") << "Get constructor..." << std::endl;
143	127786	NodeBuilder b(kind::APPLY_CONSTRUCTOR);
144	63893	if (d_datatype.isParametric())
145		{
146	269	NodeManager* nm = NodeManager::currentNM();
147	538	TypeNode typ = ctor.getSpecializedConstructorType(d_type);
148	1345	b << nm->mkNode(kind::APPLY_TYPE_ASCRIPTION,
149	538	nm->mkConst(AscriptionType(typ)),
150	1076	ctor.getConstructor());
151		}
152		else
153		{
154	63624	b << ctor.getConstructor();
155		}
156	63893	Debug("dt-enum-debug") << "Get arguments..." << std::endl;
157	63893	if (ctor.getNumArgs() > 0)
158		{
159	59457	Assert(index < d_sel_types.size());
160	59457	Assert(index < d_sel_index.size());
161	59457	Assert(d_sel_types[index].size() == ctor.getNumArgs());
162	59457	Assert(d_sel_index[index].size() == ctor.getNumArgs() - 1);
163	112690	for (int i = 0; i < (int)(ctor.getNumArgs() - 1); i++)
164		{
165	106466	Node c = getTermEnum(d_sel_types[index][i], d_sel_index[index][i]);
166	53233	Assert(!c.isNull());
167	53233	b << c;
168		}
169	59457	b << lc;
170		}
171	127786	Node nnn = Node(b);
172	63893	Debug("dt-enum-debug") << "Return... " << nnn << std::endl;
173	63893	ret = nnn;
174		}
175
176	67897	if (!d_child_enum && d_has_debruijn)
177		{
178	1683	Node nret = DatatypesRewriter::normalizeCodatatypeConstant(ret);
179	1335	if (nret != ret)
180		{
181	987	if (nret.isNull())
182		{
183	877	Trace("dt-enum-nn") << "Invalid constant : " << ret << std::endl;
184		}
185		else
186		{
187	110	Trace("dt-enum-nn") << "Non-normal constant : " << ret << std::endl;
188	110	Trace("dt-enum-nn") << " ...normal form is : " << nret << std::endl;
189		}
190	987	return Node::null();
191		}
192		}
193
194	66910	return ret;
195		}
196
197	199904	void DatatypesEnumerator::init()
198		{
199	399808	Debug("dt-enum") << "datatype is datatype? " << d_type.isDatatype()
200	199904	<< std::endl;
201	199904	Debug("dt-enum") << "datatype is kind " << d_type.getKind() << std::endl;
202	199904	Debug("dt-enum") << "datatype is " << d_type << std::endl;
203	399808	Debug("dt-enum") << "properties : " << d_datatype.isCodatatype() << " "
204	199904	<< d_datatype.isRecursiveSingleton(d_type);
205	399808	Debug("dt-enum") << " " << d_datatype.getCardinalityClass(d_type)
206	199904	<< std::endl;
207		// Start with the ground term constructed via mkGroundValue, which does
208		// a traversal over the structure of the datatype to find a finite term.
209		// Notice that mkGroundValue may be dependent upon extracting the first
210		// value of type enumerators for other non-datatype subfield types of
211		// this datatype. Since datatypes can not be embedded in non-datatype
212		// types (e.g. (Array D D) cannot be a subfield type of datatype D), this
213		// call is guaranteed to avoid infinite recursion. It is important that we
214		// start with this term, since it has the same shape as the one returned by
215		// TypeNode::mkGroundTerm for d_type, which avoids debug check model
216		// failures.
217	199904	d_zeroTerm = d_datatype.mkGroundValue(d_type);
218		// Only use the zero term if it was successfully constructed. This may
219		// fail for codatatype types whose only values are infinite.
220	199904	d_zeroTermActive = !d_zeroTerm.isNull();
221	199904	if (d_datatype.isCodatatype() && hasCyclesDt(d_datatype))
222		{
223		// start with uninterpreted constant
224	154	d_has_debruijn = 1;
225	154	d_sel_types.push_back(std::vector<TypeNode>());
226	154	d_sel_index.push_back(std::vector<unsigned>());
227	154	d_sel_sum.push_back(-1);
228		}
229		else
230		{
231		// find the "zero" term via mkGroundTerm
232	199750	Debug("dt-enum-debug") << "make ground term..." << std::endl;
233	199750	Debug("dt-enum-debug") << "done : " << d_zeroTerm << std::endl;
234	199750	Assert(d_zeroTerm.getKind() == kind::APPLY_CONSTRUCTOR);
235	199750	d_has_debruijn = 0;
236		}
237	199904	Debug("dt-enum") << "zero term : " << d_zeroTerm << std::endl;
238	199904	d_ctor = 0;
239	1512456	for (unsigned i = 0, ncons = d_datatype.getNumConstructors(); i < ncons; ++i)
240		{
241	1312552	d_sel_types.push_back(std::vector<TypeNode>());
242	1312552	d_sel_index.push_back(std::vector<unsigned>());
243	1312552	d_sel_sum.push_back(-1);
244	1312552	const DTypeConstructor& ctor = d_datatype[i];
245	2625104	TypeNode typ;
246	1312552	if (d_datatype.isParametric())
247		{
248	158	typ = ctor.getSpecializedConstructorType(d_type);
249		}
250	2796629	for (unsigned a = 0; a < ctor.getNumArgs(); ++a)
251		{
252	2968154	TypeNode tn;
253	1484077	if (d_datatype.isParametric())
254		{
255	189	tn = typ[a];
256		}
257		else
258		{
259	1483888	tn = ctor[a].getSelector().getType()[1];
260		}
261	1484077	d_sel_types.back().push_back(tn);
262	1484077	d_sel_index.back().push_back(0);
263		}
264	1312552	if (!d_sel_index.back().empty())
265		{
266	728059	d_sel_index.back().pop_back();
267		}
268		}
269	199904	d_size_limit = 0;
270	199904	if (!d_zeroTermActive)
271		{
272		// Set up initial conditions (should always succeed). Here, we are calling
273		// the increment function of this class, which ensures a term is ready to
274		// read via a dereference of this class. We use the same method for
275		// setting up the first term, if it is not already set up
276		// (d_zeroTermActive) using the increment function, for uniformity.
277	12	++*this;
278		}
279	199904	AlwaysAssert(!isFinished());
280	199904	}
281
282	17538	DatatypesEnumerator& DatatypesEnumerator::operator++()
283		{
284	17538	Debug("dt-enum-debug") << ": increment " << this << std::endl;
285	17538	if (d_zeroTermActive)
286		{
287	2715	d_zeroTermActive = false;
288		}
289	17538	unsigned prevSize = d_size_limit;
290	63452	while (d_ctor < d_has_debruijn + d_datatype.getNumConstructors())
291		{
292		// increment at index
293	48976	while (increment(d_ctor))
294		{
295	26019	Node n = getCurrentTerm(d_ctor);
296	21291	if (!n.isNull())
297		{
298	18543	if (n == d_zeroTerm)
299		{
300	1980	d_zeroTerm = Node::null();
301		}
302		else
303		{
304	16563	return *this;
305		}
306		}
307		}
308		// Here, we need to step from the current constructor to the next one
309
310		// Go to the next constructor
311	22957	d_ctor = d_ctor + 1;
312	22957	if (d_ctor >= d_has_debruijn + d_datatype.getNumConstructors())
313		{
314		// try next size limit as long as new terms were generated at last size,
315		// or other cases
316	18718	if (prevSize == d_size_limit
317	1546	\|\| (d_size_limit == 0 && d_datatype.isCodatatype())
318	20264	\|\| d_datatype.getCardinalityClass(d_type)
319		== CardinalityClass::INFINITE)
320		{
321	8793	d_size_limit++;
322	8793	d_ctor = 0;
323	29814	for (unsigned i = 0; i < d_sel_sum.size(); i++)
324		{
325	21021	d_sel_sum[i] = -1;
326		}
327		}
328		}
329		}
330	975	return *this;
331	31137	}