mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 17:45:32 +00:00
Code Activity

a test

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-05-06 19:09:31 -07:00
parent b5d1b0336a
commit d33b9f2698
2 changed files with 14 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/math/polysat/fixplex_def.h
View file

@ -763,15 +763,16 @@ namespace polysat {
//
// c = 1:
// free_v in [lo_sum, hi_sum[
// free_v in [0 - hi_sum, 1 - lo_sum[
// c = -1:
// free_v in [1 - hi_sum, 1 - lo_sum[
// free_v in [lo_sum, hi_sum + 1[
//
if (free_c == 1)
new_bound(r, free_v, lo_sum, hi_sum);
new_bound(r, free_v, 0 - hi_sum, 1 - lo_sum);
else
new_bound(r, free_v, 1 - hi_sum, 1 - lo_sum);
new_bound(r, free_v, lo_sum, hi_sum + 1);
SASSERT(in_bounds(free_v));
return;
}
for (auto const& e : M.row_entries(r)) {
@ -779,7 +780,7 @@ namespace polysat {
SASSERT(!is_free(v));
numeral const& c = e.coeff();
numeral lo_other = lo_sum - lo(v) * c;
numeral hi_other = hi_sum - (hi(v) - 1) * c - 1;
numeral hi_other = hi_sum - (hi(v) - 1) * c + 1;
//
// compute [lo_other,hi_other[ as range of
// other variables.
@ -790,6 +791,7 @@ namespace polysat {
new_bound(r, v, lo1, hi(v));
if (hi(v) > hi1)
new_bound(r, v, lo(v), hi1);
SASSERT(in_bounds(v));
}
}

7
src/test/fixplex.cpp
View file

@ -64,6 +64,13 @@ namespace polysat {
fp.set_bounds(y, 3, 6);
fp.run();
fp.propagate_bounds();
fp.reset();
coeffs[2] = 0ull - 1;
fp.add_row(x, 3, ys, coeffs);
fp.set_bounds(x, 3, 4);
fp.set_bounds(y, 3, 6);
fp.run();
fp.propagate_bounds();
}
}