mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 20:18:18 +00:00
Code Activity

Merge branch 'master' into unit_prop_on_monomials

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-09-26 20:25:43 -07:00 committed by GitHub
parent 94eb101873 9c63ea3135
commit 4b85a105bb
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 3 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/math/lp/lp_bound_propagator.h
View file

@ -145,6 +145,7 @@ public:
return (*m_column_types)[j] == column_type::fixed && get_lower_bound(j).y.is_zero(); return (*m_column_types)[j] == column_type::fixed && get_lower_bound(j).y.is_zero();
} }
void add_bound(mpq const& v, unsigned j, bool is_low, bool strict, std::function<u_dependency* ()> explain_bound) { void add_bound(mpq const& v, unsigned j, bool is_low, bool strict, std::function<u_dependency* ()> explain_bound) {
j = lp().column_to_reported_index(j); j = lp().column_to_reported_index(j);
@ -159,6 +160,7 @@ public:
if (m_improved_lower_bounds.find(j, k)) { if (m_improved_lower_bounds.find(j, k)) {
auto& found_bound = m_ibounds[k]; auto& found_bound = m_ibounds[k];
if (v > found_bound.m_bound || (v == found_bound.m_bound && !found_bound.m_strict && strict)) { if (v > found_bound.m_bound || (v == found_bound.m_bound && !found_bound.m_strict && strict)) {
found_bound.m_bound = v; found_bound.m_bound = v;
found_bound.m_strict = strict; found_bound.m_strict = strict;
found_bound.set_explain(explain_bound); found_bound.set_explain(explain_bound);
@ -174,6 +176,7 @@ public:
if (m_improved_upper_bounds.find(j, k)) { if (m_improved_upper_bounds.find(j, k)) {
auto& found_bound = m_ibounds[k]; auto& found_bound = m_ibounds[k];
if (v < found_bound.m_bound || (v == found_bound.m_bound && !found_bound.m_strict && strict)) { if (v < found_bound.m_bound || (v == found_bound.m_bound && !found_bound.m_strict && strict)) {
found_bound.m_bound = v; found_bound.m_bound = v;
found_bound.m_strict = strict; found_bound.m_strict = strict;
found_bound.set_explain(explain_bound); found_bound.set_explain(explain_bound);