mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 00:26:38 +00:00
Code Activity

merge

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-12-08 12:44:55 -08:00
commit ca9fbcf6f4
3 changed files with 39 additions and 165 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -9,10 +9,8 @@ Module Name:
Author:
Nikolaj Bjorner (nbjorner) 2021-03-19
Jakob Rath 2021-04-6
Nikolaj Bjorner (nbjorner) 2021-03-19
--*/
#include "math/polysat/forbidden_intervals.h"
@ -46,13 +44,7 @@ namespace polysat {
}
};
backtrack _backtrack(out_side_cond);
/**
* TODO: to express the interval for coefficient 2^i symbolically,
* we need right-shift/upper-bits-extract in the language.
* So currently we can only do it if the coefficient is 1 or -1.
*/
backtrack _backtrack(out_side_cond);
auto [ok1, a1, e1, b1] = linear_decompose(v, c->to_ule().lhs(), out_side_cond);
auto [ok2, a2, e2, b2] = linear_decompose(v, c->to_ule().rhs(), out_side_cond);
@ -63,26 +55,15 @@ namespace polysat {
SASSERT(b1.is_val());
SASSERT(b2.is_val());
coeff = a1;
_backtrack.released = true;
// LOG("add " << c << " " << a1 << " " << b1 << " " << a2 << " " << b2);
if (match_linear1(c, coeff, b1, e1, a2, b2, e2, out_interval, out_side_cond))
if (match_linear1(c, a1, b1, e1, a2, b2, e2, coeff, out_interval, out_side_cond))
return true;
if (match_linear2(c, coeff, b1, e1, a2, b2, e2, out_interval, out_side_cond))
if (match_linear2(c, a1, b1, e1, a2, b2, e2, coeff, out_interval, out_side_cond))
return true;
if (match_linear3(c, coeff, b1, e1, a2, b2, e2, out_interval, out_side_cond))
if (match_linear3(c, a1, b1, e1, a2, b2, e2, coeff, out_interval, out_side_cond))
return true;
#if 0
if (match_linear4(c, a1, b1, e1, a2, b2, e2, out_interval, out_side_cond))
return true;
if (match_linear5(c, a1, b1, e1, a2, b2, e2, out_interval, out_side_cond))
return true;
#endif
_backtrack.released = false;
return false;
}
@ -170,9 +151,9 @@ namespace polysat {
* condition for empty/full: e2 == -1
*/
bool forbidden_intervals::match_linear1(signed_constraint const& c,
rational & a1, pdd const& b1, pdd const& e1,
rational const & a1, pdd const& b1, pdd const& e1,
rational const & a2, pdd const& b2, pdd const& e2,
eval_interval& interval, vector<signed_constraint>& side_cond) {
rational& coeff, eval_interval& interval, vector<signed_constraint>& side_cond) {
if (a2.is_zero() && !a1.is_zero()) {
SASSERT(!a1.is_zero());
bool is_trivial = (b2 + 1).is_zero();
@ -181,7 +162,8 @@ namespace polysat {
rational lo_val = (b2 - b1 + 1).val();
auto hi = -e1;
rational hi_val = (-b1).val();
interval = to_interval(c, is_trivial, a1, lo_val, lo, hi_val, hi);
coeff = a1;
interval = to_interval(c, is_trivial, coeff, lo_val, lo, hi_val, hi);
return true;
}
return false;
@ -192,19 +174,19 @@ namespace polysat {
* condition for empty/full: e1 == 0
*/
bool forbidden_intervals::match_linear2(signed_constraint const& c,
rational & a1, pdd const& b1, pdd const& e1,
rational const & a1, pdd const& b1, pdd const& e1,
rational const & a2, pdd const& b2, pdd const& e2,
eval_interval& interval, vector<signed_constraint>& side_cond) {
rational& coeff, eval_interval& interval, vector<signed_constraint>& side_cond) {
if (a1.is_zero() && !a2.is_zero()) {
SASSERT(!a2.is_zero());
a1 = a2;
bool is_trivial = b1.is_zero();
push_eq(is_trivial, e1, side_cond);
auto lo = -e2;
rational lo_val = (-b2).val();
auto hi = e1 - e2;
rational hi_val = (b1 - b2).val();
interval = to_interval(c, is_trivial, a1, lo_val, lo, hi_val, hi);
coeff = a2;
interval = to_interval(c, is_trivial, coeff, lo_val, lo, hi_val, hi);
return true;
}
return false;
@ -215,9 +197,9 @@ namespace polysat {
* condition for empty/full: e1 == e2
*/
bool forbidden_intervals::match_linear3(signed_constraint const& c,
rational & a1, pdd const& b1, pdd const& e1,
rational const & a1, pdd const& b1, pdd const& e1,
rational const & a2, pdd const& b2, pdd const& e2,
eval_interval& interval, vector<signed_constraint>& side_cond) {
rational& coeff, eval_interval& interval, vector<signed_constraint>& side_cond) {
if (a1 == a2 && !a1.is_zero()) {
bool is_trivial = b1.val() == b2.val();
push_eq(is_trivial, e1 - e2, side_cond);
@ -225,115 +207,10 @@ namespace polysat {
rational lo_val = (-b2).val();
auto hi = -e1;
rational hi_val = (-b1).val();
interval = to_interval(c, is_trivial, a1, lo_val, lo, hi_val, hi);
coeff = a1;
interval = to_interval(c, is_trivial, coeff, lo_val, lo, hi_val, hi);
return true;
}
return false;
}
#if 0
/**
* a1*y + e1 = 0, with a1 odd
*/
bool forbidden_intervals::match_linear4(signed_constraint const& c,
rational & a1, pdd const& b1, pdd const& e1,
rational & a2, pdd const& b2, pdd const& e2,
eval_interval& interval, vector<signed_constraint>& side_cond) {
if (a1.is_odd() && a2.is_zero() && b2.val().is_zero()) {
push_eq(true, e2, side_cond);
rational a_inv, pow2 = e1.manager().max_value() + 1;
VERIFY(a1.mult_inverse(e1.manager().power_of_2(), a_inv));
auto lo = -e1 * a_inv;
auto lo_val = mod(-b1.val() * a_inv, pow2);
auto hi = lo + 1;
auto hi_val = mod(lo_val + 1, pow2);
interval = to_interval(c, false, rational::one(), lo_val, lo, hi_val, hi);
return true;
}
return false;
}
/**
* Ad-hoc linear forbidden intervals
* ax <= b, b != -1, a < b: x not in [ceil((b+1)/a) .. floor((2^K-1)/a)]
* b <= ax, 0 < a < b: x not in [0 .. floor((b-1)/a)]
* ax < b, a < b: x not in [ceil(b/a) .. floor((2^K-1)/a)]
* b < ax, 0 < a <= b: x not in [0 .. floor(b/a)]
*
* TODO: generalize to ax + b <= c scenarios where ax does not overflow
* and ax+b does not overflow, but is larger than c
* Scenarios:
* - ax + b <= c
* - ax + b < c
* - c <= ax + b
* - c < ax + b
*/
bool forbidden_intervals::match_linear5(signed_constraint const& c,
rational & a1, pdd const& b1, pdd const& e1,
rational & a2, pdd const& b2, pdd const& e2,
eval_interval& interval, vector<signed_constraint>& side_cond) {
auto& m = e1.manager();
// ax <= b, b != -1, a < b: x not in [ceil((b+1)/a) .. floor((2^K-1)/a)]
if (c.is_positive() &&
!a1.is_zero() && !a1.is_one() &&
a2.is_zero() && b1.is_zero() && e2.is_val() &&
a1 < b2.val() && b2.val() != m.max_value()) {
if (!e1.is_val())
side_cond.push_back(s.eq(e1));
auto lo_val = ceil((b2.val() + 1) / a1);
auto hi_val = floor(m.max_value() / a1) + 1;
SASSERT(lo_val < hi_val);
auto lo = m.mk_val(lo_val);
auto hi = m.mk_val(hi_val);
interval = eval_interval::proper(lo, lo_val, hi, hi_val);
return true;
}
// b <= ax, 0 < a < b: x not in [0 .. floor((b-1)/a)]
if (c.is_positive() &&
!a2.is_zero() && !a2.is_one() &&
a1.is_zero() && b2.is_zero() &&
a2 < b1.val() && e1.is_val()) {
if (!e2.is_val())
side_cond.push_back(s.eq(e2));
rational lo_val = rational::zero();
rational hi_val = floor((b1.val() - 1) / a2) + 1;
SASSERT(lo_val < hi_val);
auto lo = m.mk_val(lo_val);
auto hi = m.mk_val(hi_val);
interval = eval_interval::proper(lo, lo_val, hi, hi_val);
return true;
}
// ax < b, a < b: x not in [ceil(b/a) .. floor((2^K-1)/a)]
if (c.is_negative() &&
!a2.is_zero() && !a2.is_one() && b2.is_zero() &&
a1.is_zero() && e1.is_val() && a2 < b1.val()) {
if (!e2.is_val())
side_cond.push_back(s.eq(e2));
rational lo_val = ceil(b1.val() / a2);
rational hi_val = floor(m.max_value() / a2) + 1;
auto lo = m.mk_val(lo_val);
auto hi = m.mk_val(hi_val);
interval = eval_interval::proper(lo, lo_val, hi, hi_val);
return true;
}
// b < ax, 0 < a <= b: x not in [0 .. floor(b/a)]
if (c.is_negative() &&
!a1.is_zero() && !a1.is_one() && b1.is_zero() &&
a2.is_zero() && e2.is_val() && a1 <= b2.val()) {
if (!e1.is_val())
side_cond.push_back(s.eq(e2));
rational lo_val = rational::zero();
rational hi_val = floor(b2.val() / a1) + 1;
auto lo = m.mk_val(lo_val);
auto hi = m.mk_val(hi_val);
interval = eval_interval::proper(lo, lo_val, hi, hi_val);
return true;
}
return false;
}
#endif
}

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

@ -31,33 +31,20 @@ namespace polysat {
std::tuple<bool, rational, pdd, pdd> linear_decompose(pvar v, pdd const& p, vector<signed_constraint>& out_side_cond);
bool match_linear1(signed_constraint const& c,
rational & a1, pdd const& b1, pdd const& e1,
rational const & a1, pdd const& b1, pdd const& e1,
rational const & a2, pdd const& b2, pdd const& e2,
eval_interval& interval, vector<signed_constraint>& side_cond);
rational& coeff, eval_interval& interval, vector<signed_constraint>& side_cond);
bool match_linear2(signed_constraint const& c,
rational & a1, pdd const& b1, pdd const& e1,
rational const & a1, pdd const& b1, pdd const& e1,
rational const & a2, pdd const& b2, pdd const& e2,
eval_interval& interval, vector<signed_constraint>& side_cond);
rational& coeff, eval_interval& interval, vector<signed_constraint>& side_cond);
bool match_linear3(signed_constraint const& c,
rational & a1, pdd const& b1, pdd const& e1,
rational const & a1, pdd const& b1, pdd const& e1,
rational const & a2, pdd const& b2, pdd const& e2,
eval_interval& interval, vector<signed_constraint>& side_cond);
rational& coeff, eval_interval& interval, vector<signed_constraint>& side_cond);
#if 0
bool match_linear4(signed_constraint const& c,
rational & a1, pdd const& b1, pdd const& e1,
rational & a2, pdd const& b2, pdd const& e2,
eval_interval& interval, vector<signed_constraint>& side_cond);
bool match_linear5(signed_constraint const& c,
rational & a1, pdd const& b1, pdd const& e1,
rational & a2, pdd const& b2, pdd const& e2,
eval_interval& interval, vector<signed_constraint>& side_cond);
#endif
// bool coefficient_is_01(dd::pdd_manager& m, rational const& r) { return r.is_zero() || r.is_one() || r == m.max_value(); };
public:
forbidden_intervals(solver& s) :s(s) {}
bool get_interval(signed_constraint const& c, pvar v, rational & coeff, eval_interval& out_interval, vector<signed_constraint>& side_cond);

22
src/math/polysat/viable.cpp
View file

@ -163,14 +163,20 @@ namespace polysat {
/**
* Traverse all interval constraints with coefficients to check whether current value 'val' for
* 'v' is feasible. If not, extract a (maximal) interval to block 'v' from being assigned val.
*
* To investigate:
* - side conditions are stronger than for unit intervals. They constrain the lower and upper bounds to
* be precisely the assigned values. This is to ensure that lo/hi that are computed based on lo_val
* and division with coeff are valid. Is there a more relaxed scheme?
*/
bool viable::refine_viable(pvar v, rational const& val) {
auto* e = m_non_units[v];
if (!e)
return true;
entry* first = e;
rational const& max_value = s.var2pdd(v).max_value();
do {
rational coeff_val = mod(e->coeff * val, s.var2pdd(v).max_value() + 1);
rational coeff_val = mod(e->coeff * val, max_value + 1);
if (e->interval.currently_contains(coeff_val)) {
rational delta_l = floor((coeff_val - e->interval.lo_val()) / e->coeff);
rational delta_u = floor((e->interval.hi_val() - coeff_val - 1) / e->coeff);
@ -181,21 +187,25 @@ namespace polysat {
// pass
}
else if (e->interval.lo_val() <= coeff_val) {
hi = val + 1;
if (hi > s.var2pdd(v).max_value())
rational lambda_u = floor((max_value - coeff_val - 1) / e->coeff);
hi = val + lambda_u + 1;
if (hi > max_value)
hi = 0;
}
else {
SASSERT(coeff_val < e->interval.hi_val());
lo = val;
rational lambda_l = floor(coeff_val / e->coeff);
lo = val - lambda_l;
}
SASSERT(hi <= s.var2pdd(v).max_value());
LOG("forbidden interval " << e->interval << " - " << val << " " << coeff_val << " [" << lo << ", " << hi << "[");
entry* ne = alloc_entry();
ne->src = e->src;
ne->side_cond = e->side_cond;
ne->side_cond.push_back(s.eq(e->interval.hi(), e->interval.hi_val()));
ne->side_cond.push_back(s.eq(e->interval.lo(), e->interval.lo_val()));
ne->coeff = 1;
pdd lop = s.var2pdd(v).mk_val(lo); // TODO?
pdd lop = s.var2pdd(v).mk_val(lo);
pdd hip = s.var2pdd(v).mk_val(hi);
ne->interval = eval_interval::proper(lop, lo, hip, hi);
intersect(v, ne);
@ -435,7 +445,7 @@ namespace polysat {
do {
if (e->coeff != 1)
out << e->coeff << " * v" << v << " ";
out << e->interval << " " << e->side_cond << " " << e->src << " ";
out << e->interval << " " << e->side_cond << " " << e->src << "; ";
e = e->next();
}
while (e != first);