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, 13 insertions, 2 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;
 }