Class encapsulating CVC4 expression types. More...

#include <type.h>

Inheritance diagram for CVC4::Type:

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)

Detailed Description

Class encapsulating CVC4 expression types.

Definition at line 89 of file type.h.

Constructor & Destructor Documentation

CVC4::Type::Type	(	NodeManager *	em,
		TypeNode *	typeNode
	)

protected

Constructor for internal purposes.

Parameters

em	the expression manager that handles this expression
typeNode	the actual TypeNode pointer for this type

virtual CVC4::Type::~Type ( )

virtual

Force a virtual destructor for safety.

CVC4::Type::Type ( )

Default constructor.

CVC4::Type::Type ( const Type & t )

Copy constructor.

Parameters

t	the type to make a copy of

Member Function Documentation

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.

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

inlinestaticprotected

Accessor for derived classes.

Definition at line 121 of file type.h.

References d_typeNode, CVC4::operator!=(), and CVC4::operator==().

bool CVC4::Type::isArray ( ) const

Is this an array type?

Returns: true if the type is a array type

bool CVC4::Type::isBitVector ( ) const

Is this the bit-vector type?

Returns: true if the type is a bit-vector type

bool CVC4::Type::isBoolean ( ) const

Is this the Boolean type?

Returns: true if the type is a 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?

Returns: true if the type is a constructor type

bool CVC4::Type::isDatatype ( ) const

Is this a datatype type?

Returns: true if the type is a datatype type

bool CVC4::Type::isFunction ( ) const

Is this a function type?

Returns: true if the type is a function type

bool CVC4::Type::isInteger ( ) const

Is this the integer type?

Returns: true if the type is a integer type

bool CVC4::Type::isNull ( ) const

Check whether this is a null type.

Returns: true if type is null

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.

Returns: true if the type is a predicate type

bool CVC4::Type::isReal ( ) const

Is this the real type?

Returns: true if the type is a real type

bool CVC4::Type::isRecord ( ) const

Is this a record type?

Returns: true if the type is a record type

bool CVC4::Type::isSelector ( ) const

Is this a selector type?

Returns: true if the type is a selector type

bool CVC4::Type::isSet ( ) const

Is this a Set type?

Returns: true if the type is a Set type

bool CVC4::Type::isSExpr ( ) const

Is this a symbolic expression type?

Returns: true if the type is a symbolic expression type

bool CVC4::Type::isSort ( ) const

Is this a sort kind?

Returns: true if this is a sort kind

bool CVC4::Type::isSortConstructor ( ) const

Is this a sort constructor kind?

Returns: true if this is a sort constructor kind

bool CVC4::Type::isString ( ) const

Is this the string type?

Returns: true if the type is the string type

bool CVC4::Type::isSubrange ( ) const

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

Is this type a subtype of the given type?

bool CVC4::Type::isTester ( ) const

Is this a tester type?

Returns: true if the type is a tester type

bool CVC4::Type::isTuple ( ) const

Is this a tuple type?

Returns: true if the type is a tuple type

bool CVC4::Type::isWellFounded ( ) const

Is this a well-founded type?

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

protected

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

Parameters

typeNode the TypeNode to use

Returns: the Type corresponding to the TypeNode

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.

Parameters

t	the type to compare to

Returns: true if the types are not equal

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.

Type& CVC4::Type::operator= ( const Type & t )

Assignment operator.

Parameters

t	the type to assign to this type

Returns: this type after assignment.

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

Comparison for structural equality.

Parameters

t	the type to compare to

Returns: true if the types are equal

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.

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

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.

Parameters

out	the stream to output to

std::string CVC4::Type::toString ( ) const

Constructs a string representation of this type.

Friends And Related Function Documentation

std::ostream& CVC4::operator<<	(	std::ostream &	out,
		const Type &	t
	)

friend

TypeNode expr::exportTypeInternal	(	TypeNode	n,
		NodeManager *	from,
		NodeManager *	nm,
		ExprManagerMapCollection &	vmap
	)

friend

friend class ExprManager

friend

Definition at line 92 of file type.h.

friend class NodeManager

friend

Definition at line 93 of file type.h.

friend class SmtEngine

friend

Definition at line 91 of file type.h.

friend class TypeNode

friend

Definition at line 94 of file type.h.

Field Documentation

NodeManager* CVC4::Type::d_nodeManager

protected

The responsible expression manager.

Definition at line 104 of file type.h.

TypeNode* CVC4::Type::d_typeNode

protected

The internal expression representation.

Definition at line 101 of file type.h.

Referenced by getTypeNode().

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

src/expr/type.h

Public Member Functions

Protected Member Functions

Static Protected Member Functions

Protected Attributes

Friends

Detailed Description

Constructor & Destructor Documentation

Member Function Documentation

Friends And Related Function Documentation

Field Documentation