fixes and additions

8 files changed, 82 insertions, 122 deletions

diff --git a/src/include/debug.h b/src/include/debug.h
new file mode 100644
index 000000000..95e705bcb
--- /dev/null
+++ b/src/include/debug.h
@@ -0,0 +1,24 @@
+/*********************                                           -*- C++ -*-  */
+/** debug.h
+ ** This file is part of the CVC4 prototype.
+ **
+ ** The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ **/
+
+#ifndef __CVC4_DEBUG_H
+#define __CVC4_DEBUG_H
+
+#include <cassert>
+
+#ifdef DEBUG
+// the __builtin_expect() helps us if assert is built-in or a macro
+# define cvc4assert(x) assert(__builtin_expect((x), 1))
+#else
+// TODO: use a compiler annotation when assertions are off ?
+// (to improve optimization)
+# define cvc4assert(x)
+#endif /* DEBUG */
+
+#endif /* __CVC4_DEBUG_H */
diff --git a/src/include/exception.h b/src/include/exception.h
index 3502fdf0c..ce19b0d68 100644
--- a/src/include/exception.h
+++ b/src/include/exception.h
@@ -10,7 +10,7 @@
  **/
 
 #ifndef __CVC4_EXCEPTION_H
-#ifndef __CVC4_EXCEPTION_H
+#define __CVC4_EXCEPTION_H
 
 #include <string>
 #include <iostream>
diff --git a/src/include/expr.h b/src/include/expr.h
index 5e3559fd7..9ca449ce7 100644
--- a/src/include/expr.h
+++ b/src/include/expr.h
@@ -12,6 +12,9 @@
 #ifndef __CVC4_EXPR_H
 #define __CVC4_EXPR_H
 
+#include <vector>
+#include <stdint.h>
+
 namespace CVC4 {
 
 class ExprValue;
@@ -34,19 +37,39 @@ class Expr {
    *  Increments the reference count. */
   explicit Expr(ExprValue*);
 
+public:
+  Expr(const Expr&);
+
   /** Destructor.  Decrements the reference count and, if zero,
    *  collects the ExprValue. */
   ~Expr();
 
-public:
+  Expr& operator=(const Expr&);
+
   /** Access to the encapsulated expression.
    *  @return the encapsulated expression. */
   ExprValue* operator->();
 
-  /** Const access to the encapsulated expressoin.
+  /** Const access to the encapsulated expression.
    *  @return the encapsulated expression [const]. */
   const ExprValue* operator->() const;
 
+  uint64_t hash() const;
+
+  Expr eqExpr(const Expr& right) const;
+  Expr notExpr() const;
+  Expr negate() const; // avoid double-negatives
+  Expr andExpr(const Expr& right) const;
+  Expr orExpr(const Expr& right) const;
+  Expr iteExpr(const Expr& thenpart, const Expr& elsepart) const;
+  Expr iffExpr(const Expr& right) const;
+  Expr impExpr(const Expr& right) const;
+  Expr xorExpr(const Expr& right) const;
+  Expr skolemExpr(int i) const;
+  Expr substExpr(const std::vector<Expr>& oldTerms,
+                 const std::vector<Expr>& newTerms) const;
+
+  static Expr null() { return s_null; }
 };/* class Expr */
 
 } /* CVC4 namespace */
diff --git a/src/include/expr_builder.h b/src/include/expr_builder.h
index 59503aa4f..342834e37 100644
--- a/src/include/expr_builder.h
+++ b/src/include/expr_builder.h
@@ -43,6 +43,10 @@ class ExprBuilder {
 
 public:
 
+  ExprBuilder();
+  ExprBuilder(const Expr&);
+  ExprBuilder(const ExprBuilder&);
+
   // Compound expression constructors
   ExprBuilder& eqExpr(const Expr& right);
   ExprBuilder& notExpr();
diff --git a/src/include/expr_manager.h b/src/include/expr_manager.h
index 0c265f57f..5dae5b854 100644
--- a/src/include/expr_manager.h
+++ b/src/include/expr_manager.h
@@ -23,47 +23,29 @@ public:
   static ExprManager* currentEM() { return s_current; }
 
   // general expression-builders
-  Expr build(Kind kind);
-  Expr build(Kind kind, Expr child1);
-  Expr build(Kind kind, Expr child1, Expr child2);
-  Expr build(Kind kind, Expr child1, Expr child2, Expr child3);
-  Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4);
-  Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5);
-  Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5, Expr child6);
-  Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5, Expr child6, Expr child7);
-  Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5, Expr child6, Expr child7, Expr child8);
-  Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5, Expr child6, Expr child7, Expr child8, Expr child9);
-  Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5, Expr child6, Expr child7, Expr child8, Expr child9, Expr child10);
+  Expr mkExpr(Kind kind);
+  Expr mkExpr(Kind kind, Expr child1);
+  Expr mkExpr(Kind kind, Expr child1, Expr child2);
+  Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3);
+  Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4);
+  Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5);
   // N-ary version
-  Expr build(Kind kind, std::vector<Expr> children);
+  Expr mkExpr(Kind kind, std::vector<Expr> children);
 
   // TODO: these use the current EM (but must be renamed)
   /*
-  static Expr build(Kind kind)
-  { currentEM()->build(kind); }
-  static Expr build(Kind kind, Expr child1);
-  { currentEM()->build(kind, child1); }
-  static Expr build(Kind kind, Expr child1, Expr child2);
-  { currentEM()->build(kind, child1, child2); }
-  static Expr build(Kind kind, Expr child1, Expr child2, Expr child3);
-  { currentEM()->build(kind, child1, child2, child3); }
-  static Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4);
-  { currentEM()->build(kind, child1, child2, child3, child4); }
-  static Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5);
-  { currentEM()->build(kind, child1, child2, child3, child4, child5); }
-  static Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5, Expr child6);
-  { currentEM()->build(kind, child1, child2, child3, child4, child5, child6); }
-  static Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5, Expr child6, Expr child7);
-  { currentEM()->build(kind, child1, child2, child3, child4, child5, child6, child7); }
-  static Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5, Expr child6, Expr child7, Expr child8);
-  { currentEM()->build(kind, child1, child2, child3, child4, child5, child6, child7, child8); }
-  static Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5, Expr child6, Expr child7, Expr child8, Expr child9);
-  { currentEM()->build(kind, child1, child2, child3, child4, child5, child6, child7, child8, child9); }
-  static Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5, Expr child6, Expr child7, Expr child8, Expr child9, Expr child10);
-  { currentEM()->build(kind, child1, child2, child3, child4, child5, child6, child7, child8, child9, child10); }
-  // N-ary version
-  static Expr build(Kind kind, vector<Expr> children)
-  { currentEM()->build(kind, children); }
+  static Expr mkExpr(Kind kind)
+  { currentEM()->mkExpr(kind); }
+  static Expr mkExpr(Kind kind, Expr child1);
+  { currentEM()->mkExpr(kind, child1); }
+  static Expr mkExpr(Kind kind, Expr child1, Expr child2);
+  { currentEM()->mkExpr(kind, child1, child2); }
+  static Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3);
+  { currentEM()->mkExpr(kind, child1, child2, child3); }
+  static Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4);
+  { currentEM()->mkExpr(kind, child1, child2, child3, child4); }
+  static Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5);
+  { currentEM()->mkExpr(kind, child1, child2, child3, child4, child5); }
   */
 
   // do we want a varargs one?  perhaps not..
diff --git a/src/include/expr_value.h b/src/include/expr_value.h
index ca12b8e03..c15241ebf 100644
--- a/src/include/expr_value.h
+++ b/src/include/expr_value.h
@@ -16,6 +16,7 @@
 #ifndef __CVC4_EXPR_VALUE_H
 #define __CVC4_EXPR_VALUE_H
 
+#include <stdint.h>
 #include "expr.h"
 
 namespace CVC4 {
@@ -41,14 +42,12 @@ class ExprValue {
   /** Variable number of child nodes */
   Expr     d_children[0];
 
+  friend class Expr;
+
 public:
   /** Hash this expression.
    *  @return the hash value of this expression. */
-  unsigned hash() const;
-
-  /** Convert to (wrap in) an Expr.
-   *  @return an Expr pointing to this expression. */
-  operator Expr();
+  uint64_t hash() const;
 
   // Iterator support
 
diff --git a/src/include/kind.h b/src/include/kind.h
index 9307cc677..a015a6b71 100644
--- a/src/include/kind.h
+++ b/src/include/kind.h
@@ -22,7 +22,11 @@ enum Kind {
   XOR,
   NOT,
   PLUS,
-  MINUS
+  MINUS,
+  ITE,
+  IFF,
+  SKOLEM,
+  SUBST
 };/* enum Kind */
 
 }/* CVC4 namespace */
diff --git a/src/include/parser_temp.h b/src/include/parser_temp.h
deleted file mode 100644
index d64a770e4..000000000
--- a/src/include/parser_temp.h
+++ /dev/null
@@ -1,76 +0,0 @@
-/*********************                                           -*- C++ -*-  */
-/** parser_temp.h
- ** This file is part of the CVC4 prototype.
- **
- ** A temporary holder for data used with the parser.
- **
- ** The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- **/
-
-#ifndef __CVC4_PARSER_TEMP_H
-#define __CVC4_PARSER_TEMP_H
-
-#include <iostream>
-
-#include "expr.h"
-#include "exception.h"
-
-namespace CVC4 {
-
-  class ValidityChecker;
-
-  class ParserTemp {
-  private:
-    // Counter for uniqueID of bound variables
-    int d_uid;
-    // The main prompt when running interactive
-    std::string prompt1;
-    // The interactive prompt in the middle of a multi-line command
-    std::string prompt2;
-    // The currently used prompt
-    std::string prompt;
-  public:
-    ValidityChecker* vc;
-    std::istream* is;
-    // The current input line
-    int lineNum;
-    // File name
-    std::string fileName;
-    // The last parsed Expr
-    Expr expr;
-    // Whether we are done or not
-    bool done;
-    // Whether we are running interactive
-    bool interactive;
-    // Whether arrays are enabled for smt-lib format
-    bool arrFlag;
-    // Whether bit-vectors are enabled for smt-lib format
-    bool bvFlag;
-    // Size of bit-vectors for smt-lib format
-    int bvSize;
-    // Did we encounter a formula query (smtlib)
-    bool queryParsed;
-    // Default constructor
-    ParserTemp() : d_uid(0), prompt1("CVC> "), prompt2("- "),
-      prompt("CVC> "), lineNum(1), done(false), arrFlag(false), queryParsed(false) { }
-    // Parser error handling (implemented in parser.cpp)
-    int error(const std::string& s);
-    // Get the next uniqueID as a string
-    std::string uniqueID() {
-      std::ostringstream ss;
-      ss << d_uid++;
-      return ss.str();
-    }
-    // Get the current prompt
-    std::string getPrompt() { return prompt; }
-    // Set the prompt to the main one
-    void setPrompt1() { prompt = prompt1; }
-    // Set the prompt to the secondary one
-    void setPrompt2() { prompt = prompt2; }
-  };
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4_PARSER_TEMP_H */