20 #ifndef __CVC4__DATATYPE_H 21 #define __CVC4__DATATYPE_H 47 const std::vector<DatatypeConstructor>* d_v;
66 const std::vector<DatatypeConstructorArg>* d_v;
113 inline std::string getName()
const throw();
131 bool isUnresolvedSelf()
const throw();
136 std::
string getName() const throw();
142 Expr getSelector() const;
148 Expr getConstructor() const;
162 std::
string getTypeName() const;
167 bool isResolved() const throw();
187 std::vector<DatatypeConstructorArg> d_args;
190 const std::map<std::string, DatatypeType>& resolutions,
191 const std::vector<Type>& placeholders,
192 const std::vector<Type>& replacements,
193 const std::vector< SortConstructorType >& paramTypes,
194 const std::vector< DatatypeType >& paramReplacements,
size_t cindex)
207 Type doParametricSubstitution(
Type range,
208 const std::vector< SortConstructorType >& paramTypes,
209 const std::vector< DatatypeType >& paramReplacements);
218 explicit DatatypeConstructor(std::string name);
225 DatatypeConstructor(std::string name, std::string tester);
232 void addArg(std::string selectorName,
Type selectorType);
255 void addArg(std::string selectorName, DatatypeSelfType);
258 std::string getName()
const throw();
264 Expr getConstructor() const;
270 Expr getTester() const;
275 std::
string getTesterName() const throw();
280 inline
size_t getNumArgs() const throw();
294 Type getSpecializedConstructorType(
Type returnType) const;
307 bool isFinite() const throw(IllegalArgumentException);
314 bool isWellFounded() const throw(IllegalArgumentException);
321 Expr mkGroundTerm(
Type t ) const throw(IllegalArgumentException);
327 inline
bool isResolved() const throw();
330 inline iterator begin() throw();
332 inline iterator end() throw();
334 inline const_iterator begin() const throw();
336 inline const_iterator end() const throw();
354 Expr getSelector(
std::
string name) const;
360 bool involvesExternalType() const;
450 std::vector<Type> d_params;
452 std::vector<DatatypeConstructor> d_constructors;
488 const std::map<std::string, DatatypeType>& resolutions,
489 const std::vector<Type>& placeholders,
490 const std::vector<Type>& replacements,
491 const std::vector< SortConstructorType >& paramTypes,
492 const std::vector< DatatypeType >& paramReplacements)
499 inline explicit Datatype(std::string name,
bool isCo =
false);
505 inline Datatype(std::string name,
const std::vector<Type>& params,
bool isCo =
false);
511 void addConstructor(
const DatatypeConstructor& c);
514 inline std::string getName()
const throw();
517 inline
size_t getNumConstructors() const throw();
520 inline
bool isParametric() const throw();
523 inline
size_t getNumParameters() const throw();
526 inline
Type getParameter(
unsigned int i ) const;
529 inline
std::vector<
Type> getParameters() const;
532 inline
bool isCodatatype() const;
539 Cardinality getCardinality() const throw(IllegalArgumentException);
547 bool isFinite() const throw(IllegalArgumentException);
553 bool isWellFounded() const throw(IllegalArgumentException);
560 Expr mkGroundTerm(
Type t ) const throw(IllegalArgumentException);
566 DatatypeType getDatatypeType() const throw(IllegalArgumentException);
572 DatatypeType getDatatypeType(const
std::vector<
Type>& params) const throw(IllegalArgumentException);
587 bool operator==(const Datatype& other) const throw();
589 inline
bool operator!=(const Datatype& other) const throw();
592 inline
bool isResolved() const throw();
595 inline iterator begin() throw();
597 inline iterator end() throw();
599 inline const_iterator begin() const throw();
601 inline const_iterator end() const throw();
604 const DatatypeConstructor& operator[](
size_t index) const;
611 const DatatypeConstructor& operator[](
std::
string name) const;
621 Expr getConstructor(
std::
string name) const;
627 bool involvesExternalType() const;
642 inline size_t operator()(
const DatatypeConstructor& dtc)
const {
645 inline size_t operator()(
const DatatypeConstructor* dtc)
const {
677 d_involvesExt(false),
688 d_involvesExt(false),
697 return d_constructors.size();
701 return d_params.size() > 0;
705 return d_params.size();
710 CheckArgument(i < d_params.size(), i,
"type parameter index out of range for datatype");
724 return !(*
this == other);
732 return iterator(d_constructors,
true);
736 return iterator(d_constructors,
false);
748 return !d_tester.
isNull();
752 return d_args.size();
Class encapsulating the Selector type.
size_t operator()(const DatatypeConstructor *dtc) const
Class encapsulating CVC4 expressions and methods for constructing new expressions.
const DatatypeConstructorArg & value_type
DatatypeConstructorIterator const_iterator
The (const) type for iterators over constructors.
bool operator==(const DatatypeConstructorArgIterator &other) const
bool isResolved() const
Returns true iff this Datatype constructor has already been resolved.
bool operator!=(const DatatypeConstructorArgIterator &other) const
std::string getName() const
Get the name of this Datatype.
std::string getName() const
Get the name of this Datatype constructor.
The representation of an inductive datatype.
A Datatype constructor argument (i.e., a Datatype field).
A simple representation of a cardinality.
A holder type (used in calls to DatatypeConstructor::addArg()) to allow a Datatype to refer to itself...
Class encapsulating CVC4 expression types.
DatatypeConstructorArgIterator operator++(int)
[[ Add one-line brief description here ]]
Datatype(std::string name, bool isCo=false)
Create a new Datatype of the given name.
std::ostream & operator<<(std::ostream &, const Command &)
void CheckArgument(bool cond, const T &arg, const char *fmt,...)
size_t getNumParameters() const
Get the nubmer of type parameters.
CVC4's exception base class and some associated utilities.
bool isParametric() const
Is this datatype parametric?
DatatypeResolutionException(std::string msg)
bool operator!=(const Datatype &other) const
Return true iff the two Datatypes are not the same.
std::vector< Type > getParameters() const
Get parameters.
DatatypeConstructorIterator iterator
The type for iterators over constructors.
size_t getNumConstructors() const
Get the number of constructors (so far) for this Datatype.
bool operator!=(const DatatypeConstructorIterator &other) const
bool isCodatatype() const
is this a co-datatype?
iterator end()
Get the ending iterator over DatatypeConstructors.
DatatypeConstructorIterator & operator++()
size_t getNumArgs() const
Get the number of arguments (so far) of this Datatype constructor.
DatatypeUnresolvedType(std::string name)
iterator begin()
Get the beginning iterator over DatatypeConstructors.
bool isNull() const
Check if this is a null expression.
const DatatypeConstructor & value_type
bool isResolved() const
Return true iff this Datatype has already been resolved.
Class encapsulating the datatype type.
size_t operator()(const Datatype &dt) const
Representation for an unknown cardinality.
iterator begin()
Get the beginning iterator over DatatypeConstructor args.
Macros that should be defined everywhere during the building of the libraries and driver binary...
const DatatypeConstructor * operator->() const
const DatatypeConstructor & operator*() const
bool isResolved() const
Returns true iff this constructor argument has been resolved.
const DatatypeConstructorArg & operator*() const
iterator end()
Get the ending iterator over DatatypeConstructor args.
An exception that is thrown when a datatype resolution fails.
bool operator==(const DatatypeConstructorIterator &other) const
A constructor for a Datatype.
DatatypeConstructorIterator operator++(int)
DatatypeConstructorArgIterator iterator
The type for iterators over constructor arguments.
A hash function for Datatypes.
Type getParameter(unsigned int i) const
Get parameter.
std::string getName() const
size_t operator()(const Datatype *dt) const
DatatypeConstructorArgIterator & operator++()
An unresolved type (used in calls to DatatypeConstructor::addArg()) to allow a Datatype to refer to i...
size_t operator()(const DatatypeConstructor &dtc) const
DatatypeConstructorArgIterator const_iterator
The (const) type for iterators over constructor arguments.
Interface for expression types.
const DatatypeConstructorArg * operator->() const