From 8af245a4108c2783de63272a0217be9bdc1179cf Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Sat, 14 Mar 2020 19:55:14 -0700 Subject: [PATCH] use a simpler encoding for term indices Signed-off-by: Lev Nachmanson --- src/math/dd/pdd_interval.h | 7 --- src/math/lp/emonics.cpp | 1 - src/math/lp/gomory.cpp | 2 +- src/math/lp/int_cube.cpp | 3 +- src/math/lp/lar_solver.cpp | 76 ++++++++++++++------------------- src/math/lp/lar_solver.h | 12 ++---- src/math/lp/nla_core.cpp | 17 ++++---- src/math/lp/var_register.h | 30 +++++++------ src/smt/theory_lra.cpp | 44 +++++++++---------- src/test/lp/nla_solver_test.cpp | 68 ++++++++++++++--------------- 10 files changed, 117 insertions(+), 143 deletions(-) diff --git a/src/math/dd/pdd_interval.h b/src/math/dd/pdd_interval.h index 81153e4b5..70e6c9a9b 100644 --- a/src/math/dd/pdd_interval.h +++ b/src/math/dd/pdd_interval.h @@ -60,13 +60,6 @@ public: m_dep_intervals.add(t, lo, ret); } } - // f meant to be called when the separation happens - template - bool separated_from_zero(pdd const& p, u_dependency*& dep, std::function& f) { - scoped_dep_interval i(m()); - get_interval(p, i); - return m_dep_intervals.check_interval_for_conflict_on_zero(i, dep, f); - } }; } diff --git a/src/math/lp/emonics.cpp b/src/math/lp/emonics.cpp index e46298496..450e98c98 100644 --- a/src/math/lp/emonics.cpp +++ b/src/math/lp/emonics.cpp @@ -150,7 +150,6 @@ monic const* emonics::find_canonical(svector const& vars) const { return result; } - void emonics::remove_cg(lpvar v) { cell* c = m_use_lists[v].m_head; if (c == nullptr) { diff --git a/src/math/lp/gomory.cpp b/src/math/lp/gomory.cpp index 9f497fb09..449dec271 100644 --- a/src/math/lp/gomory.cpp +++ b/src/math/lp/gomory.cpp @@ -222,7 +222,7 @@ class create_cut { } for (const auto& p : m_t) { unsigned v = p.var(); - if (lia.lra.is_term(v)) { + if (lp::is_term(v)) { dump_declaration(out, v); } } diff --git a/src/math/lp/int_cube.cpp b/src/math/lp/int_cube.cpp index 87d89605d..87db17f70 100644 --- a/src/math/lp/int_cube.cpp +++ b/src/math/lp/int_cube.cpp @@ -57,8 +57,7 @@ namespace lp { } bool int_cube::tighten_term_for_cube(unsigned i) { - unsigned ti = i + lra.terms_start_index(); - if (!lra.term_is_used_as_row(ti)) + if (!lra.term_is_used_as_row(i)) return true; const lar_term* t = lra.terms()[i]; impq delta = get_cube_delta_for_term(*t); diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index 6f733da27..7cf314708 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -25,9 +25,8 @@ lar_solver::lar_solver() : m_status(lp_status::UNKNOWN), m_mpq_lar_core_solver(m_settings, *this), m_int_solver(nullptr), m_need_register_terms(false), - m_terms_start_index(1000000), - m_var_register(0), - m_term_register(m_terms_start_index), + m_var_register(false), + m_term_register(true), m_constraints(*this) {} @@ -46,16 +45,6 @@ lar_solver::~lar_solver(){ delete t; } -bool lar_solver::is_term(var_index j) const { - return j >= m_terms_start_index && j - m_terms_start_index < m_terms.size(); -} - -unsigned lar_solver::adjust_term_index(unsigned j) const { - lp_assert(is_term(j)); - return j - m_terms_start_index; -} - - bool lar_solver::use_lu() const { return m_settings.simplex_strategy() == simplex_strategy_enum::lu; } bool lar_solver::sizes_are_correct() const { @@ -72,7 +61,7 @@ std::ostream& lar_solver::print_implied_bound(const implied_bound& be, std::ostr unsigned v = be.m_j; if (is_term(v)) { out << "it is a term number " << be.m_j << std::endl; - print_term(*m_terms[be.m_j - m_terms_start_index], out); + print_term(*m_terms[unmask_term(v)], out); } else { out << get_variable_name(v); @@ -124,7 +113,7 @@ bool lar_solver::implied_bound_is_correctly_explained(implied_bound const & be, } rs_of_evidence /= ratio; } else { - lar_term & t = *m_terms[adjust_term_index(be.m_j)]; + lar_term & t = *m_terms[unmask_term(be.m_j)]; auto first_coeff = t.begin(); unsigned j = (*first_coeff).var(); auto it = coeff_map.find(j); @@ -206,7 +195,7 @@ unsigned lar_solver::adjust_column_index_to_term_index(unsigned j) const { if (is_term(j)) return j; unsigned ext_var_or_term = m_var_register.local_to_external(j); - return ext_var_or_term < m_terms_start_index ? j : ext_var_or_term; + return !is_term(ext_var_or_term) ? j : ext_var_or_term; } unsigned lar_solver::map_term_index_to_column_index(unsigned j) const { @@ -240,10 +229,10 @@ void lar_solver::explain_implied_bound(implied_bound & ib, lp_bound_propagator & } // lp_assert(implied_bound_is_correctly_explained(ib, explanation)); } - -bool lar_solver::term_is_used_as_row(unsigned term) const { - lp_assert(is_term(term)); - return m_var_register.external_is_used(term); +// here i is just the term index +bool lar_solver::term_is_used_as_row(unsigned i) const { + SASSERT(i < m_terms.size()); + return m_var_register.external_is_used(mask_term(i)); } void lar_solver::propagate_bounds_on_terms(lp_bound_propagator & bp) { @@ -640,8 +629,8 @@ lp_status lar_solver::maximize_term(unsigned j_or_term, const lar_term & lar_solver::get_term(unsigned j) const { - lp_assert(j >= m_terms_start_index); - return *m_terms[j - m_terms_start_index]; + lp_assert(is_term(j)); + return *m_terms[unmask_term(j)]; } void lar_solver::pop_core_solver_params() { @@ -684,7 +673,7 @@ void lar_solver::substitute_terms_in_linear_expression(const vector= m_terms_start_index) { - if (vj - m_terms_start_index >= m_terms.size()) - return false; - } else if ( vj >= A_r().column_count()) { - return false; + if (is_term(vj)) { + return unmask_term(vj) < m_terms.size(); } - return true; + return vj < A_r().column_count(); } @@ -1266,7 +1252,7 @@ void lar_solver::set_variable_name(var_index vi, std::string name) { } std::string lar_solver::get_variable_name(var_index j) const { - if (j >= m_terms_start_index) + if (is_term(j)) return std::string("_t") + T_to_string(j); if (j >= m_var_register.size()) return std::string("_s") + T_to_string(j); @@ -1338,8 +1324,8 @@ mpq lar_solver::get_left_side_val(const lar_base_constraint & cns, const std::u void lar_solver::fill_var_set_for_random_update(unsigned sz, var_index const * vars, vector& column_list) { for (unsigned i = 0; i < sz; i++) { var_index var = vars[i]; - if (var >= m_terms_start_index) { // handle the term - for (auto it : *m_terms[var - m_terms_start_index]) { + if (is_term(var)) { // handle the term + for (auto it : *m_terms[unmask_term(var)]) { column_list.push_back(it.var()); } } else { @@ -1584,7 +1570,7 @@ var_index lar_solver::add_named_var(unsigned ext_j, bool is_int, const std::stri var_index lar_solver::add_var(unsigned ext_j, bool is_int) { TRACE("add_var", tout << "adding var " << ext_j << (is_int? " int" : " nonint") << std::endl;); var_index local_j; - lp_assert(ext_j < m_terms_start_index); + lp_assert(!is_term(ext_j)); if (m_var_register.external_is_used(ext_j, local_j)) return local_j; lp_assert(m_columns_to_ul_pairs.size() == A_r().column_count()); @@ -1662,7 +1648,7 @@ void lar_solver::add_new_var_to_core_fields_for_mpq(bool register_in_basis) { var_index lar_solver::add_term_undecided(const vector> & coeffs) { push_term(new lar_term(coeffs)); - return m_terms_start_index + m_terms.size() - 1; + return mask_term(m_terms.size() - 1); } #if Z3DEBUG_CHECK_UNIQUE_TERMS @@ -1718,7 +1704,7 @@ var_index lar_solver::add_term(const vector> & coeffs, push_term(t); SASSERT(m_terms.size() == m_term_register.size()); unsigned adjusted_term_index = m_terms.size() - 1; - var_index ret = m_terms_start_index + adjusted_term_index; + var_index ret = mask_term(adjusted_term_index); if (use_tableau() && !coeffs.empty()) { add_row_from_term_no_constraint(m_terms.back(), ret); if (m_settings.bound_propagation()) @@ -1852,7 +1838,7 @@ void lar_solver::update_column_type_and_bound(var_index j, lconstraint_kind kind constraint_index lar_solver::add_var_bound_on_constraint_for_term(var_index j, lconstraint_kind kind, const mpq & right_side) { lp_assert(is_term(j)); - unsigned adjusted_term_index = adjust_term_index(j); + unsigned adjusted_term_index = unmask_term(j); // lp_assert(!term_is_int(m_terms[adjusted_term_index]) || right_side.is_int()); unsigned term_j; lar_term const* term = m_terms[adjusted_term_index]; @@ -1932,9 +1918,9 @@ void lar_solver::adjust_initial_state_for_lu() { void lar_solver::adjust_initial_state_for_tableau_rows() { for (unsigned i = 0; i < m_terms.size(); i++) { - if (m_var_register.external_is_used(i + m_terms_start_index)) + if (m_var_register.external_is_used(mask_term(i))) continue; - add_row_from_term_no_constraint(m_terms[i], i + m_terms_start_index); + add_row_from_term_no_constraint(m_terms[i], mask_term(i)); } } @@ -2176,7 +2162,7 @@ void lar_solver::update_bound_with_no_ub_no_lb(var_index j, lconstraint_kind kin } bool lar_solver::column_corresponds_to_term(unsigned j) const { - return m_var_register.local_to_external(j) >= m_terms_start_index; + return is_term(m_var_register.local_to_external(j)); } var_index lar_solver::to_column(unsigned ext_j) const { @@ -2184,7 +2170,8 @@ var_index lar_solver::to_column(unsigned ext_j) const { } bool lar_solver::tighten_term_bounds_by_delta(unsigned term_index, const impq& delta) { - unsigned tj = term_index + m_terms_start_index; + SASSERT(!is_term(term_index)); + unsigned tj = mask_term(term_index); unsigned j; if (m_var_register.external_is_used(tj, j) == false) return true; // the term is not a column so it has no bounds @@ -2242,8 +2229,7 @@ void lar_solver::round_to_integer_solution() { void lar_solver::fix_terms_with_rounded_columns() { for (unsigned i = 0; i < m_terms.size(); i++) { - unsigned ti = i + terms_start_index(); - if (!term_is_used_as_row(ti)) + if (!term_is_used_as_row(i)) continue; bool need_to_fix = false; const lar_term & t = *m_terms[i]; @@ -2254,7 +2240,7 @@ void lar_solver::fix_terms_with_rounded_columns() { } } if (need_to_fix) { - lpvar j = external_to_local(ti); + lpvar j = m_var_register.external_to_local(mask_term(i)); impq v = t.apply(m_mpq_lar_core_solver.m_r_x); m_mpq_lar_core_solver.m_r_solver.update_x(j, v); } @@ -2274,7 +2260,7 @@ bool lar_solver::sum_first_coords(const lar_term& t, mpq & val) const { } bool lar_solver::get_equality_and_right_side_for_term_on_current_x(unsigned term_index, mpq & rs, constraint_index& ci, bool &upper_bound) const { - unsigned tj = term_index + m_terms_start_index; + unsigned tj = mask_term(term_index); unsigned j; bool is_int; if (m_var_register.external_is_used(tj, j, is_int) == false) @@ -2349,7 +2335,7 @@ void lar_solver::register_existing_terms() { if (!m_need_register_terms) { TRACE("nla_solver", tout << "registering " << m_terms.size() << " terms\n";); for (unsigned k = 0; k < m_terms.size(); k++) { - lpvar j = m_var_register.external_to_local(k + m_terms_start_index); + lpvar j = m_var_register.external_to_local(mask_term(k)); register_normalized_term(*m_terms[k], j); } } diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h index a123184e3..b807df75b 100644 --- a/src/math/lp/lar_solver.h +++ b/src/math/lp/lar_solver.h @@ -89,7 +89,6 @@ private: int_solver * m_int_solver; bool m_need_register_terms; public: - const var_index m_terms_start_index; var_register m_var_register; var_register m_term_register; stacked_vector m_columns_to_ul_pairs; @@ -109,7 +108,6 @@ public: m_normalized_terms_to_columns; // end of fields - unsigned terms_start_index() const { return m_terms_start_index; } const vector & terms() const { return m_terms; } lar_term const& term(unsigned i) const { return *m_terms[i]; } constraint_set const& constraints() const { return m_constraints; } @@ -144,7 +142,6 @@ public: return m_mpq_lar_core_solver.m_r_x[j].x; } - bool is_term(var_index j) const; bool column_is_fixed(unsigned j) const; bool column_is_free(unsigned j) const; public: @@ -246,9 +243,6 @@ public: virtual ~lar_solver(); - unsigned adjust_term_index(unsigned j) const; - - bool use_lu() const; bool sizes_are_correct() const; @@ -591,15 +585,15 @@ public: t.subst_index(p.first, p.second); } } - + std::ostream& print_column_info(unsigned j, std::ostream& out) const { m_mpq_lar_core_solver.m_r_solver.print_column_info(j, out); if (is_term(j)) { - const lar_term& t = * m_terms[j - m_terms_start_index]; + const lar_term& t = * m_terms[unmask_term(j)]; print_term_as_indices(t, out) << "\n"; } else if(column_corresponds_to_term(j)) { - const lar_term& t = * m_terms[m_var_register.local_to_external(j) - m_terms_start_index]; + const lar_term& t = * m_terms[unmask_term(m_var_register.local_to_external(j))]; print_term_as_indices(t, out) << "\n"; } return out; diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index 13c402e08..c8d3cb7d1 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -66,7 +66,7 @@ lp::lar_term core::subs_terms_to_columns(const lp::lar_term& t) const { lp::lar_term r; for (const auto& p : t) { lpvar j = p.var(); - if (m_lar_solver.is_term(j)) + if (lp::is_term(j)) j = m_lar_solver.map_term_index_to_column_index(j); r.add_monomial(p.coeff(), j); } @@ -133,7 +133,7 @@ void core::add_monic(lpvar v, unsigned sz, lpvar const* vs) { m_add_buffer.resize(sz); for (unsigned i = 0; i < sz; i++) { lpvar j = vs[i]; - if (m_lar_solver.is_term(j)) + if (lp::is_term(j)) j = m_lar_solver.map_term_index_to_column_index(j); m_add_buffer[i] = j; } @@ -840,10 +840,9 @@ void core::collect_equivs() { const lp::lar_solver& s = m_lar_solver; for (unsigned i = 0; i < s.terms().size(); i++) { - unsigned ti = i + s.terms_start_index(); - if (!s.term_is_used_as_row(ti)) + if (!s.term_is_used_as_row(i)) continue; - lpvar j = s.external_to_local(ti); + lpvar j = s.external_to_local(lp::mask_term(i)); if (var_is_fixed_to_zero(j)) { TRACE("nla_solver_eq", tout << "term = "; s.print_term_as_indices(*s.terms()[i], tout);); add_equivalence_maybe(s.terms()[i], s.get_column_upper_bound_witness(j), s.get_column_lower_bound_witness(j)); @@ -1364,8 +1363,8 @@ lbool core::test_check( } std::ostream& core::print_terms(std::ostream& out) const { - for (unsigned i=0; i< m_lar_solver.m_terms.size(); i++) { - unsigned ext = i + m_lar_solver.terms_start_index(); + for (unsigned i = 0; i< m_lar_solver.m_terms.size(); i++) { + unsigned ext = lp::mask_term(i); if (!m_lar_solver.var_is_registered(ext)) { out << "term is not registered\n"; continue; @@ -1716,8 +1715,8 @@ bool core::is_nl_var(lpvar j) const { bool core::influences_nl_var(lpvar j) const { - if (m_lar_solver.is_term(j)) - j = m_lar_solver.adjust_term_index(j); + if (lp::is_term(j)) + j = lp::unmask_term(j); if (is_nl_var(j)) return true; for (const auto & c : m_lar_solver.A_r().m_columns[j]) { diff --git a/src/math/lp/var_register.h b/src/math/lp/var_register.h index b91cf6417..490c9db13 100644 --- a/src/math/lp/var_register.h +++ b/src/math/lp/var_register.h @@ -18,6 +18,15 @@ Revision History: --*/ #pragma once namespace lp { +const unsigned EF = UINT_MAX >> 1; +const unsigned left_most_bit = ~EF; + +inline unsigned unmask_term(unsigned j) { return j & EF; } + +inline bool is_term(unsigned j) { return j & left_most_bit; } + +inline unsigned mask_term(unsigned j) { return j | left_most_bit; } + class ext_var_info { unsigned m_external_j; bool m_is_integer; @@ -37,9 +46,10 @@ public: class var_register { svector m_local_to_external; std::unordered_map m_external_to_local; - unsigned m_local_offset; + unsigned m_locals_mask; + unsigned m_locals_mask_inverted; public: - var_register(unsigned offset) : m_local_offset(offset) {} + var_register(bool mask_locals): m_locals_mask(mask_locals? left_most_bit: 0), m_locals_mask_inverted(~m_locals_mask) {} void set_name(unsigned j, std::string name) { m_local_to_external[j].set_name(name); @@ -58,7 +68,7 @@ public: } m_local_to_external.push_back(ext_var_info(user_var, is_int)); - unsigned local = size() - 1 + m_local_offset; + unsigned local = ( size() - 1 ) | m_locals_mask; if (user_var != UINT_MAX) m_external_to_local[user_var] = local; @@ -75,11 +85,7 @@ public: // returns UINT_MAX if unsigned local_to_external(unsigned local_var) const { - if (local_var == UINT_MAX) - return UINT_MAX; - if (local_var < m_local_offset) - return UINT_MAX; - unsigned k = local_var - m_local_offset; + unsigned k = local_var & m_locals_mask_inverted; if (k >= m_local_to_external.size()) return UINT_MAX; return m_local_to_external[k].external_j(); @@ -119,16 +125,14 @@ public: local_j = UINT_MAX; return false; } - local_j = it->second; - SASSERT(local_j >= m_local_offset); - is_int = m_local_to_external[local_j - m_local_offset].is_integer(); + local_j = it->second & m_locals_mask_inverted; + is_int = m_local_to_external[local_j].is_integer(); return true; } bool local_is_int(unsigned j) const { - SASSERT(j >= m_local_offset); - return m_local_to_external[j - m_local_offset].is_integer(); + return m_local_to_external[j & m_locals_mask_inverted].is_integer(); } void shrink(unsigned shrunk_size) { diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index c5cb34e8b..e7e8a0a4b 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -965,7 +965,7 @@ class theory_lra::imp { } SASSERT(!m_left_side.empty()); vi = lp().add_term(m_left_side, v); - SASSERT (lp().is_term(vi)); + SASSERT (lp::is_term(vi)); TRACE("arith_verbose", tout << "v" << v << " := " << mk_pp(term, m) << " slack: " << vi << " scopes: " << m_scopes.size() << "\n"; lp().print_term(lp().get_term(vi), tout) << "\n";); } @@ -1480,7 +1480,7 @@ public: lp::impq get_ivalue(theory_var v) const { SASSERT(can_get_ivalue(v)); lpvar vi = get_lpvar(v); - if (!lp().is_term(vi)) + if (!lp::is_term(vi)) return lp().get_column_value(vi); m_todo_terms.push_back(std::make_pair(vi, rational::one())); lp::impq result(0); @@ -1488,7 +1488,7 @@ public: vi = m_todo_terms.back().first; rational coeff = m_todo_terms.back().second; m_todo_terms.pop_back(); - if (lp().is_term(vi)) { + if (lp::is_term(vi)) { const lp::lar_term& term = lp().get_term(vi); for (const auto & i: term) { m_todo_terms.push_back(std::make_pair(i.var(), coeff * i.coeff())); @@ -1510,7 +1510,7 @@ public: if (m_variable_values.count(vi) > 0) return m_variable_values[vi]; - if (!lp().is_term(vi)) { + if (!lp::is_term(vi)) { return rational::zero(); } @@ -1520,7 +1520,7 @@ public: lpvar wi = m_todo_terms.back().first; rational coeff = m_todo_terms.back().second; m_todo_terms.pop_back(); - if (lp().is_term(wi)) { + if (lp::is_term(wi)) { const lp::lar_term& term = lp().get_term(wi); for (const auto & i : term) { if (m_variable_values.count(i.var()) > 0) { @@ -1921,7 +1921,7 @@ public: expr_ref_vector ts(m); for (auto const& p : term) { lpvar wi = p.var(); - if (lp().is_term(wi)) { + if (lp::is_term(wi)) { ts.push_back(multerm(p.coeff(), term2expr(lp().get_term(wi)))); } else { @@ -1964,7 +1964,7 @@ public: for (auto const& p : term) { lpvar wi = p.var(); out << p.coeff() << " * "; - if (lp().is_term(wi)) { + if (lp::is_term(wi)) { lp().print_term(lp().get_term(wi), out) << "\n"; } else { @@ -2755,7 +2755,7 @@ public: void add_use_lists(lp_api::bound* b) { theory_var v = b->get_var(); lpvar vi = register_theory_var_in_lar_solver(v); - if (!lp().is_term(vi)) { + if (!lp::is_term(vi)) { return; } m_todo_vars.push_back(vi); @@ -2765,7 +2765,7 @@ public: lp::lar_term const& term = lp().get_term(vi); for (auto const& p : term) { lpvar wi = p.var(); - if (lp().is_term(wi)) { + if (lp::is_term(wi)) { m_todo_vars.push_back(wi); } else { @@ -2780,7 +2780,7 @@ public: void del_use_lists(lp_api::bound* b) { theory_var v = b->get_var(); lpvar vi = get_lpvar(v); - if (!lp().is_term(vi)) { + if (!lp::is_term(vi)) { return; } m_todo_vars.push_back(vi); @@ -2790,7 +2790,7 @@ public: lp::lar_term const& term = lp().get_term(vi); for (auto const& coeff : term) { lpvar wi = coeff.var(); - if (lp().is_term(wi)) { + if (lp::is_term(wi)) { m_todo_vars.push_back(wi); } else { @@ -2877,14 +2877,14 @@ public: r.reset(); theory_var v = b.get_var(); lpvar vi = get_lpvar(v); - SASSERT(m_solver->is_term(vi)); + SASSERT(lp::is_term(vi)); lp::lar_term const& term = m_solver->get_term(vi); for (auto const mono : term) { lp::var_index wi = mono.var(); lp::constraint_index ci; rational value; bool is_strict; - if (lp().is_term(wi)) { + if (lp::is_term(wi)) { return false; } if (mono.coeff().is_neg() == is_lub) { @@ -3033,8 +3033,8 @@ public: bool set_bound(lpvar vi, lp::constraint_index ci, rational const& v, bool is_lower) { - if (lp().is_term(vi)) { - lpvar ti = lp().adjust_term_index(vi); + if (lp::is_term(vi)) { + lpvar ti = lp::unmask_term(vi); auto& vec = is_lower ? m_lower_terms : m_upper_terms; if (vec.size() <= ti) { vec.resize(ti + 1, constraint_bound(UINT_MAX, rational())); @@ -3081,7 +3081,7 @@ public: bool has_lower_bound(lpvar vi, lp::constraint_index& ci, rational const& bound) { return has_bound(vi, ci, bound, true); } bool has_bound(lpvar vi, lp::constraint_index& ci, rational const& bound, bool is_lower) { - if (lp().is_term(vi)) { + if (lp::is_term(vi)) { theory_var v = lp().local_to_external(vi); rational val; TRACE("arith", tout << vi << " " << v << "\n";); @@ -3091,7 +3091,7 @@ public: } auto& vec = is_lower ? m_lower_terms : m_upper_terms; - lpvar ti = lp().adjust_term_index(vi); + lpvar ti = lp::unmask_term(vi); if (vec.size() > ti) { constraint_bound& b = vec[ti]; ci = b.first; @@ -3327,7 +3327,7 @@ public: SASSERT(m_nra); SASSERT(m_use_nra_model); lpvar vi = get_lpvar(v); - if (lp().is_term(vi)) { + if (lp::is_term(vi)) { m_todo_terms.push_back(std::make_pair(vi, rational::one())); @@ -3348,7 +3348,7 @@ public: for (auto const & arg : term) { lpvar wi = arg.var(); c1 = arg.coeff() * wcoeff; - if (lp().is_term(wi)) { + if (lp::is_term(wi)) { m_todo_terms.push_back(std::make_pair(wi, c1)); } else { @@ -3616,8 +3616,8 @@ public: void term2coeffs(lp::lar_term const& term, u_map& coeffs, rational const& coeff) { for (const auto & ti : term) { theory_var w; - if (lp().is_term(ti.var())) { - //w = m_term_index2theory_var.get(lp().adjust_term_index(ti.m_key), null_theory_var); + if (lp::is_term(ti.var())) { + //w = m_term_index2theory_var.get(lp::unmask_term(ti.m_key), null_theory_var); //if (w == null_theory_var) // if extracting expressions directly from nested term lp::lar_term const& term1 = lp().get_term(ti.var()); rational coeff2 = coeff * ti.coeff(); @@ -3685,7 +3685,7 @@ public: app_ref mk_obj(theory_var v) { lpvar vi = get_lpvar(v); bool is_int = a.is_int(get_enode(v)->get_owner()); - if (lp().is_term(vi)) { + if (lp::is_term(vi)) { return mk_term(lp().get_term(vi), is_int); } else { diff --git a/src/test/lp/nla_solver_test.cpp b/src/test/lp/nla_solver_test.cpp index ee12466b1..c36bca048 100644 --- a/src/test/lp/nla_solver_test.cpp +++ b/src/test/lp/nla_solver_test.cpp @@ -193,9 +193,9 @@ void test_basic_lemma_for_mon_neutral_from_factors_to_monomial_0() { s.set_column_value(lp_bde, lp::impq(rational(16))); - SASSERT(nla.get_core()->test_check(lv) == l_false); + SASSERT(nla.get_core().test_check(lv) == l_false); - nla.get_core()->print_lemma(std::cout); + nla.get_core().print_lemma(std::cout); ineq i0(llc::NE, lp::lar_term(), rational(1)); i0.m_term.add_var(lp_ac); @@ -259,9 +259,9 @@ void test_basic_lemma_for_mon_neutral_from_factors_to_monomial_1() { s_set_column_value(s, lp_e, rational(1)); s_set_column_value(s, lp_bde, rational(3)); - SASSERT(nla.get_core()->test_check(lemma) == l_false); + SASSERT(nla.get_core().test_check(lemma) == l_false); SASSERT(lemma[0].size() == 4); - nla.get_core()->print_lemma(std::cout); + nla.get_core().print_lemma(std::cout); ineq i0(llc::NE, lp::lar_term(), rational(1)); i0.m_term.add_var(lp_b); @@ -343,8 +343,8 @@ void test_basic_lemma_for_mon_zero_from_factors_to_monomial() { s_set_column_value(s, lp_acd, rational(1)); s_set_column_value(s, lp_be, rational(1)); - SASSERT(nla.get_core()->test_check(lemma) == l_false); - nla.get_core()->print_lemma(std::cout); + SASSERT(nla.get_core().test_check(lemma) == l_false); + nla.get_core().print_lemma(std::cout); SASSERT(lemma.size() == 1 && lemma[0].size() == 2); ineq i0(llc::NE, lp::lar_term(), rational(0)); i0.m_term.add_var(lp_b); @@ -392,9 +392,9 @@ void test_basic_lemma_for_mon_zero_from_monomial_to_factors() { s_set_column_value(s, lp_d, rational(1)); s_set_column_value(s, lp_acd, rational(0)); - SASSERT(nla.get_core()->test_check(lemma) == l_false); + SASSERT(nla.get_core().test_check(lemma) == l_false); - nla.get_core()->print_lemma(std::cout); + nla.get_core().print_lemma(std::cout); ineq i0(llc::EQ, lp::lar_term(), rational(0)); i0.m_term.add_var(lp_a); @@ -471,10 +471,10 @@ void test_basic_lemma_for_mon_neutral_from_monomial_to_factors() { s_set_column_value(s, lp_b, - rational(2)); // we have bde = -b, therefore d = +-1 and e = +-1 s_set_column_value(s, lp_d, rational(3)); - SASSERT(nla.get_core()->test_check(lemma) == l_false); + SASSERT(nla.get_core().test_check(lemma) == l_false); - nla.get_core()->print_lemma(std::cout); + nla.get_core().print_lemma(std::cout); ineq i0(llc::EQ, lp::lar_term(), rational(1)); i0.m_term.add_var(lp_d); ineq i1(llc::EQ, lp::lar_term(), -rational(1)); @@ -587,14 +587,14 @@ void test_basic_sign_lemma() { s_set_column_value(s, lp_acd, rational(3)); vector lemmas; - SASSERT(nla.get_core()->test_check(lemmas) == l_false); + SASSERT(nla.get_core().test_check(lemmas) == l_false); lp::lar_term t; t.add_var(lp_bde); t.add_var(lp_acd); ineq q(llc::EQ, t, rational(0)); - nla.get_core()->print_lemma(std::cout); + nla.get_core().print_lemma(std::cout); } void test_order_lemma_params(bool var_equiv, int sign) { @@ -686,10 +686,10 @@ void test_order_lemma_params(bool var_equiv, int sign) { s_set_column_value(s, lp_k, s.get_column_value(lp_j)); } // set the values of ab, ef, cd, and ij correctly - s_set_column_value(s, lp_ab, nla.get_core()->mon_value_by_vars(mon_ab)); - s_set_column_value(s, lp_ef, nla.get_core()->mon_value_by_vars(mon_ef)); - s_set_column_value(s, lp_cd, nla.get_core()->mon_value_by_vars(mon_cd)); - s_set_column_value(s, lp_ij, nla.get_core()->mon_value_by_vars(mon_ij)); + s_set_column_value(s, lp_ab, nla.get_core().mon_value_by_vars(mon_ab)); + s_set_column_value(s, lp_ef, nla.get_core().mon_value_by_vars(mon_ef)); + s_set_column_value(s, lp_cd, nla.get_core().mon_value_by_vars(mon_cd)); + s_set_column_value(s, lp_ij, nla.get_core().mon_value_by_vars(mon_ij)); // set abef = cdij, while it has to be abef < cdij if (sign > 0) { @@ -697,27 +697,27 @@ void test_order_lemma_params(bool var_equiv, int sign) { // we have ab < cd // we need to have ab*ef < cd*ij, so let us make ab*ef > cd*ij - s_set_column_value(s, lp_cdij, nla.get_core()->mon_value_by_vars(mon_cdij)); - s_set_column_value(s, lp_abef, nla.get_core()->mon_value_by_vars(mon_cdij) + s_set_column_value(s, lp_cdij, nla.get_core().mon_value_by_vars(mon_cdij)); + s_set_column_value(s, lp_abef, nla.get_core().mon_value_by_vars(mon_cdij) + rational(1)); } else { SASSERT(-s.get_column_value(lp_ab) < s.get_column_value(lp_cd)); // we need to have abef < cdij, so let us make abef < cdij - s_set_column_value(s, lp_cdij, nla.get_core()->mon_value_by_vars(mon_cdij)); - s_set_column_value(s, lp_abef, nla.get_core()->mon_value_by_vars(mon_cdij) + s_set_column_value(s, lp_cdij, nla.get_core().mon_value_by_vars(mon_cdij)); + s_set_column_value(s, lp_abef, nla.get_core().mon_value_by_vars(mon_cdij) + rational(1)); } vector lemma; - SASSERT(nla.get_core()->test_check(lemma) == l_false); + SASSERT(nla.get_core().test_check(lemma) == l_false); // lp::lar_term t; // t.add_monomial(lp_bde); // t.add_monomial(lp_acd); // ineq q(llc::EQ, t, rational(0)); - nla.get_core()->print_lemma(std::cout); + nla.get_core().print_lemma(std::cout); // SASSERT(q == lemma.back()); // ineq i0(llc::EQ, lp::lar_term(), rational(0)); // i0.m_term.add_monomial(lp_bde); @@ -787,16 +787,16 @@ void test_monotone_lemma() { s_set_column_value(s, lp_f, s.get_column_value(lp_j) +lp::impq( rational(1))); // set the values of ab, ef, cd, and ij correctly - s_set_column_value(s, lp_ab, nla.get_core()->mon_value_by_vars(mon_ab)); - s_set_column_value(s, lp_cd, nla.get_core()->mon_value_by_vars(mon_cd)); - s_set_column_value(s, lp_ij, nla.get_core()->mon_value_by_vars(mon_ij)); + s_set_column_value(s, lp_ab, nla.get_core().mon_value_by_vars(mon_ab)); + s_set_column_value(s, lp_cd, nla.get_core().mon_value_by_vars(mon_cd)); + s_set_column_value(s, lp_ij, nla.get_core().mon_value_by_vars(mon_ij)); // set ef = ij while it has to be ef > ij s_set_column_value(s, lp_ef, s.get_column_value(lp_ij)); vector lemma; - SASSERT(nla.get_core()->test_check(lemma) == l_false); - nla.get_core()->print_lemma(std::cout); + SASSERT(nla.get_core().test_check(lemma) == l_false); + nla.get_core().print_lemma(std::cout); */ } @@ -824,8 +824,8 @@ void test_tangent_lemma_rat() { nla.add_monic(lp_ab, vec.size(), vec.begin()); vector lemma; - SASSERT(nla.get_core()->test_check(lemma) == l_false); - nla.get_core()->print_lemma(std::cout); + SASSERT(nla.get_core().test_check(lemma) == l_false); + nla.get_core().print_lemma(std::cout); } void test_tangent_lemma_reg() { @@ -851,8 +851,8 @@ void test_tangent_lemma_reg() { nla.add_monic(lp_ab, vec.size(), vec.begin()); vector lemma; - SASSERT(nla.get_core()->test_check(lemma) == l_false); - nla.get_core()->print_lemma(std::cout); + SASSERT(nla.get_core().test_check(lemma) == l_false); + nla.get_core().print_lemma(std::cout); } void test_tangent_lemma_equiv() { @@ -894,11 +894,11 @@ void test_tangent_lemma_equiv() { vec.push_back(lp_b); int mon_ab = nla.add_monic(lp_ab, vec.size(), vec.begin()); - s_set_column_value(s, lp_ab, nla.get_core()->mon_value_by_vars(mon_ab) + rational(10)); // greater by ten than the correct value + s_set_column_value(s, lp_ab, nla.get_core().mon_value_by_vars(mon_ab) + rational(10)); // greater by ten than the correct value vector lemma; - SASSERT(nla.get_core()->test_check(lemma) == l_false); - nla.get_core()->print_lemma(std::cout); + SASSERT(nla.get_core().test_check(lemma) == l_false); + nla.get_core().print_lemma(std::cout); */ }