20 #ifndef __CVC4__DATATYPE_H
21 #define __CVC4__DATATYPE_H
72 inline std::string getName()
const throw();
90 bool isUnresolvedSelf()
const throw();
95 std::
string getName() const throw();
101 Expr getSelector() const;
107 Expr getConstructor() const;
121 std::
string getTypeName() const;
126 bool isResolved() const throw();
137 typedef std::vector<DatatypeConstructorArg>::iterator
iterator;
146 std::vector<DatatypeConstructorArg> d_args;
149 const std::map<std::string, DatatypeType>& resolutions,
150 const std::vector<Type>& placeholders,
151 const std::vector<Type>& replacements,
152 const std::vector< SortConstructorType >& paramTypes,
153 const std::vector< DatatypeType >& paramReplacements)
166 Type doParametricSubstitution(
Type range,
167 const std::vector< SortConstructorType >& paramTypes,
168 const std::vector< DatatypeType >& paramReplacements);
177 explicit DatatypeConstructor(std::string name);
184 DatatypeConstructor(std::string name, std::string tester);
191 void addArg(std::string selectorName,
Type selectorType);
217 std::string getName()
const throw();
223 Expr getConstructor() const;
229 Expr getTester() const;
234 std::
string getTesterName() const throw();
239 inline
size_t getNumArgs() const throw();
253 Type getSpecializedConstructorType(
Type returnType) const;
266 bool isFinite() const throw(IllegalArgumentException);
273 bool isWellFounded() const throw(IllegalArgumentException);
280 Expr mkGroundTerm(
Type t ) const throw(IllegalArgumentException);
286 inline
bool isResolved() const throw();
289 inline iterator begin() throw();
291 inline iterator end() throw();
293 inline const_iterator begin() const throw();
295 inline const_iterator end() const throw();
313 Expr getSelector(std::
string name) const;
319 bool involvesExternalType() const;
397 typedef std::vector<DatatypeConstructor>::iterator
iterator;
403 std::vector<Type> d_params;
404 std::vector<DatatypeConstructor> d_constructors;
439 const std::map<std::string, DatatypeType>& resolutions,
440 const std::vector<Type>& placeholders,
441 const std::vector<Type>& replacements,
442 const std::vector< SortConstructorType >& paramTypes,
443 const std::vector< DatatypeType >& paramReplacements)
450 inline explicit Datatype(std::string name);
456 inline Datatype(std::string name,
const std::vector<Type>& params);
462 void addConstructor(
const DatatypeConstructor& c);
465 inline std::string getName()
const throw();
468 inline
size_t getNumConstructors() const throw();
471 inline
bool isParametric() const throw();
474 inline
size_t getNumParameters() const throw();
477 inline
Type getParameter(
unsigned int i ) const;
480 inline std::vector<
Type> getParameters() const;
487 Cardinality getCardinality() const throw(IllegalArgumentException);
495 bool isFinite() const throw(IllegalArgumentException);
501 bool isWellFounded() const throw(IllegalArgumentException);
508 Expr mkGroundTerm(
Type t ) const throw(IllegalArgumentException);
514 DatatypeType getDatatypeType() const throw(IllegalArgumentException);
520 DatatypeType getDatatypeType(const std::vector<
Type>& params) const throw(IllegalArgumentException);
535 bool operator==(const Datatype& other) const throw();
537 inline
bool operator!=(const Datatype& other) const throw();
540 inline
bool isResolved() const throw();
543 inline std::vector<DatatypeConstructor>::iterator begin() throw();
545 inline std::vector<DatatypeConstructor>::iterator end() throw();
547 inline std::vector<DatatypeConstructor>::const_iterator begin() const throw();
549 inline std::vector<DatatypeConstructor>::const_iterator end() const throw();
552 const DatatypeConstructor& operator[](
size_t index) const;
559 const DatatypeConstructor& operator[](std::
string name) const;
569 Expr getConstructor(std::
string name) const;
575 bool involvesExternalType() const;
590 inline size_t operator()(
const DatatypeConstructor& dtc)
const {
593 inline size_t operator()(
const DatatypeConstructor* dtc)
const {
641 return d_constructors.size();
645 return d_params.size() > 0;
649 return d_params.size();
654 CheckArgument(i < d_params.size(), i,
"type parameter index out of range for datatype");
664 return !(*
this == other);
672 return d_constructors.begin();
676 return d_constructors.end();
680 return d_constructors.begin();
684 return d_constructors.end();
688 return !d_tester.
isNull();
692 return d_args.size();
713 return d_args.begin();
721 return d_args.begin();
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.
bool isResolved() const
Return true iff this Datatype has already been resolved.
size_t operator()(const DatatypeConstructor &dtc) const
size_t operator()(const Datatype *dt) const
The representation of an inductive datatype.
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.
[[ Add one-line brief description here ]]
std::ostream & operator<<(std::ostream &, const Command &)
void CheckArgument(bool cond, const T &arg, const char *fmt,...)
size_t getNumConstructors() const
Get the number of constructors (so far) for this Datatype.
std::string getName() const
CVC4's exception base class and some associated utilities.
DatatypeResolutionException(std::string msg)
This is CVC4 release version For build and installation please see the INSTALL file included with this distribution This first official release of CVC4 is the result of more than three years of efforts by researchers at New York University and The University of Iowa The project leaders are Clark please refer to the AUTHORS file in the source distribution CVC4 is a tool for determining the satisfiability of a first order formula modulo a first order CVC CVC3 but does not directly incorporate code from any previous version CVC4 is intended to be an open and extensible SMT engine It can be used as a stand alone tool or as a library It has been designed to increase the performance and reduce the memory overhead of its predecessors It is written entirely in C and is released under a free software see the INSTALL file that comes with this distribution We recommend that you visit our CVC4 tutorials online please write to the cvc users cs nyu edu mailing list *if you need to report a bug with CVC4
std::vector< DatatypeConstructor >::iterator end()
Get the ending iterator over DatatypeConstructors.
std::vector< DatatypeConstructor >::iterator iterator
The type for iterators over constructors.
Datatype(std::string name)
Create a new Datatype of the given name.
DatatypeUnresolvedType(std::string name)
std::vector< DatatypeConstructor >::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.
Class encapsulating the datatype type.
Representation for an unknown cardinality.
std::vector< DatatypeConstructor >::const_iterator const_iterator
The (const) type for iterators over constructors.
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.
std::vector< DatatypeConstructorArg >::const_iterator const_iterator
The (const) type for iterators over constructor arguments.
bool isResolved() const
Returns true iff this constructor argument has been resolved.
iterator end()
Get the ending iterator over DatatypeConstructor args.
An exception that is thrown when a datatype resolution fails.
A constructor for a Datatype.
A hash function for Datatypes.
std::vector< DatatypeConstructorArg >::iterator iterator
The type for iterators over constructor arguments.
std::string getName() const
Get the name of this Datatype.
An unresolved type (used in calls to DatatypeConstructor::addArg()) to allow a Datatype to refer to i...
std::string getName() const
Get the name of this Datatype constructor.
Interface for expression types.