CVC3  2.4.1
type.h
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  * \file type.h
4  *
5  * Author: Clark Barrett
6  *
7  * Created: Thu Dec 12 12:53:28 2002
8  *
9  * <hr>
10  *
11  * License to use, copy, modify, sell and/or distribute this software
12  * and its documentation for any purpose is hereby granted without
13  * royalty, subject to the terms and conditions defined in the \ref
14  * LICENSE file provided with this distribution.
15  *
16  * <hr>
17  *
18  */
19 /*****************************************************************************/
20 
21 // expr.h Has to be included outside of #ifndef, since it sources us
22 // recursively (read comments in expr_value.h).
23 #ifndef _cvc3__expr_h_
24 #include "expr.h"
25 #endif
26 
27 #ifndef _cvc3__include__type_h_
28 #define _cvc3__include__type_h_
29 
30 namespace CVC3 {
31 
32 #include "os.h"
33 
34 ///////////////////////////////////////////////////////////////////////////////
35 // //
36 // Class: Type //
37 // Author: Clark Barrett //
38 // Created: Thu Dec 12 12:53:34 2002 //
39 // Description: Wrapper around expr for api //
40 // //
41 ///////////////////////////////////////////////////////////////////////////////
42 class CVC_DLL Type {
43  Expr d_expr;
44 
45 public:
46  Type() {}
47  Type(Expr expr);
48  //! Special constructor that doesn't check if expr is a type
49  //TODO: make this private
50  Type(const Type& type) :d_expr(type.d_expr) {}
51  Type(Expr expr, bool dummy) :d_expr(expr) {}
52  const Expr& getExpr() const { return d_expr; }
53 
54  // Reasoning about children
55  int arity() const { return d_expr.arity(); }
56  Type operator[](int i) const { return Type(d_expr[i]); }
57 
58  // Core testers
59  bool isNull() const { return d_expr.isNull(); }
60  bool isBool() const { return d_expr.getKind() == BOOLEAN; }
61  bool isSubtype() const { return d_expr.getKind() == SUBTYPE; }
62  bool isFunction() const { return d_expr.getKind() == ARROW; }
63  //! Return cardinality of type
64  Cardinality card() const { return d_expr.typeCard(); }
65  //! Return nth (starting with 0) element in a finite type
66  /*! Returns NULL Expr if unable to compute nth element
67  */
68  Expr enumerateFinite(Unsigned n) const { return d_expr.typeEnumerateFinite(n); }
69  //! Return size of a finite type; returns 0 if size cannot be determined
70  Unsigned sizeFinite() const { return d_expr.typeSizeFinite(); }
71 
72  // Core constructors
73  static Type typeBool(ExprManager* em) { return Type(em->boolExpr(), true); }
74  static Type anyType(ExprManager* em) { return Type(em->newLeafExpr(ANY_TYPE)); }
75  static Type funType(const std::vector<Type>& typeDom, const Type& typeRan);
76  Type funType(const Type& typeRan) const
77  { return Type(Expr(ARROW, d_expr, typeRan.d_expr)); }
78 
79  // Printing
80  std::string toString() const { return getExpr().toString(); }
81 };
82 
83 inline bool operator==(const Type& t1, const Type& t2)
84 { return t1.getExpr() == t2.getExpr(); }
85 
86 inline bool operator!=(const Type& t1, const Type& t2)
87 { return t1.getExpr() != t2.getExpr(); }
88 
89 // Printing
90 inline std::ostream& operator<<(std::ostream& os, const Type& t) {
91  return os << t.getExpr();
92 }
93 
94 }
95 
96 #endif
Definition: kinds.h:48
Data structure of expressions in CVC3.
Definition: expr.h:133
Cardinality card() const
Return cardinality of type.
Definition: type.h:64
ostream & operator<<(ostream &os, const Expr &e)
Definition: expr.cpp:621
const Expr & boolExpr()
BOOLEAN Expr.
Definition: expr_manager.h:276
Type()
Definition: type.h:46
MS C++ specific settings.
Definition: type.h:42
bool isBool() const
Definition: type.h:60
Definition: kinds.h:51
bool operator==(const Expr &e1, const Expr &e2)
Definition: expr.h:1600
Expr d_expr
Definition: type.h:43
const Expr & getExpr() const
Definition: type.h:52
Type(Expr expr, bool dummy)
Definition: type.h:51
int arity() const
Definition: type.h:55
Type(const Type &type)
Special constructor that doesn't check if expr is a type.
Definition: type.h:50
Expr enumerateFinite(Unsigned n) const
Return nth (starting with 0) element in a finite type.
Definition: type.h:68
Expr typeEnumerateFinite(Unsigned n) const
Return nth (starting with 0) element in a finite type.
Definition: expr.h:1277
Abstraction over different operating systems.
Definition: kinds.h:193
Expr newLeafExpr(const Op &op)
Definition: expr_manager.h:454
#define CVC_DLL
bool isNull() const
Definition: type.h:59
std::string toString() const
Definition: type.h:80
Expression Manager.
Definition: expr_manager.h:58
static Type anyType(ExprManager *em)
Definition: type.h:74
bool operator!=(const Expr &e1, const Expr &e2)
Definition: expr.h:1605
Definition of the API to expression package. See class Expr for details.
Unsigned sizeFinite() const
Return size of a finite type; returns 0 if size cannot be determined.
Definition: type.h:70
Cardinality
Enum for cardinality of types.
Definition: expr.h:80
Definition: kinds.h:50
bool isFunction() const
Definition: type.h:62
bool isSubtype() const
Definition: type.h:61
static Type typeBool(ExprManager *em)
Definition: type.h:73
Type operator[](int i) const
Definition: type.h:56
Type funType(const Type &typeRan) const
Definition: type.h:76