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.

3 files changed, 74 insertions, 54 deletions

diff --git a/src/util/command.cpp b/src/util/command.cpp
index 9e541574a..e38695b46 100644
--- a/src/util/command.cpp
+++ b/src/util/command.cpp
@@ -7,71 +7,99 @@
 
 #include "util/command.h"
 #include "smt/smt_engine.h"
+#include "expr/expr.h"
 #include "util/result.h"
 
+namespace std {
+ostream& operator<<(ostream& out, const CVC4::Command& c) {
+  c.toString(out);
+  return out;
+}
+}
+
 namespace CVC4 {
 
 EmptyCommand::EmptyCommand() {
 }
 
-Result EmptyCommand::invoke(SmtEngine* smt_engine) {
-  return Result::VALIDITY_UNKNOWN;
+void EmptyCommand::invoke(SmtEngine* smt_engine) {
 }
 
 AssertCommand::AssertCommand(const Expr& e) :
   d_expr(e) {
 }
 
-Result AssertCommand::invoke(SmtEngine* smt_engine) {
-  return smt_engine->assert(d_expr);
+void AssertCommand::invoke(SmtEngine* smt_engine) {
+  smt_engine->assert(d_expr);
 }
 
-CheckSatCommand::CheckSatCommand() :
-  d_expr(Expr::null()) {
+CheckSatCommand::CheckSatCommand() {
 }
 
 CheckSatCommand::CheckSatCommand(const Expr& e) :
   d_expr(e) {
 }
 
-Result CheckSatCommand::invoke(SmtEngine* smt_engine) {
-  return smt_engine->checkSat(d_expr);
+void CheckSatCommand::invoke(SmtEngine* smt_engine) {
+  smt_engine->checkSat(d_expr);
 }
 
 QueryCommand::QueryCommand(const Expr& e) :
   d_expr(e) {
 }
 
-Result QueryCommand::invoke(CVC4::SmtEngine* smt_engine) {
-  return smt_engine->query(d_expr);
+void QueryCommand::invoke(CVC4::SmtEngine* smt_engine) {
+  smt_engine->query(d_expr);
 }
 
 CommandSequence::CommandSequence() :
   d_last_index(0) {
 }
 
-CommandSequence::CommandSequence(Command* cmd) :
-  d_last_index(0) {
-  addCommand(cmd);
-}
-
-
 CommandSequence::~CommandSequence() {
   for(unsigned i = d_last_index; i < d_command_sequence.size(); ++i)
     delete d_command_sequence[i];
 }
 
-Result CommandSequence::invoke(SmtEngine* smt_engine) {
-  Result r = Result::VALIDITY_UNKNOWN;
+void CommandSequence::invoke(SmtEngine* smt_engine) {
   for(; d_last_index < d_command_sequence.size(); ++d_last_index) {
-    r = d_command_sequence[d_last_index]->invoke(smt_engine);
+    d_command_sequence[d_last_index]->invoke(smt_engine);
     delete d_command_sequence[d_last_index];
   }
-  return r;
 }
 
 void CommandSequence::addCommand(Command* cmd) {
   d_command_sequence.push_back(cmd);
 }
 
+// Printout methods
+
+using namespace std;
+
+void EmptyCommand::toString(ostream& out) const {
+  out << "EmptyCommand";
+}
+
+void AssertCommand::toString(ostream& out) const {
+  out << "Assert(" << d_expr << ")";
+}
+
+void CheckSatCommand::toString(ostream& out) const {
+  if(d_expr.isNull())
+    out << "CheckSat()";
+  else
+    out << "CheckSat(" << d_expr << ")";
+}
+
+void QueryCommand::toString(ostream& out) const {
+  out << "Query(" << d_expr << ")";
+}
+
+void CommandSequence::toString(ostream& out) const {
+  out << "CommandSequence[" << endl;
+  for(unsigned i = d_last_index; i < d_command_sequence.size(); ++i)
+    out << *d_command_sequence[i] << endl;
+  out << "]";
+}
+
 }/* CVC4 namespace */
diff --git a/src/util/command.h b/src/util/command.h
index c65429fdb..ce137896a 100644
--- a/src/util/command.h
+++ b/src/util/command.h
@@ -16,7 +16,6 @@
 
 #include "cvc4_config.h"
 #include "expr/expr.h"
-#include "util/result.h"
 
 namespace CVC4 {
   class SmtEngine;
@@ -25,15 +24,14 @@ namespace CVC4 {
 }/* CVC4 namespace */
 
 namespace std {
-inline std::ostream& operator<<(std::ostream&, const CVC4::Command*) CVC4_PUBLIC;
-inline std::ostream& operator<<(std::ostream&, CVC4::Expr) CVC4_PUBLIC;
+  std::ostream& operator<<(std::ostream&, const CVC4::Command&) CVC4_PUBLIC;
 }
 
 namespace CVC4 {
 
 class CVC4_PUBLIC Command {
 public:
-  virtual Result invoke(CVC4::SmtEngine* smt_engine) = 0;
+  virtual void invoke(CVC4::SmtEngine* smt_engine) = 0;
   virtual ~Command() {};
   virtual void toString(std::ostream&) const = 0;
 };/* class Command */
@@ -41,8 +39,8 @@ public:
 class CVC4_PUBLIC EmptyCommand : public Command {
 public:
   EmptyCommand();
-  Result invoke(CVC4::SmtEngine* smt_engine);
-  void toString(std::ostream& out) const { out << "EmptyCommand"; }
+  void invoke(CVC4::SmtEngine* smt_engine);
+  void toString(std::ostream& out) const;
 };/* class EmptyCommand */
 
 
@@ -51,8 +49,8 @@ protected:
   Expr d_expr;
 public:
   AssertCommand(const Expr& e);
-  Result invoke(CVC4::SmtEngine* smt_engine);
-  void toString(std::ostream& out) const { out << "Assert(" << d_expr << ")"; }
+  void invoke(CVC4::SmtEngine* smt_engine);
+  void toString(std::ostream& out) const;
 };/* class AssertCommand */
 
 
@@ -60,8 +58,8 @@ class CVC4_PUBLIC CheckSatCommand : public Command {
 public:
   CheckSatCommand();
   CheckSatCommand(const Expr& e);
-  Result invoke(SmtEngine* smt);
-  void toString(std::ostream& out) const { out << "CheckSat(" << d_expr << ")"; }
+  void invoke(SmtEngine* smt);
+  void toString(std::ostream& out) const;
 protected:
   Expr d_expr;
 };/* class CheckSatCommand */
@@ -70,8 +68,8 @@ protected:
 class CVC4_PUBLIC QueryCommand : public Command {
 public:
   QueryCommand(const Expr& e);
-  Result invoke(SmtEngine* smt);
-  void toString(std::ostream& out) const { out << "Query(" << d_expr << ")"; }
+  void invoke(SmtEngine* smt);
+  void toString(std::ostream& out) const;
 protected:
   Expr d_expr;
 };/* class QueryCommand */
@@ -80,21 +78,10 @@ protected:
 class CVC4_PUBLIC CommandSequence : public Command {
 public:
   CommandSequence();
-  CommandSequence(Command* cmd);
   ~CommandSequence();
-  Result invoke(SmtEngine* smt);
+  void invoke(SmtEngine* smt);
   void addCommand(Command* cmd);
-  void toString(std::ostream& out) const {
-    out << "CommandSequence(";
-    for(std::vector<Command*>::const_iterator i = d_command_sequence.begin();
-        i != d_command_sequence.end();
-        ++i) {
-      out << *i;
-      if(i != d_command_sequence.end())
-        out << " ; ";
-    }
-    out << ")";
-  }
+  void toString(std::ostream& out) const;
 private:
   /** All the commands to be executed (in sequence) */
   std::vector<Command*> d_command_sequence;
@@ -104,11 +91,4 @@ private:
 
 }/* CVC4 namespace */
 
-inline std::ostream& std::operator<<(std::ostream& out, const CVC4::Command* c) {
-  if(c)
-    c->toString(out);
-  else out << "(null)";
-  return out;
-}
-
 #endif /* __CVC4__COMMAND_H */
diff --git a/src/util/options.h b/src/util/options.h
index 54b4e2f9b..8d2d113a2 100644
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -18,6 +18,7 @@
 namespace CVC4 {
 
 struct Options {
+
   std::string binary_name;
 
   bool smtcomp_mode;
@@ -33,7 +34,18 @@ struct Options {
   /* with 3, the solver is slowed down by all the scrolling */
   int verbosity;
 
-  std::string lang;
+  /** The input language option */
+  enum InputLanguage {
+    /** The SMTLIB input language */
+    LANG_SMTLIB,
+    /** The CVC4 input language */
+    LANG_CVC4,
+    /** Auto-detect the language */
+    LANG_AUTO
+  };
+
+  /** The input language */
+  InputLanguage lang;
 
   Options() : binary_name(),
               smtcomp_mode(false),
@@ -41,7 +53,7 @@ struct Options {
               out(0),
               err(0),
               verbosity(0),
-              lang()
+              lang(LANG_AUTO)
   {}
 };/* struct Options */