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

fixes in interval explanations

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-06-10 15:10:54 -07:00
parent 2d5595eddc
commit 46b9273a79
3 changed files with 9 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -56,6 +56,7 @@ public :
{} {}
void analyze() { void analyze() {
TRACE("lp_bound_prop", print_linear_combination_of_column_indices_only(m_row, tout); tout << " = " << m_rs << "\n";);
for (const auto & c : m_row) { for (const auto & c : m_row) {
if ((m_column_of_l == -2) && (m_column_of_u == -2)) if ((m_column_of_l == -2) && (m_column_of_u == -2))
break; break;

2
src/math/lp/lp_bound_propagator.cpp
View file

@ -42,6 +42,7 @@ bool lp_bound_propagator::lower_bound_is_available_for_column(unsigned j) const
return false; return false;
} }
} }
bool lp_bound_propagator::upper_bound_is_available(unsigned j) const { bool lp_bound_propagator::upper_bound_is_available(unsigned j) const {
if (upper_bound_is_available_for_column(j)) if (upper_bound_is_available_for_column(j))
return true; return true;
@ -123,6 +124,7 @@ bool lp_bound_propagator::nl_monomial_upper_bound_should_be_taken(unsigned j) co
} }
bool lp_bound_propagator::nl_monomial_lower_bound_should_be_taken(unsigned j) const { bool lp_bound_propagator::nl_monomial_lower_bound_should_be_taken(unsigned j) const {
lp_assert(lower_bound_is_available(j));
return (!lower_bound_is_available_for_column(j)) || (nl_monomial_lower_bound_is_available(j) && m_nla_solver->get_lower_bound(j) > m_lar_solver.m_mpq_lar_core_solver.m_r_lower_bounds()[j]); return (!lower_bound_is_available_for_column(j)) || (nl_monomial_lower_bound_is_available(j) && m_nla_solver->get_lower_bound(j) > m_lar_solver.m_mpq_lar_core_solver.m_r_lower_bounds()[j]);
} }

12
src/math/lp/nla_intervals.cpp
View file

@ -23,12 +23,12 @@ intervals::interval intervals::mul_signs_with_deps(const svector<lpvar>& vars) c
m_imanager.set(a, mpq(1)); m_imanager.set(a, mpq(1));
for (lpvar v : vars) { for (lpvar v : vars) {
set_var_interval_signs_with_deps(v, b); set_var_interval_signs_with_deps(v, b);
if (m_imanager.is_zero(b))
return b;
interval_deps deps; interval_deps deps;
m_imanager.mul(a, b, c, deps); m_imanager.mul(a, b, c, deps);
m_imanager.set(a, c); m_imanager.set(a, c);
m_config.add_deps(a, b, deps, a); m_config.add_deps(a, b, deps, a);
if (m_imanager.is_zero(a))
return a;
} }
return a; return a;
@ -174,7 +174,7 @@ lp::impq intervals::get_upper_bound_of_monomial(lpvar j) const {
auto r = lp::impq(a.m_upper); auto r = lp::impq(a.m_upper);
if (a.m_upper_open) if (a.m_upper_open)
r.y = -1; r.y = -1;
TRACE("nla_intervals", m_core->print_monomial_with_vars(m, tout) << "upper = " << r << "\n";); TRACE("nla_intervals_detail", m_core->print_monomial_with_vars(m, tout) << "upper = " << r << "\n";);
return r; return r;
} }
lp::impq intervals::get_lower_bound_of_monomial(lpvar j) const { lp::impq intervals::get_lower_bound_of_monomial(lpvar j) const {
@ -184,7 +184,7 @@ lp::impq intervals::get_lower_bound_of_monomial(lpvar j) const {
auto r = lp::impq(a.m_lower); auto r = lp::impq(a.m_lower);
if (a.m_lower_open) if (a.m_lower_open)
r.y = 1; r.y = 1;
TRACE("nla_intervals", m_core->print_monomial_with_vars(m, tout) << "lower = " << r << "\n";); TRACE("nla_intervals_detail", m_core->print_monomial_with_vars(m, tout) << "lower = " << r << "\n";);
return r; return r;
} }
@ -240,9 +240,9 @@ lp::lar_solver& intervals::ls() { return m_core->m_lar_solver; }
const lp::lar_solver& intervals::ls() const { return m_core->m_lar_solver; } const lp::lar_solver& intervals::ls() const { return m_core->m_lar_solver; }
std::ostream& intervals::print_explanations(const svector<lp::constraint_index> &expl , std::ostream& out) const { std::ostream& intervals::print_explanations(const svector<lp::constraint_index> &expl , std::ostream& out) const {
out << "interv expl: "; out << "interv expl:\n ";
for (auto ci : expl) for (auto ci : expl)
m_core->m_lar_solver.print_constraint(ci, out) << "\n"; m_core->m_lar_solver.print_constraint_indices_only(ci, out);
return out; return out;
} }