From 0e86c567ccce4a1ac0825288c47e7cfe9bf000bb Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 14 Jan 2020 16:49:40 -0800 Subject: [PATCH] prepare the mixed case Signed-off-by: Lev Nachmanson --- src/math/lp/lar_solver.cpp | 33 +++++++++++++++++++++------------ src/math/lp/lar_solver.h | 5 ++++- src/math/lp/nla_core.cpp | 8 +++----- src/smt/theory_lra.cpp | 13 +++++++++---- 4 files changed, 37 insertions(+), 22 deletions(-) diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index b8640d7af..45a33f439 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -1289,44 +1289,53 @@ void lar_solver::get_infeasibility_explanation_for_inf_sign( } } +// (x, y) != (x', y') => (x + delty*y) != (x' + delty*y') void lar_solver::get_model(std::unordered_map & variable_values) const { lp_assert(m_mpq_lar_core_solver.m_r_solver.calc_current_x_is_feasible_include_non_basis()); variable_values.clear(); - mpq delta = mpq(1, 2); // start from 0.5 to have less clashes + mpq delta = m_mpq_lar_core_solver.find_delta_for_strict_bounds(mpq(1, 2)); // start from 0.5 to have less clashes unsigned j; unsigned n = m_mpq_lar_core_solver.m_r_x.size(); + std::unordered_set set_of_different_pairs; + std::unordered_set set_of_different_singles; do { - // different pairs have to produce different singleton values - std::unordered_set set_of_different_pairs; - std::unordered_set set_of_different_singles; - delta = m_mpq_lar_core_solver.find_delta_for_strict_bounds(delta); + set_of_different_pairs.clear(); + set_of_different_singles.clear(); for (j = 0; j < n; j++ ) { const numeric_pair & rp = m_mpq_lar_core_solver.m_r_x[j]; set_of_different_pairs.insert(rp); mpq x = rp.x + delta * rp.y; set_of_different_singles.insert(x); - if (set_of_different_pairs.size() - != set_of_different_singles.size()) { + if (set_of_different_pairs.size() != set_of_different_singles.size()) { delta /= mpq(2); break; } - TRACE("get_model", tout << this->get_variable_name(j) << " := " << x << "\n";); - if (!column_corresponds_to_term(j)) - variable_values[j] = x; + variable_values[j] = x; } } while (j != n); + TRACE("lar_solver_model", tout << "delta = " << delta << "\nmodel:\n"; + for (auto p : variable_values ) { + tout << this->get_variable_name(p.first) << " = " << p.second << "\n"; + }); } void lar_solver::get_model_do_not_care_about_diff_vars(std::unordered_map & variable_values) const { - mpq delta = mpq(1); - delta = m_mpq_lar_core_solver.find_delta_for_strict_bounds(delta); + mpq delta = m_mpq_lar_core_solver.find_delta_for_strict_bounds(mpq(1)); for (unsigned i = 0; i < m_mpq_lar_core_solver.m_r_x.size(); i++ ) { const impq & rp = m_mpq_lar_core_solver.m_r_x[i]; variable_values[i] = rp.x + delta * rp.y; } } +void lar_solver::get_rid_of_inf_eps() { + mpq delta = m_mpq_lar_core_solver.find_delta_for_strict_bounds(mpq(1)); + for (unsigned j = 0; j < number_of_vars(); j++) { + auto & r = m_mpq_lar_core_solver.m_r_x[j]; + r = impq(r.x + delta * r.y); + } +} + void lar_solver::set_variable_name(var_index vi, std::string name) { m_var_register.set_name(vi, name); } diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h index 4ca0fc2d2..014b872f2 100644 --- a/src/math/lp/lar_solver.h +++ b/src/math/lp/lar_solver.h @@ -45,9 +45,10 @@ Revision History: namespace lp { +typedef unsigned lpvar; +const lpvar null_lpvar = UINT_MAX; class lar_solver : public column_namer { - typedef unsigned lpvar; struct term_hasher { std::size_t operator()(const lar_term &t) const { @@ -483,6 +484,8 @@ public: void get_model(std::unordered_map & variable_values) const; + void get_rid_of_inf_eps(); + void get_model_do_not_care_about_diff_vars(std::unordered_map & variable_values) const; std::string get_variable_name(var_index vi) const; diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index bf378f111..b07abc9e6 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -164,7 +164,8 @@ rational core::product_value(const unsigned_vector & m) const { // return true iff the monic value is equal to the product of the values of the factors bool core::check_monic(const monic& m) const { - SASSERT((!m_lar_solver.column_is_int(m.var())) || m_lar_solver.get_column_value(m.var()).is_int()); + SASSERT((!m_lar_solver.column_is_int(m.var())) || m_lar_solver.get_column_value(m.var()).is_int()); + TRACE("nla_solver", print_monic_with_vars(m, tout) << '\n';); return product_value(m.vars()) == m_lar_solver.get_column_value_rational(m.var()); } @@ -1122,13 +1123,9 @@ std::unordered_map core::get_rm_by_arity() { return m; } - - bool core::rm_check(const monic& rm) const { return check_monic(m_emons[rm.var()]); } - - /** \brief Add |v| ~ |bound| @@ -1330,6 +1327,7 @@ bool core::elists_are_consistent(bool check_in_model) const { lbool core::check(vector& l_vec) { lp_settings().stats().m_nla_calls++; TRACE("nla_solver", tout << "calls = " << lp_settings().stats().m_nla_calls << "\n";); + m_lar_solver.get_rid_of_inf_eps(); m_lemma_vec = &l_vec; if (!(m_lar_solver.get_status() == lp::lp_status::OPTIMAL || m_lar_solver.get_status() == lp::lp_status::FEASIBLE )) { TRACE("nla_solver", tout << "unknown because of the m_lar_solver.m_status = " << m_lar_solver.get_status() << "\n";); diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index a756b8477..7a0914bec 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -752,7 +752,7 @@ class theory_lra::imp { lpvar register_theory_var_in_lar_solver(theory_var v) { lpvar lpv = lp().external_to_local(v); - if (lpv + 1) + if (lpv != lp::null_lpvar) return lpv; return lp().add_var(v, is_int(v)); } @@ -3717,12 +3717,17 @@ public: } - void display(std::ostream & out) const { + void display(std::ostream & out) { if (m_solver) { lp().print_constraints(out); lp().print_terms(out); - // auto pp = lp ::core_solver_pretty_printer(lp().m_mpq_lar_core_solver.m_r_solver, out); - // pp.print(); + // the tableau + auto pp = lp ::core_solver_pretty_printer( + lp().m_mpq_lar_core_solver.m_r_solver, out); + pp.print(); + for (unsigned j = 0; j < lp().number_of_vars(); j++) { + lp().m_mpq_lar_core_solver.m_r_solver.print_column_info(j, out); + } } unsigned nv = th.get_num_vars(); for (unsigned v = 0; v < nv; ++v) {