1 files changed, 52 insertions, 47 deletions

diff --git a/src/parser/symbol_table.h b/src/parser/symbol_table.h
index 3b08aa5f5..32532c734 100644
--- a/src/parser/symbol_table.h
+++ b/src/parser/symbol_table.h
@@ -9,6 +9,9 @@
  **
  **/
 
+#ifndef __CVC4__PARSER__SYMBOL_TABLE_H
+#define __CVC4__PARSER__SYMBOL_TABLE_H
+
 #include <string>
 #include <stack>
 #include <ext/hash_map>
@@ -31,63 +34,65 @@ namespace parser {
  * Generic symbol table for looking up variables by name.
  */
 template<typename ObjectType>
-  class SymbolTable {
+class SymbolTable {
 
-  private:
+private:
 
-    /** The name to expression bindings */
-    typedef __gnu_cxx ::hash_map<std::string, std::stack<ObjectType> >
-        LookupTable;
-    /** The table iterator */
-    typedef typename LookupTable::iterator table_iterator;
-    /** The table iterator */
-    typedef typename LookupTable::const_iterator const_table_iterator;
+  /** The name to expression bindings */
+  typedef __gnu_cxx ::hash_map<std::string, std::stack<ObjectType> >
+  LookupTable;
+  /** The table iterator */
+  typedef typename LookupTable::iterator table_iterator;
+  /** The table iterator */
+  typedef typename LookupTable::const_iterator const_table_iterator;
 
-    /** Bindings for the names */
-    LookupTable d_name_bindings;
+  /** Bindings for the names */
+  LookupTable d_name_bindings;
 
-  public:
+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_name_bindings[name].push(obj);
-    }
+  /**
+   * 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_name_bindings[name].push(obj);
+  }
 
-    /**
-     * Unbinds the last binding of the name to the expression.
-     */
-    void unbindName(const std::string name) throw () {
-      table_iterator find = d_name_bindings.find(name);
-      if(find != d_name_bindings.end()) {
-        find->second.pop();
-        if(find->second.empty()) {
-          d_name_bindings.erase(find);
-        }
+  /**
+   * Unbinds the last binding of the name to the expression.
+   */
+  void unbindName(const std::string name) throw () {
+    table_iterator find = d_name_bindings.find(name);
+    if(find != d_name_bindings.end()) {
+      find->second.pop();
+      if(find->second.empty()) {
+        d_name_bindings.erase(find);
       }
     }
+  }
 
-    /**
-     * Returns the last binding expression of the name.
-     */
-    ObjectType getObject(const std::string name) throw () {
-      ObjectType result;
-      table_iterator find = d_name_bindings.find(name);
-      if(find != d_name_bindings.end())
-        result = find->second.top();
-      return result;
-    }
+  /**
+   * Returns the last binding expression of the name.
+   */
+  ObjectType getObject(const std::string name) throw () {
+    ObjectType result;
+    table_iterator find = d_name_bindings.find(name);
+    if(find != d_name_bindings.end())
+      result = find->second.top();
+    return result;
+  }
 
-    /**
-     * Returns true is name is bound to an expression.
-     */
-    bool isBound(const std::string name) const throw () {
-      const_table_iterator find = d_name_bindings.find(name);
-      return (find != d_name_bindings.end());
-    }
-  };
+  /**
+   * Returns true is name is bound to an expression.
+   */
+  bool isBound(const std::string name) const throw () {
+    const_table_iterator find = d_name_bindings.find(name);
+    return (find != d_name_bindings.end());
+  }
+};
 
 }/* CVC4::parser namespace */
 }/* CVC4 namespace */
+
+#endif /* __CVC4__PARSER__SYMBOL_TABLE_H */