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

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