CVC3

type.h

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  * \file type.h
00004  * 
00005  * Author: Clark Barrett
00006  * 
00007  * Created: Thu Dec 12 12:53:28 2002
00008  *
00009  * <hr>
00010  *
00011  * License to use, copy, modify, sell and/or distribute this software
00012  * and its documentation for any purpose is hereby granted without
00013  * royalty, subject to the terms and conditions defined in the \ref
00014  * LICENSE file provided with this distribution.
00015  * 
00016  * <hr>
00017  * 
00018  */
00019 /*****************************************************************************/
00020 
00021 // expr.h Has to be included outside of #ifndef, since it sources us
00022 // recursively (read comments in expr_value.h).
00023 #ifndef _cvc3__expr_h_
00024 #include "expr.h"
00025 #endif
00026 
00027 #ifndef _cvc3__include__type_h_
00028 #define _cvc3__include__type_h_
00029 
00030 namespace CVC3 {
00031 
00032 #include "os.h"
00033 
00034 ///////////////////////////////////////////////////////////////////////////////
00035 //                                                                           //
00036 // Class: Type                     //
00037 // Author: Clark Barrett                                                     //
00038 // Created: Thu Dec 12 12:53:34 2002               //
00039 // Description: Wrapper around expr for api                                  //
00040 //                                                                           //
00041 ///////////////////////////////////////////////////////////////////////////////
00042 class CVC_DLL Type {
00043   Expr d_expr;
00044 
00045 public:
00046   Type() {}
00047   Type(Expr expr);
00048   //! Special constructor that doesn't check if expr is a type
00049   //TODO: make this private
00050   Type(const Type& type) :d_expr(type.d_expr) {}
00051   Type(Expr expr, bool dummy) :d_expr(expr) {}
00052   const Expr& getExpr() const { return d_expr; }
00053 
00054   // Reasoning about children
00055   int arity() const { return d_expr.arity(); }
00056   Type operator[](int i) const { return Type(d_expr[i]); }
00057 
00058   // Core testers
00059   bool isNull() const { return d_expr.isNull(); }
00060   bool isBool() const { return d_expr.getKind() == BOOLEAN; }
00061   bool isSubtype() const { return d_expr.getKind() == SUBTYPE; }
00062   bool isFunction() const { return d_expr.getKind() == ARROW; }
00063   //! Return cardinality of type
00064   Cardinality card() const { return d_expr.typeCard(); }
00065   //! Return nth (starting with 0) element in a finite type
00066   /*! Returns NULL Expr if unable to compute nth element
00067    */
00068   Expr enumerateFinite(Unsigned n) const { return d_expr.typeEnumerateFinite(n); }
00069   //! Return size of a finite type; returns 0 if size cannot be determined
00070   Unsigned sizeFinite() const { return d_expr.typeSizeFinite(); }
00071 
00072   // Core constructors
00073   static Type typeBool(ExprManager* em) { return Type(em->boolExpr(), true); }
00074   static Type anyType(ExprManager* em) { return Type(em->newLeafExpr(ANY_TYPE)); }
00075   static Type funType(const std::vector<Type>& typeDom, const Type& typeRan);
00076   Type funType(const Type& typeRan) const
00077   { return Type(Expr(ARROW, d_expr, typeRan.d_expr)); }
00078 
00079   // Printing
00080   std::string toString() const { return getExpr().toString(); }
00081 };
00082 
00083 inline bool operator==(const Type& t1, const Type& t2)
00084 { return t1.getExpr() == t2.getExpr(); }
00085 
00086 inline bool operator!=(const Type& t1, const Type& t2)
00087 { return t1.getExpr() != t2.getExpr(); }
00088 
00089 // Printing
00090 inline std::ostream& operator<<(std::ostream& os, const Type& t) {
00091   return os << t.getExpr();
00092 }
00093 
00094 }
00095 
00096 #endif