add >, <=, and >= comparisons for Exprs and Nodes

diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index c3191ab489bf27fceb4deda30c1d71a9c6818c7f..fc67bcba1530561c43c896184eca42a54f54472c 100644 (file)
--- 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 34d4a1a9e2163523f1894c54efb5171b20c053f1..517931477f61d35b3252d5fe8cbbc29de94b7305 100644 (file)
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -159,6 +159,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 09a1ad8bc7a6d57c69f1f7d403145051cbd88bd2..218b9a3ea3a932afc11a5fb633e424bf55621eb8 100644 (file)
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -244,6 +244,39 @@ public:
     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
+   */
+  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