mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 10:52:02 +00:00
Code Activity

remove explanation.reset() and fixes in add_var_bound()

Browse source 
Signed-off-by: Lev <levnach@hotmail.com>
This commit is contained in:
Lev 2018-11-09 10:04:08 -08:00 • committed by Lev Nachmanson
parent 1d51c5689e
commit 2993453798
4 changed files with 15 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/smt/theory_lra.cpp
View file

@ -2023,7 +2023,7 @@ public:
if (!check_idiv_bounds()) { if (!check_idiv_bounds()) {
return l_false; return l_false;
} }
m_explanation.reset(); m_explanation.clear();
switch (m_lia->check()) { switch (m_lia->check()) {
case lp::lia_move::sat: case lp::lia_move::sat:
lia_check = l_true; lia_check = l_true;
@ -2195,7 +2195,7 @@ public:
if (!m_nra && !m_nla) return l_true; if (!m_nra && !m_nla) return l_true;
if (!m_switcher.need_check()) return l_true; if (!m_switcher.need_check()) return l_true;
m_a1 = nullptr; m_a2 = nullptr; 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); 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); return m_nra? check_aftermath_nra(r) : check_aftermath_nla(r);
} }

2
src/util/lp/explanation.h
View file

@ -34,7 +34,7 @@ public:
m_set_of_ci.insert(j); m_set_of_ci.insert(j);
m_explanation.push_back(std::make_pair(one_of_type<mpq>(), j)); m_explanation.push_back(std::make_pair(one_of_type<mpq>(), j));
} }
void reset() { m_explanation.reset(); }
template <typename A> void add(const A& a) { for (constraint_index j : a) push_justification(j); } template <typename A> void add(const A& a) { for (constraint_index j : a) push_justification(j); }
}; };
} }

15
src/util/lp/lar_solver.cpp
View file

@ -304,7 +304,9 @@ lp_status lar_solver::solve() {
} }
void lar_solver::fill_explanation_from_infeasible_column(explanation & evidence) const{ void lar_solver::fill_explanation_from_infeasible_column(explanation & evidence) const{
lp_assert(static_cast<int>(get_column_type(m_infeasible_column)) >= static_cast<int>(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 // 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]; const ul_pair & ul = m_columns_to_ul_pairs[m_infeasible_column];
evidence.push_justification(ul.upper_bound_witness(), numeric_traits<mpq>::one()); evidence.push_justification(ul.upper_bound_witness(), numeric_traits<mpq>::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) { 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(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); mpq y_of_bound(0);
switch (kind) { 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_upper_bound_witness(j, ci);
set_lower_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_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; break;
} }
default: default:
lp_unreachable(); 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) { 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(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); mpq y_of_bound(0);
switch (kind) { switch (kind) {
case LT: 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) { 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(!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); mpq y_of_bound(0);
switch (kind) { switch (kind) {
case LT: case LT:

2
src/util/lp/nra_solver.cpp
View file

@ -118,7 +118,7 @@ typedef nla::variable_map_type variable_map_type;
case l_true: case l_true:
break; break;
case l_false: case l_false:
ex.reset(); ex.clear();
m_nlsat->get_core(core); m_nlsat->get_core(core);
for (auto c : core) { for (auto c : core) {
unsigned idx = static_cast<unsigned>(static_cast<imp*>(c) - this); unsigned idx = static_cast<unsigned>(static_cast<imp*>(c) - this);