cvc4-1.4
CVC4::DatatypeConstructorArg Class Reference

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

Friends

class DatatypeConstructor
 
class Datatype
 

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.

Friends And Related Function Documentation

friend class Datatype
friend

Definition at line 129 of file datatype.h.

friend class DatatypeConstructor
friend

Definition at line 128 of file datatype.h.


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