cvc4-1.4
CVC4::Datatype Class Reference

The representation of an inductive datatype. More...

#include <datatype.h>

Public Types

typedef DatatypeConstructorIterator iterator
 The type for iterators over constructors. More...
 
typedef DatatypeConstructorIterator const_iterator
 The (const) type for iterators over constructors. More...
 

Public Member Functions

 Datatype (std::string name, bool isCo=false)
 Create a new Datatype of the given name. More...
 
 Datatype (std::string name, const std::vector< Type > &params, bool isCo=false)
 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...
 
bool isCodatatype () const
 is this a co-datatype? 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...
 
iterator begin () throw ()
 Get the beginning iterator over DatatypeConstructors. More...
 
iterator end () throw ()
 Get the ending iterator over DatatypeConstructors. More...
 
const_iterator begin () const throw ()
 Get the beginning const_iterator over DatatypeConstructors. More...
 
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...
 
static size_t cindexOf (Expr item)
 Get the index of constructor corresponding to selector. 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 423 of file datatype.h.

Member Typedef Documentation

The (const) type for iterators over constructors.

Definition at line 446 of file datatype.h.

The type for iterators over constructors.

Definition at line 444 of file datatype.h.

Constructor & Destructor Documentation

CVC4::Datatype::Datatype ( std::string  name,
bool  isCo = false 
)
inlineexplicit

Create a new Datatype of the given name.

Definition at line 670 of file datatype.h.

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

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

Definition at line 681 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 731 of file datatype.h.

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

Get the beginning const_iterator over DatatypeConstructors.

Definition at line 739 of file datatype.h.

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

Get the index of constructor corresponding to selector.

(Zero is always the first index.)

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 735 of file datatype.h.

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

Get the ending const_iterator over DatatypeConstructors.

Definition at line 743 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 692 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 696 of file datatype.h.

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

Get the nubmer of type parameters.

Definition at line 704 of file datatype.h.

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

Get parameter.

Definition at line 708 of file datatype.h.

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

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

Get parameters.

Definition at line 714 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::isCodatatype ( ) const
inline

is this a co-datatype?

Definition at line 719 of file datatype.h.

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 700 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 727 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 723 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 494 of file datatype.h.


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