From 068b77d43a96acc33dd92e13a69b09a153eb76df Mon Sep 17 00:00:00 2001
From: Yakir Vizel <yakir.vizel@gmail.com>
Date: Wed, 27 Dec 2017 12:44:20 -0500
Subject: [PATCH] Normalizing LE and GE with constants

---
 src/muz/spacer/spacer_term_graph.cpp | 16 ++++++++++++++--
 1 file changed, 14 insertions(+), 2 deletions(-)

diff --git a/src/muz/spacer/spacer_term_graph.cpp b/src/muz/spacer/spacer_term_graph.cpp
index 859111c6c..5cd531870 100644
--- a/src/muz/spacer/spacer_term_graph.cpp
+++ b/src/muz/spacer/spacer_term_graph.cpp
@@ -118,7 +118,7 @@ public:
     app* mk_le_zero(expr *arg) {
         expr *e1, *e2, *e3;
         // XXX currently disabled
-        if (false && m_arith.is_add(arg, e1, e2)) {
+        if (m_arith.is_add(arg, e1, e2)) {
             // e1-e2<=0 --> e1<=e2
             if (m_arith.is_times_minus_one(e2, e3)) {
                 return m_arith.mk_le(e1, e3);
@@ -133,7 +133,7 @@ public:
     app* mk_ge_zero(expr *arg) {
         expr *e1, *e2, *e3;
         // XXX currently disabled
-        if (false && m_arith.is_add(arg, e1, e2)) {
+        if (m_arith.is_add(arg, e1, e2)) {
             // e1-e2>=0 --> e1>=e2
             if (m_arith.is_times_minus_one(e2, e3)) {
                 return m_arith.mk_ge(e1, e3);
@@ -148,6 +148,7 @@ public:
 
     bool mk_le_core (expr *arg1, expr * arg2, app_ref &result) {
         // t <= -1  ==> t < 0 ==> ! (t >= 0)
+        rational n;
         if (m_arith.is_int (arg1) && m_arith.is_minus_one (arg2)) {
             result = m.mk_not (mk_ge_zero (arg1));
             return true;
@@ -156,6 +157,11 @@ public:
             result = mk_le_zero(arg1);
             return true;
         }
+        else if (m_arith.is_numeral(arg2, n)) {
+            // t <= n ==> t < n + 1 ==> ! (t >= n + 1)
+            result = m.mk_not(m_arith.mk_ge(arg1, m_arith.mk_numeral(n+1, true)));
+            return true;
+        }
         return false;
     }
 
@@ -167,6 +173,7 @@ public:
 
     bool mk_ge_core (expr * arg1, expr * arg2, app_ref &result) {
         // t >= 1 ==> t > 0 ==> ! (t <= 0)
+        rational n;
         if (m_arith.is_int (arg1) && is_one (arg2)) {
             result = m.mk_not (mk_le_zero (arg1));
             return true;
@@ -175,6 +182,11 @@ public:
             result = mk_ge_zero(arg1);
             return true;
         }
+        else if (m_arith.is_numeral(arg2, n)) {
+            // t >= n ==> t > n - 1 ==> ! (t <= n - 1)
+            result = m.mk_not(m_arith.mk_le(arg1, m_arith.mk_numeral(n-1, true)));
+            return true;
+        }
         return false;
     }