cvc4-1.4
CVC4::DatatypeConstructor Class Reference

A constructor for a Datatype. More...

#include <datatype.h>

Public Types

typedef DatatypeConstructorArgIterator iterator
 The type for iterators over constructor arguments. More...
 
typedef DatatypeConstructorArgIterator const_iterator
 The (const) type for iterators over constructor arguments. More...
 

Public Member Functions

 DatatypeConstructor (std::string name)
 Create a new Datatype constructor with the given name for the constructor and the same name (prefixed with "is_") for the tester. More...
 
 DatatypeConstructor (std::string name, std::string tester)
 Create a new Datatype constructor with the given name for the constructor and the given name for the tester. More...
 
void addArg (std::string selectorName, Type selectorType)
 Add an argument (i.e., a data field) of the given name and type to this Datatype constructor. More...
 
void addArg (std::string selectorName, DatatypeUnresolvedType selectorType)
 Add an argument (i.e., a data field) of the given name to this Datatype constructor that refers to an as-yet-unresolved Datatype (which may be mutually-recursive). More...
 
void addArg (std::string selectorName, DatatypeSelfType)
 Add a self-referential (i.e., a data field) of the given name to this Datatype constructor that refers to the enclosing Datatype. More...
 
std::string getName () const throw ()
 Get the name of this Datatype constructor. More...
 
Expr getConstructor () const
 Get the constructor operator of this Datatype constructor. More...
 
Expr getTester () const
 Get the tester operator of this Datatype constructor. More...
 
std::string getTesterName () const throw ()
 Get the tester name for this Datatype constructor. More...
 
size_t getNumArgs () const throw ()
 Get the number of arguments (so far) of this Datatype constructor. More...
 
Type getSpecializedConstructorType (Type returnType) const
 Get the specialized constructor type for a parametric constructor; this call is only permitted after resolution. More...
 
Cardinality getCardinality () const throw (IllegalArgumentException)
 Return the cardinality of this constructor (the product of the cardinalities of its arguments). More...
 
bool isFinite () const throw (IllegalArgumentException)
 Return true iff this constructor is finite (it is nullary or each of its argument types are finite). More...
 
bool isWellFounded () const throw (IllegalArgumentException)
 Return true iff this constructor is well-founded (there exist ground terms). More...
 
Expr mkGroundTerm (Type t) const throw (IllegalArgumentException)
 Construct and return a ground term of this constructor. More...
 
bool isResolved () const throw ()
 Returns true iff this Datatype constructor has already been resolved. More...
 
iterator begin () throw ()
 Get the beginning iterator over DatatypeConstructor args. More...
 
iterator end () throw ()
 Get the ending iterator over DatatypeConstructor args. More...
 
const_iterator begin () const throw ()
 Get the beginning const_iterator over DatatypeConstructor args. More...
 
const_iterator end () const throw ()
 Get the ending const_iterator over DatatypeConstructor args. More...
 
const DatatypeConstructorArgoperator[] (size_t index) const
 Get the ith DatatypeConstructor arg. More...
 
const DatatypeConstructorArgoperator[] (std::string name) const
 Get the DatatypeConstructor arg named. More...
 
Expr getSelector (std::string name) const
 Get the selector named. More...
 
bool involvesExternalType () const
 Get whether this datatype involves an external type. More...
 

Friends

class Datatype
 

Detailed Description

A constructor for a Datatype.

Definition at line 174 of file datatype.h.

Member Typedef Documentation

◆ const_iterator

The (const) type for iterators over constructor arguments.

Definition at line 180 of file datatype.h.

◆ iterator

The type for iterators over constructor arguments.

Definition at line 178 of file datatype.h.

Constructor & Destructor Documentation

◆ DatatypeConstructor() [1/2]

CVC4::DatatypeConstructor::DatatypeConstructor ( std::string  name)
explicit

Create a new Datatype constructor with the given name for the constructor and the same name (prefixed with "is_") for the tester.

The actual constructor and tester (meaning, the Exprs representing operators for these entities) aren't created until resolution time.

◆ DatatypeConstructor() [2/2]

CVC4::DatatypeConstructor::DatatypeConstructor ( std::string  name,
std::string  tester 
)

Create a new Datatype constructor with the given name for the constructor and the given name for the tester.

The actual constructor and tester aren't created until resolution time.

Member Function Documentation

◆ addArg() [1/3]

void CVC4::DatatypeConstructor::addArg ( std::string  selectorName,
Type  selectorType 
)

Add an argument (i.e., a data field) of the given name and type to this Datatype constructor.

Selector names need not be unique; they are for convenience and pretty-printing only.

◆ addArg() [2/3]

void CVC4::DatatypeConstructor::addArg ( std::string  selectorName,
DatatypeUnresolvedType  selectorType 
)

Add an argument (i.e., a data field) of the given name to this Datatype constructor that refers to an as-yet-unresolved Datatype (which may be mutually-recursive).

Selector names need not be unique; they are for convenience and pretty-printing only.

◆ addArg() [3/3]

void CVC4::DatatypeConstructor::addArg ( std::string  selectorName,
DatatypeSelfType   
)

Add a self-referential (i.e., a data field) of the given name to this Datatype constructor that refers to the enclosing Datatype.

For example, using the familiar "nat" Datatype, to create the "pred" field for "succ" constructor, one uses succ::addArg("pred", DatatypeSelfType())—the actual Type cannot be passed because the Datatype is still under construction. Selector names need not be unique; they are for convenience and pretty-printing only.

This is a special case of DatatypeConstructor::addArg(std::string, DatatypeUnresolvedType).

◆ begin() [1/2]

DatatypeConstructor::iterator CVC4::DatatypeConstructor::begin ( )
throw (
)
inline

Get the beginning iterator over DatatypeConstructor args.

Definition at line 772 of file datatype.h.

◆ begin() [2/2]

DatatypeConstructor::const_iterator CVC4::DatatypeConstructor::begin ( ) const
throw (
)
inline

Get the beginning const_iterator over DatatypeConstructor args.

Definition at line 780 of file datatype.h.

◆ end() [1/2]

DatatypeConstructor::iterator CVC4::DatatypeConstructor::end ( )
throw (
)
inline

Get the ending iterator over DatatypeConstructor args.

Definition at line 776 of file datatype.h.

◆ end() [2/2]

DatatypeConstructor::const_iterator CVC4::DatatypeConstructor::end ( ) const
throw (
)
inline

Get the ending const_iterator over DatatypeConstructor args.

Definition at line 784 of file datatype.h.

◆ getCardinality()

Cardinality CVC4::DatatypeConstructor::getCardinality ( ) const
throw (IllegalArgumentException
)

Return the cardinality of this constructor (the product of the cardinalities of its arguments).

◆ getConstructor()

Expr CVC4::DatatypeConstructor::getConstructor ( ) const

Get the constructor operator of this Datatype constructor.

The Datatype must be resolved.

◆ getName()

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

Get the name of this Datatype constructor.

Referenced by CVC4::DatatypeHashFunction::operator()().

◆ getNumArgs()

size_t CVC4::DatatypeConstructor::getNumArgs ( ) const
throw (
)
inline

Get the number of arguments (so far) of this Datatype constructor.

Definition at line 751 of file datatype.h.

◆ getSelector()

Expr CVC4::DatatypeConstructor::getSelector ( std::string  name) const

Get the selector named.

This is a linear search through the arguments, so in the case of multiple, similarly-named arguments, the selector for the first is returned.

◆ getSpecializedConstructorType()

Type CVC4::DatatypeConstructor::getSpecializedConstructorType ( Type  returnType) const

Get the specialized constructor type for a parametric constructor; this call is only permitted after resolution.

Given a (concrete) returnType, the constructor's concrete type in this parametric datatype is returned.

For instance, if the datatype is list[T], with constructor "cons[T]" of type "T -> list[T] -> list[T]", then calling this function with "list[int]" will return the concrete "cons" constructor type for lists of int—namely, "int -> list[int] -> list[int]".

◆ getTester()

Expr CVC4::DatatypeConstructor::getTester ( ) const

Get the tester operator of this Datatype constructor.

The Datatype must be resolved.

◆ getTesterName()

std::string CVC4::DatatypeConstructor::getTesterName ( ) const
throw (
)

Get the tester name for this Datatype constructor.

◆ involvesExternalType()

bool CVC4::DatatypeConstructor::involvesExternalType ( ) const

Get whether this datatype involves an external type.

If so, then we will pose additional requirements for sharing.

◆ isFinite()

bool CVC4::DatatypeConstructor::isFinite ( ) const
throw (IllegalArgumentException
)

Return true iff this constructor is finite (it is nullary or each of its argument types are finite).

This function can only be called for resolved constructors.

◆ isResolved()

bool CVC4::DatatypeConstructor::isResolved ( ) const
throw (
)
inline

Returns true iff this Datatype constructor has already been resolved.

Definition at line 747 of file datatype.h.

References CVC4::Expr::isNull().

◆ isWellFounded()

bool CVC4::DatatypeConstructor::isWellFounded ( ) const
throw (IllegalArgumentException
)

Return true iff this constructor is well-founded (there exist ground terms).

The constructor must be resolved or an exception is thrown.

◆ mkGroundTerm()

Expr CVC4::DatatypeConstructor::mkGroundTerm ( Type  t) const
throw (IllegalArgumentException
)

Construct and return a ground term of this constructor.

The constructor must be both resolved and well-founded, or else an exception is thrown.

◆ operator[]() [1/2]

const DatatypeConstructorArg& CVC4::DatatypeConstructor::operator[] ( size_t  index) const

Get the ith DatatypeConstructor arg.

◆ operator[]() [2/2]

const DatatypeConstructorArg& CVC4::DatatypeConstructor::operator[] ( std::string  name) const

Get the DatatypeConstructor arg named.

This is a linear search through the arguments, so in the case of multiple, similarly-named arguments, the first is returned.

Friends And Related Function Documentation

◆ Datatype

friend class Datatype
friend

Definition at line 196 of file datatype.h.


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