From bbaba2f7c94050712802b3ae39d92d727853ffc9 Mon Sep 17 00:00:00 2001 From: Peter Collingbourne Date: Wed, 18 May 2011 21:49:00 +0000 Subject: 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 --- lib/Expr/Expr.cpp | 15 +++++++++++++-- lib/Solver/IndependentSolver.cpp | 8 ++++---- 2 files changed, 17 insertions(+), 6 deletions(-) (limited to 'lib') 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::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; icompare(*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 -inline std::ostream &operator<<(std::ostream &os, const DenseSet &dis) { +inline std::ostream &operator<<(std::ostream &os, const ::DenseSet &dis) { dis.print(os); return os; } class IndependentElementSet { - typedef std::map > elements_ty; + typedef std::map > elements_ty; elements_ty elements; std::set wholeObjects; @@ -103,7 +103,7 @@ public: if (!wholeObjects.count(array)) { if (ConstantExpr *CE = dyn_cast(re->index)) { - DenseSet &dis = elements[array]; + ::DenseSet &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 &dis = it->second; + const ::DenseSet &dis = it->second; if (first) { first = false; -- cgit 1.4.1