mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 17:45:32 +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:38:26 -08:00
parent c848192962
commit 0657cdd4a7
1 changed files with 12 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -325,8 +325,18 @@ namespace polysat {
/**
* 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
* p <= k & p*x + q = 0 & q = 0 => p = 0 or x = 0 or x >= 2^K/k
* p <= k & p*x = 0 => p = 0 or x = 0 or x >= 2^K/k
*
* TODO
* p*x = 0 => p = 0 or even(x)
* Generaly:
* p*x = 0 => p = 0 or x = 0 or parity(x) + parity(y) >= K
* (if we use the convention parity(0) = K, then we can just write
* p*x = 0 => parity(x) + parity(y) >= K)
*
* TODO
* x*y = k & ~ovfl(x,y) & x = j => y = k/j where j is a divisor of k
*/
/**