Some cleanup. Also added the integer and real types.

6 files changed, 288 insertions, 129 deletions

diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index cbfcdd110..39c1c91b9 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -311,10 +311,6 @@ public:
   template <class NodeClass, class T>
   NodeClass mkConstInternal(const T&);
 
-  /** Create a type-variable */
-  TypeNode mkTypeVar();
-  TypeNode mkTypeVar(const std::string& name);
-
   /** Create a node with no children. */
   TypeNode mkTypeNode(Kind kind, const std::vector<TypeNode>& children);
 
@@ -446,9 +442,15 @@ public:
                            const AttrKind& attr,
                            const typename AttrKind::value_type& value);
 
-  /** Get the (singleton) type for booleans. */
+  /** Get the (singleton) type for Booleans. */
   inline TypeNode booleanType();
 
+  /** Get the (singleton) type for integers. */
+  inline TypeNode integerType();
+
+  /** Get the (singleton) type for booleans. */
+  inline TypeNode realType();
+
   /** Get the (singleton) type for sorts. */
   inline TypeNode kindType();
 
@@ -607,6 +609,16 @@ inline TypeNode NodeManager::booleanType() {
   return TypeNode(mkTypeConst<TypeConstant>(BOOLEAN_TYPE));
 }
 
+/** Get the (singleton) type for integers. */
+inline TypeNode NodeManager::integerType() {
+  return TypeNode(mkTypeConst<TypeConstant>(INTEGER_TYPE));
+}
+
+/** Get the (singleton) type for reals. */
+inline TypeNode NodeManager::realType() {
+  return TypeNode(mkTypeConst<TypeConstant>(REAL_TYPE));
+}
+
 /** Get the (singleton) type for sorts. */
 inline TypeNode NodeManager::kindType() {
   return TypeNode(mkTypeConst<TypeConstant>(KIND_TYPE));
@@ -648,14 +660,6 @@ NodeManager::mkPredicateType(const std::vector<TypeNode>& sorts) {
   return mkTypeNode(kind::FUNCTION_TYPE, sortNodes);
 }
 
-inline TypeNode NodeManager::mkSort() {
-  return mkTypeVar();
-}
-
-inline TypeNode NodeManager::mkSort(const std::string& name) {
-  return mkTypeVar(name);
-}
-
 inline TypeNode NodeManager::getType(TNode n)  {
   TypeNode typeNode;
   getAttribute(n, TypeAttr(), typeNode);
@@ -749,6 +753,17 @@ inline bool NodeManager::hasOperator(Kind k) {
   }
 }
 
+inline TypeNode NodeManager::mkSort() {
+  TypeNode type = NodeBuilder<0>(this, kind::VARIABLE).constructTypeNode();
+  return type;
+}
+
+inline TypeNode NodeManager::mkSort(const std::string& name) {
+  TypeNode type = mkSort();
+  type.setAttribute(expr::VarNameAttr(), name);
+  return type;
+}
+
 inline Node NodeManager::mkNode(Kind kind) {
   return NodeBuilder<0>(this, kind);
 }
@@ -854,17 +869,6 @@ inline Node NodeManager::mkVar(const TypeNode& type) {
   return n;
 }
 
-inline TypeNode NodeManager::mkTypeVar(const std::string& name) {
-  TypeNode type = mkTypeVar();
-  type.setAttribute(expr::VarNameAttr(), name);
-  return type;
-}
-
-inline TypeNode NodeManager::mkTypeVar() {
-  TypeNode type = NodeBuilder<0>(this, kind::VARIABLE).constructTypeNode();
-  return type;
-}
-
 inline Node* NodeManager::mkVarPtr(const TypeNode& type) {
   Node* n = NodeBuilder<0>(this, kind::VARIABLE).constructNodePtr();
   n->setAttribute(TypeAttr(), type);
diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index 98a7e88e7..c76349fe3 100644
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -84,13 +84,8 @@ bool Type::operator!=(const Type& t) const {
 
 void Type::toStream(std::ostream& out) const {
   NodeManagerScope nms(d_nodeManager);
-  // Do the cast by hand
-  if (isBoolean()) { out << (BooleanType)*this; return; }
-  if (isFunction()) { out << (FunctionType)*this; return; }
-  if (isKind()) { out << (KindType)*this; return; }
-  if (isSort()) { out << (SortType)*this; return; }
-  // We should not get here
-  Unreachable("Type not implemented completely");
+  out << *d_typeNode;
+  return;
 }
 
 /** Is this the Boolean type? */
@@ -100,12 +95,38 @@ bool Type::isBoolean() const {
 }
 
 /** Cast to a Boolean type */
-Type::operator BooleanType() const {
+Type::operator BooleanType() const throw (AssertionException) {
   NodeManagerScope nms(d_nodeManager);
   Assert(isBoolean());
   return BooleanType(*this);
 }
 
+/** Is this the integer type? */
+bool Type::isInteger() const {
+  NodeManagerScope nms(d_nodeManager);
+  return d_typeNode->isInteger();
+}
+
+/** Cast to a integer type */
+Type::operator IntegerType() const throw (AssertionException) {
+  NodeManagerScope nms(d_nodeManager);
+  Assert(isInteger());
+  return IntegerType(*this);
+}
+
+/** Is this the real type? */
+bool Type::isReal() const {
+  NodeManagerScope nms(d_nodeManager);
+  return d_typeNode->isInteger();
+}
+
+/** Cast to a integer type */
+Type::operator RealType() const throw (AssertionException) {
+  NodeManagerScope nms(d_nodeManager);
+  Assert(isReal());
+  return RealType(*this);
+}
+
 /** Is this a function type? */
 bool Type::isFunction() const {
   NodeManagerScope nms(d_nodeManager);
@@ -120,7 +141,7 @@ bool Type::isPredicate() const {
 }
 
 /** Cast to a function type */
-Type::operator FunctionType() const {
+Type::operator FunctionType() const throw (AssertionException) {
   NodeManagerScope nms(d_nodeManager);
   Assert(isFunction());
   return FunctionType(*this);
@@ -133,7 +154,7 @@ bool Type::isSort() const {
 }
 
 /** Cast to a sort type */
-Type::operator SortType() const {
+Type::operator SortType() const throw (AssertionException) {
   NodeManagerScope nms(d_nodeManager);
   Assert(isSort());
   return SortType(*this);
@@ -146,7 +167,7 @@ bool Type::isKind() const {
 }
 
 /** Cast to a kind type */
-Type::operator KindType() const {
+Type::operator KindType() const throw (AssertionException) {
   NodeManagerScope nms(d_nodeManager);
   Assert(isKind());
   return KindType(*this);
@@ -170,45 +191,46 @@ Type FunctionType::getRangeType() const {
   return makeType(d_typeNode->getRangeType());
 }
 
-void BooleanType::toStream(std::ostream& out) const {
-  out << "BOOLEAN";
-}
-
 std::string SortType::getName() const {
   NodeManagerScope nms(d_nodeManager);
   return d_typeNode->getAttribute(expr::VarNameAttr());
 }
 
-void SortType::toStream(std::ostream& out) const {
-  NodeManagerScope nms(d_nodeManager);
-  out << getName();
+BooleanType::BooleanType(const Type& t) throw (AssertionException)
+: Type(t)
+{
+  Assert(isBoolean());
 }
 
-void FunctionType::toStream(std::ostream& out) const {
-  NodeManagerScope nms(d_nodeManager);
-  unsigned arity = d_typeNode->getNumChildren();
+IntegerType::IntegerType(const Type& t) throw (AssertionException)
+: Type(t)
+{
+  Assert(isInteger());
+}
 
-  if(arity > 2) {
-    out << "(";
-  }
-  unsigned int i;
-  for(i=0; i < arity - 1; ++i) {
-    if(i > 0) {
-      out << ",";
-    }
-    out << makeType((*d_typeNode)[i]);
-  }
-  if(arity > 2) {
-    out << ")";
-  }
-  out << " -> ";
-  (*d_typeNode)[i].toStream(out);
+RealType::RealType(const Type& t) throw (AssertionException)
+: Type(t)
+{
+  Assert(isReal());
 }
 
-BooleanType::BooleanType(const Type& t) : Type(t) {}
-FunctionType::FunctionType(const Type& t) : Type(t) {}
-KindType::KindType(const Type& t) : Type(t) {}
-SortType::SortType(const Type& t) : Type(t) {}
+FunctionType::FunctionType(const Type& t) throw (AssertionException)
+: Type(t)
+{
+  Assert(isFunction());
+}
+
+KindType::KindType(const Type& t) throw (AssertionException)
+: Type(t)
+{
+  Assert(isKind());
+}
+
+SortType::SortType(const Type& t) throw (AssertionException)
+: Type(t)
+{
+  Assert(isSort());
+}
 
 
 }/* CVC4 namespace */
diff --git a/src/expr/type.h b/src/expr/type.h
index 5cbe0613a..c61b67f77 100644
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -1,7 +1,7 @@
 /*********************                                                        */
 /** type.h
  ** Original author: cconway
- ** Major contributors: mdeters
+ ** Major contributors: mdeters, dejan
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
@@ -32,6 +32,8 @@ class NodeManager;
 class TypeNode;
 
 class BooleanType;
+class IntegerType;
+class RealType;
 class FunctionType;
 class KindType;
 class SortType;
@@ -52,14 +54,16 @@ protected:
   NodeManager* d_nodeManager;
 
   /**
-   * Construct a new type given the typeNode;
+   * Construct a new type given the typeNode, for internal use only.
+   * @param typeNode the TypeNode to use
+   * @return the Type corresponding to the TypeNode
    */
   Type makeType(const TypeNode& typeNode) const;
 
   /**
    * Constructor for internal purposes.
    * @param em the expression manager that handles this expression
-   * @param node the actual expression node pointer for this type
+   * @param typeNode the actual TypeNode pointer for this type
    */
   Type(NodeManager* em, TypeNode* typeNode);
 
@@ -79,72 +83,160 @@ public:
   /** Default constructor */
   Type();
 
-  /** Copy constructor */
+  /**
+   * Copy constructor.
+   * @param t the type to make a copy of
+   */
   Type(const Type& t);
 
-  /** Check whether this is a null type */
+  /**
+   * Check whether this is a null type
+   * @return true if type is null
+   */
   bool isNull() const;
 
-  /** Assignment operator */
+  /**
+   * Assignment operator.
+   * @param t the type to assign to this type
+   * @return this type after assignment.
+   */
   Type& operator=(const Type& t);
 
-  /** Comparison for equality */
+  /**
+   * Comparison for structural equality.
+   * @param t the type to compare to
+   * @returns true if the types are equal
+   */
   bool operator==(const Type& t) const;
 
-  /** Comparison for disequality */
+  /**
+   * Comparison for structural disequality.
+   * @param t the type to compare to
+   * @returns true if the types are not equal
+   */
   bool operator!=(const Type& t) const;
 
-  /** Is this the Boolean type? */
+  /**
+   * Is this the Boolean type?
+   * @return true if the type is a Boolean type
+   */
   bool isBoolean() const;
 
-  /** Cast to a Boolean type */
-  operator BooleanType() const;
+  /**
+   * Cast this type to a Boolean type
+   * @return the BooleanType
+   */
+  operator BooleanType() const throw (AssertionException);
+
+  /**
+   * Is this the integer type?
+   * @return true if the type is a integer type
+   */
+  bool isInteger() const;
+
+  /**
+   * Cast this type to a integer type
+   * @return the IntegerType
+   */
+  operator IntegerType() const throw (AssertionException);
+
+  /**
+   * Is this the real type?
+   * @return true if the type is a real type
+   */
+  bool isReal() const;
 
-  /** Is this a function type? */
+  /**
+   * Cast this type to a real type
+   * @return the RealType
+   */
+  operator RealType() const throw (AssertionException);
+
+  /**
+   * Is this a function type?
+   * @return true if the type is a Boolean type
+   */
   bool isFunction() const;
 
-  /** Is this a predicate type? NOTE: all predicate types are also
-      function types. */
+  /**
+   * Is this a predicate type, i.e. if it's a function type mapping to Boolean.
+   * Aall predicate types are also function types.
+   * @return true if the type is a predicate type
+   */
   bool isPredicate() const;
 
-  /** Cast to a function type */
-  operator FunctionType() const;
+  /**
+   * Cast this type to a function type
+   * @return the FunctionType
+   */
+  operator FunctionType() const throw (AssertionException);
 
-  /** Is this a sort kind */
+  /**
+   * Is this a sort kind?
+   * @return true if this is a sort kind
+   */
   bool isSort() const;
 
-  /** Cast to a sort type */
-  operator SortType() const;
+  /**
+   * Cast this type to a sort type
+   * @return the function Type
+   */
+  operator SortType() const throw (AssertionException);
 
-  /** Is this a kind type (i.e., the type of a type)? */
+  /**
+   * Is this a kind type (i.e., the type of a type)?
+   * @return true if this is a kind type
+   */
   bool isKind() const;
 
-  /** Cast to a kind type */
-  operator KindType() const;
-
-  /** Outputs a string representation of this type to the stream. */
-  virtual void toStream(std::ostream& out) const;
+  /**
+   * Cast to a kind type
+   * @return the kind type
+   */
+  operator KindType() const throw (AssertionException);
 
+  /**
+   * Outputs a string representation of this type to the stream.
+   * @param out the stream to output to
+   */
+  void toStream(std::ostream& out) const;
 };
 
 /**
- * Singleton class encapsulating the boolean type.
+ * Singleton class encapsulating the Boolean type.
  */
 class CVC4_PUBLIC BooleanType : public Type {
 
 public:
 
   /** Construct from the base type */
-  BooleanType(const Type& type);
+  BooleanType(const Type& type) throw (AssertionException);
+};
 
-  /** Is this the boolean type? (Returns true.) */
-  bool isBoolean() const;
+/**
+ * Singleton class encapsulating the integer type.
+ */
+class CVC4_PUBLIC IntegerType : public Type {
 
-  /** Just outputs BOOLEAN */
-  void toStream(std::ostream& out) const;
+public:
+
+  /** Construct from the base type */
+  IntegerType(const Type& type) throw (AssertionException);
 };
 
 /**
+ * Singleton class encapsulating the real type.
+ */
+class CVC4_PUBLIC RealType : public Type {
+
+public:
+
+  /** Construct from the base type */
+  RealType(const Type& type) throw (AssertionException);
+};
+
+
+/**
  * Class encapsulating a function type.
  */
 class CVC4_PUBLIC FunctionType : public Type {
@@ -152,20 +244,13 @@ class CVC4_PUBLIC FunctionType : public Type {
 public:
 
   /** Construct from the base type */
-  FunctionType(const Type& type);
+  FunctionType(const Type& type) throw (AssertionException);
 
   /** Get the argument types */
   std::vector<Type> getArgTypes() const;
 
   /** Get the range type (i.e., the type of the result). */
   Type getRangeType() const;
-
-  /**
-   * Outputs a string representation of this type to the stream,
-   * in the format "D -> R" or "(A, B, C) -> R".
-   */
-  void toStream(std::ostream& out) const;
-
 };
 
 /**
@@ -176,13 +261,10 @@ class CVC4_PUBLIC SortType : public Type {
 public:
 
   /** Construct from the base type */
-  SortType(const Type& type);
+  SortType(const Type& type) throw (AssertionException);
 
   /** Get the name of the sort */
   std::string getName() const;
-
-  /** Outouts the name of the sort */
-  void toStream(std::ostream& out) const;
 };
 
 /**
@@ -193,11 +275,7 @@ class CVC4_PUBLIC KindType : public Type {
 public:
 
   /** Construct from the base type */
-  KindType(const Type& type);
-
-  /** Is this the kind type? (Returns true.) */
-  bool isKind() const;
-
+  KindType(const Type& type) throw (AssertionException);
 };
 
 /**
diff --git a/src/expr/type_constant.h b/src/expr/type_constant.h
index 86698459b..a847bc827 100644
--- a/src/expr/type_constant.h
+++ b/src/expr/type_constant.h
@@ -1,26 +1,67 @@
-/*
- * type_constant.h
- *
- *  Created on: Apr 5, 2010
- *      Author: dejan
- */
+/*********************                                                        */
+/** type_constant.h
+ ** Original author: dejan
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.
+ **
+ ** Interface for expression types
+ **/
 
 #ifndef __CVC4__TYPE_CONSTANT_H_
 #define __CVC4__TYPE_CONSTANT_H_
 
 namespace CVC4 {
 
+/**
+ * The enumeration for the built-in atomic types.
+ */
 enum TypeConstant {
+  /** The Boolean type */
   BOOLEAN_TYPE,
+  /** The integer type */
+  INTEGER_TYPE,
+  /** The real type */
+  REAL_TYPE,
+  /** The kind type (type of types) */
   KIND_TYPE
 };
 
+/**
+ * We hash the constants with their values.
+ */
 struct TypeConstantHashStrategy {
   static inline size_t hash(TypeConstant tc) {
     return tc;
   }
 };/* struct BoolHashStrategy */
 
+inline std::ostream& operator<<(std::ostream& out, TypeConstant typeConstant) {
+
+  switch(typeConstant) {
+  case BOOLEAN_TYPE:
+    out << "BOOLEAN";
+    break;
+  case INTEGER_TYPE:
+    out << "INTEGER";
+    break;
+  case REAL_TYPE:
+    out << "REAL";
+    break;
+  case KIND_TYPE:
+    out << "KIND";
+    break;
+  default:
+    out << "UNKNOWN_TYPE_CONSTANT";
+    break;
+  }
+  return out;
+}
+
 }
 
 #endif /* __CVC4__TYPE_CONSTANT_H_ */
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index 87b6ed58a..08e50844b 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -23,6 +23,14 @@ bool TypeNode::isBoolean() const {
   return getKind() == kind::TYPE_CONSTANT && getConst<TypeConstant>() == BOOLEAN_TYPE;
 }
 
+bool TypeNode::isInteger() const {
+  return getKind() == kind::TYPE_CONSTANT && getConst<TypeConstant>() == INTEGER_TYPE;
+}
+
+bool TypeNode::isReal() const {
+  return getKind() == kind::TYPE_CONSTANT && getConst<TypeConstant>() == REAL_TYPE;
+}
+
 /** Is this a function type? */
 bool TypeNode::isFunction() const {
   return getKind() == kind::FUNCTION_TYPE;
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index 7747b93e1..12df5513f 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -38,14 +38,14 @@ class NodeValue;
 }/* CVC4::expr namespace */
 
 /**
- * Encapsulation of an NodeValue pointer.  The reference count is
- * maintained in the NodeValue if ref_count is true.
+ * Encapsulation of an NodeValue pointer for Types. The reference count is
+ * maintained in the NodeValue.
  */
 class TypeNode {
 
   /**
    * The NodeValue has access to the private constructors, so that the
-   * iterators can can create new nodes.
+   * iterators can can create new types.
    */
   friend class expr::NodeValue;
 
@@ -105,14 +105,6 @@ public:
   }
 
   /**
-   * Returns true if this type is a null type.
-   * @return true if null
-   */
-  bool isNull() const {
-    return d_nv == &expr::NodeValue::s_null;
-  }
-
-  /**
    * Structural comparison operator for expressions.
    * @param typeNode the type node to compare to
    * @return true if expressions are equal, false otherwise
@@ -292,9 +284,23 @@ public:
    */
   void printAst(std::ostream & o, int indent = 0) const;
 
+  /**
+   * Returns true if this type is a null type.
+   * @return true if null
+   */
+  bool isNull() const {
+    return d_nv == &expr::NodeValue::s_null;
+  }
+
   /** Is this the Boolean type? */
   bool isBoolean() const;
 
+  /** Is this the Integer type? */
+  bool isInteger() const;
+
+  /** Is this the Real type? */
+  bool isReal() const;
+
   /** Is this a function type? */
   bool isFunction() const;