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, 26 insertions, 8 deletions

diff --git a/src/parser/antlr_parser.cpp b/src/parser/antlr_parser.cpp
index c1cd85731..c4e6eef19 100644
--- a/src/parser/antlr_parser.cpp
+++ b/src/parser/antlr_parser.cpp
@@ -5,6 +5,8 @@
  *      Author: dejan
  */
 
+#include <iostream>
+
 #include "antlr_parser.h"
 #include "expr/expr_manager.h"
 
@@ -24,7 +26,8 @@ ostream& operator <<(ostream& out, AntlrParser::BenchmarkStatus status) {
     out << "unknown";
     break;
   default:
-    CVC4::UnhandledImpl("Unhandled ostream case for AntlrParser::BenchmarkStatus");
+    CVC4::UnhandledImpl(
+        "Unhandled ostream case for AntlrParser::BenchmarkStatus");
   }
   return out;
 }
@@ -42,8 +45,7 @@ AntlrParser::AntlrParser(antlr::TokenStream& lexer, int k) :
 }
 
 Expr AntlrParser::getVariable(std::string var_name) {
-  cout << "getVariable(" << var_name << ")" << endl;
-  return d_expr_manager->mkExpr(VARIABLE);
+  return d_var_symbol_table.getObject(var_name);
 }
 
 Expr AntlrParser::getTrueExpr() const {
@@ -55,21 +57,37 @@ Expr AntlrParser::getFalseExpr() const {
 }
 
 Expr AntlrParser::newExpression(Kind kind, const std::vector<Expr>& children) {
-  cout << "newExpression(" << kind << ", " << children.size()
-      << ")" << endl;
   return d_expr_manager->mkExpr(kind, children);
 }
 
 void AntlrParser::newPredicate(std::string p_name,
     std::vector<std::string>& p_sorts) {
-  cout << "newPredicate(" << p_name << ", " << p_sorts.size() << ")" << endl;
+  if(p_sorts.size() == 0)
+    d_var_symbol_table.bindName(p_name, d_expr_manager->mkExpr(VARIABLE));
+  else
+    Unhandled("Non unary predicate not supported yet!");
 }
 
 void AntlrParser::setBenchmarkStatus(BenchmarkStatus status) {
-  cout << "setBenchmarkStatus()" << endl;
   d_benchmark_status = status;
 }
 
 void AntlrParser::addExtraSorts(std::vector<std::string>& extra_sorts) {
-  cout << "addExtraSorts()" << endl;
+}
+
+void AntlrParser::setExpressionManager(ExprManager* em) {
+  d_expr_manager = em;
+}
+
+bool AntlrParser::isDeclared(string name, SymbolType type) {
+  switch(type) {
+  case SYM_VARIABLE:
+    return d_var_symbol_table.isBound(name);
+  default:
+    Unhandled("Unhandled symbol type!");
+  }
+}
+
+void AntlrParser::rethrow(antlr::SemanticException& e, string new_message) throw(antlr::SemanticException) {
+  throw antlr::SemanticException(new_message, getFilename(), LT(0).get()->getLine(), LT(0).get()->getColumn());
 }