cvc4-1.3
CVC4::Datatype Class Reference

The representation of an inductive datatype. More...

#include <datatype.h>

Public Types

typedef std::vector
< DatatypeConstructor >
::iterator 
iterator
 The type for iterators over constructors. More...
 
typedef std::vector
< DatatypeConstructor >
::const_iterator 
const_iterator
 The (const) type for iterators over constructors. More...
 

Public Member Functions

 Datatype (std::string name)
 Create a new Datatype of the given name. More...
 
 Datatype (std::string name, const std::vector< Type > &params)
 Create a new Datatype of the given name, with the given parameterization. More...
 
void addConstructor (const DatatypeConstructor &c)
 Add a constructor to this Datatype. More...
 
std::string getName () const throw ()
 Get the name of this Datatype. More...
 
size_t getNumConstructors () const throw ()
 Get the number of constructors (so far) for this Datatype. More...
 
bool isParametric () const throw ()
 Is this datatype parametric? More...
 
size_t getNumParameters () const throw ()
 Get the nubmer of type parameters. More...
 
Type getParameter (unsigned int i) const
 Get parameter. More...
 
std::vector< TypegetParameters () const
 Get parameters. More...
 
Cardinality getCardinality () const throw (IllegalArgumentException)
 Return the cardinality of this datatype (the sum of the cardinalities of its constructors). More...
 
bool isFinite () const throw (IllegalArgumentException)
 Return true iff this Datatype is finite (all constructors are finite, i.e., there are finitely many ground terms). More...
 
bool isWellFounded () const throw (IllegalArgumentException)
 Return true iff this datatype is well-founded (there exist ground terms). More...
 
Expr mkGroundTerm (Type t) const throw (IllegalArgumentException)
 Construct and return a ground term of this Datatype. More...
 
DatatypeType getDatatypeType () const throw (IllegalArgumentException)
 Get the DatatypeType associated to this Datatype. More...
 
DatatypeType getDatatypeType (const std::vector< Type > &params) const throw (IllegalArgumentException)
 Get the DatatypeType associated to this (parameterized) Datatype. More...
 
bool operator== (const Datatype &other) const throw ()
 Return true iff the two Datatypes are the same. More...
 
bool operator!= (const Datatype &other) const throw ()
 Return true iff the two Datatypes are not the same. More...
 
bool isResolved () const throw ()
 Return true iff this Datatype has already been resolved. More...
 
std::vector
< DatatypeConstructor >
::iterator 
begin () throw ()
 Get the beginning iterator over DatatypeConstructors. More...
 
std::vector
< DatatypeConstructor >
::iterator 
end () throw ()
 Get the ending iterator over DatatypeConstructors. More...
 
std::vector
< DatatypeConstructor >
::const_iterator 
begin () const throw ()
 Get the beginning const_iterator over DatatypeConstructors. More...
 
std::vector
< DatatypeConstructor >
::const_iterator 
end () const throw ()
 Get the ending const_iterator over DatatypeConstructors. More...
 
const DatatypeConstructoroperator[] (size_t index) const
 Get the ith DatatypeConstructor. More...
 
const DatatypeConstructoroperator[] (std::string name) const
 Get the DatatypeConstructor named. More...
 
Expr getConstructor (std::string name) const
 Get the constructor operator for the named constructor. More...
 
bool involvesExternalType () const
 Get whether this datatype involves an external type. More...
 

Static Public Member Functions

static const DatatypedatatypeOf (Expr item)
 Get the datatype of a constructor, selector, or tester operator. More...
 
static size_t indexOf (Expr item)
 Get the index of a constructor or tester in its datatype, or the index of a selector in its constructor. More...
 

Friends

class ExprManager
 

Detailed Description

The representation of an inductive datatype.

This is far more complicated than it first seems. Consider this datatype definition:

DATATYPE nat = succ(pred: nat) | zero END;

You cannot define "nat" until you have a Type for it, but you cannot have a Type for it until you fill in the type of the "pred" selector, which needs the Type. So we have a chicken-and-egg problem. It's even more complicated when we have mutual recursion between datatypes, since the CVC presentation language does not require forward-declarations. Here, we define trees of lists that contain trees of lists (etc):

DATATYPE tree = node(left: tree, right: tree) | leaf(list), list = cons(car: tree, cdr: list) | nil END;

Note that while parsing the "tree" definition, we have to take it on faith that "list" is a valid type. We build Datatype objects to describe "tree" and "list", and their constructors and constructor arguments, but leave any unknown types (including self-references) in an "unresolved" state. After parsing the whole DATATYPE block, we create a DatatypeType through ExprManager::mkMutualDatatypeTypes(). The ExprManager creates a DatatypeType for each, but before "releasing" this type into the wild, it does a round of in-place "resolution" on each Datatype by calling Datatype::resolve() with a map of string -> DatatypeType to allow the datatype to construct the necessary testers and selectors.

An additional point to make is that we want to ease the burden on both the parser AND the users of the CVC4 API, so this class takes on the task of generating its own selectors and testers, for instance. That means that, after reifying the Datatype with the ExprManager, the parser needs to go through the (now-resolved) Datatype and request the constructor, selector, and tester terms. See src/parser/parser.cpp for how this is done. For API usage ideas, see test/unit/util/datatype_black.h.

Datatypes may also be defined parametrically, such as this example:

DATATYPE list[T] = cons(car : T, cdr : list[T]) | null, tree = node(children : list[tree]) | leaf END;

Here, the definition of the parametric datatype list, where T is a type variable. In other words, this defines a family of types list[C] where C is any concrete type. Datatypes can be parameterized over multiple type variables using the syntax sym[ T1, ..., Tn ] = ...,

Definition at line 382 of file datatype.h.

Member Typedef Documentation

The (const) type for iterators over constructors.

Definition at line 399 of file datatype.h.

The type for iterators over constructors.

Definition at line 397 of file datatype.h.

Constructor & Destructor Documentation

CVC4::Datatype::Datatype ( std::string  name)
inlineexplicit

Create a new Datatype of the given name.

Definition at line 618 of file datatype.h.

CVC4::Datatype::Datatype ( std::string  name,
const std::vector< Type > &  params 
)
inline

Create a new Datatype of the given name, with the given parameterization.

Definition at line 627 of file datatype.h.

Member Function Documentation

void CVC4::Datatype::addConstructor ( const DatatypeConstructor c)

Add a constructor to this Datatype.

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

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

Get the beginning iterator over DatatypeConstructors.

Definition at line 671 of file datatype.h.

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

Get the beginning const_iterator over DatatypeConstructors.

Definition at line 679 of file datatype.h.

static const Datatype& CVC4::Datatype::datatypeOf ( Expr  item)
static

Get the datatype of a constructor, selector, or tester operator.

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

Get the ending iterator over DatatypeConstructors.

Definition at line 675 of file datatype.h.

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

Get the ending const_iterator over DatatypeConstructors.

Definition at line 683 of file datatype.h.

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

Return the cardinality of this datatype (the sum of the cardinalities of its constructors).

The Datatype must be resolved.

Expr CVC4::Datatype::getConstructor ( std::string  name) const

Get the constructor operator for the named constructor.

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

This Datatype must be resolved.

DatatypeType CVC4::Datatype::getDatatypeType ( ) const
throw (IllegalArgumentException
)

Get the DatatypeType associated to this Datatype.

Can only be called post-resolution.

DatatypeType CVC4::Datatype::getDatatypeType ( const std::vector< Type > &  params) const
throw (IllegalArgumentException
)

Get the DatatypeType associated to this (parameterized) Datatype.

Can only be called post-resolution.

std::string CVC4::Datatype::getName ( ) const
throw (
)
inline

Get the name of this Datatype.

Definition at line 636 of file datatype.h.

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

size_t CVC4::Datatype::getNumConstructors ( ) const
throw (
)
inline

Get the number of constructors (so far) for this Datatype.

Definition at line 640 of file datatype.h.

size_t CVC4::Datatype::getNumParameters ( ) const
throw (
)
inline

Get the nubmer of type parameters.

Definition at line 648 of file datatype.h.

Type CVC4::Datatype::getParameter ( unsigned int  i) const
inline

Get parameter.

Definition at line 652 of file datatype.h.

References CVC4::CheckArgument(), and isParametric().

std::vector< Type > CVC4::Datatype::getParameters ( ) const
inline

Get parameters.

Definition at line 658 of file datatype.h.

References CVC4::CheckArgument(), and isParametric().

static size_t CVC4::Datatype::indexOf ( Expr  item)
static

Get the index of a constructor or tester in its datatype, or the index of a selector in its constructor.

(Zero is always the first index.)

bool CVC4::Datatype::involvesExternalType ( ) const

Get whether this datatype involves an external type.

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

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

Return true iff this Datatype is finite (all constructors are finite, i.e., there are finitely many ground terms).

If the datatype is not well-founded, this function returns false. The Datatype must be resolved or an exception is thrown.

bool CVC4::Datatype::isParametric ( ) const
throw (
)
inline

Is this datatype parametric?

Definition at line 644 of file datatype.h.

Referenced by getParameter(), and getParameters().

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

Return true iff this Datatype has already been resolved.

Definition at line 667 of file datatype.h.

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

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

The Datatype must be resolved or an exception is thrown.

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

Construct and return a ground term of this Datatype.

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

bool CVC4::Datatype::operator!= ( const Datatype other) const
throw (
)
inline

Return true iff the two Datatypes are not the same.

Definition at line 663 of file datatype.h.

bool CVC4::Datatype::operator== ( const Datatype other) const
throw (
)

Return true iff the two Datatypes are the same.

We need == for mkConst(Datatype) to properly work—since if the Datatype Expr requested is the same as an already-existing one, we need to return that one. For that, we have a hash and operator==. We provide != for symmetry. We don't provide operator<() etc. because given two Datatype Exprs, you could simply compare those rather than the (bare) Datatypes. This means, though, that Datatype cannot be stored in a sorted list or RB tree directly, so maybe we can consider adding these comparison operators later on.

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

Get the ith DatatypeConstructor.

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

Get the DatatypeConstructor named.

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

Friends And Related Function Documentation

friend class ExprManager
friend

Definition at line 445 of file datatype.h.


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