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

na

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

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

@ -733,6 +733,15 @@ namespace polysat {
propagate_bounds(row(i));
}
/**
* Bounds propagation
* works so far if coefficient to variable is 1 or -1
* Generalization is TBD:
* Explore an efficient way to propagate with the following idea:
* For odd c, multiply row by inverse of c and accumulate similar
* propagation.
*/
template<typename Ext>
void fixplex<Ext>::propagate_bounds(row const& r) {
numeral lo_sum = 0, hi_sum = 0, diff = 0, free_c = 0;
@ -758,7 +767,6 @@ namespace polysat {
return;
}
std::cout << "bounds " << free_v << "\n";
if (free_v != null_var) {
//
@ -779,24 +787,22 @@ namespace polysat {
var_t v = e.var();
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;
//
// compute [lo_other,hi_other[ as range of
// other variables.
//
numeral lo1 = 1 - hi_other;
numeral hi1 = 1 - lo_other;
if (lo(v) < lo1)
new_bound(r, v, lo1, hi(v));
if (hi(v) > hi1)
new_bound(r, v, lo(v), hi1);
if (c != 1 && c + 1 != 0)
continue;
numeral lo_sum1 = lo_sum - lo(v) * c;
numeral hi_sum1 = hi_sum - (hi(v) - 1) * c;
if (c == 1)
new_bound(r, v, 0 - hi_sum1, 1 - lo_sum1);
else
new_bound(r, v, lo_sum1, hi_sum1 + 1);
SASSERT(in_bounds(v));
}
}
template<typename Ext>
void fixplex<Ext>::new_bound(row const& r, var_t x, numeral const& l, numeral const& h) {
if (!is_free(x) && l <= lo(x) && hi(x) <= h)
return;
IF_VERBOSE(0, verbose_stream() << "new-bound v" << x << " [" << l << "," << h << "[\n");
}