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

2 files changed, 17 insertions, 6 deletions

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;