cvc4-1.4
|
Class encapsulating CVC4 expression types. More...
#include <type.h>
Public Member Functions | |
virtual | ~Type () |
Force a virtual destructor for safety. More... | |
Type () | |
Default constructor. More... | |
Type (const Type &t) | |
Copy constructor. More... | |
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... | |
Type & | operator= (const Type &t) |
Assignment operator. 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 | isSet () const |
Is this a Set 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... | |
Protected Member Functions | |
Type | makeType (const TypeNode &typeNode) const |
Construct a new type given the typeNode, for internal use only. More... | |
Type (NodeManager *em, TypeNode *typeNode) | |
Constructor for internal purposes. 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... | |
Friends | |
class | SmtEngine |
class | ExprManager |
class | NodeManager |
class | TypeNode |
std::ostream & | CVC4::operator<< (std::ostream &out, const Type &t) |
TypeNode | expr::exportTypeInternal (TypeNode n, NodeManager *from, NodeManager *nm, ExprManagerMapCollection &vmap) |
|
protected |
Constructor for internal purposes.
em | the expression manager that handles this expression |
typeNode | the actual TypeNode pointer for this type |
|
virtual |
Force a virtual destructor for safety.
CVC4::Type::Type | ( | ) |
Default constructor.
CVC4::Type::Type | ( | const Type & | t | ) |
Copy constructor.
t | the type to make a copy of |
Type CVC4::Type::exportTo | ( | ExprManager * | exprManager, |
ExprManagerMapCollection & | vmap | ||
) | const |
Exports this type into a different ExprManager.
Referenced by CVC4::Command::ExportTransformer::operator()().
Type CVC4::Type::getBaseType | ( | ) | const |
Get the most general base type of this type.
Cardinality CVC4::Type::getCardinality | ( | ) | const |
Return the cardinality of this type.
ExprManager* CVC4::Type::getExprManager | ( | ) | const |
Get this type's ExprManager.
bool CVC4::Type::isArray | ( | ) | const |
Is this an array type?
bool CVC4::Type::isBitVector | ( | ) | const |
Is this the bit-vector type?
bool CVC4::Type::isBoolean | ( | ) | const |
Is this the Boolean type?
bool CVC4::Type::isComparableTo | ( | Type | t | ) | const |
Is this type comparable to the given type (i.e., do they share a common ancestor in the subtype tree)?
bool CVC4::Type::isConstructor | ( | ) | const |
Is this a constructor type?
bool CVC4::Type::isDatatype | ( | ) | const |
Is this a datatype type?
bool CVC4::Type::isFunction | ( | ) | const |
Is this a function type?
bool CVC4::Type::isInteger | ( | ) | const |
Is this the integer type?
bool CVC4::Type::isNull | ( | ) | const |
Check whether this is a null type.
bool CVC4::Type::isPredicate | ( | ) | const |
Is this a predicate type, i.e.
if it's a function type mapping to Boolean. All predicate types are also function types.
bool CVC4::Type::isReal | ( | ) | const |
Is this the real type?
bool CVC4::Type::isRecord | ( | ) | const |
Is this a record type?
bool CVC4::Type::isSelector | ( | ) | const |
Is this a selector type?
bool CVC4::Type::isSet | ( | ) | const |
Is this a Set type?
bool CVC4::Type::isSExpr | ( | ) | const |
Is this a symbolic expression type?
bool CVC4::Type::isSort | ( | ) | const |
Is this a sort kind?
bool CVC4::Type::isSortConstructor | ( | ) | const |
Is this a sort constructor kind?
bool CVC4::Type::isString | ( | ) | const |
Is this the string type?
bool CVC4::Type::isSubrange | ( | ) | const |
Is this a predicate subtype?
bool CVC4::Type::isSubtypeOf | ( | Type | t | ) | const |
Is this type a subtype of the given type?
bool CVC4::Type::isTester | ( | ) | const |
Is this a tester type?
bool CVC4::Type::isTuple | ( | ) | const |
Is this a tuple type?
bool CVC4::Type::isWellFounded | ( | ) | const |
Is this a well-founded type?
Construct a new type given the typeNode, for internal use only.
typeNode | the TypeNode to use |
Expr CVC4::Type::mkGroundTerm | ( | ) | const |
Construct and return a ground term for this Type.
Throws an exception if this type is not well-founded.
bool CVC4::Type::operator!= | ( | const Type & | t | ) | const |
Comparison for structural disequality.
t | the type to compare to |
bool CVC4::Type::operator< | ( | const Type & | t | ) | const |
An ordering on Types so they can be stored in maps, etc.
bool CVC4::Type::operator<= | ( | const Type & | t | ) | const |
An ordering on Types so they can be stored in maps, etc.
Assignment operator.
t | the type to assign to this type |
bool CVC4::Type::operator== | ( | const Type & | t | ) | const |
Comparison for structural equality.
t | the type to compare to |
bool CVC4::Type::operator> | ( | const Type & | t | ) | const |
An ordering on Types so they can be stored in maps, etc.
bool CVC4::Type::operator>= | ( | const Type & | t | ) | const |
An ordering on Types so they can be stored in maps, etc.
Substitution of Types.
Type CVC4::Type::substitute | ( | const std::vector< Type > & | types, |
const std::vector< Type > & | replacements | ||
) | const |
Simultaneous substitution of Types.
void CVC4::Type::toStream | ( | std::ostream & | out | ) | const |
Outputs a string representation of this type to the stream.
out | the stream to output to |
std::string CVC4::Type::toString | ( | ) | const |
Constructs a string representation of this type.
|
friend |
|
friend |
|
friend |
|
protected |
|
protected |