1 files changed, 35 insertions, 10 deletions

diff --git a/proofs/lfsc_checker/expr.h b/proofs/lfsc_checker/expr.h
index a461e847c..632aaa18a 100644
--- a/proofs/lfsc_checker/expr.h
+++ b/proofs/lfsc_checker/expr.h
@@ -1,12 +1,14 @@
 #ifndef sc2__expr_h
 #define sc2__expr_h
 
-#include "gmp.h"
-#include <string>
-#include <vector>
+#include <stdint.h>
+#include <ext/hash_set>
 #include <iostream>
 #include <map>
+#include <string>
+#include <vector>
 #include "chunking_memory_management.h"
+#include "gmp.h"
 
 #define USE_FLAT_APP  //AJR: off deprecated
 #define MARKVAR_32
@@ -52,8 +54,25 @@ enum { NOT_CEXPR = 0, // for INT_EXPR, HOLE_EXPR, SYM_EXPR, SYMS_EXPR
        COMPARE
 };
 
+class Expr;
 class SymExpr;
 
+namespace __gnu_cxx {
+template <>
+struct hash<Expr *> {
+  size_t operator()(const Expr *x) const {
+    return reinterpret_cast<uintptr_t>(x);
+  }
+};
+}
+
+struct eqExprPtr {
+  bool operator()(const Expr *e1, const Expr *e2) const { return e1 == e2; }
+};
+
+typedef __gnu_cxx::hash_set<Expr *, __gnu_cxx::hash<Expr *>, eqExprPtr>
+    expr_ptr_set_t;
+
 class Expr {
 protected:
   /* bits 0-2: Expr class
@@ -62,8 +81,6 @@ protected:
      bits 9-31: ref count*/
   int data;
 
-  void destroy(bool dec_kids);
-
   enum { INC, DEC, CREATE };
   void debugrefcnt(int ref, int what) {
     std::cout << "[";
@@ -88,6 +105,8 @@ protected:
     : data(1 << 9 /* refcount 1, not cloned */| (_op << 3) | _class)
   { }
 
+  bool _free_in(Expr *x, expr_ptr_set_t *visited);
+
  public:
   virtual ~Expr() {}
 
@@ -138,6 +157,9 @@ protected:
   inline bool isArithTerm() const {
     return getop() == ADD || getop() == NEG;
   }
+  inline bool isSymbolic() const {
+    return getclass() == SYM_EXPR || getclass() == SYMS_EXPR;
+  }
 
   static Expr *build_app(Expr *hd, const std::vector<Expr *> &args, 
 			 int start = 0);
@@ -149,9 +171,9 @@ protected:
      otherwise not. */
   Expr *collect_args(std::vector<Expr *> &args, bool follow_defs = true);
 
-  Expr *get_head(bool follow_defs = true);
+  Expr *get_head(bool follow_defs = true) const;
 
-  Expr *get_body(int op = PI, bool follow_defs = true);
+  Expr *get_body(int op = PI, bool follow_defs = true) const;
 
   std::string toString();
 
@@ -167,11 +189,14 @@ protected:
   /* return a clone of this expr.  All abstractions are really duplicated
      in memory.  Other expressions may not actually be duplicated in
      memory, but their refcounts will be incremented. */
-  Expr *clone(); 
+  Expr *clone();
 
   // x can be a SymExpr or a HoleExpr.
-  bool free_in(Expr *x);
-  bool get_free_in() { return data & 256; }
+  bool free_in(Expr *x) {
+    expr_ptr_set_t visited;
+    return _free_in(x, &visited);
+  }
+  bool get_free_in() const { return data & 256; }
   void calc_free_in();
 
   static int cargCount;