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

minor

Browse source
This commit is contained in:
Jakob Rath 2023-10-24 13:13:18 +02:00
parent f1b2a504d1
commit aea1b7836c
2 changed files with 11 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -41,6 +41,7 @@ namespace polysat {
} }
bool forbidden_intervals::get_interval_umul_ovfl(signed_constraint const& c, pvar v, fi_record& fi) { bool forbidden_intervals::get_interval_umul_ovfl(signed_constraint const& c, pvar v, fi_record& fi) {
using std::swap;
backtrack _backtrack(fi.side_cond); backtrack _backtrack(fi.side_cond);
@ -57,10 +58,10 @@ namespace polysat {
rational bound = m.max_value(); rational bound = m.max_value();
if (ok2 && !ok1) { if (ok2 && !ok1) {
std::swap(a1, a2); swap(a1, a2);
std::swap(e1, e2); swap(e1, e2);
std::swap(b1, b2); swap(b1, b2);
std::swap(ok1, ok2); swap(ok1, ok2);
} }
if (ok1 && !ok2 && a1.is_one() && b1.is_zero()) { if (ok1 && !ok2 && a1.is_one() && b1.is_zero()) {
if (c.is_positive()) { if (c.is_positive()) {
@ -79,9 +80,9 @@ namespace polysat {
if (a2.is_one() && a1.is_zero()) { if (a2.is_one() && a1.is_zero()) {
std::swap(a1, a2); swap(a1, a2);
std::swap(e1, e2); swap(e1, e2);
std::swap(b1, b2); swap(b1, b2);
} }
if (!a1.is_one() || !a2.is_zero()) if (!a1.is_one() || !a2.is_zero())
@ -262,9 +263,10 @@ namespace polysat {
return eval_interval::full(); return eval_interval::full();
} }
rational pow2 = m.max_value() + 1; rational pow2 = m.two_to_N();
if (coeff > pow2/2) { if (coeff > pow2/2) {
// TODO: if coeff != pow2 - 1, isn't this counterproductive now? considering the gap condition on refine-equal-lin acceleration.
coeff = pow2 - coeff; coeff = pow2 - coeff;
SASSERT(coeff > 0); SASSERT(coeff > 0);

2
src/math/polysat/forbidden_intervals.h
View file

@ -25,7 +25,7 @@ namespace polysat {
vector<signed_constraint> side_cond; vector<signed_constraint> side_cond;
vector<signed_constraint> src; // only units may have multiple src (as they can consist of contracted bit constraints) vector<signed_constraint> src; // only units may have multiple src (as they can consist of contracted bit constraints)
rational coeff; rational coeff;
unsigned bit_width = 0; // number of lower bits unsigned bit_width = 0; // number of lower bits; TODO: should move this to viable::entry; where the coeff/bit-width is adapted accordingly
/** Create invalid fi_record */ /** Create invalid fi_record */
fi_record(): interval(eval_interval::full()) {} fi_record(): interval(eval_interval::full()) {}