mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity

sketch fixed variable callback mechanism

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-01-08 12:50:46 -08:00
parent c1a62d346c
commit 270c127407
3 changed files with 63 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1950,14 +1950,20 @@ namespace lp {
tout << std::endl;
}
});
bool was_fixed = column_is_fixed(j);
mpq rs = adjust_bound_for_int(j, kind, right_side);
if (column_has_upper_bound(j))
update_column_type_and_bound_with_ub(j, kind, rs, dep);
else
update_column_type_and_bound_with_no_ub(j, kind, rs, dep);
if (is_base(j) && column_is_fixed(j))
if (!was_fixed && column_is_fixed(j) && m_fixed_var_eh)
m_fixed_var_eh(j);
if (is_base(j) && column_is_fixed(j))
m_fixed_base_var_set.insert(j);
TRACE("lar_solver_feas", tout << "j = " << j << " became " << (this->column_is_feasible(j) ? "feas" : "non-feas") << ", and " << (this->column_is_bounded(j) ? "bounded" : "non-bounded") << std::endl;);
}

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

@ -311,6 +311,7 @@ public:
inline void restore_x() { m_mpq_lar_core_solver.m_r_x = m_backup_x; }
std::function<void(lpvar)> m_fixed_var_eh;
template <typename T>
void explain_implied_bound(const implied_bound& ib, lp_bound_propagator<T>& bp) {
u_dependency* dep = ib.explain_implied();