diff --git a/src/math/polysat/constraint.cpp b/src/math/polysat/constraint.cpp index 2a70b6aac..5b08d78ae 100644 --- a/src/math/polysat/constraint.cpp +++ b/src/math/polysat/constraint.cpp @@ -29,6 +29,23 @@ namespace polysat { return *dynamic_cast(this); } + ule_constraint& constraint::to_ule() { + return *dynamic_cast(this); + } + + ule_constraint const& constraint::to_ule() const { + return *dynamic_cast(this); + } + + var_constraint& constraint::to_bit() { + return *dynamic_cast(this); + } + + var_constraint const& constraint::to_bit() const { + return *dynamic_cast(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); } diff --git a/src/math/polysat/constraint.h b/src/math/polysat/constraint.h index 0fa30f8a5..3465a6778 100644 --- a/src/math/polysat/constraint.h +++ b/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; } diff --git a/src/math/polysat/fixplex.h b/src/math/polysat/fixplex.h index 3ff14e8fc..67e48839d 100644 --- a/src/math/polysat/fixplex.h +++ b/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 { var_t m_var; - stashed_bound(var_t v, numeral const& lo, numeral const& hi): - mod_interval(lo, hi), + stashed_bound(var_t v, mod_interval const& i): + mod_interval(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); diff --git a/src/math/polysat/fixplex_def.h b/src/math/polysat/fixplex_def.h index 49590c9d4..e60cf11de 100644 --- a/src/math/polysat/fixplex_def.h +++ b/src/math/polysat/fixplex_def.h @@ -440,8 +440,8 @@ namespace polysat { * - the variable v is queued to patch if v is basic. */ template - void fixplex::set_bounds(var_t v, numeral const& lo, numeral const& hi) { - m_vars[v] = mod_interval(lo, hi); + void fixplex::set_bounds(var_t v, numeral const& l, numeral const& h) { + m_vars[v] = mod_interval(l, h); if (in_bounds(v)) return; if (is_base(v)) @@ -454,10 +454,17 @@ namespace polysat { void fixplex::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 + void fixplex::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 void fixplex::restore_bound() { auto const& b = m_stashed_bounds.back(); diff --git a/src/math/polysat/linear_solver.cpp b/src/math/polysat/linear_solver.cpp index faf5d3f1b..341cb8aed 100644 --- a/src/math/polysat/linear_solver.cpp +++ b/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: - NOT_IMPLEMENTED_YET(); + case trail_i::add_var_i: { + 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: { - // - // create the row c.p() - v == 0 - // 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::eq_t: + new_eq(c.to_eq()); + 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: { - var_t v = m_bool_var2row[c.bvar()]; - pdd p = c.to_eq().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); - break; - } + case ckind_t::eq_t: + assert_eq(c.to_eq()); + 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)); - fp.set_bounds(v, lo, hi); + m_rows.push_back(std::make_pair(w, sz)); + 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. diff --git a/src/math/polysat/linear_solver.h b/src/math/polysat/linear_solver.h index 2b4a7f429..cd80cc7ce 100644 --- a/src/math/polysat/linear_solver.h +++ b/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, - activate_constraint_i + add_row_i }; solver& s; @@ -54,14 +52,25 @@ namespace polysat { svector m_vars; vector m_coeffs; svector 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