diff --git a/src/math/polysat/forbidden_intervals.cpp b/src/math/polysat/forbidden_intervals.cpp index 893cfba33..c98e7e404 100644 --- a/src/math/polysat/forbidden_intervals.cpp +++ b/src/math/polysat/forbidden_intervals.cpp @@ -9,10 +9,8 @@ Module Name: Author: - Nikolaj Bjorner (nbjorner) 2021-03-19 Jakob Rath 2021-04-6 - - + Nikolaj Bjorner (nbjorner) 2021-03-19 --*/ #include "math/polysat/forbidden_intervals.h" @@ -46,13 +44,7 @@ namespace polysat { } }; - backtrack _backtrack(out_side_cond); - - /** - * TODO: to express the interval for coefficient 2^i symbolically, - * we need right-shift/upper-bits-extract in the language. - * So currently we can only do it if the coefficient is 1 or -1. - */ + backtrack _backtrack(out_side_cond); auto [ok1, a1, e1, b1] = linear_decompose(v, c->to_ule().lhs(), out_side_cond); auto [ok2, a2, e2, b2] = linear_decompose(v, c->to_ule().rhs(), out_side_cond); @@ -63,26 +55,15 @@ namespace polysat { SASSERT(b1.is_val()); SASSERT(b2.is_val()); - coeff = a1; - _backtrack.released = true; - // LOG("add " << c << " " << a1 << " " << b1 << " " << a2 << " " << b2); - - if (match_linear1(c, coeff, b1, e1, a2, b2, e2, out_interval, out_side_cond)) + if (match_linear1(c, a1, b1, e1, a2, b2, e2, coeff, out_interval, out_side_cond)) return true; - if (match_linear2(c, coeff, b1, e1, a2, b2, e2, out_interval, out_side_cond)) + if (match_linear2(c, a1, b1, e1, a2, b2, e2, coeff, out_interval, out_side_cond)) return true; - if (match_linear3(c, coeff, b1, e1, a2, b2, e2, out_interval, out_side_cond)) + if (match_linear3(c, a1, b1, e1, a2, b2, e2, coeff, out_interval, out_side_cond)) return true; - -#if 0 - if (match_linear4(c, a1, b1, e1, a2, b2, e2, out_interval, out_side_cond)) - return true; - if (match_linear5(c, a1, b1, e1, a2, b2, e2, out_interval, out_side_cond)) - return true; -#endif _backtrack.released = false; return false; } @@ -170,9 +151,9 @@ namespace polysat { * condition for empty/full: e2 == -1 */ bool forbidden_intervals::match_linear1(signed_constraint const& c, - rational & a1, pdd const& b1, pdd const& e1, + rational const & a1, pdd const& b1, pdd const& e1, rational const & a2, pdd const& b2, pdd const& e2, - eval_interval& interval, vector& side_cond) { + rational& coeff, eval_interval& interval, vector& side_cond) { if (a2.is_zero() && !a1.is_zero()) { SASSERT(!a1.is_zero()); bool is_trivial = (b2 + 1).is_zero(); @@ -181,7 +162,8 @@ namespace polysat { rational lo_val = (b2 - b1 + 1).val(); auto hi = -e1; rational hi_val = (-b1).val(); - interval = to_interval(c, is_trivial, a1, lo_val, lo, hi_val, hi); + coeff = a1; + interval = to_interval(c, is_trivial, coeff, lo_val, lo, hi_val, hi); return true; } return false; @@ -192,19 +174,19 @@ namespace polysat { * condition for empty/full: e1 == 0 */ bool forbidden_intervals::match_linear2(signed_constraint const& c, - rational & a1, pdd const& b1, pdd const& e1, + rational const & a1, pdd const& b1, pdd const& e1, rational const & a2, pdd const& b2, pdd const& e2, - eval_interval& interval, vector& side_cond) { + rational& coeff, eval_interval& interval, vector& side_cond) { if (a1.is_zero() && !a2.is_zero()) { SASSERT(!a2.is_zero()); - a1 = a2; bool is_trivial = b1.is_zero(); push_eq(is_trivial, e1, side_cond); auto lo = -e2; rational lo_val = (-b2).val(); auto hi = e1 - e2; rational hi_val = (b1 - b2).val(); - interval = to_interval(c, is_trivial, a1, lo_val, lo, hi_val, hi); + coeff = a2; + interval = to_interval(c, is_trivial, coeff, lo_val, lo, hi_val, hi); return true; } return false; @@ -215,9 +197,9 @@ namespace polysat { * condition for empty/full: e1 == e2 */ bool forbidden_intervals::match_linear3(signed_constraint const& c, - rational & a1, pdd const& b1, pdd const& e1, + rational const & a1, pdd const& b1, pdd const& e1, rational const & a2, pdd const& b2, pdd const& e2, - eval_interval& interval, vector& side_cond) { + rational& coeff, eval_interval& interval, vector& side_cond) { if (a1 == a2 && !a1.is_zero()) { bool is_trivial = b1.val() == b2.val(); push_eq(is_trivial, e1 - e2, side_cond); @@ -225,115 +207,10 @@ namespace polysat { rational lo_val = (-b2).val(); auto hi = -e1; rational hi_val = (-b1).val(); - interval = to_interval(c, is_trivial, a1, lo_val, lo, hi_val, hi); + coeff = a1; + interval = to_interval(c, is_trivial, coeff, lo_val, lo, hi_val, hi); return true; } return false; } - -#if 0 - /** - * a1*y + e1 = 0, with a1 odd - */ - bool forbidden_intervals::match_linear4(signed_constraint const& c, - rational & a1, pdd const& b1, pdd const& e1, - rational & a2, pdd const& b2, pdd const& e2, - eval_interval& interval, vector& side_cond) { - if (a1.is_odd() && a2.is_zero() && b2.val().is_zero()) { - push_eq(true, e2, side_cond); - rational a_inv, pow2 = e1.manager().max_value() + 1; - VERIFY(a1.mult_inverse(e1.manager().power_of_2(), a_inv)); - auto lo = -e1 * a_inv; - auto lo_val = mod(-b1.val() * a_inv, pow2); - auto hi = lo + 1; - auto hi_val = mod(lo_val + 1, pow2); - interval = to_interval(c, false, rational::one(), lo_val, lo, hi_val, hi); - return true; - } - return false; - } - - /** - * Ad-hoc linear forbidden intervals - * ax <= b, b != -1, a < b: x not in [ceil((b+1)/a) .. floor((2^K-1)/a)] - * b <= ax, 0 < a < b: x not in [0 .. floor((b-1)/a)] - * ax < b, a < b: x not in [ceil(b/a) .. floor((2^K-1)/a)] - * b < ax, 0 < a <= b: x not in [0 .. floor(b/a)] - * - * TODO: generalize to ax + b <= c scenarios where ax does not overflow - * and ax+b does not overflow, but is larger than c - * Scenarios: - * - ax + b <= c - * - ax + b < c - * - c <= ax + b - * - c < ax + b - */ - bool forbidden_intervals::match_linear5(signed_constraint const& c, - rational & a1, pdd const& b1, pdd const& e1, - rational & a2, pdd const& b2, pdd const& e2, - eval_interval& interval, vector& side_cond) { - auto& m = e1.manager(); - - // ax <= b, b != -1, a < b: x not in [ceil((b+1)/a) .. floor((2^K-1)/a)] - if (c.is_positive() && - !a1.is_zero() && !a1.is_one() && - a2.is_zero() && b1.is_zero() && e2.is_val() && - a1 < b2.val() && b2.val() != m.max_value()) { - if (!e1.is_val()) - side_cond.push_back(s.eq(e1)); - auto lo_val = ceil((b2.val() + 1) / a1); - auto hi_val = floor(m.max_value() / a1) + 1; - SASSERT(lo_val < hi_val); - auto lo = m.mk_val(lo_val); - auto hi = m.mk_val(hi_val); - interval = eval_interval::proper(lo, lo_val, hi, hi_val); - return true; - } - - // b <= ax, 0 < a < b: x not in [0 .. floor((b-1)/a)] - if (c.is_positive() && - !a2.is_zero() && !a2.is_one() && - a1.is_zero() && b2.is_zero() && - a2 < b1.val() && e1.is_val()) { - if (!e2.is_val()) - side_cond.push_back(s.eq(e2)); - rational lo_val = rational::zero(); - rational hi_val = floor((b1.val() - 1) / a2) + 1; - SASSERT(lo_val < hi_val); - auto lo = m.mk_val(lo_val); - auto hi = m.mk_val(hi_val); - interval = eval_interval::proper(lo, lo_val, hi, hi_val); - return true; - } - - // ax < b, a < b: x not in [ceil(b/a) .. floor((2^K-1)/a)] - if (c.is_negative() && - !a2.is_zero() && !a2.is_one() && b2.is_zero() && - a1.is_zero() && e1.is_val() && a2 < b1.val()) { - if (!e2.is_val()) - side_cond.push_back(s.eq(e2)); - rational lo_val = ceil(b1.val() / a2); - rational hi_val = floor(m.max_value() / a2) + 1; - auto lo = m.mk_val(lo_val); - auto hi = m.mk_val(hi_val); - interval = eval_interval::proper(lo, lo_val, hi, hi_val); - return true; - } - - // b < ax, 0 < a <= b: x not in [0 .. floor(b/a)] - if (c.is_negative() && - !a1.is_zero() && !a1.is_one() && b1.is_zero() && - a2.is_zero() && e2.is_val() && a1 <= b2.val()) { - if (!e1.is_val()) - side_cond.push_back(s.eq(e2)); - rational lo_val = rational::zero(); - rational hi_val = floor(b2.val() / a1) + 1; - auto lo = m.mk_val(lo_val); - auto hi = m.mk_val(hi_val); - interval = eval_interval::proper(lo, lo_val, hi, hi_val); - return true; - } - return false; - } -#endif } diff --git a/src/math/polysat/forbidden_intervals.h b/src/math/polysat/forbidden_intervals.h index 5246ba6c4..dd5fbb178 100644 --- a/src/math/polysat/forbidden_intervals.h +++ b/src/math/polysat/forbidden_intervals.h @@ -31,33 +31,20 @@ namespace polysat { std::tuple linear_decompose(pvar v, pdd const& p, vector& out_side_cond); bool match_linear1(signed_constraint const& c, - rational & a1, pdd const& b1, pdd const& e1, + rational const & a1, pdd const& b1, pdd const& e1, rational const & a2, pdd const& b2, pdd const& e2, - eval_interval& interval, vector& side_cond); + rational& coeff, eval_interval& interval, vector& side_cond); bool match_linear2(signed_constraint const& c, - rational & a1, pdd const& b1, pdd const& e1, + rational const & a1, pdd const& b1, pdd const& e1, rational const & a2, pdd const& b2, pdd const& e2, - eval_interval& interval, vector& side_cond); + rational& coeff, eval_interval& interval, vector& side_cond); bool match_linear3(signed_constraint const& c, - rational & a1, pdd const& b1, pdd const& e1, + rational const & a1, pdd const& b1, pdd const& e1, rational const & a2, pdd const& b2, pdd const& e2, - eval_interval& interval, vector& side_cond); + rational& coeff, eval_interval& interval, vector& side_cond); -#if 0 - bool match_linear4(signed_constraint const& c, - rational & a1, pdd const& b1, pdd const& e1, - rational & a2, pdd const& b2, pdd const& e2, - eval_interval& interval, vector& side_cond); - - bool match_linear5(signed_constraint const& c, - rational & a1, pdd const& b1, pdd const& e1, - rational & a2, pdd const& b2, pdd const& e2, - eval_interval& interval, vector& side_cond); -#endif - - // bool coefficient_is_01(dd::pdd_manager& m, rational const& r) { return r.is_zero() || r.is_one() || r == m.max_value(); }; public: forbidden_intervals(solver& s) :s(s) {} bool get_interval(signed_constraint const& c, pvar v, rational & coeff, eval_interval& out_interval, vector& side_cond); diff --git a/src/math/polysat/viable.cpp b/src/math/polysat/viable.cpp index c09330009..1569b99c1 100644 --- a/src/math/polysat/viable.cpp +++ b/src/math/polysat/viable.cpp @@ -163,14 +163,20 @@ namespace polysat { /** * Traverse all interval constraints with coefficients to check whether current value 'val' for * 'v' is feasible. If not, extract a (maximal) interval to block 'v' from being assigned val. + * + * To investigate: + * - side conditions are stronger than for unit intervals. They constrain the lower and upper bounds to + * be precisely the assigned values. This is to ensure that lo/hi that are computed based on lo_val + * and division with coeff are valid. Is there a more relaxed scheme? */ bool viable::refine_viable(pvar v, rational const& val) { auto* e = m_non_units[v]; if (!e) return true; entry* first = e; + rational const& max_value = s.var2pdd(v).max_value(); do { - rational coeff_val = mod(e->coeff * val, s.var2pdd(v).max_value() + 1); + rational coeff_val = mod(e->coeff * val, max_value + 1); if (e->interval.currently_contains(coeff_val)) { rational delta_l = floor((coeff_val - e->interval.lo_val()) / e->coeff); rational delta_u = floor((e->interval.hi_val() - coeff_val - 1) / e->coeff); @@ -181,21 +187,25 @@ namespace polysat { // pass } else if (e->interval.lo_val() <= coeff_val) { - hi = val + 1; - if (hi > s.var2pdd(v).max_value()) + rational lambda_u = floor((max_value - coeff_val - 1) / e->coeff); + hi = val + lambda_u + 1; + if (hi > max_value) hi = 0; } else { SASSERT(coeff_val < e->interval.hi_val()); - lo = val; + rational lambda_l = floor(coeff_val / e->coeff); + lo = val - lambda_l; } SASSERT(hi <= s.var2pdd(v).max_value()); LOG("forbidden interval " << e->interval << " - " << val << " " << coeff_val << " [" << lo << ", " << hi << "["); entry* ne = alloc_entry(); ne->src = e->src; ne->side_cond = e->side_cond; + ne->side_cond.push_back(s.eq(e->interval.hi(), e->interval.hi_val())); + ne->side_cond.push_back(s.eq(e->interval.lo(), e->interval.lo_val())); ne->coeff = 1; - pdd lop = s.var2pdd(v).mk_val(lo); // TODO? + pdd lop = s.var2pdd(v).mk_val(lo); pdd hip = s.var2pdd(v).mk_val(hi); ne->interval = eval_interval::proper(lop, lo, hip, hi); intersect(v, ne); @@ -435,7 +445,7 @@ namespace polysat { do { if (e->coeff != 1) out << e->coeff << " * v" << v << " "; - out << e->interval << " " << e->side_cond << " " << e->src << " "; + out << e->interval << " " << e->side_cond << " " << e->src << "; "; e = e->next(); } while (e != first);