Minor optimizations to parser (use const string& for ids, keep only one binding in symtab)

7 files changed, 47 insertions, 41 deletions

diff --git a/src/expr/expr_manager.cpp b/src/expr/expr_manager.cpp
index 6231d5a8a..6e1be2e09 100644
--- a/src/expr/expr_manager.cpp
+++ b/src/expr/expr_manager.cpp
@@ -117,13 +117,13 @@ ExprManager::mkFunctionType(const std::vector<const Type*>& argTypes,
   return FunctionType::getInstance(this, argTypes, range);
 }
 
-const Type* ExprManager::mkSort(std::string name) {
+const Type* ExprManager::mkSort(const std::string& name) {
   // FIXME: Sorts should be unique per-ExprManager
   NodeManagerScope nms(d_nodeManager);
   return new SortType(this, name);
 }
 
-Expr ExprManager::mkVar(const Type* type, string name) {
+Expr ExprManager::mkVar(const Type* type, const std::string& name) {
   NodeManagerScope nms(d_nodeManager);
   return Expr(this, new Node(d_nodeManager->mkVar(type, name)));
 }
diff --git a/src/expr/expr_manager.h b/src/expr/expr_manager.h
index 4b00c27fc..319a5d318 100644
--- a/src/expr/expr_manager.h
+++ b/src/expr/expr_manager.h
@@ -100,10 +100,10 @@ public:
                    const Type* range);
 
   /** Make a new sort with the given name. */
-  const Type* mkSort(std::string name);
+  const Type* mkSort(const std::string& name);
 
   // variables are special, because duplicates are permitted
-  Expr mkVar(const Type* type, std::string name);
+  Expr mkVar(const Type* type, const std::string& name);
   Expr mkVar(const Type* type);
 
 private:
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index ae6bdbd29..556b577e5 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -72,7 +72,7 @@ Node NodeManager::mkNode(Kind kind, const vector<Node>& children) {
   return NodeBuilder<>(this, kind).append(children);
 }
 
-Node NodeManager::mkVar(const Type* type, string name) {
+Node NodeManager::mkVar(const Type* type, const std::string& name) {
   Node n = mkVar(type);
   n.setAttribute(VarNameAttr(), name);
   return n;
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 29c738c10..1c46743e9 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -74,7 +74,7 @@ public:
   Node mkNode(Kind kind, const std::vector<Node>& children);
 
   // variables are special, because duplicates are permitted
-  Node mkVar(const Type* type, std::string name);
+  Node mkVar(const Type* type, const std::string& name);
   Node mkVar(const Type* type);
   Node mkVar();
 
diff --git a/src/parser/antlr_parser.cpp b/src/parser/antlr_parser.cpp
index 28cee62e7..066cb3aed 100644
--- a/src/parser/antlr_parser.cpp
+++ b/src/parser/antlr_parser.cpp
@@ -48,7 +48,7 @@ AntlrParser::AntlrParser(antlr::TokenStream& lexer, int k) :
   antlr::LLkParser(lexer, k), d_checksEnabled(true) {
 }
 
-Expr AntlrParser::getSymbol(std::string name, SymbolType type) {
+Expr AntlrParser::getSymbol(const std::string& name, SymbolType type) {
   Assert( isDeclared(name, type) );
 
 
@@ -63,40 +63,40 @@ Expr AntlrParser::getSymbol(std::string name, SymbolType type) {
   }
 }
 
-Expr AntlrParser::getVariable(std::string name) {
+Expr AntlrParser::getVariable(const std::string& name) {
   return getSymbol(name, SYM_VARIABLE);
 }
 
-Expr AntlrParser::getFunction(std::string name) {
+Expr AntlrParser::getFunction(const std::string& name) {
   return getSymbol(name, SYM_FUNCTION);
 }
 
 const Type* 
-AntlrParser::getType(std::string var_name, 
+AntlrParser::getType(const std::string& var_name,
                      SymbolType type) {
   Assert( isDeclared(var_name, type) );
   const Type* t = getSymbol(var_name,type).getType();
   return t;
 }
 
-const Type* AntlrParser::getSort(std::string name) {
+const Type* AntlrParser::getSort(const std::string& name) {
   Assert( isDeclared(name, SYM_SORT) );
   const Type* t = d_sortTable.getObject(name);
   return t;
 }
 
 /* Returns true if name is bound to a boolean variable. */
-bool AntlrParser::isBoolean(std::string name) {
+bool AntlrParser::isBoolean(const std::string& name) {
   return isDeclared(name, SYM_VARIABLE) && getType(name)->isBoolean();
 }
 
 /* Returns true if name is bound to a function. */
-bool AntlrParser::isFunction(std::string name) {
+bool AntlrParser::isFunction(const std::string& name) {
   return isDeclared(name, SYM_FUNCTION) && getType(name)->isFunction();
 }
 
 /* Returns true if name is bound to a function returning boolean. */
-bool AntlrParser::isPredicate(std::string name) {
+bool AntlrParser::isPredicate(const std::string& name) {
   return isDeclared(name, SYM_FUNCTION) && getType(name)->isPredicate();
 }
 
@@ -168,7 +168,7 @@ const Type* AntlrParser::predicateType(const std::vector<const Type*>& sorts) {
 }
 
 Expr 
-AntlrParser::mkVar(const std::string name, const Type* type) {
+AntlrParser::mkVar(const std::string& name, const Type* type) {
   Debug("parser") << "mkVar(" << name << "," << *type << ")" << std::endl;
   Assert( !isDeclared(name) ) ;
   Expr expr = d_exprManager->mkVar(type, name);
@@ -189,7 +189,7 @@ AntlrParser::mkVars(const std::vector<std::string> names,
 
 
 const Type* 
-AntlrParser::newSort(std::string name) {
+AntlrParser::newSort(const std::string& name) {
   Debug("parser") << "newSort(" << name << ")" << std::endl;
   Assert( !isDeclared(name, SYM_SORT) ) ;
   const Type* type = d_exprManager->mkSort(name);
@@ -279,7 +279,7 @@ void AntlrParser::setExpressionManager(ExprManager* em) {
   d_exprManager = em;
 }
 
-bool AntlrParser::isDeclared(string name, SymbolType type) {
+bool AntlrParser::isDeclared(const std::string& name, SymbolType type) {
   switch(type) {
   case SYM_VARIABLE: // Functions share var namespace
   case SYM_FUNCTION:
@@ -291,14 +291,14 @@ bool AntlrParser::isDeclared(string name, SymbolType type) {
   }
 }
 
-void AntlrParser::parseError(string message)
+void AntlrParser::parseError(const std::string& message)
     throw (antlr::SemanticException) {
   throw antlr::SemanticException(message, getFilename(),
                                  LT(1).get()->getLine(),
                                  LT(1).get()->getColumn());
 }
 
-void AntlrParser::checkDeclaration(string varName,
+void AntlrParser::checkDeclaration(const std::string& varName,
                                    DeclarationCheck check,
                                    SymbolType type)
     throw (antlr::SemanticException) {
@@ -327,7 +327,7 @@ void AntlrParser::checkDeclaration(string varName,
   }
 }
 
-void AntlrParser::checkFunction(string name)
+void AntlrParser::checkFunction(const std::string& name)
   throw (antlr::SemanticException) {
   if( d_checksEnabled && !isFunction(name) ) {
     parseError("Expecting function symbol, found '" + name + "'");
diff --git a/src/parser/antlr_parser.h b/src/parser/antlr_parser.h
index cab0a4f38..3fd94f82b 100644
--- a/src/parser/antlr_parser.h
+++ b/src/parser/antlr_parser.h
@@ -109,26 +109,26 @@ protected:
   /**
    * Throws an ANTLR semantic exception with the given message.
    */
-  void parseError(std::string msg) throw (antlr::SemanticException);
+  void parseError(const std::string& msg) throw (antlr::SemanticException);
 
   /**
    * Returns a variable, given a name and a type.
    * @param var_name the name of the variable
    * @return the variable expression
    */
-  Expr getVariable(std::string var_name);
+  Expr getVariable(const 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);
+  Expr getFunction(const std::string& name);
 
   /**
    * Returns a sort, given a name
    */
-  const Type* getSort(std::string sort_name);
+  const Type* getSort(const std::string& sort_name);
 
   /**
    * Types of symbols. Used to define namespaces.
@@ -148,7 +148,7 @@ protected:
    * @param type the symbol type
    * @return true iff the symbol has been declared with the given type
    */
-  bool isDeclared(std::string name, SymbolType type = SYM_VARIABLE);
+  bool isDeclared(const std::string& name, SymbolType type = SYM_VARIABLE);
 
   /**
    * Checks if the declaration policy we want to enforce holds
@@ -158,7 +158,7 @@ protected:
    * @param type the type of the symbol
    * @throws SemanticException if checks are enabled and the check fails
    */
-  void checkDeclaration(std::string name,
+  void checkDeclaration(const std::string& name,
                         DeclarationCheck check,
                         SymbolType type = SYM_VARIABLE)
     throw (antlr::SemanticException);
@@ -168,7 +168,7 @@ protected:
    * @param name the name to check
    * @throws SemanticException if checks are enabled and name is not bound to a function
    */
-  void checkFunction(std::string name) throw (antlr::SemanticException);
+  void checkFunction(const std::string& name) throw (antlr::SemanticException);
 
   /**
    * Check that <code>kind</code> can accept <code>numArgs</codes> arguments.
@@ -184,7 +184,7 @@ protected:
    * @param name the symbol to lookup 
    * @param type the (namespace) type of the symbol
    */
-  const Type* getType(std::string var_name,
+  const Type* getType(const std::string& var_name,
                       SymbolType type = SYM_VARIABLE);
 
   /**
@@ -235,7 +235,7 @@ protected:
   Expr mkExpr(Kind kind, const std::vector<Expr>& children);
 
   /** Create a new CVC4 variable expression of the given type. */
-  Expr mkVar(const std::string name, const Type* type);
+  Expr mkVar(const std::string& name, const Type* type);
 
   /** Create a set of new CVC4 variable expressions of the given
       type. */
@@ -271,7 +271,7 @@ protected:
   /**
    * Creates a new sort with the given name.
    */
-  const Type* newSort(std::string name);
+  const Type* newSort(const std::string& name);
 
   /**
    * Creates a new sorts with the given names.
@@ -280,13 +280,13 @@ protected:
   newSorts(const std::vector<std::string>& names);
 
   /** Is the symbol bound to a boolean variable? */
-  bool isBoolean(std::string name);
+  bool isBoolean(const std::string& name);
 
   /** Is the symbol bound to a function? */
-  bool isFunction(std::string name);
+  bool isFunction(const std::string& name);
 
   /** Is the symbol bound to a predicate? */
-  bool isPredicate(std::string name);
+  bool isPredicate(const std::string& name);
 
   /** Returns the boolean type. */
   const BooleanType* booleanType();
@@ -339,7 +339,7 @@ private:
   bool d_checksEnabled;
 
   /** Lookup a symbol in the given namespace. */
-  Expr getSymbol(std::string var_name, SymbolType type);
+  Expr getSymbol(const std::string& var_name, SymbolType type);
 };
 
 
diff --git a/src/parser/symbol_table.h b/src/parser/symbol_table.h
index dd110c4c1..1f43dbda6 100644
--- a/src/parser/symbol_table.h
+++ b/src/parser/symbol_table.h
@@ -42,8 +42,12 @@ class SymbolTable {
 private:
 
   /** The name to expression bindings */
+  typedef __gnu_cxx::hash_map<std::string, ObjectType>
+  LookupTable;
+/*
   typedef __gnu_cxx::hash_map<std::string, std::stack<ObjectType> >
   LookupTable;
+*/
   /** The table iterator */
   typedef typename LookupTable::iterator table_iterator;
   /** The table iterator */
@@ -58,21 +62,23 @@ public:
    * Bind the name of the variable to the given expression. If the variable
    * has been bind before, this will redefine it until its undefined.
    */
-  void bindName(const std::string name, const ObjectType& obj) throw () {
-    d_nameBindings[name].push(obj);
+  void bindName(const std::string& name, const ObjectType& obj) throw () {
+    d_nameBindings[name] = obj;
     Assert(isBound(name), "Expected name to be bound!");
   }
 
   /**
    * Unbinds the last binding of the name to the expression.
    */
-  void unbindName(const std::string name) throw () {
+  void unbindName(const std::string& name) throw () {
     table_iterator find = d_nameBindings.find(name);
     if(find != d_nameBindings.end()) {
+/*
       find->second.pop();
       if(find->second.empty()) {
+*/
         d_nameBindings.erase(find);
-      }
+/*      }*/
     }
   }
 
@@ -80,16 +86,16 @@ public:
    * Returns the last binding expression of the name.
    * Requires the name to have a binding in the table.
    */
-  ObjectType getObject(const std::string name) throw () {
+  ObjectType getObject(const std::string& name) throw () {
     table_iterator find = d_nameBindings.find(name);
     Assert(find != d_nameBindings.end());
-    return find->second.top();
+    return find->second /*.top()*/ ;
   }
 
   /**
    * Returns true is name is bound to an expression.
    */
-  bool isBound(const std::string name) const throw () {
+  bool isBound(const std::string& name) const throw () {
     const_table_iterator find = d_nameBindings.find(name);
     return (find != d_nameBindings.end());
   }