mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 03:07:07 +00:00
Code Activity

provisionary fix for #5127

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-04-06 22:32:22 -07:00
parent dcfd9c859d
commit 46831e7ebb
1 changed files with 24 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

38
src/math/lp/lp_bound_propagator.h
View file

@ -103,12 +103,14 @@ class lp_bound_propagator {
// x[m_root->column()] - m_pol[j].pol()*x[j] == const;
// to bind polarity and the vertex in the table
struct pol_vert {
int m_polarity;
const vertex* m_v;
pol_vert() {}
pol_vert(int p, const vertex* v): m_polarity(p), m_v(v) {}
int m_polarity { -2 };
unsigned m_row_index { 0 };
const vertex* m_v { nullptr };
pol_vert() {}
pol_vert(int p, unsigned r, const vertex* v): m_polarity(p), m_row_index(r), m_v(v) {}
int pol() const { return m_polarity; }
const vertex* v() const { return m_v; }
unsigned row() const { return m_row_index; }
};
u_map<pol_vert> m_pol;
// if m_pos.contains(j) then x[j] = x[m_root->column()] + o
@ -258,21 +260,29 @@ public:
// pol for polarity
int pol(const vertex* v) const { return pol(v->column()); }
int pol(unsigned j) const { return m_pol[j].pol(); }
void set_polarity(const vertex* v, int p) {
void set_polarity(const vertex* v, unsigned r, int p) {
SASSERT(p == 1 || p == -1);
unsigned j = v->column();
SASSERT(!m_pol.contains(j));
m_pol.insert(j, pol_vert(p, v));
m_pol.insert(j, pol_vert(p, r, v));
}
void check_and_set_polarity(vertex* v, int polarity, unsigned row_index) {
pol_vert prev_pol;
if (!m_pol.find(v->column(), prev_pol)) {
set_polarity(v, polarity);
set_polarity(v, row_index, polarity);
return;
}
if (prev_pol.pol() == polarity)
return;
return;
//
// TODO disabled pending fix for #5127
// the explanation is missing some terms.
// Probably because in this case there isn't a single, but two paths
// from u to v. The bounds for the fixed variables for the two paths
// have to be taken into account.
//
const vertex *u = prev_pol.v();
// we have a path L between u and v with p(L) = -1, that means we can
// create an equality of the form x + x = a, where x = v->column() = u->column()
@ -282,7 +292,7 @@ public:
explain_fixed_in_row(row_index, m_fixed_vertex_explanation);
set_fixed_vertex(v);
TRACE("cheap_eq",
tout << "polarity switch: " << polarity << "\nv = "; print(tout , v) << "\nu = "; print(tout, u) << "\n";
tout << "polarity switch: " << row_index << " pol: " << polarity << "\nv = "; print(tout , v) << "\nu = "; print(tout, u) << "\n";
tout << "fixed vertex explanation\n";
for (auto p : m_fixed_vertex_explanation)
lp().constraints().display(tout, [this](lpvar j) { return lp().get_variable_name(j);}, p.ci()););
@ -316,7 +326,7 @@ public:
}
TRACE("cheap_eq", print_row(tout, row_index););
m_root = alloc_v(x);
set_polarity(m_root, 1); // keep m_root in the positive table
set_polarity(m_root, row_index, 1); // keep m_root in the positive table
if (not_set(y)) {
set_fixed_vertex(m_root);
explain_fixed_in_row(row_index, m_fixed_vertex_explanation);
@ -482,14 +492,14 @@ public:
}
void explain_fixed_in_row(unsigned row, explanation& ex) const {
for (const auto & c : lp().get_row(row)) {
if (lp().is_fixed(c.var())) {
TRACE("cheap_eq", tout << "explain-row " << row << "\n";);
for (const auto & c : lp().get_row(row))
if (lp().is_fixed(c.var()))
explain_fixed_column(c.var(), ex);
}
}
}
void explain_fixed_column(unsigned j, explanation & ex) const {
TRACE("cheap_eq", tout << "explain-column " << j << "\n";);
SASSERT(column_is_fixed(j));
constraint_index lc, uc;
lp().get_bound_constraint_witnesses_for_column(j, lc, uc);
@ -547,7 +557,7 @@ public:
out << "\nchildren :\n";
for (auto c : v->edges()) {
out << "row = ";
print_row(out, c.row());
print_row(out << c.row() << ": ", c.row());
print_tree(out, c.target());
}
return out;