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, 13 insertions, 15 deletions

diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp
index f60dd6e24..2daead11b 100644
--- a/src/main/getopt.cpp
+++ b/src/main/getopt.cpp
@@ -25,11 +25,9 @@
 #include "util/exception.h"
 #include "usage.h"
 #include "about.h"
-#include "parser/language.h"
 
 using namespace std;
 using namespace CVC4;
-using namespace CVC4::parser;
 
 namespace CVC4 {
 namespace main {
@@ -58,7 +56,7 @@ static struct option cmdlineOptions[] = {
   { "stats"  , no_argument      , NULL, STATS   }
 };
 
-int parseOptions(int argc, char** argv, CVC4::Options* opts) throw(Exception*) {
+int parseOptions(int argc, char** argv, CVC4::Options* opts) throw(OptionException) {
   const char *progName = argv[0];
   int c;
 
@@ -89,19 +87,19 @@ int parseOptions(int argc, char** argv, CVC4::Options* opts) throw(Exception*) {
       break;
 
     case 'L':
-      if(!strcmp(argv[optind], "cvc4") || !strcmp(argv[optind], "pl")) {
-        opts->lang = PL;
+      if(!strcmp(optarg, "cvc4") || !strcmp(optarg, "pl")) {
+        opts->lang = Options::LANG_CVC4;
         break;
-      } else if(!strcmp(argv[optind], "smtlib") || !strcmp(argv[optind], "smt")) {
-        opts->lang = SMTLIB;
+      } else if(!strcmp(optarg, "smtlib") || !strcmp(optarg, "smt")) {
+        opts->lang = Options::LANG_SMTLIB;
         break;
-      } else if(!strcmp(argv[optind], "auto")) {
-        opts->lang = AUTO;
+      } else if(!strcmp(optarg, "auto")) {
+        opts->lang = Options::LANG_AUTO;
         break;
       }
 
-      if(strcmp(argv[optind], "help"))
-        throw new OptionException(string("unknown language for --lang: `") + argv[optind] + "'.  Try --lang help.");
+      if(strcmp(optarg, "help"))
+        throw OptionException(string("unknown language for --lang: `") + argv[optind] + "'.  Try --lang help.");
 
       fputs(lang_help, stdout);
       exit(1);
@@ -114,17 +112,17 @@ int parseOptions(int argc, char** argv, CVC4::Options* opts) throw(Exception*) {
       // silences CVC4 (except "sat" or "unsat" or "unknown", forces smtlib input)
       opts->smtcomp_mode = true;
       opts->verbosity = -1;
-      opts->lang = SMTLIB;
+      opts->lang = Options::LANG_SMTLIB;
       break;
 
     case '?':
-      throw new OptionException(string("can't understand option: `") + argv[optind] + "'");
+      throw OptionException(string("can't understand option: `") + argv[optind] + "'");
 
     case ':':
-      throw new OptionException(string("option `") + argv[optind] + "' missing its required argument");
+      throw OptionException(string("option `") + argv[optind] + "' missing its required argument");
 
     default:
-      throw new OptionException(string("can't understand option: `") + argv[optind] + "'");
+      throw OptionException(string("can't understand option: `") + argv[optind] + "'");
     }
 
   }