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