work on propositional layer, expression builder support for large expressions, output classes, and minisat

1 files changed, 9 insertions, 5 deletions

diff --git a/src/expr/expr.h b/src/expr/expr.h
index a16ffee13..013888baa 100644
--- a/src/expr/expr.h
+++ b/src/expr/expr.h
@@ -60,19 +60,23 @@ class CVC4_PUBLIC Expr {
 public:
 
   /** Default constructor, makes a null expression. */
-  CVC4_PUBLIC Expr();
+  Expr();
 
-  CVC4_PUBLIC Expr(const Expr&);
+  Expr(const Expr&);
 
   /** Destructor.  Decrements the reference count and, if zero,
    *  collects the ExprValue. */
-  CVC4_PUBLIC ~Expr();
+  ~Expr();
 
-  Expr& operator=(const Expr&) CVC4_PUBLIC;
+  bool operator==(const Expr& e) const { return d_ev == e.d_ev; }
+  bool operator!=(const Expr& e) const { return d_ev != e.d_ev; }
+  bool operator<(const Expr& e) const { return d_ev < e.d_ev; }// for map key
+
+  Expr& operator=(const Expr&);
 
   /** Access to the encapsulated expression.
    *  @return the encapsulated expression. */
-  ExprValue* operator->() const CVC4_PUBLIC;
+  ExprValue* operator->() const;
 
   uint64_t hash() const;