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 
00064   // Core constructors
00065   static Type typeBool(ExprManager* em) { return Type(em->boolExpr(), true); }
00066   static Type anyType(ExprManager* em) { return Type(em->newLeafExpr(ANY_TYPE)); }
00067   static Type funType(const std::vector<Type>& typeDom, const Type& typeRan);
00068   Type funType(const Type& typeRan) const
00069   { return Type(Expr(ARROW, d_expr, typeRan.d_expr)); }
00070 
00071   // Printing
00072   std::string toString() const { return getExpr().toString(); }
00073 };
00074 
00075 inline bool operator==(const Type& t1, const Type& t2)
00076 { return t1.getExpr() == t2.getExpr(); }
00077 
00078 inline bool operator!=(const Type& t1, const Type& t2)
00079 { return t1.getExpr() != t2.getExpr(); }
00080 
00081 // Printing
00082 inline std::ostream& operator<<(std::ostream& os, const Type& t) {
00083   return os << t.getExpr();
00084 }
00085 
00086 }
00087 
00088 #endif

Generated on Tue Jul 3 14:33:42 2007 for CVC3 by  doxygen 1.5.1