mirror of
https://github.com/Z3Prover/z3
synced 2025-04-23 17:15:31 +00:00
Forward propagation for op_constraints + optimization for left/right shift
This commit is contained in:
Clemens Eisenhofer
parent
1d0ad1ccc0
commit
2581754c3e
4 changed files with 89 additions and 45 deletions
|
|
@ -453,6 +453,16 @@ namespace polysat {
|
|||
return -p - 1;
|
||||
}
|
||||
|
||||
static unsigned min_coefficient_power_of_2(const pdd& p) {
|
||||
if (p.is_zero())
|
||||
return 0; // TODO: Or something different?
|
||||
|
||||
unsigned min_power = UINT32_MAX;
|
||||
for (auto& m : p)
|
||||
min_power = std::min(min_power, m.coeff.trailing_zeros());
|
||||
return min_power;
|
||||
}
|
||||
|
||||
pdd constraint_manager::mk_op_term(op_constraint::code op, pdd const& p, pdd const& q) {
|
||||
auto& m = p.manager();
|
||||
unsigned sz = m.power_of_2();
|
||||
|
|
@ -470,23 +480,34 @@ namespace polysat {
|
|||
}
|
||||
|
||||
pdd constraint_manager::lshr(pdd const& p, pdd const& q) {
|
||||
if (p.is_val() && q.is_val() && q.val().is_unsigned()) {
|
||||
return p.manager().mk_val(div(p.val(), rational::power_of_two(q.val().get_unsigned())));
|
||||
if (q.is_val()) {
|
||||
if (!q.val().is_unsigned())
|
||||
return p.manager().zero(); // TODO: The number is huge. We will for sure shift out all bits
|
||||
if (p.is_val())
|
||||
return p.manager().mk_val(div(p.val(), rational::power_of_two(q.val().get_unsigned())));
|
||||
|
||||
unsigned common = min_coefficient_power_of_2(p);
|
||||
pdd div = p.manager().zero();
|
||||
for (auto& m : p)
|
||||
div += machine_div(m.coeff, rational::power_of_two(common));
|
||||
return div;
|
||||
}
|
||||
|
||||
return mk_op_term(op_constraint::code::lshr_op, p, q);
|
||||
}
|
||||
|
||||
pdd constraint_manager::shl(pdd const& p, pdd const& q) {
|
||||
if (p.is_val() && q.is_val() && q.val().is_unsigned()) {
|
||||
return p.manager().mk_val(p.val() * rational::power_of_two(q.val().get_unsigned()));
|
||||
if (q.is_val()) {
|
||||
if (!q.val().is_unsigned())
|
||||
return p.manager().zero();
|
||||
return p * rational::power_of_two(q.val().get_unsigned());
|
||||
}
|
||||
return mk_op_term(op_constraint::code::shl_op, p, q);
|
||||
}
|
||||
|
||||
pdd constraint_manager::band(pdd const& p, pdd const& q) {
|
||||
if (p.is_val() && q.is_val()) {
|
||||
if (p.is_val() && q.is_val())
|
||||
return p.manager().mk_val(bitwise_and(p.val(), q.val()));
|
||||
}
|
||||
return mk_op_term(op_constraint::code::and_op, p, q);
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -229,10 +229,11 @@ namespace polysat {
|
|||
* when r, q are variables.
|
||||
*/
|
||||
clause_ref op_constraint::lemma_lshr(solver& s, assignment const& a) {
|
||||
auto& m = p().manager();
|
||||
auto const pv = a.apply_to(p());
|
||||
auto const qv = a.apply_to(q());
|
||||
auto const rv = a.apply_to(r());
|
||||
unsigned const K = p().manager().power_of_2();
|
||||
unsigned const K = m.power_of_2();
|
||||
|
||||
signed_constraint const lshr(this, true);
|
||||
|
||||
|
|
@ -253,7 +254,7 @@ namespace polysat {
|
|||
// q >= k -> r <= 2^{K-k} - 1
|
||||
return s.mk_clause(~lshr, ~s.ule(qv.val(), q()), s.ule(r(), rational::power_of_two(K - qv.val().get_unsigned()) - 1), true);
|
||||
else if (pv.is_val() && rv.is_val() && qv.is_val() && !qv.is_zero()) {
|
||||
unsigned const k = qv.val().get_unsigned();
|
||||
unsigned k = qv.val().get_unsigned();
|
||||
// q = k -> r[i] = p[i+k] for 0 <= i < K - k
|
||||
for (unsigned i = 0; i < K - k; ++i) {
|
||||
if (rv.val().get_bit(i) && !pv.val().get_bit(i + k)) {
|
||||
|
|
@ -265,7 +266,18 @@ namespace polysat {
|
|||
}
|
||||
}
|
||||
else {
|
||||
// forward propagation
|
||||
SASSERT(!(pv.is_val() && qv.is_val() && rv.is_val()));
|
||||
if (qv.is_val() && !rv.is_val()) {
|
||||
const rational& qr = qv.val();
|
||||
if (qr >= m.power_of_2())
|
||||
return s.mk_clause(~lshr, ~s.ule(m.mk_val(m.power_of_2()), q()), s.eq(r()), true);
|
||||
|
||||
if (rv.is_val()) {
|
||||
const rational& pr = pv.val();
|
||||
return s.mk_clause(~lshr, ~s.eq(p(), m.mk_val(pr)), ~s.eq(q(), m.mk_val(qr)), s.eq(r(), m.mk_val(machine_div(pr, rational::power_of_two(qr.get_unsigned())))), true);
|
||||
}
|
||||
}
|
||||
}
|
||||
return {};
|
||||
}
|
||||
|
|
@ -309,10 +321,11 @@ namespace polysat {
|
|||
* q = 0 -> r = p
|
||||
*/
|
||||
clause_ref op_constraint::lemma_shl(solver& s, assignment const& a) {
|
||||
auto& m = p().manager();
|
||||
auto const pv = a.apply_to(p());
|
||||
auto const qv = a.apply_to(q());
|
||||
auto const rv = a.apply_to(r());
|
||||
unsigned const K = p().manager().power_of_2();
|
||||
unsigned const K = m.power_of_2();
|
||||
|
||||
signed_constraint const shl(this, true);
|
||||
|
||||
|
|
@ -333,7 +346,7 @@ namespace polysat {
|
|||
// q >= k -> r - 1 >= 2^k - 1 (equivalent unit constraint to better support narrowing)
|
||||
return s.mk_clause(~shl, ~s.ule(qv.val(), q()), s.ule(rational::power_of_two(qv.val().get_unsigned()) - 1, r() - 1), true);
|
||||
else if (pv.is_val() && rv.is_val() && qv.is_val() && !qv.is_zero()) {
|
||||
unsigned const k = qv.val().get_unsigned();
|
||||
unsigned k = qv.val().get_unsigned();
|
||||
// q = k -> r[i+k] = p[i] for 0 <= i < K - k
|
||||
for (unsigned i = 0; i < K - k; ++i) {
|
||||
if (rv.val().get_bit(i + k) && !pv.val().get_bit(i)) {
|
||||
|
|
@ -345,7 +358,18 @@ namespace polysat {
|
|||
}
|
||||
}
|
||||
else {
|
||||
// forward propagation
|
||||
SASSERT(!(pv.is_val() && qv.is_val() && rv.is_val()));
|
||||
if (qv.is_val() && !rv.is_val()) {
|
||||
const rational& qr = qv.val();
|
||||
if (qr >= m.power_of_2())
|
||||
return s.mk_clause(~shl, ~s.ule(m.mk_val(m.power_of_2()), q()), s.eq(r()), true);
|
||||
|
||||
if (rv.is_val()) {
|
||||
const rational& pr = pv.val();
|
||||
return s.mk_clause(~shl, ~s.eq(p(), m.mk_val(pr)), ~s.eq(q(), m.mk_val(qr)), s.eq(r(), m.mk_val(rational::power_of_two(qr.get_unsigned()) * pr)), true);
|
||||
}
|
||||
}
|
||||
}
|
||||
return {};
|
||||
}
|
||||
|
|
@ -525,6 +549,12 @@ namespace polysat {
|
|||
return s.mk_clause(~andc, s.ule(r(), p()), true);
|
||||
if (qv.is_zero() && !rv.is_zero()) // rv not necessarily fully evaluated
|
||||
return s.mk_clause(~andc, s.ule(r(), q()), true);
|
||||
|
||||
if (pv.is_val() && qv.is_val() && !rv.is_val()) {
|
||||
const rational& pr = pv.val();
|
||||
const rational& qr = qv.val();
|
||||
return s.mk_clause(~s.eq(p(), m.mk_val(pr)), ~s.eq(q(), m.mk_val(qr)), s.eq(r(), m.mk_val(bitwise_and(pr, qr))), true);
|
||||
}
|
||||
return {};
|
||||
}
|
||||
|
||||
|
|
@ -596,27 +626,39 @@ namespace polysat {
|
|||
auto& m = p().manager();
|
||||
auto pv = a.apply_to(p());
|
||||
auto rv = a.apply_to(r());
|
||||
|
||||
if (!pv.is_val() || !rv.is_val() || eval_inv(pv, rv) == l_true)
|
||||
|
||||
if (eval_inv(pv, rv) == l_true)
|
||||
return {};
|
||||
|
||||
unsigned parity_pv = pv.val().trailing_zeros();
|
||||
unsigned parity_rv = rv.val().trailing_zeros();
|
||||
|
||||
|
||||
signed_constraint const invc(this, true);
|
||||
|
||||
|
||||
// p = 0 => r = 0
|
||||
if (pv.is_zero())
|
||||
return s.mk_clause(~invc, ~s.eq(p()), s.eq(r()), true);
|
||||
// r = 0 => p = 0
|
||||
if (rv.is_zero())
|
||||
return s.mk_clause(~invc, ~s.eq(r()), s.eq(p()), true);
|
||||
|
||||
// p assigned => r = pseudo_inverse(eval(p))
|
||||
if (pv.is_val() && !rv.is_val()) {
|
||||
verbose_stream() << "Inverse ---+++ \n";
|
||||
verbose_stream() << "Inverse of " << s.eq(p(), pv) << " = " << s.eq(r(), pv.val().pseudo_inverse(m.power_of_2())) << "\n";
|
||||
return s.mk_clause(~invc, ~s.eq(p(), pv), s.eq(r(), pv.val().pseudo_inverse(m.power_of_2())), true);
|
||||
}
|
||||
|
||||
if (!pv.is_val() || !rv.is_val())
|
||||
return {};
|
||||
|
||||
unsigned parity_pv = pv.val().trailing_zeros();
|
||||
unsigned parity_rv = rv.val().trailing_zeros();
|
||||
|
||||
// odd(r)
|
||||
if (parity_rv != 0)
|
||||
return s.mk_clause(~invc, s.odd(r()), true);
|
||||
// parity(p) >= k && p * r < 2^k => p * r >= 2^k
|
||||
// parity(p) < k && p * r >= 2^k => p * r < 2^k
|
||||
rational prod = (p() * r()).val();
|
||||
pdd prod = p() * r();
|
||||
rational prodv = (pv * rv).val();
|
||||
SASSERT(prod != rational::power_of_two(parity_pv)); // Why did it evaluate to false in this case?
|
||||
unsigned lower = 0, upper = p().power_of_2();
|
||||
// binary search for the parity
|
||||
|
|
@ -626,14 +668,14 @@ namespace polysat {
|
|||
if (parity_pv >= middle) {
|
||||
lower = middle;
|
||||
LOG("Its in [" << lower << "; " << upper << ")");
|
||||
if (prod < rational::power_of_two(middle))
|
||||
return s.mk_clause(~invc, ~s.parity_at_least(p(), middle), s.uge(p() * r(), rational::power_of_two(middle)), false);
|
||||
if (prodv < rational::power_of_two(middle))
|
||||
return s.mk_clause(~invc, ~s.parity_at_least(p(), middle), s.uge(prod, rational::power_of_two(middle)), false);
|
||||
}
|
||||
else {
|
||||
upper = middle;
|
||||
LOG("Its in [" << lower << "; " << upper << ")");
|
||||
if (prod >= rational::power_of_two(middle))
|
||||
return s.mk_clause(~invc, s.parity_at_least(p(), middle), s.ult(p() * r(), rational::power_of_two(middle)), false);
|
||||
if (prodv >= rational::power_of_two(middle))
|
||||
return s.mk_clause(~invc, s.parity_at_least(p(), middle), s.ult(prod, rational::power_of_two(middle)), false);
|
||||
}
|
||||
}
|
||||
UNREACHABLE();
|
||||
|
|
|
|||
|
|
@ -1070,12 +1070,14 @@ namespace polysat {
|
|||
}
|
||||
|
||||
void solver::assign_decision(sat::literal lit) {
|
||||
SASSERT(lit != sat::null_literal);
|
||||
m_bvars.decision(lit, m_level);
|
||||
m_trail.push_back(trail_instr_t::assign_bool_i);
|
||||
m_search.push_boolean(lit);
|
||||
}
|
||||
|
||||
void solver::assign_propagate(sat::literal lit, clause& reason) {
|
||||
SASSERT(lit != sat::null_literal);
|
||||
m_bvars.propagate(lit, level(lit, reason), reason);
|
||||
m_trail.push_back(trail_instr_t::assign_bool_i);
|
||||
m_search.push_boolean(lit);
|
||||
|
|
|
|||
|
|
@ -684,8 +684,7 @@ namespace polysat {
|
|||
//return { p, false, {} };
|
||||
LOG("Warning: Inverting " << a << " although it is not a single variable - might not be a good idea");
|
||||
}
|
||||
|
||||
#if 1
|
||||
|
||||
unsigned a_parity;
|
||||
if ((a_parity = saturation.min_parity(a)) != saturation.max_parity(a) || saturation.min_parity(a1) < a_parity)
|
||||
return { p, false }; // We need the parity of a and this has to be for sure less than the parity of a1
|
||||
|
|
@ -699,6 +698,7 @@ namespace polysat {
|
|||
pdd a_pi = s.pseudo_inv(a);
|
||||
//precondition.insert_eval(~s.eq(a_pi * a, rational::power_of_two(a_parity))); // TODO: This is unfortunately not a justification as the inverse might not be set yet (Can we make it to one?)
|
||||
precondition.insert_eval(~s.parity_at_most(a, a_parity));
|
||||
verbose_stream() << "parity at most: " << ~s.parity_at_most(a, a_parity) << "\n";
|
||||
#endif
|
||||
|
||||
pdd shift = a;
|
||||
|
|
@ -716,27 +716,6 @@ namespace polysat {
|
|||
LOG("shifted a" << shift);
|
||||
LOG("Forced elimination: " << a_pi * (-b) * shift + b1);
|
||||
return { a_pi * (-b) * shift + b1, true };
|
||||
#else
|
||||
unsigned a_parity;
|
||||
unsigned a1_parity;
|
||||
|
||||
if ((a_parity = saturation.min_parity(a)) != saturation.max_parity(a) || (a1_parity = saturation.min_parity(a1)) != saturation.max_parity(a1))
|
||||
return { p, false }; // We need the parity, but we failed to get it precisely
|
||||
|
||||
if (a_parity > a1_parity) {
|
||||
SASSERT(false); // get_multiple should have excluded this case already
|
||||
return { p, false };
|
||||
}
|
||||
|
||||
auto odd_a = get_odd(a, a_parity, precondition);
|
||||
auto odd_a1 = get_odd(a1, a1_parity, precondition);
|
||||
pdd inv_odd_a = get_inverse(odd_a);
|
||||
|
||||
LOG("Forced elimination: " << odd_a1 * inv_odd_a * rational::power_of_two(a1_parity - a_parity) * b + b1);
|
||||
verbose_stream() << "Forced elimination: " << odd_a1 * inv_odd_a * rational::power_of_two(a1_parity - a_parity) * (-b) + b1 << "\n";
|
||||
verbose_stream() << "From: " << "eliminated v" << x << " with a = " << a << "; -b = " << -b << "; p = " << p << "\n";
|
||||
return { odd_a1 * inv_odd_a * rational::power_of_two(a1_parity - a_parity) * (-b) + b1, true };
|
||||
#endif
|
||||
#endif
|
||||
}
|
||||
}
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue