mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-04 10:20:23 +00:00
Code Activity

update names and nature of multiplication blast rules

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-02-01 17:12:35 -08:00
parent 60add85c47
commit 88b315cdb0
5 changed files with 54 additions and 22 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/sat/smt/polysat/constraints.cpp
View file

@ -88,6 +88,10 @@ namespace polysat {
return eq(p * rational::power_of_two(N - k)); return eq(p * rational::power_of_two(N - k));
} }
signed_constraint constraints::parity_at_most(pdd const& p, unsigned k) {
return ~parity_at_least(p, k + 1);
}
// 2^{N-i-1}* p >= 2^{N-1} // 2^{N-i-1}* p >= 2^{N-1}
signed_constraint constraints::bit(pdd const& p, unsigned i) { signed_constraint constraints::bit(pdd const& p, unsigned i) {
unsigned N = p.manager().power_of_2(); unsigned N = p.manager().power_of_2();

1
src/sat/smt/polysat/constraints.h
View file

@ -169,6 +169,7 @@ namespace polysat {
signed_constraint umul_ovfl(unsigned p, pdd const& q) { return umul_ovfl(rational(p), q); } signed_constraint umul_ovfl(unsigned p, pdd const& q) { return umul_ovfl(rational(p), q); }
signed_constraint parity_at_least(pdd const& p, unsigned k); signed_constraint parity_at_least(pdd const& p, unsigned k);
signed_constraint parity_at_most(pdd const& p, unsigned k);
signed_constraint lshr(pdd const& a, pdd const& b, pdd const& r); signed_constraint lshr(pdd const& a, pdd const& b, pdd const& r);
signed_constraint ashr(pdd const& a, pdd const& b, pdd const& r); signed_constraint ashr(pdd const& a, pdd const& b, pdd const& r);

53
src/sat/smt/polysat/monomials.cpp
View file

@ -66,12 +66,12 @@ namespace polysat {
return l_false; return l_false;
if (any_of(m_to_refine, [&](auto i) { return mul1(m_monomials[i]); })) if (any_of(m_to_refine, [&](auto i) { return mul1(m_monomials[i]); }))
return l_false; return l_false;
if (any_of(m_to_refine, [&](auto i) { return mul1_inverse(m_monomials[i]); })) if (any_of(m_to_refine, [&](auto i) { return mul_parametric_inverse(m_monomials[i]); }))
return l_false; return l_false;
if (any_of(m_to_refine, [&](auto i) { return non_overflow_unit(m_monomials[i]); })) if (any_of(m_to_refine, [&](auto i) { return mul1_inverse(m_monomials[i]); }))
return l_false; return l_false;
if (any_of(m_to_refine, [&](auto i) { return non_overflow_zero(m_monomials[i]); })) if (any_of(m_to_refine, [&](auto i) { return mul0_inverse(m_monomials[i]); }))
return l_false; return l_false;
if (false && any_of(m_to_refine, [&](auto i) { return parity0(m_monomials[i]); })) if (false && any_of(m_to_refine, [&](auto i) { return parity0(m_monomials[i]); }))
return l_false; return l_false;
@ -171,19 +171,32 @@ namespace polysat {
return c.add_axiom("p = k => p * q = k * q", cs, true); return c.add_axiom("p = k => p * q = k * q", cs, true);
} }
// p * q = p => q = 1 or p = 0 // p * q = p => parity(q - 1) + parity(p) >= N
// // p * q = p & ~Ovfl(p,q) => q = 1 or p = 0
// In general not true, because there exist a, b >= 2 with a * b = 0; then (a+1) * b = b. bool monomials::mul_parametric_inverse(monomial const& mon) {
// For now, add no-overflow condition on p*q.
bool monomials::mul1_inverse(monomial const& mon) {
for (unsigned j = mon.size(); j-- > 0; ) { for (unsigned j = mon.size(); j-- > 0; ) {
auto const& arg_val = mon.arg_vals[j]; auto const& arg_val = mon.arg_vals[j];
if (arg_val == mon.val) { if (arg_val == mon.val) {
auto const& p = mon.args[j]; auto const& p = mon.args[j];
pdd qs = c.value(rational(1), mon.num_bits()); pdd qs = c.value(rational(1), mon.num_bits());
rational qv(1);
for (unsigned k = mon.size(); k-- > 0; ) for (unsigned k = mon.size(); k-- > 0; )
if (k != j) if (k != j)
qs *= mon.args[k]; qs *= mon.args[k], qv *= mon.arg_vals[k];
if (qv == 0) {
if (c.add_axiom("q = 0 & p * q = p => p = 0", { ~C.eq(qs), ~C.eq(mon.var, p), C.eq(p)}, true))
return true;
continue;
}
qv = qv - 1;
unsigned qb = qv.get_num_bits();
unsigned pb = arg_val.get_num_bits();
unsigned N = p.manager().power_of_2();
if (qb + pb < N) {
if (c.add_axiom("p * q = p => parity(q - 1) + parity(p) >= N", { ~C.eq(mon.var, p), ~C.parity_at_most(p, pb), C.parity_at_least(qs - 1, N - pb) }, true))
return true;
}
if (c.add_axiom("p * q = p => q = 1 or p = 0", { ~C.eq(mon.var, p), ~C.umul_ovfl(p, qs), C.eq(qs, 1), C.eq(p) }, true)) if (c.add_axiom("p * q = p => q = 1 or p = 0", { ~C.eq(mon.var, p), ~C.umul_ovfl(p, qs), C.eq(qs, 1), C.eq(p) }, true))
return true; return true;
} }
@ -234,8 +247,21 @@ namespace polysat {
return c.add_axiom("~ovfl*(p,q) & q != 0 => p <= p*q", clause, true); return c.add_axiom("~ovfl*(p,q) & q != 0 => p <= p*q", clause, true);
} }
// p * q = 1 => parity(p) = 0 (instance of parity(p*q) >= min(N, parity(p) + parity(q))
// ~ovfl*(p,q) & p*q = 1 => p = 1, q = 1 // ~ovfl*(p,q) & p*q = 1 => p = 1, q = 1
bool monomials::non_overflow_unit(monomial const& mon) { bool monomials::mul1_inverse(monomial const& mon) {
if (!mon.val.is_odd())
return false;
unsigned j = 0;
for (auto const& val : mon.arg_vals) {
if (val.is_even()) {
if (c.add_axiom("odd(p*q) => odd(p)",
{~C.parity_at_most(mon.var, 0), C.parity_at_most(mon.args[j], 0) }, true))
return true;
}
++j;
}
if (mon.val != 1) if (mon.val != 1)
return false; return false;
rational product(1); rational product(1);
@ -260,8 +286,11 @@ namespace polysat {
return new_axiom; return new_axiom;
} }
// p*q = 0 => parity(p) + parity(q) >= N
// TODO: update to use parity instead of overflow
// ~ovfl*(p,q) & p*q = 0 => p = 0 or q = 0 // ~ovfl*(p,q) & p*q = 0 => p = 0 or q = 0
bool monomials::non_overflow_zero(monomial const& mon) { bool monomials::mul0_inverse(monomial const& mon) {
if (mon.val != 0) if (mon.val != 0)
return false; return false;
for (auto const& val : mon.arg_vals) for (auto const& val : mon.arg_vals)

6
src/sat/smt/polysat/monomials.h
View file

@ -49,12 +49,12 @@ namespace polysat {
bool mul0(monomial const& mon); bool mul0(monomial const& mon);
bool mul1(monomial const& mon); bool mul1(monomial const& mon);
bool mulp2(monomial const& mon); bool mulp2(monomial const& mon);
bool mul1_inverse(monomial const& mon); bool mul_parametric_inverse(monomial const& mon);
bool mul(monomial const& mon, std::function<bool(rational const&)> const& p); bool mul(monomial const& mon, std::function<bool(rational const&)> const& p);
bool parity(monomial const& mon); bool parity(monomial const& mon);
bool non_overflow_monotone(monomial const& mon); bool non_overflow_monotone(monomial const& mon);
bool non_overflow_unit(monomial const& mon); bool mul1_inverse(monomial const& mon);
bool non_overflow_zero(monomial const& mon); bool mul0_inverse(monomial const& mon);
bool parity0(monomial const& mon); bool parity0(monomial const& mon);
bool prefix_overflow(monomial const& mon); bool prefix_overflow(monomial const& mon);

12
src/sat/smt/polysat/saturation.cpp
View file

@ -268,7 +268,7 @@ namespace polysat {
add_clause("~Ovfl(x, y) & x <= y => x < 2^{(N + 1) div 2}", add_clause("~Ovfl(x, y) & x <= y => x < 2^{(N + 1) div 2}",
{ d, ~C.ule(x, y), C.ult(x, rational::power_of_two((N + 1) / 2)) }, { d, ~C.ule(x, y), C.ult(x, rational::power_of_two((N + 1) / 2)) },
true); true);
} }
else if (bx + by > N + 1) else if (bx + by > N + 1)
add_clause("~Ovfl(x, y) & msb(x) >= k => msb(y) <= N - k - 1", add_clause("~Ovfl(x, y) & msb(x) >= k => msb(y) <= N - k - 1",
{d, ~msb_ge(x, k), msb_le(y, N - k - 1)}, {d, ~msb_ge(x, k), msb_le(y, N - k - 1)},
@ -276,11 +276,9 @@ namespace polysat {
else { else {
auto x1 = c.mk_zero_extend(1, x); auto x1 = c.mk_zero_extend(1, x);
auto y1 = c.mk_zero_extend(1, y); auto y1 = c.mk_zero_extend(1, y);
add_clause("~Ovfl(x, y) & msb(x) >= k & msb(y) >= N - k - 1 => 0x * 0y < 2^{N-1}", add_clause("~Ovfl(x, y) => 0x * 0y < 2^{N}",
{ d, ~msb_ge(x, k), { d, C.ult(x1 * y1, rational::power_of_two(N)) },
~msb_ge(y, N - k - 1), true);
C.ult(x1 * y1, rational::power_of_two(N - 1))
}, true);
} }
} }
else { else {
@ -303,7 +301,7 @@ namespace polysat {
auto k = bx - 1; auto k = bx - 1;
auto x1 = c.mk_zero_extend(1, x); auto x1 = c.mk_zero_extend(1, x);
auto y1 = c.mk_zero_extend(1, y); auto y1 = c.mk_zero_extend(1, y);
add_clause("Ovfl(x, y) & msb(x) <= k & msb(y) <= N - k - 1 = > 0x * 0y >= 2 ^ {N - 1}", add_clause("Ovfl(x, y) & msb(x) <= k & msb(y) <= N - k - 1 => 0x * 0y >= 2 ^ {N - 1}",
{ d, ~msb_le(x, k), ~msb_le(y, N - k - 1), C.uge(x1 * y1, rational::power_of_two(N - 1)) }, { d, ~msb_le(x, k), ~msb_le(y, N - k - 1), C.uge(x1 * y1, rational::power_of_two(N - 1)) },
true); true);
} }