Maintain an equivalence set during comparison operations

This results in a significant speedup of certain comparisons
involving large partially shared expression trees.

git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@131585 91177308-0d34-0410-b5e6-96231b3b80d8

1 files changed, 7 insertions, 1 deletions

diff --git a/include/klee/Expr.h b/include/klee/Expr.h
index 3f544289..ccbd9163 100644
--- a/include/klee/Expr.h
+++ b/include/klee/Expr.h
@@ -15,6 +15,7 @@
 
 #include "llvm/ADT/APInt.h"
 #include "llvm/ADT/APFloat.h"
+#include "llvm/ADT/DenseSet.h"
 #include "llvm/ADT/SmallVector.h"
 
 #include <set>
@@ -193,7 +194,12 @@ public:
   virtual unsigned computeHash();
   
   /// Returns 0 iff b is structuraly equivalent to *this
-  int compare(const Expr &b) const;
+  typedef llvm::DenseSet<std::pair<const Expr *, const Expr *> > ExprEquivSet;
+  int compare(const Expr &b, ExprEquivSet &equivs) const;
+  int compare(const Expr &b) const {
+    ExprEquivSet equivs;
+    return compare(b, equivs);
+  }
   virtual int compareContents(const Expr &b) const { return 0; }
 
   // Given an array of new kids return a copy of the expression