mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-29 17:38:45 +00:00
Code Activity

try_umul_blast

Browse source
This commit is contained in:
Jakob Rath 2024-03-13 14:01:07 +01:00
parent 8a16631fd1
commit 7da7e99ca2
1 changed files with 17 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -144,7 +144,7 @@ namespace polysat {
* [y] z' < y /\ yx < zx ==> Ω*(x,y) \/ (z' + 1)x < zx (TODO?) * [y] z' < y /\ yx < zx ==> Ω*(x,y) \/ (z' + 1)x < zx (TODO?)
*/ */
void saturation::try_ugt_y(pvar v, inequality const& i) { void saturation::try_ugt_y(pvar v, inequality const& i) {
auto y = c.var(v); pdd const y = c.var(v);
pdd x = y; pdd x = y;
pdd z = y; pdd z = y;
if (!i.is_Xy_l_XZ(v, x, z)) if (!i.is_Xy_l_XZ(v, x, z))
@ -214,15 +214,17 @@ namespace polysat {
} }
/** /**
* Expand the following axioms: * Expand the following axioms:
* Ovfl(x, y) & x <= y => y >= 2^{(N + 1) div 2} * Ovfl(x, y) & x <= y => y >= 2^{(N + 1) div 2}
* Ovfl(x, y) & msb(x) <= k => msb(y) >= N - k + 1 * [ as approximation of Ovfl(x, y) & x <= y => y >= ceil(sqrt(2^N)) ]
* Ovfl(x, y) & msb(x) <= k & msb(y) <= N - k + 1 => 0x * 0y >= 2^N * Ovfl(x, y) & msb(x) <= k => msb(y) >= N - k + 1
* * Ovfl(x, y) & msb(x) <= k & msb(y) <= N - k + 1 => 0x * 0y >= 2^N
* ~Ovfl(x, y) & x <= y => x < 2^{(N + 1) div 2} *
* ~Ovfl(x,y) & msb(x) >= k => msb(y) <= N - k + 1 * ~Ovfl(x, y) & x <= y => x < 2^{(N + 1) div 2}
* ~Ovfl(x,y) & msb(x) >= k & msb(y) >= N - k + 1 => 0x * 0y < 2^N * [ as approximation of ~Ovfl(x, y) & x <= y => x < ceil(sqrt(2^N)) ]
*/ * ~Ovfl(x,y) & msb(x) >= k => msb(y) <= N - k + 1
* ~Ovfl(x,y) & msb(x) >= k & msb(y) >= N - k + 1 => 0x * 0y < 2^N
*/
void saturation::try_umul_blast(umul_ovfl const& sc) { void saturation::try_umul_blast(umul_ovfl const& sc) {
auto x = sc.p(); auto x = sc.p();
auto y = sc.q(); auto y = sc.q();
@ -231,7 +233,7 @@ namespace polysat {
return; return;
if (!c.try_eval(y, vy)) if (!c.try_eval(y, vy))
return; return;
auto N = x.manager().power_of_2(); unsigned N = x.manager().power_of_2();
auto d = c.get_dependency(sc.id()); auto d = c.get_dependency(sc.id());
auto bx = vx.get_num_bits(); auto bx = vx.get_num_bits();
@ -258,7 +260,7 @@ namespace polysat {
} }
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, ~C.msb_ge(x, bx), C.msb_le(y, N - bx + 1)}, true); { d, ~C.msb_ge(x, bx), C.msb_le(y, N - bx + 1) }, true);
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);
@ -271,9 +273,9 @@ namespace polysat {
if (bx <= 1) { if (bx <= 1) {
add_clause("Ovfl(x, y) => x > 1", { d, C.ugt(x, 1) }, true); add_clause("Ovfl(x, y) => x > 1", { d, C.ugt(x, 1) }, true);
} }
else if (bx < (N + 1) / 2) { else if (by < N / 2) {
add_clause("Ovfl(x, y) & x <= y => y >= 2^{(N + 1) div 2}", add_clause("Ovfl(x, y) & x <= y => y >= 2^{N div 2}",
{ d, ~C.ule(x, y), C.uge(x, rational::power_of_two((N + 1) / 2)) }, true); { d, ~C.ule(x, y), C.uge(y, rational::power_of_two(N / 2)) }, true);
} }
else if (bx + by < N + 1) { else if (bx + by < N + 1) {
SASSERT(bx <= by); SASSERT(bx <= by);