mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-01 22:57:51 +00:00
Code Activity

catch a conflict with a fractional sum of fixed variables in a term

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-12-30 16:09:24 -10:00 • committed by Nikolaj Bjorner
parent cf287e6a64
commit 0da98c1378
1 changed files with 24 additions and 23 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -929,12 +929,10 @@ namespace lp {
unsigned j = m_q.pop_front(); unsigned j = m_q.pop_front();
mpq alpha = get_coeff_in_e_row(ei, j); mpq alpha = get_coeff_in_e_row(ei, j);
if (alpha.is_zero()) continue; if (alpha.is_zero()) continue;
if (m_k2s.has_key(j)) { if (m_k2s.has_key(j))
substitute_on_q_with_entry_in_S(ei, j, alpha); substitute_on_q_with_entry_in_S(ei, j, alpha);
} else
else {
substitute_with_fresh_def(ei, j, alpha); substitute_with_fresh_def(ei, j, alpha);
}
} }
} }
bool term_is_in_range(const lar_term& t) const { bool term_is_in_range(const lar_term& t) const {
@ -952,6 +950,7 @@ namespace lp {
// adds entry i0 multiplied by coeff to entry i1 // adds entry i0 multiplied by coeff to entry i1
void add_two_entries(const mpq& coeff, unsigned i0, unsigned i1) { void add_two_entries(const mpq& coeff, unsigned i0, unsigned i1) {
SASSERT(coeff.is_int());
m_e_matrix.add_rows(coeff, i0, i1); m_e_matrix.add_rows(coeff, i0, i1);
m_l_matrix.add_rows(coeff, i0, i1); m_l_matrix.add_rows(coeff, i0, i1);
m_sum_of_fixed[i1] += coeff * m_sum_of_fixed[i0]; m_sum_of_fixed[i1] += coeff * m_sum_of_fixed[i0];
@ -966,7 +965,7 @@ namespace lp {
} }
void recalculate_entry(unsigned ei) { void recalculate_entry(unsigned ei) {
TRACE(dio, print_entry(ei, tout) << std::endl;); TRACE(dio, print_entry(ei, tout, true) << std::endl;);
mpq& fixed_sum = m_sum_of_fixed[ei]; mpq& fixed_sum = m_sum_of_fixed[ei];
fixed_sum = mpq(0); fixed_sum = mpq(0);
open_l_term_to_espace(ei, fixed_sum); open_l_term_to_espace(ei, fixed_sum);
@ -985,9 +984,10 @@ namespace lp {
m_l_matrix.multiply_row(ei, denom); m_l_matrix.multiply_row(ei, denom);
m_e_matrix.multiply_row(ei, denom); m_e_matrix.multiply_row(ei, denom);
} }
if (belongs_to_s(ei)) { if (belongs_to_s(ei))
remove_from_S(ei); remove_from_S(ei);
} TRACE(dio, tout << "recalculated entry:\n"; print_entry(ei, tout, true) << std::endl;);
} }
void find_changed_terms_and_more_changed_rows() { void find_changed_terms_and_more_changed_rows() {
@ -1220,13 +1220,13 @@ namespace lp {
// The function returns true if and only if there is no conflict. // The function returns true if and only if there is no conflict.
bool normalize_e_by_gcd(unsigned ei, mpq& g) { bool normalize_e_by_gcd(unsigned ei, mpq& g) {
mpq& e = m_sum_of_fixed[ei]; mpq& e = m_sum_of_fixed[ei];
TRACE(dio, print_entry(ei, tout) << std::endl;); TRACE(dio, print_entry(ei, tout, true) << std::endl;);
g = gcd_of_coeffs(m_e_matrix.m_rows[ei], false); g = gcd_of_coeffs(m_e_matrix.m_rows[ei], true);
TRACE(dio, tout << "g:" << g << std::endl;);
if (g.is_zero() || g.is_one()) { if (g.is_zero() || g.is_one()) {
SASSERT(g.is_one() || e.is_zero()); SASSERT(g.is_one() || e.is_zero());
return true; return true;
} }
TRACE(dio, tout << "g:" << g << std::endl;);
mpq c_g = e / g; mpq c_g = e / g;
if (c_g.is_int()) { if (c_g.is_int()) {
for (auto& p : m_e_matrix.m_rows[ei]) { for (auto& p : m_e_matrix.m_rows[ei]) {
@ -1234,15 +1234,14 @@ namespace lp {
} }
m_sum_of_fixed[ei] = c_g; m_sum_of_fixed[ei] = c_g;
// e.m_l /= g // e.m_l /= g
for (auto& p : m_l_matrix.m_rows[ei]) { for (auto& p : m_l_matrix.m_rows[ei])
p.coeff() /= g; p.coeff() /= g;
}
TRACE(dio, tout << "ep_m_e:"; TRACE(dio, tout << "ep_m_e:"; print_entry(ei, tout, true) << std::endl;);
print_entry(ei, tout) << std::endl;);
SASSERT(entry_invariant(ei)); SASSERT(entry_invariant(ei));
return true; return true;
} }
TRACE(dio, tout << "false\n";);
// c_g is not integral // c_g is not integral
return false; return false;
} }
@ -1459,8 +1458,6 @@ namespace lp {
t1.add_monomial(mpq(1), j); t1.add_monomial(mpq(1), j);
term_o rs = fix_vars(t1); term_o rs = fix_vars(t1);
if (ls != rs) { if (ls != rs) {
std::cout << "enabling trace dio\n";
enable_trace("dio");
TRACE(dio, tout << "ls:"; print_term_o(ls, tout) << "\n"; TRACE(dio, tout << "ls:"; print_term_o(ls, tout) << "\n";
tout << "rs:"; print_term_o(rs, tout) << "\n";); tout << "rs:"; print_term_o(rs, tout) << "\n";);
return false; return false;
@ -2167,9 +2164,10 @@ namespace lp {
m_sum_of_fixed[i] -= j_sign * coeff * e; m_sum_of_fixed[i] -= j_sign * coeff * e;
m_e_matrix.pivot_row_to_row_given_cell_with_sign(ei, c, j, j_sign); m_e_matrix.pivot_row_to_row_given_cell_with_sign(ei, c, j, j_sign);
// m_sum_of_fixed[i].m_l -= j_sign * coeff * e.m_l; // m_sum_of_fixed[i].m_l -= j_sign * coeff * e.m_l;
TRACE(dio, print_term_o(open_ml(m_l_matrix.m_rows[ei]), tout << "l row " << ei << ":") << "\n";);
m_l_matrix.add_rows(-j_sign * coeff, ei, i); m_l_matrix.add_rows(-j_sign * coeff, ei, i);
TRACE(dio, tout << "after pivoting c_row:"; TRACE(dio, tout << "after pivoting c_row:";
print_entry(i, tout);); print_entry(i, tout, true););
CTRACE( CTRACE(
dio, !entry_invariant(i), tout << "invariant delta:"; { dio, !entry_invariant(i), tout << "invariant delta:"; {
print_term_o(get_term_from_entry(ei) - print_term_o(get_term_from_entry(ei) -
@ -2242,7 +2240,6 @@ namespace lp {
continue; continue;
unsigned j = local_to_lar_solver(p.var()); unsigned j = local_to_lar_solver(p.var());
if (is_fixed(j)) { if (is_fixed(j)) {
enable_trace("dio");
TRACE(dio, tout << "x" << j << "(local: " << "x" << p.var() << ") should not be fixed\nbad entry:"; print_entry(ei, tout) << "\n";); TRACE(dio, tout << "x" << j << "(local: " << "x" << p.var() << ") should not be fixed\nbad entry:"; print_entry(ei, tout) << "\n";);
return false; return false;
} }
@ -2251,8 +2248,6 @@ namespace lp {
term_o ls = term_to_lar_solver(remove_fresh_vars(get_term_from_entry(ei))); term_o ls = term_to_lar_solver(remove_fresh_vars(get_term_from_entry(ei)));
mpq ls_val = get_term_value(ls); mpq ls_val = get_term_value(ls);
if (!ls_val.is_zero()) { if (!ls_val.is_zero()) {
std::cout << "ls_val is not zero\n";
enable_trace("dio");
TRACE(dio, { TRACE(dio, {
tout << "get_term_from_entry(" << ei << "):"; tout << "get_term_from_entry(" << ei << "):";
print_term_o(get_term_from_entry(ei), tout) << std::endl; print_term_o(get_term_from_entry(ei), tout) << std::endl;
@ -2270,7 +2265,6 @@ namespace lp {
} }
bool ret = ls == fix_vars(open_ml(m_l_matrix.m_rows[ei])); bool ret = ls == fix_vars(open_ml(m_l_matrix.m_rows[ei]));
if (!ret) { if (!ret) {
enable_trace("dio");
CTRACE(dio, !ret, CTRACE(dio, !ret,
{ {
tout << "get_term_from_entry(" << ei << "):"; tout << "get_term_from_entry(" << ei << "):";
@ -2486,15 +2480,22 @@ namespace lp {
unsigned ei = f_vector[i]; unsigned ei = f_vector[i];
SASSERT (belongs_to_f(ei)); SASSERT (belongs_to_f(ei));
if (m_e_matrix.m_rows[ei].size() == 0) { if (m_e_matrix.m_rows[ei].size() == 0) {
if (m_sum_of_fixed[ei].is_zero()) { if (m_sum_of_fixed[ei].is_zero())
continue; continue;
}
else { else {
TRACE(dio, tout << "zero row with non_zero fixed sum conflict:\n"; print_entry(ei, tout, true) << std::endl;);
set_rewrite_conflict(ei, mpq(0)); set_rewrite_conflict(ei, mpq(0));
return lia_move::conflict; return lia_move::conflict;
} }
} }
if (!m_sum_of_fixed[ei].is_int()) {
TRACE(dio, tout << "new conflict: early non-integral entry in S after move_entry_from_f_to_s\n";
print_entry(ei, tout) << std::endl;);
set_rewrite_conflict(ei, mpq(0));
return lia_move::conflict;
}
auto [ahk, k, k_sign, markovich_number] = find_minimal_abs_coeff(ei); auto [ahk, k, k_sign, markovich_number] = find_minimal_abs_coeff(ei);
mpq gcd; mpq gcd;
if (!normalize_e_by_gcd(ei, gcd)) { if (!normalize_e_by_gcd(ei, gcd)) {