mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

revert the term sorting

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-02-08 14:25:10 -10:00 committed by Lev Nachmanson
parent f2c1fd4c14
commit 5ebee24850
1 changed files with 13 additions and 29 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1354,41 +1354,25 @@ namespace lp {
} }
lia_move tighten_terms_with_S() { lia_move tighten_terms_with_S() {
// Copy changed terms to another vector for sorting
std_vector<unsigned> sorted_changed_terms;
std_vector<unsigned> cleanup; std_vector<unsigned> cleanup;
lia_move ret = lia_move::undef;
for (unsigned j : m_changed_terms) { for (unsigned j : m_changed_terms) {
if ( cleanup.push_back(j);
j >= lra.column_count() || if (j >= lra.column_count()) continue;
!lra.column_has_term(j) || if (!lra.column_has_term(j) || lra.column_is_free(j) ||
lra.column_is_free(j) ||
is_fixed(j) || !lia.column_is_int(j)) { is_fixed(j) || !lia.column_is_int(j)) {
cleanup.push_back(j); continue;
continue; }
}
sorted_changed_terms.push_back(j);
}
// Sort by term_weight descending
std::sort(sorted_changed_terms.begin(), sorted_changed_terms.end(),
[this](unsigned j1, unsigned j2) {
return term_weight(lra.get_term(j1)) > term_weight(lra.get_term(j2) );
});
lia_move r = lia_move::undef; if (tighten_bounds_for_term_column(j)) {
// Process sorted terms ret = lia_move::conflict;
for (unsigned j : sorted_changed_terms) {
m_changed_terms.remove(j);
if (tighten_bounds_for_term_column(j)) {
r = lia_move::conflict;
break; break;
} }
} }
for (unsigned j : cleanup) { for (unsigned j: cleanup) {
m_changed_terms.remove(j); m_changed_terms.remove(j);
} }
return r; return ret;
} }
std::ostream& print_queue(std::queue<unsigned> q, std::ostream& out) { std::ostream& print_queue(std::queue<unsigned> q, std::ostream& out) {
@ -1999,8 +1983,8 @@ namespace lp {
} }
} }
unsigned find_markovich_number(unsigned k, unsigned h) { unsigned markovich_number(unsigned k, unsigned h) {
return m_e_matrix.m_columns[k].size() * m_e_matrix.m_rows[h].size(); return (unsigned) m_e_matrix.m_columns[k].size() * m_e_matrix.m_rows[h].size();
} }
std::tuple<mpq, unsigned, int, unsigned> find_minimal_abs_coeff(unsigned ei) { std::tuple<mpq, unsigned, int, unsigned> find_minimal_abs_coeff(unsigned ei) {
@ -2021,7 +2005,7 @@ namespace lp {
} }
} }
return std::make_tuple(ahk, k, k_sign, find_markovich_number(k, ei)); return std::make_tuple(ahk, k, k_sign, markovich_number(k, ei));
} }