From 029d726eb8aabbf9bc0b7266f1e7aa27b05c1970 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Mon, 25 Sep 2023 15:33:40 +0100 Subject: [PATCH 1/3] minor code simplification --- src/smt/smt_context.h | 4 +--- src/smt/smt_context_pp.cpp | 2 +- 2 files changed, 2 insertions(+), 4 deletions(-) diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 7a267fdec..f9560cb01 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -134,7 +134,6 @@ namespace smt { enode * m_lhs; enode * m_rhs; eq_justification m_justification; - new_eq() {} new_eq(enode * lhs, enode * rhs, eq_justification const & js): m_lhs(lhs), m_rhs(rhs), m_justification(js) {} }; @@ -143,7 +142,6 @@ namespace smt { theory_id m_th_id; theory_var m_lhs; theory_var m_rhs; - new_th_eq():m_th_id(null_theory_id), m_lhs(null_theory_var), m_rhs(null_theory_var) {} new_th_eq(theory_id id, theory_var l, theory_var r):m_th_id(id), m_lhs(l), m_rhs(r) {} }; svector m_th_eq_propagation_queue; @@ -215,7 +213,7 @@ namespace smt { // ----------------------------------- proto_model_ref m_proto_model; model_ref m_model; - std::string m_unknown; + const char * m_unknown; void mk_proto_model(); void reset_model() { m_model = nullptr; m_proto_model = nullptr; } diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp index fe86c6811..3925a4e21 100644 --- a/src/smt/smt_context_pp.cpp +++ b/src/smt/smt_context_pp.cpp @@ -66,6 +66,7 @@ namespace smt { std::string context::last_failure_as_string() const { std::string r; switch(m_last_search_failure) { + case UNKNOWN: case OK: r = m_unknown; break; case MEMOUT: r = "memout"; break; case CANCELED: r = "canceled"; break; @@ -82,7 +83,6 @@ namespace smt { case RESOURCE_LIMIT: r = "(resource limits reached)"; break; case QUANTIFIERS: r = "(incomplete quantifiers)"; break; case LAMBDAS: r = "(incomplete lambdas)"; break; - case UNKNOWN: r = m_unknown; break; } return r; } From 8d2b65b20bafa7cb016d44e9799047ecda4196fa Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 26 Sep 2023 19:18:44 -0700 Subject: [PATCH 2/3] add options to allow testing the effect of non-linear hammers Signed-off-by: Nikolaj Bjorner --- src/smt/params/smt_params_helper.pyg | 5 ++++- src/smt/params/theory_arith_params.cpp | 6 ++++++ src/smt/params/theory_arith_params.h | 3 +++ src/smt/theory_arith_nl.h | 6 +++++- 4 files changed, 18 insertions(+), 2 deletions(-) diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index f059dccb8..9fcda7f64 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -78,7 +78,10 @@ def_module_params(module_name='smt', ('arith.nl.grobner_cnfl_to_report', UINT, 1, 'grobner\'s maximum number of conflicts to report'), ('arith.nl.gr_q', UINT, 10, 'grobner\'s quota'), ('arith.nl.grobner_subs_fixed', UINT, 1, '0 - no subs, 1 - substitute, 2 - substitute fixed zeros only'), - ('arith.nl.delay', UINT, 500, 'number of calls to final check before invoking bounded nlsat check'), + ('arith.nl.delay', UINT, 500, 'number of calls to final check before invoking bounded nlsat check'), + ('arith.nl.propagate_linear_monomials', BOOL, True, 'propagate linear monomials'), + ('arith.nl.optimize_bounds', BOOL, True, 'enable bounds optimization'), + ('arith.nl.cross_nested', BOOL, True, 'enable cross-nested consistency checking'), ('arith.propagate_eqs', BOOL, True, 'propagate (cheap) equalities'), ('arith.propagation_mode', UINT, 1, '0 - no propagation, 1 - propagate existing literals, 2 - refine finite bounds'), ('arith.branch_cut_ratio', UINT, 2, 'branch/cut ratio for linear integer arithmetic'), diff --git a/src/smt/params/theory_arith_params.cpp b/src/smt/params/theory_arith_params.cpp index 7f3f1ca23..9bc830dd1 100644 --- a/src/smt/params/theory_arith_params.cpp +++ b/src/smt/params/theory_arith_params.cpp @@ -36,6 +36,9 @@ void theory_arith_params::updt_params(params_ref const & _p) { m_arith_bound_prop = static_cast(p.arith_propagation_mode()); m_arith_eager_eq_axioms = p.arith_eager_eq_axioms(); m_arith_auto_config_simplex = p.arith_auto_config_simplex(); + m_nl_arith_propagate_linear_monomials = p.arith_nl_propagate_linear_monomials(); + m_nl_arith_optimize_bounds = p.arith_nl_optimize_bounds(); + m_nl_arith_cross_nested = p.arith_nl_cross_nested(); arith_rewriter_params ap(_p); m_arith_eq2ineq = ap.eq2ineq(); @@ -89,4 +92,7 @@ void theory_arith_params::display(std::ostream & out) const { DISPLAY_PARAM(m_nl_arith_max_degree); DISPLAY_PARAM(m_nl_arith_branching); DISPLAY_PARAM(m_nl_arith_rounds); + DISPLAY_PARAM(m_nl_arith_propagate_linear_monomials); + DISPLAY_PARAM(m_nl_arith_optimize_bounds); + DISPLAY_PARAM(m_nl_arith_cross_nested); } diff --git a/src/smt/params/theory_arith_params.h b/src/smt/params/theory_arith_params.h index 526cb6f09..f78086300 100644 --- a/src/smt/params/theory_arith_params.h +++ b/src/smt/params/theory_arith_params.h @@ -105,6 +105,9 @@ struct theory_arith_params { unsigned m_nl_arith_max_degree = 6; bool m_nl_arith_branching = true; unsigned m_nl_arith_rounds = 1024; + bool m_nl_arith_propagate_linear_monomials = true; + bool m_nl_arith_optimize_bounds = true; + bool m_nl_arith_cross_nested = true; theory_arith_params(params_ref const & p = params_ref()) { diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h index f44516cad..ae0af89ec 100644 --- a/src/smt/theory_arith_nl.h +++ b/src/smt/theory_arith_nl.h @@ -902,6 +902,8 @@ bool theory_arith::propagate_linear_monomial(theory_var v) { */ template bool theory_arith::propagate_linear_monomials() { + if (!m_params.m_nl_arith_propagate_linear_monomials) + return false; if (!reflection_enabled()) return false; TRACE("non_linear", tout << "propagating linear monomials...\n";); @@ -2278,6 +2280,8 @@ typename theory_arith::gb_result theory_arith::compute_grobner(svector */ template bool theory_arith::max_min_nl_vars() { + if (!m_params.m_nl_arith_optimize_bounds) + return true; var_set already_found; svector vars; for (theory_var v : m_nl_monomials) { @@ -2360,7 +2364,7 @@ final_check_status theory_arith::process_non_linear() { } break; case 1: - if (!is_cross_nested_consistent(vars)) + if (m_params.m_nl_arith_cross_nested && !is_cross_nested_consistent(vars)) progress = true; break; case 2: From ec2937e2debb85448c8c008e742a2dbac36a022f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 26 Sep 2023 20:08:30 -0700 Subject: [PATCH 3/3] port over moving m_nla_lemmas into nla_core from the linear monomial propagation branch Signed-off-by: Nikolaj Bjorner --- src/math/lp/nla_basics_lemmas.cpp | 2 +- src/math/lp/nla_core.cpp | 50 +++++++++++++++---------------- src/math/lp/nla_core.h | 13 ++++---- src/math/lp/nla_solver.cpp | 19 +++++++----- src/math/lp/nla_solver.h | 9 +++--- src/sat/smt/arith_solver.cpp | 4 +-- src/sat/smt/arith_solver.h | 1 - src/smt/theory_lra.cpp | 16 +++++----- src/test/lp/nla_solver_test.cpp | 50 ++++++++++++++----------------- 9 files changed, 80 insertions(+), 84 deletions(-) diff --git a/src/math/lp/nla_basics_lemmas.cpp b/src/math/lp/nla_basics_lemmas.cpp index 7124fd409..191e59a79 100644 --- a/src/math/lp/nla_basics_lemmas.cpp +++ b/src/math/lp/nla_basics_lemmas.cpp @@ -104,7 +104,7 @@ bool basics::basic_sign_lemma_model_based() { return true; } } - return c().m_lemma_vec->size() > 0; + return c().m_lemmas.size() > 0; } diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index 3ab89e012..4990a087c 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -808,7 +808,7 @@ void core::print_stats(std::ostream& out) { void core::clear() { - m_lemma_vec->clear(); + m_lemmas.clear(); m_literal_vec->clear(); } @@ -1045,7 +1045,7 @@ rational core::val(const factorization& f) const { } new_lemma::new_lemma(core& c, char const* name):name(name), c(c) { - c.m_lemma_vec->push_back(lemma()); + c.m_lemmas.push_back(lemma()); } new_lemma& new_lemma::operator|=(ineq const& ineq) { @@ -1067,7 +1067,7 @@ new_lemma::~new_lemma() { } lemma& new_lemma::current() const { - return c.m_lemma_vec->back(); + return c.m_lemmas.back(); } new_lemma& new_lemma::operator&=(lp::explanation const& e) { @@ -1180,7 +1180,7 @@ void core::negate_relation(new_lemma& lemma, unsigned j, const rational& a) { } bool core::conflict_found() const { - for (const auto & l : * m_lemma_vec) { + for (const auto & l : m_lemmas) { if (l.is_conflict()) return true; } @@ -1188,7 +1188,7 @@ bool core::conflict_found() const { } bool core::done() const { - return m_lemma_vec->size() >= 10 || + return m_lemmas.size() >= 10 || conflict_found() || lp_settings().get_cancel_flag(); } @@ -1477,7 +1477,7 @@ void core::check_weighted(unsigned sz, std::pair 0 && !done() && m_lemma_vec->empty()) { + while (bound > 0 && !done() && m_lemmas.empty()) { unsigned n = random() % bound; for (unsigned i = 0; i < sz; ++i) { if (seen.contains(i)) @@ -1493,13 +1493,13 @@ void core::check_weighted(unsigned sz, std::pair& l_vec) { - m_lemma_vec = &l_vec; - return m_powers.check(r, x, y, l_vec); +lbool core::check_power(lpvar r, lpvar x, lpvar y) { + m_lemmas.reset(); + return m_powers.check(r, x, y, m_lemmas); } -void core::check_bounded_divisions(vector& l_vec) { - m_lemma_vec = &l_vec; +void core::check_bounded_divisions() { + m_lemmas.reset(); m_divisions.check_bounded_divisions(); } // looking for a free variable inside of a monic to split @@ -1518,11 +1518,10 @@ void core::add_bounds() { } } -lbool core::check(vector& lits, vector& l_vec) { +lbool core::check(vector& lits) { lp_settings().stats().m_nla_calls++; TRACE("nla_solver", tout << "calls = " << lp_settings().stats().m_nla_calls << "\n";); lra.get_rid_of_inf_eps(); - m_lemma_vec = &l_vec; m_literal_vec = &lits; if (!(lra.get_status() == lp::lp_status::OPTIMAL || lra.get_status() == lp::lp_status::FEASIBLE)) { @@ -1543,7 +1542,7 @@ lbool core::check(vector& lits, vector& l_vec) { bool run_bounded_nlsat = should_run_bounded_nlsat(); bool run_bounds = params().arith_nl_branching(); - auto no_effect = [&]() { return !done() && l_vec.empty() && lits.empty(); }; + auto no_effect = [&]() { return !done() && m_lemmas.empty() && lits.empty(); }; if (no_effect()) m_monomial_bounds.propagate(); @@ -1561,7 +1560,7 @@ lbool core::check(vector& lits, vector& l_vec) { {1, check2}, {1, check3} }; check_weighted(3, checks); - if (!l_vec.empty() || !lits.empty()) + if (!m_lemmas.empty() || !lits.empty()) return l_false; } @@ -1598,15 +1597,15 @@ lbool core::check(vector& lits, vector& l_vec) { m_stats.m_nra_calls++; } - if (ret == l_undef && !l_vec.empty() && m_reslim.inc()) + if (ret == l_undef && !m_lemmas.empty() && m_reslim.inc()) ret = l_false; - m_stats.m_nla_lemmas += l_vec.size(); - for (const auto& l : l_vec) + m_stats.m_nla_lemmas += m_lemmas.size(); + for (const auto& l : m_lemmas) m_stats.m_nla_explanations += static_cast(l.expl().size()); - TRACE("nla_solver", tout << "ret = " << ret << ", lemmas count = " << l_vec.size() << "\n";); + TRACE("nla_solver", tout << "ret = " << ret << ", lemmas count = " << m_lemmas.size() << "\n";); IF_VERBOSE(2, if(ret == l_undef) {verbose_stream() << "Monomials\n"; print_monics(verbose_stream());}); CTRACE("nla_solver", ret == l_undef, tout << "Monomials\n"; print_monics(tout);); return ret; @@ -1641,13 +1640,13 @@ lbool core::bounded_nlsat() { m_nlsat_delay /= 2; } if (ret == l_true) { - m_lemma_vec->reset(); + m_lemmas.reset(); } return ret; } bool core::no_lemmas_hold() const { - for (auto & l : * m_lemma_vec) { + for (auto & l : m_lemmas) { if (lemma_holds(l)) { TRACE("nla_solver", print_lemma(l, tout);); return false; @@ -1656,10 +1655,10 @@ bool core::no_lemmas_hold() const { return true; } -lbool core::test_check(vector& l) { +lbool core::test_check() { vector lits; lra.set_status(lp::lp_status::OPTIMAL); - return check(lits, l); + return check(lits); } std::ostream& core::print_terms(std::ostream& out) const { @@ -1811,12 +1810,11 @@ bool core::improve_bounds() { return bounds_improved; } -void core::propagate(vector& lemmas) { +void core::propagate() { // disable for now return; // propagate linear monomials - lemmas.reset(); - m_lemma_vec = &lemmas; + m_lemmas.reset(); m_monomial_bounds.unit_propagate(); diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h index 9c96f2fbf..b50e43b32 100644 --- a/src/math/lp/nla_core.h +++ b/src/math/lp/nla_core.h @@ -85,7 +85,7 @@ class core { reslimit& m_reslim; smt_params_helper m_params; std::function m_relevant; - vector * m_lemma_vec; + vector m_lemmas; vector * m_literal_vec = nullptr; indexed_uint_set m_to_refine; tangents m_tangents; @@ -386,15 +386,15 @@ public: bool conflict_found() const; - lbool check(vector& ineqs, vector& l_vec); - lbool check_power(lpvar r, lpvar x, lpvar y, vector& l_vec); - void check_bounded_divisions(vector&); + lbool check(vector& ineqs); + lbool check_power(lpvar r, lpvar x, lpvar y); + void check_bounded_divisions(); bool no_lemmas_hold() const; - void propagate(vector& lemmas); + void propagate(); - lbool test_check(vector& l); + lbool test_check(); lpvar map_to_root(lpvar) const; std::ostream& print_terms(std::ostream&) const; std::ostream& print_term(const lp::lar_term&, std::ostream&) const; @@ -428,6 +428,7 @@ public: void set_use_nra_model(bool m); bool use_nra_model() const { return m_use_nra_model; } void collect_statistics(::statistics&); + vector const& lemmas() const { return m_lemmas; } private: void restore_patched_values(); void constrain_nl_in_tableau(); diff --git a/src/math/lp/nla_solver.cpp b/src/math/lp/nla_solver.cpp index b7197ff2f..5417d5d63 100644 --- a/src/math/lp/nla_solver.cpp +++ b/src/math/lp/nla_solver.cpp @@ -42,12 +42,12 @@ namespace nla { bool solver::need_check() { return m_core->has_relevant_monomial(); } - lbool solver::check(vector& lits, vector& lemmas) { - return m_core->check(lits, lemmas); + lbool solver::check(vector& lits) { + return m_core->check(lits); } - void solver::propagate(vector& lemmas) { - m_core->propagate(lemmas); + void solver::propagate() { + m_core->propagate(); } void solver::push(){ @@ -93,12 +93,15 @@ namespace nla { } // ensure r = x^y, add abstraction/refinement lemmas - lbool solver::check_power(lpvar r, lpvar x, lpvar y, vector& lemmas) { - return m_core->check_power(r, x, y, lemmas); + lbool solver::check_power(lpvar r, lpvar x, lpvar y) { + return m_core->check_power(r, x, y); } - void solver::check_bounded_divisions(vector& lemmas) { - m_core->check_bounded_divisions(lemmas); + void solver::check_bounded_divisions() { + m_core->check_bounded_divisions(); } + vector const& solver::lemmas() const { + return m_core->lemmas(); + } } diff --git a/src/math/lp/nla_solver.h b/src/math/lp/nla_solver.h index 7a8a97b3f..9a1bf9d14 100644 --- a/src/math/lp/nla_solver.h +++ b/src/math/lp/nla_solver.h @@ -31,14 +31,14 @@ namespace nla { void add_idivision(lpvar q, lpvar x, lpvar y); void add_rdivision(lpvar q, lpvar x, lpvar y); void add_bounded_division(lpvar q, lpvar x, lpvar y); - void check_bounded_divisions(vector&); + void check_bounded_divisions(); void set_relevant(std::function& is_relevant); void push(); void pop(unsigned scopes); bool need_check(); - lbool check(vector& lits, vector&); - void propagate(vector& lemmas); - lbool check_power(lpvar r, lpvar x, lpvar y, vector&); + lbool check(vector& lits); + void propagate(); + lbool check_power(lpvar r, lpvar x, lpvar y); bool is_monic_var(lpvar) const; bool influences_nl_var(lpvar) const; std::ostream& display(std::ostream& out) const; @@ -47,5 +47,6 @@ namespace nla { nlsat::anum_manager& am(); nlsat::anum const& am_value(lp::var_index v) const; void collect_statistics(::statistics & st); + vector const& lemmas() const; }; } diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp index c06b8fafb..4c6e5b4be 100644 --- a/src/sat/smt/arith_solver.cpp +++ b/src/sat/smt/arith_solver.cpp @@ -1459,11 +1459,11 @@ namespace arith { return l_true; m_a1 = nullptr; m_a2 = nullptr; - lbool r = m_nla->check(m_nla_literals, m_nla_lemma_vector); + lbool r = m_nla->check(m_nla_literals); switch (r) { case l_false: assume_literals(); - for (const nla::lemma& l : m_nla_lemma_vector) + for (const nla::lemma& l : m_nla->lemmas()) false_case_of_check_nla(l); break; case l_true: diff --git a/src/sat/smt/arith_solver.h b/src/sat/smt/arith_solver.h index e23162393..f21e41786 100644 --- a/src/sat/smt/arith_solver.h +++ b/src/sat/smt/arith_solver.h @@ -248,7 +248,6 @@ namespace arith { // lemmas lp::explanation m_explanation; - vector m_nla_lemma_vector; vector m_nla_literals; literal_vector m_core, m_core2; vector m_coeffs; diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 41426e0d6..518cffe25 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -1598,11 +1598,11 @@ public: return FC_DONE; if (!m_nla) return FC_GIVEUP; - switch (m_nla->check_power(get_lpvar(e), get_lpvar(x), get_lpvar(y), m_nla_lemma_vector)) { + switch (m_nla->check_power(get_lpvar(e), get_lpvar(x), get_lpvar(y))) { case l_true: return FC_DONE; case l_false: - for (const nla::lemma & l : m_nla_lemma_vector) + for (const nla::lemma & l : m_nla->lemmas()) false_case_of_check_nla(l); return FC_CONTINUE; case l_undef: @@ -1800,8 +1800,8 @@ public: if (!m_nla) return true; m_nla_lemma_vector.reset(); - m_nla->check_bounded_divisions(m_nla_lemma_vector); - for (auto & lemma : m_nla_lemma_vector) + m_nla->check_bounded_divisions(); + for (auto & lemma : m_nla->lemmas()) false_case_of_check_nla(lemma); return m_nla_lemma_vector.empty(); } @@ -2022,13 +2022,13 @@ public: final_check_status check_nla_continue() { m_a1 = nullptr; m_a2 = nullptr; - lbool r = m_nla->check(m_nla_literals, m_nla_lemma_vector); + lbool r = m_nla->check(m_nla_literals); switch (r) { case l_false: for (const nla::ineq& i : m_nla_literals) assume_literal(i); - for (const nla::lemma & l : m_nla_lemma_vector) + for (const nla::lemma & l : m_nla->lemmas()) false_case_of_check_nla(l); return FC_CONTINUE; case l_true: @@ -2161,8 +2161,8 @@ public: void propagate_nla() { if (!m_nla) return; - m_nla->propagate(m_nla_lemma_vector); - for (nla::lemma const& l : m_nla_lemma_vector) + m_nla->propagate(); + for (nla::lemma const& l : m_nla->lemmas()) false_case_of_check_nla(l); } diff --git a/src/test/lp/nla_solver_test.cpp b/src/test/lp/nla_solver_test.cpp index ce934e7ca..054c6583f 100644 --- a/src/test/lp/nla_solver_test.cpp +++ b/src/test/lp/nla_solver_test.cpp @@ -179,7 +179,6 @@ void test_basic_lemma_for_mon_neutral_from_factors_to_monomial_0() { v.push_back(lp_a);v.push_back(lp_c); nla.add_monic(lp_ac, v.size(), v.begin()); - vector lv; // set abcde = ac * bde // ac = 1 then abcde = bde, but we have abcde < bde @@ -193,8 +192,9 @@ void test_basic_lemma_for_mon_neutral_from_factors_to_monomial_0() { s.set_column_value_test(lp_bde, lp::impq(rational(16))); - VERIFY(nla.get_core().test_check(lv) == l_false); + VERIFY(nla.get_core().test_check() == l_false); + auto const& lv = nla.get_core().lemmas(); nla.get_core().print_lemma(lv.back(), std::cout); ineq i0(lp_ac, llc::NE, 1); @@ -250,8 +250,6 @@ void test_basic_lemma_for_mon_neutral_from_factors_to_monomial_1() { 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()); - vector lemma; - s_set_column_value_test(s, lp_a, rational(1)); s_set_column_value_test(s, lp_b, rational(1)); s_set_column_value_test(s, lp_c, rational(1)); @@ -259,7 +257,8 @@ void test_basic_lemma_for_mon_neutral_from_factors_to_monomial_1() { s_set_column_value_test(s, lp_e, rational(1)); s_set_column_value_test(s, lp_bde, rational(3)); - VERIFY(nla.get_core().test_check(lemma) == l_false); + VERIFY(nla.get_core().test_check() == l_false); + auto const& lemma = nla.get_core().lemmas(); SASSERT(lemma[0].size() == 4); nla.get_core().print_lemma(lemma.back(), std::cout); @@ -330,7 +329,6 @@ void test_basic_lemma_for_mon_zero_from_factors_to_monomial() { lp_bde, lp_acd, lp_be); - vector lemma; // set vars s_set_column_value_test(s, lp_a, rational(1)); @@ -344,7 +342,8 @@ void test_basic_lemma_for_mon_zero_from_factors_to_monomial() { s_set_column_value_test(s, lp_acd, rational(1)); s_set_column_value_test(s, lp_be, rational(1)); - VERIFY(nla.get_core().test_check(lemma) == l_false); + VERIFY(nla.get_core().test_check() == l_false); + auto const& lemma = nla.get_core().lemmas(); nla.get_core().print_lemma(lemma.back(), std::cout); SASSERT(lemma.size() == 1 && lemma[0].size() == 2); lp::lar_term t0, t1; @@ -389,14 +388,13 @@ void test_basic_lemma_for_mon_zero_from_monomial_to_factors() { vec.push_back(lp_d); nla.add_monic(lp_acd, vec.size(), vec.begin()); - vector lemma; s_set_column_value_test(s, lp_a, rational(1)); s_set_column_value_test(s, lp_c, rational(1)); s_set_column_value_test(s, lp_d, rational(1)); s_set_column_value_test(s, lp_acd, rational(0)); - VERIFY(nla.get_core().test_check(lemma) == l_false); - + VERIFY(nla.get_core().test_check() == l_false); + auto const& lemma = nla.get_core().lemmas(); nla.get_core().print_lemma(lemma.back(), std::cout); ineq i0(lp_a, llc::EQ, 0); @@ -452,7 +450,6 @@ void test_basic_lemma_for_mon_neutral_from_monomial_to_factors() { lp_bde, lp_acd, lp_be); - vector lemma; // set all vars to 1 s_set_column_value_test(s, lp_a, rational(1)); @@ -471,8 +468,8 @@ void test_basic_lemma_for_mon_neutral_from_monomial_to_factors() { s_set_column_value_test(s, lp_b, - rational(2)); // we have bde = -b, therefore d = +-1 and e = +-1 s_set_column_value_test(s, lp_d, rational(3)); - VERIFY(nla.get_core().test_check(lemma) == l_false); - + VERIFY(nla.get_core().test_check() == l_false); + auto const& lemma = nla.get_core().lemmas(); nla.get_core().print_lemma(lemma.back(), std::cout); ineq i0(lp_d, llc::EQ, 1); @@ -584,9 +581,8 @@ void test_basic_sign_lemma() { s_set_column_value_test(s, lp_bde, rational(5)); s_set_column_value_test(s, lp_acd, rational(3)); - vector lemmas; - VERIFY(nla.get_core().test_check(lemmas) == l_false); - + VERIFY(nla.get_core().test_check() == l_false); + auto const& lemmas = nla.get_core().lemmas(); lp::lar_term t; t.add_var(lp_bde); t.add_var(lp_acd); @@ -707,9 +703,9 @@ void test_order_lemma_params(bool var_equiv, int sign) { s_set_column_value_test(s, lp_abef, nla.get_core().mon_value_by_vars(mon_cdij) + rational(1)); } - vector lemma; - VERIFY(nla.get_core().test_check(lemma) == l_false); + VERIFY(nla.get_core().test_check() == l_false); + auto const& lemma = nla.get_core().lemmas(); // lp::lar_term t; // t.add_monomial(lp_bde); // t.add_monomial(lp_acd); @@ -792,8 +788,8 @@ void test_monotone_lemma() { // set ef = ij while it has to be ef > ij s_set_column_value_test(s, lp_ef, s.get_column_value(lp_ij)); - vector lemma; - VERIFY(nla.get_core().test_check(lemma) == l_false); + VERIFY(nla.get_core().test_check() == l_false); + auto const& lemma = nla.get_core().lemmas(); nla.get_core().print_lemma(lemma.back(), std::cout); */ } @@ -821,8 +817,8 @@ void test_tangent_lemma_rat() { vec.push_back(lp_b); nla.add_monic(lp_ab, vec.size(), vec.begin()); - vector lemma; - VERIFY(nla.get_core().test_check(lemma) == l_false); + VERIFY(nla.get_core().test_check() == l_false); + auto const& lemma = nla.get_core().lemmas(); nla.get_core().print_lemma(lemma.back(), std::cout); } @@ -848,9 +844,8 @@ void test_tangent_lemma_reg() { vec.push_back(lp_b); nla.add_monic(lp_ab, vec.size(), vec.begin()); - vector lemma; - VERIFY(nla.get_core().test_check(lemma) == l_false); - nla.get_core().print_lemma(lemma.back(), std::cout); + VERIFY(nla.get_core().test_check() == l_false); + nla.get_core().print_lemma(nla.get_core().lemmas().back(), std::cout); } void test_tangent_lemma_equiv() { @@ -893,10 +888,9 @@ void test_tangent_lemma_equiv() { int mon_ab = nla.add_monic(lp_ab, vec.size(), vec.begin()); s_set_column_value_test(s, lp_ab, nla.get_core().mon_value_by_vars(mon_ab) + rational(10)); // greater by ten than the correct value - vector lemma; - VERIFY(nla.get_core().test_check(lemma) == l_false); - nla.get_core().print_lemma(lemma.back(), std::cout); + VERIFY(nla.get_core().test_check() == l_false); + nla.get_core().print_lemma(nla.get_core().lemmas().back(), std::cout); */ }