Big chunk of changes:

* Fixed bugs in option parsing
* Simplified the main.cpp significantly (more c++ like)
* Added the null kind, expr value, and expression, with the default constructor public
* Simplified commands, we need to discuss this in the meeting (what to do with command results?)
* Removed all the lex/yacc files
* Symbol table is now a templated class, as we will have tables for variables, predicates and functions
* The ANTLR parsing infrastructure/makefiles is all in. SMT lib Boolean benchmarks should parse + giving nice error such as 
      Parse Error: /home/dejan/eclipse-cxx/smtlib-parser/test/test4.smt:3:16: Undeclared variable p
      Parse Error: /home/dejan/eclipse-cxx/smtlib-parser/test/test2.smt:2:11: unexpected token: sa
      
Didn't add any unit tests as the unit testing doesn't work with the updated build system -- it doesn't know how to create directories in the corresponding build directory.

TODO: 
 * add the PL grammar and unit test when the testing becomes available
 * with this build setup my eclipse debugger doesn't work.  Might have something to do with the visibility of symbols?
 * i'm getting g++ depracated warnings regarding the hash_map from the symbol table, need to figure out how to use it in a standard manner. the new <unordered_map> header is for C++0x, and the <ext/hash_map> is getting deprecation warningns... weird.

1 files changed, 72 insertions, 13 deletions

diff --git a/src/parser/symbol_table.h b/src/parser/symbol_table.h
index 9135343f5..3b08aa5f5 100644
--- a/src/parser/symbol_table.h
+++ b/src/parser/symbol_table.h
@@ -10,25 +10,84 @@
  **/
 
 #include <string>
-#include <list>
-#include <vector>
+#include <stack>
+#include <ext/hash_map>
 
 #include "expr/expr.h"
 
+namespace __gnu_cxx {
+template<>
+  struct hash<std::string> {
+    size_t operator()(const std::string& str) const {
+      return hash<const char*> ()(str.c_str());
+    }
+  };
+}
+
 namespace CVC4 {
 namespace parser {
 
-class SymbolTable {
-public:
-  // FIXME: No definitions for Type yet
-  // void defineType(const std::string&, const Type&);
-  void defineVar(const std::string, const void*) throw();
-  void defineVarList(const std::list<std::string>*, const void*) throw();
-  void defineVarList(const std::vector<std::string>*, const void*) throw();
-
-  // Type& lookupType(const std::string&);
-  Expr& lookupVar(const std::string*) throw();
-};
+/**
+ * Generic symbol table for looking up variables by name.
+ */
+template<typename ObjectType>
+  class SymbolTable {
+
+  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;
+
+    /** Bindings for the names */
+    LookupTable d_name_bindings;
+
+  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);
+    }
+
+    /**
+     * 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 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 */