type.h

Go to the documentation of this file.

/*****************************************************************************/
/*!
 * \file type.h
 * 
 * Author: Clark Barrett
 * 
 * Created: Thu Dec 12 12:53:28 2002
 *
 * <hr>
 * Copyright (C) 2003 by the Board of Trustees of Leland Stanford
 * Junior University and by New York University. 
 *
 * License to use, copy, modify, sell and/or distribute this software
 * and its documentation for any purpose is hereby granted without
 * royalty, subject to the terms and conditions defined in the \ref
 * LICENSE file provided with this distribution.  In particular:
 *
 * - The above copyright notice and this permission notice must appear
 * in all copies of the software and related documentation.
 *
 * - THE SOFTWARE IS PROVIDED "AS-IS", WITHOUT ANY WARRANTIES,
 * EXPRESSED OR IMPLIED.  USE IT AT YOUR OWN RISK.
 * 
 * <hr>
 * 
 */
/*****************************************************************************/

// expr.h Has to be included outside of #ifndef, since it sources us
// recursively (read comments in expr_value.h).
#ifndef _CVC_lite__expr_h_
#include "expr.h"
#endif

#ifndef _cvcl__include__type_h_
#define _cvcl__include__type_h_

namespace CVCL {

///////////////////////////////////////////////////////////////////////////////
//                                                                           //
// Class: Type                                                               //
// Author: Clark Barrett                                                     //
// Created: Thu Dec 12 12:53:34 2002                                         //
// Description: Wrapper around expr for api                                  //
//                                                                           //
///////////////////////////////////////////////////////////////////////////////
class Type {
  Expr d_expr;

public:
  Type() {}
  Type(Expr expr);
  //! Special constructor that doesn't check if expr is a type
  //TODO: make this private
  Type(Expr expr, bool dummy) :d_expr(expr) {}
  const Expr& getExpr() const { return d_expr; }

  // Reasoning about children
  int arity() const { return d_expr.arity(); }
  Type operator[](int i) const { return Type(d_expr[i]); }

  // Core testers
  bool isNull() const { return d_expr.isNull(); }
  bool isBool() const { return d_expr.getKind() == BOOLEAN; }
  bool isSubtype() const { return d_expr.getKind() == SUBTYPE; }
  bool isFunction() const { return d_expr.getKind() == ARROW; }

  // Core constructors
  static Type typeBool(ExprManager* em) { return Type(em->boolExpr(), true); }
  static Type funType(const std::vector<Type>& typeDom, const Type& typeRan);
  Type funType(const Type& typeRan) const
  { return Type(Expr(ARROW, d_expr, typeRan.d_expr)); }

  // Printing
  std::string toString() const { return getExpr().toString(); }
};

inline bool operator==(const Type& t1, const Type& t2)
{ return t1.getExpr() == t2.getExpr(); }

inline bool operator!=(const Type& t1, const Type& t2)
{ return t1.getExpr() != t2.getExpr(); }

// Printing
inline std::ostream& operator<<(std::ostream& os, const Type& t) {
  return os << t.getExpr();
}

}

#endif

---