mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-05-03 22:05:45 +00:00
Code Activity

fixes in lar_solver around nl unit propagation

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2023-10-01 11:39:58 -07:00
parent 702322a6e9
commit a297a2b25c
8 changed files with 28 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -21,8 +21,14 @@ namespace nla {
coeffs.push_back(std::make_pair(rational::one(), monic_var));
lp::lpvar term_index = c().lra.add_term(coeffs, UINT_MAX);
auto* dep = explain_fixed(vars, non_fixed);
// term_index becomes the column index of the term slack variable
term_index = c().lra.map_term_index_to_column_index(term_index);
c().lra.update_column_type_and_bound(term_index, lp::lconstraint_kind::EQ, mpq(0), dep);
c().lra.track_column_feasibility(term_index);
if (!c().lra.column_is_feasible(term_index)) {
c().lra.set_status(lp::lp_status::UNKNOWN);
}
}
u_dependency* monomial_bounds::explain_fixed(const svector<lpvar>& vars, lpvar non_fixed) {