mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-11 21:50:52 +00:00
Code Activity

fi: match_non_zero_linear

Browse source
This commit is contained in:
Jakob Rath 2022-01-26 11:08:03 +01:00
parent bbddeffe0b
commit cbed3bfde4
2 changed files with 53 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -55,14 +55,7 @@ namespace polysat {
_backtrack.released = true; _backtrack.released = true;
// a*v <= 0, a odd
if (ok1 && ok2 && match_zero(c, a1, b1, e1, a2, b2, e2, fi))
return true;
// v > q // v > q
// 2^k*a*v + b > 0
// TODO: is !ok2 required?
if (ok1 && !ok2 && match_non_zero(c, a1, b1, e1, fi)) if (ok1 && !ok2 && match_non_zero(c, a1, b1, e1, fi))
return true; return true;
@ -77,6 +70,14 @@ namespace polysat {
SASSERT(b1.is_val()); SASSERT(b1.is_val());
SASSERT(b2.is_val()); SASSERT(b2.is_val());
// a*v <= 0, a odd
if (match_zero(c, a1, b1, e1, a2, b2, e2, fi))
return true;
// a*v + b > 0, a odd
if (match_non_zero_linear(c, a1, b1, e1, a2, b2, e2, fi))
return true;
if (match_linear1(c, a1, b1, e1, a2, b2, e2, fi)) if (match_linear1(c, a1, b1, e1, a2, b2, e2, fi))
return true; return true;
if (match_linear2(c, a1, b1, e1, a2, b2, e2, fi)) if (match_linear2(c, a1, b1, e1, a2, b2, e2, fi))
@ -271,6 +272,10 @@ namespace polysat {
/** /**
* a*v <= 0, a odd * a*v <= 0, a odd
* forbidden interval for v is [1,0[ * forbidden interval for v is [1,0[
*
* TODO: extend to
* 2^k*a*v <= 0, a odd
* (using periodic intervals?)
*/ */
bool forbidden_intervals::match_zero( bool forbidden_intervals::match_zero(
signed_constraint const& c, signed_constraint const& c,
@ -294,6 +299,42 @@ namespace polysat {
return false; return false;
} }
/**
* a*v + b > 0, a odd
*
* TODO: extend to
* 2^k*a*v + b > 0, a odd
* (using periodic intervals?)
*/
bool forbidden_intervals::match_non_zero_linear(
signed_constraint const& c,
rational const & a1, pdd const& b1, pdd const& e1,
rational const & a2, pdd const& b2, pdd const& e2,
fi_record& fi) {
if (c.is_negative() && a1.is_odd() && a2.is_zero() && b2.is_zero()) {
// a*v + b > 0
// <=> a*v + b != 0
// <=> v + a^-1 * b != 0
// <=> v != - a^-1 * b
auto& m = e1.manager();
rational const& mod_value = m.two_to_N();
rational a1_inv;
VERIFY(a1.mult_inverse(m.power_of_2(), a1_inv));
rational lo_val(mod(-b1.val() * a1_inv, mod_value));
auto lo = -e1 * a1_inv;
rational hi_val(mod(lo_val + 1, mod_value));
auto hi = lo + 1;
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));
if (b2 != e2)
fi.side_cond.push_back(s.eq(b2, e2));
return true;
}
return false;
}
/** /**
* v > q * v > q
* forbidden interval for v is [0,1[ * forbidden interval for v is [0,1[

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

@ -57,6 +57,11 @@ namespace polysat {
rational const & a2, pdd const& b2, pdd const& e2, rational const & a2, pdd const& b2, pdd const& e2,
fi_record& fi); fi_record& fi);
bool match_non_zero_linear(signed_constraint const& c,
rational const & a1, pdd const& b1, pdd const& e1,
rational const & a2, pdd const& b2, pdd const& e2,
fi_record& fi);
bool match_non_zero(signed_constraint const& c, bool match_non_zero(signed_constraint const& c,
rational const & a1, pdd const& b1, pdd const& e1, rational const & a1, pdd const& b1, pdd const& e1,
fi_record& fi); fi_record& fi);