From 08d4716e7882be14d3b2d466d0fa8a58d087523d Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Mon, 28 Nov 2016 10:57:12 +0000 Subject: Clean up `Expr::compare()` interface by * Making `Expr::compre(const Expr&, ExprEquivSet)` private and moving its implementation into `Expr.cpp`. * Document `Expr::compare(const Expr&)`. This partially addresses #515 . --- include/klee/Expr.h | 29 ++++++++++++++++++----------- 1 file changed, 18 insertions(+), 11 deletions(-) (limited to 'include') diff --git a/include/klee/Expr.h b/include/klee/Expr.h index 26c91ae3..4584ab0d 100644 --- a/include/klee/Expr.h +++ b/include/klee/Expr.h @@ -223,22 +223,25 @@ public: /// Returns the hash value. virtual unsigned computeHash(); - /// Returns 0 iff b is structuraly equivalent to *this - typedef llvm::DenseSet > ExprEquivSet; - int compare(const Expr &b, ExprEquivSet &equivs) const; - int compare(const Expr &b) const { - static ExprEquivSet equivs; - int r = compare(b, equivs); - equivs.clear(); - return r; - } + /// Compares `b` to `this` Expr for structural equivalence. + /// + /// This method effectively defines a total order over all Expr. + /// + /// \param [in] b Expr to compare `this` to. + /// + /// \return One of the following values: + /// + /// * -1 iff `this` is `<` `b` + /// * 0 iff `this` is structurally equivalent to `b` + /// * 1 iff `this` is `>` `b` + /// + /// `<` and `>` are binary relations that express the total order. + int compare(const Expr &b) const; // Given an array of new kids return a copy of the expression // but using those children. virtual ref rebuild(ref kids[/* getNumKids() */]) const = 0; - // - /// isZero - Is this a constant zero. bool isZero() const; @@ -279,6 +282,10 @@ public: static bool needsResultType() { return false; } static bool classof(const Expr *) { return true; } + +private: + typedef llvm::DenseSet > ExprEquivSet; + int compare(const Expr &b, ExprEquivSet &equivs) const; }; struct Expr::CreateArg { -- cgit 1.4.1