cvc4-1.3
|
#include <cvc3_compat.h>
Public Member Functions | |
Type () | |
Type (const CVC4::Type &type) | |
Type (const Type &type) | |
Expr | getExpr () const |
int | arity () const |
Type | operator[] (int i) const |
bool | isBool () const |
bool | isSubtype () const |
Cardinality | card () const |
Return cardinality of type. More... | |
Expr | enumerateFinite (Unsigned n) const |
Return nth (starting with 0) element in a finite type. More... | |
Unsigned | sizeFinite () const |
Return size of a finite type; returns 0 if size cannot be determined. More... | |
Type | funType (const Type &typeRan) const |
bool | isNull () const |
Check whether this is a null type. More... | |
Cardinality | getCardinality () const |
Return the cardinality of this type. More... | |
bool | isWellFounded () const |
Is this a well-founded type? More... | |
Expr | mkGroundTerm () const |
Construct and return a ground term for this Type. More... | |
bool | isSubtypeOf (Type t) const |
Is this type a subtype of the given type? More... | |
bool | isComparableTo (Type t) const |
Is this type comparable to the given type (i.e., do they share a common ancestor in the subtype tree)? More... | |
Type | getBaseType () const |
Get the most general base type of this type. More... | |
Type | substitute (const Type &type, const Type &replacement) const |
Substitution of Types. More... | |
Type | substitute (const std::vector< Type > &types, const std::vector< Type > &replacements) const |
Simultaneous substitution of Types. More... | |
ExprManager * | getExprManager () const |
Get this type's ExprManager. More... | |
Type | exportTo (ExprManager *exprManager, ExprManagerMapCollection &vmap) const |
Exports this type into a different ExprManager. More... | |
bool | operator== (const Type &t) const |
Comparison for structural equality. More... | |
bool | operator!= (const Type &t) const |
Comparison for structural disequality. More... | |
bool | operator< (const Type &t) const |
An ordering on Types so they can be stored in maps, etc. More... | |
bool | operator<= (const Type &t) const |
An ordering on Types so they can be stored in maps, etc. More... | |
bool | operator> (const Type &t) const |
An ordering on Types so they can be stored in maps, etc. More... | |
bool | operator>= (const Type &t) const |
An ordering on Types so they can be stored in maps, etc. More... | |
bool | isBoolean () const |
Is this the Boolean type? More... | |
bool | isInteger () const |
Is this the integer type? More... | |
bool | isReal () const |
Is this the real type? More... | |
bool | isString () const |
Is this the string type? More... | |
bool | isBitVector () const |
Is this the bit-vector type? More... | |
bool | isFunction () const |
Is this a function type? More... | |
bool | isPredicate () const |
Is this a predicate type, i.e. More... | |
bool | isTuple () const |
Is this a tuple type? More... | |
bool | isRecord () const |
Is this a record type? More... | |
bool | isSExpr () const |
Is this a symbolic expression type? More... | |
bool | isArray () const |
Is this an array type? More... | |
bool | isDatatype () const |
Is this a datatype type? More... | |
bool | isConstructor () const |
Is this a constructor type? More... | |
bool | isSelector () const |
Is this a selector type? More... | |
bool | isTester () const |
Is this a tester type? More... | |
bool | isSort () const |
Is this a sort kind? More... | |
bool | isSortConstructor () const |
Is this a sort constructor kind? More... | |
bool | isSubrange () const |
Is this a predicate subtype? More... | |
void | toStream (std::ostream &out) const |
Outputs a string representation of this type to the stream. More... | |
std::string | toString () const |
Constructs a string representation of this type. More... | |
Static Public Member Functions | |
static Type | typeBool (ExprManager *em) |
static Type | funType (const std::vector< Type > &typeDom, const Type &typeRan) |
Protected Member Functions | |
Type | makeType (const TypeNode &typeNode) const |
Construct a new type given the typeNode, for internal use only. More... | |
Static Protected Member Functions | |
static TypeNode * | getTypeNode (const Type &t) throw () |
Accessor for derived classes. More... | |
Protected Attributes | |
TypeNode * | d_typeNode |
The internal expression representation. More... | |
NodeManager * | d_nodeManager |
The responsible expression manager. More... | |
Definition at line 279 of file cvc3_compat.h.
CVC3::Type::Type | ( | ) |
CVC3::Type::Type | ( | const CVC4::Type & | type | ) |
CVC3::Type::Type | ( | const Type & | type | ) |
int CVC3::Type::arity | ( | ) | const |
Cardinality CVC3::Type::card | ( | ) | const |
Return cardinality of type.
Return nth (starting with 0) element in a finite type.
Returns NULL Expr if unable to compute nth element
|
inherited |
Exports this type into a different ExprManager.
Referenced by CVC4::Command::ExportTransformer::operator()().
|
static |
|
inherited |
Get the most general base type of this type.
|
inherited |
Return the cardinality of this type.
Expr CVC3::Type::getExpr | ( | ) | const |
|
inherited |
Get this type's ExprManager.
|
inherited |
Is this an array type?
|
inherited |
Is this the bit-vector type?
bool CVC3::Type::isBool | ( | ) | const |
|
inherited |
Is this the Boolean type?
|
inherited |
Is this type comparable to the given type (i.e., do they share a common ancestor in the subtype tree)?
|
inherited |
Is this a constructor type?
|
inherited |
Is this a datatype type?
|
inherited |
Is this a function type?
|
inherited |
Is this the integer type?
|
inherited |
Check whether this is a null type.
|
inherited |
Is this a predicate type, i.e.
if it's a function type mapping to Boolean. All predicate types are also function types.
|
inherited |
Is this the real type?
|
inherited |
Is this a record type?
|
inherited |
Is this a selector type?
|
inherited |
Is this a symbolic expression type?
|
inherited |
Is this a sort kind?
|
inherited |
Is this a sort constructor kind?
|
inherited |
Is this the string type?
|
inherited |
Is this a predicate subtype?
bool CVC3::Type::isSubtype | ( | ) | const |
|
inherited |
Is this type a subtype of the given type?
|
inherited |
Is this a tester type?
|
inherited |
Is this a tuple type?
|
inherited |
Is this a well-founded type?
Construct a new type given the typeNode, for internal use only.
typeNode | the TypeNode to use |
|
inherited |
Construct and return a ground term for this Type.
Throws an exception if this type is not well-founded.
|
inherited |
Comparison for structural disequality.
t | the type to compare to |
|
inherited |
An ordering on Types so they can be stored in maps, etc.
|
inherited |
An ordering on Types so they can be stored in maps, etc.
|
inherited |
Comparison for structural equality.
t | the type to compare to |
|
inherited |
An ordering on Types so they can be stored in maps, etc.
|
inherited |
An ordering on Types so they can be stored in maps, etc.
Type CVC3::Type::operator[] | ( | int | i | ) | const |
Unsigned CVC3::Type::sizeFinite | ( | ) | const |
Return size of a finite type; returns 0 if size cannot be determined.
Substitution of Types.
|
inherited |
Simultaneous substitution of Types.
|
inherited |
Outputs a string representation of this type to the stream.
out | the stream to output to |
|
inherited |
Constructs a string representation of this type.
|
static |
|
protectedinherited |
|
protectedinherited |