Documenting type.h/cpp

Making Boolean and Kind types singletons

3 files changed, 75 insertions, 110 deletions

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