mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-05-11 09:44:43 +00:00
Code Activity

restore lar_solver::add_named_var

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-05-08 17:18:41 -07:00
parent 935f076a05
commit 7da06df64f
2 changed files with 11 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1289,6 +1289,11 @@ namespace lp {
#endif #endif
return true; return true;
} }
lpvar lar_solver::add_named_var(unsigned ext_j, bool is_int, const std::string& name) {
lpvar j = add_var(ext_j, is_int);
m_imp->m_var_register.set_name(j, name);
return j;
}
bool lar_solver::inf_explanation_is_correct() const { bool lar_solver::inf_explanation_is_correct() const {
#ifdef Z3DEBUG #ifdef Z3DEBUG
@ -1415,33 +1420,25 @@ namespace lp {
#if 1 #if 1
if(is_upper) { if(is_upper) {
unsigned current_update_index = ul.previous_upper(); if (ul.previous_upper() != UINT_MAX) {
while (current_update_index != UINT_MAX) { auto const& [_is_upper, _j, _bound, _column] = m_imp->m_column_updates[ul.previous_upper()];
auto const& [_is_upper, _j, _bound, _column] = m_imp->m_column_updates[current_update_index];
auto new_slack = slack + coeff * (_bound - get_upper_bound(j)); auto new_slack = slack + coeff * (_bound - get_upper_bound(j));
if (sign == get_sign(new_slack)) { if (sign == get_sign(new_slack)) {
//verbose_stream() << "can weaken upper j" << j << " " << coeff << " " << get_upper_bound(j) << " " << _bound << "\n"; //verbose_stream() << "can weaken upper j" << j << " " << coeff << " " << get_upper_bound(j) << " " << _bound << "\n";
slack = new_slack; slack = new_slack;
bound_constr_i = _column.upper_bound_witness(); bound_constr_i = _column.upper_bound_witness();
current_update_index = _column.previous_upper(); // Move to the next previous bound in the list }
} else
break; // Stop if weakening is not possible with this previous bound
} }
} }
else { else {
unsigned prev_l = ul.previous_lower(); if (ul.previous_lower() != UINT_MAX) {
while (prev_l != UINT_MAX) { auto const& [_is_upper, _j, _bound, _column] = m_imp->m_column_updates[ul.previous_lower()];
auto const& [_is_upper, _j, _bound, _column] = m_imp->m_column_updates[prev_l];
auto new_slack = slack + coeff * (_bound - get_lower_bound(j)); auto new_slack = slack + coeff * (_bound - get_lower_bound(j));
if (sign == get_sign(new_slack)) { if (sign == get_sign(new_slack)) {
//verbose_stream() << "can weaken lower j" << j << " " << coeff << " " << get_lower_bound(j) << " " << _bound << "\n"; //verbose_stream() << "can weaken lower j" << j << " " << coeff << " " << get_lower_bound(j) << " " << _bound << "\n";
slack = new_slack; slack = new_slack;
bound_constr_i = _column.lower_bound_witness(); bound_constr_i = _column.lower_bound_witness();
prev_l = _column.previous_lower();
} }
else
break;
} }
} }
#endif #endif

1
src/math/lp/lar_solver.h
View file

@ -296,6 +296,7 @@ public:
lar_term t; lar_term t;
}; };
lpvar add_named_var(unsigned ext_j, bool is_integer, const std::string&);
void solve_for(unsigned_vector const& js, vector<solution>& sol); void solve_for(unsigned_vector const& js, vector<solution>& sol);
void check_fixed(unsigned j); void check_fixed(unsigned j);
void solve_for(unsigned j, uint_set& tabu, vector<solution>& sol); void solve_for(unsigned j, uint_set& tabu, vector<solution>& sol);