na

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

src/math/polysat/constraint.cpp

@@ -29,6 +29,23 @@ namespace polysat {
         return *dynamic_cast<eq_constraint const*>(this); 
     }
 
+    ule_constraint& constraint::to_ule() {
+        return *dynamic_cast<ule_constraint*>(this);
+    }
+
+    ule_constraint const& constraint::to_ule() const {
+        return *dynamic_cast<ule_constraint const*>(this);
+    }
+
+    var_constraint& constraint::to_bit() {
+        return *dynamic_cast<var_constraint*>(this);
+    }
+
+    var_constraint const& constraint::to_bit() const {
+        return *dynamic_cast<var_constraint const*>(this);
+    }
+
+
     constraint* constraint::eq(unsigned lvl, bool_var bvar, csign_t sign, pdd const& p, p_dependency_ref const& d) {
         return alloc(eq_constraint, lvl, bvar, sign, p, d);
     }

src/math/polysat/constraint.h

@@ -58,6 +58,10 @@ namespace polysat {
         virtual void narrow(solver& s) = 0;
         eq_constraint& to_eq();
         eq_constraint const& to_eq() const;
+        ule_constraint& to_ule();
+        ule_constraint const& to_ule() const;
+        var_constraint& to_bit();
+        var_constraint const& to_bit() const;
         p_dependency* dep() const { return m_dep; }
         unsigned_vector& vars() { return m_vars; }
         unsigned level() const { return m_level; }

src/math/polysat/fixplex.h

@@ -32,12 +32,14 @@ namespace polysat {
     typedef unsigned var_t;
 
     struct fixplex_base {
+        virtual ~fixplex_base() {}
         virtual lbool make_feasible() = 0;
         virtual void add_row(var_t base, unsigned num_vars, var_t const* vars, rational const* coeffs) = 0;
         virtual void del_row(var_t base_var) = 0;
         virtual std::ostream& display(std::ostream& out) const = 0;
         virtual void collect_statistics(::statistics & st) const = 0;
         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;   
     };
 
@@ -111,8 +113,8 @@ namespace polysat {
 
         struct stashed_bound : mod_interval<numeral> {
             var_t m_var;
-            stashed_bound(var_t v, numeral const& lo, numeral const& hi):
+            stashed_bound(var_t v, mod_interval<numeral> const& i):
-                mod_interval<numeral>(lo, hi),
+                mod_interval<numeral>(i),
                 m_var(v)
             {}
         };
@@ -150,7 +152,7 @@ namespace polysat {
             M(m),
             m_to_patch(1024) {}
 
-        ~fixplex();
+        ~fixplex() override;
 
         lbool make_feasible() override;
         void add_row(var_t base, unsigned num_vars, var_t const* vars, rational const* coeffs) override;
@@ -158,6 +160,7 @@ namespace polysat {
         void collect_statistics(::statistics & st) const override;
         void del_row(var_t base_var) override;
         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 set_bounds(var_t v, numeral const& lo, numeral const& hi);

src/math/polysat/fixplex_def.h

@@ -440,8 +440,8 @@ namespace polysat {
      * - the variable v is queued to patch if v is basic.
      */
     template<typename Ext>
-    void fixplex<Ext>::set_bounds(var_t v, numeral const& lo, numeral const& hi) {        
+    void fixplex<Ext>::set_bounds(var_t v, numeral const& l, numeral const& h) {        
-        m_vars[v] = mod_interval(lo, hi);
+        m_vars[v] = mod_interval(l, h);
         if (in_bounds(v))
             return;
         if (is_base(v)) 
@@ -454,10 +454,17 @@ namespace polysat {
     void fixplex<Ext>::set_bounds(var_t v, rational const& _lo, rational const& _hi) {
         numeral lo = m.from_rational(_lo);
         numeral hi = m.from_rational(_hi);
-        m_stashed_bounds.push_back(stashed_bound(v, lo, hi));
+        m_stashed_bounds.push_back(stashed_bound(v, m_vars[v]));
         set_bounds(v, lo, hi);
     }
 
+    template<typename Ext>
+    void fixplex<Ext>::set_value(var_t v, rational const& _val) {
+        numeral val = m.from_rational(_val);
+        m_stashed_bounds.push_back(stashed_bound(v, m_vars[v]));
+        set_bounds(v, val, val + 1);
+    }
+
     template<typename Ext>
     void fixplex<Ext>::restore_bound() {
         auto const& b = m_stashed_bounds.back();

src/math/polysat/linear_solver.cpp

@@ -27,34 +27,31 @@ namespace polysat {
             case trail_i::inc_level_i:
                 --n;
                 break;
-            case trail_i::add_var_i:
+            case trail_i::add_var_i: {
-                NOT_IMPLEMENTED_YET();
+                auto [v, sz] = m_rows.back();
+                --m_sz2num_vars[sz];
+                m_rows.pop_back();
                 break;
+            }
             case trail_i::set_bound_i: {
                 auto [v, sz] = m_rows.back();
                 sz2fixplex(sz).restore_bound();
                 m_rows.pop_back();
                 break;
             }
-            case trail_i::set_value_i:
-                break;
             case trail_i::add_row_i: {
                 auto [v, sz] = m_rows.back();
                 sz2fixplex(sz).del_row(v);
                 m_rows.pop_back();
                 break;
             }
-            case trail_i::activate_constraint_i:
-                // not needed?
-                NOT_IMPLEMENTED_YET();
-                break;
             default:
                 UNREACHABLE();
             }
             m_trail.pop_back();
         }
     }
-
+    
     fixplex_base& linear_solver::sz2fixplex(unsigned sz) { 
         fixplex_base* b = m_fix.get(sz, nullptr);
         if (!b) {
@@ -74,51 +71,107 @@ namespace polysat {
             m_fix.set(sz, b);
         }
         return *b;
-    }        
+    }  
+
+
+    var_t linear_solver::internalize_pdd(pdd const& p) {
+        unsigned sz = p.power_of_2();
+        linearize(p);
+        if (m_vars.size() == 1 && m_coeffs.back() == 1) 
+            return m_vars.back();
+        var_t v = fresh_var(sz);
+        m_vars.push_back(v);
+        m_coeffs.push_back(rational::power_of_two(sz) - 1);
+        sz2fixplex(sz).add_row(v, m_vars.size(), m_vars.data(), m_coeffs.data());
+        m_rows.push_back(std::make_pair(v, sz));
+        m_trail.push_back(trail_i::add_row_i);
+        return v;
+    }
+    
+    /**
+     * create the row c.p() - v == 0
+     * when equality is asserted, set range on v as v == 0 or v > 0.
+     */
+        
+    void linear_solver::new_eq(eq_constraint& c) {
+        pdd p = c.p();
+        var_t v = internalize_pdd(c.p());
+        m_bool_var2row.setx(c.bvar(), v, UINT_MAX);        
+    }
+    
+    void linear_solver::assert_eq(eq_constraint& c) {
+        var_t v = m_bool_var2row[c.bvar()];
+        pdd p = c.p();
+        unsigned sz = p.power_of_2();
+        auto& fp = sz2fixplex(sz);            
+        m_trail.push_back(trail_i::set_bound_i);
+        m_rows.push_back(std::make_pair(v, sz));
+        if (c.is_positive()) 
+            fp.set_bounds(v, rational::zero(), rational::zero());
+        else 
+            fp.set_bounds(v, rational::one(), rational::power_of_two(sz) - 1);
+    }
+
+    void linear_solver::new_le(ule_constraint& c) {
+        var_t v = internalize_pdd(c.lhs());
+        m_bool_var2row.setx(c.bvar(), v, UINT_MAX);
+        var_t w = internalize_pdd(c.rhs());
+        m_bool_var2row.setx(c.bvar(), w, UINT_MAX);
+        // todo: track both variables
+    }
+
+    void linear_solver::assert_le(ule_constraint& c) {
+        // 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::new_bit(var_constraint& c) {
+    }
+
+    void linear_solver::assert_bit(var_constraint& c) {
+
+    }
+
 
     void linear_solver::new_constraint(constraint& c) {
         switch (c.kind()) {
-        case ckind_t::eq_t: {
+        case ckind_t::eq_t: 
-            //
+            new_eq(c.to_eq());
-            // create the row c.p() - v == 0
+            break;        
-            // when equality is asserted, set range on v as v == 0 or v > 0.
-            //
-            pdd p = c.to_eq().p();
-            unsigned sz = p.power_of_2();
-            linearize(p);
-            var_t v = fresh_var(sz);
-            m_vars.push_back(v);
-            m_coeffs.push_back(rational::power_of_two(sz) - 1);
-            sz2fixplex(sz).add_row(v, m_vars.size(), m_vars.data(), m_coeffs.data());
-            m_rows.push_back(std::make_pair(v, sz));
-            m_trail.push_back(trail_i::add_row_i);
-            m_bool_var2row.setx(c.bvar(), v, UINT_MAX);
-            break;
-        }
         case ckind_t::ule_t:
+            new_le(c.to_ule());
+            break;
         case ckind_t::bit_t:
+            new_bit(c.to_bit());
+            break;
+        default:
+            UNREACHABLE();
             break;
         }
     }
 
     void linear_solver::activate_constraint(constraint& c) {
         switch (c.kind()) {
-        case ckind_t::eq_t: {
+        case ckind_t::eq_t: 
-            var_t v = m_bool_var2row[c.bvar()];
+            assert_eq(c.to_eq());
-            pdd p = c.to_eq().p();
+            break;        
-            unsigned sz = p.power_of_2();
-            auto& fp = sz2fixplex(sz);
-            
-            m_trail.push_back(trail_i::set_bound_i);
-            m_rows.push_back(std::make_pair(v, sz));
-            if (c.is_positive()) 
-                fp.set_bounds(v, rational::zero(), rational::zero());
-            else 
-                fp.set_bounds(v, rational::one(), rational::power_of_two(sz) - 1);
-            break;
-        }
         case ckind_t::ule_t:
+            assert_le(c.to_ule());
+            break;
         case ckind_t::bit_t:
+            assert_bit(c.to_bit());            
+            break;
+        default:
+            UNREACHABLE();
             break;
         }
     }
@@ -138,28 +191,45 @@ namespace polysat {
         return 0;
     }
 
-    var_t linear_solver::fresh_var(unsigned sz) {
+    var_t linear_solver::pvar2var(unsigned sz, pvar v) {
         NOT_IMPLEMENTED_YET();
         return 0;
     }
 
+    var_t linear_solver::fresh_var(unsigned sz) {
+        m_sz2num_vars.reserve(sz + 1);
+        m_trail.push_back(trail_i::add_var_i);
+        m_rows.push_back(std::make_pair(0, sz));
+        return m_sz2num_vars[sz]++;
+    }
+
     void linear_solver::set_value(pvar v, rational const& value) {
+        unsigned sz = s.size(v);
+        auto& fp = sz2fixplex(sz);
+        var_t w = pvar2var(sz, v);
+        m_trail.push_back(trail_i::set_bound_i);
+        m_rows.push_back(std::make_pair(w, sz));
+        fp.set_value(w, value);        
     }
 
     void linear_solver::set_bound(pvar v, rational const& lo, rational const& hi) {
         unsigned sz = s.size(v);
         auto& fp = sz2fixplex(sz);
+        var_t w = pvar2var(sz, v);
         m_trail.push_back(trail_i::set_bound_i);
-        m_rows.push_back(std::make_pair(v, sz));
+        m_rows.push_back(std::make_pair(w, sz));
-        fp.set_bounds(v, lo, hi);        
+        fp.set_bounds(w, lo, hi);        
     }
     
     // check integer modular feasibility under current bounds.
     lbool linear_solver::check() { 
-        return l_undef; 
+        lbool res = l_true;
+        // loop over fp solvers that have been touched and use make_feasible.        
+        return res; 
     }
 
     void linear_solver::unsat_core(unsigned_vector& deps) {
+        NOT_IMPLEMENTED_YET();
     }
 
     // current value assigned to (linear) variable according to tableau.

src/math/polysat/linear_solver.h

@@ -39,9 +39,7 @@ namespace polysat {
             inc_level_i,
             add_var_i,
             set_bound_i,
-            set_value_i,
+            add_row_i
-            add_row_i,
-            activate_constraint_i
         };
 
         solver&                  s;
@@ -54,14 +52,25 @@ namespace polysat {
         svector<var_t>           m_vars;
         vector<rational>         m_coeffs;
         svector<var_t>           m_bool_var2row;
+        unsigned_vector          m_sz2num_vars;
 
         fixplex_base& sz2fixplex(unsigned sz);
 
         void linearize(pdd const& p);
         var_t fresh_var(unsigned sz);
 
+
+        var_t internalize_pdd(pdd const& p);
+        void new_eq(eq_constraint& eq);
+        void new_le(ule_constraint& le);
+        void new_bit(var_constraint& vc);
+        void assert_eq(eq_constraint& eq);
+        void assert_le(ule_constraint& le);
+        void assert_bit(var_constraint& vc);
+
         // bind monomial to variable.
         var_t mono2var(unsigned sz, unsigned_vector const& m);
+        var_t pvar2var(unsigned sz, pvar v);
         unsigned_vector var2mono(unsigned sz, var_t v) { throw default_exception("nyi"); }
         //
         // TBD trail object for