4 files changed, 63 insertions, 21 deletions

diff --git a/src/expr/.gitignore b/src/expr/.gitignore
new file mode 100644
index 000000000..4618e07b0
--- /dev/null
+++ b/src/expr/.gitignore
@@ -0,0 +1,4 @@
+/.deps
+/Makefile.in
+/kind.h
+/metakind.h
diff --git a/src/expr/command.h b/src/expr/command.h
index 3c42c153c..e5994b3c7 100644
--- a/src/expr/command.h
+++ b/src/expr/command.h
@@ -36,6 +36,20 @@ class Command;
 inline std::ostream& operator<<(std::ostream&, const Command&) CVC4_PUBLIC;
 std::ostream& operator<<(std::ostream&, const Command*) CVC4_PUBLIC;
 
+/** The status an SMT benchmark can have */
+enum BenchmarkStatus {
+  /** Benchmark is satisfiable */
+  SMT_SATISFIABLE,
+  /** Benchmark is unsatisfiable */
+  SMT_UNSATISFIABLE,
+  /** The status of the benchmark is unknown */
+  SMT_UNKNOWN
+};
+
+inline std::ostream& operator<<(std::ostream& out,
+                                BenchmarkStatus status)
+  CVC4_PUBLIC;
+
 class CVC4_PUBLIC Command {
 public:
   virtual void invoke(CVC4::SmtEngine* smt_engine) = 0;
@@ -107,15 +121,6 @@ protected:
 
 class CVC4_PUBLIC SetBenchmarkStatusCommand : public Command {
 public:
-  /** The status an SMT benchmark can have */
-  enum BenchmarkStatus {
-    /** Benchmark is satisfiable */
-    SMT_SATISFIABLE,
-    /** Benchmark is unsatisfiable */
-    SMT_UNSATISFIABLE,
-    /** The status of the benchmark is unknown */
-    SMT_UNKNOWN
-  };
   SetBenchmarkStatusCommand(BenchmarkStatus status);
   void invoke(SmtEngine* smt);
   void toStream(std::ostream& out) const;
@@ -123,9 +128,6 @@ protected:
   BenchmarkStatus d_status;
 };/* class SetBenchmarkStatusCommand */
 
-inline std::ostream& operator<<(std::ostream& out,
-                                SetBenchmarkStatusCommand::BenchmarkStatus status)
-  CVC4_PUBLIC;
 
 class CVC4_PUBLIC SetBenchmarkLogicCommand : public Command {
 public:
@@ -288,16 +290,16 @@ inline void SetBenchmarkLogicCommand::toStream(std::ostream& out) const {
 
 /* output stream insertion operator for benchmark statuses */
 inline std::ostream& operator<<(std::ostream& out,
-                                SetBenchmarkStatusCommand::BenchmarkStatus status) {
+                                BenchmarkStatus status) {
   switch(status) {
 
-  case SetBenchmarkStatusCommand::SMT_SATISFIABLE:
+  case SMT_SATISFIABLE:
     return out << "sat";
 
-  case SetBenchmarkStatusCommand::SMT_UNSATISFIABLE:
+  case SMT_UNSATISFIABLE:
     return out << "unsat";
 
-  case SetBenchmarkStatusCommand::SMT_UNKNOWN:
+  case SMT_UNKNOWN:
     return out << "unknown";
 
   default:
diff --git a/src/expr/expr.cpp b/src/expr/expr.cpp
index 5acd0736a..2bcd28422 100644
--- a/src/expr/expr.cpp
+++ b/src/expr/expr.cpp
@@ -40,6 +40,12 @@ Expr::Expr(const Expr& e) :
   d_node(new Node(*e.d_node)), d_exprManager(e.d_exprManager) {
 }
 
+Expr::Expr(uintptr_t n) :
+    d_node(new Node()),
+    d_exprManager(NULL) {
+  AlwaysAssert(n==0);
+}
+
 ExprManager* Expr::getExprManager() const {
   return d_exprManager;
 }
@@ -50,13 +56,26 @@ Expr::~Expr() {
 }
 
 Expr& Expr::operator=(const Expr& e) {
-  if(this != &e) {
-    ExprManagerScope ems(*this);
-    delete d_node;
-    d_node = new Node(*e.d_node);
-    d_exprManager = e.d_exprManager;
+  Assert(d_node != NULL, "Unexpected NULL expression pointer!");
+  Assert(e.d_node != NULL, "Unexpected NULL expression pointer!");
+  ExprManagerScope ems(*this);
+  *d_node = *e.d_node;
+  d_exprManager = e.d_exprManager;
+  return *this;
+}
+
+/* This should only ever be assigning NULL to a null Expr! */
+Expr& Expr::operator=(uintptr_t n) {
+  AlwaysAssert(n==0);
+  Assert(d_node != NULL, "Unexpected NULL expression pointer!");
+  if( EXPECT_FALSE(!isNull()) ) {
+    *d_node = Node::null();
   }
   return *this;
+/*
+  Assert(isNull());
+  return *this;
+*/
 }
 
 bool Expr::operator==(const Expr& e) const {
diff --git a/src/expr/expr.h b/src/expr/expr.h
index c5478b1da..48b64fd17 100644
--- a/src/expr/expr.h
+++ b/src/expr/expr.h
@@ -48,6 +48,14 @@ public:
    */
   Expr(const Expr& e);
 
+  /**
+   * Initialize from an integer. Fails if the integer is not 0.
+   * NOTE: This is here purely to support the auto-initialization
+   * behavior of the ANTLR3 C backend. Should be removed if future
+   * versions of ANTLR fix the problem.
+   */
+  Expr(uintptr_t n);
+
   /** Destructor */
   ~Expr();
 
@@ -61,6 +69,15 @@ public:
   Expr& operator=(const Expr& e);
 
   /**
+   * Assignment from an integer. Fails if the integer is not 0.
+   * NOTE: This is here purely to support the auto-initialization
+   * behavior of the ANTLR3 C backend (i.e., a rule attribute
+   * <code>Expr e</code> gets initialized with <code>e = NULL;</code>.
+   * Should be removed if future versions of ANTLR fix the problem.
+   */
+  Expr& operator=(uintptr_t n);
+
+  /**
    * Syntactic comparison operator. Returns true if expressions belong to the
    * same expression manager and are syntactically identical.
    * @param e the expression to compare to