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.

5 files changed, 35 insertions, 3 deletions

diff --git a/src/expr/expr.cpp b/src/expr/expr.cpp
index 2e3d7a7e2..e88189bcc 100644
--- a/src/expr/expr.cpp
+++ b/src/expr/expr.cpp
@@ -18,7 +18,18 @@ using namespace CVC4::expr;
 
 namespace CVC4 {
 
-Expr Expr::s_null(0);
+ExprValue ExprValue::s_null;
+
+Expr Expr::s_null(&ExprValue::s_null);
+
+bool Expr::isNull() const {
+  return d_ev == &ExprValue::s_null;
+}
+
+Expr::Expr() :
+  d_ev(&ExprValue::s_null) {
+  // No refcount needed
+}
 
 Expr::Expr(ExprValue* ev)
   : d_ev(ev) {
diff --git a/src/expr/expr.h b/src/expr/expr.h
index 5a11e0fbd..0fcb5ea6a 100644
--- a/src/expr/expr.h
+++ b/src/expr/expr.h
@@ -60,6 +60,10 @@ class CVC4_PUBLIC Expr {
   friend class ExprManager;
 
 public:
+
+  /** Default constructor, makes a null expression. */
+  CVC4_PUBLIC Expr();
+
   CVC4_PUBLIC Expr(const Expr&);
 
   /** Destructor.  Decrements the reference count and, if zero,
@@ -103,6 +107,9 @@ public:
   inline iterator end() const;
 
   void toString(std::ostream&) const;
+
+  bool isNull() const;
+
 };/* class Expr */
 
 }/* CVC4 namespace */
diff --git a/src/expr/expr_value.cpp b/src/expr/expr_value.cpp
index e24bb88b1..c511c580a 100644
--- a/src/expr/expr_value.cpp
+++ b/src/expr/expr_value.cpp
@@ -18,7 +18,11 @@
 
 namespace CVC4 {
 
-size_t ExprValue::next_id = 0;
+ExprValue::ExprValue() :
+  d_id(0), d_rc(MAX_RC), d_kind(NULL_EXPR), d_nchildren(0) {
+}
+
+size_t ExprValue::next_id = 1;
 
 uint64_t ExprValue::hash() const {
   uint64_t hash = d_kind;
diff --git a/src/expr/expr_value.h b/src/expr/expr_value.h
index decd57045..6df7ad76f 100644
--- a/src/expr/expr_value.h
+++ b/src/expr/expr_value.h
@@ -34,13 +34,17 @@ namespace expr {
  * This is an ExprValue.
  */
 class ExprValue {
+
+  /** A convenient null-valued expression value */
+  static ExprValue s_null;
+
   /** Maximum reference count possible.  Used for sticky
    *  reference-counting.  Should be (1 << num_bits(d_rc)) - 1 */
   static const unsigned MAX_RC = 255;
 
   // this header fits into one 64-bit word
 
-  /** The ID */
+  /** The ID (0 is reserved for the null value) */
   unsigned d_id        : 32;
 
   /** The expression's reference count.  @see cvc4::Expr. */
@@ -65,6 +69,9 @@ class ExprValue {
 
   static size_t next_id;
 
+  /** Private default constructor for the null value. */
+  ExprValue();
+
 public:
   /** Hash this expression.
    *  @return the hash value of this expression. */
diff --git a/src/expr/kind.h b/src/expr/kind.h
index 790fd644d..49321b47f 100644
--- a/src/expr/kind.h
+++ b/src/expr/kind.h
@@ -23,6 +23,8 @@ namespace CVC4 {
 enum Kind {
   /* undefined */
   UNDEFINED_KIND = -1,
+  /** Null Kind */
+  NULL_EXPR,
 
   /* built-ins */
   EQUAL,
@@ -57,6 +59,7 @@ inline std::ostream& operator<<(std::ostream& out, const CVC4::Kind& k) {
 
   switch(k) {
   case UNDEFINED_KIND: out << "UNDEFINED_KIND"; break;
+  case NULL_EXPR:      out << "NULL";           break;
   case EQUAL:          out << "EQUAL";          break;
   case ITE:            out << "ITE";            break;
   case SKOLEM:         out << "SKOLEM";         break;