1 /********************* */
2 /*! \file type_enumerator.cpp
3 ** \verbatim
4 ** Top contributors (to current version):
5 ** Andrew Reynolds, Morgan Deters
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2019 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 "theory/datatypes/type_enumerator.h"
18 #include "theory/datatypes/datatypes_rewriter.h"
19
20 using namespace CVC4;
21 using namespace theory;
22 using namespace datatypes;
23
getTermEnum(TypeNode tn,unsigned i)24 Node DatatypesEnumerator::getTermEnum( TypeNode tn, unsigned i ){
25 Node ret;
26 if( i<d_terms[tn].size() ){
27 ret = d_terms[tn][i];
28 }else{
29 Debug("dt-enum-debug") << "get term enum " << tn << " " << i << std::endl;
30 std::map< TypeNode, unsigned >::iterator it = d_te_index.find( tn );
31 unsigned tei;
32 if( it==d_te_index.end() ){
33 //initialize child enumerator for type
34 tei = d_children.size();
35 d_te_index[tn] = tei;
36 if( tn.isDatatype() && d_has_debruijn ){
37 //must indicate that this is a child enumerator (do not normalize constants for it)
38 DatatypesEnumerator * dte = new DatatypesEnumerator( tn, true, d_tep );
39 d_children.push_back( TypeEnumerator( dte ) );
40 }else{
41 d_children.push_back( TypeEnumerator( tn, d_tep ) );
42 }
43 d_terms[tn].push_back( *d_children[tei] );
44 }else{
45 tei = it->second;
46 }
47 //enumerate terms until index is reached
48 while( i>=d_terms[tn].size() ){
49 ++d_children[tei];
50 if( d_children[tei].isFinished() ){
51 Debug("dt-enum-debug") << "...fail term enum " << tn << " " << i << std::endl;
52 return Node::null();
53 }
54 d_terms[tn].push_back( *d_children[tei] );
55 }
56 Debug("dt-enum-debug") << "...return term enum " << tn << " " << i << " : " << d_terms[tn][i] << std::endl;
57 ret = d_terms[tn][i];
58 }
59 return ret;
60 }
61
increment(unsigned index)62 bool DatatypesEnumerator::increment( unsigned index ){
63 Debug("dt-enum") << "Incrementing " << d_type << " " << d_ctor << " at size " << d_sel_sum[index] << "/" << d_size_limit << std::endl;
64 if( d_sel_sum[index]==-1 ){
65 //first time
66 d_sel_sum[index] = 0;
67 //special case: no children to iterate
68 if( index>=d_has_debruijn && d_sel_types[index].empty() ){
69 Debug("dt-enum") << "...success (nc) = " << (d_size_limit==0) << std::endl;
70 return d_size_limit==0;
71 }else{
72 Debug("dt-enum") << "...success" << std::endl;
73 return true;
74 }
75 }else{
76 unsigned i = 0;
77 while( i < d_sel_index[index].size() ){
78 //increment if the sum of iterations on arguments is less than the limit
79 if( d_sel_sum[index]<(int)d_size_limit ){
80 //also check if child enumerator has enough terms
81 if( !getTermEnum( d_sel_types[index][i], d_sel_index[index][i]+1 ).isNull() ){
82 Debug("dt-enum") << "...success increment child " << i << std::endl;
83 d_sel_index[index][i]++;
84 d_sel_sum[index]++;
85 return true;
86 }
87 }
88 Debug("dt-enum") << "......failed increment child " << i << std::endl;
89 //reset child, iterate next
90 d_sel_sum[index] -= d_sel_index[index][i];
91 d_sel_index[index][i] = 0;
92 i++;
93 }
94 Debug("dt-enum") << "...failure." << std::endl;
95 return false;
96 }
97 }
98
getCurrentTerm(unsigned index)99 Node DatatypesEnumerator::getCurrentTerm( unsigned index ){
100 Debug("dt-enum-debug") << "Get current term at " << index << " " << d_type << std::endl;
101 Node ret;
102 if( index<d_has_debruijn ){
103 if( d_child_enum ){
104 ret = NodeManager::currentNM()->mkConst(UninterpretedConstant(d_type.toType(), d_size_limit));
105 }else{
106 //no top-level variables
107 return Node::null();
108 }
109 }else{
110 Debug("dt-enum-debug") << "Look at constructor " << (index - d_has_debruijn) << std::endl;
111 DatatypeConstructor ctor = d_datatype[index - d_has_debruijn];
112 Debug("dt-enum-debug") << "Check last term..." << std::endl;
113 //we first check if the last argument (which is forced to make sum of iterated arguments equal to d_size_limit) is defined
114 Node lc;
115 if( ctor.getNumArgs()>0 ){
116 Assert( index<d_sel_types.size() );
117 Assert( ctor.getNumArgs()-1<d_sel_types[index].size() );
118 lc = getTermEnum( d_sel_types[index][ctor.getNumArgs()-1], d_size_limit - d_sel_sum[index] );
119 if( lc.isNull() ){
120 Debug("dt-enum-debug") << "Current infeasible." << std::endl;
121 return Node::null();
122 }
123 }
124 Debug("dt-enum-debug") << "Get constructor..." << std::endl;
125 NodeBuilder<> b(kind::APPLY_CONSTRUCTOR);
126 Type typ;
127 if( d_datatype.isParametric() ){
128 typ = ctor.getSpecializedConstructorType(d_type.toType());
129 b << NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION,
130 NodeManager::currentNM()->mkConst(AscriptionType(typ)), Node::fromExpr( ctor.getConstructor() ) );
131 }else{
132 b << ctor.getConstructor();
133 }
134 Debug("dt-enum-debug") << "Get arguments..." << std::endl;
135 if( ctor.getNumArgs()>0 ){
136 Assert( index<d_sel_types.size() );
137 Assert( index<d_sel_index.size() );
138 Assert( d_sel_types[index].size()==ctor.getNumArgs() );
139 Assert( d_sel_index[index].size()==ctor.getNumArgs()-1 );
140 for( int i=0; i<(int)(ctor.getNumArgs()-1); i++ ){
141 Node c = getTermEnum( d_sel_types[index][i], d_sel_index[index][i] );
142 Assert( !c.isNull() );
143 b << c;
144 }
145 b << lc;
146 }
147 Node nnn = Node(b);
148 Debug("dt-enum-debug") << "Return... " << nnn << std::endl;
149 ret = nnn;
150 }
151
152 if( !d_child_enum && d_has_debruijn ){
153 Node nret = DatatypesRewriter::normalizeCodatatypeConstant( ret );
154 if( nret!=ret ){
155 if( nret.isNull() ){
156 Trace("dt-enum-nn") << "Invalid constant : " << ret << std::endl;
157 }else{
158 Trace("dt-enum-nn") << "Non-normal constant : " << ret << std::endl;
159 Trace("dt-enum-nn") << " ...normal form is : " << nret << std::endl;
160 }
161 return Node::null();
162 }
163 }
164
165 return ret;
166 }
167
init()168 void DatatypesEnumerator::init(){
169 //Assert(type.isDatatype());
170 Debug("dt-enum") << "datatype is datatype? " << d_type.isDatatype() << std::endl;
171 Debug("dt-enum") << "datatype is kind " << d_type.getKind() << std::endl;
172 Debug("dt-enum") << "datatype is " << d_type << std::endl;
173 Debug("dt-enum") << "properties : " << d_datatype.isCodatatype() << " " << d_datatype.isRecursiveSingleton( d_type.toType() );
174 Debug("dt-enum") << " " << d_datatype.isInterpretedFinite( d_type.toType() ) << std::endl;
175
176 if( d_datatype.isCodatatype() && hasCyclesDt( d_datatype ) ){
177 //start with uninterpreted constant
178 d_zeroCtor = 0;
179 d_has_debruijn = 1;
180 d_sel_types.push_back( std::vector< TypeNode >() );
181 d_sel_index.push_back( std::vector< unsigned >() );
182 d_sel_sum.push_back( -1 );
183 }else{
184 // find the "zero" constructor via mkGroundTerm
185 Debug("dt-enum-debug") << "make ground term..." << std::endl;
186 Node t = d_type.mkGroundTerm();
187 Debug("dt-enum-debug") << "done : " << t << std::endl;
188 Assert( t.getKind()==kind::APPLY_CONSTRUCTOR );
189 // start with the constructor for which a ground term is constructed
190 d_zeroCtor = datatypes::DatatypesRewriter::indexOf(t.getOperator());
191 d_has_debruijn = 0;
192 }
193 Debug("dt-enum") << "zero ctor : " << d_zeroCtor << std::endl;
194 d_ctor = d_zeroCtor;
195 for( unsigned i=0; i<d_datatype.getNumConstructors(); ++i ){
196 d_sel_types.push_back( std::vector< TypeNode >() );
197 d_sel_index.push_back( std::vector< unsigned >() );
198 d_sel_sum.push_back( -1 );
199 DatatypeConstructor ctor = d_datatype[i];
200 Type typ;
201 if( d_datatype.isParametric() ){
202 typ = ctor.getSpecializedConstructorType(d_type.toType());
203 }
204 for( unsigned a = 0; a < ctor.getNumArgs(); ++a ){
205 TypeNode tn;
206 if( d_datatype.isParametric() ){
207 tn = TypeNode::fromType( typ )[a];
208 }else{
209 tn = Node::fromExpr(ctor[a].getSelector()).getType()[1];
210 }
211 d_sel_types.back().push_back( tn );
212 d_sel_index.back().push_back( 0 );
213 }
214 if( !d_sel_index.back().empty() ){
215 d_sel_index.back().pop_back();
216 }
217 }
218 d_size_limit = 0;
219 //set up initial conditions (should always succeed)
220 ++*this; //increment( d_ctor );
221 AlwaysAssert( !isFinished() );
222 }
223
224