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

fixes in dio

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2024-10-01 10:34:17 -07:00 committed by Lev Nachmanson
parent a8e667c643
commit 44fd0e48a8
2 changed files with 27 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -325,11 +325,11 @@ namespace lp {
lia_move tighten_with_S() { lia_move tighten_with_S() {
// following the pattern of int_cube // Following the pattern of int_cube, but do not push/pop the state. Instead, we keep the new bounds.
int change = 0; int change = 0;
for (unsigned j = 0; j < lra.column_count(); j++) { for (unsigned j = 0; j < lra.column_count(); j++) {
if (!lra.column_has_term(j) || lra.column_is_free(j) || if (!lra.column_has_term(j) || lra.column_is_free(j) ||
lra.column_is_fixed(j) || !lia.column_is_int(j)) continue; lra.column_is_fixed(j) || !lia.column_is_int(j)) continue;
if (tighten_bounds_for_column(j)) { if (tighten_bounds_for_column(j)) {
change++; change++;
} }
@ -379,7 +379,6 @@ namespace lp {
return false; return false;
} }
return tighten_bounds_for_term(t, g, j, dep); return tighten_bounds_for_term(t, g, j, dep);
} }
void handle_constant_term(term_o& t, unsigned j, u_dependency* dep) { void handle_constant_term(term_o& t, unsigned j, u_dependency* dep) {
@ -397,8 +396,8 @@ namespace lp {
for (const auto& p: lra.flatten(b_dep)) { for (const auto& p: lra.flatten(b_dep)) {
m_infeas_explanation.push_back(p); m_infeas_explanation.push_back(p);
} }
return;
} }
return;
} }
if (lra.has_lower_bound(j, b_dep, rs, is_strict)) { if (lra.has_lower_bound(j, b_dep, rs, is_strict)) {
if (t.c() < rs || is_strict && t.c() == rs) { if (t.c() < rs || is_strict && t.c() == rs) {
@ -516,23 +515,37 @@ namespace lp {
} }
std::tuple<mpq, unsigned, int> find_minimal_abs_coeff(const term_o& eh) const { std::tuple<mpq, unsigned, int> find_minimal_abs_coeff(const term_o& eh) const {
bool first = true; bool first = true, first_fresh = true;
mpq ahk; mpq ahk, ahk_fresh;
unsigned k; unsigned k, k_fresh;
int k_sign; int k_sign, k_sign_fresh;
mpq t; mpq t;
for (const auto& p : eh) { for (const auto& p : eh) {
t = abs(p.coeff()); t = abs(p.coeff());
if (first || t < ahk) { if (first_fresh || t < ahk_fresh) {
ahk_fresh = t;
k_sign_fresh = p.coeff().is_pos() ? 1 : -1;
k_fresh = p.j();
first_fresh = false;
} else if (first || t < ahk) {
ahk = t; ahk = t;
k_sign = p.coeff().is_pos() ? 1 : -1; k_sign = p.coeff().is_pos() ? 1 : -1;
k = p.j(); k = p.j();
first = false;
if (ahk.is_one()) if (ahk.is_one())
break; break;
first = false;
} }
} }
return std::make_tuple(ahk, k, k_sign); if (first_fresh) // did not find any fresh variables
return std::make_tuple(ahk, k, k_sign);
if (first) // only fresh vars
return std::make_tuple(ahk_fresh, k_fresh, k_sign_fresh);
SASSERT(!first && !first_fresh);
if (ahk <= ahk_fresh) {
return std::make_tuple(ahk, k, k_sign);
}
return std::make_tuple(ahk_fresh, k_fresh, k_sign_fresh);
} }
term_o get_term_to_subst(const term_o& eh, unsigned k, int k_sign) { term_o get_term_to_subst(const term_o& eh, unsigned k, int k_sign) {

6
src/math/lp/lar_solver.cpp
View file

@ -1061,15 +1061,15 @@ namespace lp {
return ret; return ret;
} }
bool lar_solver::has_lower_bound(lpvar var, u_dependency*& ci, mpq& value, bool& is_strict) const { bool lar_solver::has_lower_bound(lpvar var, u_dependency*& dep, mpq& value, bool& is_strict) const {
if (var >= m_columns.size()) { if (var >= m_columns.size()) {
// TBD: bounds on terms could also be used, caller may have to track these. // TBD: bounds on terms could also be used, caller may have to track these.
return false; return false;
} }
const column& ul = m_columns[var]; const column& ul = m_columns[var];
ci = ul.lower_bound_witness(); dep = ul.lower_bound_witness();
if (ci != nullptr) { if (dep != nullptr) {
auto& p = m_mpq_lar_core_solver.m_r_lower_bounds()[var]; auto& p = m_mpq_lar_core_solver.m_r_lower_bounds()[var];
value = p.x; value = p.x;
is_strict = p.y.is_pos(); is_strict = p.y.is_pos();