From 29934537981de9df5c29b04af0d225d0a9a7d790 Mon Sep 17 00:00:00 2001 From: Lev Date: Fri, 9 Nov 2018 10:04:08 -0800 Subject: [PATCH] remove explanation.reset() and fixes in add_var_bound() Signed-off-by: Lev --- src/smt/theory_lra.cpp | 4 ++-- src/util/lp/explanation.h | 2 +- src/util/lp/lar_solver.cpp | 15 +++++++++++---- src/util/lp/nra_solver.cpp | 2 +- 4 files changed, 15 insertions(+), 8 deletions(-) diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 982bad237..0f1cf30d3 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -2023,7 +2023,7 @@ public: if (!check_idiv_bounds()) { return l_false; } - m_explanation.reset(); + m_explanation.clear(); switch (m_lia->check()) { case lp::lia_move::sat: lia_check = l_true; @@ -2195,7 +2195,7 @@ public: if (!m_nra && !m_nla) return l_true; if (!m_switcher.need_check()) return l_true; m_a1 = nullptr; m_a2 = nullptr; - m_explanation.reset(); + m_explanation.clear(); lbool r = m_nra? m_nra->check(m_explanation): m_nla->check(m_explanation, m_lemma); return m_nra? check_aftermath_nra(r) : check_aftermath_nla(r); } diff --git a/src/util/lp/explanation.h b/src/util/lp/explanation.h index 0592621f9..217dc8c02 100644 --- a/src/util/lp/explanation.h +++ b/src/util/lp/explanation.h @@ -34,7 +34,7 @@ public: m_set_of_ci.insert(j); m_explanation.push_back(std::make_pair(one_of_type(), j)); } - void reset() { m_explanation.reset(); } + template void add(const A& a) { for (constraint_index j : a) push_justification(j); } }; } diff --git a/src/util/lp/lar_solver.cpp b/src/util/lp/lar_solver.cpp index 4a792e1c3..548166fd7 100644 --- a/src/util/lp/lar_solver.cpp +++ b/src/util/lp/lar_solver.cpp @@ -304,7 +304,9 @@ lp_status lar_solver::solve() { } void lar_solver::fill_explanation_from_infeasible_column(explanation & evidence) const{ - + lp_assert(static_cast(get_column_type(m_infeasible_column)) >= static_cast(column_type::boxed)); + lp_assert(!m_mpq_lar_core_solver.m_r_solver.column_is_feasible(m_infeasible_column)); + // this is the case when the lower bound is in conflict with the upper one const ul_pair & ul = m_columns_to_ul_pairs[m_infeasible_column]; evidence.push_justification(ul.upper_bound_witness(), numeric_traits::one()); @@ -1960,6 +1962,8 @@ void lar_solver::update_column_type_and_bound_with_no_ub(unsigned j, lp::lconstr void lar_solver::update_bound_with_ub_lb(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index ci) { lp_assert(column_has_lower_bound(j) && column_has_upper_bound(j)); + lp_assert(m_mpq_lar_core_solver.m_column_types[j] == column_type::boxed || + m_mpq_lar_core_solver.m_column_types[j] == column_type::fixed); mpq y_of_bound(0); switch (kind) { @@ -2003,17 +2007,20 @@ void lar_solver::update_bound_with_ub_lb(var_index j, lconstraint_kind kind, con set_upper_bound_witness(j, ci); set_lower_bound_witness(j, ci); m_mpq_lar_core_solver.m_r_upper_bounds[j] = m_mpq_lar_core_solver.m_r_lower_bounds[j] = v; - m_mpq_lar_core_solver.m_column_types[j] = column_type::fixed; break; } default: lp_unreachable(); } + if (m_mpq_lar_core_solver.m_r_upper_bounds[j] == m_mpq_lar_core_solver.m_r_lower_bounds[j]) { + m_mpq_lar_core_solver.m_column_types[j] = column_type::fixed; + } } void lar_solver::update_bound_with_no_ub_lb(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index ci) { lp_assert(column_has_lower_bound(j) && !column_has_upper_bound(j)); - + lp_assert(m_mpq_lar_core_solver.m_column_types[j] == column_type::lower_bound); + mpq y_of_bound(0); switch (kind) { case LT: @@ -2065,7 +2072,7 @@ void lar_solver::update_bound_with_no_ub_lb(var_index j, lconstraint_kind kind, void lar_solver::update_bound_with_ub_no_lb(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index ci) { lp_assert(!column_has_lower_bound(j) && column_has_upper_bound(j)); - + lp_assert(m_mpq_lar_core_solver.m_column_types[j] == column_type::upper_bound); mpq y_of_bound(0); switch (kind) { case LT: diff --git a/src/util/lp/nra_solver.cpp b/src/util/lp/nra_solver.cpp index ee0752a54..a19c3f932 100644 --- a/src/util/lp/nra_solver.cpp +++ b/src/util/lp/nra_solver.cpp @@ -118,7 +118,7 @@ typedef nla::variable_map_type variable_map_type; case l_true: break; case l_false: - ex.reset(); + ex.clear(); m_nlsat->get_core(core); for (auto c : core) { unsigned idx = static_cast(static_cast(c) - this);