From 5ad486901e21e2a8a331b60338465c4b6202f347 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 21 May 2021 18:03:05 -0700
Subject: [PATCH] na

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/polysat/fixplex.h         |  4 ++
 src/math/polysat/fixplex_def.h     | 11 ++++++
 src/math/polysat/linear_solver.cpp | 61 ++++++++++++++++++++++++------
 src/test/polysat.cpp               |  7 +++-
 4 files changed, 70 insertions(+), 13 deletions(-)

diff --git a/src/math/polysat/fixplex.h b/src/math/polysat/fixplex.h
index 9219fa3c0..5a4f53a98 100644
--- a/src/math/polysat/fixplex.h
+++ b/src/math/polysat/fixplex.h
@@ -41,6 +41,8 @@ namespace polysat {
         virtual void set_bounds(var_t v, rational const& lo, rational const& hi) = 0;        
         virtual void set_value(var_t v, rational const& val) = 0;
         virtual void restore_bound() = 0;   
+        virtual void add_le(var_t v, var_t w) = 0;
+        virtual void add_lt(var_t v, var_t w) = 0;
     };
 
 
@@ -162,6 +164,8 @@ namespace polysat {
         void set_bounds(var_t v, rational const& lo, rational const& hi) override;
         void set_value(var_t v, rational const& val) override;
         void restore_bound() override;
+        void add_le(var_t v, var_t w) override;
+        void add_lt(var_t v, var_t w) override;
 
         void set_bounds(var_t v, numeral const& lo, numeral const& hi);
         void unset_bounds(var_t v) { m_vars[v].set_free(); }
diff --git a/src/math/polysat/fixplex_def.h b/src/math/polysat/fixplex_def.h
index e60cf11de..404667e3d 100644
--- a/src/math/polysat/fixplex_def.h
+++ b/src/math/polysat/fixplex_def.h
@@ -472,6 +472,17 @@ namespace polysat {
         m_stashed_bounds.pop_back();
     }
 
+    template<typename Ext>
+    void fixplex<Ext>::add_le(var_t v, var_t w) {
+        NOT_IMPLEMENTED_YET();
+    }
+
+    template<typename Ext>
+    void fixplex<Ext>::add_lt(var_t v, var_t w) {
+        NOT_IMPLEMENTED_YET();        
+    }
+
+
     /**
      * Check if the coefficient b of y has the minimal number of trailing zeros.
      * In other words, the coefficient b is a multiple of the smallest power of 2.
diff --git a/src/math/polysat/linear_solver.cpp b/src/math/polysat/linear_solver.cpp
index 024f1e64b..308629dcb 100644
--- a/src/math/polysat/linear_solver.cpp
+++ b/src/math/polysat/linear_solver.cpp
@@ -128,19 +128,58 @@ namespace polysat {
         m_bool_var2row.setx(c.bvar(), pr, pr);
     }
 
+    //
+    // v <= w:
+    // static constraints:
+    // - lo(v) <= lo(w)
+    // - hi(v) <= hi(w)
+    //
+    // special case for inequalities with constant bounds
+    // bounds propagation on fp, then bounds strengthening
+    // based on static constraints
+    // internal backtrack search over bounds
+    // inequality graph (with offsets)
+    // 
+
     void linear_solver::assert_le(ule_constraint& c) {
         auto [v, w] = m_bool_var2row[c.bvar()];
-        // v <= w:
-        // static constraints:
-        // - lo(v) <= lo(w)
-        // - hi(v) <= hi(w)
-        //
-        // special case for inequalities with constant bounds
-        // bounds propagation on fp, then bounds strengthening
-        // based on static constraints
-        // internal backtrack search over bounds
-        // inequality graph (with offsets)
-        // 
+        unsigned sz = c.lhs().power_of_2();
+        auto& fp = sz2fixplex(sz);     
+        rational z(0);
+        if (c.rhs().is_val()) {
+            bool is_max_value = false; 
+            if (c.is_positive()) 
+                // v <= rhs
+                fp.set_bounds(v, z, c.rhs().val());                 
+            else if (is_max_value) 
+                throw default_exception("conflict not implemented");
+            else 
+                // rhs < v
+                fp.set_bounds(v, c.rhs().val() + 1, z);
+            m_trail.push_back(trail_i::set_bound_i);
+            m_rows.push_back(std::make_pair(v, sz));
+            return;
+        }
+
+        if (c.lhs().is_val()) {
+            if (c.is_positive()) 
+                // w >= lhs 
+                fp.set_bounds(w, c.lhs().val(), z);
+            else if (c.lhs().val() == 0)
+                throw default_exception("conflict not implemented");
+            else 
+                // w < lhs 
+                fp.set_bounds(w, z, c.lhs().val() - 1);
+            m_trail.push_back(trail_i::set_bound_i);
+            m_rows.push_back(std::make_pair(w, sz));
+            return;
+        }
+
+        if (c.is_positive()) 
+            fp.add_le(v, w);
+        else 
+            fp.add_lt(w, v);
+
     }
 
     void linear_solver::new_bit(var_constraint& c) {
diff --git a/src/test/polysat.cpp b/src/test/polysat.cpp
index 164c3e20e..6a9d78562 100644
--- a/src/test/polysat.cpp
+++ b/src/test/polysat.cpp
@@ -582,7 +582,7 @@ namespace polysat {
 
      * We do overflow checks by doubling the base bitwidth here.
      */
-    static void test_fixed_point_arith_div_mul_inverse() {
+    static void test_fixed_point_arith_div_mul_inverse2() {
         scoped_solver s(__func__);
 
         auto baseBw = 5;
@@ -605,7 +605,7 @@ namespace polysat {
 
         // q = max_int / idx <=> q * idx + r - max_int = 0
         auto q = s.var(s.add_var(bw));
-        auto r = s.var(s.add_var(bw));
+        r = s.var(s.add_var(bw));
         s.add_eq((q * idx) + r - max_int);
         s.add_ult(r, idx);
         s.add_ule(q * idx, max_int);
@@ -684,6 +684,9 @@ void tst_polysat() {
     polysat::test_ineq_basic4();
     polysat::test_ineq_basic5();
     polysat::test_ineq_basic6();
+    polysat::test_fixed_point_arith_div_mul_inverse2();
+    polysat::test_fixed_point_arith_div_mul_inverse();
+    polysat::test_fixed_point_arith_mul_div_inverse();
 #if 0
     // worry about this later
     polysat::test_ineq1();