mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 00:26:38 +00:00
Code Activity

Fix try_ugt_y

Browse source
This commit is contained in:
Jakob Rath 2023-04-03 16:18:01 +02:00
parent c3c9883b0a
commit 76c18ee6e3
1 changed files with 6 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/math/polysat/saturation.cpp
View file

@ -569,9 +569,11 @@ namespace polysat {
/**
* [y] z' <= y /\ yx <= zx ==> Ω*(x,y) \/ z'x <= zx
* [y] z' <= y /\ yx < zx ==> Ω*(x,y) \/ z'x < zx
* [y] z' < y /\ yx <= zx ==> Ω*(x,y) \/ z'x < zx
* [y] z' < y /\ yx < zx ==> Ω*(x,y) \/ z'x < zx TODO: could strengthen the conclusion to z'x + 1 < zx
* [y] z' <= y /\ yx < zx ==> Ω*(x,y) \/ z'x < zx
* [y] z' < y /\ yx <= zx ==> Ω*(x,y) \/ z'x <= zx
* [y] z' < y /\ yx < zx ==> Ω*(x,y) \/ z'x < zx
* [y] z' < y /\ yx < zx ==> Ω*(x,y) \/ z'x + 1 < zx (TODO?)
* [y] z' < y /\ yx < zx ==> Ω*(x,y) \/ (z' + 1)x < zx (TODO?)
*/
bool saturation::try_ugt_y(pvar v, conflict& core, inequality const& yx_l_zx) {
set_rule("[y] z' <= y & yx <= zx");
@ -605,7 +607,7 @@ namespace polysat {
pdd const& z_prime = l_y.lhs();
m_lemma.reset();
m_lemma.insert_eval(~non_ovfl);
return add_conflict(v, core, l_y, yx_l_zx, ineq(yx_l_zx.is_strict() || l_y.is_strict(), z_prime * x, z * x));
return add_conflict(v, core, l_y, yx_l_zx, ineq(yx_l_zx.is_strict(), z_prime * x, z * x));
}
/**