mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-25 15:23:41 +00:00
Code Activity

remove commented code

Browse source
This commit is contained in:
Jakob Rath 2022-12-22 17:38:17 +01:00
parent 9207bb5d1e
commit 3739372776
1 changed files with 0 additions and 18 deletions
Download patch file Download diff file Expand all files Collapse all files

18
src/math/polysat/forbidden_intervals.cpp
View file

@ -460,20 +460,6 @@ namespace polysat {
fi.interval = eval_interval::proper(lo, lo_val, hi, hi_val); fi.interval = eval_interval::proper(lo, lo_val, hi, hi_val);
return true; return true;
} }
#if 0 // this case is subsumed by the next one, which even creates stronger intervals
if (a1.is_odd() && b1.is_zero() && c.is_negative()) {
auto& m = e1.manager();
rational lo_val(0);
auto lo = m.zero();
rational hi_val(1);
auto hi = m.one();
fi.coeff = 1;
fi.interval = eval_interval::proper(lo, lo_val, hi, hi_val);
if (b1 != e1)
fi.side_cond.push_back(s.eq(b1, e1));
return true;
}
#endif
if (a1.is_odd() && b1.is_val() && c.is_negative()) { if (a1.is_odd() && b1.is_val() && c.is_negative()) {
auto& m = e1.manager(); auto& m = e1.manager();
rational const& mod_value = m.two_to_N(); rational const& mod_value = m.two_to_N();
@ -485,10 +471,6 @@ namespace polysat {
auto hi = lo + 1; auto hi = lo + 1;
fi.coeff = 1; fi.coeff = 1;
fi.interval = eval_interval::proper(lo, lo_val, hi, hi_val); fi.interval = eval_interval::proper(lo, lo_val, hi, hi_val);
#if 0 // side condition is not needed because we use e1 in the symbolic bounds
if (b1 != e1)
fi.side_cond.push_back(s.eq(b1, e1));
#endif
return true; return true;
} }
return false; return false;