From 0dcebde0603aa0a49d2a0f082e8ac32fc851d663 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 19 Feb 2019 10:19:10 -0800 Subject: [PATCH] replace s() to lp() it theory_lra Signed-off-by: Lev Nachmanson --- src/smt/theory_lra.cpp | 264 ++++++++++++++++++++--------------------- 1 file changed, 132 insertions(+), 132 deletions(-) diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 88bdcda51..538e0d5e6 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -361,8 +361,8 @@ class theory_lra::imp { enode* get_enode(expr* e) const { return ctx().get_enode(e); } expr* get_owner(theory_var v) const { return get_enode(v)->get_owner(); } - lp::lar_solver& s() { return *m_solver.get(); } - const lp::lar_solver& s() const { return *m_solver.get(); } + lp::lar_solver& lp(){ return *m_solver.get(); } + const lp::lar_solver& lp() const { return *m_solver.get(); } void init_solver() { if (m_solver) return; @@ -376,20 +376,20 @@ class theory_lra::imp { get_zero(true); get_zero(false); - lp_params lp(ctx().get_params()); - s().settings().set_resource_limit(m_resource_limit); - s().settings().simplex_strategy() = static_cast(lp.simplex_strategy()); - s().settings().bound_propagation() = BP_NONE != propagation_mode(); - s().settings().m_enable_hnf = lp.enable_hnf(); - s().set_track_pivoted_rows(lp.bprop_on_pivoted_rows()); + lp_params lpar(ctx().get_params()); + lp().settings().set_resource_limit(m_resource_limit); + lp().settings().simplex_strategy() = static_cast(lpar.simplex_strategy()); + lp().settings().bound_propagation() = BP_NONE != propagation_mode(); + lp().settings().m_enable_hnf = lpar.enable_hnf(); + lp().set_track_pivoted_rows(lpar.bprop_on_pivoted_rows()); // todo : do not use m_arith_branch_cut_ratio for deciding on cheap cuts unsigned branch_cut_ratio = ctx().get_fparams().m_arith_branch_cut_ratio; - s().set_cut_strategy(branch_cut_ratio); + lp().set_cut_strategy(branch_cut_ratio); - s().settings().m_int_run_gcd_test = ctx().get_fparams().m_arith_gcd_test; - s().settings().set_random_seed(ctx().get_fparams().m_random_seed); - m_switcher.m_use_nla = m_use_nla = lp.nla(); + lp().settings().m_int_run_gcd_test = ctx().get_fparams().m_arith_gcd_test; + lp().settings().set_random_seed(ctx().get_fparams().m_random_seed); + m_switcher.m_use_nla = m_use_nla = lpar.nla(); m_lia = alloc(lp::int_solver, m_solver.get()); get_one(true); get_zero(true); @@ -415,10 +415,10 @@ class theory_lra::imp { app_ref cnst(a.mk_numeral(rational(c), is_int), m); mk_enode(cnst); theory_var v = mk_var(cnst); - var = s().add_var(v, true); - s().push(); - add_def_constraint(s().add_var_bound(var, lp::GE, rational(c))); - add_def_constraint(s().add_var_bound(var, lp::LE, rational(c))); + var = lp().add_var(v, true); + lp().push(); + add_def_constraint(lp().add_var_bound(var, lp::GE, rational(c))); + add_def_constraint(lp().add_var_bound(var, lp::LE, rational(c))); TRACE("arith", tout << "add " << cnst << ", var = " << var << "\n";); return var; } @@ -717,16 +717,16 @@ class theory_lra::imp { } bool theory_var_is_registered_in_lar_solver(theory_var v) const { - return s().external_is_used(v); + return lp().external_is_used(v); } - bool const has_int() const { return s().has_int_var(); } + bool const has_int() const { return lp().has_int_var(); } lpvar register_theory_var_in_lar_solver(theory_var v) { - lpvar lpv = s().external_to_local(v); + lpvar lpv = lp().external_to_local(v); if (lpv + 1) return lpv; - return s().add_var(v, is_int(v)); + return lp().add_var(v, is_int(v)); } void init_left_side(scoped_internalize_state& st) { @@ -775,7 +775,7 @@ class theory_lra::imp { m_constraint_sources.setx(index, inequality_source, null_source); m_inequalities.setx(index, lit, null_literal); ++m_stats.m_add_rows; - TRACE("arith", s().print_constraint(index, tout) << " m_stats.m_add_rows = " << m_stats.m_add_rows << "\n";); + TRACE("arith", lp().print_constraint(index, tout) << " m_stats.m_add_rows = " << m_stats.m_add_rows << "\n";); } void add_def_constraint(lp::constraint_index index) { @@ -792,7 +792,7 @@ class theory_lra::imp { bool is_infeasible() const { - return s().get_status() == lp::lp_status::INFEASIBLE; + return lp().get_status() == lp::lp_status::INFEASIBLE; } void internalize_eq(theory_var v1, theory_var v2) { @@ -804,11 +804,11 @@ class theory_lra::imp { st.coeffs().push_back(rational::minus_one()); theory_var z = internalize_linearized_def(term, st); lpvar vi = register_theory_var_in_lar_solver(z); - add_def_constraint(s().add_var_bound(vi, lp::LE, rational::zero())); + add_def_constraint(lp().add_var_bound(vi, lp::LE, rational::zero())); // if (is_infeasible()) { // process_conflict(); // exit here? // } - add_def_constraint(s().add_var_bound(vi, lp::GE, rational::zero())); + add_def_constraint(lp().add_var_bound(vi, lp::GE, rational::zero())); // if (is_infeasible()) { // process_conflict(); // } @@ -879,7 +879,7 @@ class theory_lra::imp { } lpvar get_lpvar(theory_var v) const { - return s().external_to_local(v); + return lp().external_to_local(v); } theory_var internalize_linearized_def(app* term, scoped_internalize_state& st) { @@ -903,10 +903,10 @@ class theory_lra::imp { m_left_side.push_back(std::make_pair(offset, get_one(a.is_int(term)))); } SASSERT(!m_left_side.empty()); - vi = s().add_term(m_left_side, v); - SASSERT (s().is_term(vi)); + vi = lp().add_term(m_left_side, v); + SASSERT (lp().is_term(vi)); TRACE("arith_verbose", tout << "v" << v << " := " << mk_pp(term, m) << " slack: " << vi << " scopes: " << m_scopes.size() << "\n"; - s().print_term(s().get_term(vi), tout) << "\n";); + lp().print_term(lp().get_term(vi), tout) << "\n";); } rational val; if (a.is_numeral(term, val)) { @@ -1073,7 +1073,7 @@ public: sc.m_asserted_atoms_lim = m_asserted_atoms.size(); sc.m_not_handled = m_not_handled; sc.m_underspecified_lim = m_underspecified.size(); - s().push(); + lp().push(); m_switcher.push(); } @@ -1090,7 +1090,7 @@ public: m_underspecified.shrink(m_scopes[old_size].m_underspecified_lim); m_not_handled = m_scopes[old_size].m_not_handled; m_scopes.resize(old_size); - s().pop(num_scopes); + lp().pop(num_scopes); // VERIFY(l_false != make_feasible()); m_new_bounds.reset(); m_to_check.reset(); @@ -1210,12 +1210,12 @@ public: get_enode(w)->get_owner()))); theory_var z = internalize_def(term); lpvar vi = register_theory_var_in_lar_solver(z); - add_def_constraint(s().add_var_bound(vi, lp::GE, rational::zero())); - add_def_constraint(s().add_var_bound(vi, lp::LE, rational::zero())); - add_def_constraint(s().add_var_bound(register_theory_var_in_lar_solver(v), lp::GE, rational::zero())); - add_def_constraint(s().add_var_bound(register_theory_var_in_lar_solver(v), lp::LT, abs(r))); + add_def_constraint(lp().add_var_bound(vi, lp::GE, rational::zero())); + add_def_constraint(lp().add_var_bound(vi, lp::LE, rational::zero())); + add_def_constraint(lp().add_var_bound(register_theory_var_in_lar_solver(v), lp::GE, rational::zero())); + add_def_constraint(lp().add_var_bound(register_theory_var_in_lar_solver(v), lp::LT, abs(r))); SASSERT(!is_infeasible()); - TRACE("arith", s().print_constraints(tout << term << "\n");); + TRACE("arith", lp().print_constraints(tout << term << "\n");); } void mk_idiv_mod_axioms(expr * p, expr * q) { @@ -1441,7 +1441,7 @@ public: } bool can_get_bound(theory_var v) const { - return v != null_theory_var && s().external_is_used(v); + return v != null_theory_var && lp().external_is_used(v); } bool can_get_ivalue(theory_var v) const { @@ -1453,29 +1453,29 @@ public: lp::impq get_ivalue(theory_var v) const { SASSERT(can_get_ivalue(v)); lpvar vi = get_lpvar(v); - if (!s().is_term(vi)) - return s().get_column_value(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); while (!m_todo_terms.empty()) { vi = m_todo_terms.back().first; rational coeff = m_todo_terms.back().second; m_todo_terms.pop_back(); - if (s().is_term(vi)) { - const lp::lar_term& term = s().get_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())); } } else { - result += s().get_column_value(vi) * coeff; + result += lp().get_column_value(vi) * coeff; } } return result; } rational get_value(theory_var v) const { - if (v == null_theory_var || !s().external_is_used(v)) { + if (v == null_theory_var || !lp().external_is_used(v)) { TRACE("arith", tout << "Variable v" << v << " not internalized\n";); return rational::zero(); } @@ -1484,7 +1484,7 @@ public: if (m_variable_values.count(vi) > 0) return m_variable_values[vi]; - if (!s().is_term(vi)) { + if (!lp().is_term(vi)) { TRACE("arith", tout << "not a term v" << v << "\n";); return rational::zero(); } @@ -1495,8 +1495,8 @@ public: lpvar wi = m_todo_terms.back().first; rational coeff = m_todo_terms.back().second; m_todo_terms.pop_back(); - if (s().is_term(wi)) { - const lp::lar_term& term = s().get_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) { result += m_variable_values[i.var()] * coeff * i.coeff(); @@ -1518,7 +1518,7 @@ public: reset_variable_values(); if (!m.canceled() && m_solver.get() && th.get_num_vars() > 0) { TRACE("arith", tout << "update variable values\n";); - s().get_model(m_variable_values); + lp().get_model(m_variable_values); } } @@ -1546,7 +1546,7 @@ public: } tout << "\n"; ); if (!m_use_nra_model) { - s().random_update(vars.size(), vars.c_ptr()); + lp().random_update(vars.size(), vars.c_ptr()); } m_model_eqs.reset(); TRACE("arith", display(tout);); @@ -1625,9 +1625,9 @@ public: IF_VERBOSE(12, verbose_stream() << "final-check " << m_solver->get_status() << "\n"); m_use_nra_model = false; lbool is_sat = l_true; - s().restore_rounded_columns(); - SASSERT(s().ax_is_correct()); - if (s().get_status() != lp::lp_status::OPTIMAL) { + lp().restore_rounded_columns(); + SASSERT(lp().ax_is_correct()); + if (lp().get_status() != lp::lp_status::OPTIMAL) { is_sat = make_feasible(); } final_check_status st = FC_DONE; @@ -1708,7 +1708,7 @@ public: u_map coeffs; term2coeffs(term, coeffs); TRACE("arith", - s().print_term(term, tout << "term: ") << "\n"; + lp().print_term(term, tout << "term: ") << "\n"; for (auto const& kv : coeffs) { tout << "v" << kv.m_key << " * " << kv.m_value << "\n"; } @@ -1757,7 +1757,7 @@ public: } TRACE("arith", tout << t << ": " << atom << "\n"; - s().print_term(term, tout << "bound atom: ") << (lower_bound?" >= ":" <= ") << k << "\n";); + lp().print_term(term, tout << "bound atom: ") << (lower_bound?" >= ":" <= ") << k << "\n";); ctx().internalize(atom, true); ctx().mark_as_relevant(atom.get()); return atom; @@ -1774,7 +1774,7 @@ public: // lpvar vi = m_theory_var2var_index[v]; // if (vi == UINT_MAX) // continue; - // if (!s().is_term(vi) && !var_has_bound(vi, true) && !var_has_bound(vi, false)) { + // if (!lp().is_term(vi) && !var_has_bound(vi, true) && !var_has_bound(vi, false)) { // lp::lar_term term; // term.add_coeff_var(rational::one(), vi); // app_ref b = mk_bound(term, rational::zero(), true); @@ -1901,7 +1901,7 @@ public: expr_ref var2expr(lpvar v) { std::ostringstream name; - name << "v" << s().local_to_external(v); + name << "v" << lp().local_to_external(v); return expr_ref(m.mk_const(symbol(name.str().c_str()), a.mk_int()), m); } @@ -1915,8 +1915,8 @@ public: expr_ref_vector ts(m); for (auto const& p : term) { lpvar wi = p.var(); - if (s().is_term(wi)) { - ts.push_back(multerm(p.coeff(), term2expr(s().get_term(wi)))); + if (lp().is_term(wi)) { + ts.push_back(multerm(p.coeff(), term2expr(lp().get_term(wi)))); } else { ts.push_back(multerm(p.coeff(), var2expr(wi))); @@ -1932,7 +1932,7 @@ public: } expr_ref constraint2fml(lp::constraint_index ci) { - lp::lar_base_constraint const& c = *s().constraints()[ci]; + lp::lar_base_constraint const& c = *lp().constraints()[ci]; expr_ref fml(m); expr_ref_vector ts(m); rational rhs = c.m_right_side; @@ -1953,20 +1953,20 @@ public: } void dump_cut_lemma(std::ostream& out, lp::lar_term const& term, lp::mpq const& k, lp::explanation const& ex, bool upper) { - s().print_term(term, out << "bound: "); + lp().print_term(term, out << "bound: "); out << (upper?" <= ":" >= ") << k << "\n"; for (auto const& p : term) { lpvar wi = p.var(); out << p.coeff() << " * "; - if (s().is_term(wi)) { - s().print_term(s().get_term(wi), out) << "\n"; + if (lp().is_term(wi)) { + lp().print_term(lp().get_term(wi), out) << "\n"; } else { - out << "v" << s().local_to_external(wi) << "\n"; + out << "v" << lp().local_to_external(wi) << "\n"; } } for (auto const& ev : ex) { - s().print_constraint(ev.second, out << ev.first << ": "); + lp().print_constraint(ev.second, out << ev.first << ": "); } expr_ref_vector fmls(m); for (auto const& ev : ex) { @@ -2101,13 +2101,13 @@ public: // convert the theory var back to lpvar expr_ref_vector mul(m); for (lpvar v : mon) { - theory_var w = s().local_to_external(v); + theory_var w = lp().local_to_external(v); mul.push_back(get_enode(w)->get_owner()); } app_ref t(a.mk_mul(mul.size(), mul.c_ptr()), m); VERIFY(internalize_term(t)); theory_var w = ctx().get_enode(t)->get_th_var(get_id()); - term.add_coeff_var(mon.get_coeff(), s().external_to_local(w)); + term.add_coeff_var(mon.get_coeff(), lp().external_to_local(w)); } } return term; @@ -2268,14 +2268,14 @@ public: if (BP_NONE == propagation_mode()) { return; } - int num_of_p = s().settings().st().m_num_of_implied_bounds; + int num_of_p = lp().settings().st().m_num_of_implied_bounds; (void)num_of_p; local_bound_propagator bp(*this); - s().propagate_bounds_for_touched_rows(bp); + lp().propagate_bounds_for_touched_rows(bp); if (m.canceled()) { return; } - int new_num_of_p = s().settings().st().m_num_of_implied_bounds; + int new_num_of_p = lp().settings().st().m_num_of_implied_bounds; (void)new_num_of_p; CTRACE("arith", new_num_of_p > num_of_p, tout << "found " << new_num_of_p << " implied bounds\n";); if (is_infeasible()) { @@ -2289,7 +2289,7 @@ public: } bool bound_is_interesting(unsigned vi, lp::lconstraint_kind kind, const rational & bval) const { - theory_var v = s().local_to_external(vi); + theory_var v = lp().local_to_external(vi); if (v == null_theory_var) return false; if (m_unassigned_bounds[v] == 0 || m_bounds.size() <= static_cast(v)) { @@ -2327,11 +2327,11 @@ public: void propagate_lp_solver_bound(lp::implied_bound& be) { lpvar vi = be.m_j; - theory_var v = s().local_to_external(vi); + theory_var v = lp().local_to_external(vi); if (v == null_theory_var) return; TRACE("arith", tout << "v" << v << " " << be.kind() << " " << be.m_bound << "\n"; - // if (m_unassigned_bounds[v] == 0) s().print_bound_evidence(be, tout); + // if (m_unassigned_bounds[v] == 0) lp().print_bound_evidence(be, tout); ); @@ -2352,7 +2352,7 @@ public: } TRACE("arith", tout << lit << " bound: " << *b << " first: " << first << "\n";); - s().settings().st().m_num_of_implied_bounds ++; + lp().settings().st().m_num_of_implied_bounds ++; if (first) { first = false; m_core.reset(); @@ -2360,7 +2360,7 @@ public: m_params.reset(); m_explanation.clear(); local_bound_propagator bp(*this); - s().explain_implied_bound(be, bp); + lp().explain_implied_bound(be, bp); } CTRACE("arith", m_unassigned_bounds[v] == 0, tout << "missed bound\n";); updt_unassigned_bounds(v, -1); @@ -2370,7 +2370,7 @@ public: ctx().display_literal_verbose(tout, lit); tout << "\n"; display_evidence(tout, m_explanation); - s().print_implied_bound(be, tout); + lp().print_implied_bound(be, tout); ); DEBUG_CODE( for (auto& lit : m_core) { @@ -2765,21 +2765,21 @@ 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 (!s().is_term(vi)) { + if (!lp().is_term(vi)) { return; } m_todo_vars.push_back(vi); while (!m_todo_vars.empty()) { vi = m_todo_vars.back(); m_todo_vars.pop_back(); - lp::lar_term const& term = s().get_term(vi); + lp::lar_term const& term = lp().get_term(vi); for (auto const& p : term) { lpvar wi = p.var(); - if (s().is_term(wi)) { + if (lp().is_term(wi)) { m_todo_vars.push_back(wi); } else { - unsigned w = s().local_to_external(wi); + unsigned w = lp().local_to_external(wi); m_use_list.reserve(w + 1, ptr_vector()); m_use_list[w].push_back(b); } @@ -2790,21 +2790,21 @@ public: void del_use_lists(lp_api::bound* b) { theory_var v = b->get_var(); lpvar vi = get_lpvar(v); - if (!s().is_term(vi)) { + if (!lp().is_term(vi)) { return; } m_todo_vars.push_back(vi); while (!m_todo_vars.empty()) { vi = m_todo_vars.back(); m_todo_vars.pop_back(); - lp::lar_term const& term = s().get_term(vi); + lp::lar_term const& term = lp().get_term(vi); for (auto const& coeff : term) { lpvar wi = coeff.var(); - if (s().is_term(wi)) { + if (lp().is_term(wi)) { m_todo_vars.push_back(wi); } else { - unsigned w = s().local_to_external(wi); + unsigned w = lp().local_to_external(wi); SASSERT(m_use_list[w].back() == b); m_use_list[w].pop_back(); } @@ -2894,12 +2894,12 @@ public: lp::constraint_index ci; rational value; bool is_strict; - if (s().is_term(wi)) { + if (lp().is_term(wi)) { return false; } if (mono.coeff().is_neg() == is_lub) { // -3*x ... <= lub based on lower bound for x. - if (!s().has_lower_bound(wi, ci, value, is_strict)) { + if (!lp().has_lower_bound(wi, ci, value, is_strict)) { return false; } if (is_strict) { @@ -2907,7 +2907,7 @@ public: } } else { - if (!s().has_upper_bound(wi, ci, value, is_strict)) { + if (!lp().has_upper_bound(wi, ci, value, is_strict)) { return false; } if (is_strict) { @@ -3009,8 +3009,8 @@ public: bool set_bound(lpvar vi, lp::constraint_index ci, rational const& v, bool is_lower) { - if (s().is_term(vi)) { - lpvar ti = s().adjust_term_index(vi); + if (lp().is_term(vi)) { + lpvar ti = lp().adjust_term_index(vi); auto& vec = is_lower ? m_lower_terms : m_upper_terms; if (vec.size() <= ti) { vec.resize(ti + 1, constraint_bound(UINT_MAX, rational())); @@ -3030,10 +3030,10 @@ public: bool is_strict = false; rational b; if (is_lower) { - return s().has_lower_bound(vi, ci, b, is_strict) && !is_strict && b == v; + return lp().has_lower_bound(vi, ci, b, is_strict) && !is_strict && b == v; } else { - return s().has_upper_bound(vi, ci, b, is_strict) && !is_strict && b == v; + return lp().has_upper_bound(vi, ci, b, is_strict) && !is_strict && b == v; } } @@ -3044,10 +3044,10 @@ public: rational b; lp::constraint_index ci; if (is_lower) { - return s().has_lower_bound(vi, ci, b, is_strict); + return lp().has_lower_bound(vi, ci, b, is_strict); } else { - return s().has_upper_bound(vi, ci, b, is_strict); + return lp().has_upper_bound(vi, ci, b, is_strict); } } @@ -3056,8 +3056,8 @@ 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 (s().is_term(vi)) { - theory_var v = s().local_to_external(vi); + if (lp().is_term(vi)) { + theory_var v = lp().local_to_external(vi); rational val; TRACE("arith", tout << vi << " " << v << "\n";); if (v != null_theory_var && a.is_numeral(get_owner(v), val) && bound == val) { @@ -3066,7 +3066,7 @@ public: } auto& vec = is_lower ? m_lower_terms : m_upper_terms; - lpvar ti = s().adjust_term_index(vi); + lpvar ti = lp().adjust_term_index(vi); if (vec.size() > ti) { constraint_bound& b = vec[ti]; ci = b.first; @@ -3080,10 +3080,10 @@ public: bool is_strict = false; rational b; if (is_lower) { - return s().has_lower_bound(vi, ci, b, is_strict) && b == bound && !is_strict; + return lp().has_lower_bound(vi, ci, b, is_strict) && b == bound && !is_strict; } else { - return s().has_upper_bound(vi, ci, b, is_strict) && b == bound && !is_strict; + return lp().has_upper_bound(vi, ci, b, is_strict) && b == bound && !is_strict; } } } @@ -3146,15 +3146,15 @@ public: } lbool make_feasible() { - TRACE("pcs", s().print_constraints(tout);); - auto status = s().find_feasible_solution(); + TRACE("pcs", lp().print_constraints(tout);); + auto status = lp().find_feasible_solution(); TRACE("arith_verbose", display(tout);); switch (status) { case lp::lp_status::INFEASIBLE: return l_false; case lp::lp_status::FEASIBLE: case lp::lp_status::OPTIMAL: - SASSERT(s().all_constraints_hold()); + SASSERT(lp().all_constraints_hold()); return l_true; case lp::lp_status::TIME_EXHAUSTED: @@ -3203,7 +3203,7 @@ public: void get_infeasibility_explanation_and_set_conflict() { m_explanation.clear(); - s().get_infeasibility_explanation(m_explanation); + lp().get_infeasibility_explanation(m_explanation); set_conflict(); } @@ -3219,7 +3219,7 @@ public: for (literal lit : core) { m_core.push_back(lit); } - // s().shrink_explanation_to_minimum(m_explanation); // todo, enable when perf is fixed + // lp().shrink_explanation_to_minimum(m_explanation); // todo, enable when perf is fixed /* static unsigned cn = 0; static unsigned num_l = 0; @@ -3289,20 +3289,20 @@ public: SASSERT(m_nra); SASSERT(m_use_nra_model); lpvar vi = get_lpvar(v); - if (s().is_term(vi)) { + if (lp().is_term(vi)) { m_todo_terms.push_back(std::make_pair(vi, rational::one())); TRACE("arith", tout << "v" << v << " := w" << vi << "\n"; - s().print_term(s().get_term(vi), tout) << "\n";); + lp().print_term(lp().get_term(vi), tout) << "\n";); m_nra->am().set(r, 0); while (!m_todo_terms.empty()) { rational wcoeff = m_todo_terms.back().second; vi = m_todo_terms.back().first; m_todo_terms.pop_back(); - lp::lar_term const& term = s().get_term(vi); - TRACE("arith", s().print_term(term, tout) << "\n";); + lp::lar_term const& term = lp().get_term(vi); + TRACE("arith", lp().print_term(term, tout) << "\n";); scoped_anum r1(m_nra->am()); rational c1(0); m_nra->am().set(r1, c1.to_mpq()); @@ -3310,7 +3310,7 @@ public: for (auto const & arg : term) { lpvar wi = arg.var(); c1 = arg.coeff() * wcoeff; - if (s().is_term(wi)) { + if (lp().is_term(wi)) { m_todo_terms.push_back(std::make_pair(wi, c1)); } else { @@ -3350,7 +3350,7 @@ public: theory_var v = n->get_th_var(get_id()); if (!can_get_bound(v)) return false; lpvar vi = get_lpvar(v); - if (s().has_value(vi, val)) { + if (lp().has_value(vi, val)) { TRACE("arith", tout << expr_ref(n->get_owner(), m) << " := " << val << "\n";); if (is_int(n) && !val.is_int()) return false; return true; @@ -3379,7 +3379,7 @@ public: } lpvar vi = get_lpvar(v); lp::constraint_index ci; - return s().has_lower_bound(vi, ci, val, is_strict); + return lp().has_lower_bound(vi, ci, val, is_strict); } bool get_lower(enode* n, expr_ref& r) { @@ -3398,7 +3398,7 @@ public: return false; lpvar vi = get_lpvar(v); lp::constraint_index ci; - return s().has_upper_bound(vi, ci, val, is_strict); + return lp().has_upper_bound(vi, ci, val, is_strict); } @@ -3501,7 +3501,7 @@ public: } else { vi = get_lpvar(v); - st = s().maximize_term(vi, term_max); + st = lp().maximize_term(vi, term_max); } switch (st) { case lp::lp_status::OPTIMAL: { @@ -3567,16 +3567,16 @@ public: void term2coeffs(lp::lar_term const& term, u_map& coeffs, rational const& coeff) { for (const auto & ti : term) { theory_var w; - if (s().is_term(ti.var())) { - //w = m_term_index2theory_var.get(s().adjust_term_index(ti.var()), null_theory_var); + if (lp().is_term(ti.var())) { + //w = m_term_index2theory_var.get(lp().adjust_term_index(ti.var()), null_theory_var); //if (w == null_theory_var) // if extracting expressions directly from nested term - lp::lar_term const& term1 = s().get_term(ti.var()); + lp::lar_term const& term1 = lp().get_term(ti.var()); rational coeff2 = coeff * ti.coeff(); term2coeffs(term1, coeffs, coeff2); continue; } else { - w = s().local_to_external(ti.var()); + w = lp().local_to_external(ti.var()); } rational c0(0); coeffs.find(w, c0); @@ -3636,11 +3636,11 @@ 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 (s().is_term(vi)) { - return mk_term(s().get_term(vi), is_int); + if (lp().is_term(vi)) { + return mk_term(lp().get_term(vi), is_int); } else { - theory_var w = s().external_to_local(vi); + theory_var w = lp().external_to_local(vi); return app_ref(get_enode(w)->get_owner(), m); } } @@ -3682,9 +3682,9 @@ public: void display(std::ostream & out) const { if (m_solver) { - s().print_constraints(out); - s().print_terms(out); - // auto pp = lp ::core_solver_pretty_printer(s().m_mpq_lar_core_solver.m_r_solver, out); + 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(); } unsigned nv = th.get_num_vars(); @@ -3732,7 +3732,7 @@ public: } } for (auto const& ev : evidence) { - s().print_constraint(ev.second, out << ev.first << ": "); + lp().print_constraint(ev.second, out << ev.first << ": "); } } @@ -3743,7 +3743,7 @@ public: st.update("arith-rows", m_stats.m_add_rows); st.update("arith-propagations", m_stats.m_bounds_propagations); st.update("arith-iterations", m_stats.m_num_iterations); - st.update("arith-factorizations", s().settings().st().m_num_factorizations); + st.update("arith-factorizations", lp().settings().st().m_num_factorizations); st.update("arith-pivots", m_stats.m_need_to_solve_inf); st.update("arith-plateau-iterations", m_stats.m_num_iterations_with_no_progress); st.update("arith-fixed-eqs", m_stats.m_fixed_eqs); @@ -3751,17 +3751,17 @@ public: st.update("arith-bound-propagations-lp", m_stats.m_bound_propagations1); st.update("arith-bound-propagations-cheap", m_stats.m_bound_propagations2); st.update("arith-diseq", m_stats.m_assert_diseq); - st.update("arith-make-feasible", s().settings().st().m_make_feasible); - st.update("arith-max-columns", s().settings().st().m_max_cols); - st.update("arith-max-rows", s().settings().st().m_max_rows); - st.update("gcd-calls", s().settings().st().m_gcd_calls); - st.update("gcd-conflict", s().settings().st().m_gcd_conflicts); - st.update("cube-calls", s().settings().st().m_cube_calls); - st.update("cube-success", s().settings().st().m_cube_success); - st.update("arith-patches", s().settings().st().m_patches); - st.update("arith-patches-success", s().settings().st().m_patches_success); - st.update("arith-hnf-calls", s().settings().st().m_hnf_cutter_calls); - st.update("arith-hnf-cuts", s().settings().st().m_hnf_cuts); + st.update("arith-make-feasible", lp().settings().st().m_make_feasible); + st.update("arith-max-columns", lp().settings().st().m_max_cols); + st.update("arith-max-rows", lp().settings().st().m_max_rows); + st.update("gcd-calls", lp().settings().st().m_gcd_calls); + st.update("gcd-conflict", lp().settings().st().m_gcd_conflicts); + st.update("cube-calls", lp().settings().st().m_cube_calls); + st.update("cube-success", lp().settings().st().m_cube_success); + st.update("arith-patches", lp().settings().st().m_patches); + st.update("arith-patches-success", lp().settings().st().m_patches_success); + st.update("arith-hnf-calls", lp().settings().st().m_hnf_cutter_calls); + st.update("arith-hnf-cuts", lp().settings().st().m_hnf_cuts); } };