Documenting type.h/cpp

Making Boolean and Kind types singletons

4 files changed, 181 insertions, 53 deletions

diff --git a/src/expr/expr_manager.cpp b/src/expr/expr_manager.cpp
index ee61c14c9..8bd9b21f6 100644
--- a/src/expr/expr_manager.cpp
+++ b/src/expr/expr_manager.cpp
@@ -31,9 +31,7 @@ using namespace std;
 namespace CVC4 {
 
 ExprManager::ExprManager()
-  : d_nm(new NodeManager()), 
-    d_booleanType(new BooleanType(this)),
-    d_kindType(new KindType(this)) {
+  : d_nm(new NodeManager()) {
 }
 
 ExprManager::~ExprManager() {
@@ -41,11 +39,11 @@ ExprManager::~ExprManager() {
 }
 
 const BooleanType* ExprManager::booleanType() {
-  return d_booleanType;
+  return BooleanType::getInstance();
 }
 
 const KindType* ExprManager::kindType() {
-  return d_kindType;
+  return KindType::getInstance();
 }
 
 Expr ExprManager::mkExpr(Kind kind) {
@@ -97,14 +95,14 @@ Expr ExprManager::mkExpr(Kind kind, const vector<Expr>& children) {
 const FunctionType* 
 ExprManager::mkFunctionType(const Type* domain, 
                             const Type* range) {
-  return new FunctionType(this,domain,range);
+  return FunctionType::getInstance(this,domain,range);
 }
 
 /** Make a function type with input types from argTypes. */
 const FunctionType* 
 ExprManager::mkFunctionType(const std::vector<const Type*>& argTypes, 
                             const Type* range) {
-  return new FunctionType(this,argTypes,range);
+  return FunctionType::getInstance(this,argTypes,range);
 }
 
 const Type* ExprManager::mkSort(std::string name) {
diff --git a/src/expr/expr_manager.h b/src/expr/expr_manager.h
index 41766d64b..1ca707fae 100644
--- a/src/expr/expr_manager.h
+++ b/src/expr/expr_manager.h
@@ -108,8 +108,6 @@ public:
 private:
   /** The internal node manager */
   NodeManager* d_nm;
-  BooleanType* d_booleanType;
-  KindType* d_kindType;
   
   /**
    * Returns the internal node manager. This should only be used by internal
diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index 5052a3b79..d4662d420 100644
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -33,13 +33,12 @@ Type::Type(ExprManager* exprManager, std::string name) :
   d_exprManager(exprManager), d_name(name) { 
 }
 
-// Type Type::operator=(const Type& t) {
-//   if( this != &t ) {
-//     d_name == t.d_name;
-// }
+Type::Type(std::string name) : 
+  d_name(name) { 
+}
 
 bool Type::operator==(const Type& t) const {
-  return d_name == t.d_name;
+  return d_exprManager == t.d_exprManager && d_name == t.d_name;
 }
 
 bool Type::operator!=(const Type& t) const {
@@ -54,39 +53,53 @@ std::string Type::getName() const {
   return d_name;
 }
 
-// void Type::toStream(std::ostream& out) const {
-//   out << getName();
-// }
+BooleanType BooleanType::s_instance;
 
-BooleanType::BooleanType(ExprManager* exprManager) 
-  : Type(exprManager,std::string("BOOLEAN")) {
+BooleanType::BooleanType() : Type(std::string("BOOLEAN")) {
 }
 
 BooleanType::~BooleanType() {
 }
 
+BooleanType*
+BooleanType::getInstance() {
+  return &s_instance;
+}
+
 bool BooleanType::isBoolean() const {
   return true;
 }
 
 FunctionType::FunctionType(ExprManager* exprManager, 
-                           const Type* domain, 
+                           const std::vector<const Type*>& argTypes, 
                            const Type* range) 
-  : Type(exprManager), d_argTypes(), d_rangeType(range) {
-  d_argTypes.push_back(domain);
+  : Type(exprManager), d_argTypes(argTypes), d_rangeType(range) {
+  Assert( argTypes.size() > 0 );
 }
 
   // FIXME: What becomes of argument types?
 FunctionType::~FunctionType() {
 }
 
-FunctionType::FunctionType(ExprManager* exprManager, 
-                           const std::vector<const Type*>& argTypes, 
-                           const Type* range) 
-  : Type(exprManager), d_argTypes(argTypes), d_rangeType(range) {
+FunctionType* 
+FunctionType::getInstance(ExprManager* exprManager, 
+                          const Type* domain, 
+                          const Type* range) {
+  std::vector<const Type*> argTypes;
+  argTypes.push_back(domain);
+  return getInstance(exprManager,argTypes,range);
+}
+
+  //FIXME: should be singleton
+FunctionType* 
+FunctionType::getInstance(ExprManager* exprManager, 
+            const std::vector<const Type*>& argTypes, 
+            const Type* range) {
   Assert( argTypes.size() > 0 );
+  return new FunctionType(exprManager,argTypes,range);
 }
 
+
 const std::vector<const Type*> FunctionType::getArgTypes() const {
   return d_argTypes;
 }
@@ -120,8 +133,9 @@ void FunctionType::toStream(std::ostream& out) const {
   d_rangeType->toStream(out);
 }
 
-KindType::KindType(ExprManager* exprManager) 
-  : Type(exprManager,std::string("KIND")) {
+KindType KindType::s_instance;
+
+KindType::KindType() : Type(std::string("KIND")) {
 }
 
 KindType::~KindType() {
@@ -131,6 +145,11 @@ bool KindType::isKind() const {
   return true;
 }
 
+KindType*
+KindType::getInstance() {
+  return &s_instance;
+}
+
 SortType::SortType(ExprManager* exprManager,std::string name) 
   : Type(exprManager,name) {
 }
diff --git a/src/expr/type.h b/src/expr/type.h
index 87c3d8f5c..e5fda779e 100644
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -27,86 +27,199 @@ class ExprManager;
 
 /**
  * Class encapsulating CVC4 expression types.
- * NOTE: This is very much a stub interface!!! I'm putting this here
- * so the parser can do some very simple type differentiation, but
- * this is obviously hopelessly inadequate. -Chris
  */
 class Type {
  public:
-  Type() { };
-  Type(ExprManager* const exprManager);
-  Type(ExprManager* const exprManager, std::string name);
-  virtual ~Type() { };
-
+  /** Comparision for equality */
   bool operator==(const Type& t) const;
+
+  /** Comparison for disequality */
   bool operator!=(const Type& e) const;
 
+  /** Get the ExprManager associated with this type. May be NULL for
+      singleton types. */
   ExprManager* getExprManager() const;
 
+  /** Get the name of this type. May be empty for composite types. */
   std::string getName() const;
 
+  /** Is this the boolean type? */
   virtual bool isBoolean() const {
     return false;
   }
 
+  /** Is this a function type? */
   virtual bool isFunction() const { 
     return false;
   }
 
+  /** Is this a predicate type? NOTE: all predicate types are also
+      function types. */
   virtual bool isPredicate() const {
     return false;
   }
 
+  /** Is this a kind type (i.e., the type of a type)? */
   virtual bool isKind() const {
     return false;
   }
 
+  /** Outputs a string representation of this type to the stream. */
   virtual void toStream(std::ostream& out) const {
     out << getName();
   }
 
 protected:
+  /** Create a type associated with exprManager. */
+  Type(ExprManager* const exprManager);
+
+  /** Create a type associated with exprManager with the given name. */
+  Type(ExprManager* const exprManager, std::string name);
+
+  /** Create a type with the given name. */
+  Type(std::string name);
+
+  /** Destructor */
+  virtual ~Type() { };
+
+  /** The associated ExprManager */
   ExprManager* d_exprManager;
+
+  /** The name of the type (may be empty). */
   std::string d_name;
 };
 
+/**
+ * Singleton class encapsulating the boolean type.
+ */
 class BooleanType : public Type {
- public:
-  BooleanType(ExprManager* exprManager);
-  ~BooleanType();
+
+public:
+  static BooleanType* getInstance();
+
+  /** Is this the boolean type? (Returns true.) */
   bool isBoolean() const;
+
+private:
+  /** Create a type associated with exprManager. */
+  BooleanType();
+
+  /** Do-nothing private copy constructor operator, to prevent
+      copy-construction. */
+  BooleanType(const BooleanType&); 
+
+  /** Destructor */
+  ~BooleanType();
+
+  /** Do-nothing private assignment operator, to prevent
+     assignment. */
+  BooleanType& operator=(const BooleanType&);
+  
+  /** The singleton instance */
+  static BooleanType s_instance;
 };
 
+/**
+ * Class encapsulating a function type.
+ * TODO: Override == to check component types?
+ */
 class FunctionType : public Type {
- public:
-  FunctionType(ExprManager* exprManager, 
-               const Type* domain, 
-               const Type* range);
-  FunctionType(ExprManager* exprManager, 
-               const std::vector<const Type*>& argTypes, 
-               const Type* range);
-  ~FunctionType();
+
+public:
+  static FunctionType* getInstance(ExprManager* exprManager, 
+                                   const Type* domain, 
+                                   const Type* range);
+
+  static FunctionType* getInstance(ExprManager* exprManager, 
+                                   const std::vector<const Type*>& argTypes, 
+                                   const Type* range);
+
+
+  /** Retrieve the argument types. The vector will be non-empty. */
   const std::vector<const Type*> getArgTypes() const;
+
+  /** Get the range type (i.e., the type of the result). */
   const Type* getRangeType() const;
+  
+  /** Is this as function type? (Returns true.) */
   bool isFunction() const;
+
+  /** Is this as predicate type? (Returns true if range is
+      boolean.) */
   bool isPredicate() 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;
 
- private:
-  std::vector<const Type*> d_argTypes;
+private:
+
+  /** Construct a function type associated with exprManager,
+      given a vector of argument types and the range type. 
+      
+      @param argTypes a non-empty vector of input types
+      @param range the result type
+  */
+  FunctionType(ExprManager* exprManager, 
+               const std::vector<const Type*>& argTypes, 
+               const Type* range);
+
+  /** Destructor */
+  ~FunctionType();
+  
+  /** The list of input types. */
+  const std::vector<const Type*> d_argTypes;
+
+  /** The result type. */
   const Type* d_rangeType;
+
 };
 
+
+/** Class encapsulating the kind type (the type of types). 
+    TODO: Should be a singleton per-ExprManager.
+*/
 class KindType : public Type {
- public:
-  KindType(ExprManager* exprManager);
-  ~KindType();
+
+public:
+
+  /** Create a type associated with exprManager. */
+  static KindType* getInstance();
+
+  /** Is this the kind type? (Returns true.) */
   bool isKind() const;
+
+private:
+
+  /** Create a type associated with exprManager. */
+  KindType();
+
+  /* Do-nothing private copy constructor, to prevent
+     copy construction. */
+  KindType(const KindType&); 
+
+  /** Destructor */
+  ~KindType();
+
+  /* Do-nothing private assignment operator, to prevent
+     assignment. */
+  KindType& operator=(const KindType&);
+
+  /** The singleton instance */
+  static KindType s_instance;
 };
 
+/** Class encapsulating a user-defined sort. 
+    TODO: Should sort be uniquely named per-exprManager and not conflict
+    with any builtins? */
 class SortType : public Type {
- public:
+
+public:
+
+  /** Create a sort associated with exprManager with the given name. */
   SortType(ExprManager* exprManager, std::string name);
+
+  /** Destructor */
   ~SortType();
 };