From 3c1f1a3b65cd416038f365aa3b28e7ffb4f69eee Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 6 Jan 2013 21:50:36 -0800
Subject: [PATCH] Fix bug in realclosure::compare function

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/math/interval/interval.h         | 5 +++++
 src/math/interval/interval_def.h     | 7 +++++++
 src/math/realclosure/realclosure.cpp | 6 +++---
 3 files changed, 15 insertions(+), 3 deletions(-)

diff --git a/src/math/interval/interval.h b/src/math/interval/interval.h
index 32c76c87f..1fe797861 100644
--- a/src/math/interval/interval.h
+++ b/src/math/interval/interval.h
@@ -200,6 +200,11 @@ public:
 
     bool eq(interval const & a, interval const & b) const;
 
+    /**
+       \brief Return true if all values in 'a' are less than all values in 'b'.
+    */
+    bool before(interval const & a, interval const & b) const;
+
     /**
        \brief Set lower bound to -oo.
     */
diff --git a/src/math/interval/interval_def.h b/src/math/interval/interval_def.h
index c4259fad7..51c1652d7 100644
--- a/src/math/interval/interval_def.h
+++ b/src/math/interval/interval_def.h
@@ -687,6 +687,13 @@ bool interval_manager<C>::eq(interval const & a, interval const & b) const {
         upper_is_open(a) == upper_is_open(b);
 }
 
+template<typename C>
+bool interval_manager<C>::before(interval const & a, interval const & b) const {
+    if (upper_is_inf(a) || lower_is_inf(b))
+        return false;
+    return m().lt(upper(a), lower(b)) || (upper_is_open(a) && m().eq(upper(a), lower(b)));
+}
+
 template<typename C>
 void interval_manager<C>::neg_jst(interval const & a, interval_deps & b_deps) {
     if (lower_is_inf(a)) {
diff --git a/src/math/realclosure/realclosure.cpp b/src/math/realclosure/realclosure.cpp
index a1b110cc1..0b0483e3c 100644
--- a/src/math/realclosure/realclosure.cpp
+++ b/src/math/realclosure/realclosure.cpp
@@ -2500,10 +2500,10 @@ namespace realclosure {
             else if (is_nz_rational(a) && is_nz_rational(b))
                 return qm().lt(to_mpq(a), to_mpq(b)) ? -1 : 1;
             else {
-                // TODO: try to refine interval before switching to sub/expensive approach
-                if (bqm().lt(interval(a).upper(), interval(b).lower()))
+                // TODO: try to refine interval before switching to sub+sign approach
+                if (bqim().before(interval(a), interval(b)))
                     return -1;
-                else if (bqm().lt(interval(b).upper(), interval(a).lower()))
+                else if (bqim().before(interval(b), interval(a)))
                     return 1;
                 else {
                     value_ref diff(*this);