From befc47902efb688e83300d71cbb4bd01e067d5c0 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 22 May 2021 17:57:23 -0700
Subject: [PATCH] track

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/polysat/fixplex.h     |  1 +
 src/math/polysat/fixplex_def.h | 26 ++++++++++++++++++++------
 2 files changed, 21 insertions(+), 6 deletions(-)

diff --git a/src/math/polysat/fixplex.h b/src/math/polysat/fixplex.h
index 1f5428b98..35f3ce890 100644
--- a/src/math/polysat/fixplex.h
+++ b/src/math/polysat/fixplex.h
@@ -223,6 +223,7 @@ namespace polysat {
         void propagate_bounds(row const& r);
         void propagate_bounds(ineq const& i);
         void new_bound(row const& r, var_t x, mod_interval<numeral> const& range);
+        void new_bound(ineq const& i, var_t x, numeral const& lo, numeral const& hi);
         void pivot(var_t x_i, var_t x_j, numeral const& b, numeral const& value);
         numeral value2delta(var_t v, numeral const& new_value) const;
         numeral value2error(var_t v, numeral const& new_value) const;
diff --git a/src/math/polysat/fixplex_def.h b/src/math/polysat/fixplex_def.h
index 94181612d..f64828ab1 100644
--- a/src/math/polysat/fixplex_def.h
+++ b/src/math/polysat/fixplex_def.h
@@ -1086,17 +1086,31 @@ namespace polysat {
         // v < w => lo(v) < lo(w)
         // v <= w => hi(v) <= hi(w)
         // v <= w => lo(v) <= lo(w)
+        // TBD: detect conflicts, 
+        // ensure overflow / underflow conditions
         var_t v = i.v, w = i.w;
         if (i.strict && hi(v) >= hi(w))
-            ;
+            new_bound(i, v, lo(v), hi(w) - 1);
         if (i.strict && lo(v) >= lo(w))
-            ;
+            new_bound(i, w, lo(v) + 1, hi(w));
         if (!i.strict && hi(v) > hi(w))
-            ;
+            new_bound(i, v, lo(v), hi(w));
         if (!i.strict && lo(v) > lo(w))
-            ;
+            new_bound(i, w, lo(v), hi(w));
+    }
+
+    template<typename Ext>
+    void fixplex<Ext>::new_bound(ineq const& i, var_t x, numeral const& l, numeral const& h) {
+        mod_interval<numeral> r(l, h);
+        bool was_fixed = lo(x) + 1 == hi(x);
+        m_vars[x] &= r;
+        if (m_vars[x].is_empty())
+            m_infeasible_var = x;
+        else if (!was_fixed && lo(x) + 1 == hi(x)) {
+            // TBD: track based on inequality not row
+            // fixed_var_eh(r, x);
+        }
     }
-    
 
     template<typename Ext>
     void fixplex<Ext>::new_bound(row const& r, var_t x, mod_interval<numeral> const& range) {
@@ -1107,7 +1121,7 @@ namespace polysat {
         IF_VERBOSE(0, verbose_stream() << "new-bound v" << x << " " << m_vars[x] << "\n");
         if (m_vars[x].is_empty()) 
             m_infeasible_var = x;
-        else if (!was_fixed && lo(x) + 1 == hi(x))
+        else if (!was_fixed && lo(x) + 1 == hi(x)) 
             fixed_var_eh(r, x);
     }