From: Tim King <taking@cs.nyu.edu>
Date: Mon, 2 Oct 2017 16:11:49 +0000 (-0700)
Subject: Removing throw specifiers from SymbolTable::Implementation. (#1183)
X-Git-Tag: cvc5-1.0.0~5589
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f1c7be3a9b96f1a949f127344ecc775680da2c8e;p=cvc5.git

Removing throw specifiers from SymbolTable::Implementation. (#1183)
---

diff --git a/src/expr/symbol_table.cpp b/src/expr/symbol_table.cpp
index b411d8dfb..33046be7a 100644
--- a/src/expr/symbol_table.cpp
+++ b/src/expr/symbol_table.cpp
@@ -20,8 +20,8 @@
 
 #include <ostream>
 #include <string>
-#include <utility>
 #include <unordered_map>
+#include <utility>
 
 #include "context/cdhashmap.h"
 #include "context/cdhashset.h"
@@ -45,82 +45,84 @@ using ::std::vector;
 // This data structure stores a trie of expressions with
 // the same name, and must be distinguished by their argument types.
 // It is context-dependent.
-class OverloadedTypeTrie
-{
-public:
-  OverloadedTypeTrie(Context * c ) :
-    d_overloaded_symbols(new (true) CDHashSet<Expr, ExprHashFunction>(c)) {
-  }  
-  ~OverloadedTypeTrie() {
-    d_overloaded_symbols->deleteSelf();
-  }
+class OverloadedTypeTrie {
+ public:
+  OverloadedTypeTrie(Context* c)
+      : d_overloaded_symbols(new (true) CDHashSet<Expr, ExprHashFunction>(c)) {}
+  ~OverloadedTypeTrie() { d_overloaded_symbols->deleteSelf(); }
+
   /** is this function overloaded? */
   bool isOverloadedFunction(Expr fun) const;
-  
+
   /** Get overloaded constant for type.
    * If possible, it returns a defined symbol with name
    * that has type t. Otherwise returns null expression.
-  */
+   */
   Expr getOverloadedConstantForType(const std::string& name, Type t) const;
-  
+
   /**
    * If possible, returns a defined function for a name
    * and a vector of expected argument types. Otherwise returns
    * null expression.
    */
-  Expr getOverloadedFunctionForTypes(const std::string& name, const std::vector< Type >& argTypes) const;
-  /** called when obj is bound to name, and prev_bound_obj was already bound to name 
-  * Returns false if the binding is invalid.
-  */
+  Expr getOverloadedFunctionForTypes(const std::string& name,
+                                     const std::vector<Type>& argTypes) const;
+  /** called when obj is bound to name, and prev_bound_obj was already bound to
+   * name Returns false if the binding is invalid.
+   */
   bool bind(const string& name, Expr prev_bound_obj, Expr obj);
-private:
-  /** Marks expression obj with name as overloaded. 
+
+ private:
+  /** Marks expression obj with name as overloaded.
    * Adds relevant information to the type arg trie data structure.
    * It returns false if there is already an expression bound to that name
-   * whose type expects the same arguments as the type of obj but is not identical
-   * to the type of obj.  For example, if we declare :
+   * whose type expects the same arguments as the type of obj but is not
+   * identical to the type of obj.  For example, if we declare :
    *
    * (declare-datatypes () ((List (cons (hd Int) (tl List)) (nil))))
    * (declare-fun cons (Int List) List)
    *
    * cons : constructor_type( Int, List, List )
    * cons : function_type( Int, List, List )
-   * 
+   *
    * These are put in the same place in the trie but do not have identical type,
    * hence we return false.
-  */
+   */
   bool markOverloaded(const string& name, Expr obj);
   /** the null expression */
   Expr d_nullExpr;
   // The (context-independent) trie storing that maps expected argument
-  // vectors to symbols. All expressions stored in d_symbols are only 
+  // vectors to symbols. All expressions stored in d_symbols are only
   // interpreted as active if they also appear in the context-dependent
   // set d_overloaded_symbols.
   class TypeArgTrie {
-  public:
+   public:
     // children of this node
-    std::map< Type, TypeArgTrie > d_children;
+    std::map<Type, TypeArgTrie> d_children;
     // symbols at this node
-    std::map< Type, Expr > d_symbols;
+    std::map<Type, Expr> d_symbols;
   };
-  /** for each string with operator overloading, this stores the data structure above. */
-  std::unordered_map< std::string, TypeArgTrie > d_overload_type_arg_trie;
+  /** for each string with operator overloading, this stores the data structure
+   * above. */
+  std::unordered_map<std::string, TypeArgTrie> d_overload_type_arg_trie;
   /** The set of overloaded symbols. */
   CDHashSet<Expr, ExprHashFunction>* d_overloaded_symbols;
 };
 
 bool OverloadedTypeTrie::isOverloadedFunction(Expr fun) const {
-  return d_overloaded_symbols->find(fun)!=d_overloaded_symbols->end();
+  return d_overloaded_symbols->find(fun) != d_overloaded_symbols->end();
 }
 
-Expr OverloadedTypeTrie::getOverloadedConstantForType(const std::string& name, Type t) const {
-  std::unordered_map< std::string, TypeArgTrie >::const_iterator it = d_overload_type_arg_trie.find(name);
-  if(it!=d_overload_type_arg_trie.end()) {
-    std::map< Type, Expr >::const_iterator its = it->second.d_symbols.find(t);
-    if(its!=it->second.d_symbols.end()) {
+Expr OverloadedTypeTrie::getOverloadedConstantForType(const std::string& name,
+                                                      Type t) const {
+  std::unordered_map<std::string, TypeArgTrie>::const_iterator it =
+      d_overload_type_arg_trie.find(name);
+  if (it != d_overload_type_arg_trie.end()) {
+    std::map<Type, Expr>::const_iterator its = it->second.d_symbols.find(t);
+    if (its != it->second.d_symbols.end()) {
       Expr expr = its->second;
       // must be an active symbol
-      if(isOverloadedFunction(expr)) {
+      if (isOverloadedFunction(expr)) {
         return expr;
       }
     }
@@ -128,28 +130,31 @@ Expr OverloadedTypeTrie::getOverloadedConstantForType(const std::string& name, T
   return d_nullExpr;
 }
 
-Expr OverloadedTypeTrie::getOverloadedFunctionForTypes(const std::string& name, 
-                                                       const std::vector< Type >& argTypes) const {
-  std::unordered_map< std::string, TypeArgTrie >::const_iterator it = d_overload_type_arg_trie.find(name);
-  if(it!=d_overload_type_arg_trie.end()) {
-    const TypeArgTrie * tat = &it->second;
-    for(unsigned i=0; i<argTypes.size(); i++) {
-      std::map< Type, TypeArgTrie >::const_iterator itc = tat->d_children.find(argTypes[i]);
-      if(itc!=tat->d_children.end()) {
+Expr OverloadedTypeTrie::getOverloadedFunctionForTypes(
+    const std::string& name, const std::vector<Type>& argTypes) const {
+  std::unordered_map<std::string, TypeArgTrie>::const_iterator it =
+      d_overload_type_arg_trie.find(name);
+  if (it != d_overload_type_arg_trie.end()) {
+    const TypeArgTrie* tat = &it->second;
+    for (unsigned i = 0; i < argTypes.size(); i++) {
+      std::map<Type, TypeArgTrie>::const_iterator itc =
+          tat->d_children.find(argTypes[i]);
+      if (itc != tat->d_children.end()) {
         tat = &itc->second;
-      }else{
-        // no functions match 
+      } else {
+        // no functions match
         return d_nullExpr;
       }
     }
     // now, we must ensure that there is *only* one active symbol at this node
     Expr retExpr;
-    for(std::map< Type, Expr >::const_iterator its = tat->d_symbols.begin(); its != tat->d_symbols.end(); ++its) {
+    for (std::map<Type, Expr>::const_iterator its = tat->d_symbols.begin();
+         its != tat->d_symbols.end(); ++its) {
       Expr expr = its->second;
-      if(isOverloadedFunction(expr)) {
-        if(retExpr.isNull()) {
+      if (isOverloadedFunction(expr)) {
+        if (retExpr.isNull()) {
           retExpr = expr;
-        }else{
+        } else {
           // multiple functions match
           return d_nullExpr;
         }
@@ -160,9 +165,10 @@ Expr OverloadedTypeTrie::getOverloadedFunctionForTypes(const std::string& name,
   return d_nullExpr;
 }
 
-bool OverloadedTypeTrie::bind(const string& name, Expr prev_bound_obj, Expr obj) {
+bool OverloadedTypeTrie::bind(const string& name, Expr prev_bound_obj,
+                              Expr obj) {
   bool retprev = true;
-  if(!isOverloadedFunction(prev_bound_obj)) {
+  if (!isOverloadedFunction(prev_bound_obj)) {
     // mark previous as overloaded
     retprev = markOverloaded(name, prev_bound_obj);
   }
@@ -177,56 +183,58 @@ bool OverloadedTypeTrie::markOverloaded(const string& name, Expr obj) {
   // get the argument types
   Type t = obj.getType();
   Type rangeType = t;
-  std::vector< Type > argTypes;
-  if(t.isFunction()) {
+  std::vector<Type> argTypes;
+  if (t.isFunction()) {
     argTypes = static_cast<FunctionType>(t).getArgTypes();
     rangeType = static_cast<FunctionType>(t).getRangeType();
-  }else if(t.isConstructor()) {
+  } else if (t.isConstructor()) {
     argTypes = static_cast<ConstructorType>(t).getArgTypes();
     rangeType = static_cast<ConstructorType>(t).getRangeType();
-  }else if(t.isTester()) {
-    argTypes.push_back( static_cast<TesterType>(t).getDomain() );
+  } else if (t.isTester()) {
+    argTypes.push_back(static_cast<TesterType>(t).getDomain());
     rangeType = static_cast<TesterType>(t).getRangeType();
-  }else if(t.isSelector()) {
-    argTypes.push_back( static_cast<SelectorType>(t).getDomain() );
+  } else if (t.isSelector()) {
+    argTypes.push_back(static_cast<SelectorType>(t).getDomain());
     rangeType = static_cast<SelectorType>(t).getRangeType();
   }
   // add to the trie
-  TypeArgTrie * tat = &d_overload_type_arg_trie[name];
-  for(unsigned i=0; i<argTypes.size(); i++) {
+  TypeArgTrie* tat = &d_overload_type_arg_trie[name];
+  for (unsigned i = 0; i < argTypes.size(); i++) {
     tat = &(tat->d_children[argTypes[i]]);
   }
-  
-  // types can be identical but vary on the kind of the type, thus we must distinguish based on this
-  std::map< Type, Expr >::iterator it = tat->d_symbols.find( rangeType );
-  if( it!=tat->d_symbols.end() ){
+
+  // types can be identical but vary on the kind of the type, thus we must
+  // distinguish based on this
+  std::map<Type, Expr>::iterator it = tat->d_symbols.find(rangeType);
+  if (it != tat->d_symbols.end()) {
     Expr prev_obj = it->second;
-    // if there is already an active function with the same name and expects the same argument types
-    if( isOverloadedFunction(prev_obj) ){
-      if( prev_obj.getType()==obj.getType() ){
-        //types are identical, simply ignore it
+    // if there is already an active function with the same name and expects the
+    // same argument types
+    if (isOverloadedFunction(prev_obj)) {
+      if (prev_obj.getType() == obj.getType()) {
+        // types are identical, simply ignore it
         return true;
-      }else{
-        //otherwise there is no way to distinguish these types, we return an error
+      } else {
+        // otherwise there is no way to distinguish these types, we return an
+        // error
         return false;
       }
     }
   }
-  
+
   // otherwise, update the symbols
   d_overloaded_symbols->insert(obj);
   tat->d_symbols[rangeType] = obj;
   return true;
 }
 
-
 class SymbolTable::Implementation {
  public:
   Implementation()
       : d_context(),
         d_exprMap(new (true) CDHashMap<string, Expr>(&d_context)),
         d_typeMap(new (true) TypeMap(&d_context)),
-        d_functions(new (true) CDHashSet<Expr, ExprHashFunction>(&d_context)){
+        d_functions(new (true) CDHashSet<Expr, ExprHashFunction>(&d_context)) {
     d_overload_trie = new OverloadedTypeTrie(&d_context);
   }
 
@@ -237,33 +245,34 @@ class SymbolTable::Implementation {
     delete d_overload_trie;
   }
 
-  bool bind(const string& name, Expr obj, bool levelZero, bool doOverload) throw();
-  bool bindDefinedFunction(const string& name, Expr obj,
-                           bool levelZero, bool doOverload) throw();
-  void bindType(const string& name, Type t, bool levelZero = false) throw();
+  bool bind(const string& name, Expr obj, bool levelZero, bool doOverload);
+  bool bindDefinedFunction(const string& name, Expr obj, bool levelZero,
+                           bool doOverload);
+  void bindType(const string& name, Type t, bool levelZero = false);
   void bindType(const string& name, const vector<Type>& params, Type t,
-                bool levelZero = false) throw();
-  bool isBound(const string& name) const throw();
-  bool isBoundDefinedFunction(const string& name) const throw();
-  bool isBoundDefinedFunction(Expr func) const throw();
-  bool isBoundType(const string& name) const throw();
-  Expr lookup(const string& name) const throw();
-  Type lookupType(const string& name) const throw();
-  Type lookupType(const string& name, const vector<Type>& params) const throw();
+                bool levelZero = false);
+  bool isBound(const string& name) const;
+  bool isBoundDefinedFunction(const string& name) const;
+  bool isBoundDefinedFunction(Expr func) const;
+  bool isBoundType(const string& name) const;
+  Expr lookup(const string& name) const;
+  Type lookupType(const string& name) const;
+  Type lookupType(const string& name, const vector<Type>& params) const;
   size_t lookupArity(const string& name);
-  void popScope() throw(ScopeException);
-  void pushScope() throw();
-  size_t getLevel() const throw();
+  void popScope();
+  void pushScope();
+  size_t getLevel() const;
   void reset();
   //------------------------ operator overloading
   /** implementation of function from header */
   bool isOverloadedFunction(Expr fun) const;
-  
+
   /** implementation of function from header */
   Expr getOverloadedConstantForType(const std::string& name, Type t) const;
-  
+
   /** implementation of function from header */
-  Expr getOverloadedFunctionForTypes(const std::string& name, const std::vector< Type >& argTypes) const;
+  Expr getOverloadedFunctionForTypes(const std::string& name,
+                                     const std::vector<Type>& argTypes) const;
   //------------------------ end operator overloading
  private:
   /** The context manager for the scope maps. */
@@ -278,27 +287,27 @@ class SymbolTable::Implementation {
 
   /** A set of defined functions. */
   CDHashSet<Expr, ExprHashFunction>* d_functions;
-  
+
   //------------------------ operator overloading
   // the null expression
   Expr d_nullExpr;
   // overloaded type trie, stores all information regarding overloading
-  OverloadedTypeTrie * d_overload_trie;
+  OverloadedTypeTrie* d_overload_trie;
   /** bind with overloading
-   * This is called whenever obj is bound to name where overloading symbols is allowed.
-   * If a symbol is previously bound to that name, it marks both as overloaded.
-   * Returns false if the binding was invalid.
-  */
+   * This is called whenever obj is bound to name where overloading symbols is
+   * allowed. If a symbol is previously bound to that name, it marks both as
+   * overloaded. Returns false if the binding was invalid.
+   */
   bool bindWithOverloading(const string& name, Expr obj);
   //------------------------ end operator overloading
 }; /* SymbolTable::Implementation */
 
 bool SymbolTable::Implementation::bind(const string& name, Expr obj,
-                                       bool levelZero, bool doOverload) throw() {
+                                       bool levelZero, bool doOverload) {
   PrettyCheckArgument(!obj.isNull(), obj, "cannot bind to a null Expr");
   ExprManagerScope ems(obj);
   if (doOverload) {
-    if( !bindWithOverloading(name, obj) ){
+    if (!bindWithOverloading(name, obj)) {
       return false;
     }
   }
@@ -311,13 +320,12 @@ bool SymbolTable::Implementation::bind(const string& name, Expr obj,
 }
 
 bool SymbolTable::Implementation::bindDefinedFunction(const string& name,
-                                                      Expr obj,
-                                                      bool levelZero, 
-                                                      bool doOverload) throw() {
+                                                      Expr obj, bool levelZero,
+                                                      bool doOverload) {
   PrettyCheckArgument(!obj.isNull(), obj, "cannot bind to a null Expr");
   ExprManagerScope ems(obj);
   if (doOverload) {
-    if( !bindWithOverloading(name, obj) ){
+    if (!bindWithOverloading(name, obj)) {
       return false;
     }
   }
@@ -331,32 +339,32 @@ bool SymbolTable::Implementation::bindDefinedFunction(const string& name,
   return true;
 }
 
-bool SymbolTable::Implementation::isBound(const string& name) const throw() {
+bool SymbolTable::Implementation::isBound(const string& name) const {
   return d_exprMap->find(name) != d_exprMap->end();
 }
 
 bool SymbolTable::Implementation::isBoundDefinedFunction(
-    const string& name) const throw() {
+    const string& name) const {
   CDHashMap<string, Expr>::iterator found = d_exprMap->find(name);
   return found != d_exprMap->end() && d_functions->contains((*found).second);
 }
 
-bool SymbolTable::Implementation::isBoundDefinedFunction(Expr func) const
-    throw() {
+bool SymbolTable::Implementation::isBoundDefinedFunction(Expr func) const {
   return d_functions->contains(func);
 }
 
-Expr SymbolTable::Implementation::lookup(const string& name) const throw() {
+Expr SymbolTable::Implementation::lookup(const string& name) const {
+  Assert(isBound(name));
   Expr expr = (*d_exprMap->find(name)).second;
-  if(isOverloadedFunction(expr)) {
+  if (isOverloadedFunction(expr)) {
     return d_nullExpr;
-  }else{
+  } else {
     return expr;
   }
 }
 
 void SymbolTable::Implementation::bindType(const string& name, Type t,
-                                           bool levelZero) throw() {
+                                           bool levelZero) {
   if (levelZero) {
     d_typeMap->insertAtContextLevelZero(name, make_pair(vector<Type>(), t));
   } else {
@@ -366,7 +374,7 @@ void SymbolTable::Implementation::bindType(const string& name, Type t,
 
 void SymbolTable::Implementation::bindType(const string& name,
                                            const vector<Type>& params, Type t,
-                                           bool levelZero) throw() {
+                                           bool levelZero) {
   if (Debug.isOn("sort")) {
     Debug("sort") << "bindType(" << name << ", [";
     if (params.size() > 0) {
@@ -383,12 +391,11 @@ void SymbolTable::Implementation::bindType(const string& name,
   }
 }
 
-bool SymbolTable::Implementation::isBoundType(const string& name) const
-    throw() {
+bool SymbolTable::Implementation::isBoundType(const string& name) const {
   return d_typeMap->find(name) != d_typeMap->end();
 }
 
-Type SymbolTable::Implementation::lookupType(const string& name) const throw() {
+Type SymbolTable::Implementation::lookupType(const string& name) const {
   pair<vector<Type>, Type> p = (*d_typeMap->find(name)).second;
   PrettyCheckArgument(p.first.size() == 0, name,
                       "type constructor arity is wrong: "
@@ -398,8 +405,7 @@ Type SymbolTable::Implementation::lookupType(const string& name) const throw() {
 }
 
 Type SymbolTable::Implementation::lookupType(const string& name,
-                                             const vector<Type>& params) const
-    throw() {
+                                             const vector<Type>& params) const {
   pair<vector<Type>, Type> p = (*d_typeMap->find(name)).second;
   PrettyCheckArgument(p.first.size() == params.size(), params,
                       "type constructor arity is wrong: "
@@ -459,16 +465,16 @@ size_t SymbolTable::Implementation::lookupArity(const string& name) {
   return p.first.size();
 }
 
-void SymbolTable::Implementation::popScope() throw(ScopeException) {
+void SymbolTable::Implementation::popScope() {
   if (d_context.getLevel() == 0) {
     throw ScopeException();
   }
   d_context.pop();
 }
 
-void SymbolTable::Implementation::pushScope() throw() { d_context.push(); }
+void SymbolTable::Implementation::pushScope() { d_context.push(); }
 
-size_t SymbolTable::Implementation::getLevel() const throw() {
+size_t SymbolTable::Implementation::getLevel() const {
   return d_context.getLevel();
 }
 
@@ -481,20 +487,22 @@ bool SymbolTable::Implementation::isOverloadedFunction(Expr fun) const {
   return d_overload_trie->isOverloadedFunction(fun);
 }
 
-Expr SymbolTable::Implementation::getOverloadedConstantForType(const std::string& name, Type t) const {
+Expr SymbolTable::Implementation::getOverloadedConstantForType(
+    const std::string& name, Type t) const {
   return d_overload_trie->getOverloadedConstantForType(name, t);
 }
 
-Expr SymbolTable::Implementation::getOverloadedFunctionForTypes(const std::string& name, 
-                                                                const std::vector< Type >& argTypes) const {
+Expr SymbolTable::Implementation::getOverloadedFunctionForTypes(
+    const std::string& name, const std::vector<Type>& argTypes) const {
   return d_overload_trie->getOverloadedFunctionForTypes(name, argTypes);
 }
 
-bool SymbolTable::Implementation::bindWithOverloading(const string& name, Expr obj){
+bool SymbolTable::Implementation::bindWithOverloading(const string& name,
+                                                      Expr obj) {
   CDHashMap<string, Expr>::const_iterator it = d_exprMap->find(name);
-  if(it != d_exprMap->end()) {
+  if (it != d_exprMap->end()) {
     const Expr& prev_bound_obj = (*it).second;
-    if(prev_bound_obj!=obj) {
+    if (prev_bound_obj != obj) {
       return d_overload_trie->bind(name, prev_bound_obj, obj);
     }
   }
@@ -505,12 +513,13 @@ bool SymbolTable::isOverloadedFunction(Expr fun) const {
   return d_implementation->isOverloadedFunction(fun);
 }
 
-Expr SymbolTable::getOverloadedConstantForType(const std::string& name, Type t) const {
+Expr SymbolTable::getOverloadedConstantForType(const std::string& name,
+                                               Type t) const {
   return d_implementation->getOverloadedConstantForType(name, t);
 }
 
-Expr SymbolTable::getOverloadedFunctionForTypes(const std::string& name, 
-                                                const std::vector< Type >& argTypes) const {
+Expr SymbolTable::getOverloadedFunctionForTypes(
+    const std::string& name, const std::vector<Type>& argTypes) const {
   return d_implementation->getOverloadedFunctionForTypes(name, argTypes);
 }
 
@@ -519,13 +528,15 @@ SymbolTable::SymbolTable()
 
 SymbolTable::~SymbolTable() {}
 
-bool SymbolTable::bind(const string& name, Expr obj, bool levelZero, bool doOverload) throw() {
+bool SymbolTable::bind(const string& name, Expr obj, bool levelZero,
+                       bool doOverload) throw() {
   return d_implementation->bind(name, obj, levelZero, doOverload);
 }
 
 bool SymbolTable::bindDefinedFunction(const string& name, Expr obj,
                                       bool levelZero, bool doOverload) throw() {
-  return d_implementation->bindDefinedFunction(name, obj, levelZero, doOverload);
+  return d_implementation->bindDefinedFunction(name, obj, levelZero,
+                                               doOverload);
 }
 
 void SymbolTable::bindType(const string& name, Type t, bool levelZero) throw() {
diff --git a/src/expr/symbol_table.h b/src/expr/symbol_table.h
index b6ca7a76f..854e8a04e 100644
--- a/src/expr/symbol_table.h
+++ b/src/expr/symbol_table.h
@@ -43,13 +43,13 @@ class CVC4_PUBLIC SymbolTable {
   ~SymbolTable();
 
   /**
-   * Bind an expression to a name in the current scope level.  
+   * Bind an expression to a name in the current scope level.
    *
    * When doOverload is false:
    * if <code>name</code> is already bound to an expression in the current
    * level, then the binding is replaced. If <code>name</code> is bound
    * in a previous level, then the binding is "covered" by this one
-   * until the current scope is popped. 
+   * until the current scope is popped.
    * If levelZero is true the name shouldn't be already bound.
    *
    * When doOverload is true:
@@ -64,17 +64,17 @@ class CVC4_PUBLIC SymbolTable {
    *
    * Returns false if the binding was invalid.
    */
-  bool bind(const std::string& name, Expr obj, bool levelZero = false, 
+  bool bind(const std::string& name, Expr obj, bool levelZero = false,
             bool doOverload = false) throw();
 
   /**
-   * Bind a function body to a name in the current scope.  
+   * Bind a function body to a name in the current scope.
    *
    * When doOverload is false:
    * if <code>name</code> is already bound to an expression in the current
    * level, then the binding is replaced. If <code>name</code> is bound
    * in a previous level, then the binding is "covered" by this one
-   * until the current scope is popped. 
+   * until the current scope is popped.
    * If levelZero is true the name shouldn't be already bound.
    *
    * When doOverload is true:
@@ -82,7 +82,7 @@ class CVC4_PUBLIC SymbolTable {
    * level, then we mark the previous bound expression and obj as overloaded
    * functions.
    *
-   * Same as bind() but registers this as a function (so that 
+   * Same as bind() but registers this as a function (so that
    * isBoundDefinedFunction() returns true).
    *
    * @param name an identifier
@@ -93,7 +93,7 @@ class CVC4_PUBLIC SymbolTable {
    * Returns false if the binding was invalid.
    */
   bool bindDefinedFunction(const std::string& name, Expr obj,
-                           bool levelZero = false, 
+                           bool levelZero = false,
                            bool doOverload = false) throw();
 
   /**
@@ -158,8 +158,9 @@ class CVC4_PUBLIC SymbolTable {
    * Lookup a bound expression.
    *
    * @param name the identifier to lookup
-   * @returns the unique expression bound to <code>name</code> in the current scope.
-   * It returns the null expression if there is not a unique expression bound to 
+   * @returns the unique expression bound to <code>name</code> in the current
+   * scope.
+   * It returns the null expression if there is not a unique expression bound to
    * <code>name</code> in the current scope (i.e. if there is not exactly one).
    */
   Expr lookup(const std::string& name) const throw();
@@ -189,15 +190,14 @@ class CVC4_PUBLIC SymbolTable {
   size_t lookupArity(const std::string& name);
 
   /**
-   * Pop a scope level. Deletes all bindings since the last call to
-   * <code>pushScope</code>. Calls to <code>pushScope</code> and
-   * <code>popScope</code> must be "properly nested." I.e., a call to
-   * <code>popScope</code> is only legal if the number of prior calls to
-   * <code>pushScope</code> on this <code>SymbolTable</code> is strictly
-   * greater than then number of prior calls to <code>popScope</code>. */
+   * Pop a scope level, deletes all bindings since the last call to pushScope,
+   * and decreases the level by 1.
+   *
+   * @throws ScopeException if the scope level is 0.
+   */
   void popScope() throw(ScopeException);
 
-  /** Push a scope level. */
+  /** Push a scope level and increase the scope level by 1. */
   void pushScope() throw();
 
   /** Get the current level of this symbol table. */
@@ -205,31 +205,32 @@ class CVC4_PUBLIC SymbolTable {
 
   /** Reset everything. */
   void reset();
-  
+
   //------------------------ operator overloading
   /** is this function overloaded? */
   bool isOverloadedFunction(Expr fun) const;
-  
+
   /** Get overloaded constant for type.
    * If possible, it returns the defined symbol with name
    * that has type t. Otherwise returns null expression.
   */
   Expr getOverloadedConstantForType(const std::string& name, Type t) const;
-  
+
   /**
    * If possible, returns the unique defined function for a name
    * that expects arguments with types "argTypes".
-   * For example, if argTypes = ( T1, ..., Tn ), then this may return 
-   * an expression with type function( T1, ..., Tn ), or constructor( T1, ...., Tn ).
-   * 
+   * For example, if argTypes = (T1, ..., Tn), then this may return an
+   * expression with type function(T1, ..., Tn), or constructor(T1, ...., Tn).
+   *
    * If there is not a unique defined function for the name and argTypes,
    * this returns the null expression. This can happen either if there are
    * no functions with name and expected argTypes, or alternatively there is
    * more than one function with name and expected argTypes.
    */
-  Expr getOverloadedFunctionForTypes(const std::string& name, const std::vector< Type >& argTypes) const;
+  Expr getOverloadedFunctionForTypes(const std::string& name,
+                                     const std::vector< Type >& argTypes) const;
   //------------------------ end operator overloading
-  
+
  private:
   // Copying and assignment have not yet been implemented.
   SymbolTable(const SymbolTable&);