From 32055a31db921044fb8279e3bbe7b8b5f1c343fe Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 12 May 2020 10:49:16 -0700 Subject: [PATCH] pass resource limits by reference Signed-off-by: Nikolaj Bjorner --- src/math/lp/nla_core.h | 2 +- src/math/lp/nla_solver.cpp | 5 +++-- src/math/lp/nla_solver.h | 3 +-- src/smt/theory_lra.cpp | 2 +- src/test/lp/nla_solver_test.cpp | 24 ++++++++++++------------ 5 files changed, 18 insertions(+), 18 deletions(-) diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h index 6e1cc06c0..fb8697d00 100644 --- a/src/math/lp/nla_core.h +++ b/src/math/lp/nla_core.h @@ -160,7 +160,7 @@ private: mutable lp::u_set m_active_var_set; lp::u_set m_rows; public: - reslimit m_reslim; + reslimit& m_reslim; void insert_to_refine(lpvar j); void erase_from_to_refine(lpvar j); diff --git a/src/math/lp/nla_solver.cpp b/src/math/lp/nla_solver.cpp index c5403b66f..f75718bb1 100644 --- a/src/math/lp/nla_solver.cpp +++ b/src/math/lp/nla_solver.cpp @@ -51,8 +51,9 @@ void solver::pop(unsigned n) { m_core->pop(n); } -solver::solver(lp::lar_solver& s): m_core(alloc(core, s, m_res_limit)), - m_nra(s, m_res_limit, *m_core) { +solver::solver(lp::lar_solver& s, reslimit& limit): + m_core(alloc(core, s, limit)), + m_nra(s, limit, *m_core) { } bool solver::influences_nl_var(lpvar j) const { diff --git a/src/math/lp/nla_solver.h b/src/math/lp/nla_solver.h index 0ee0f7a1e..b61e8a26e 100644 --- a/src/math/lp/nla_solver.h +++ b/src/math/lp/nla_solver.h @@ -22,7 +22,6 @@ namespace nla { class core; // nonlinear integer incremental linear solver class solver { - reslimit m_res_limit; core* m_core; nra::solver m_nra; bool m_use_nra_model; @@ -31,7 +30,7 @@ class solver { public: void add_monic(lpvar v, unsigned sz, lpvar const* vs); - solver(lp::lar_solver& s); + solver(lp::lar_solver& s, reslimit& limit); ~solver(); nla_settings& settings(); void push(); diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 526514782..328a5e952 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -387,7 +387,7 @@ class theory_lra::imp { void ensure_nla() { if (!m_nla) { - m_nla = alloc(nla::solver, *m_solver.get()); + m_nla = alloc(nla::solver, *m_solver.get(), m.limit()); for (auto const& _s : m_scopes) { (void)_s; m_nla->push(); diff --git a/src/test/lp/nla_solver_test.cpp b/src/test/lp/nla_solver_test.cpp index 45c719733..f52f303ce 100644 --- a/src/test/lp/nla_solver_test.cpp +++ b/src/test/lp/nla_solver_test.cpp @@ -169,7 +169,7 @@ void test_basic_lemma_for_mon_neutral_from_factors_to_monomial_0() { reslimit l; params_ref p; - solver nla(s); + solver nla(s, l); svector v; v.push_back(lp_b);v.push_back(lp_d);v.push_back(lp_e); nla.add_monic(lp_bde, v.size(), v.begin()); v.clear(); @@ -246,7 +246,7 @@ void test_basic_lemma_for_mon_neutral_from_factors_to_monomial_1() { reslimit l; params_ref p; - solver nla(s); + solver nla(s, l); svector v; v.push_back(lp_b);v.push_back(lp_d);v.push_back(lp_e); nla.add_monic(lp_bde, v.size(), v.begin()); @@ -317,7 +317,7 @@ void test_basic_lemma_for_mon_zero_from_factors_to_monomial() { reslimit l; params_ref p; - solver nla(s); + solver nla(s, l); create_abcde(nla, lp_a, @@ -379,7 +379,7 @@ void test_basic_lemma_for_mon_zero_from_monomial_to_factors() { reslimit l; params_ref p; - solver nla(s); + solver nla(s, l); // create monomial acd unsigned_vector vec; @@ -439,7 +439,7 @@ void test_basic_lemma_for_mon_neutral_from_monomial_to_factors() { reslimit l; params_ref p; - solver nla(s); + solver nla(s, l); create_abcde(nla, lp_a, @@ -514,7 +514,7 @@ void test_horner() { reslimit l; params_ref p; - solver nla(s); + solver nla(s, l); vector v; v.push_back(a); v.push_back(b); nla.add_monic(lp_ab, v.size(), v.begin()); @@ -551,7 +551,7 @@ void test_basic_sign_lemma() { reslimit l; params_ref p; - solver nla(s); + solver nla(s, l); // create monomial bde vector vec; @@ -626,7 +626,7 @@ void test_order_lemma_params(bool var_equiv, int sign) { reslimit l; params_ref p; - solver nla(s); + solver nla(s,l); // create monomial ab vector vec; vec.push_back(lp_a); @@ -757,7 +757,7 @@ void test_monotone_lemma() { reslimit l; params_ref p; - solver nla(s); + solver nla(s, l); // create monomial ab vector vec; vec.push_back(lp_a); @@ -814,7 +814,7 @@ void test_tangent_lemma_rat() { s_set_column_value_test(s, lp_ab, v); reslimit l; params_ref p; - solver nla(s); + solver nla(s, l); // create monomial ab vector vec; vec.push_back(lp_a); @@ -841,7 +841,7 @@ void test_tangent_lemma_reg() { s_set_column_value_test(s, lp_ab, rational(11)); reslimit l; params_ref p; - solver nla(s); + solver nla(s, l); // create monomial ab vector vec; vec.push_back(lp_a); @@ -885,7 +885,7 @@ void test_tangent_lemma_equiv() { s_set_column_value_test(s, lp_a, - s.get_column_value(lp_k)); reslimit l; params_ref p; - solver nla(s); + solver nla(s, l); // create monomial ab vector vec; vec.push_back(lp_a);