cvc4-1.4
datatype.h
Go to the documentation of this file.
1 /********************* */
18 #include "cvc4_public.h"
19 
20 #ifndef __CVC4__DATATYPE_H
21 #define __CVC4__DATATYPE_H
22 
23 #include <iostream>
24 #include <string>
25 #include <vector>
26 #include <map>
27 
28 namespace CVC4 {
29  // messy; Expr needs Datatype (because it's the payload of a
30  // CONSTANT-kinded expression), and Datatype needs Expr.
31  class CVC4_PUBLIC Datatype;
32 }/* CVC4 namespace */
33 
34 #include "expr/expr.h"
35 #include "expr/type.h"
36 #include "util/hash.h"
37 #include "util/exception.h"
38 
39 namespace CVC4 {
40 
42 
43 class CVC4_PUBLIC DatatypeConstructor;
44 class CVC4_PUBLIC DatatypeConstructorArg;
45 
47  const std::vector<DatatypeConstructor>* d_v;
48  size_t d_i;
49 
50  friend class Datatype;
51 
52  DatatypeConstructorIterator(const std::vector<DatatypeConstructor>& v, bool start) : d_v(&v), d_i(start ? 0 : v.size()) {
53  }
54 
55 public:
57  const DatatypeConstructor& operator*() const { return (*d_v)[d_i]; }
58  const DatatypeConstructor* operator->() const { return &(*d_v)[d_i]; }
59  DatatypeConstructorIterator& operator++() { ++d_i; return *this; }
61  bool operator==(const DatatypeConstructorIterator& other) const { return d_v == other.d_v && d_i == other.d_i; }
62  bool operator!=(const DatatypeConstructorIterator& other) const { return d_v != other.d_v || d_i != other.d_i; }
63 };/* class DatatypeConstructorIterator */
64 
66  const std::vector<DatatypeConstructorArg>* d_v;
67  size_t d_i;
68 
69  friend class DatatypeConstructor;
70 
71  DatatypeConstructorArgIterator(const std::vector<DatatypeConstructorArg>& v, bool start) : d_v(&v), d_i(start ? 0 : v.size()) {
72  }
73 
74 public:
76  const DatatypeConstructorArg& operator*() const { return (*d_v)[d_i]; }
77  const DatatypeConstructorArg* operator->() const { return &(*d_v)[d_i]; }
78  DatatypeConstructorArgIterator& operator++() { ++d_i; return *this; }
80  bool operator==(const DatatypeConstructorArgIterator& other) const { return d_v == other.d_v && d_i == other.d_i; }
81  bool operator!=(const DatatypeConstructorArgIterator& other) const { return d_v != other.d_v || d_i != other.d_i; }
82 };/* class DatatypeConstructorArgIterator */
83 
88 public:
89  inline DatatypeResolutionException(std::string msg);
90 };/* class DatatypeResolutionException */
91 
99 };/* class DatatypeSelfType */
100 
110  std::string d_name;
111 public:
112  inline DatatypeUnresolvedType(std::string name);
113  inline std::string getName() const throw();
114 };/* class DatatypeUnresolvedType */
115 
120 
121  std::string d_name;
122  Expr d_selector;
124  Expr d_constructor;
125  bool d_resolved;
126 
127  DatatypeConstructorArg(std::string name, Expr selector);
128  friend class DatatypeConstructor;
129  friend class Datatype;
130 
131  bool isUnresolvedSelf() const throw();
132 
133 public:
134 
136  std::string getName() const throw();
137 
142  Expr getSelector() const;
143 
148  Expr getConstructor() const;
149 
154  SelectorType getType() const;
155 
162  std::string getTypeName() const;
163 
167  bool isResolved() const throw();
168 
169 };/* class DatatypeConstructorArg */
170 
175 public:
176 
181 
182 private:
183 
184  std::string d_name;
185  Expr d_constructor;
186  Expr d_tester;
187  std::vector<DatatypeConstructorArg> d_args;
188 
189  void resolve(ExprManager* em, DatatypeType self,
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)
196  friend class Datatype;
197 
207  Type doParametricSubstitution(Type range,
208  const std::vector< SortConstructorType >& paramTypes,
209  const std::vector< DatatypeType >& paramReplacements);
210 public:
218  explicit DatatypeConstructor(std::string name);
219 
225  DatatypeConstructor(std::string name, std::string tester);
226 
232  void addArg(std::string selectorName, Type selectorType);
233 
240  void addArg(std::string selectorName, DatatypeUnresolvedType selectorType);
241 
255  void addArg(std::string selectorName, DatatypeSelfType);
256 
258  std::string getName() const throw();
259 
264  Expr getConstructor() const;
265 
270  Expr getTester() const;
271 
275  std::string getTesterName() const throw();
276 
280  inline size_t getNumArgs() const throw();
281 
294  Type getSpecializedConstructorType(Type returnType) const;
295 
300  Cardinality getCardinality() const throw(IllegalArgumentException);
301 
307  bool isFinite() const throw(IllegalArgumentException);
308 
314  bool isWellFounded() const throw(IllegalArgumentException);
315 
321  Expr mkGroundTerm( Type t ) const throw(IllegalArgumentException);
322 
327  inline bool isResolved() const throw();
328 
330  inline iterator begin() throw();
332  inline iterator end() throw();
334  inline const_iterator begin() const throw();
336  inline const_iterator end() const throw();
337 
339  const DatatypeConstructorArg& operator[](size_t index) const;
340 
346  const DatatypeConstructorArg& operator[](std::string name) const;
347 
354  Expr getSelector(std::string name) const;
355 
360  bool involvesExternalType() const;
361 
362 };/* class DatatypeConstructor */
363 
424 public:
428  static const Datatype& datatypeOf(Expr item) CVC4_PUBLIC;
429 
435  static size_t indexOf(Expr item) CVC4_PUBLIC;
436 
441  static size_t cindexOf(Expr item) CVC4_PUBLIC;
442 
447 
448 private:
449  std::string d_name;
450  std::vector<Type> d_params;
451  bool d_isCo;
452  std::vector<DatatypeConstructor> d_constructors;
453  bool d_resolved;
454  Type d_self;
455  bool d_involvesExt;
456 
457  // "mutable" because computing the cardinality can be expensive,
458  // and so it's computed just once, on demand---this is the cache
459  mutable Cardinality d_card;
460 
487  void resolve(ExprManager* em,
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)
493  throw(IllegalArgumentException, DatatypeResolutionException);
494  friend class ExprManager;// for access to resolve()
495 
496 public:
497 
499  inline explicit Datatype(std::string name, bool isCo = false);
500 
505  inline Datatype(std::string name, const std::vector<Type>& params, bool isCo = false);
506 
511  void addConstructor(const DatatypeConstructor& c);
512 
514  inline std::string getName() const throw();
515 
517  inline size_t getNumConstructors() const throw();
518 
520  inline bool isParametric() const throw();
521 
523  inline size_t getNumParameters() const throw();
524 
526  inline Type getParameter( unsigned int i ) const;
527 
529  inline std::vector<Type> getParameters() const;
530 
532  inline bool isCodatatype() const;
533 
539  Cardinality getCardinality() const throw(IllegalArgumentException);
540 
547  bool isFinite() const throw(IllegalArgumentException);
548 
553  bool isWellFounded() const throw(IllegalArgumentException);
554 
560  Expr mkGroundTerm( Type t ) const throw(IllegalArgumentException);
561 
566  DatatypeType getDatatypeType() const throw(IllegalArgumentException);
567 
572  DatatypeType getDatatypeType(const std::vector<Type>& params) const throw(IllegalArgumentException);
573 
587  bool operator==(const Datatype& other) const throw();
589  inline bool operator!=(const Datatype& other) const throw();
590 
592  inline bool isResolved() const throw();
593 
595  inline iterator begin() throw();
597  inline iterator end() throw();
599  inline const_iterator begin() const throw();
601  inline const_iterator end() const throw();
602 
604  const DatatypeConstructor& operator[](size_t index) const;
605 
611  const DatatypeConstructor& operator[](std::string name) const;
612 
621  Expr getConstructor(std::string name) const;
622 
627  bool involvesExternalType() const;
628 
629 };/* class Datatype */
630 
635 struct CVC4_PUBLIC DatatypeHashFunction {
636  inline size_t operator()(const Datatype& dt) const {
637  return StringHashFunction()(dt.getName());
638  }
639  inline size_t operator()(const Datatype* dt) const {
640  return StringHashFunction()(dt->getName());
641  }
642  inline size_t operator()(const DatatypeConstructor& dtc) const {
643  return StringHashFunction()(dtc.getName());
644  }
645  inline size_t operator()(const DatatypeConstructor* dtc) const {
646  return StringHashFunction()(dtc->getName());
647  }
648 };/* struct DatatypeHashFunction */
649 
650 // FUNCTION DECLARATIONS FOR OUTPUT STREAMS
651 
652 std::ostream& operator<<(std::ostream& os, const Datatype& dt) CVC4_PUBLIC;
653 std::ostream& operator<<(std::ostream& os, const DatatypeConstructor& ctor) CVC4_PUBLIC;
654 std::ostream& operator<<(std::ostream& os, const DatatypeConstructorArg& arg) CVC4_PUBLIC;
655 
656 // INLINE FUNCTIONS
657 
659  Exception(msg) {
660 }
661 
663  d_name(name) {
664 }
665 
666 inline std::string DatatypeUnresolvedType::getName() const throw() {
667  return d_name;
668 }
669 
670 inline Datatype::Datatype(std::string name, bool isCo) :
671  d_name(name),
672  d_params(),
673  d_isCo(isCo),
674  d_constructors(),
675  d_resolved(false),
676  d_self(),
677  d_involvesExt(false),
678  d_card(CardinalityUnknown()) {
679 }
680 
681 inline Datatype::Datatype(std::string name, const std::vector<Type>& params, bool isCo) :
682  d_name(name),
683  d_params(params),
684  d_isCo(isCo),
685  d_constructors(),
686  d_resolved(false),
687  d_self(),
688  d_involvesExt(false),
689  d_card(CardinalityUnknown()) {
690 }
691 
692 inline std::string Datatype::getName() const throw() {
693  return d_name;
694 }
695 
696 inline size_t Datatype::getNumConstructors() const throw() {
697  return d_constructors.size();
698 }
699 
700 inline bool Datatype::isParametric() const throw() {
701  return d_params.size() > 0;
702 }
703 
704 inline size_t Datatype::getNumParameters() const throw() {
705  return d_params.size();
706 }
707 
708 inline Type Datatype::getParameter( unsigned int i ) const {
709  CheckArgument(isParametric(), this, "cannot get type parameter of a non-parametric datatype");
710  CheckArgument(i < d_params.size(), i, "type parameter index out of range for datatype");
711  return d_params[i];
712 }
713 
714 inline std::vector<Type> Datatype::getParameters() const {
715  CheckArgument(isParametric(), this, "cannot get type parameters of a non-parametric datatype");
716  return d_params;
717 }
718 
719 inline bool Datatype::isCodatatype() const {
720  return d_isCo;
721 }
722 
723 inline bool Datatype::operator!=(const Datatype& other) const throw() {
724  return !(*this == other);
725 }
726 
727 inline bool Datatype::isResolved() const throw() {
728  return d_resolved;
729 }
730 
732  return iterator(d_constructors, true);
733 }
734 
736  return iterator(d_constructors, false);
737 }
738 
740  return const_iterator(d_constructors, true);
741 }
742 
743 inline Datatype::const_iterator Datatype::end() const throw() {
744  return const_iterator(d_constructors, false);
745 }
746 
747 inline bool DatatypeConstructor::isResolved() const throw() {
748  return !d_tester.isNull();
749 }
750 
751 inline size_t DatatypeConstructor::getNumArgs() const throw() {
752  return d_args.size();
753 }
754 
755 inline bool DatatypeConstructorArg::isResolved() const throw() {
756  // We could just write:
757  //
758  // return !d_selector.isNull() && d_selector.getType().isSelector();
759  //
760  // HOWEVER, this causes problems in ExprManager tear-down, because
761  // the attributes are removed before the pool is purged. When the
762  // pool is purged, this triggers an equality test between Datatypes,
763  // and this triggers a call to isResolved(), which breaks because
764  // d_selector has no type after attributes are stripped.
765  //
766  // This problem, coupled with the fact that this function is called
767  // _often_, means we should just use a boolean flag.
768  //
769  return d_resolved;
770 }
771 
773  return iterator(d_args, true);
774 }
775 
777  return iterator(d_args, false);
778 }
779 
781  return const_iterator(d_args, true);
782 }
783 
785  return const_iterator(d_args, false);
786 }
787 
788 }/* CVC4 namespace */
789 
790 #endif /* __CVC4__DATATYPE_H */
Class encapsulating the Selector type.
Definition: type.h:683
size_t operator()(const DatatypeConstructor *dtc) const
Definition: datatype.h:645
Class encapsulating CVC4 expressions and methods for constructing new expressions.
Definition: expr.h:227
const DatatypeConstructorArg & value_type
Definition: datatype.h:75
DatatypeConstructorIterator const_iterator
The (const) type for iterators over constructors.
Definition: datatype.h:446
bool operator==(const DatatypeConstructorArgIterator &other) const
Definition: datatype.h:80
bool isResolved() const
Returns true iff this Datatype constructor has already been resolved.
Definition: datatype.h:747
bool operator!=(const DatatypeConstructorArgIterator &other) const
Definition: datatype.h:81
std::string getName() const
Get the name of this Datatype.
Definition: datatype.h:692
void * ExprManager
std::string getName() const
Get the name of this Datatype constructor.
The representation of an inductive datatype.
Definition: datatype.h:423
A Datatype constructor argument (i.e., a Datatype field).
Definition: datatype.h:119
A simple representation of a cardinality.
Definition: cardinality.h:65
A holder type (used in calls to DatatypeConstructor::addArg()) to allow a Datatype to refer to itself...
Definition: datatype.h:98
Class encapsulating CVC4 expression types.
Definition: type.h:89
DatatypeConstructorArgIterator operator++(int)
Definition: datatype.h:79
[[ Add one-line brief description here ]]
STL namespace.
Datatype(std::string name, bool isCo=false)
Create a new Datatype of the given name.
Definition: datatype.h:670
std::ostream & operator<<(std::ostream &, const Command &)
void CheckArgument(bool cond, const T &arg, const char *fmt,...)
Definition: exception.h:140
size_t getNumParameters() const
Get the nubmer of type parameters.
Definition: datatype.h:704
CVC4&#39;s exception base class and some associated utilities.
bool isParametric() const
Is this datatype parametric?
Definition: datatype.h:700
DatatypeResolutionException(std::string msg)
Definition: datatype.h:658
bool operator!=(const Datatype &other) const
Return true iff the two Datatypes are not the same.
Definition: datatype.h:723
std::vector< Type > getParameters() const
Get parameters.
Definition: datatype.h:714
DatatypeConstructorIterator iterator
The type for iterators over constructors.
Definition: datatype.h:444
size_t getNumConstructors() const
Get the number of constructors (so far) for this Datatype.
Definition: datatype.h:696
bool operator!=(const DatatypeConstructorIterator &other) const
Definition: datatype.h:62
bool isCodatatype() const
is this a co-datatype?
Definition: datatype.h:719
iterator end()
Get the ending iterator over DatatypeConstructors.
Definition: datatype.h:735
DatatypeConstructorIterator & operator++()
Definition: datatype.h:59
size_t getNumArgs() const
Get the number of arguments (so far) of this Datatype constructor.
Definition: datatype.h:751
DatatypeUnresolvedType(std::string name)
Definition: datatype.h:662
iterator begin()
Get the beginning iterator over DatatypeConstructors.
Definition: datatype.h:731
bool isNull() const
Check if this is a null expression.
#define CVC4_PUBLIC
Definition: cvc4_public.h:30
const DatatypeConstructor & value_type
Definition: datatype.h:56
bool isResolved() const
Return true iff this Datatype has already been resolved.
Definition: datatype.h:727
Class encapsulating the datatype type.
Definition: type.h:615
size_t operator()(const Datatype &dt) const
Definition: datatype.h:636
Representation for an unknown cardinality.
Definition: cardinality.h:54
iterator begin()
Get the beginning iterator over DatatypeConstructor args.
Definition: datatype.h:772
Macros that should be defined everywhere during the building of the libraries and driver binary...
const DatatypeConstructor * operator->() const
Definition: datatype.h:58
const DatatypeConstructor & operator*() const
Definition: datatype.h:57
bool isResolved() const
Returns true iff this constructor argument has been resolved.
Definition: datatype.h:755
const DatatypeConstructorArg & operator*() const
Definition: datatype.h:76
iterator end()
Get the ending iterator over DatatypeConstructor args.
Definition: datatype.h:776
An exception that is thrown when a datatype resolution fails.
Definition: datatype.h:87
bool operator==(const DatatypeConstructorIterator &other) const
Definition: datatype.h:61
expr.h
A constructor for a Datatype.
Definition: datatype.h:174
DatatypeConstructorIterator operator++(int)
Definition: datatype.h:60
DatatypeConstructorArgIterator iterator
The type for iterators over constructor arguments.
Definition: datatype.h:178
A hash function for Datatypes.
Definition: datatype.h:635
Type getParameter(unsigned int i) const
Get parameter.
Definition: datatype.h:708
std::string getName() const
Definition: datatype.h:666
size_t operator()(const Datatype *dt) const
Definition: datatype.h:639
DatatypeConstructorArgIterator & operator++()
Definition: datatype.h:78
An unresolved type (used in calls to DatatypeConstructor::addArg()) to allow a Datatype to refer to i...
Definition: datatype.h:109
size_t operator()(const DatatypeConstructor &dtc) const
Definition: datatype.h:642
DatatypeConstructorArgIterator const_iterator
The (const) type for iterators over constructor arguments.
Definition: datatype.h:180
Interface for expression types.
const DatatypeConstructorArg * operator->() const
Definition: datatype.h:77