mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

slicing-conflict debug output

Browse source
This commit is contained in:
Jakob Rath 2023-08-08 16:05:24 +02:00
parent 46a794ff67
commit 5ec11c591f
1 changed files with 22 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

22
src/math/polysat/slicing.cpp
View file

@ -646,6 +646,7 @@ namespace polysat {
}
else if (y == null_var) {
UNREACHABLE();
/*
SASSERT(is_value(sx->get_root()));
// the egraph has derived that x (or a sub-slice thereof) must have value b that differs from the currently assigned value of x.
// the explanation is: lits ==> x[...] = b
@ -689,9 +690,30 @@ namespace polysat {
// otherwise, we will generate tautologies in this branch.
}
}
*/
}
else {
SASSERT(x != y);
unsigned x_hi, x_lo, y_hi, y_lo;
VERIFY(find_range_in_ancestor(sx, var2slice(x), x_hi, x_lo));
VERIFY(find_range_in_ancestor(sy, var2slice(y), y_hi, y_lo));
LOG("find_range_in_ancestor: v" << x << "[" << x_hi << ":" << x_lo << "] = " << slice_pp(*this, sx) << ", slice-value " << get_value(sx->get_root()));
LOG("find_range_in_ancestor: v" << y << "[" << y_hi << ":" << y_lo << "] = " << slice_pp(*this, sy) << ", slice-value " << get_value(sy->get_root()));
if (m_solver.is_assigned(x)) {
rational sval = mod2k(machine_div2k(m_solver.get_value(x), x_lo), x_hi - x_lo + 1);
LOG("Variable v" << x << " has solver-value " << m_solver.get_value(x) << ", i.e., v" << x << "[" << x_hi << ":" << x_lo << "] = " << sval);
}
if (m_solver.is_assigned(y)) {
rational sval = mod2k(machine_div2k(m_solver.get_value(y), y_lo), y_hi - y_lo + 1);
LOG("Variable v" << y << " has solver-value " << m_solver.get_value(y) << ", i.e., v" << y << "[" << y_hi << ":" << y_lo << "] = " << sval);
}
std::abort();
// below is TODO
// LOG("Slice sx=" << slice_pp(*this, sx) << " has value " << get_value(sx->get_root()));
// LOG("Slice sy=" << slice_pp(*this, sy) << " has value " << get_value(sy->get_root()));
// the egraph has derived that x (or a subslice of x) must be equal to y (or a subslice of y),
// but the currently assigned values differ.
// the explanation is: lits ==> x[...] = y[...]