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();
size_t operator()(const Datatype &dt) const
Class encapsulating the Selector type.
size_t getNumArgs() const
Get the number of arguments (so far) of this Datatype constructor.
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 isResolved() const
Return true iff this Datatype has already been resolved.
size_t operator()(const DatatypeConstructor &dtc) const
bool operator!=(const DatatypeConstructorIterator &other) const
size_t operator()(const Datatype *dt) const
The representation of an inductive datatype.
const DatatypeConstructor & operator*() const
A Datatype constructor argument (i.e., a Datatype field).
bool isNull() const
Check if this is a null expression.
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)
std::ostream & operator<<(std::ostream &out, const Predicate &p)
[[ Add one-line brief description here ]]
Datatype(std::string name, bool isCo=false)
Create a new Datatype of the given name.
void CheckArgument(bool cond, const T &arg, const char *fmt,...)
size_t getNumConstructors() const
Get the number of constructors (so far) for this Datatype.
const DatatypeConstructorArg & operator*() const
std::string getName() const
CVC4's exception base class and some associated utilities.
bool operator!=(const DatatypeConstructorArgIterator &other) const
DatatypeResolutionException(std::string msg)
DatatypeConstructorIterator iterator
The type for iterators over constructors.
iterator end()
Get the ending iterator over DatatypeConstructors.
DatatypeConstructorIterator & operator++()
DatatypeUnresolvedType(std::string name)
iterator begin()
Get the beginning iterator over DatatypeConstructors.
bool operator!=(const Datatype &other) const
Return true iff the two Datatypes are not the same.
std::vector< Type > getParameters() const
Get parameters.
size_t getNumParameters() const
Get the nubmer of type parameters.
bool isParametric() const
Is this datatype parametric?
Type getParameter(unsigned int i) const
Get parameter.
const DatatypeConstructor & value_type
Class encapsulating the datatype type.
bool operator==(const DatatypeConstructorArgIterator &other) 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...
bool isResolved() const
Returns true iff this Datatype constructor has already been resolved.
bool isResolved() const
Returns true iff this constructor argument has been resolved.
bool isCodatatype() const
is this a co-datatype?
iterator end()
Get the ending iterator over DatatypeConstructor args.
An exception that is thrown when a datatype resolution fails.
A constructor for a Datatype.
bool operator==(const DatatypeConstructorIterator &other) const
DatatypeConstructorIterator operator++(int)
DatatypeConstructorArgIterator iterator
The type for iterators over constructor arguments.
A hash function for Datatypes.
std::string getName() const
Get the name of this Datatype.
DatatypeConstructorArgIterator & operator++()
An unresolved type (used in calls to DatatypeConstructor::addArg()) to allow a Datatype to refer to i...
const DatatypeConstructor * operator->() const
const DatatypeConstructorArg * operator->() const
DatatypeConstructorArgIterator const_iterator
The (const) type for iterators over constructor arguments.
std::string getName() const
Get the name of this Datatype constructor.
Interface for expression types.