2 #include "util/datatype.h"
4 //typedef CVC4::Datatype::Constructor DatatypeConstructor;
9 %rename(DatatypeConstructor) CVC4::Datatype::Constructor;
10 %rename(DatatypeConstructor) CVC4::Constructor;
13 %extend std::vector< CVC4::Datatype > {
14 %ignore vector(size_type);
16 %template(vectorDatatype) std::vector< CVC4::Datatype >;
18 %extend std::vector< CVC4::Datatype::Constructor > {
19 %ignore vector(size_type);
21 %template(vectorDatatypeConstructor) std::vector< CVC4::Datatype::Constructor >;
23 %rename(equals) CVC4::Datatype::operator==(const Datatype&) const;
24 %ignore CVC4::Datatype::operator!=(const Datatype&) const;
26 %rename(beginConst) CVC4::Datatype::begin() const;
27 %rename(endConst) CVC4::Datatype::end() const;
29 %rename(getConstructor) CVC4::Datatype::operator[](size_t) const;
31 %rename(apply) CVC4::DatatypeHashFunction::operator()(const Datatype&) const;
32 %ignore CVC4::DatatypeHashFunction::operator()(const Datatype*) const;
33 %rename(apply) CVC4::DatatypeHashFunction::operator()(const Datatype::Constructor&) const;
34 %ignore CVC4::DatatypeHashFunction::operator()(const Datatype::Constructor*) const;
36 %ignore CVC4::operator<<(std::ostream&, const Datatype&);
37 %ignore CVC4::operator<<(std::ostream&, const Datatype::Constructor&);
38 %ignore CVC4::operator<<(std::ostream&, const Datatype::Constructor::Arg&);
40 %feature("valuewrapper") CVC4::Datatype::UnresolvedType;
42 %include "util/datatype.h"
45 class CVC4_PUBLIC Arg {
49 /** the constructor associated with this selector */
53 explicit Arg(std::string name, Expr selector);
54 friend class Constructor;
55 friend class Datatype;
57 bool isUnresolvedSelf() const throw();
61 /** Get the name of this constructor argument. */
62 std::string getName() const throw();
65 * Get the selector for this constructor argument; this call is
66 * only permitted after resolution.
68 Expr getSelector() const;
71 * Get the associated constructor for this constructor argument;
72 * this call is only permitted after resolution.
74 Expr getConstructor() const;
77 * Get the selector for this constructor argument; this call is
78 * only permitted after resolution.
80 Type getSelectorType() const;
83 * Get the name of the type of this constructor argument
84 * (Datatype field). Can be used for not-yet-resolved Datatypes
85 * (in which case the name of the unresolved type, or "[self]"
86 * for a self-referential type is returned).
88 std::string getSelectorTypeName() const;
91 * Returns true iff this constructor argument has been resolved.
93 bool isResolved() const throw();
95 };/* class Datatype::Constructor::Arg */
100 /** The type for iterators over constructor arguments. */
101 typedef std::vector<Arg>::iterator iterator;
102 /** The (const) type for iterators over constructor arguments. */
103 typedef std::vector<Arg>::const_iterator const_iterator;
110 std::vector<Arg> d_args;
112 void resolve(ExprManager* em, DatatypeType self,
113 const std::map<std::string, DatatypeType>& resolutions,
114 const std::vector<Type>& placeholders,
115 const std::vector<Type>& replacements,
116 const std::vector< SortConstructorType >& paramTypes,
117 const std::vector< DatatypeType >& paramReplacements)
118 throw(AssertionException, DatatypeResolutionException);
119 friend class Datatype;
121 /** @FIXME document this! */
122 Type doParametricSubstitution(Type range,
123 const std::vector< SortConstructorType >& paramTypes,
124 const std::vector< DatatypeType >& paramReplacements);
127 * Create a new Datatype constructor with the given name for the
128 * constructor and the given name for the tester. The actual
129 * constructor and tester aren't created until resolution time.
131 explicit Constructor(std::string name, std::string tester);
134 * Add an argument (i.e., a data field) of the given name and type
135 * to this Datatype constructor.
137 void addArg(std::string selectorName, Type selectorType);
140 * Add an argument (i.e., a data field) of the given name to this
141 * Datatype constructor that refers to an as-yet-unresolved
142 * Datatype (which may be mutually-recursive).
144 void addArg(std::string selectorName, Datatype::UnresolvedType selectorType);
147 * Add a self-referential (i.e., a data field) of the given name
148 * to this Datatype constructor that refers to the enclosing
149 * Datatype. For example, using the familiar "nat" Datatype, to
150 * create the "pred" field for "succ" constructor, one uses
151 * succ::addArg("pred", Datatype::SelfType())---the actual Type
152 * cannot be passed because the Datatype is still under
155 * This is a special case of
156 * Constructor::addArg(std::string, Datatype::UnresolvedType).
158 void addArg(std::string selectorName, Datatype::SelfType);
160 /** Get the name of this Datatype constructor. */
161 std::string getName() const throw();
163 * Get the constructor operator of this Datatype constructor. The
164 * Datatype must be resolved.
166 Expr getConstructor() const;
168 * Get the tester operator of this Datatype constructor. The
169 * Datatype must be resolved.
171 Expr getTester() const;
173 * Get the number of arguments (so far) of this Datatype constructor.
175 inline size_t getNumArgs() const throw();
178 * Get the specialized constructor type for a parametric
179 * constructor; this call is only permitted after resolution.
181 Type getSpecializedConstructorType(Type returnType) const;
184 * Return the cardinality of this constructor (the product of the
185 * cardinalities of its arguments).
187 Cardinality getCardinality() const throw(AssertionException);
190 * Return true iff this constructor is finite (it is nullary or
191 * each of its argument types are finite). This function can
192 * only be called for resolved constructors.
194 bool isFinite() const throw(AssertionException);
197 * Return true iff this constructor is well-founded (there exist
198 * ground terms). The constructor must be resolved or an
199 * exception is thrown.
201 bool isWellFounded() const throw(AssertionException);
204 * Construct and return a ground term of this constructor. The
205 * constructor must be both resolved and well-founded, or else an
206 * exception is thrown.
208 Expr mkGroundTerm( Type t ) const throw(AssertionException);
211 * Returns true iff this Datatype constructor has already been
214 inline bool isResolved() const throw();
216 /** Get the beginning iterator over Constructor args. */
217 inline iterator begin() throw();
218 /** Get the ending iterator over Constructor args. */
219 inline iterator end() throw();
220 /** Get the beginning const_iterator over Constructor args. */
221 inline const_iterator begin() const throw();
222 /** Get the ending const_iterator over Constructor args. */
223 inline const_iterator end() const throw();
225 /** Get the ith Constructor arg. */
226 const Arg& operator[](size_t index) const;
228 };/* class Datatype::Constructor */
232 };/* class Datatype::SelfType */
235 * An unresolved type (used in calls to
236 * Datatype::Constructor::addArg()) to allow a Datatype to refer to
237 * itself or to other mutually-recursive Datatypes. Unresolved-type
238 * fields of Datatypes will be properly typed when a Type is created
239 * for the Datatype by the ExprManager (which calls
240 * Datatype::resolve()).
242 class UnresolvedType {
245 inline UnresolvedType(std::string name);
246 inline std::string getName() const throw();
247 };/* class Datatype::UnresolvedType */
251 typedef Datatype::Constructor Constructor;
252 typedef Datatype::Constructor::Arg Arg;
253 typedef Datatype::SelfType SelfType;
254 typedef Datatype::UnresolvedType UnresolvedType;