3 files changed, 76 insertions, 0 deletions

diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index c3191ab48..fc67bcba1 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -138,6 +138,16 @@ bool Expr::operator<(const Expr& e) const {
   return *d_node < *e.d_node;
 }
 
+bool Expr::operator>(const Expr& e) const {
+  Assert(d_node != NULL, "Unexpected NULL expression pointer!");
+  Assert(e.d_node != NULL, "Unexpected NULL expression pointer!");
+  if(isNull() && !e.isNull()) {
+    return true;
+  }
+  ExprManagerScope ems(*this);
+  return *d_node > *e.d_node;
+}
+
 Kind Expr::getKind() const {
   ExprManagerScope ems(*this);
   Assert(d_node != NULL, "Unexpected NULL expression pointer!");
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index 34d4a1a9e..517931477 100644
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -160,6 +160,39 @@ public:
   bool operator<(const Expr& e) const;
 
   /**
+   * Order comparison operator. The only invariant on the order of expressions
+   * is that the expressions that were created sooner will be smaller in the
+   * ordering than all the expressions created later. Null expression is the
+   * smallest element of the ordering. The behavior of the operator is
+   * undefined if the expressions come from two different expression managers.
+   * @param e the expression to compare to
+   * @return true if this expression is greater than the given one
+   */
+  bool operator>(const Expr& e) const;
+
+  /**
+   * Order comparison operator. The only invariant on the order of expressions
+   * is that the expressions that were created sooner will be smaller in the
+   * ordering than all the expressions created later. Null expression is the
+   * smallest element of the ordering. The behavior of the operator is
+   * undefined if the expressions come from two different expression managers.
+   * @param e the expression to compare to
+   * @return true if this expression is smaller or equal to the given one
+   */
+  bool operator<=(const Expr& e) const { return !(*this > e); }
+
+  /**
+   * Order comparison operator. The only invariant on the order of expressions
+   * is that the expressions that were created sooner will be smaller in the
+   * ordering than all the expressions created later. Null expression is the
+   * smallest element of the ordering. The behavior of the operator is
+   * undefined if the expressions come from two different expression managers.
+   * @param e the expression to compare to
+   * @return true if this expression is greater or equal to the given one
+   */
+  bool operator>=(const Expr& e) const { return !(*this < e); }
+
+  /**
    * Returns the kind of the expression (AND, PLUS ...).
    * @return the kind of the expression
    */
diff --git a/src/expr/node.h b/src/expr/node.h
index 09a1ad8bc..218b9a3ea 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -245,6 +245,39 @@ public:
   }
 
   /**
+   * We compare by expression ids so, keeping things deterministic and having
+   * that subexpressions have to be smaller than the enclosing expressions.
+   * @param node the node to compare to
+   * @return true if this expression is greater
+   */
+  template <bool ref_count_1>
+  inline bool operator>(const NodeTemplate<ref_count_1>& node) const {
+    return d_nv->d_id > node.d_nv->d_id;
+  }
+
+  /**
+   * We compare by expression ids so, keeping things deterministic and having
+   * that subexpressions have to be smaller than the enclosing expressions.
+   * @param node the node to compare to
+   * @return true if this expression is smaller than or equal to
+   */
+  template <bool ref_count_1>
+  inline bool operator<=(const NodeTemplate<ref_count_1>& node) const {
+    return d_nv->d_id <= node.d_nv->d_id;
+  }
+
+  /**
+   * We compare by expression ids so, keeping things deterministic and having
+   * that subexpressions have to be smaller than the enclosing expressions.
+   * @param node the node to compare to
+   * @return true if this expression is greater than or equal to
+   */
+  template <bool ref_count_1>
+  inline bool operator>=(const NodeTemplate<ref_count_1>& node) const {
+    return d_nv->d_id >= node.d_nv->d_id;
+  }
+
+  /**
    * Returns the i-th child of this node.
    * @param i the index of the child
    * @return the node representing the i-th child