cvc4-1.3
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 
47 public:
48  inline DatatypeResolutionException(std::string msg);
49 };/* class DatatypeResolutionException */
50 
58 };/* class DatatypeSelfType */
59 
69  std::string d_name;
70 public:
71  inline DatatypeUnresolvedType(std::string name);
72  inline std::string getName() const throw();
73 };/* class DatatypeUnresolvedType */
74 
79 
80  std::string d_name;
81  Expr d_selector;
83  Expr d_constructor;
84  bool d_resolved;
85 
86  DatatypeConstructorArg(std::string name, Expr selector);
87  friend class DatatypeConstructor;
88  friend class Datatype;
89 
90  bool isUnresolvedSelf() const throw();
91 
92 public:
93 
95  std::string getName() const throw();
96 
101  Expr getSelector() const;
102 
107  Expr getConstructor() const;
108 
113  SelectorType getType() const;
114 
121  std::string getTypeName() const;
122 
126  bool isResolved() const throw();
127 
128 };/* class DatatypeConstructorArg */
129 
134 public:
135 
137  typedef std::vector<DatatypeConstructorArg>::iterator iterator;
139  typedef std::vector<DatatypeConstructorArg>::const_iterator const_iterator;
140 
141 private:
142 
143  std::string d_name;
144  Expr d_constructor;
145  Expr d_tester;
146  std::vector<DatatypeConstructorArg> d_args;
147 
148  void resolve(ExprManager* em, DatatypeType self,
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)
155  friend class Datatype;
156 
166  Type doParametricSubstitution(Type range,
167  const std::vector< SortConstructorType >& paramTypes,
168  const std::vector< DatatypeType >& paramReplacements);
169 public:
177  explicit DatatypeConstructor(std::string name);
178 
184  DatatypeConstructor(std::string name, std::string tester);
185 
191  void addArg(std::string selectorName, Type selectorType);
192 
199  void addArg(std::string selectorName, DatatypeUnresolvedType selectorType);
200 
214  void addArg(std::string selectorName, DatatypeSelfType);
215 
217  std::string getName() const throw();
218 
223  Expr getConstructor() const;
224 
229  Expr getTester() const;
230 
234  std::string getTesterName() const throw();
235 
239  inline size_t getNumArgs() const throw();
240 
253  Type getSpecializedConstructorType(Type returnType) const;
254 
259  Cardinality getCardinality() const throw(IllegalArgumentException);
260 
266  bool isFinite() const throw(IllegalArgumentException);
267 
273  bool isWellFounded() const throw(IllegalArgumentException);
274 
280  Expr mkGroundTerm( Type t ) const throw(IllegalArgumentException);
281 
286  inline bool isResolved() const throw();
287 
289  inline iterator begin() throw();
291  inline iterator end() throw();
293  inline const_iterator begin() const throw();
295  inline const_iterator end() const throw();
296 
298  const DatatypeConstructorArg& operator[](size_t index) const;
299 
305  const DatatypeConstructorArg& operator[](std::string name) const;
306 
313  Expr getSelector(std::string name) const;
314 
319  bool involvesExternalType() const;
320 
321 };/* class DatatypeConstructor */
322 
383 public:
387  static const Datatype& datatypeOf(Expr item) CVC4_PUBLIC;
388 
394  static size_t indexOf(Expr item) CVC4_PUBLIC;
395 
397  typedef std::vector<DatatypeConstructor>::iterator iterator;
399  typedef std::vector<DatatypeConstructor>::const_iterator const_iterator;
400 
401 private:
402  std::string d_name;
403  std::vector<Type> d_params;
404  std::vector<DatatypeConstructor> d_constructors;
405  bool d_resolved;
406  Type d_self;
407 
408  // "mutable" because computing the cardinality can be expensive,
409  // and so it's computed just once, on demand---this is the cache
410  mutable Cardinality d_card;
411 
438  void resolve(ExprManager* em,
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)
444  throw(IllegalArgumentException, DatatypeResolutionException);
445  friend class ExprManager;// for access to resolve()
446 
447 public:
448 
450  inline explicit Datatype(std::string name);
451 
456  inline Datatype(std::string name, const std::vector<Type>& params);
457 
462  void addConstructor(const DatatypeConstructor& c);
463 
465  inline std::string getName() const throw();
466 
468  inline size_t getNumConstructors() const throw();
469 
471  inline bool isParametric() const throw();
472 
474  inline size_t getNumParameters() const throw();
475 
477  inline Type getParameter( unsigned int i ) const;
478 
480  inline std::vector<Type> getParameters() const;
481 
487  Cardinality getCardinality() const throw(IllegalArgumentException);
488 
495  bool isFinite() const throw(IllegalArgumentException);
496 
501  bool isWellFounded() const throw(IllegalArgumentException);
502 
508  Expr mkGroundTerm( Type t ) const throw(IllegalArgumentException);
509 
514  DatatypeType getDatatypeType() const throw(IllegalArgumentException);
515 
520  DatatypeType getDatatypeType(const std::vector<Type>& params) const throw(IllegalArgumentException);
521 
535  bool operator==(const Datatype& other) const throw();
537  inline bool operator!=(const Datatype& other) const throw();
538 
540  inline bool isResolved() const throw();
541 
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();
550 
552  const DatatypeConstructor& operator[](size_t index) const;
553 
559  const DatatypeConstructor& operator[](std::string name) const;
560 
569  Expr getConstructor(std::string name) const;
570 
575  bool involvesExternalType() const;
576 
577 };/* class Datatype */
578 
583 struct CVC4_PUBLIC DatatypeHashFunction {
584  inline size_t operator()(const Datatype& dt) const {
585  return StringHashFunction()(dt.getName());
586  }
587  inline size_t operator()(const Datatype* dt) const {
588  return StringHashFunction()(dt->getName());
589  }
590  inline size_t operator()(const DatatypeConstructor& dtc) const {
591  return StringHashFunction()(dtc.getName());
592  }
593  inline size_t operator()(const DatatypeConstructor* dtc) const {
594  return StringHashFunction()(dtc->getName());
595  }
596 };/* struct DatatypeHashFunction */
597 
598 // FUNCTION DECLARATIONS FOR OUTPUT STREAMS
599 
600 std::ostream& operator<<(std::ostream& os, const Datatype& dt) CVC4_PUBLIC;
601 std::ostream& operator<<(std::ostream& os, const DatatypeConstructor& ctor) CVC4_PUBLIC;
602 std::ostream& operator<<(std::ostream& os, const DatatypeConstructorArg& arg) CVC4_PUBLIC;
603 
604 // INLINE FUNCTIONS
605 
607  Exception(msg) {
608 }
609 
611  d_name(name) {
612 }
613 
614 inline std::string DatatypeUnresolvedType::getName() const throw() {
615  return d_name;
616 }
617 
618 inline Datatype::Datatype(std::string name) :
619  d_name(name),
620  d_params(),
621  d_constructors(),
622  d_resolved(false),
623  d_self(),
624  d_card(CardinalityUnknown()) {
625 }
626 
627 inline Datatype::Datatype(std::string name, const std::vector<Type>& params) :
628  d_name(name),
629  d_params(params),
630  d_constructors(),
631  d_resolved(false),
632  d_self(),
633  d_card(CardinalityUnknown()) {
634 }
635 
636 inline std::string Datatype::getName() const throw() {
637  return d_name;
638 }
639 
640 inline size_t Datatype::getNumConstructors() const throw() {
641  return d_constructors.size();
642 }
643 
644 inline bool Datatype::isParametric() const throw() {
645  return d_params.size() > 0;
646 }
647 
648 inline size_t Datatype::getNumParameters() const throw() {
649  return d_params.size();
650 }
651 
652 inline Type Datatype::getParameter( unsigned int i ) const {
653  CheckArgument(isParametric(), this, "cannot get type parameter of a non-parametric datatype");
654  CheckArgument(i < d_params.size(), i, "type parameter index out of range for datatype");
655  return d_params[i];
656 }
657 
658 inline std::vector<Type> Datatype::getParameters() const {
659  CheckArgument(isParametric(), this, "cannot get type parameters of a non-parametric datatype");
660  return d_params;
661 }
662 
663 inline bool Datatype::operator!=(const Datatype& other) const throw() {
664  return !(*this == other);
665 }
666 
667 inline bool Datatype::isResolved() const throw() {
668  return d_resolved;
669 }
670 
672  return d_constructors.begin();
673 }
674 
676  return d_constructors.end();
677 }
678 
680  return d_constructors.begin();
681 }
682 
683 inline Datatype::const_iterator Datatype::end() const throw() {
684  return d_constructors.end();
685 }
686 
687 inline bool DatatypeConstructor::isResolved() const throw() {
688  return !d_tester.isNull();
689 }
690 
691 inline size_t DatatypeConstructor::getNumArgs() const throw() {
692  return d_args.size();
693 }
694 
695 inline bool DatatypeConstructorArg::isResolved() const throw() {
696  // We could just write:
697  //
698  // return !d_selector.isNull() && d_selector.getType().isSelector();
699  //
700  // HOWEVER, this causes problems in ExprManager tear-down, because
701  // the attributes are removed before the pool is purged. When the
702  // pool is purged, this triggers an equality test between Datatypes,
703  // and this triggers a call to isResolved(), which breaks because
704  // d_selector has no type after attributes are stripped.
705  //
706  // This problem, coupled with the fact that this function is called
707  // _often_, means we should just use a boolean flag.
708  //
709  return d_resolved;
710 }
711 
713  return d_args.begin();
714 }
715 
717  return d_args.end();
718 }
719 
721  return d_args.begin();
722 }
723 
725  return d_args.end();
726 }
727 
728 }/* CVC4 namespace */
729 
730 #endif /* __CVC4__DATATYPE_H */
size_t operator()(const Datatype &dt) const
Definition: datatype.h:584
Class encapsulating the Selector type.
Definition: type.h:662
size_t getNumArgs() const
Get the number of arguments (so far) of this Datatype constructor.
Definition: datatype.h:691
size_t operator()(const DatatypeConstructor *dtc) const
Definition: datatype.h:593
Class encapsulating CVC4 expressions and methods for constructing new expressions.
Definition: expr.h:226
bool isResolved() const
Return true iff this Datatype has already been resolved.
Definition: datatype.h:667
size_t operator()(const DatatypeConstructor &dtc) const
Definition: datatype.h:590
size_t operator()(const Datatype *dt) const
Definition: datatype.h:587
void * ExprManager
The representation of an inductive datatype.
Definition: datatype.h:382
A Datatype constructor argument (i.e., a Datatype field).
Definition: datatype.h:78
bool isNull() const
Check if this is a null expression.
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:57
Class encapsulating CVC4 expression types.
Definition: type.h:88
[[ Add one-line brief description here ]]
void CheckArgument(bool cond, const T &arg, const char *fmt,...)
Definition: exception.h:140
size_t getNumConstructors() const
Get the number of constructors (so far) for this Datatype.
Definition: datatype.h:640
std::ostream & operator<<(std::ostream &out, const Result &r)
std::string getName() const
Definition: datatype.h:614
CVC4's exception base class and some associated utilities.
DatatypeResolutionException(std::string msg)
Definition: datatype.h:606
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
Definition: README:39
std::vector< DatatypeConstructor >::iterator end()
Get the ending iterator over DatatypeConstructors.
Definition: datatype.h:675
std::vector< DatatypeConstructor >::iterator iterator
The type for iterators over constructors.
Definition: datatype.h:397
Datatype(std::string name)
Create a new Datatype of the given name.
Definition: datatype.h:618
DatatypeUnresolvedType(std::string name)
Definition: datatype.h:610
std::vector< DatatypeConstructor >::iterator begin()
Get the beginning iterator over DatatypeConstructors.
Definition: datatype.h:671
bool operator!=(const Datatype &other) const
Return true iff the two Datatypes are not the same.
Definition: datatype.h:663
std::vector< Type > getParameters() const
Get parameters.
Definition: datatype.h:658
size_t getNumParameters() const
Get the nubmer of type parameters.
Definition: datatype.h:648
bool isParametric() const
Is this datatype parametric?
Definition: datatype.h:644
#define CVC4_PUBLIC
Definition: cvc4_public.h:30
Type getParameter(unsigned int i) const
Get parameter.
Definition: datatype.h:652
Class encapsulating the datatype type.
Definition: type.h:594
Representation for an unknown cardinality.
Definition: cardinality.h:54
std::vector< DatatypeConstructor >::const_iterator const_iterator
The (const) type for iterators over constructors.
Definition: datatype.h:399
iterator begin()
Get the beginning iterator over DatatypeConstructor args.
Definition: datatype.h:712
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.
Definition: datatype.h:687
std::vector< DatatypeConstructorArg >::const_iterator const_iterator
The (const) type for iterators over constructor arguments.
Definition: datatype.h:139
bool isResolved() const
Returns true iff this constructor argument has been resolved.
Definition: datatype.h:695
iterator end()
Get the ending iterator over DatatypeConstructor args.
Definition: datatype.h:716
An exception that is thrown when a datatype resolution fails.
Definition: datatype.h:46
expr.h
A constructor for a Datatype.
Definition: datatype.h:133
A hash function for Datatypes.
Definition: datatype.h:583
std::vector< DatatypeConstructorArg >::iterator iterator
The type for iterators over constructor arguments.
Definition: datatype.h:137
std::string getName() const
Get the name of this Datatype.
Definition: datatype.h:636
An unresolved type (used in calls to DatatypeConstructor::addArg()) to allow a Datatype to refer to i...
Definition: datatype.h:68
std::string getName() const
Get the name of this Datatype constructor.
Interface for expression types.