1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
|
%{
#include "util/datatype.h"
%}
namespace CVC4 {
%rename(DatatypeConstructor) CVC4::Datatype::Constructor;
%rename(DatatypeConstructor) CVC4::Constructor;
}
%extend std::vector< CVC4::Datatype > {
%ignore vector(size_type);
};
%template(vectorDatatype) std::vector< CVC4::Datatype >;
%extend std::vector< CVC4::Datatype::Constructor > {
%ignore vector(size_type);
};
%template(vectorDatatypeConstructor) std::vector< CVC4::Datatype::Constructor >;
%rename(equals) CVC4::Datatype::operator==(const Datatype&) const;
%ignore CVC4::Datatype::operator!=(const Datatype&) const;
%rename(beginConst) CVC4::Datatype::begin() const;
%rename(endConst) CVC4::Datatype::end() const;
%rename(getConstructor) CVC4::Datatype::operator[](size_t) const;
%rename(apply) CVC4::DatatypeHashFunction::operator()(const Datatype&) const;
%ignore CVC4::DatatypeHashFunction::operator()(const Datatype*) const;
%rename(apply) CVC4::DatatypeHashFunction::operator()(const Datatype::Constructor&) const;
%ignore CVC4::DatatypeHashFunction::operator()(const Datatype::Constructor*) const;
%rename(beginConst) CVC4::Constructor::begin() const;
%rename(endConst) CVC4::Constructor::end() const;
%rename(getArg) CVC4::Constructor::operator[](size_t) const;
%ignore CVC4::operator<<(std::ostream&, const Datatype&);
%ignore CVC4::operator<<(std::ostream&, const Datatype::Constructor&);
%ignore CVC4::operator<<(std::ostream&, const Datatype::Constructor::Arg&);
%feature("valuewrapper") CVC4::Datatype::UnresolvedType;
%include "util/datatype.h"
namespace CVC4 {
class CVC4_PUBLIC Arg {
std::string d_name;
Expr d_selector;
/** the constructor associated with this selector */
Expr d_constructor;
bool d_resolved;
explicit Arg(std::string name, Expr selector);
friend class Constructor;
friend class Datatype;
bool isUnresolvedSelf() const throw();
public:
/** Get the name of this constructor argument. */
std::string getName() const throw();
/**
* Get the selector for this constructor argument; this call is
* only permitted after resolution.
*/
Expr getSelector() const;
/**
* Get the associated constructor for this constructor argument;
* this call is only permitted after resolution.
*/
Expr getConstructor() const;
/**
* Get the selector for this constructor argument; this call is
* only permitted after resolution.
*/
Type getSelectorType() const;
/**
* Get the name of the type of this constructor argument
* (Datatype field). Can be used for not-yet-resolved Datatypes
* (in which case the name of the unresolved type, or "[self]"
* for a self-referential type is returned).
*/
std::string getSelectorTypeName() const;
/**
* Returns true iff this constructor argument has been resolved.
*/
bool isResolved() const throw();
};/* class Datatype::Constructor::Arg */
class Constructor {
public:
/** The type for iterators over constructor arguments. */
typedef std::vector<Arg>::iterator iterator;
/** The (const) type for iterators over constructor arguments. */
typedef std::vector<Arg>::const_iterator const_iterator;
private:
std::string d_name;
Expr d_constructor;
Expr d_tester;
std::vector<Arg> d_args;
void resolve(ExprManager* em, DatatypeType self,
const std::map<std::string, DatatypeType>& resolutions,
const std::vector<Type>& placeholders,
const std::vector<Type>& replacements,
const std::vector< SortConstructorType >& paramTypes,
const std::vector< DatatypeType >& paramReplacements)
throw(AssertionException, DatatypeResolutionException);
friend class Datatype;
/** @FIXME document this! */
Type doParametricSubstitution(Type range,
const std::vector< SortConstructorType >& paramTypes,
const std::vector< DatatypeType >& paramReplacements);
public:
/**
* Create a new Datatype constructor with the given name for the
* constructor and the given name for the tester. The actual
* constructor and tester aren't created until resolution time.
*/
explicit Constructor(std::string name, std::string tester);
/**
* Add an argument (i.e., a data field) of the given name and type
* to this Datatype constructor.
*/
void addArg(std::string selectorName, Type selectorType);
/**
* Add an argument (i.e., a data field) of the given name to this
* Datatype constructor that refers to an as-yet-unresolved
* Datatype (which may be mutually-recursive).
*/
void addArg(std::string selectorName, Datatype::UnresolvedType selectorType);
/**
* Add a self-referential (i.e., a data field) of the given name
* to this Datatype constructor that refers to the enclosing
* Datatype. For example, using the familiar "nat" Datatype, to
* create the "pred" field for "succ" constructor, one uses
* succ::addArg("pred", Datatype::SelfType())---the actual Type
* cannot be passed because the Datatype is still under
* construction.
*
* This is a special case of
* Constructor::addArg(std::string, Datatype::UnresolvedType).
*/
void addArg(std::string selectorName, Datatype::SelfType);
/** Get the name of this Datatype constructor. */
std::string getName() const throw();
/**
* Get the constructor operator of this Datatype constructor. The
* Datatype must be resolved.
*/
Expr getConstructor() const;
/**
* Get the tester operator of this Datatype constructor. The
* Datatype must be resolved.
*/
Expr getTester() const;
/**
* Get the number of arguments (so far) of this Datatype constructor.
*/
inline size_t getNumArgs() const throw();
/**
* Get the specialized constructor type for a parametric
* constructor; this call is only permitted after resolution.
*/
Type getSpecializedConstructorType(Type returnType) const;
/**
* Return the cardinality of this constructor (the product of the
* cardinalities of its arguments).
*/
Cardinality getCardinality() const throw(AssertionException);
/**
* Return true iff this constructor is finite (it is nullary or
* each of its argument types are finite). This function can
* only be called for resolved constructors.
*/
bool isFinite() const throw(AssertionException);
/**
* Return true iff this constructor is well-founded (there exist
* ground terms). The constructor must be resolved or an
* exception is thrown.
*/
bool isWellFounded() const throw(AssertionException);
/**
* Construct and return a ground term of this constructor. The
* constructor must be both resolved and well-founded, or else an
* exception is thrown.
*/
Expr mkGroundTerm( Type t ) const throw(AssertionException);
/**
* Returns true iff this Datatype constructor has already been
* resolved.
*/
inline bool isResolved() const throw();
/** Get the beginning iterator over Constructor args. */
inline iterator begin() throw();
/** Get the ending iterator over Constructor args. */
inline iterator end() throw();
/** Get the beginning const_iterator over Constructor args. */
inline const_iterator begin() const throw();
/** Get the ending const_iterator over Constructor args. */
inline const_iterator end() const throw();
/** Get the ith Constructor arg. */
const Arg& operator[](size_t index) const;
};/* class Datatype::Constructor */
class SelfType {
};/* class Datatype::SelfType */
/**
* An unresolved type (used in calls to
* Datatype::Constructor::addArg()) to allow a Datatype to refer to
* itself or to other mutually-recursive Datatypes. Unresolved-type
* fields of Datatypes will be properly typed when a Type is created
* for the Datatype by the ExprManager (which calls
* Datatype::resolve()).
*/
class UnresolvedType {
std::string d_name;
public:
inline UnresolvedType(std::string name);
inline std::string getName() const throw();
};/* class Datatype::UnresolvedType */
}
%{
namespace CVC4 {
typedef Datatype::Constructor Constructor;
typedef Datatype::Constructor::Arg Arg;
typedef Datatype::SelfType SelfType;
typedef Datatype::UnresolvedType UnresolvedType;
}
%}
|
