A Datatype constructor argument (i.e., a Datatype field). More...

#include <datatype.h>

Public Member Functions
std::string	getName () const throw ()
	Get the name of this constructor argument. More...

Expr	getSelector () const
	Get the selector for this constructor argument; this call is only permitted after resolution. More...

Expr	getConstructor () const
	Get the associated constructor for this constructor argument; this call is only permitted after resolution. More...

SelectorType	getType () const
	Get the type of the selector for this constructor argument; this call is only permitted after resolution. More...

std::string	getTypeName () const
	Get the name of the type of this constructor argument (Datatype field). More...

bool	isResolved () const throw ()
	Returns true iff this constructor argument has been resolved. More...

Detailed Description

A Datatype constructor argument (i.e., a Datatype field).

Definition at line 119 of file datatype.h.

Member Function Documentation

Expr CVC4::DatatypeConstructorArg::getConstructor ( ) const

Get the associated constructor for this constructor argument; this call is only permitted after resolution.

std::string CVC4::DatatypeConstructorArg::getName	(	)	const
throw	(
	)

Get the name of this constructor argument.

Expr CVC4::DatatypeConstructorArg::getSelector ( ) const

Get the selector for this constructor argument; this call is only permitted after resolution.

SelectorType CVC4::DatatypeConstructorArg::getType ( ) const

Get the type of the selector for this constructor argument; this call is only permitted after resolution.

std::string CVC4::DatatypeConstructorArg::getTypeName ( ) const

Get the name of the type of this constructor argument (Datatype field).

Can be used for not-yet-resolved Datatypes (in which case the name of the unresolved type, or "[self]" for a self-referential type is returned).

bool CVC4::DatatypeConstructorArg::isResolved	(	)	const
throw	(
	)

inline

Returns true iff this constructor argument has been resolved.

Definition at line 755 of file datatype.h.

friend class Datatype

friend

Definition at line 129 of file datatype.h.

friend

Definition at line 128 of file datatype.h.

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