diff --git a/src/math/polysat/fixed_bits.cpp b/src/math/polysat/fixed_bits.cpp index d49916c10..5393f96bc 100644 --- a/src/math/polysat/fixed_bits.cpp +++ b/src/math/polysat/fixed_bits.cpp @@ -18,30 +18,59 @@ Author: namespace polysat { /** - * Constraint lhs <= rhs. - * - * 2^(k - d) * x = 2^(k - d) * c - * ==> x[|d|:0] = c[|d|:0] - * - * -2^(k - 2) * x > 2^(k - 1) - * <=> 2 + x[1:0] > 2 (mod 4) - * ==> x[1:0] = 1 - * -- TODO: Generalize [the obvious solution does not work] - */ - - /** - * 2^(k - d) * x = 2^(k - d) * c - * ==> x[|d|:0] = c[|d|:0] + * 2^k * x = 2^k * b + * ==> x[N-k-1:0] = b[N-k-1:0] */ bool get_eq_fixed_lsb(pdd const& p, fixed_bits& out) { + SASSERT(!p.is_val()); + unsigned const N = p.power_of_2(); + // Recognize p = 2^k * a * x - 2^k * b if (!p.hi().is_val()) return false; - // TODO: - return false; + if (!p.lo().is_val()) + return false; + // p = c * x - d + rational const c = p.hi().val(); + rational const d = (-p.lo()).val(); + SASSERT(!c.is_zero()); +#if 1 + // NOTE: ule_constraint::simplify removes odd factors of the leading term + unsigned k; + VERIFY(c.is_power_of_two(k)); + if (d.parity(N) < k) + return false; + rational const b = machine_div2k(d, k); + out = fixed_bits(N - k - 1, 0, b); + SASSERT_EQ(d, b * rational::power_of_two(k)); + SASSERT_EQ(p, (p.manager().mk_var(p.var()) - out.value) * rational::power_of_two(k)); + return true; +#else + // branch if we want to support non-simplifed constraints (not recommended) + // + // 2^k * a * x = 2^k * b + // ==> x[N-k-1:0] = a^-1 * b[N-k-1:0] + // for odd a + unsigned k = c.parity(N); + if (d.parity(N) < k) + return false; + rational const a = machine_div2k(c, k); + SASSERT(a.is_odd()); + SASSERT(a.is_one()); // TODO: ule-simplify will multiply with a_inv already, so we can drop the check here. + rational a_inv; + VERIFY(a.mult_inverse(N, a_inv)); + rational const b = machine_div2k(d, k); + out.hi = N - k - 1; + out.lo = 0; + out.value = a_inv * b; + SASSERT_EQ(p, (p.manager().mk_var(p.var()) - out.value) * a * rational::power_of_two(k)); + return true; +#endif } bool get_eq_fixed_bits(pdd const& p, fixed_bits& out) { - return get_eq_fixed_lsb(p, out); + if (get_eq_fixed_lsb(p, out)) + return true; + return false; } /** @@ -56,7 +85,53 @@ namespace polysat { return false; } + /** + * Constraint lhs <= rhs. + * + * x <= 2^k - 1 ==> x[N-1:k] = 0 + * x < 2^k ==> x[N-1:k] = 0 + */ + bool get_ule_fixed_msb(pdd const& p, pdd const& q, bool is_positive, fixed_bits& out) { + SASSERT(!q.is_zero()); // equalities are handled elsewhere + unsigned const N = p.power_of_2(); + pdd const& lhs = is_positive ? p : q; + pdd const& rhs = is_positive ? q : p; + bool const is_strict = !is_positive; + if (lhs.is_var() && rhs.is_val()) { + // x <= c + // find smallest k such that c <= 2^k - 1, i.e., c+1 <= 2^k + // ==> x <= 2^k - 1 ==> x[N-1:k] = 0 + // + // x < c + // find smallest k such that c <= 2^k + // ==> x < 2^k ==> x[N-1:k] = 0 + rational const c = is_strict ? rhs.val() : (rhs.val() + 1); + unsigned const k = c.next_power_of_two(); + if (k < N) { + out.hi = N - 1; + out.lo = k; + out.value = 0; + return true; + } + } + return false; + } + + // 2^(N-1) <= 2^(N-1-i) * x + bool get_ule_fixed_bit(pdd const& p, pdd const& q, bool is_positive, fixed_bits& out) { + return false; + } + bool get_ule_fixed_bits(pdd const& lhs, pdd const& rhs, bool is_positive, fixed_bits& out) { + SASSERT(ule_constraint::is_simplified(lhs, rhs)); + if (rhs.is_zero()) + return is_positive ? get_eq_fixed_bits(lhs, out) : false; + if (get_ule_fixed_msb(lhs, rhs, is_positive, out)) + return true; + if (get_ule_fixed_lsb(lhs, rhs, is_positive, out)) + return true; + if (get_ule_fixed_bit(lhs, rhs, is_positive, out)) + return true; return false; } @@ -79,44 +154,6 @@ namespace polysat { SASSERT(lhs.is_univariate() && lhs.degree() <= 1); SASSERT(rhs.is_univariate() && rhs.degree() <= 1); - if (rhs.is_zero()) { // equality - auto lhs_decomp = decouple_constant(lhs); - - lhs = lhs_decomp.first; - rhs = -lhs_decomp.second; - - SASSERT(rhs.is_val()); - - unsigned k = lhs.manager().power_of_2(); - unsigned d = lhs.max_pow2_divisor(); - unsigned span = k - d; - if (span == 0 || lhs.is_val()) - return false; - - p = lhs.div(rational::power_of_two(d)); - rational rhs_val = rhs.val(); - info.bits = rhs_val / rational::power_of_two(d); - if (!info.bits.is_int()) - return false; - - SASSERT(lhs.is_univariate() && lhs.degree() <= 1); - - auto it = p.begin(); - auto first = *it; - it++; - if (it == p.end()) { - // if the lhs contains only one monomial it is of the form: odd * x = mask. We can multiply by the inverse to get the mask for x - SASSERT(first.coeff.is_odd()); - rational inv; - VERIFY(first.coeff.mult_inverse(lhs.power_of_2(), inv)); - p *= inv; - info.bits = mod2k(info.bits * inv, span); - } - - info.length = span; - info.positive = pos; - return true; - } else { // inequality - check for special case if (pos || lhs.power_of_2() < 3) return false; diff --git a/src/math/polysat/fixed_bits.h b/src/math/polysat/fixed_bits.h index 895ac8763..f37eafeb1 100644 --- a/src/math/polysat/fixed_bits.h +++ b/src/math/polysat/fixed_bits.h @@ -3,7 +3,7 @@ Copyright (c) 2022 Microsoft Corporation Module Name: - Extract fixed bits from (univariate) constraints + Extract fixed bits of variables from univariate constraints Author: @@ -35,6 +35,8 @@ namespace polysat { bool get_eq_fixed_bits(pdd const& p, fixed_bits& out); bool get_ule_fixed_lsb(pdd const& lhs, pdd const& rhs, bool is_positive, fixed_bits& out); + bool get_ule_fixed_msb(pdd const& lhs, pdd const& rhs, bool is_positive, fixed_bits& out); + bool get_ule_fixed_bit(pdd const& lhs, pdd const& rhs, bool is_positive, fixed_bits& out); bool get_ule_fixed_bits(pdd const& lhs, pdd const& rhs, bool is_positive, fixed_bits& out); bool get_fixed_bits(signed_constraint c, fixed_bits& out);