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

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. */