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

try sorting terms before tightening

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-02-07 12:56:20 -10:00 committed by Lev Nachmanson
parent dcd5783232
commit 5b0b224a5c
1 changed files with 38 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1339,26 +1339,56 @@ namespace lp {
subs_front_in_indexed_vector(q);
}
lia_move tighten_terms_with_S() {
std_vector<unsigned> cleanup;
lia_move ret = lia_move::undef;
for (unsigned j : m_changed_terms) {
cleanup.push_back(j);
if (j >= lra.column_count()) continue;
if (!lra.column_has_term(j) || lra.column_is_free(j) ||
is_fixed(j) || !lia.column_is_int(j)) {
continue;
unsigned term_weight(const lar_term& t) const {
unsigned weight = 0;
for (const auto& p : t) {
// Get index j from coefficient
unsigned j = p.var();
// Look up j in columns_to_terms map
auto it = m_columns_to_terms.find(j);
if (it != m_columns_to_terms.end())
weight += static_cast<unsigned>(it->second.size());
}
return weight;
}
lia_move tighten_terms_with_S() {
// Copy changed terms to another vector for sorting
std_vector<unsigned> sorted_changed_terms;
std_vector<unsigned> cleanup;
for (unsigned j : m_changed_terms) {
if (
j >= lra.column_count() ||
!lra.column_has_term(j) ||
lra.column_is_free(j) ||
is_fixed(j) || !lia.column_is_int(j)) {
cleanup.push_back(j);
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;
// Process sorted terms
for (unsigned j : sorted_changed_terms) {
m_changed_terms.remove(j);
if (tighten_bounds_for_term_column(j)) {
ret = lia_move::conflict;
r = lia_move::conflict;
break;
}
}
for (unsigned j : cleanup) {
m_changed_terms.remove(j);
}
return ret;
return r;
}
std::ostream& print_queue(std::queue<unsigned> q, std::ostream& out) {