mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-18 03:46:17 +00:00
Code Activity

add TODO marker in saturation for overflow rule

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-12-03 08:29:13 -08:00
parent 9572623675
commit c848192962
1 changed files with 6 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -323,6 +323,12 @@ namespace polysat {
return propagate(core, y_l_ax, x_l_z, x_l_z.is_strict() || y_l_ax.is_strict(), y, a * z); return propagate(core, y_l_ax, x_l_z, x_l_z.is_strict() || y_l_ax.is_strict(), y, a * z);
} }
/**
* TODO - add saturation based on Bench25 and other
* p <= k & p*v + q = 0 & q = 0 => p = 0 or v = 0 or v >= 2^K/k
* p <= k & p*v = 0 => p = 0 or v = 0 or v >= 2^K/k
*/
/** /**
* [x] p(x) <= q(x) where value(p) > value(q) * [x] p(x) <= q(x) where value(p) > value(q)
* ==> q <= value(q) => p <= value(q) * ==> q <= value(q) => p <= value(q)