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

comments

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-12-21 15:45:24 -08:00
parent d0f0d5c3c6
commit 78aea59387
2 changed files with 18 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

18
src/sat/smt/polysat/op_constraint.cpp
View file

@ -528,6 +528,24 @@ namespace polysat {
} }
} }
#if 0
// introduce multiplication constraint and do away with non-linear polynomials in inequalities.
//
// z = x * y
// x = 0 or y = 0 => z = 0
// x = 1 => z = y
// y = 1 => z = y
// ~ovfl(x, y) => z >= x & z >= y
// ~ovfl(x, y) & x > 1 & y > 1 => z > x, z > y
// parity(x) + parity(y) >= N => z = 0
// parity(x) + parity(y) < N => parity(z) = parity(x) + parity(y)
// blast:
// z = sum_i bit(x,i) ? y*2^i : 0
#endif
#if 0 #if 0
/** /**

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

@ -226,12 +226,6 @@ namespace polysat {
prop = true; prop = true;
if (try_mul_eq_bound(v, core, i)) if (try_mul_eq_bound(v, core, i))
prop = true; prop = true;
if (try_ugt_x(v, core, i))
prop = true;
if (try_ugt_y(v, core, i))
prop = true;
if (try_ugt_z(v, core, i))
prop = true;
if (try_y_l_ax_and_x_l_z(v, core, i)) if (try_y_l_ax_and_x_l_z(v, core, i))
prop = true; prop = true;
if (false && try_tangent(v, core, i)) if (false && try_tangent(v, core, i))