mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-22 13:53:39 +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 18:53:05 -07:00
parent 1d724de915
commit a1ded7f1ec
1 changed files with 6 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -738,7 +738,7 @@ namespace polysat {
if (is_free(v)) { if (is_free(v)) {
if (free_v != null_var) if (free_v != null_var)
return; return;
if (c != 1 && c + 1 != 1) if (c != 1 && c + 1 != 0)
return; return;
free_v = v; free_v = v;
free_c = c; free_c = c;
@ -768,27 +768,26 @@ namespace polysat {
} }
for (auto const& e : M.row_entries(r)) { for (auto const& e : M.row_entries(r)) {
var_t v = e.var(); var_t v = e.var();
SASSERT(!is_free(v));
numeral const& c = e.coeff(); numeral const& c = e.coeff();
numeral lo_other = lo_sum - lo(v) * c; numeral lo_other = lo_sum - lo(v) * c;
numeral hi_other = hi_sum - (hi(v) - 1) * c; numeral hi_other = hi_sum - (hi(v) - 1) * c - 1;
// //
// compute [lo_other,hi_other[ as range of // compute [lo_other,hi_other[ as range of
// other variables. // other variables.
// //
numeral lo1 = 1 - hi_other; numeral lo1 = 1 - hi_other;
numeral hi1 = 1 - lo_other; numeral hi1 = 1 - lo_other;
if (lo(v) < lo1) { if (lo(v) < lo1)
new_bound(r, v, lo1, hi(v)); new_bound(r, v, lo1, hi(v));
} if (hi(v) > hi1)
if (hi(v) > hi1) {
new_bound(r, v, lo(v), hi1); new_bound(r, v, lo(v), hi1);
} }
} }
}
template<typename Ext> template<typename Ext>
void fixplex<Ext>::new_bound(row const& r, var_t x, numeral const& l, numeral const& h) { void fixplex<Ext>::new_bound(row const& r, var_t x, numeral const& l, numeral const& h) {
IF_VERBOSE(0, verbose_stream() << "new-bound v" << x << " [" << l << "," << h << "[\n");
} }
template<typename Ext> template<typename Ext>