mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 17:45:32 +00:00
Code Activity

chasing interval bug

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-12-03 07:49:17 -08:00
parent ff22b433cc
commit eda3cac8d4
2 changed files with 39 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/math/dd/dd_pdd.cpp
View file

@ -1685,7 +1685,7 @@ namespace dd {
if (require_parens)
out << ")";
return out;
} else
} else
return out << m.normalize(val);
}

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

@ -127,6 +127,8 @@ namespace polysat {
return true;
}
static char* _last_function = "";
bool forbidden_intervals::get_interval_ule(signed_constraint const& c, pvar v, fi_record& fi) {
@ -135,6 +137,26 @@ namespace polysat {
fi.coeff = 1;
fi.src = c;
struct show {
forbidden_intervals& f;
signed_constraint const& c;
pvar v;
fi_record& fi;
backtrack& _backtrack;
show(forbidden_intervals& f,
signed_constraint const& c,
pvar v,
fi_record& fi,
backtrack& _backtrack):f(f), c(c), v(v), fi(fi), _backtrack(_backtrack) {}
~show() {
if (!_backtrack.released)
return;
IF_VERBOSE(0, verbose_stream() << _last_function << " " << v << " " << c << " " << fi.interval << " " << fi.side_cond << "\n");
}
};
// uncomment to trace intervals
// show _show(*this, c, v, fi, _backtrack);
// eval(lhs) = a1*v + eval(e1) = a1*v + b1
// eval(rhs) = a2*v + eval(e2) = a2*v + b2
// We keep the e1, e2 around in case we need side conditions such as e1=b1, e2=b2.
@ -261,12 +283,19 @@ namespace polysat {
/**
* Match e1 + t <= e2, with t = a1*y
* condition for empty/full: e2 == -1
* condition for empty/full: e2 == -1
*/
// NSB - bug?
// what happens when a1 != 1 and a1 != -1?
// if a1 is even is this still correct?
// example: match_linear1 12 v81 + -1*v20*v12 == 0 [v81 + 1 ; v81[ := [1;0[ v20 + -532 == 0 v81 == 0
// from bench25.smt2
//
bool forbidden_intervals::match_linear1(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) {
_last_function = __func__;
if (a2.is_zero() && !a1.is_zero()) {
SASSERT(!a1.is_zero());
bool is_trivial = (b2 + 1).is_zero();
@ -291,6 +320,7 @@ namespace polysat {
rational const & a1, pdd const& b1, pdd const& e1,
rational const & a2, pdd const& b2, pdd const& e2,
fi_record& fi) {
_last_function = __func__;
if (a1.is_zero() && !a2.is_zero()) {
SASSERT(!a2.is_zero());
bool is_trivial = b1.is_zero();
@ -315,6 +345,7 @@ namespace polysat {
rational const & a1, pdd const& b1, pdd const& e1,
rational const & a2, pdd const& b2, pdd const& e2,
fi_record& fi) {
_last_function = __func__;
if (a1 == a2 && !a1.is_zero()) {
bool is_trivial = b1.val() == b2.val();
push_eq(is_trivial, e1 - e2, fi.side_cond);
@ -337,6 +368,7 @@ namespace polysat {
rational const & a1, pdd const& b1, pdd const& e1,
rational const & a2, pdd const& b2, pdd const& e2,
fi_record& fi) {
_last_function = __func__;
if (a1 != a2 && !a1.is_zero() && !a2.is_zero()) {
// NOTE: we don't have an interval here in the same sense as in the other cases.
// We use the interval to smuggle out the values a1,b1,a2,b2 without adding additional fields.
@ -368,6 +400,7 @@ namespace polysat {
rational const & a1, pdd const& b1, pdd const& e1,
rational const & a2, pdd const& b2, pdd const& e2,
fi_record& fi) {
_last_function = __func__;
if (c.is_positive() && a1.is_odd() && b1.is_zero() && a2.is_zero() && b2.is_zero()) {
auto& m = e1.manager();
rational lo_val(1);
@ -380,6 +413,7 @@ namespace polysat {
fi.side_cond.push_back(s.eq(b1, e1));
if (b2 != e2)
fi.side_cond.push_back(s.eq(b2, e2));
IF_VERBOSE(0, verbose_stream() << fi.interval << " " << fi.side_cond << "\n");
return true;
}
return false;
@ -397,6 +431,7 @@ namespace polysat {
rational const & a1, pdd const& b1, pdd const& e1,
rational const & a2, pdd const& b2, pdd const& e2,
fi_record& fi) {
_last_function = __func__;
if (c.is_negative() && a1.is_odd() && a2.is_zero() && b2.is_zero()) {
// a*v + b > 0
// <=> a*v + b != 0
@ -435,6 +470,7 @@ namespace polysat {
signed_constraint const& c,
rational const & a1, pdd const& b1, pdd const& e1,
fi_record& fi) {
_last_function = __func__;
if (a1.is_odd() && b1.is_zero() && c.is_negative()) {
auto& m = e1.manager();
rational lo_val(0);
@ -475,6 +511,7 @@ namespace polysat {
signed_constraint const& c,
rational const & a2, pdd const& b2, pdd const& e2,
fi_record& fi) {
_last_function = __func__;
if (a2.is_one() && b2.is_val() && c.is_negative()) {
auto& m = e2.manager();
rational const& mod_value = m.two_to_N();