From 6b28973799ac245c80b46c41d7150856fbed7b9e Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 13 May 2020 13:52:42 -0700 Subject: [PATCH] nla review (#4321) * simplify the nla_solver interface Signed-off-by: Lev Nachmanson * more simplifications Signed-off-by: Lev Nachmanson * init m_use_nra_model Signed-off-by: Lev Nachmanson * work on NSB comments Signed-off-by: Lev Nachmanson * work on NSB comments Signed-off-by: Lev Nachmanson Co-authored-by: Nikolaj Bjorner --- src/math/lp/gomory.cpp | 5 +- src/math/lp/int_solver.cpp | 9 ++ src/math/lp/int_solver.h | 4 +- src/math/lp/nla_basics_lemmas.cpp | 143 ++++++++++-------------------- src/math/lp/nla_basics_lemmas.h | 6 +- src/math/lp/nla_common.h | 3 + src/math/lp/nla_core.cpp | 16 ++-- src/math/lp/nla_core.h | 1 - src/math/lp/nla_solver.cpp | 1 - src/smt/theory_lra.cpp | 1 + 10 files changed, 71 insertions(+), 118 deletions(-) diff --git a/src/math/lp/gomory.cpp b/src/math/lp/gomory.cpp index 751937085..14c908dbf 100644 --- a/src/math/lp/gomory.cpp +++ b/src/math/lp/gomory.cpp @@ -346,10 +346,7 @@ public: if (some_int_columns) adjust_term_and_k_for_some_ints_case_gomory(); TRACE("gomory_cut_detail", dump_cut_and_constraints_as_smt_lemma(tout);); - lp_assert(lia.current_solution_is_inf_on_cut()); - // NSB code review: this is also used in nla_core. - // but it isn't consistent: when theory_lra accesses lar_solver::get_term, the term that is returned uses - // column indices, not terms. + lp_assert(lia.current_solution_is_inf_on_cut()); // checks that indices are columns TRACE("gomory_cut", print_linear_combination_of_column_indices_only(m_t.coeffs_as_vector(), tout << "gomory cut:"); tout << " <= " << m_k << std::endl;); return lia_move::cut; } diff --git a/src/math/lp/int_solver.cpp b/src/math/lp/int_solver.cpp index 98f87f4c4..91cf8bebd 100644 --- a/src/math/lp/int_solver.cpp +++ b/src/math/lp/int_solver.cpp @@ -189,7 +189,16 @@ std::ostream& int_solver::display_inf_rows(std::ostream& out) const { return out; } +bool int_solver::cut_indices_are_columns() const { + for (const auto & p: m_t) { + if (p.column().index() >= lra.A_r().column_count()) + return false; + } + return true; +} + bool int_solver::current_solution_is_inf_on_cut() const { + SASSERT(cut_indices_are_columns()); const auto & x = lrac.m_r_x; impq v = m_t.apply(x); mpq sign = m_upper ? one_of_type() : -one_of_type(); diff --git a/src/math/lp/int_solver.h b/src/math/lp/int_solver.h index e4dbace0b..55a308f54 100644 --- a/src/math/lp/int_solver.h +++ b/src/math/lp/int_solver.h @@ -109,8 +109,8 @@ private: bool has_upper(unsigned j) const; unsigned row_of_basic_column(unsigned j) const; bool non_basic_columns_are_at_bounds() const; - - + bool cut_indices_are_columns() const; + public: std::ostream& display_column(std::ostream & out, unsigned j) const; constraint_index column_upper_bound_constraint(unsigned j) const; diff --git a/src/math/lp/nla_basics_lemmas.cpp b/src/math/lp/nla_basics_lemmas.cpp index ea6bf2539..f77c99097 100644 --- a/src/math/lp/nla_basics_lemmas.cpp +++ b/src/math/lp/nla_basics_lemmas.cpp @@ -220,10 +220,11 @@ void basics::negate_strict_sign(new_lemma& lemma, lpvar j) { // here we use the fact // xy = 0 -> x = 0 or y = 0 bool basics::basic_lemma_for_mon_zero(const monic& rm, const factorization& f) { - // NSB review: how is the code-path calling this function disabled? - NOT_IMPLEMENTED_YET(); - return true; -#if 0 + // it seems this code is never exercised + for (auto j : f) { + if (val(j).is_zero()) + return false; + } TRACE("nla_solver", c().trace_print_monic_and_factorization(rm, f, tout);); new_lemma lemma(c(), "xy = 0 -> x = 0 or y = 0"); lemma.explain_fixed(var(rm)); @@ -235,7 +236,6 @@ bool basics::basic_lemma_for_mon_zero(const monic& rm, const factorization& f) { lemma &= rm; lemma &= f; return true; -#endif } // use basic multiplication properties to create a lemma @@ -285,8 +285,6 @@ bool basics::basic_lemma_for_mon_derived(const monic& rm) { return true; if (basic_lemma_for_mon_neutral_derived(rm, factorization)) return true; - if (proportion_lemma_derived(rm, factorization)) - return true; } } return false; @@ -375,65 +373,36 @@ void basics::proportion_lemma_model_based(const monic& rm, const factorization& factor_index++; } } -// x != 0 or y = 0 => |xy| >= |y| -bool basics::proportion_lemma_derived(const monic& rm, const factorization& factorization) { - // NSB review: why return false? - return false; - if (c().has_real(factorization)) - return false; - rational rmv = abs(var_val(rm)); - if (rmv.is_zero()) { - SASSERT(c().has_zero_factor(factorization)); - return false; - } - int factor_index = 0; - for (factor f : factorization) { - if (abs(val(f)) > rmv) { - generate_pl(rm, factorization, factor_index); - return true; - } - factor_index++; - } - return false; -} /** - if there are no zero factors then |m| >= |m[factor_index]| - m := f_1*...*f_n - sign_m*m < 0 or f_j = 0 or \/_{i != j} sign_j*f_j < 0 or sign_m*m >= sign_j*f_j + k is the index of such that |m| < |val(m[k]| + + If for all 1 <= j <= n, j != k we have f_j != 0 then |m| >= |f_k| + + The lemma looks like + sign_m*m < 0 or \/_{i != k} f_i = 0 or sign_m*m >= sign_k*f_k -NSB review: - -- This rule cannot be applied for reals - For example 1/4 = 1/2*1/2 and each factor is bigger than product. - -- Stronger rule is possible for integers: - - sign_m*m < 0 or f_j = 0 or \/_{i != j} sign_m*m >= sign_i*f_i - */ -void basics::generate_pl_on_mon(const monic& m, unsigned factor_index) { +void basics::generate_pl_on_mon(const monic& m, unsigned k) { SASSERT(!c().has_real(m)); new_lemma lemma(c(), "generate_pl_on_mon"); unsigned mon_var = m.var(); rational mv = val(mon_var); + SASSERT(abs(mv) < abs(val(m.vars()[k]))); rational sm = rational(nla::rat_sign(mv)); lemma |= ineq(term(sm, mon_var), llc::LT, 0); for (unsigned fi = 0; fi < m.size(); fi ++) { lpvar j = m.vars()[fi]; - if (fi != factor_index) { + if (fi != k) { lemma |= ineq(j, llc::EQ, 0); } else { - rational jv = val(j); - rational sj = rational(nla::rat_sign(jv)); - // NSB review: what is the justification for this assert: SASSERT(sm*mv < sj*jv); - // NSB review: removed c().mk_ineq(sj, j, llc::LT); + rational sj = rational(nla::rat_sign(val(j))); lemma |= ineq(term(sm, mon_var, -sj, j), llc::GE, 0); } } - lemma &= m; + // lemma &= m; // no need to "explain" monomial m here } /** @@ -467,13 +436,11 @@ void basics::generate_pl(const monic& m, const factorization& fc, int factor_ind lpvar j = var(f); rational jv = val(j); rational sj = rational(nla::rat_sign(jv)); - // NSB review: removed SASSERT(sm*mv < sj*jv); - // NSB review: removed lemma |= ineq(term(sj, j), llc::LT, 0); lemma |= ineq(term(sm, mon_var, -sj, j), llc::GE, 0); } } lemma &= fc; - lemma &= m; + lemma &= m; } bool basics::is_separated_from_zero(const factorization& f) const { @@ -539,37 +506,10 @@ void basics::basic_lemma_for_mon_model_based(const monic& rm) { or - /\_j f_j = val(f_j) => m = sign */ -// NSB code review: can't we just use basic_lemma_for_mon_neutral_from_factors_to_model_based? -// then the factorization is the same as the monomial. -// then the only difference is to omit adding some explanations. - bool basics::basic_lemma_for_mon_neutral_from_factors_to_monic_model_based_fm(const monic& m) { - lpvar not_one = null_lpvar; - rational sign(1); - TRACE("nla_solver_bl", tout << "m = "; c().print_monic(m, tout);); - for (auto j : m.vars()) { - auto v = val(j); - if (v == rational(1)) { - continue; - } - if (v == -rational(1)) { - sign = -sign; - continue; - } - if (not_one == null_lpvar) { - not_one = j; - continue; - } - // if we are here then there are at least two factors with values different from one and minus one: cannot create the lemma + lpvar not_one; rational sign; + if (!can_create_lemma_for_mon_neutral_from_factors_to_monic_model_based(m, m, not_one, sign)) return false; - } - - if (not_one != null_lpvar) { // we found the only not_one - if (var_val(m) == val(not_one) * sign) { - TRACE("nla_solver", tout << "the whole equal to the factor" << std::endl;); - return false; - } - } new_lemma lemma(c(), __FUNCTION__); for (auto j : m.vars()) { @@ -621,7 +561,8 @@ bool basics::basic_lemma_for_mon_neutral_monic_to_factor_model_based(const monic lemma |= ineq(term(u, rational(val(u) == -val(mon_var) ? 1 : -1), mon_var), llc::NE, 0); lemma |= ineq(v, llc::EQ, 1); lemma |= ineq(v, llc::EQ, -1); - lemma &= rm; // NSB review: is this dependency required? + lemma &= rm; // NSB review: is this dependency required? - it does because it explains how monomial is equivalent + // to the rooted monomial lemma &= f; return true; @@ -637,24 +578,11 @@ void basics::basic_lemma_for_mon_neutral_model_based(const monic& rm, const fact basic_lemma_for_mon_neutral_from_factors_to_monic_model_based(rm, f); } } - -/** - - m := f1*f2*.. - - f_i are factors of m - - at most one variable among f_i evaluates to something else than -1, +1. - - m = sign * f_i - - sign = sign of f_1 * .. * f_{i-1} * f_{i+1} ... = +/- 1 - - lemma: - /\_{j != i} f_j = val(f_j) => m = sign * f_i - or - /\ f_j = val(f_j) => m = sign if all factors evaluate to +/- 1 - -*/ -bool basics::basic_lemma_for_mon_neutral_from_factors_to_monic_model_based(const monic& m, const factorization& f) { - rational sign(1); - SASSERT(m.rsign() == canonize_sign(f)); - TRACE("nla_solver_bl", tout << pp_mon_with_vars(_(), m) <<"\nf = " << c().pp(f) << "sign = " << sign << '\n';); - lpvar not_one = null_lpvar; +template +bool basics::can_create_lemma_for_mon_neutral_from_factors_to_monic_model_based(const monic& m, const T& f, lpvar ¬_one, rational& sign) { + sign = rational(1); + // TRACE("nla_solver_bl", tout << pp_mon_with_vars(_(), m) <<"\nf = " << c().pp(f) << "sign = " << sign << '\n';); + not_one = null_lpvar; for (auto j : f) { TRACE("nla_solver_bl", tout << "j = "; c().print_factor_with_vars(j, tout);); auto v = val(j); @@ -685,6 +613,25 @@ bool basics::basic_lemma_for_mon_neutral_from_factors_to_monic_model_based(const return false; } + return true; +} + +/** + - m := f1*f2*.. + - f_i are factors of m + - at most one variable among f_i evaluates to something else than -1, +1. + - m = sign * f_i + - sign = sign of f_1 * .. * f_{i-1} * f_{i+1} ... = +/- 1 + - lemma: + /\_{j != i} f_j = val(f_j) => m = sign * f_i + or + /\ f_j = val(f_j) => m = sign if all factors evaluate to +/- 1 + +*/ +bool basics::basic_lemma_for_mon_neutral_from_factors_to_monic_model_based(const monic& m, const factorization& f) { + lpvar not_one; rational sign; + if (!can_create_lemma_for_mon_neutral_from_factors_to_monic_model_based(m, f, not_one, sign)) + return false; TRACE("nla_solver_bl", tout << "not_one = " << not_one << "\n";); new_lemma lemma(c(), __FUNCTION__); diff --git a/src/math/lp/nla_basics_lemmas.h b/src/math/lp/nla_basics_lemmas.h index 7a18fa0ed..58fb0e92f 100644 --- a/src/math/lp/nla_basics_lemmas.h +++ b/src/math/lp/nla_basics_lemmas.h @@ -48,6 +48,10 @@ struct basics: common { // bool basic_lemma_for_mon_neutral_monic_to_factor_model_based_fm(const monic& m); bool basic_lemma_for_mon_neutral_monic_to_factor_derived(const monic& rm, const factorization& f); + // use the fact + // 1 * 1 ... * 1 * x * 1 ... * 1 = x + template + bool can_create_lemma_for_mon_neutral_from_factors_to_monic_model_based(const monic& rm, const T&, lpvar&, rational&); // use the fact // 1 * 1 ... * 1 * x * 1 ... * 1 = x bool basic_lemma_for_mon_neutral_from_factors_to_monic_model_based(const monic& rm, const factorization& f); @@ -83,8 +87,6 @@ struct basics: common { void negate_strict_sign(new_lemma& lemma, lpvar j); // x != 0 or y = 0 => |xy| >= |y| void proportion_lemma_model_based(const monic& rm, const factorization& factorization); - // x != 0 or y = 0 => |xy| >= |y| - bool proportion_lemma_derived(const monic& rm, const factorization& factorization); // if there are no zero factors then |m| >= |m[factor_index]| void generate_pl_on_mon(const monic& m, unsigned factor_index); diff --git a/src/math/lp/nla_common.h b/src/math/lp/nla_common.h index c4ad649a7..f2e59f975 100644 --- a/src/math/lp/nla_common.h +++ b/src/math/lp/nla_common.h @@ -49,6 +49,9 @@ struct common { rational var_val(monic const& m) const; // value obtained from variable representing monomial rational mul_val(monic const& m) const; // value obtained from multiplying variables of monomial template lpvar var(T const& t) const; + // this needed in can_create_lemma_for_mon_neutral_from_factors_to_monic_model_based when iterating + // over a monic + lpvar var(lpvar j) const { return j; } bool done() const; template bool canonize_sign(const T&) const; diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index 6df7af584..11652dd26 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -1476,21 +1476,16 @@ lbool core::check(vector& l_vec) { patch_monomials_with_real_vars(); if (m_to_refine.is_empty()) { return l_true; } init_search(); - + set_use_nra_model(false); - - if (need_to_call_algebraic_methods() && m_horner.horner_lemmas()) - goto finish_up; - - if (!done()) { - clear_and_resize_active_var_set(); // NSB code review: why is this independent of whether Grobner is run? - if (m_nla_settings.run_grobner()) { + if (need_to_call_algebraic_methods()) { + if (!m_horner.horner_lemmas() && m_nla_settings.run_grobner() && !done()) { + clear_and_resize_active_var_set(); find_nl_cluster(); - run_grobner(); + run_grobner(); } } - TRACE("nla_solver_details", print_terms(tout); tout << m_lar_solver.constraints();); if (!done()) m_basics.basic_lemma(true); @@ -1511,6 +1506,7 @@ lbool core::check(vector& l_vec) { m_tangents.tangent_lemma(); } + if (!m_reslim.inc()) return l_undef; diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h index c70f32fe6..6dbf9e757 100644 --- a/src/math/lp/nla_core.h +++ b/src/math/lp/nla_core.h @@ -404,7 +404,6 @@ public: bool rm_check(const monic&) const; std::unordered_map get_rm_by_arity(); - // NSB code review: these could be methods on new_lemma void add_abs_bound(new_lemma& lemma, lpvar v, llc cmp); void add_abs_bound(new_lemma& lemma, lpvar v, llc cmp, rational const& bound); void negate_relation(new_lemma& lemma, unsigned j, const rational& a); diff --git a/src/math/lp/nla_solver.cpp b/src/math/lp/nla_solver.cpp index 3f34fbdf1..21c092efb 100644 --- a/src/math/lp/nla_solver.cpp +++ b/src/math/lp/nla_solver.cpp @@ -28,7 +28,6 @@ bool solver::is_monic_var(lpvar v) const { bool solver::need_check() { return true; } - lbool solver::check(vector& l) { return m_core->check(l); } diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index b8a36fd28..0d7623615 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -2158,6 +2158,7 @@ public: } lbool check_nla_continue() { + m_a1 = nullptr; m_a2 = nullptr; lbool r = m_nla->check(m_nla_lemma_vector); if (use_nra_model()) m_stats.m_nra_calls ++;