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

1 files changed, 143 insertions, 132 deletions

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() {