From 1d51c5689ef9c0e5c7789a18e7dbe5ecfa9a7260 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Thu, 8 Nov 2018 11:00:12 -0800 Subject: [PATCH] roll back add_var api Signed-off-by: Lev Nachmanson --- src/smt/theory_lra.cpp | 40 ++++++-------- src/test/lp/lp.cpp | 61 +++++++++----------- src/test/lp/smt_reader.h | 8 +-- src/util/lp/lar_solver.cpp | 110 ++++++++++++++++++------------------- src/util/lp/lar_solver.h | 29 ++++++---- src/util/lp/mps_reader.h | 12 ++-- 6 files changed, 122 insertions(+), 138 deletions(-) diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 2a7ad9ed2..982bad237 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -422,9 +422,8 @@ class theory_lra::imp { m_theory_var2var_index.setx(v, var, UINT_MAX); m_var_index2theory_var.setx(var, v, UINT_MAX); m_var_trail.push_back(v); - lp::explanation e; - add_def_constraint(m_solver->add_var_bound(var, lp::GE, rational(c), e)); - add_def_constraint(m_solver->add_var_bound(var, lp::LE, rational(c), e)); + add_def_constraint(m_solver->add_var_bound(var, lp::GE, rational(c))); + add_def_constraint(m_solver->add_var_bound(var, lp::LE, rational(c))); return var; } @@ -801,9 +800,6 @@ class theory_lra::imp { ++m_stats.m_add_rows; } - void process_conflict() { - NOT_IMPLEMENTED_YET(); - } bool is_infeasible() const { return m_solver->get_status() == lp::lp_status::INFEASIBLE; @@ -818,14 +814,14 @@ class theory_lra::imp { st.coeffs().push_back(rational::minus_one()); theory_var z = internalize_linearized_def(term, st); lp::var_index vi = register_theory_var_in_lar_solver(z); - add_def_constraint(m_solver->add_var_bound(vi, lp::LE, rational::zero(), m_explanation)); - if (is_infeasible()) { - process_conflict(); // exit here? - } - add_def_constraint(m_solver->add_var_bound(vi, lp::GE, rational::zero(), m_explanation)); - if (is_infeasible()) { - process_conflict(); - } + add_def_constraint(m_solver->add_var_bound(vi, lp::LE, rational::zero())); + // if (is_infeasible()) { + // process_conflict(); // exit here? + // } + add_def_constraint(m_solver->add_var_bound(vi, lp::GE, rational::zero())); + // if (is_infeasible()) { + // process_conflict(); + // } TRACE("arith", { expr* o1 = get_enode(v1)->get_owner(); @@ -1241,12 +1237,11 @@ public: get_enode(w)->get_owner()))); theory_var z = internalize_def(term); lp::var_index vi = register_theory_var_in_lar_solver(z); - lp::explanation e; - add_def_constraint(m_solver->add_var_bound(vi, lp::GE, rational::zero(), e)); - add_def_constraint(m_solver->add_var_bound(vi, lp::LE, rational::zero(), e)); - add_def_constraint(m_solver->add_var_bound(register_theory_var_in_lar_solver(v), lp::GE, rational::zero(), e)); - add_def_constraint(m_solver->add_var_bound(register_theory_var_in_lar_solver(v), lp::LT, abs(r), e)); - SASSERT(m_solver->get_status() != lp::lp_status::INFEASIBLE); + add_def_constraint(m_solver->add_var_bound(vi, lp::GE, rational::zero())); + add_def_constraint(m_solver->add_var_bound(vi, lp::LE, rational::zero())); + add_def_constraint(m_solver->add_var_bound(register_theory_var_in_lar_solver(v), lp::GE, rational::zero())); + add_def_constraint(m_solver->add_var_bound(register_theory_var_in_lar_solver(v), lp::LT, abs(r))); + SASSERT(!is_infeasible()); TRACE("arith", m_solver->print_constraints(tout << term << "\n");); } @@ -2988,13 +2983,12 @@ public: lp::constraint_index ci; if (is_int && !is_true) { rational bound = b.get_value(false).get_rational(); - ci = m_solver->add_var_bound(vi, k, bound, m_explanation); + ci = m_solver->add_var_bound(vi, k, bound); } else { - ci = m_solver->add_var_bound(vi, k, b.get_value(), m_explanation); + ci = m_solver->add_var_bound(vi, k, b.get_value()); } if (is_infeasible()) { - set_conflict1(); return; } TRACE("arith", tout << "v" << b.get_var() << "\n";); diff --git a/src/test/lp/lp.cpp b/src/test/lp/lp.cpp index 4ae037a96..f9aa371c5 100644 --- a/src/test/lp/lp.cpp +++ b/src/test/lp/lp.cpp @@ -2682,8 +2682,7 @@ void test_term() { vector> term_one; term_one.push_back(std::make_pair(mpq(1), one)); - explanation e; - solver.add_constraint(term_one, lconstraint_kind::EQ, mpq(0), e); + solver.add_constraint(term_one, lconstraint_kind::EQ, mpq(0)); vector> term_ls; term_ls.push_back(std::pair(mpq(1), x)); @@ -2695,13 +2694,13 @@ void test_term() { ls.push_back(std::pair(mpq(1), x)); ls.push_back(std::pair(mpq(1), y)); ls.push_back(std::pair(mpq(1), z)); - - solver.add_constraint(ls, lconstraint_kind::EQ, mpq(0), e); + + solver.add_constraint(ls, lconstraint_kind::EQ, mpq(0)); ls.clear(); ls.push_back(std::pair(mpq(1), x)); - solver.add_constraint(ls, lconstraint_kind::LT, mpq(0), e); + solver.add_constraint(ls, lconstraint_kind::LT, mpq(0)); ls.push_back(std::pair(mpq(2), y)); - solver.add_constraint(ls, lconstraint_kind::GT, mpq(0), e); + solver.add_constraint(ls, lconstraint_kind::GT, mpq(0)); auto status = solver.solve(); std::cout << lp_status_to_string(status) << std::endl; std::unordered_map model; @@ -2718,7 +2717,6 @@ void test_term() { void test_evidence_for_total_inf_simple(argument_parser & args_parser) { lar_solver solver; - explanation e; var_index x = solver.add_var(0, false); var_index y = solver.add_var(1, false); solver.add_var_bound(x, LE, mpq(-1)); @@ -2727,11 +2725,10 @@ void test_evidence_for_total_inf_simple(argument_parser & args_parser) { ls.push_back(std::pair(mpq(1), x)); ls.push_back(std::pair(mpq(1), y)); - - solver.add_constraint(ls, GE, mpq(1), e); + solver.add_constraint(ls, GE, mpq(1)); ls.pop_back(); ls.push_back(std::pair(- mpq(1), y)); - solver.add_constraint(ls, lconstraint_kind::GE, mpq(0), e); + solver.add_constraint(ls, lconstraint_kind::GE, mpq(0)); auto status = solver.solve(); std::cout << lp_status_to_string(status) << std::endl; std::unordered_map model; @@ -2775,7 +2772,7 @@ void test_bound_propagation_one_small_sample1() { coeffs.push_back(std::pair(mpq(-1), c)); ls.add_constraint(coeffs, LE, zero_of_type()); vector ev; - ls.add_var_bound(a, LE, mpq(1), e); + ls.add_var_bound(a, LE, mpq(1)); ls.solve(); my_bound_propagator bp(ls); ls.propagate_bounds_for_touched_rows(bp); @@ -2829,7 +2826,7 @@ void test_bound_propagation_one_row() { explanation e; ls.add_constraint(c, EQ, one_of_type(), e); vector ev; - ls.add_var_bound(x0, LE, mpq(1), e); + ls.add_var_bound(x0, LE, mpq(1)); ls.solve(); my_bound_propagator bp(ls); ls.propagate_bounds_for_touched_rows(bp); @@ -2844,9 +2841,9 @@ void test_bound_propagation_one_row_with_bounded_vars() { explanation e; ls.add_constraint(c, EQ, one_of_type(), e); vector ev; - ls.add_var_bound(x0, GE, mpq(-3), e); - ls.add_var_bound(x0, LE, mpq(3), e); - ls.add_var_bound(x0, LE, mpq(1), e); + ls.add_var_bound(x0, GE, mpq(-3)); + ls.add_var_bound(x0, LE, mpq(3)); + ls.add_var_bound(x0, LE, mpq(1)); ls.solve(); my_bound_propagator bp(ls); ls.propagate_bounds_for_touched_rows(bp); @@ -2861,7 +2858,7 @@ void test_bound_propagation_one_row_mixed() { explanation e; ls.add_constraint(c, EQ, one_of_type(), e); vector ev; - ls.add_var_bound(x1, LE, mpq(1), e); + ls.add_var_bound(x1, LE, mpq(1)); ls.solve(); my_bound_propagator bp(ls); ls.propagate_bounds_for_touched_rows(bp); @@ -2876,16 +2873,15 @@ void test_bound_propagation_two_rows() { c.push_back(std::pair(mpq(1), x)); c.push_back(std::pair(mpq(2), y)); c.push_back(std::pair(mpq(3), z)); - explanation e; - ls.add_constraint(c, GE, one_of_type(), e); + ls.add_constraint(c, GE, one_of_type()); c.clear(); c.push_back(std::pair(mpq(3), x)); c.push_back(std::pair(mpq(2), y)); c.push_back(std::pair(mpq(y), z)); - ls.add_constraint(c, GE, one_of_type(), e); - ls.add_var_bound(x, LE, mpq(2), e); + ls.add_constraint(c, GE, one_of_type()); + ls.add_var_bound(x, LE, mpq(2)); vector ev; - ls.add_var_bound(y, LE, mpq(1), e); + ls.add_var_bound(y, LE, mpq(1)); ls.solve(); my_bound_propagator bp(ls); ls.propagate_bounds_for_touched_rows(bp); @@ -2898,15 +2894,14 @@ void test_total_case_u() { unsigned y = ls.add_var(1, false); unsigned z = ls.add_var(2, false); vector> c; - explanation e; c.push_back(std::pair(mpq(1), x)); c.push_back(std::pair(mpq(2), y)); c.push_back(std::pair(mpq(3), z)); - ls.add_constraint(c, LE, one_of_type(), e); - ls.add_var_bound(x, GE, zero_of_type(), e); - ls.add_var_bound(y, GE, zero_of_type(), e); + ls.add_constraint(c, LE, one_of_type()); + ls.add_var_bound(x, GE, zero_of_type()); + ls.add_var_bound(y, GE, zero_of_type()); vector ev; - ls.add_var_bound(z, GE, zero_of_type(), e); + ls.add_var_bound(z, GE, zero_of_type()); ls.solve(); my_bound_propagator bp(ls); ls.propagate_bounds_for_touched_rows(bp); @@ -2925,16 +2920,15 @@ void test_total_case_l(){ unsigned y = ls.add_var(1, false); unsigned z = ls.add_var(2, false); vector> c; - explanation e; c.push_back(std::pair(mpq(1), x)); c.push_back(std::pair(mpq(2), y)); c.push_back(std::pair(mpq(3), z)); - ls.add_constraint(c, GE, one_of_type(), e); - ls.add_var_bound(x, LE, one_of_type(), e); - ls.add_var_bound(y, LE, one_of_type(), e); + ls.add_constraint(c, GE, one_of_type()); + ls.add_var_bound(x, LE, one_of_type()); + ls.add_var_bound(y, LE, one_of_type()); ls.settings().presolve_with_double_solver_for_lar = true; vector ev; - ls.add_var_bound(z, LE, zero_of_type(), e); + ls.add_var_bound(z, LE, zero_of_type()); ls.solve(); my_bound_propagator bp(ls); ls.propagate_bounds_for_touched_rows(bp); @@ -3516,9 +3510,8 @@ void test_maximize_term() { term_ls.push_back(std::pair(mpq(2), y)); unsigned term_2x_pl_2y = solver.add_term(term_ls); - explanation e; - solver.add_var_bound(term_x_min_y, LE, zero_of_type(), e); - solver.add_var_bound(term_2x_pl_2y, LE, mpq(5), e); + solver.add_var_bound(term_x_min_y, LE, zero_of_type()); + solver.add_var_bound(term_2x_pl_2y, LE, mpq(5)); solver.find_feasible_solution(); lp_assert(solver.get_status() == lp_status::OPTIMAL); solver.print_constraints(std::cout); diff --git a/src/test/lp/smt_reader.h b/src/test/lp/smt_reader.h index 4f456c3f6..4bce99765 100644 --- a/src/test/lp/smt_reader.h +++ b/src/test/lp/smt_reader.h @@ -386,17 +386,17 @@ namespace lp { return ret; } - void add_constraint_to_solver(lar_solver * solver, formula_constraint & fc, explanation& e) { + void add_constraint_to_solver(lar_solver * solver, formula_constraint & fc) { vector> ls; for (auto & it : fc.m_coeffs) { ls.push_back(std::make_pair(it.first, solver->add_var(register_name(it.second), false))); } - solver->add_constraint(ls, fc.m_kind, fc.m_right_side, e); + solver->add_constraint(ls, fc.m_kind, fc.m_right_side); } - explanation e; + void fill_lar_solver(lar_solver * solver) { for (formula_constraint & fc : m_constraints) - add_constraint_to_solver(solver, fc, e); + add_constraint_to_solver(solver, fc); } diff --git a/src/util/lp/lar_solver.cpp b/src/util/lp/lar_solver.cpp index 030217bb5..4a792e1c3 100644 --- a/src/util/lp/lar_solver.cpp +++ b/src/util/lp/lar_solver.cpp @@ -28,6 +28,7 @@ void clear() {lp_assert(false); // not implemented lar_solver::lar_solver() : m_status(lp_status::UNKNOWN), + m_infeasible_column(-1), m_terms_start_index(1000000), m_mpq_lar_core_solver(m_settings, *this), m_int_solver(nullptr) @@ -302,6 +303,15 @@ lp_status lar_solver::solve() { return m_status; } +void lar_solver::fill_explanation_from_infeasible_column(explanation & evidence) const{ + + // 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()); + evidence.push_justification(ul.lower_bound_witness(), -numeric_traits::one()); +} + + unsigned lar_solver::get_total_iterations() const { return m_mpq_lar_core_solver.m_r_solver.total_iterations(); } vector lar_solver::get_list_of_all_var_indices() const { @@ -314,6 +324,7 @@ void lar_solver::push() { m_simplex_strategy = m_settings.simplex_strategy(); m_simplex_strategy.push(); m_columns_to_ul_pairs.push(); + m_infeasible_column.push(); m_mpq_lar_core_solver.push(); m_term_count = m_terms.size(); m_term_count.push(); @@ -340,7 +351,7 @@ void lar_solver::pop(unsigned k) { TRACE("int_solver", tout << "pop" << std::endl;); TRACE("lar_solver", tout << "k = " << k << std::endl;); restore_rounded_columns(); // if it is not done now, the basis changes and restore_rounded_columns would now work - m_infeasible_column_index.pop(k); + m_infeasible_column.pop(k); unsigned n = m_columns_to_ul_pairs.peek_size(k); m_var_register.shrink(n); if (m_settings.use_tableau()) { @@ -1197,6 +1208,10 @@ bool lar_solver::has_value(var_index var, mpq& value) const { void lar_solver::get_infeasibility_explanation(explanation& exp) const { exp.clear(); + if (m_infeasible_column != -1) { + fill_explanation_from_infeasible_column(exp); + return; + } if (m_mpq_lar_core_solver.get_infeasible_sum_sign() == 0) { return; } @@ -1767,17 +1782,17 @@ bool lar_solver::bound_is_integer_for_integer_column(unsigned j, const mpq & rig return right_side.is_int(); } -constraint_index lar_solver::add_var_bound(var_index j, lconstraint_kind kind, const mpq & right_side, explanation& e) { +constraint_index lar_solver::add_var_bound(var_index j, lconstraint_kind kind, const mpq & right_side) { TRACE("lar_solver", tout << "j = " << j << std::endl;); constraint_index ci = m_constraints.size(); if (!is_term(j)) { // j is a var lp_assert(bound_is_integer_for_integer_column(j, right_side)); auto vc = new lar_var_constraint(j, kind, right_side); m_constraints.push_back(vc); - update_column_type_and_bound(j, kind, right_side, ci, e); + update_column_type_and_bound(j, kind, right_side, ci); } else { - add_var_bound_on_constraint_for_term(j, kind, right_side, ci, e); + add_var_bound_on_constraint_for_term(j, kind, right_side, ci); } lp_assert(sizes_are_correct()); return ci; @@ -1803,43 +1818,42 @@ bool lar_solver::compare_values(impq const& lhs, lconstraint_kind k, const mpq & } void lar_solver::update_column_type_and_bound(var_index j, lconstraint_kind kind, const mpq & right_side, - constraint_index constr_index, - explanation& e) { + constraint_index constr_index) { if (column_has_upper_bound(j)) - update_column_type_and_bound_with_ub(j, kind, right_side, constr_index, e); + update_column_type_and_bound_with_ub(j, kind, right_side, constr_index); else - update_column_type_and_bound_with_no_ub(j, kind, right_side, constr_index, e); + update_column_type_and_bound_with_no_ub(j, kind, right_side, constr_index); } -void lar_solver::add_var_bound_on_constraint_for_term(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index ci, explanation & e) { +void lar_solver::add_var_bound_on_constraint_for_term(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index ci) { lp_assert(is_term(j)); unsigned adjusted_term_index = adjust_term_index(j); // lp_assert(!term_is_int(m_terms[adjusted_term_index]) || right_side.is_int()); unsigned term_j; if (m_var_register.external_is_used(j, term_j)) { m_constraints.push_back(new lar_term_constraint(m_terms[adjusted_term_index], kind, right_side)); - update_column_type_and_bound(term_j, kind, right_side, ci, e); + update_column_type_and_bound(term_j, kind, right_side, ci); } else { - add_constraint_from_term_and_create_new_column_row(j, m_terms[adjusted_term_index], kind, right_side, e); + add_constraint_from_term_and_create_new_column_row(j, m_terms[adjusted_term_index], kind, right_side); } } -constraint_index lar_solver::add_constraint(const vector>& left_side_with_terms, lconstraint_kind kind_par, const mpq& right_side_parm, explanation & e) { +constraint_index lar_solver::add_constraint(const vector>& left_side_with_terms, lconstraint_kind kind_par, const mpq& right_side_parm) { vector> left_side; substitute_terms_in_linear_expression(left_side_with_terms, left_side); unsigned term_index = add_term(left_side); constraint_index ci = m_constraints.size(); - add_var_bound_on_constraint_for_term(term_index, kind_par, right_side_parm, ci, e); + add_var_bound_on_constraint_for_term(term_index, kind_par, right_side_parm, ci); return ci; } void lar_solver::add_constraint_from_term_and_create_new_column_row(unsigned term_j, const lar_term* term, - lconstraint_kind kind, const mpq & right_side, explanation & e) { + lconstraint_kind kind, const mpq & right_side) { add_row_from_term_no_constraint(term, term_j); unsigned j = A_r().column_count() - 1; - update_column_type_and_bound(j, kind, right_side, m_constraints.size(), e); + update_column_type_and_bound(j, kind, right_side, m_constraints.size()); m_constraints.push_back(new lar_term_constraint(term, kind, right_side)); lp_assert(A_r().column_count() == m_mpq_lar_core_solver.m_r_solver.m_costs.size()); } @@ -1925,26 +1939,26 @@ void lar_solver::fill_last_row_of_A_d(static_matrix & A, const l lp_assert(A.is_correct()); } -void lar_solver::update_column_type_and_bound_with_ub(unsigned j, lp::lconstraint_kind kind, const mpq & right_side, unsigned constraint_index, lp::explanation& e) { +void lar_solver::update_column_type_and_bound_with_ub(unsigned j, lp::lconstraint_kind kind, const mpq & right_side, unsigned constraint_index) { SASSERT(column_has_upper_bound(j)); if (column_has_lower_bound(j)) { - update_bound_with_ub_lb(j, kind, right_side, constraint_index, e); + update_bound_with_ub_lb(j, kind, right_side, constraint_index); } else { - update_bound_with_ub_no_lb(j, kind, right_side, constraint_index, e); + update_bound_with_ub_no_lb(j, kind, right_side, constraint_index); } } -void lar_solver::update_column_type_and_bound_with_no_ub(unsigned j, lp::lconstraint_kind kind, const mpq & right_side, unsigned constraint_index, lp::explanation& e) { +void lar_solver::update_column_type_and_bound_with_no_ub(unsigned j, lp::lconstraint_kind kind, const mpq & right_side, unsigned constraint_index) { SASSERT(!column_has_upper_bound(j)); if (column_has_lower_bound(j)) { - update_bound_with_no_ub_lb(j, kind, right_side, constraint_index, e); + update_bound_with_no_ub_lb(j, kind, right_side, constraint_index); } else { - update_bound_with_no_ub_no_lb(j, kind, right_side, constraint_index, e); + update_bound_with_no_ub_no_lb(j, kind, right_side, constraint_index); } } -void lar_solver::update_bound_with_ub_lb(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index ci, explanation& e) { +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)); mpq y_of_bound(0); @@ -1955,9 +1969,7 @@ void lar_solver::update_bound_with_ub_lb(var_index j, lconstraint_kind kind, con { auto up = numeric_pair(right_side, y_of_bound); if (up < m_mpq_lar_core_solver.m_r_lower_bounds[j]) { - set_status(lp_status::INFEASIBLE); - e.push_justification(ci); - e.push_justification(get_column_lower_bound_witness(j)); + set_infeasible_column(j); } if (up >= m_mpq_lar_core_solver.m_r_upper_bounds[j]) return; m_mpq_lar_core_solver.m_r_upper_bounds[j] = up; @@ -1971,9 +1983,7 @@ void lar_solver::update_bound_with_ub_lb(var_index j, lconstraint_kind kind, con { auto low = numeric_pair(right_side, y_of_bound); if (low > m_mpq_lar_core_solver.m_r_upper_bounds[j]) { - set_status(lp_status::INFEASIBLE); - e.push_justification(ci); - e.push_justification(get_column_upper_bound_witness(j)); + set_infeasible_column(j); } if (low < m_mpq_lar_core_solver.m_r_lower_bounds[j]) { return; @@ -1987,15 +1997,8 @@ void lar_solver::update_bound_with_ub_lb(var_index j, lconstraint_kind kind, con case EQ: { auto v = numeric_pair(right_side, zero_of_type()); - if (v > m_mpq_lar_core_solver.m_r_upper_bounds[j]) { - set_status(lp_status::INFEASIBLE); - e.push_justification(ci); - e.push_justification(get_column_upper_bound_witness(j)); - } - if (v < m_mpq_lar_core_solver.m_r_lower_bounds[j]) { - set_status(lp_status::INFEASIBLE); - e.push_justification(ci); - e.push_justification(get_column_lower_bound_witness(j)); + if (v > m_mpq_lar_core_solver.m_r_upper_bounds[j] || v < m_mpq_lar_core_solver.m_r_lower_bounds[j]) { + set_infeasible_column(j); } set_upper_bound_witness(j, ci); set_lower_bound_witness(j, ci); @@ -2008,7 +2011,7 @@ void lar_solver::update_bound_with_ub_lb(var_index j, lconstraint_kind kind, con lp_unreachable(); } } -void lar_solver::update_bound_with_no_ub_lb(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index ci, explanation& e) { +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)); mpq y_of_bound(0); @@ -2019,9 +2022,7 @@ void lar_solver::update_bound_with_no_ub_lb(var_index j, lconstraint_kind kind, { auto up = numeric_pair(right_side, y_of_bound); if (up < m_mpq_lar_core_solver.m_r_lower_bounds[j]) { - set_status(lp_status::INFEASIBLE); - e.push_justification(ci); - e.push_justification(get_column_lower_bound_witness(j)); + set_infeasible_column(j); } m_mpq_lar_core_solver.m_r_upper_bounds[j] = up; set_upper_bound_witness(j, ci); @@ -2046,9 +2047,7 @@ void lar_solver::update_bound_with_no_ub_lb(var_index j, lconstraint_kind kind, { auto v = numeric_pair(right_side, zero_of_type()); if (v < m_mpq_lar_core_solver.m_r_lower_bounds[j]) { - set_status(lp_status::INFEASIBLE); - e.push_justification(ci); - e.push_justification(get_column_lower_bound_witness(j)); + set_infeasible_column(j); } set_upper_bound_witness(j, ci); @@ -2064,7 +2063,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, explanation& e) { +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)); mpq y_of_bound(0); @@ -2086,9 +2085,7 @@ void lar_solver::update_bound_with_ub_no_lb(var_index j, lconstraint_kind kind, { auto low = numeric_pair(right_side, y_of_bound); if (low > m_mpq_lar_core_solver.m_r_upper_bounds[j]) { - set_status(lp_status::INFEASIBLE); - e.push_justification(ci); - e.push_justification(get_column_upper_bound_witness(j)); + set_infeasible_column(j); } m_mpq_lar_core_solver.m_r_lower_bounds[j] = low; m_columns_with_changed_bound.insert(j); @@ -2100,11 +2097,9 @@ void lar_solver::update_bound_with_ub_no_lb(var_index j, lconstraint_kind kind, { auto v = numeric_pair(right_side, zero_of_type()); if (v > m_mpq_lar_core_solver.m_r_upper_bounds[j]) { - set_status(lp_status::INFEASIBLE); - e.push_justification(ci); - e.push_justification(get_column_upper_bound_witness(j)); + set_infeasible_column(j); } - + 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; @@ -2116,7 +2111,7 @@ void lar_solver::update_bound_with_ub_no_lb(var_index j, lconstraint_kind kind, lp_unreachable(); } } -void lar_solver::update_bound_with_no_ub_no_lb(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index ci, explanation&) { +void lar_solver::update_bound_with_no_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)); m_columns_with_changed_bound.insert(j); @@ -2180,19 +2175,18 @@ bool lar_solver::tighten_term_bounds_by_delta(unsigned term_index, const impq& d return false; } } - explanation e; TRACE("cube", tout << "can tighten";); if (slv.column_has_upper_bound(j)) { if (!is_zero(delta.y)) - add_var_bound(tj, lconstraint_kind::LT, slv.m_upper_bounds[j].x - delta.x, e); + add_var_bound(tj, lconstraint_kind::LT, slv.m_upper_bounds[j].x - delta.x); else - add_var_bound(tj, lconstraint_kind::LE, slv.m_upper_bounds[j].x - delta.x, e); + add_var_bound(tj, lconstraint_kind::LE, slv.m_upper_bounds[j].x - delta.x); } if (slv.column_has_lower_bound(j)) { if (!is_zero(delta.y)) - add_var_bound(tj, lconstraint_kind::GT, slv.m_lower_bounds[j].x + delta.x, e); + add_var_bound(tj, lconstraint_kind::GT, slv.m_lower_bounds[j].x + delta.x); else - add_var_bound(tj, lconstraint_kind::GE, slv.m_lower_bounds[j].x + delta.x, e); + add_var_bound(tj, lconstraint_kind::GE, slv.m_lower_bounds[j].x + delta.x); } return true; } diff --git a/src/util/lp/lar_solver.h b/src/util/lp/lar_solver.h index 5322a801d..566a78929 100644 --- a/src/util/lp/lar_solver.h +++ b/src/util/lp/lar_solver.h @@ -193,25 +193,29 @@ public: void add_basic_var_to_core_fields(); - constraint_index add_var_bound(var_index j, lconstraint_kind kind, const mpq & right_side, explanation&) ; + constraint_index add_var_bound(var_index j, lconstraint_kind kind, const mpq & right_side) ; bool compare_values(var_index j, lconstraint_kind kind, const mpq & right_side); bool compare_values(impq const& lhs, lconstraint_kind k, const mpq & rhs); - void update_column_type_and_bound(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index constr_index, explanation&); - void update_column_type_and_bound_with_ub(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index constr_index, explanation&); - void update_column_type_and_bound_with_no_ub(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index constr_index, explanation&); - void update_bound_with_ub_lb(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index constr_index, explanation&); - void update_bound_with_no_ub_lb(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index constr_index, explanation&); - void update_bound_with_ub_no_lb(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index constr_index, explanation&); - void update_bound_with_no_ub_no_lb(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index constr_index, explanation&); + void update_column_type_and_bound(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index constr_index); + void update_column_type_and_bound_with_ub(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index constr_index); + void update_column_type_and_bound_with_no_ub(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index constr_index); + void update_bound_with_ub_lb(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index constr_index); + void update_bound_with_no_ub_lb(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index constr_index); + void update_bound_with_ub_no_lb(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index constr_index); + void update_bound_with_no_ub_no_lb(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index constr_index); - void add_var_bound_on_constraint_for_term(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index ci, explanation&); + void add_var_bound_on_constraint_for_term(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index ci); + void set_infeasible_column(unsigned j) { + set_status(lp_status::INFEASIBLE); + m_infeasible_column = j; + } void add_constraint_from_term_and_create_new_column_row(unsigned term_j, const lar_term* term, - lconstraint_kind kind, const mpq & right_side, explanation&); + lconstraint_kind kind, const mpq & right_side); unsigned row_of_basic_column(unsigned) const; @@ -313,6 +317,9 @@ public: lp_status solve(); + void fill_explanation_from_infeasible_column(explanation & evidence) const; + + unsigned get_total_iterations() const; // see http://research.microsoft.com/projects/z3/smt07.pdf // This method searches for a feasible solution with as many different values of variables, reverenced in vars, as it can find @@ -442,7 +449,7 @@ public: bool all_constrained_variables_are_registered(const vector>& left_side); - constraint_index add_constraint(const vector>& left_side_with_terms, lconstraint_kind kind_par, const mpq& right_side_parm, explanation &); + constraint_index add_constraint(const vector>& left_side_with_terms, lconstraint_kind kind_par, const mpq& right_side_parm); bool all_constraints_hold() const; bool constraint_holds(const lar_base_constraint & constr, std::unordered_map & var_map) const; bool the_relations_are_of_same_type(const vector> & evidence, lconstraint_kind & the_kind_of_sum) const; diff --git a/src/util/lp/mps_reader.h b/src/util/lp/mps_reader.h index 72616509b..bc2a8432e 100644 --- a/src/util/lp/mps_reader.h +++ b/src/util/lp/mps_reader.h @@ -817,7 +817,6 @@ public: } void fill_lar_solver_on_row(row * row, lar_solver *solver) { - explanation e; if (row->m_name != m_cost_row_name) { auto kind = get_lar_relation_from_row(row->m_type); vector> ls; @@ -825,7 +824,7 @@ public: var_index i = solver->add_var(get_var_index(s.first), false); ls.push_back(std::make_pair(s.second, i)); } - solver->add_constraint(ls, kind, row->m_right_side, e); + solver->add_constraint(ls, kind, row->m_right_side); } else { // ignore the cost row } @@ -842,24 +841,21 @@ public: vector> ls; var_index i = solver->add_var(col->m_index, false); ls.push_back(std::make_pair(numeric_traits::one(), i)); - explanation e; - solver->add_constraint(ls, GE, b->m_low, e); + solver->add_constraint(ls, GE, b->m_low); } void create_upper_constraint_for_var(column* col, bound * b, lar_solver *solver) { var_index i = solver->add_var(col->m_index, false); vector> ls; ls.push_back(std::make_pair(numeric_traits::one(), i)); - explanation e; - solver->add_constraint(ls, LE, b->m_upper, e); + solver->add_constraint(ls, LE, b->m_upper); } void create_equality_contraint_for_var(column* col, bound * b, lar_solver *solver) { var_index i = solver->add_var(col->m_index, false); vector> ls; ls.push_back(std::make_pair(numeric_traits::one(), i)); - explanation e; - solver->add_constraint(ls, EQ, b->m_fixed_value, e); + solver->add_constraint(ls, EQ, b->m_fixed_value); } void fill_lar_solver_on_columns(lar_solver * solver) {