diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 25e9d9576..832cddc06 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -258,23 +258,23 @@ class theory_lra::imp { // non-linear arithmetic scoped_ptr m_nra; - bool m_use_niil; - scoped_ptr m_niil; + bool m_use_nla; + scoped_ptr m_nla; bool m_use_nra_model; scoped_ptr m_a1, m_a2; struct switcher { theory_lra::imp& m_th_imp; scoped_ptr* m_nra; - scoped_ptr* m_niil; - bool m_use_niil; - switcher(theory_lra::imp& i): m_th_imp(i), m_nra(nullptr), m_niil(nullptr) { + scoped_ptr* m_nla; + bool m_use_nla; + switcher(theory_lra::imp& i): m_th_imp(i), m_nra(nullptr), m_nla(nullptr) { } bool need_check() { - if (m_use_niil) { - if (m_niil != nullptr) - return (*m_niil)->need_check(); + if (m_use_nla) { + if (m_nla != nullptr) + return (*m_nla)->need_check(); } else { if (m_nra != nullptr) @@ -284,9 +284,9 @@ class theory_lra::imp { } void push() { - if (m_use_niil) { - if (m_niil != nullptr) - (*m_niil)->push(); + if (m_use_nla) { + if (m_nla != nullptr) + (*m_nla)->push(); } else { if (m_nra != nullptr) @@ -295,9 +295,9 @@ class theory_lra::imp { } void pop(unsigned scopes) { - if (m_use_niil) { - if (m_niil != nullptr) - (*m_niil)->pop(scopes); + if (m_use_nla) { + if (m_nla != nullptr) + (*m_nla)->pop(scopes); } else { if (m_nra != nullptr) @@ -307,9 +307,9 @@ class theory_lra::imp { void add_monomial(lp::var_index v, unsigned sz, lp::var_index const* vs) { - if (m_use_niil) { - m_th_imp.ensure_niil(); - (*m_niil)->add_monomial(v, sz, vs); + if (m_use_nla) { + m_th_imp.ensure_nla(); + (*m_nla)->add_monomial(v, sz, vs); } else { m_th_imp.ensure_nra(); @@ -383,7 +383,7 @@ class theory_lra::imp { m_solver->settings().m_int_run_gcd_test = ctx().get_fparams().m_arith_gcd_test; m_solver->settings().set_random_seed(ctx().get_fparams().m_random_seed); - m_switcher.m_use_niil = m_use_niil = lp.niil(); + m_switcher.m_use_nla = m_use_nla = lp.nla(); m_lia = alloc(lp::int_solver, m_solver.get()); get_one(true); get_zero(true); @@ -431,9 +431,14 @@ class theory_lra::imp { if (!m_niil) { m_niil = alloc(niil::solver, *m_solver.get(), m.limit(), ctx().get_params()); m_switcher.m_niil = &m_niil; + + void ensure_nla() { + if (!m_nla) { + m_nla = alloc(nla::solver, *m_solver.get(), m.limit(), ctx().get_params()); + m_switcher.m_nla = &m_nla; for (auto const& _s : m_scopes) { (void)_s; - m_niil->push(); + m_nla->push(); } } } @@ -1600,7 +1605,7 @@ public: bool is_eq(theory_var v1, theory_var v2) { if (m_use_nra_model) { - lp_assert(!m_use_niil); + lp_assert(!m_use_nla); return m_nra->am().eq(nl_value(v1, *m_a1), nl_value(v2, *m_a2)); } else { @@ -2097,9 +2102,9 @@ public: return r; } - niil::lemma m_lemma; + nla::lemma m_lemma; - lbool check_aftermath_niil(lbool r) { + lbool check_aftermath_nla(lbool r) { switch (r) { case l_false: { literal_vector core; @@ -2147,12 +2152,12 @@ public: TRACE("arith", tout << "canceled\n";); return l_undef; } - if (!m_nra && !m_niil) return l_true; + if (!m_nra && !m_nla) return l_true; if (!m_switcher.need_check()) return l_true; m_a1 = nullptr; m_a2 = nullptr; m_explanation.reset(); - lbool r = m_nra? m_nra->check(m_explanation): m_niil->check(m_explanation, m_lemma); - return m_nra? check_aftermath_nra(r) : check_aftermath_niil(r); + lbool r = m_nra? m_nra->check(m_explanation): m_nla->check(m_explanation, m_lemma); + return m_nra? check_aftermath_nra(r) : check_aftermath_nla(r); } /** diff --git a/src/util/lp/lp_params.pyg b/src/util/lp/lp_params.pyg index 02da979bd..1922b64fa 100644 --- a/src/util/lp/lp_params.pyg +++ b/src/util/lp/lp_params.pyg @@ -7,7 +7,7 @@ def_module_params('lp', ('simplex_strategy', UINT, 0, 'simplex strategy for the solver'), ('enable_hnf', BOOL, True, 'enable hnf cuts'), ('bprop_on_pivoted_rows', BOOL, True, 'propagate bounds on rows changed by the pivot operation'), - ('niil', BOOL, False, 'call nonlinear integer solver with incremental linearization') + ('nla', BOOL, False, 'call nonlinear integer solver with incremental linearization') )) diff --git a/src/util/lp/nla_solver.cpp b/src/util/lp/nla_solver.cpp index af215334b..e4c70535c 100644 --- a/src/util/lp/nla_solver.cpp +++ b/src/util/lp/nla_solver.cpp @@ -21,7 +21,7 @@ #include "util/map.h" #include "util/lp/mon_eq.h" #include "util/lp/lp_utils.h" -namespace niil { +namespace nla { typedef lp::constraint_index lpci; typedef std::unordered_set expl_set; typedef nra::mon_eq mon_eq; @@ -251,7 +251,7 @@ struct solver::imp { fill_explanation_and_lemma_sign(m_monomials[i_mon], other_m, sign * other_sign); - TRACE("niil_solver", tout << "lemma generated\n";); + TRACE("nla_solver", tout << "lemma generated\n";); return true; } @@ -291,7 +291,7 @@ struct solver::imp { add_explanation_of_reducing_to_mininal_monomial(b, expl); m_expl->clear(); m_expl->add(expl); - TRACE("niil_solver", + TRACE("nla_solver", tout << "used constraints: "; for (auto &p : *m_expl) m_lar_solver.print_constraint(p.second, tout); tout << "\n"; @@ -299,7 +299,7 @@ struct solver::imp { lp::lar_term t; t.add_coeff_var(rational(1), a.var()); t.add_coeff_var(rational(- sign), b.var()); - TRACE("niil_solver", print_explanation_and_lemma(tout);); + TRACE("nla_solver", print_explanation_and_lemma(tout);); ineq in(lp::lconstraint_kind::NE, t); m_lemma->push_back(in); } @@ -465,7 +465,7 @@ struct solver::imp { default: if (mon_val.is_zero() && var_is_fixed_to_zero(mon.var())) { create_lemma_one_of_the_factors_is_zero(mon); - TRACE("niil_solver", print_explanation_and_lemma(tout);); + TRACE("nla_solver", print_explanation_and_lemma(tout);); return true; } return false; @@ -475,7 +475,7 @@ struct solver::imp { t.m_v = -rs; ineq in(kind, t); m_lemma->push_back(in); - TRACE("niil_solver", print_explanation_and_lemma(tout);); + TRACE("nla_solver", print_explanation_and_lemma(tout);); return true; } @@ -590,7 +590,7 @@ struct solver::imp { } vector get_ones_of_monomimal(const svector & vars) { - TRACE("niil_solver", tout << "get_ones_of_monomimal";); + TRACE("nla_solver", tout << "get_ones_of_monomimal";); vector ret; for (unsigned i = 0; i < vars.size(); i++) { mono_index_with_sign mi; @@ -722,7 +722,7 @@ struct solver::imp { t.add_coeff_var(rational(- sign), j); ineq in(lp::lconstraint_kind::EQ, t); m_lemma->push_back(in); - TRACE("niil_solver", print_explanation_and_lemma(tout);); + TRACE("nla_solver", print_explanation_and_lemma(tout);); } // vars here are minimal vars for m.vs @@ -738,7 +738,7 @@ struct solver::imp { if (mask[k] == 0) { mask[k] = 1; sign *= ones_of_monomial[k].m_sign; - TRACE("niil_solver", tout << "index m_i = " << ones_of_monomial[k].m_i;); + TRACE("nla_solver", tout << "index m_i = " << ones_of_monomial[k].m_i;); vars.erase(vars.begin() + ones_of_monomial[k].m_i); std::sort(vars.begin(), vars.end()); // now the value of vars has to be v*sign @@ -811,7 +811,7 @@ struct solver::imp { bool large_lemma_for_proportion_case(const mon_eq& m, const unsigned_vector & mask, const unsigned_vector & large, unsigned j) { - TRACE("niil_solver", ); + TRACE("nla_solver", ); const rational j_val = m_lar_solver.get_column_value_rational(j); const rational m_val = m_lar_solver.get_column_value_rational(m.m_v); const rational m_abs_val = lp::abs(m_lar_solver.get_column_value_rational(m.m_v)); @@ -835,7 +835,7 @@ struct solver::imp { bool small_lemma_for_proportion_case(const mon_eq& m, const unsigned_vector & mask, const unsigned_vector & _small, unsigned j) { - TRACE("niil_solver", ); + TRACE("nla_solver", ); const rational j_val = m_lar_solver.get_column_value_rational(j); const rational m_val = m_lar_solver.get_column_value_rational(m.m_v); const rational m_abs_val = lp::abs(m_lar_solver.get_column_value_rational(m.m_v)); @@ -891,7 +891,7 @@ struct solver::imp { for (unsigned k = 0; k < mask.size(); k++) { if (mask[k] == 0) { mask[k] = 1; - TRACE("niil_solver", tout << "large[" << k << "] = " << large[k];); + TRACE("nla_solver", tout << "large[" << k << "] = " << large[k];); SASSERT(std::find(vars.begin(), vars.end(), vars_copy[large[k]]) != vars.end()); vars.erase(vars_copy[large[k]]); std::sort(vars.begin(), vars.end()); @@ -899,7 +899,7 @@ struct solver::imp { lpvar j; if (find_compimenting_monomial(vars, j) && large_lemma_for_proportion_case(m, mask, large, j)) { - TRACE("niil_solver", print_explanation_and_lemma(tout);); + TRACE("nla_solver", print_explanation_and_lemma(tout);); return true; } } else { @@ -922,7 +922,7 @@ struct solver::imp { for (unsigned k = 0; k < mask.size(); k++) { if (mask[k] == 0) { mask[k] = 1; - TRACE("niil_solver", tout << "_small[" << k << "] = " << _small[k];); + TRACE("nla_solver", tout << "_small[" << k << "] = " << _small[k];); SASSERT(std::find(vars.begin(), vars.end(), vars_copy[_small[k]]) != vars.end()); vars.erase(vars_copy[_small[k]]); std::sort(vars.begin(), vars.end()); @@ -930,7 +930,7 @@ struct solver::imp { lpvar j; if (find_compimenting_monomial(vars, j) && small_lemma_for_proportion_case(m, mask, _small, j)) { - TRACE("niil_solver", print_explanation_and_lemma(tout);); + TRACE("nla_solver", print_explanation_and_lemma(tout);); return true; } } else { @@ -949,7 +949,7 @@ struct solver::imp { unsigned_vector large; unsigned_vector _small; get_large_and_small_indices_of_monomimal(m, large, _small); - TRACE("niil_solver", tout << "large size = " << large.size() << ", _small size = " << _small.size();); + TRACE("nla_solver", tout << "large size = " << large.size() << ", _small size = " << _small.size();); if (large.empty() && _small.empty()) return false; @@ -966,7 +966,7 @@ struct solver::imp { } bool generate_basic_lemma_for_mon_proportionality(unsigned i_mon) { - TRACE("niil_solver", tout << "generate_basic_lemma_for_mon_proportionality";); + TRACE("nla_solver", tout << "generate_basic_lemma_for_mon_proportionality";); if (basic_lemma_for_mon_proportionality_from_factors_to_product(i_mon)) return true; @@ -1172,7 +1172,7 @@ struct solver::imp { } lbool check(lp::explanation & exp, lemma& l) { - TRACE("niil_solver", tout << "check of niil";); + TRACE("nla_solver", tout << "check of nla";); m_expl = &exp; m_lemma = &l; lp_assert(m_lar_solver.get_status() == lp::lp_status::OPTIMAL); @@ -1185,7 +1185,7 @@ struct solver::imp { if (to_refine.empty()) return l_true; - TRACE("niil_solver", tout << "to_refine.size() = " << to_refine.size() << std::endl;); + TRACE("nla_solver", tout << "to_refine.size() = " << to_refine.size() << std::endl;); init_search(); diff --git a/src/util/lp/nla_solver.h b/src/util/lp/nla_solver.h index 71c9eec37..c8cf074b9 100644 --- a/src/util/lp/nla_solver.h +++ b/src/util/lp/nla_solver.h @@ -24,7 +24,7 @@ Revision History: #include "util/params.h" #include "nlsat/nlsat_solver.h" #include "util/lp/lar_solver.h" -namespace niil { +namespace nla { struct ineq { lp::lconstraint_kind m_cmp; lp::lar_term m_term;