mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

debug issue 5127

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2021-04-08 13:25:18 -07:00
parent a5f957afb3
commit 18610bf31f
2 changed files with 64 additions and 56 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -70,18 +70,17 @@ class lp_bound_propagator {
};
static int other(int x, int y, int z) { SASSERT(x == z || y == z); return x == z ? y : x; }
std::ostream& print(std::ostream & out, const vertex* v) const {
out << "c = " << v->column() << ", P = {";
std::ostream& print_vert(std::ostream & out, const vertex* v) const {
out << "(c = " << v->column() << ", parent = {";
if (v->parent()) { out << "(" << v->parent()->column() << ")";}
else { out << "null"; }
out << "} , lvl = " << v->level();
if (fixed_phase()) {
out << " fixed phase";
} if (m_pol.contains(v->column())) {
if (m_pol.contains(v->column())) {
out << (pol(v) == -1? " -":" +");
} else {
out << " not in m_pol";
}
out << ')';
return out;
}
@ -103,14 +102,12 @@ 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 { -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 m_polarity;
const vertex* m_v;
pol_vert() {}
pol_vert(int p, const vertex* v): m_polarity(p), 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
@ -211,18 +208,31 @@ public:
}
void try_add_equation_with_lp_fixed_tables(const vertex *v) {
static int count = 0;
std::cout << ++count << std::endl;
if (count == 21)
enable_trace("cheap_eq");
SASSERT(m_fixed_vertex);
unsigned v_j = v->column();
unsigned j = null_lpvar;
if (!lp().find_in_fixed_tables(val(v_j), is_int(v_j), j))
return;
TRACE("cheap_eq", tout << "found j = " << j << " v_j = " << v_j << " for v = ";
print(tout, v) << "\n in lp.fixed tables\n";);
vector<edge> path;
find_path_on_tree(path, v, m_fixed_vertex);
TRACE("cheap_eq", tout << "v_j = "; lp().print_column_info(v_j, tout) << std::endl;);
TRACE("cheap_eq", tout << "v = "; print_vert(tout, v) << std::endl;);
TRACE("cheap_eq", tout << "found j " << j << std::endl;
lp().print_column_info(j, tout)<< std::endl;);
TRACE("cheap_eq", tout << "found j = " << j << std::endl;);
vector<edge> path = connect_u_v_in_tree(v, m_fixed_vertex);
explanation ex = get_explanation_from_path(path);
TRACE("cheap_eq", tout << "path expl = \n"; print_expl(tout, ex) << std::endl;);
TRACE("cheap_eq", tout << "fixed vert= \n"; print_vert(tout, m_fixed_vertex) << std::endl;);
TRACE("cheap_eq", tout << "fix vert expl = \n"; print_expl(tout, m_fixed_vertex_explanation) << std::endl;);
ex.add_expl(m_fixed_vertex_explanation);
explain_fixed_column(j, ex);
TRACE("cheap_eq", tout << "full expl = \n"; print_expl(tout, ex) << std::endl;);
add_eq_on_columns(ex, j, v->column());
}
void try_add_equation_with_val_table(const vertex *v) {
@ -238,9 +248,8 @@ public:
return;
TRACE("cheap_eq", tout << "found j=" << j << " for v=";
print(tout, v) << "\n in m_vals_to_verts\n";);
vector<edge> path;
find_path_on_tree(path, u, v);
print_vert(tout, v) << "\n in m_vals_to_verts\n";);
vector<edge> path = connect_u_v_in_tree(u, v);
explanation ex = get_explanation_from_path(path);
ex.add_expl(m_fixed_vertex_explanation);
add_eq_on_columns(ex, j, v_j);
@ -260,39 +269,30 @@ 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, unsigned r, int p) {
void set_polarity(const vertex* v, int p) {
SASSERT(p == 1 || p == -1);
unsigned j = v->column();
SASSERT(!m_pol.contains(j));
m_pol.insert(j, pol_vert(p, r, v));
m_pol.insert(j, pol_vert(p, 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, row_index, polarity);
set_polarity(v, 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()
vector<edge> path;
find_path_on_tree(path, u, v);
vector<edge> path = connect_u_v_in_tree(u, v);
m_fixed_vertex_explanation = get_explanation_from_path(path);
explain_fixed_in_row(row_index, m_fixed_vertex_explanation);
set_fixed_vertex(v);
TRACE("cheap_eq",
tout << "polarity switch: " << row_index << " pol: " << polarity << "\nv = "; print(tout , v) << "\nu = "; print(tout, u) << "\n";
tout << "polarity switch: " << polarity << "\nv = "; print_vert(tout , v) << "\nu = "; print_vert(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()););
@ -326,7 +326,7 @@ public:
}
TRACE("cheap_eq", print_row(tout, row_index););
m_root = alloc_v(x);
set_polarity(m_root, row_index, 1); // keep m_root in the positive table
set_polarity(m_root, 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);
@ -389,10 +389,10 @@ public:
}
void check_for_eq_and_add_to_val_table(vertex* v, map<mpq, const vertex*, obj_hash<mpq>, default_eq<mpq>>& table) {
TRACE("cheap_eq", tout << "v = "; print(tout, v) << "\n";);
TRACE("cheap_eq", tout << "v = "; print_vert(tout, v) << "\n";);
const vertex *k; // the other vertex
if (table.find(val(v), k)) {
TRACE("cheap_eq", tout << "found k " ; print(tout, k) << "\n";);
TRACE("cheap_eq", tout << "found k " ; print_vert(tout, k) << "\n";);
if (k->column() != v->column() &&
is_int(k->column()) == is_int(v->column()) &&
!is_equal(k->column(), v->column())) {
@ -401,13 +401,13 @@ public:
TRACE("cheap_eq", tout << "no report\n";);
}
} else {
TRACE("cheap_eq", tout << "registered: " << val(v) << " -> { "; print(tout, v) << "} \n";);
TRACE("cheap_eq", tout << "registered: " << val(v) << " -> { "; print_vert(tout, v) << "} \n";);
table.insert(val(v), v);
}
}
void check_for_eq_and_add_to_val_tables(vertex* v) {
TRACE("cheap_eq_det", print(tout, v) << "\n";);
TRACE("cheap_eq_det", print_vert(tout, v) << "\n";);
if (!fixed_phase()) {
if (pol(v->column()) == -1)
check_for_eq_and_add_to_val_table(v, m_vals_to_verts_neg);
@ -443,16 +443,22 @@ public:
SASSERT(v_i != v_j);
SASSERT(lp().get_column_value(v_i->column()) == lp().get_column_value(v_j->column()));
TRACE("cheap_eq", tout << v_i->column() << " = " << v_j->column() << "\nu = ";
print(tout, v_i) << "\nv = "; print(tout, v_j) <<"\n";
print_vert(tout, v_i) << "\nv = "; print_vert(tout, v_j) <<"\n";
);
vector<edge> path;
find_path_on_tree(path, v_i, v_j);
vector<edge> path = connect_u_v_in_tree(v_i, v_j);
lp::explanation exp = get_explanation_from_path(path);
add_eq_on_columns(exp, v_i->column(), v_j->column());
}
std::ostream& print_expl(std::ostream & out, const explanation& exp) const {
for (auto p : exp) {
lp().constraints().display(out, [this](lpvar j) { return lp().get_variable_name(j);}, p.ci());
}
return out;
}
void add_eq_on_columns(const explanation& exp, lpvar j, lpvar k) {
SASSERT(j != k);
unsigned je = lp().column_to_reported_index(j);
@ -460,10 +466,8 @@ public:
TRACE("cheap_eq",
tout << "reporting eq " << j << ", " << k << "\n";
tout << "reported idx " << je << ", " << ke << "\n";
for (auto p : exp) {
lp().constraints().display(tout, [this](lpvar j) { return lp().get_variable_name(j);}, p.ci());
}
tout << "theory_vars v" << lp().local_to_external(je) << " == v" << lp().local_to_external(ke) << "\n";
print_expl(tout, exp);
tout << "theory_vars v" << lp().local_to_external(je) << " == v" << lp().local_to_external(ke) << "\n";
);
m_imp.add_eq(je, ke, exp);
@ -492,14 +496,17 @@ public:
}
void explain_fixed_in_row(unsigned row, explanation& ex) const {
TRACE("cheap_eq", tout << "explain-row " << row << "\n";);
for (const auto & c : lp().get_row(row))
if (lp().is_fixed(c.var()))
TRACE("cheap_eq",
tout << lp().get_row(row) << std::endl;
);
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);
@ -507,8 +514,9 @@ public:
ex.push_back(uc);
}
void find_path_on_tree(vector<edge> & path, const vertex* u, const vertex* v) const {
TRACE("cheap_eq_details", tout << "u = " ; print(tout, u); tout << "\nv = ";print(tout, v) << "\n";);
vector<edge> connect_u_v_in_tree(const vertex* u, const vertex* v) const {
vector<edge> path;
TRACE("cheap_eq_details", tout << "u = " ; print_vert(tout, u); tout << "\nv = ";print_vert(tout, v) << "\n";);
vector<edge> v_branch;
// equalize the levels
while (u->level() > v->level()) {
@ -521,18 +529,18 @@ public:
v = v->parent();
}
SASSERT(u->level() == v->level());
TRACE("cheap_eq_details", tout << "u = " ; print(tout, u); tout << "\nv = "; print(tout, v) << "\n";);
TRACE("cheap_eq_details", tout << "u = " ; print_vert(tout, u); tout << "\nv = "; print_vert(tout, v) << "\n";);
while (u != v) {
path.push_back(u->edge_from_parent().reverse());
v_branch.push_back(v->edge_from_parent());
u = u->parent();
v = v->parent();
}
for (unsigned i = v_branch.size(); i--; ) {
path.push_back(v_branch[i]);
}
TRACE("cheap_eq", print_path(path, tout););
return path;
}
bool tree_is_correct() const {
@ -553,11 +561,11 @@ public:
return true;
}
std::ostream& print_tree(std::ostream & out, vertex* v) const {
print(out, v);
print_vert(out, v);
out << "\nchildren :\n";
for (auto c : v->edges()) {
out << "row = ";
print_row(out << c.row() << ": ", c.row());
print_row(out, c.row());
print_tree(out, c.target());
}
return out;
@ -625,7 +633,7 @@ public:
}
void set_fixed_vertex(vertex *v) {
TRACE("cheap_eq", if (v) print(tout, v); else tout << "set m_fixed_vertex to nullptr"; tout << "\n";);
TRACE("cheap_eq", if (v) print_vert(tout, v); else tout << "set m_fixed_vertex to nullptr"; tout << "\n";);
SASSERT(!m_fixed_vertex || v == nullptr);
m_fixed_vertex = v;
}

2
src/smt/theory_lra.cpp
View file

@ -3052,7 +3052,7 @@ public:
scoped_trace_stream _sts(th, fn);
// SASSERT(validate_eq(x, y));
SASSERT(validate_eq(x, y));
ctx().assign_eq(x, y, eq_justification(js));
}