GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/datatypes/type_enumerator.h Lines: 48 48 100.0 %
Date: 2021-03-22 Branches: 50 92 54.3 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file type_enumerator.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Tim King, Morgan Deters
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 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 "expr/dtype.h"
23
#include "expr/kind.h"
24
#include "expr/type_node.h"
25
#include "options/quantifiers_options.h"
26
#include "theory/type_enumerator.h"
27
28
namespace CVC4 {
29
namespace theory {
30
namespace datatypes {
31
32
33
338362
class DatatypesEnumerator : public TypeEnumeratorBase<DatatypesEnumerator> {
34
  /** type properties */
35
  TypeEnumeratorProperties * d_tep;
36
  /** The datatype we're enumerating */
37
  const DType& 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 term to consider in the enumeration */
45
  Node d_zeroTerm;
46
  /** Whether we are currently considering the above term */
47
  bool d_zeroTermActive;
48
  /** list of type enumerators (one for each type in a selector argument) */
49
  std::map< TypeNode, unsigned > d_te_index;
50
  std::vector< TypeEnumerator > d_children;
51
  //std::vector< DatatypesEnumerator > d_dt_children;
52
  /** terms produced for types */
53
  std::map< TypeNode, std::vector< Node > > d_terms;
54
  /** arg type of each selector, for each constructor */
55
  std::vector< std::vector< TypeNode > > d_sel_types;
56
  /** current index for each argument, for each constructor */
57
  std::vector< std::vector< unsigned > > d_sel_index;
58
  /** current sum of argument indicies for each constructor */
59
  std::vector< int > d_sel_sum;
60
  /** current bound on the number of times we can iterate argument enumerators */
61
  unsigned d_size_limit;
62
  /** child */
63
  bool d_child_enum;
64
65
120
  bool hasCyclesDt(const DType& dt)
66
  {
67
120
    return dt.isRecursiveSingleton(d_type) || !dt.isFinite(d_type);
68
  }
69
  bool hasCycles( TypeNode tn ){
70
    if( tn.isDatatype() ){
71
      const DType& dt = tn.getDType();
72
      return hasCyclesDt( dt );
73
    }else{
74
      return false;
75
    }
76
  }
77
78
  Node getTermEnum( TypeNode tn, unsigned i );
79
80
  bool increment( unsigned index );
81
82
  Node getCurrentTerm( unsigned index );
83
84
  void init();
85
86
 public:
87
160856
  DatatypesEnumerator(TypeNode type, TypeEnumeratorProperties* tep = nullptr)
88
160856
      : TypeEnumeratorBase<DatatypesEnumerator>(type),
89
        d_tep(tep),
90
160856
        d_datatype(type.getDType()),
91
        d_type(type),
92
        d_ctor(0),
93
321712
        d_zeroTermActive(false)
94
  {
95
160856
    d_child_enum = false;
96
160856
    init();
97
160856
  }
98
74
  DatatypesEnumerator(TypeNode type,
99
                      bool childEnum,
100
                      TypeEnumeratorProperties* tep = nullptr)
101
74
      : TypeEnumeratorBase<DatatypesEnumerator>(type),
102
        d_tep(tep),
103
74
        d_datatype(type.getDType()),
104
        d_type(type),
105
        d_ctor(0),
106
148
        d_zeroTermActive(false)
107
  {
108
74
    d_child_enum = childEnum;
109
74
    init();
110
74
  }
111
8251
  DatatypesEnumerator(const DatatypesEnumerator& de)
112
24753
      : TypeEnumeratorBase<DatatypesEnumerator>(de.getType()),
113
8251
        d_tep(de.d_tep),
114
8251
        d_datatype(de.d_datatype),
115
        d_type(de.d_type),
116
8251
        d_ctor(de.d_ctor),
117
        d_zeroTerm(de.d_zeroTerm),
118
49506
        d_zeroTermActive(de.d_zeroTermActive)
119
  {
120
8567
    for( std::map< TypeNode, unsigned >::const_iterator it = de.d_te_index.begin(); it != de.d_te_index.end(); ++it ){
121
316
      d_te_index[it->first] = it->second;
122
    }
123
8567
    for( std::map< TypeNode, std::vector< Node > >::const_iterator it = de.d_terms.begin(); it != de.d_terms.end(); ++it ){
124
316
      d_terms[it->first].insert( d_terms[it->first].end(), it->second.begin(), it->second.end() );
125
    }
126
56080
    for( unsigned i=0; i<de.d_sel_types.size(); i++ ){
127
47829
      d_sel_types.push_back( std::vector< TypeNode >() );
128
47829
      d_sel_types[i].insert( d_sel_types[i].end(), de.d_sel_types[i].begin(), de.d_sel_types[i].end() );
129
    }
130
56080
    for( unsigned i=0; i<de.d_sel_index.size(); i++ ){
131
47829
      d_sel_index.push_back( std::vector< unsigned >() );
132
47829
      d_sel_index[i].insert( d_sel_index[i].end(), de.d_sel_index[i].begin(), de.d_sel_index[i].end() );
133
    }
134
135
8251
    d_children.insert( d_children.end(), de.d_children.begin(), de.d_children.end() );
136
8251
    d_sel_sum.insert( d_sel_sum.end(), de.d_sel_sum.begin(), de.d_sel_sum.end() );
137
8251
    d_size_limit = de.d_size_limit;
138
8251
    d_has_debruijn = de.d_has_debruijn;
139
8251
    d_child_enum = de.d_child_enum;
140
8251
  }
141
142
403639
  Node operator*() override
143
  {
144
403639
    Debug("dt-enum-debug") << ": get term " << this << std::endl;
145
403639
    if (d_zeroTermActive)
146
    {
147
323211
      return d_zeroTerm;
148
    }
149
80428
    else if (d_ctor < d_has_debruijn + d_datatype.getNumConstructors())
150
    {
151
79470
      return getCurrentTerm( d_ctor );
152
    }
153
958
    throw NoMoreValuesException(getType());
154
  }
155
156
  DatatypesEnumerator& operator++() override;
157
158
592852
  bool isFinished() override
159
  {
160
592852
    return d_ctor >= d_has_debruijn+d_datatype.getNumConstructors();
161
  }
162
163
};/* DatatypesEnumerator */
164
165
}/* CVC4::theory::datatypes namespace */
166
}/* CVC4::theory namespace */
167
}/* CVC4 namespace */
168
169
#endif /* CVC4__THEORY__DATATYPES__TYPE_ENUMERATOR_H */