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 .

2 files changed, 25 insertions, 11 deletions

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<std::pair<const Expr *, const Expr *> > 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<Expr> rebuild(ref<Expr> 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<std::pair<const Expr *, const Expr *> > ExprEquivSet;
+  int compare(const Expr &b, ExprEquivSet &equivs) const;
 };
 
 struct Expr::CreateArg {
diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp
index 182093b9..15f52184 100644
--- a/lib/Expr/Expr.cpp
+++ b/lib/Expr/Expr.cpp
@@ -83,6 +83,13 @@ ref<Expr> Expr::createTempRead(const Array *array, Expr::Width w) {
   }
 }
 
+int Expr::compare(const Expr &b) const {
+  static ExprEquivSet equivs;
+  int r = compare(b, equivs);
+  equivs.clear();
+  return r;
+}
+
 // returns 0 if b is structurally equal to *this
 int Expr::compare(const Expr &b, ExprEquivSet &equivs) const {
   if (this == &b) return 0;