1 /*********************                                                        */
2 /*! \file type_enumerator.h
3  ** \verbatim
4  ** Top contributors (to current version):
5  **   Andrew Reynolds, Morgan Deters, Tim King
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 An enumerator for datatypes
13  **
14  ** An enumerator for datatypes.
15  **/
16 
17 #include "cvc4_private.h"
18 
19 #ifndef __CVC4__THEORY__DATATYPES__TYPE_ENUMERATOR_H
20 #define __CVC4__THEORY__DATATYPES__TYPE_ENUMERATOR_H
21 
22 #include "theory/type_enumerator.h"
23 #include "expr/type_node.h"
24 #include "expr/type.h"
25 #include "expr/kind.h"
26 #include "options/quantifiers_options.h"
27 
28 namespace CVC4 {
29 namespace theory {
30 namespace datatypes {
31 
32 
33 class DatatypesEnumerator : public TypeEnumeratorBase<DatatypesEnumerator> {
34   /** type properties */
35   TypeEnumeratorProperties * d_tep;
36   /** The datatype we're enumerating */
37   const Datatype& d_datatype;
38   /** extra cons */
39   unsigned d_has_debruijn;
40   /** type */
41   TypeNode d_type;
42   /** The datatype constructor we're currently enumerating */
43   unsigned d_ctor;
44   /** The "first" constructor to consider; it's non-recursive */
45   unsigned d_zeroCtor;
46   /** list of type enumerators (one for each type in a selector argument) */
47   std::map< TypeNode, unsigned > d_te_index;
48   std::vector< TypeEnumerator > d_children;
49   //std::vector< DatatypesEnumerator > d_dt_children;
50   /** terms produced for types */
51   std::map< TypeNode, std::vector< Node > > d_terms;
52   /** arg type of each selector, for each constructor */
53   std::vector< std::vector< TypeNode > > d_sel_types;
54   /** current index for each argument, for each constructor */
55   std::vector< std::vector< unsigned > > d_sel_index;
56   /** current sum of argument indicies for each constructor */
57   std::vector< int > d_sel_sum;
58   /** current bound on the number of times we can iterate argument enumerators */
59   unsigned d_size_limit;
60   /** child */
61   bool d_child_enum;
62 
hasCyclesDt(const Datatype & dt)63   bool hasCyclesDt( const Datatype& dt ) {
64     return dt.isRecursiveSingleton( d_type.toType() ) || !dt.isFinite( d_type.toType() );
65   }
hasCycles(TypeNode tn)66   bool hasCycles( TypeNode tn ){
67     if( tn.isDatatype() ){
68       const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
69       return hasCyclesDt( dt );
70     }else{
71       return false;
72     }
73   }
74 
75   Node getTermEnum( TypeNode tn, unsigned i );
76 
77   bool increment( unsigned index );
78 
79   Node getCurrentTerm( unsigned index );
80 
81   void init();
82 
83  public:
84   DatatypesEnumerator(TypeNode type, TypeEnumeratorProperties* tep = nullptr)
85       : TypeEnumeratorBase<DatatypesEnumerator>(type),
86         d_tep(tep),
87         d_datatype(DatatypeType(type.toType()).getDatatype()),
88         d_type(type)
89   {
90     d_child_enum = false;
91     init();
92   }
93   DatatypesEnumerator(TypeNode type,
94                       bool childEnum,
95                       TypeEnumeratorProperties* tep = nullptr)
96       : TypeEnumeratorBase<DatatypesEnumerator>(type),
97         d_tep(tep),
98         d_datatype(DatatypeType(type.toType()).getDatatype()),
99         d_type(type)
100   {
101     d_child_enum = childEnum;
102     init();
103   }
DatatypesEnumerator(const DatatypesEnumerator & de)104   DatatypesEnumerator(const DatatypesEnumerator& de) :
105     TypeEnumeratorBase<DatatypesEnumerator>(de.getType()),
106     d_tep(de.d_tep),
107     d_datatype(de.d_datatype),
108     d_type(de.d_type),
109     d_ctor(de.d_ctor),
110     d_zeroCtor(de.d_zeroCtor) {
111 
112     for( std::map< TypeNode, unsigned >::const_iterator it = de.d_te_index.begin(); it != de.d_te_index.end(); ++it ){
113       d_te_index[it->first] = it->second;
114     }
115     for( std::map< TypeNode, std::vector< Node > >::const_iterator it = de.d_terms.begin(); it != de.d_terms.end(); ++it ){
116       d_terms[it->first].insert( d_terms[it->first].end(), it->second.begin(), it->second.end() );
117     }
118     for( unsigned i=0; i<de.d_sel_types.size(); i++ ){
119       d_sel_types.push_back( std::vector< TypeNode >() );
120       d_sel_types[i].insert( d_sel_types[i].end(), de.d_sel_types[i].begin(), de.d_sel_types[i].end() );
121     }
122     for( unsigned i=0; i<de.d_sel_index.size(); i++ ){
123       d_sel_index.push_back( std::vector< unsigned >() );
124       d_sel_index[i].insert( d_sel_index[i].end(), de.d_sel_index[i].begin(), de.d_sel_index[i].end() );
125     }
126 
127     d_children.insert( d_children.end(), de.d_children.begin(), de.d_children.end() );
128     d_sel_sum.insert( d_sel_sum.end(), de.d_sel_sum.begin(), de.d_sel_sum.end() );
129     d_size_limit = de.d_size_limit;
130     d_has_debruijn = de.d_has_debruijn;
131     d_child_enum = de.d_child_enum;
132   }
133 
134   Node operator*() override
135   {
136     Debug("dt-enum-debug") << ": get term " << this << std::endl;
137     if(d_ctor < d_has_debruijn + d_datatype.getNumConstructors()) {
138       return getCurrentTerm( d_ctor );
139     } else {
140       throw NoMoreValuesException(getType());
141     }
142   }
143 
144   DatatypesEnumerator& operator++() override
145   {
146     Debug("dt-enum-debug") << ": increment " << this << std::endl;
147     unsigned prevSize = d_size_limit;
148     while(d_ctor < d_has_debruijn+d_datatype.getNumConstructors()) {
149       //increment at index
150       while( increment( d_ctor ) ){
151         Node n = getCurrentTerm( d_ctor );
152         if( !n.isNull() ){
153           return *this;
154         }
155       }
156       // Here, we need to step from the current constructor to the next one
157 
158       // Find the next constructor (only complicated by the notion of the "zero" constructor
159       d_ctor = (d_ctor == d_zeroCtor) ? 0 : d_ctor + 1;
160       if(d_ctor == d_zeroCtor) {
161         ++d_ctor;
162       }
163       if( d_ctor>=d_has_debruijn+d_datatype.getNumConstructors() ){
164         //try next size limit as long as new terms were generated at last size, or other cases
165         if( prevSize==d_size_limit || ( d_size_limit==0 && d_datatype.isCodatatype() ) || !d_datatype.isInterpretedFinite( d_type.toType() ) ){
166           d_size_limit++;
167           d_ctor = d_zeroCtor;
168           for( unsigned i=0; i<d_sel_sum.size(); i++ ){
169             d_sel_sum[i] = -1;
170           }
171         }
172       }
173     }
174     return *this;
175   }
176 
isFinished()177   bool isFinished() override
178   {
179     return d_ctor >= d_has_debruijn+d_datatype.getNumConstructors();
180   }
181 
182 };/* DatatypesEnumerator */
183 
184 }/* CVC4::theory::datatypes namespace */
185 }/* CVC4::theory namespace */
186 }/* CVC4 namespace */
187 
188 #endif /* __CVC4__THEORY__DATATYPES__TYPE_ENUMERATOR_H */
189