na

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/math/polysat/constraint.cpp

@@ -15,6 +15,7 @@ Author:
 #include "math/polysat/constraint.h"
 #include "math/polysat/solver.h"
 #include "math/polysat/log.h"
+#include "math/polysat/log_helper.h"
 #include "math/polysat/var_constraint.h"
 #include "math/polysat/eq_constraint.h"
 #include "math/polysat/ule_constraint.h"

src/math/polysat/fixplex.h

@@ -43,6 +43,7 @@ namespace polysat {
         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;
+        virtual void restore_ineq() = 0;
     };
 
 
@@ -128,6 +129,15 @@ namespace polysat {
             fix_entry():x(null_var), r(0) {}
         };
 
+        struct ineq {
+            var_t v { null_var };
+            var_t w { null_var };
+            bool strict { false };
+            bool is_active { true };
+            ineq(var_t v, var_t w, bool s):
+                v(v), w(w), strict(s) {}
+        };
+
         static const var_t null_var = UINT_MAX;
         reslimit&                   m_limit;
         mutable manager             m;
@@ -148,6 +158,13 @@ namespace polysat {
         vector<stashed_bound>       m_stashed_bounds;
         map<numeral, fix_entry, typename manager::hash, typename manager::eq> m_value2fixed_var;
 
+        // inequalities
+        svector<ineq>               m_ineqs;
+        unsigned_vector             m_ineqs_to_check;
+        bool_vector                 m_var_is_touched;
+        vector<unsigned_vector>     m_var2ineqs;
+        svector<var_t>              m_vars_to_untouch;
+
     public:
         fixplex(reslimit& lim):
             m_limit(lim),
@@ -164,8 +181,9 @@ 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 add_le(var_t v, var_t w) override { add_ineq(v, w, false); }
+        void add_lt(var_t v, var_t w) override { add_ineq(v, w, true); }
+        virtual void restore_ineq() override;
 
         void set_bounds(var_t v, numeral const& lo, numeral const& hi);
         void unset_bounds(var_t v) { m_vars[v].set_free(); }
@@ -235,6 +253,11 @@ namespace polysat {
         pivot_strategy_t pivot_strategy() { return m_bland ? S_BLAND : S_DEFAULT; }
         var_t select_error_var(bool least);
 
+        // facilities for handling inequalities
+        void add_ineq(var_t v, var_t w, bool strict);
+        void touch_var(var_t x);
+        lbool check_ineqs();
+
         bool is_solved(row const& r) const;
         bool is_solved(var_t v) const { SASSERT(is_base(v)); return is_solved(base2row(v)); }
 

src/math/polysat/fixplex_def.h

@@ -76,11 +76,13 @@ namespace polysat {
                 return l_false;
             case l_undef:
                 m_to_patch.insert(v);
+                if (l_false == check_ineqs())
+                    return l_false;
                 return l_undef;
             }
         }
         SASSERT(well_formed());
-        return l_true;
+        return check_ineqs();
     }
 
     template<typename Ext>
@@ -226,6 +228,7 @@ namespace polysat {
         if (delta == 0)
             return;
         m_vars[v].m_value += delta;
+        touch_var(v);
         SASSERT(!is_base(v));
 
         //
@@ -473,15 +476,66 @@ namespace polysat {
     }
 
     template<typename Ext>
-    void fixplex<Ext>::add_le(var_t v, var_t w) {
-        NOT_IMPLEMENTED_YET();
+    void fixplex<Ext>::add_ineq(var_t v, var_t w, bool strict) {
+        unsigned idx = m_ineqs.size();
+        m_var2ineqs.reserve(std::max(v, w) + 1);
+        m_var2ineqs[v].push_back(idx);
+        m_var2ineqs[w].push_back(idx);
+        m_ineqs_to_check.push_back(idx);
+        m_ineqs.push_back(ineq(v, w, strict));
     }
 
     template<typename Ext>
-    void fixplex<Ext>::add_lt(var_t v, var_t w) {
-        NOT_IMPLEMENTED_YET();        
+    void fixplex<Ext>::restore_ineq() {
+        auto ineq = m_ineqs.back();
+        m_var2ineqs[ineq.v].pop_back();
+        m_var2ineqs[ineq.w].pop_back();
+        m_ineqs.pop_back();
     }
 
+    template<typename Ext>
+    void fixplex<Ext>::touch_var(var_t v) {
+        if (v >= m_var2ineqs.size())
+            return;
+        if (m_var_is_touched.get(v, false))
+            return;
+        m_var_is_touched.set(v, true);
+        for (auto idx : m_var2ineqs[v]) {
+            if (!m_ineqs[idx].is_active) {
+                m_ineqs[idx].is_active = true;
+                m_ineqs_to_check.push_back(idx);
+            }
+        }
+    }
+
+    template<typename Ext>
+    lbool fixplex<Ext>::check_ineqs() {
+        m_vars_to_untouch.reset();
+        for (auto idx : m_ineqs_to_check) {
+            if (idx >= m_ineqs.size())
+                continue;
+            auto& ineq = m_ineqs[idx];
+            var_t v = ineq.v;
+            var_t w = ineq.w;
+            if (ineq.strict && value(v) >= value(w)) {
+                IF_VERBOSE(0, verbose_stream() << "violated v" << v << " < v" << w << "\n");
+                return l_false;
+            }
+            if (ineq.strict && value(v) > value(w)) {
+                IF_VERBOSE(0, verbose_stream() << "violated v" << v << " <= v" << w << "\n");
+                return l_false;
+            }
+            ineq.is_active = false;
+            m_vars_to_untouch.push_back(v);
+            m_vars_to_untouch.push_back(w);
+        }
+        for (auto v : m_vars_to_untouch)
+            m_var_is_touched.set(v, false);
+        m_ineqs_to_check.reset();
+        m_vars_to_untouch.reset();
+        return l_true;
+    } 
+
 
     /**
      * Check if the coefficient b of y has the minimal number of trailing zeros.
@@ -615,6 +669,7 @@ namespace polysat {
         set_base_value(y);
         xI.m_is_base = false;
         xI.m_value = new_value;
+        touch_var(x);
         row r_x(rx);
         add_patch(y);
         SASSERT(well_formed_row(r_x));
@@ -815,6 +870,7 @@ namespace polysat {
         SASSERT(is_base(x));
         row r = base2row(x);
         m_vars[x].m_value = solve_for(row2value(r), row2base_coeff(r));
+        touch_var(x);
         bool was_integral = row_is_integral(r);
         m_rows[r.id()].m_integral = is_solved(r);
         if (was_integral && !row_is_integral(r))

src/math/polysat/linear_solver.cpp

@@ -53,6 +53,12 @@ namespace polysat {
                 m_rows.pop_back();
                 break;
             }
+            case trail_i::add_ineq_i: {
+                auto [v, sz] = m_rows.back();
+                sz2fixplex(sz).restore_ineq();
+                m_rows.pop_back();
+                break;
+            }
             default:
                 UNREACHABLE();
             }
@@ -179,7 +185,8 @@ namespace polysat {
             fp.add_le(v, w);
         else 
             fp.add_lt(w, v);
-
+        m_trail.push_back(trail_i::add_ineq_i);
+        m_rows.push_back(std::make_pair(v, sz));
     }
 
     void linear_solver::new_bit(var_constraint& c) {

src/math/polysat/linear_solver.h

@@ -42,6 +42,7 @@ namespace polysat {
             add_var_i,
             add_mono_i,
             set_bound_i,
+            add_ineq_i,
             add_row_i
         };