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

3 files changed, 24 insertions, 7 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
diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp
index c9754765..66793b13 100644
--- a/lib/Expr/Expr.cpp
+++ b/lib/Expr/Expr.cpp
@@ -80,9 +80,19 @@ ref<Expr> Expr::createTempRead(const Array *array, Expr::Width w) {
 }
 
 // returns 0 if b is structurally equal to *this
-int Expr::compare(const Expr &b) const {
+int Expr::compare(const Expr &b, ExprEquivSet &equivs) const {
   if (this == &b) return 0;
 
+  const Expr *ap, *bp;
+  if (this < &b) {
+    ap = this; bp = &b;
+  } else {
+    ap = &b; bp = this;
+  }
+
+  if (equivs.count(std::make_pair(ap, bp)))
+    return 0;
+
   Kind ak = getKind(), bk = b.getKind();
   if (ak!=bk)
     return (ak < bk) ? -1 : 1;
@@ -95,9 +105,10 @@ int Expr::compare(const Expr &b) const {
 
   unsigned aN = getNumKids();
   for (unsigned i=0; i<aN; i++)
-    if (int res = getKid(i).compare(b.getKid(i)))
+    if (int res = getKid(i)->compare(*b.getKid(i), equivs))
       return res;
 
+  equivs.insert(std::make_pair(ap, bp));
   return 0;
 }
 
diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp
index 090d027a..70f3cab2 100644
--- a/lib/Solver/IndependentSolver.cpp
+++ b/lib/Solver/IndependentSolver.cpp
@@ -77,13 +77,13 @@ public:
 };
 
 template<class T>
-inline std::ostream &operator<<(std::ostream &os, const DenseSet<T> &dis) {
+inline std::ostream &operator<<(std::ostream &os, const ::DenseSet<T> &dis) {
   dis.print(os);
   return os;
 }
 
 class IndependentElementSet {
-  typedef std::map<const Array*, DenseSet<unsigned> > elements_ty;
+  typedef std::map<const Array*, ::DenseSet<unsigned> > elements_ty;
   elements_ty elements;
   std::set<const Array*> wholeObjects;
 
@@ -103,7 +103,7 @@ public:
 
       if (!wholeObjects.count(array)) {
         if (ConstantExpr *CE = dyn_cast<ConstantExpr>(re->index)) {
-          DenseSet<unsigned> &dis = elements[array];
+          ::DenseSet<unsigned> &dis = elements[array];
           dis.add((unsigned) CE->getZExtValue(32));
         } else {
           elements_ty::iterator it2 = elements.find(array);
@@ -142,7 +142,7 @@ public:
     for (elements_ty::const_iterator it = elements.begin(), ie = elements.end();
          it != ie; ++it) {
       const Array *array = it->first;
-      const DenseSet<unsigned> &dis = it->second;
+      const ::DenseSet<unsigned> &dis = it->second;
 
       if (first) {
         first = false;