mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 11:25:51 +00:00
Code Activity

before getting explanations for monomials upper and low bounds

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-06-06 15:53:43 -07:00
parent 74ecdf3191
commit 02133bbcc5
4 changed files with 30 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -239,6 +239,7 @@ void lar_solver::explain_implied_bound(implied_bound & ib, lp_bound_propagator &
int a_sign = is_pos(a)? 1: -1;
int sign = j_sign * a_sign;
const ul_pair & ul = m_columns_to_ul_pairs[j];
// todo : process witnesses from monomials!!!!!!!!!!!!!!!!!!!!!
auto witness = sign > 0? ul.upper_bound_witness(): ul.lower_bound_witness();
lp_assert(is_valid(witness));
bp.consume(a, witness);