1 /********************* -*- C++ -*- */
3 ** Original author: cconway
4 ** Major contributors: none
5 ** Minor contributors (to current version): none
6 ** This file is part of the CVC4 prototype.
7 ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
8 ** Courant Institute of Mathematical Sciences
10 ** See the file COPYING in the top-level source directory for licensing
13 ** Interface for expression types
16 #ifndef __CVC4__TYPE_H
17 #define __CVC4__TYPE_H
19 #include "cvc4_config.h"
29 * Class encapsulating CVC4 expression types.
33 /** Comparision for equality */
34 bool operator==(const Type
& t
) const;
36 /** Comparison for disequality */
37 bool operator!=(const Type
& e
) const;
39 /** Get the ExprManager associated with this type. May be NULL for
41 ExprManager
* getExprManager() const;
43 /** Get the name of this type. May be empty for composite types. */
44 std::string
getName() const;
46 /** Is this the boolean type? */
47 virtual bool isBoolean() const {
51 /** Is this a function type? */
52 virtual bool isFunction() const {
56 /** Is this a predicate type? NOTE: all predicate types are also
58 virtual bool isPredicate() const {
62 /** Is this a kind type (i.e., the type of a type)? */
63 virtual bool isKind() const {
67 /** Outputs a string representation of this type to the stream. */
68 virtual void toStream(std::ostream
& out
) const {
73 /** Create a type associated with exprManager. */
74 Type(ExprManager
* const exprManager
);
76 /** Create a type associated with exprManager with the given name. */
77 Type(ExprManager
* const exprManager
, std::string name
);
79 /** Create a type with the given name. */
80 Type(std::string name
);
85 /** The associated ExprManager */
86 ExprManager
* d_exprManager
;
88 /** The name of the type (may be empty). */
93 * Singleton class encapsulating the boolean type.
95 class BooleanType
: public Type
{
98 static BooleanType
* getInstance();
100 /** Is this the boolean type? (Returns true.) */
101 bool isBoolean() const;
104 /** Create a type associated with exprManager. */
107 /** Do-nothing private copy constructor operator, to prevent
108 copy-construction. */
109 BooleanType(const BooleanType
&);
114 /** Do-nothing private assignment operator, to prevent
116 BooleanType
& operator=(const BooleanType
&);
118 /** The singleton instance */
119 static BooleanType s_instance
;
123 * Class encapsulating a function type.
124 * TODO: Override == to check component types?
126 class FunctionType
: public Type
{
129 static FunctionType
* getInstance(ExprManager
* exprManager
,
133 static FunctionType
* getInstance(ExprManager
* exprManager
,
134 const std::vector
<const Type
*>& argTypes
,
138 /** Retrieve the argument types. The vector will be non-empty. */
139 const std::vector
<const Type
*> getArgTypes() const;
141 /** Get the range type (i.e., the type of the result). */
142 const Type
* getRangeType() const;
144 /** Is this as function type? (Returns true.) */
145 bool isFunction() const;
147 /** Is this as predicate type? (Returns true if range is
149 bool isPredicate() const;
151 /** Outputs a string representation of this type to the stream,
152 in the format "D -> R" or "(A, B, C) -> R". */
153 void toStream(std::ostream
& out
) const;
157 /** Construct a function type associated with exprManager,
158 given a vector of argument types and the range type.
160 @param argTypes a non-empty vector of input types
161 @param range the result type
163 FunctionType(ExprManager
* exprManager
,
164 const std::vector
<const Type
*>& argTypes
,
170 /** The list of input types. */
171 const std::vector
<const Type
*> d_argTypes
;
173 /** The result type. */
174 const Type
* d_rangeType
;
179 /** Class encapsulating the kind type (the type of types).
180 TODO: Should be a singleton per-ExprManager.
182 class KindType
: public Type
{
186 /** Create a type associated with exprManager. */
187 static KindType
* getInstance();
189 /** Is this the kind type? (Returns true.) */
194 /** Create a type associated with exprManager. */
197 /* Do-nothing private copy constructor, to prevent
198 copy construction. */
199 KindType(const KindType
&);
204 /* Do-nothing private assignment operator, to prevent
206 KindType
& operator=(const KindType
&);
208 /** The singleton instance */
209 static KindType s_instance
;
212 /** Class encapsulating a user-defined sort.
213 TODO: Should sort be uniquely named per-exprManager and not conflict
214 with any builtins? */
215 class SortType
: public Type
{
219 /** Create a sort associated with exprManager with the given name. */
220 SortType(ExprManager
* exprManager
, std::string name
);
227 * Output operator for types
228 * @param out the stream to output to
229 * @param e the type to output
232 std::ostream
& operator<<(std::ostream
& out
, const Type
& t
) CVC4_PUBLIC
;
236 #endif /* __CVC4__TYPE_H */