Documenting type.h/cpp

Making Boolean and Kind types singletons

7 files changed, 256 insertions, 163 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();
 };
 
diff --git a/src/parser/antlr_parser.cpp b/src/parser/antlr_parser.cpp
index 5a9af8d4a..bd263f72d 100644
--- a/src/parser/antlr_parser.cpp
+++ b/src/parser/antlr_parser.cpp
@@ -51,8 +51,7 @@ AntlrParser::AntlrParser(antlr::TokenStream& lexer, int k) :
 Expr AntlrParser::getSymbol(std::string name, SymbolType type) {
   Assert( isDeclared(name,type) );
   switch( type ) {
-  case SYM_VARIABLE: // Predicates and functions share var namespace
-  // case SYM_PREDICATE:
+  case SYM_VARIABLE: // Functions share var namespace
   case SYM_FUNCTION:
     return d_varSymbolTable.getObject(name);
   default:
@@ -68,10 +67,6 @@ Expr AntlrParser::getFunction(std::string name) {
   return getSymbol(name,SYM_FUNCTION);
 }
 
-// Expr AntlrParser::getPredicate(std::string name) {
-//   return getSymbol(name,SYM_PREDICATE);
-// }
-
 const Type* 
 AntlrParser::getType(std::string var_name, 
                      SymbolType type) {
@@ -96,8 +91,7 @@ bool AntlrParser::isFunction(std::string name) {
   return isDeclared(name,SYM_FUNCTION) && getType(name)->isFunction();
 }
 
-/* Returns true if name is either a boolean variable OR a function
-   returning boolean. */
+/* Returns true if name is bound to a function returning boolean. */
 bool AntlrParser::isPredicate(std::string name) {
   return isDeclared(name,SYM_FUNCTION) && getType(name)->isPredicate();
 }
@@ -135,45 +129,32 @@ Expr AntlrParser::mkExpr(Kind kind, const std::vector<Expr>& children) {
   return result;
 }
 
-const FunctionType* 
+const Type* 
 AntlrParser::functionType(const Type* domainType, 
                           const Type* rangeType) {
   return d_exprManager->mkFunctionType(domainType,rangeType);
 }
 
-const FunctionType* 
+const Type* 
 AntlrParser::functionType(const std::vector<const Type*>& argTypes, 
                           const Type* rangeType) {
   Assert( argTypes.size() > 0 );
   return d_exprManager->mkFunctionType(argTypes,rangeType);
 }
 
-const FunctionType* 
+const Type* 
 AntlrParser::functionType(const std::vector<const Type*>& sorts) {
-  Assert( sorts.size() > 1 );
-  std::vector<const Type*> argTypes(sorts);
-  const Type* rangeType = argTypes.back();
-  argTypes.pop_back();
-  return functionType(argTypes,rangeType);
-}
-
-Expr AntlrParser::newFunction(std::string name, 
-                              const std::vector<const Type*>& sorts) {
   Assert( sorts.size() > 0 );
   if( sorts.size() == 1 ) {
-    return mkVar(name, sorts[0]);
+    return sorts[0];
   } else {
-    return mkVar(name, functionType(sorts));
+    std::vector<const Type*> argTypes(sorts);
+    const Type* rangeType = argTypes.back();
+    argTypes.pop_back();
+    return functionType(argTypes,rangeType);
   }
 }
 
-const std::vector<Expr>
-AntlrParser::newFunctions(const std::vector<std::string>& names, 
-                          const std::vector<const Type*>& sorts) {
-  const FunctionType* t = functionType(sorts);
-  return mkVars(names, t);
-}
-
 const Type* AntlrParser::predicateType(const std::vector<const Type*>& sorts) {
   if(sorts.size() == 0) {
     return d_exprManager->booleanType();
@@ -182,20 +163,6 @@ const Type* AntlrParser::predicateType(const std::vector<const Type*>& sorts) {
   }
 }
 
-Expr
-AntlrParser::newPredicate(std::string name,
-                          const std::vector<const Type*>& sorts) {
-  const Type* t = predicateType(sorts);
-  return mkVar(name, t);
-}
-
-const std::vector<Expr>
-AntlrParser::newPredicates(const std::vector<std::string>& names,
-                                const std::vector<const Type*>& sorts) {
-  const Type* t = predicateType(sorts);
-  return mkVars(names, t);
-}
-
 Expr 
 AntlrParser::mkVar(const std::string name, const Type* type) {
   Debug("parser") << "mkVar(" << name << "," << *type << ")" << std::endl;
@@ -301,7 +268,7 @@ unsigned int AntlrParser::maxArity(Kind kind) {
     return UINT_MAX;
 
   default:
-    Unhandled("kind in minArity");
+    Unhandled("kind in maxArity");
   }
 }
 
@@ -311,8 +278,7 @@ void AntlrParser::setExpressionManager(ExprManager* em) {
 
 bool AntlrParser::isDeclared(string name, SymbolType type) {
   switch(type) {
-  case SYM_VARIABLE: // Predicates and functions share var namespace
-  // case SYM_PREDICATE:
+  case SYM_VARIABLE: // Functions share var namespace
   case SYM_FUNCTION:
     return d_varSymbolTable.isBound(name);
   case SYM_SORT:
diff --git a/src/parser/antlr_parser.h b/src/parser/antlr_parser.h
index 3cfe4fc5d..76200368c 100644
--- a/src/parser/antlr_parser.h
+++ b/src/parser/antlr_parser.h
@@ -112,8 +112,13 @@ protected:
    * @return the variable expression
    */
   Expr getVariable(std::string var_name);
-  Expr getFunction(std::string var_name);
-  /* Expr getPredicate(std::string var_name); */
+
+  /**
+   * Returns a function, given a name and a type.
+   * @param name the name of the function
+   * @return the function expression
+   */
+  Expr getFunction(std::string name);
 
   /**
    * Returns a sort, given a name
@@ -121,13 +126,11 @@ protected:
   const Type* getSort(std::string sort_name);
 
   /**
-   * Types of symbols.
+   * Types of symbols. Used to define namespaces.
    */
   enum SymbolType {
     /** Variables */
     SYM_VARIABLE,
-    /** Predicates */
-    /* SYM_PREDICATE, */
     /** Functions */
     SYM_FUNCTION,
     /** Sorts */
@@ -135,23 +138,30 @@ protected:
   };
 
   /**
-   * Checks if the variable has been declared.
-   * @param the variable name
+   * Checks if a symbol has been declared.
+   * @param name the symbol name
+   * @param type the symbol type
    */
-  bool isDeclared(std::string var_name, SymbolType type = SYM_VARIABLE);
+  bool isDeclared(std::string name, SymbolType type = SYM_VARIABLE);
 
   /**
-   * Return true if the the declaration policy we want to enforce is true.
-   * @param varName the symbol to check
+   * Return true if the the declaration policy we want to enforce holds
+   * for the given symbol.
+   * @param name the symbol to check
    * @oaram check the kind of check to perform
+   * @param type the type of the symbol
    * @return true if the check holds
    */
-  bool checkDeclaration(std::string varName, 
+  bool checkDeclaration(std::string name, 
                         DeclarationCheck check,
                         SymbolType type = SYM_VARIABLE);
 
 
-  /** Returns the type for the variable with the given name. */
+  /** 
+   * Returns the type for the variable with the given name. 
+   * @param name the symbol to lookup 
+   * @param type the (namespace) type of the symbol
+   */
   const Type* getType(std::string var_name,
                       SymbolType type = SYM_VARIABLE);
 
@@ -202,63 +212,39 @@ protected:
    */
   Expr mkExpr(Kind kind, const std::vector<Expr>& children);
 
-  /* Create a new CVC4 variable expression . */
+  /** Create a new CVC4 variable expression of the given type. */
   Expr mkVar(const std::string name, const Type* type);
 
+  /** Create a set of new CVC4 variable expressions of the given
+      type. */
   const std::vector<Expr> 
   mkVars(const std::vector<std::string> names, 
          const Type* type);
 
 
   /** Returns a function type over the given domain and range types. */
-  const FunctionType* functionType(const Type* domain, const Type* range);
-  /** Returns a function type over the given types. argTypes must have
-      at least 1 element. */
-  const FunctionType* functionType(const std::vector<const Type*>& argTypes,
-                             const Type* rangeType);
-  /** Returns a function type over the given types. types must have
-      at least 2 elements (i.e., a domain and range). */
-  const FunctionType* functionType(const std::vector<const Type*>& types);
+  const Type* functionType(const Type* domain, const Type* range);
 
-  /**
-   * Creates a new function over the given sorts. The function
-   * has arity sorts.size() - 1 and range type sorts[sorts.size() - 1].
-   * @param name the name of the function
-   * @param sorts the sorts
-   */
-  Expr newFunction(std::string name, 
-                   const std::vector<const Type*>& sorts);
+  /** Returns a function type over the given types. argTypes must be
+      non-empty. */
+  const Type* functionType(const std::vector<const Type*>& argTypes,
+                           const Type* rangeType);
 
-  /**
-   * Creates new functions over the given sorts. Each function has
-   * arity sorts.size() - 1 and range type sorts[sorts.size() - 1].
-   * @param name the name of the function
-   * @param sorts the sorts
+  /** 
+   * Returns a function type over the given types. If types has only
+   * one element, then the type is just types[0].
+   *
+   * @param types a non-empty list of input and output types. 
    */
-  const std::vector<Expr> 
-  newFunctions(const std::vector<std::string>& names, 
-               const std::vector<const Type*>& sorts);
+  const Type* functionType(const std::vector<const Type*>& types);
 
-  /** Returns a predicate type over the given sorts. sorts must be 
-      non-empty. If sorts has size 1, then the type is just BOOLEAN. */
-  const Type* predicateType(const std::vector<const Type*>& sorts);
-
-  /**
-   * Creates a new predicate (a function with range boolean) over the 
-   * given sorts. The predicate has sorts.size().
-   * @param name the name of the predicate
-   * @param sorts the sorts
-   */
-  Expr newPredicate(std::string name, const std::vector<const Type*>& sorts);
+  /** 
+   * Returns a predicate type over the given sorts. If sorts is empty,
+   * then the type is just BOOLEAN.
 
-  /**
-   * Creates new predicates (a function with range boolean) over the 
-   * given sorts. Each predicate will have arity sorts.size().
-   * @param p_names the names of the predicates
+   * @param sorts a list of input types
    */
-  const std::vector<Expr>
-  newPredicates(const std::vector<std::string>& names,
-                const std::vector<const Type*>& sorts);
+  const Type* predicateType(const std::vector<const Type*>& sorts);
 
   /**
    * Creates a new sort with the given name.
@@ -271,21 +257,29 @@ protected:
   const std::vector<const Type*>
   newSorts(const std::vector<std::string>& names);
 
+  /** Is the symbol bound to a boolean variable? */
   bool isBoolean(std::string name);
+
+  /** Is the symbol bound to a function? */
   bool isFunction(std::string name);
+
+  /** Is the symbol bound to a predicate? */
   bool isPredicate(std::string name);
 
+  /** Returns the boolean type. */
   const BooleanType* booleanType();
+
+  /** Returns the kind type (i.e., the type of types). */
   const KindType* kindType();
 
-  unsigned int minArity(Kind kind);
-  unsigned int maxArity(Kind kind);
+  /** Returns the minimum arity of the given kind. */
+  static unsigned int minArity(Kind kind);
 
-  /**
-   * Returns the precedence rank of the kind.
-   */
-  static unsigned getPrecedence(Kind kind);
+  /** Returns the maximum arity of the given kind. */
+  static unsigned int maxArity(Kind kind);
 
+  /** Returns a string representation of the given object (for
+      debugging). */
   inline std::string toString(DeclarationCheck check) {
     switch(check) {
     case CHECK_NONE: return "CHECK_NONE";
@@ -295,6 +289,8 @@ protected:
     }
   }
 
+  /** Returns a string representation of the given object (for
+      debugging). */
   inline std::string toString(SymbolType type) {
     switch(type) {
     case SYM_VARIABLE: return "SYM_VARIABLE";
@@ -319,8 +315,8 @@ private:
   /** The sort table */
   SymbolTable<const Type*> d_sortTable;
 
+  /** Lookup a symbol in the given namespace. */
   Expr getSymbol(std::string var_name, SymbolType type);
-
 };
 
 
diff --git a/src/parser/smt/smt_parser.g b/src/parser/smt/smt_parser.g
index 28101532b..dbc9e1a21 100644
--- a/src/parser/smt/smt_parser.g
+++ b/src/parser/smt/smt_parser.g
@@ -259,7 +259,8 @@ functionDeclaration
       t = sortSymbol // require at least one sort
     { sorts.push_back(t); }
       sortList[sorts] RPAREN
-    { newFunction(name, sorts); } 
+    { t = functionType(sorts);
+      mkVar(name, t); } 
   ;
               
 /**
@@ -269,9 +270,11 @@ predicateDeclaration
 {
   string p_name;
   std::vector<const Type*> p_sorts;
+  const Type *t;
 }
   : LPAREN p_name = predicateName[CHECK_UNDECLARED] sortList[p_sorts] RPAREN
-    { newPredicate(p_name, p_sorts); } 
+    { t = predicateType(p_sorts);
+      mkVar(p_name, t); } 
   ;
 
 sortDeclaration