cvc4-1.4
CVC4::Type Class Reference

Class encapsulating CVC4 expression types. More...

#include <type.h>

Inheritance diagram for CVC4::Type:
CVC3::Type CVC4::ArrayType CVC4::BitVectorType CVC4::BooleanType CVC4::ConstructorType CVC4::DatatypeType CVC4::FunctionType CVC4::IntegerType CVC4::RealType CVC4::RecordType CVC4::SelectorType CVC4::SetType CVC4::SExprType CVC4::SortConstructorType CVC4::SortType CVC4::StringType CVC4::SubrangeType CVC4::TesterType CVC4::TupleType

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...
 
ExprManagergetExprManager () const
 Get this type's ExprManager. More...
 
Type exportTo (ExprManager *exprManager, ExprManagerMapCollection &vmap) const
 Exports this type into a different ExprManager. More...
 
Typeoperator= (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 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...
 

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
emthe expression manager that handles this expression
typeNodethe 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
tthe 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.

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
typeNodethe 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
tthe 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
tthe type to assign to this type
Returns
this type after assignment.
bool CVC4::Type::operator== ( const Type t) const

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

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
outthe 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
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.


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