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

debugging #5127

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-04-06 20:06:51 -07:00
parent e5e663e874
commit 0b0efa83ca
3 changed files with 23 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -214,7 +214,7 @@ public:
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 << " for v=";
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);
@ -281,11 +281,11 @@ public:
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 between: v = "; print(tout , v) << "\nand u = "; print(tout, u) << "\n";);
TRACE("cheap_eq", 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());
});
TRACE("cheap_eq",
tout << "polarity switch: " << 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()););
}
@ -379,7 +379,7 @@ 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(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";);
@ -447,7 +447,9 @@ public:
SASSERT(j != k);
unsigned je = lp().column_to_reported_index(j);
unsigned ke = lp().column_to_reported_index(k);
TRACE("cheap_eq", tout << "reporting eq " << j << ", " << k << "\n";
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());
}

14
src/smt/smt_context_pp.cpp
View file

@ -220,12 +220,22 @@ namespace smt {
void context::display_assignment(std::ostream & out) const {
if (!m_assigned_literals.empty()) {
out << "current assignment:\n";
unsigned level = 0;
for (literal lit : m_assigned_literals) {
display_literal(out, lit);
if (level < get_assign_level(lit.var())) {
level = get_assign_level(lit.var());
out << "level " << level << "\n";
}
display_literal(out << lit << " ", lit);
if (!is_relevant(lit)) out << " n ";
out << ": ";
display_verbose(out, m, 1, &lit, m_bool_var2expr.c_ptr());
out << "\n";
if (level > 0) {
auto j = get_justification(lit.var());
display(out << " ", j);
}
else
out << "\n";
}
}
}

1
src/smt/theory_seq.cpp
View file

@ -2811,6 +2811,7 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
expr_ref f(m);
literal lit(v, !is_true);
TRACE("seq", tout << (is_true?"":"not ") << mk_bounded_pp(e, m) << "\n";);
TRACE("seq", tout << (is_true?"":"not ") << mk_bounded_pp(e, m) << " " << ctx.get_scope_level() << " " << lit << "\n";);
if (m_util.str.is_prefix(e, e1, e2)) {
if (is_true) {