cvc4-1.3
CVC4::SExprType Class Reference

Class encapsulating a tuple type. More...

#include <type.h>

Inheritance diagram for CVC4::SExprType:
CVC4::Type

Public Member Functions

 SExprType (const Type &type=Type()) throw (IllegalArgumentException)
 Construct from the base type. More...
 
std::vector< TypegetTypes () const
 Get the constituent types. 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...
 
ExprManagergetExprManager () 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...
 

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 TypeNodegetTypeNode (const Type &t) throw ()
 Accessor for derived classes. More...
 

Protected Attributes

TypeNoded_typeNode
 The internal expression representation. More...
 
NodeManagerd_nodeManager
 The responsible expression manager. More...
 

Detailed Description

Class encapsulating a tuple type.

Definition at line 463 of file type.h.

Constructor & Destructor Documentation

CVC4::SExprType::SExprType ( const Type type = Type())
throw (IllegalArgumentException
)

Construct from the base type.

Member Function Documentation

Type CVC4::Type::exportTo ( ExprManager exprManager,
ExprManagerMapCollection vmap 
) const
inherited

Exports this type into a different ExprManager.

Referenced by CVC4::Command::ExportTransformer::operator()().

Type CVC4::Type::getBaseType ( ) const
inherited

Get the most general base type of this type.

Cardinality CVC4::Type::getCardinality ( ) const
inherited

Return the cardinality of this type.

ExprManager* CVC4::Type::getExprManager ( ) const
inherited

Get this type's ExprManager.

static TypeNode* CVC4::Type::getTypeNode ( const Type t)
throw (
)
inlinestaticprotectedinherited

Accessor for derived classes.

Definition at line 120 of file type.h.

std::vector<Type> CVC4::SExprType::getTypes ( ) const

Get the constituent types.

bool CVC4::Type::isArray ( ) const
inherited

Is this an array type?

Returns
true if the type is a array type
bool CVC4::Type::isBitVector ( ) const
inherited

Is this the bit-vector type?

Returns
true if the type is a bit-vector type
bool CVC4::Type::isBoolean ( ) const
inherited

Is this the Boolean type?

Returns
true if the type is a Boolean type
bool CVC4::Type::isComparableTo ( Type  t) const
inherited

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
inherited

Is this a constructor type?

Returns
true if the type is a constructor type
bool CVC4::Type::isDatatype ( ) const
inherited

Is this a datatype type?

Returns
true if the type is a datatype type
bool CVC4::Type::isFunction ( ) const
inherited

Is this a function type?

Returns
true if the type is a function type
bool CVC4::Type::isInteger ( ) const
inherited

Is this the integer type?

Returns
true if the type is a integer type
bool CVC4::Type::isNull ( ) const
inherited

Check whether this is a null type.

Returns
true if type is null
bool CVC4::Type::isPredicate ( ) const
inherited

Is this a predicate type, i.e.

if it's a function type mapping to Boolean. All predicate types are also function types.

Returns
true if the type is a predicate type
bool CVC4::Type::isReal ( ) const
inherited

Is this the real type?

Returns
true if the type is a real type
bool CVC4::Type::isRecord ( ) const
inherited

Is this a record type?

Returns
true if the type is a record type
bool CVC4::Type::isSelector ( ) const
inherited

Is this a selector type?

Returns
true if the type is a selector type
bool CVC4::Type::isSExpr ( ) const
inherited

Is this a symbolic expression type?

Returns
true if the type is a symbolic expression type
bool CVC4::Type::isSort ( ) const
inherited

Is this a sort kind?

Returns
true if this is a sort kind
bool CVC4::Type::isSortConstructor ( ) const
inherited

Is this a sort constructor kind?

Returns
true if this is a sort constructor kind
bool CVC4::Type::isString ( ) const
inherited

Is this the string type?

Returns
true if the type is the string type
bool CVC4::Type::isSubrange ( ) const
inherited

Is this a predicate subtype?

Returns
true if this is a predicate subtype Is this an integer subrange type?
true if this is an integer subrange type
bool CVC4::Type::isSubtypeOf ( Type  t) const
inherited

Is this type a subtype of the given type?

bool CVC4::Type::isTester ( ) const
inherited

Is this a tester type?

Returns
true if the type is a tester type
bool CVC4::Type::isTuple ( ) const
inherited

Is this a tuple type?

Returns
true if the type is a tuple type
bool CVC4::Type::isWellFounded ( ) const
inherited

Is this a well-founded type?

Type CVC4::Type::makeType ( const TypeNode typeNode) const
protectedinherited

Construct a new type given the typeNode, for internal use only.

Parameters
typeNodethe TypeNode to use
Returns
the Type corresponding to the TypeNode
Expr CVC4::Type::mkGroundTerm ( ) const
inherited

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
inherited

Comparison for structural disequality.

Parameters
tthe type to compare to
Returns
true if the types are not equal
bool CVC4::Type::operator< ( const Type t) const
inherited

An ordering on Types so they can be stored in maps, etc.

bool CVC4::Type::operator<= ( const Type t) const
inherited

An ordering on Types so they can be stored in maps, etc.

bool CVC4::Type::operator== ( const Type t) const
inherited

Comparison for structural equality.

Parameters
tthe type to compare to
Returns
true if the types are equal
bool CVC4::Type::operator> ( const Type t) const
inherited

An ordering on Types so they can be stored in maps, etc.

bool CVC4::Type::operator>= ( const Type t) const
inherited

An ordering on Types so they can be stored in maps, etc.

Type CVC4::Type::substitute ( const Type type,
const Type replacement 
) const
inherited

Substitution of Types.

Type CVC4::Type::substitute ( const std::vector< Type > &  types,
const std::vector< Type > &  replacements 
) const
inherited

Simultaneous substitution of Types.

void CVC4::Type::toStream ( std::ostream &  out) const
inherited

Outputs a string representation of this type to the stream.

Parameters
outthe stream to output to
std::string CVC4::Type::toString ( ) const
inherited

Constructs a string representation of this type.

Field Documentation

NodeManager* CVC4::Type::d_nodeManager
protectedinherited

The responsible expression manager.

Definition at line 103 of file type.h.

TypeNode* CVC4::Type::d_typeNode
protectedinherited

The internal expression representation.

Definition at line 100 of file type.h.


The documentation for this class was generated from the following file: