mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-30 04:15:51 +00:00
Code Activity

fix #4359 and regression to #3270

Browse source
This commit is contained in:
Nikolaj Bjorner 2020-05-18 12:41:42 -07:00
parent 1c760b04cf
commit 78a4717c06
4 changed files with 37 additions and 29 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/math/interval/dep_intervals.cpp
View file

@ -101,12 +101,16 @@ std::ostream& dep_intervals::display(std::ostream& out, const interval& i) const
out << rational(m_imanager.upper(i)) << (m_imanager.upper_is_open(i)? ")":"]");
}
if (i.m_lower_dep) {
// out << "\nlower deps\n";
// TBD: print_dependencies(i.m_lower_dep, out);
vector<unsigned, false> ex;
linearize(i.m_lower_dep, ex);
out << " ld";
for (unsigned d : ex) out << " " << d;
}
if (i.m_upper_dep) {
// out << "\nupper deps\n";
// TBD: print_dependencies(i.m_upper_dep, out);
vector<unsigned, false> ex;
linearize(i.m_upper_dep, ex);
out << " ud";
for (unsigned d : ex) out << " " << d;
}
return out;
}

25
src/math/interval/dep_intervals.h
View file

@ -55,13 +55,17 @@ private:
};
void add_deps(interval const& a, interval const& b, interval_deps_combine_rule const& deps, interval& i) const {
i.m_lower_dep = lower_is_inf(i) ? nullptr : mk_dependency(a, b, deps.m_lower_combine);
i.m_upper_dep = upper_is_inf(i) ? nullptr : mk_dependency(a, b, deps.m_upper_combine);
auto lower_dep = lower_is_inf(i) ? nullptr : mk_dependency(a, b, deps.m_lower_combine);
auto upper_dep = upper_is_inf(i) ? nullptr : mk_dependency(a, b, deps.m_upper_combine);
i.m_lower_dep = lower_dep;
i.m_upper_dep = upper_dep;
}
void add_deps(interval const& a, interval_deps_combine_rule const& deps, interval& i) const {
i.m_lower_dep = lower_is_inf(i) ? nullptr : mk_dependency(a, deps.m_lower_combine);
i.m_upper_dep = upper_is_inf(i) ? nullptr : mk_dependency(a, deps.m_upper_combine);
auto lower_dep = lower_is_inf(i) ? nullptr : mk_dependency(a, deps.m_lower_combine);
auto upper_dep = upper_is_inf(i) ? nullptr : mk_dependency(a, deps.m_upper_combine);
i.m_lower_dep = lower_dep;
i.m_upper_dep = upper_dep;
}
@ -221,14 +225,13 @@ public:
if (r.is_zero()) return;
m_imanager.mul(r.to_mpq(), a, b);
if (wd == with_deps) {
if (r.is_pos()) {
b.m_lower_dep = a.m_lower_dep;
b.m_upper_dep = a.m_upper_dep;
}
else {
b.m_upper_dep = a.m_lower_dep;
b.m_lower_dep = a.m_upper_dep;
auto lower_dep = a.m_lower_dep;
auto upper_dep = a.m_upper_dep;
if (!r.is_pos()) {
std::swap(lower_dep, upper_dep);
}
b.m_lower_dep = lower_dep;
b.m_upper_dep = upper_dep;
}
}

27
src/math/lp/monomial_bounds.cpp
View file

@ -17,13 +17,11 @@ namespace nla {
common(c),
dep(c->m_intervals.get_dep_intervals()) {}
bool monomial_bounds::operator()() {
bool propagated = false;
void monomial_bounds::operator()() {
for (lpvar v : c().m_to_refine) {
monic const& m = c().emons()[v];
propagated |= propagate(m);
propagate(m);
}
return propagated;
}
/**
@ -88,10 +86,10 @@ namespace nla {
bool monomial_bounds::propagate_value(dep_interval& range, lpvar v, unsigned p) {
SASSERT(p > 0);
if (p == 1)
if (p == 1)
return propagate_value(range, v);
auto val = c().val(v);
val = power(val, p);
auto val_v = c().val(v);
auto val = power(val_v, p);
rational r;
if (dep.is_below(range, val)) {
lp::explanation ex;
@ -101,21 +99,24 @@ namespace nla {
lemma &= ex;
return true;
}
if (rational(dep.upper(range)).root(p, r)) {
{
else if (rational(dep.upper(range)).root(p, r)) {
// v = -2, [-4,-3]^3 < v^3 -> add bound v <= -3
// v = -2, [-1,+1]^2 < v^2 -> add bound v >= -1
if ((p % 2 == 1) || val_v.is_pos()) {
auto le = dep.upper_is_open(range) ? llc::LT : llc::LE;
new_lemma lemma(c(), "propagate value - root case - lower bound of range is below value");
new_lemma lemma(c(), "propagate value - root case - upper bound of range is below value");
lemma &= ex;
lemma |= ineq(v, le, r);
return true;
}
if (p % 2 == 0) {
if (p % 2 == 0 && val_v.is_neg()) {
SASSERT(!r.is_neg());
auto ge = dep.upper_is_open(range) ? llc::GT : llc::GE;
new_lemma lemma(c(), "propagate value - root case - lower bound of range is below value");
new_lemma lemma(c(), "propagate value - root case - upper bound of range is below negative value");
lemma &= ex;
lemma |= ineq(v, ge, -r);
return true;
}
return true;
}
// TBD: add bounds as long as difference to val is above some epsilon.
}

2
src/math/lp/monomial_bounds.h
View file

@ -28,6 +28,6 @@ namespace nla {
bool is_zero(lpvar v) const;
public:
monomial_bounds(core* core);
bool operator()();
void operator()();
};
}