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

debug tighten_bounds

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-03-07 07:58:13 -08:00
parent e1cb1bc326
commit a7e4a3a2be
2 changed files with 17 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1489,7 +1489,7 @@ namespace lp {
protected_queue q; protected_queue q;
copy_row_to_espace(h); copy_row_to_espace(h);
remove_fresh_from_espace(); remove_fresh_from_espace();
// change m_espace indices from local to lar_solver: have to restore for clear to work // change m_espace indices from local to lar_solver: have to restore for clear to work
for (auto & p: m_espace.m_data) { for (auto & p: m_espace.m_data) {
SASSERT(!var_is_fresh(p.m_j)); SASSERT(!var_is_fresh(p.m_j));
@ -1506,12 +1506,7 @@ namespace lp {
TRACE("dio", tout <<"no new bounds\n";); TRACE("dio", tout <<"no new bounds\n";);
return lia_move::undef; return lia_move::undef;
} }
TRACE("dio", tout << "prop_bounds:\n"; TRACE("dio", tout << "prop_bounds:\n"; for (auto& pb: m_prop_bounds) print_prop_bound(pb, tout););
for (auto& pb: m_prop_bounds) {
print_prop_bound(pb, tout);
});
if (m_prop_bounds.size() == 0)
return lia_move::undef;
u_dependency * dep = explain_fixed_in_meta_term(m_l_matrix.m_rows[h]); u_dependency * dep = explain_fixed_in_meta_term(m_l_matrix.m_rows[h]);
bool change = false; bool change = false;
for (auto& pb: m_prop_bounds) { for (auto& pb: m_prop_bounds) {
@ -1639,10 +1634,11 @@ namespace lp {
} }
return ret; return ret;
} }
impq get_term_value(const lar_term& t) const {
impq ret; mpq get_term_value(const term_o& t) const {
mpq ret = t.c();
for (const auto& p : t) { for (const auto& p : t) {
ret += p.coeff() * lra.get_column_value(p.j()); ret += p.coeff() * lra.get_column_value(p.var()).x;
} }
return ret; return ret;
} }
@ -2466,6 +2462,7 @@ namespace lp {
bool entry_invariant(unsigned ei) const { bool entry_invariant(unsigned ei) const {
if (lra.settings().get_cancel_flag()) if (lra.settings().get_cancel_flag())
return true; return true;
for (const auto& p : m_e_matrix.m_rows[ei]) { for (const auto& p : m_e_matrix.m_rows[ei]) {
if (!p.coeff().is_int()) { if (!p.coeff().is_int()) {
return false; return false;
@ -2480,9 +2477,13 @@ namespace lp {
} }
} }
bool ret = term_o ls = term_to_lar_solver(remove_fresh_vars(get_term_from_entry(ei)));
term_to_lar_solver(remove_fresh_vars(get_term_from_entry(ei))) == mpq ls_val = get_term_value(ls);
fix_vars(open_ml(m_l_matrix.m_rows[ei])); if (!ls_val.is_zero()) {
std::cout << "ls_val is not zero\n";
return false;
}
bool ret = ls == fix_vars(open_ml(m_l_matrix.m_rows[ei]));
if (!ret) { if (!ret) {
enable_trace("dio"); enable_trace("dio");
CTRACE("dio", !ret, CTRACE("dio", !ret,

5
src/smt/theory_lra.cpp
View file

@ -3452,11 +3452,12 @@ public:
set_evidence(ev.ci(), m_core, m_eqs); set_evidence(ev.ci(), m_core, m_eqs);
if (params().m_arith_validate)
VERIFY(validate_conflict());
if (params().m_arith_dump_lemmas) if (params().m_arith_dump_lemmas)
dump_conflict(); dump_conflict();
if (params().m_arith_validate)
VERIFY(validate_conflict());
if (is_conflict) { if (is_conflict) {
ctx().set_conflict( ctx().set_conflict(
ctx().mk_justification( ctx().mk_justification(