CVC3
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