From 179c9c2da28e8e64d0711d588f40c4ceceb39a7f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 10 May 2020 18:31:57 -0700 Subject: [PATCH] consolidate methods that add lemma specific information to under "new_lemma" --- src/math/lp/nla_basics_lemmas.cpp | 214 ++++++++------------- src/math/lp/nla_basics_lemmas.h | 6 +- src/math/lp/nla_common.cpp | 53 ------ src/math/lp/nla_common.h | 24 --- src/math/lp/nla_core.cpp | 276 +++++++++++----------------- src/math/lp/nla_core.h | 85 +++------ src/math/lp/nla_intervals.cpp | 2 +- src/math/lp/nla_monotone_lemmas.cpp | 10 +- src/math/lp/nla_order_lemmas.cpp | 76 ++++---- src/math/lp/nla_tangent_lemmas.cpp | 83 ++++----- src/math/lp/nla_tangent_lemmas.h | 1 - src/test/lp/nla_solver_test.cpp | 44 ++--- 12 files changed, 314 insertions(+), 560 deletions(-) diff --git a/src/math/lp/nla_basics_lemmas.cpp b/src/math/lp/nla_basics_lemmas.cpp index 673839d42..868f96526 100644 --- a/src/math/lp/nla_basics_lemmas.cpp +++ b/src/math/lp/nla_basics_lemmas.cpp @@ -85,7 +85,7 @@ void basics::basic_sign_lemma_model_based_one_mon(const monic& m, int product_si } else { new_lemma lemma(c(), __FUNCTION__); for (lpvar j: m.vars()) { - negate_strict_sign(j); + negate_strict_sign(lemma, j); } lemma |= ineq(m.var(), product_sign == 1? llc::GT : llc::LT, 0); } @@ -155,8 +155,8 @@ void basics::generate_sign_lemma(const monic& m, const monic& n, const rational& tout << "n = " << pp_mon_with_vars(_(), n); ); lemma |= ineq(term(m.var(), -sign, n.var()), llc::EQ, 0); - explain(m); - explain(n); + lemma &= m; + lemma &= n; } // try to find a variable j such that val(j) = 0 // and the bounds on j contain 0 as an inner point @@ -187,31 +187,32 @@ void basics::generate_strict_case_zero_lemma(const monic& m, unsigned zero_j, in lemma |= ineq(zero_j, sign_of_zj == 1? llc::GT : llc::LT, 0); for (unsigned j : m.vars()) { if (j != zero_j) { - negate_strict_sign(j); + negate_strict_sign(lemma, j); } } - negate_strict_sign(m.var()); + negate_strict_sign(lemma, m.var()); } void basics::add_fixed_zero_lemma(const monic& m, lpvar j) { new_lemma lemma(c(), "fixed zero"); - c().explain_fixed_var(j); + lemma.explain_fixed(j); lemma |= ineq(m.var(), llc::EQ, 0); } -void basics::negate_strict_sign(lpvar j) { +void basics::negate_strict_sign(new_lemma& lemma, lpvar j) { TRACE("nla_solver_details", tout << pp_var(c(), j) << "\n";); if (!val(j).is_zero()) { int sign = nla::rat_sign(val(j)); - c().mk_ineq(j, (sign == 1? llc::LE : llc::GE)); - } else { // val(j).is_zero() + lemma |= ineq(j, (sign == 1? llc::LE : llc::GE), 0); + } + else { // val(j).is_zero() if (c().has_lower_bound(j) && c().get_lower_bound(j) >= rational(0)) { - c().explain_existing_lower_bound(j); - c().mk_ineq(j, llc::GT); + c().explain_existing_lower_bound(lemma, j); + lemma |= ineq(j, llc::GT, 0); } else { SASSERT(c().has_upper_bound(j) && c().get_upper_bound(j) <= rational(0)); - c().explain_existing_upper_bound(j); - c().mk_ineq(j, llc::LT); + c().explain_existing_upper_bound(lemma, j); + lemma |= ineq(j, llc::LT, 0); } } } @@ -219,21 +220,24 @@ void basics::negate_strict_sign(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 TRACE("nla_solver", c().trace_print_monic_and_factorization(rm, f, tout);); new_lemma lemma(c(), "xy = 0 -> x = 0 or y = 0"); - c().explain_fixed_var(var(rm)); + lemma.explain_fixed(var(rm)); std::unordered_set processed; for (auto j : f) { if (try_insert(var(j), processed)) lemma |= ineq(var(j), llc::EQ, 0); } - explain(rm); + lemma &= rm; + lemma &= f; return true; #endif } + // use basic multiplication properties to create a lemma bool basics::basic_lemma(bool derived) { if (basic_sign_lemma(derived)) @@ -266,48 +270,44 @@ bool basics::basic_lemma_for_mon_derived(const monic& rm) { if (c().var_is_fixed_to_zero(var(rm))) { for (auto factorization : factorization_factory_imp(rm, c())) { if (factorization.is_empty()) - continue; - if (basic_lemma_for_mon_zero(rm, factorization) || - basic_lemma_for_mon_neutral_derived(rm, factorization)) { - explain(factorization); + continue; + if (basic_lemma_for_mon_zero(rm, factorization)) + return true; + if (basic_lemma_for_mon_neutral_derived(rm, factorization)) return true; - } } - } else { + } + else { for (auto factorization : factorization_factory_imp(rm, c())) { if (factorization.is_empty()) continue; - if (basic_lemma_for_mon_non_zero_derived(rm, factorization) || - basic_lemma_for_mon_neutral_derived(rm, factorization) || - proportion_lemma_derived(rm, factorization)) { - explain(factorization); + if (basic_lemma_for_mon_non_zero_derived(rm, factorization)) + return true; + if (basic_lemma_for_mon_neutral_derived(rm, factorization)) + return true; + if (proportion_lemma_derived(rm, factorization)) return true; - } } } return false; } + // x = 0 or y = 0 -> xy = 0 bool basics::basic_lemma_for_mon_non_zero_derived(const monic& rm, const factorization& f) { TRACE("nla_solver", c().trace_print_monic_and_factorization(rm, f, tout);); if (!c().var_is_separated_from_zero(var(rm))) return false; - lpvar zero_j = null_lpvar; - for (auto j : f) { - if (c().var_is_fixed_to_zero(var(j))) { - zero_j = var(j); - break; - } + for (auto fc : f) { + if (!c().var_is_fixed_to_zero(var(fc))) + continue; + new_lemma lemma(c(), "x = 0 or y = 0 -> xy = 0"); + lemma.explain_fixed(var(fc)); + c().explain_var_separated_from_zero(lemma, var(rm)); + lemma &= rm; + lemma &= f; + return true; } - - if (zero_j == null_lpvar) { - return false; - } - new_lemma lemma(c(), "x = 0 or y = 0 -> xy = 0"); - c().explain_fixed_var(zero_j); - c().explain_var_separated_from_zero(var(rm)); - explain(rm); - return true; + return false; } // use the fact that @@ -315,7 +315,7 @@ bool basics::basic_lemma_for_mon_non_zero_derived(const monic& rm, const factori // it holds for integers, and for reals for a pair of factors // |x*a| = |x| & x != 0 -> |a| = 1 -bool basics::basic_lemma_for_mon_neutral_monic_to_factor_derived(const monic& rm, const factorization& f) { +bool basics::basic_lemma_for_mon_neutral_derived(const monic& rm, const factorization& f) { TRACE("nla_solver", c().trace_print_monic_and_factorization(rm, f, tout);); lpvar mon_var = c().emons()[rm.var()].var(); @@ -350,26 +350,22 @@ bool basics::basic_lemma_for_mon_neutral_monic_to_factor_derived(const monic& rm new_lemma lemma(c(), "|xa| = |x| & x != 0 -> |a| = 1"); // mon_var = 0 if (mon_var_is_sep_from_zero) - c().explain_var_separated_from_zero(mon_var); + c().explain_var_separated_from_zero(lemma, mon_var); else - c().explain_var_separated_from_zero(jl); - - c().explain_equiv_vars(mon_var, jl); + c().explain_var_separated_from_zero(lemma, jl); + + lemma.explain_equiv(mon_var, jl); // not_one_j = 1 lemma |= ineq(not_one_j, llc::EQ, 1); // not_one_j = -1 lemma |= ineq(not_one_j, llc::EQ, -1); - explain(rm); + lemma &= rm; + lemma &= f; return true; } -bool basics::basic_lemma_for_mon_neutral_derived(const monic& rm, const factorization& factorization) { - return - basic_lemma_for_mon_neutral_monic_to_factor_derived(rm, factorization); -} - // x != 0 or y = 0 => |xy| >= |y| void basics::proportion_lemma_model_based(const monic& rm, const factorization& factorization) { if (factorization_has_real(factorization)) // todo: handle the situaiton when all factors are greater than 1, @@ -392,6 +388,8 @@ void basics::proportion_lemma_model_based(const monic& rm, const factorization& bool basics::proportion_lemma_derived(const monic& rm, const factorization& factorization) { // NSB review: why return false? return false; + if (factorization_has_real(factorization)) + return false; rational rmv = abs(var_val(rm)); if (rmv.is_zero()) { SASSERT(c().has_zero_factor(factorization)); @@ -429,13 +427,12 @@ NSB review: */ void basics::generate_pl_on_mon(const monic& m, unsigned factor_index) { - if (mon_has_real(m)) - return; + SASSERT(!mon_has_real(m)); new_lemma lemma(c(), "generate_pl_on_mon"); unsigned mon_var = m.var(); rational mv = val(mon_var); rational sm = rational(nla::rat_sign(mv)); - c().mk_ineq(sm, mon_var, llc::LT); + 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) { @@ -448,6 +445,7 @@ void basics::generate_pl_on_mon(const monic& m, unsigned factor_index) { lemma |= ineq(term(sm, mon_var, -sj, j), llc::GE, 0); } } + lemma &= m; } /** @@ -459,8 +457,7 @@ void basics::generate_pl_on_mon(const monic& m, unsigned factor_index) { sign_m*m < 0 or f_i = 0 or \/_{j != i} sign_m*m >= sign_j*f_j */ void basics::generate_pl(const monic& m, const factorization& fc, int factor_index) { - if (factorization_has_real(fc)) - return; + SASSERT(!factorization_has_real(fc)); TRACE("nla_solver", tout << "factor_index = " << factor_index << ", m = " << pp_mon(c(), m); tout << ", fc = " << c().pp(fc); @@ -487,8 +484,8 @@ void basics::generate_pl(const monic& m, const factorization& fc, int factor_ind lemma |= ineq(term(sm, mon_var, -sj, j), llc::GE, 0); } } - explain(fc); - explain(m); + lemma &= fc; + lemma &= m; } bool basics::is_separated_from_zero(const factorization& f) const { @@ -532,10 +529,10 @@ void basics::basic_lemma_for_mon_zero_model_based(const monic& rm, const factori } else { lemma |= ineq(var(rm), llc::NE, 0); for (auto j : f) { - c().explain_separation_from_zero(var(j)); + c().explain_separation_from_zero(lemma, var(j)); } } - explain(f); + lemma &= f; } void basics::basic_lemma_for_mon_model_based(const monic& rm) { @@ -558,51 +555,6 @@ void basics::basic_lemma_for_mon_model_based(const monic& rm) { } } -// use the fact that -// |xabc| = |x| and x != 0 -> |a| = |b| = |c| = 1 -bool basics::basic_lemma_for_mon_neutral_monic_to_factor_model_based_fm(const monic& m) { - TRACE("nla_solver_bl", c().print_monic(m, tout);); - - lpvar mon_var = m.var(); - const auto mv = var_val(m); - const auto abs_mv = abs(mv); - if (abs_mv == rational::zero()) { - return false; - } - lpvar jl = null_lpvar, not_one_j = null_lpvar; - bool all_int = true; - for (auto j : m.vars()) { - all_int &= c().var_is_int(j); - if (jl == null_lpvar && abs(val(j)) == abs_mv) - jl = j; - else if (jl == j) - return false; - else if (abs(val(j)) != rational(1)) - not_one_j = j; - } - if (jl == null_lpvar || not_one_j == null_lpvar) - return false; - - if (!all_int && m.size() > 2) - return false; - - new_lemma lemma(c(), __FUNCTION__); - // mon_var = 0 - lemma |= ineq(mon_var, llc::EQ, 0); - - // negate abs(jl) == abs() - if (val(jl) == - val(mon_var)) - lemma |= ineq(term(jl, mon_var), llc::NE, 0); - else // jl == mon_var - lemma |= ineq(term(jl, -rational(1), mon_var), llc::NE, 0); - - // not_one_j = 1 - lemma |= ineq(not_one_j, llc::EQ, 1); - - // not_one_j = -1 - lemma |= ineq(not_one_j, llc::EQ, -1); - return true; -} /** m = f1 * f2 * .. * fn @@ -615,6 +567,10 @@ bool basics::basic_lemma_for_mon_neutral_monic_to_factor_model_based_fm(const mo 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); @@ -689,26 +645,23 @@ bool basics::basic_lemma_for_mon_neutral_monic_to_factor_model_based(const monic // mon_var = 0 lemma |= ineq(mon_var, llc::EQ, 0); - // negate abs(jl) == abs() - if (val(jl) == - val(mon_var)) - lemma |= ineq(term(jl, mon_var), llc::NE, 0); - else // jl == mon_var - lemma |= ineq(term(jl, -rational(1), mon_var), llc::NE, 0); + // negate abs(jl) == abs() + lemma |= ineq(term(jl, rational(val(jl) == -val(mon_var) ? 1 : -1), mon_var), llc::NE, 0); // not_one_j = 1 lemma |= ineq(not_one_j, llc::EQ, 1); // not_one_j = -1 lemma |= ineq(not_one_j, llc::EQ, -1); - explain(rm); - explain(f); + lemma &= rm; + lemma &= f; return true; } void basics::basic_lemma_for_mon_neutral_model_based(const monic& rm, const factorization& f) { if (f.is_mon()) { - basic_lemma_for_mon_neutral_monic_to_factor_model_based_fm(f.mon()); + basic_lemma_for_mon_neutral_monic_to_factor_model_based(rm, f); basic_lemma_for_mon_neutral_from_factors_to_monic_model_based_fm(f.mon()); } else { @@ -779,35 +732,24 @@ bool basics::basic_lemma_for_mon_neutral_from_factors_to_monic_model_based(const lemma |= ineq(m.var(), llc::EQ, sign); else lemma |= ineq(term(m.var(), -sign, not_one), llc::EQ, 0); - explain(m); - explain(f); + lemma &= m; + lemma &= f; TRACE("nla_solver", tout << "m = " << pp_mon_with_vars(c(), m);); return true; } - -void basics::basic_lemma_for_mon_non_zero_model_based_mf(const factorization& f) { - TRACE("nla_solver_bl", tout << c().pp(f);); - for (auto j : f) { - if (val(j).is_zero()) { - lpvar zero_j = var(j); - new_lemma lemma(c(), "x = 0 => x*... = 0"); - lemma |= ineq(zero_j, llc::NE, 0); - lemma |= ineq(f.mon().var(), llc::EQ, 0); - return; - } - } -} - // x = 0 or y = 0 -> xy = 0 void basics::basic_lemma_for_mon_non_zero_model_based(const monic& rm, const factorization& f) { TRACE("nla_solver_bl", c().trace_print_monic_and_factorization(rm, f, tout);); -// NSB code review: -// the two branches are the same - if (f.is_mon()) - basic_lemma_for_mon_non_zero_model_based_mf(f); - else - basic_lemma_for_mon_non_zero_model_based_mf(f); + for (auto j : f) { + if (val(j).is_zero()) { + new_lemma lemma(c(), "x = 0 => x*... = 0"); + lemma |= ineq(var(j), llc::NE, 0); + lemma |= ineq(f.mon().var(), llc::EQ, 0); + lemma &= f; + return; + } + } } diff --git a/src/math/lp/nla_basics_lemmas.h b/src/math/lp/nla_basics_lemmas.h index 9baa4336c..d4ff23ef4 100644 --- a/src/math/lp/nla_basics_lemmas.h +++ b/src/math/lp/nla_basics_lemmas.h @@ -14,6 +14,7 @@ namespace nla { class core; +class new_lemma; struct basics: common { basics(core *core); bool basic_sign_lemma_on_two_monics(const monic& m, const monic& n); @@ -36,7 +37,6 @@ struct basics: common { // x = 0 or y = 0 -> xy = 0 void basic_lemma_for_mon_non_zero_model_based_rm(const monic& rm, const factorization& f); - void basic_lemma_for_mon_non_zero_model_based_mf(const factorization& f); // x = 0 or y = 0 -> xy = 0 bool basic_lemma_for_mon_non_zero_derived(const monic& rm, const factorization& f); @@ -45,7 +45,7 @@ struct basics: common { bool basic_lemma_for_mon_neutral_monic_to_factor_model_based(const monic& rm, const factorization& f); // use the fact that // |xabc| = |x| and x != 0 -> |a| = |b| = |c| = 1 - bool basic_lemma_for_mon_neutral_monic_to_factor_model_based_fm(const monic& m); + // 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 @@ -80,7 +80,7 @@ struct basics: common { void generate_strict_case_zero_lemma(const monic& m, unsigned zero_j, int sign_of_zj); void add_fixed_zero_lemma(const monic& m, lpvar j); - void negate_strict_sign(lpvar j); + 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| diff --git a/src/math/lp/nla_common.cpp b/src/math/lp/nla_common.cpp index 5630f09c1..8f635f391 100644 --- a/src/math/lp/nla_common.cpp +++ b/src/math/lp/nla_common.cpp @@ -12,14 +12,6 @@ namespace nla { bool common::done() const { return c().done(); } -template void common::explain(const T& t) { - c().explain(t, c().current_expl()); -} -template void common::explain(const monic& t); -template void common::explain(const factor& t); -template void common::explain(const factorization& t); - -void common::explain(lpvar j) { c().explain(j, c().current_expl()); } template rational common::val(T const& t) const { return c().val(t); } template rational common::val(factor const& t) const; @@ -39,52 +31,7 @@ template bool common::canonize_sign(const factor&) const; template bool common::canonize_sign(const lpvar&) const; template bool common::canonize_sign(const factorization&) const; -void common::mk_ineq(lp::lar_term& t, llc cmp, const rational& rs){ - c().mk_ineq(t, cmp, rs); -} -void common::mk_ineq(const rational& a, lpvar j, const rational& b, lpvar k, llc cmp, const rational& rs){ - c().mk_ineq(a, j, b, j, cmp, rs); -} -void common::mk_ineq(lpvar j, const rational& b, lpvar k, llc cmp, const rational& rs){ - c().mk_ineq(j, b, k, cmp, rs); -} - -void common::mk_ineq(lpvar j, const rational& b, lpvar k, llc cmp){ - c().mk_ineq(j, b, k, cmp); -} - -void common::mk_ineq(const rational& a, lpvar j, const rational& b, lpvar k, llc cmp) { - c().mk_ineq(a, j, b, k, cmp); -} - -void common::mk_ineq(bool a, lpvar j, bool b, lpvar k, llc cmp) { - c().mk_ineq(sign_to_rat(a), j, sign_to_rat(b), k, cmp); -} - -void common::mk_ineq(const rational& a ,lpvar j, lpvar k, llc cmp, const rational& rs) { - c().mk_ineq(a, j, k, cmp, rs); -} - -void common::mk_ineq(lpvar j, lpvar k, llc cmp, const rational& rs) { - c().mk_ineq(j, k, cmp, rs);} - -void common::mk_ineq(lpvar j, llc cmp, const rational& rs){ - c().mk_ineq(j, cmp, rs);} - -void common::mk_ineq(const rational& a, lpvar j, llc cmp, const rational& rs) { - c().mk_ineq(a, j, cmp, rs); -} -void common::mk_ineq(const rational& a, lpvar j, llc cmp){ - c().mk_ineq(a, j, cmp); -} - -void common::mk_ineq(lpvar j, llc cmp){ - c().mk_ineq(j, cmp); -} -std::ostream& common::print_lemma(std::ostream& out) const { - return c().print_lemma(out); -} template std::ostream& common::print_product(const T & m, std::ostream& out) const { return c().print_product(m, out); diff --git a/src/math/lp/nla_common.h b/src/math/lp/nla_common.h index c202dc427..c4ad649a7 100644 --- a/src/math/lp/nla_common.h +++ b/src/math/lp/nla_common.h @@ -50,31 +50,7 @@ struct common { rational mul_val(monic const& m) const; // value obtained from multiplying variables of monomial template lpvar var(T const& t) const; bool done() const; - template void explain(const T&); - void explain(lpvar); template bool canonize_sign(const T&) const; - void mk_ineq(lp::lar_term& t, llc cmp, const rational& rs); - void mk_ineq(const rational& a, lpvar j, const rational& b, lpvar k, llc cmp, const rational& rs); - - void mk_ineq(lpvar j, const rational& b, lpvar k, llc cmp, const rational& rs); - - void mk_ineq(lpvar j, const rational& b, lpvar k, llc cmp); - - void mk_ineq(const rational& a, lpvar j, const rational& b, lpvar k, llc cmp); - void mk_ineq(bool a, lpvar j, bool b, lpvar k, llc cmp); - - void mk_ineq(const rational& a ,lpvar j, lpvar k, llc cmp, const rational& rs); - - void mk_ineq(lpvar j, lpvar k, llc cmp, const rational& rs); - - void mk_ineq(lpvar j, llc cmp, const rational& rs); - - void mk_ineq(const rational& a, lpvar j, llc cmp, const rational& rs); - void mk_ineq(const rational& a, lpvar j, llc cmp); - - void mk_ineq(lpvar j, llc cmp); - - std::ostream& print_lemma(std::ostream&) const; template std::ostream& print_product(const T & m, std::ostream& out) const; diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index 66fac9195..e2f474526 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -18,6 +18,8 @@ Author: #include "math/dd/pdd_eval.h" namespace nla { +typedef lp::lar_term term; + core::core(lp::lar_solver& s, reslimit & lim) : m_evars(), m_lar_solver(s), @@ -160,22 +162,6 @@ bool core::check_monic(const monic& m) const { return ret; } -void core::explain(const monic& m, lp::explanation& exp) const { - for (lpvar j : m.vars()) - explain(j, exp); -} - -void core::explain(const factor& f, lp::explanation& exp) const { - if (f.type() == factor_type::VAR) { - explain(f.var(), exp); - } else { - explain(m_emons[f.var()], exp); - } -} - -void core::explain(lpvar j, lp::explanation& exp) const { - m_evars.explain(j, exp); -} template std::ostream& core::print_product(const T & m, std::ostream& out) const { @@ -358,7 +344,7 @@ bool core::explain_coeff_upper_bound(const lp::lar_term::ival& p, rational& boun } // return true iff the negation of the ineq can be derived from the constraints -bool core::explain_ineq(const lp::lar_term& t, llc cmp, const rational& rs) { +bool core::explain_ineq(new_lemma& lemma, const lp::lar_term& t, llc cmp, const rational& rs) { // check that we have something like 0 < 0, which is always false and can be safely // removed from the lemma @@ -366,7 +352,7 @@ bool core::explain_ineq(const lp::lar_term& t, llc cmp, const rational& rs) { (cmp == llc::LT || cmp == llc::GT || cmp == llc::NE)) return true; lp::explanation exp; bool r; - switch(negate(cmp)) { + switch (negate(cmp)) { case llc::LE: r = explain_upper_bound(t, rs, exp); break; @@ -393,7 +379,7 @@ bool core::explain_ineq(const lp::lar_term& t, llc cmp, const rational& rs) { return false; } if (r) { - current_expl().add(exp); + lemma &= exp; return true; } @@ -419,59 +405,14 @@ bool core::explain_by_equiv(const lp::lar_term& t, lp::explanation& e) const { } -void core::mk_ineq(lp::lar_term& t, llc cmp, const rational& rs) { - TRACE("nla_solver_details", m_lar_solver.print_term_as_indices(t, tout << "t = ");); - if (!explain_ineq(t, cmp, rs)) { - current_lemma().push_back(ineq(cmp, t, rs)); - CTRACE("nla_solver", ineq_holds(ineq(cmp, t, rs)), print_ineq(ineq(cmp, t, rs), tout) << "\n";); - SASSERT(!ineq_holds(ineq(cmp, t, rs))); - } -} -void core::mk_ineq_no_expl_check(lp::lar_term& t, llc cmp, const rational& rs) { +void core::mk_ineq_no_expl_check(new_lemma& lemma, lp::lar_term& t, llc cmp, const rational& rs) { TRACE("nla_solver_details", m_lar_solver.print_term_as_indices(t, tout << "t = ");); - current_lemma().push_back(ineq(cmp, t, rs)); + lemma |= ineq(cmp, t, rs); CTRACE("nla_solver", ineq_holds(ineq(cmp, t, rs)), print_ineq(ineq(cmp, t, rs), tout) << "\n";); SASSERT(!ineq_holds(ineq(cmp, t, rs))); } -void core::mk_ineq(const rational& a, lpvar j, const rational& b, lpvar k, llc cmp, const rational& rs) { - lp::lar_term t; - t.add_monomial(a, j); - t.add_monomial(b, k); - mk_ineq(t, cmp, rs); -} - -void core::mk_ineq(lpvar j, const rational& b, lpvar k, llc cmp, const rational& rs) { - mk_ineq(rational(1), j, b, k, cmp, rs); -} - -void core::mk_ineq(lpvar j, const rational& b, lpvar k, llc cmp) { - mk_ineq(j, b, k, cmp, rational::zero()); -} - -void core::mk_ineq(const rational& a, lpvar j, const rational& b, lpvar k, llc cmp) { - mk_ineq(a, j, b, k, cmp, rational::zero()); -} - -void core::mk_ineq(const rational& a ,lpvar j, lpvar k, llc cmp, const rational& rs) { - mk_ineq(a, j, rational(1), k, cmp, rs); -} - -void core::mk_ineq(lpvar j, lpvar k, llc cmp, const rational& rs) { - mk_ineq(j, rational(1), k, cmp, rs); -} - -void core::mk_ineq(lpvar j, llc cmp, const rational& rs) { - mk_ineq(rational(1), j, cmp, rs); -} - -void core::mk_ineq(const rational& a, lpvar j, llc cmp, const rational& rs) { - lp::lar_term t; - t.add_monomial(a, j); - mk_ineq(t, cmp, rs); -} - llc apply_minus(llc cmp) { switch(cmp) { case llc::LE: return llc::GE; @@ -483,28 +424,15 @@ llc apply_minus(llc cmp) { return cmp; } -void core::mk_ineq(const rational& a, lpvar j, llc cmp) { - mk_ineq(a, j, cmp, rational::zero()); -} - - -void core::mk_ineq(lpvar j, llc cmp) { - mk_ineq(j, cmp, rational::zero()); -} // the monics should be equal by modulo sign but this is not so in the model -void core::fill_explanation_and_lemma_sign(const monic& a, const monic & b, rational const& sign) { +void core::fill_explanation_and_lemma_sign(new_lemma& lemma, const monic& a, const monic & b, rational const& sign) { SASSERT(sign == 1 || sign == -1); - explain(a, current_expl()); - explain(b, current_expl()); - TRACE("nla_solver", - tout << "used constraints: "; - for (auto &p : current_expl()) - m_lar_solver.constraints().display(tout, p.second); tout << "\n"; - ); - SASSERT(current_ineqs().size() == 0); - mk_ineq(rational(1), a.var(), -sign, b.var(), llc::EQ, rational::zero()); - TRACE("nla_solver", print_lemma(tout);); + lemma &= a; + lemma &= b; + TRACE("nla_solver", tout << "used constraints: " << lemma;); + SASSERT(lemma.num_ineqs() == 0); + lemma |= ineq(term(rational(1), a.var(), -sign, b.var()), llc::EQ, 0); } // Replaces each variable index by the root in the tree and flips the sign if the var comes with a minus. @@ -536,13 +464,6 @@ monic_coeff core::canonize_monic(monic const& m) const { return monic_coeff(vars, sign); } -lemma& core::current_lemma() { return m_lemma_vec->back(); } -const lemma& core::current_lemma() const { return m_lemma_vec->back(); } -vector& core::current_ineqs() { return current_lemma().ineqs(); } -lp::explanation& core::current_expl() { return current_lemma().expl(); } -const lp::explanation& core::current_expl() const { return current_lemma().expl(); } - - int core::vars_sign(const svector& v) { int sign = 1; for (lpvar j : v) { @@ -704,47 +625,40 @@ bool core::is_canonical_monic(lpvar j) const { } -void core::explain_existing_lower_bound(lpvar j) { +void core::explain_existing_lower_bound(new_lemma& lemma, lpvar j) { SASSERT(has_lower_bound(j)); - current_expl().add(m_lar_solver.get_column_lower_bound_witness(j)); + lemma &= m_lar_solver.get_column_lower_bound_witness(j); } -void core::explain_existing_upper_bound(lpvar j) { +void core::explain_existing_upper_bound(new_lemma& lemma, lpvar j) { SASSERT(has_upper_bound(j)); - current_expl().add(m_lar_solver.get_column_upper_bound_witness(j)); + lemma &= m_lar_solver.get_column_upper_bound_witness(j); } -void core::explain_separation_from_zero(lpvar j) { +void core::explain_separation_from_zero(new_lemma& lemma, lpvar j) { SASSERT(!val(j).is_zero()); if (val(j).is_pos()) - explain_existing_lower_bound(j); + explain_existing_lower_bound(lemma, j); else - explain_existing_upper_bound(j); + explain_existing_upper_bound(lemma, j); } void core::trace_print_monic_and_factorization(const monic& rm, const factorization& f, std::ostream& out) const { out << "rooted vars: "; - print_product(rm.rvars(), out); - out << "\n"; - - out << "mon: " << pp_mon(*this, rm.var()) << "\n"; + print_product(rm.rvars(), out) << "\n"; + out << "mon: " << pp_mon(*this, rm.var()) << "\n"; out << "value: " << var_val(rm) << "\n"; print_factorization(f, out << "fact: ") << "\n"; } -void core::explain_var_separated_from_zero(lpvar j) { +void core::explain_var_separated_from_zero(new_lemma& lemma, lpvar j) { SASSERT(var_is_separated_from_zero(j)); if (m_lar_solver.column_has_upper_bound(j) && (m_lar_solver.get_upper_bound(j)< lp::zero_of_type())) - current_expl().add(m_lar_solver.get_column_upper_bound_witness(j)); + lemma &= m_lar_solver.get_column_upper_bound_witness(j); else - current_expl().add(m_lar_solver.get_column_lower_bound_witness(j)); + lemma &= m_lar_solver.get_column_lower_bound_witness(j); } -void core::explain_fixed_var(lpvar j) { - SASSERT(var_is_fixed(j)); - current_expl().add(m_lar_solver.get_column_upper_bound_witness(j)); - current_expl().add(m_lar_solver.get_column_lower_bound_witness(j)); -} bool core::var_has_positive_lower_bound(lpvar j) const { return m_lar_solver.column_has_lower_bound(j) && m_lar_solver.get_lower_bound(j) > lp::zero_of_type(); @@ -765,26 +679,7 @@ bool core::vars_are_equiv(lpvar a, lpvar b) const { SASSERT(abs(val(a)) == abs(val(b))); return m_evars.vars_are_equiv(a, b); } - -void core::explain_equiv_vars(lpvar a, lpvar b) { - SASSERT(abs(val(a)) == abs(val(b))); - if (m_evars.vars_are_equiv(a, b)) { - explain(a, current_expl()); - explain(b, current_expl()); - } else { - explain_fixed_var(a); - explain_fixed_var(b); - } -} - -void core::explain(const factorization& f, lp::explanation& exp) { - SASSERT(!f.is_mon()); - for (const auto& fc : f) { - explain(fc, exp); - } -} - bool core::has_zero_factor(const factorization& factorization) const { for (factor f : factorization) { if (val(f).is_zero()) @@ -983,12 +878,12 @@ std::unordered_set core::collect_vars(const lemma& l) const { } }; - for (const auto& i : current_lemma().ineqs()) { + for (const auto& i : l.ineqs()) { for (const auto& p : i.term()) { insert_j(p.column()); } } - for (const auto& p : current_expl()) { + for (const auto& p : l.expl()) { const auto& c = m_lar_solver.constraints()[p.second]; for (const auto& r : c.coeffs()) { insert_j(r.second); @@ -1026,16 +921,12 @@ bool core::divide(const monic& bc, const factor& c, factor & b) const { return true; } -void core::negate_var_relation_strictly(lpvar a, lpvar b) { +void core::negate_var_relation_strictly(new_lemma& lemma, lpvar a, lpvar b) { SASSERT(val(a) != val(b)); - if (val(a) < val(b)) { - mk_ineq(a, -rational(1), b, llc::GT); - } else { - mk_ineq(a, -rational(1), b, llc::LT); - } + lemma |= ineq(term(a, -rational(1), b), val(a) < val(b) ? llc::GT : llc::LT, 0); } -void core::negate_factor_equality(const factor& c, +void core::negate_factor_equality(new_lemma& lemma, const factor& c, const factor& d) { if (c == d) return; @@ -1043,30 +934,22 @@ void core::negate_factor_equality(const factor& c, lpvar j = var(d); auto iv = val(i), jv = val(j); SASSERT(abs(iv) == abs(jv)); - if (iv == jv) { - mk_ineq(i, -rational(1), j, llc::NE); - } else { // iv == -jv - mk_ineq(i, j, llc::NE, rational::zero()); - } + lemma |= ineq(term(i, rational(iv == jv ? -1 : 1), j), llc::NE, 0); } -void core::negate_factor_relation(const rational& a_sign, const factor& a, const rational& b_sign, const factor& b) { +void core::negate_factor_relation(new_lemma& lemma, const rational& a_sign, const factor& a, const rational& b_sign, const factor& b) { rational a_fs = sign_to_rat(canonize_sign(a)); rational b_fs = sign_to_rat(canonize_sign(b)); llc cmp = a_sign*val(a) < b_sign*val(b)? llc::GE : llc::LE; - mk_ineq(a_fs*a_sign, var(a), - b_fs*b_sign, var(b), cmp); + lemma |= ineq(term(a_fs*a_sign, var(a), - b_fs*b_sign, var(b)), cmp, 0); } -std::ostream& core::print_lemma(std::ostream& out) const { - return print_specific_lemma(current_lemma(), out); -} - -std::ostream& core::print_specific_lemma(const lemma& l, std::ostream& out) const { +std::ostream& core::print_lemma(const lemma& l, std::ostream& out) const { static int n = 0; out << "lemma:" << ++n << " "; print_ineqs(l, out); print_explanation(l.expl(), out); - for (lpvar j : collect_vars(current_lemma())) { + for (lpvar j : collect_vars(l)) { print_var(j, out); } return out; @@ -1146,11 +1029,11 @@ bool core::rm_check(const monic& rm) const { */ -void core::add_abs_bound(lpvar v, llc cmp) { - add_abs_bound(v, cmp, val(v)); +void core::add_abs_bound(new_lemma& lemma, lpvar v, llc cmp) { + add_abs_bound(lemma, v, cmp, val(v)); } -void core::add_abs_bound(lpvar v, llc cmp, rational const& bound) { +void core::add_abs_bound(new_lemma& lemma, lpvar v, llc cmp, rational const& bound) { SASSERT(!val(v).is_zero()); lp::lar_term t; // t = abs(v) t.add_monomial(rrat_sign(val(v)), v); @@ -1158,7 +1041,7 @@ void core::add_abs_bound(lpvar v, llc cmp, rational const& bound) { switch (cmp) { case llc::GT: case llc::GE: // negate abs(v) >= 0 - mk_ineq(t, llc::LT, rational(0)); + lemma |= ineq(t, llc::LT, 0); break; case llc::LT: case llc::LE: @@ -1167,7 +1050,7 @@ void core::add_abs_bound(lpvar v, llc cmp, rational const& bound) { UNREACHABLE(); break; } - mk_ineq(t, cmp, abs(bound)); + lemma |= ineq(t, cmp, abs(bound)); } // NB - move this comment to monotonicity or appropriate. @@ -1234,11 +1117,11 @@ new_lemma::new_lemma(core& c, char const* name):name(name), c(c) { c.m_lemma_vec->push_back(lemma()); } -new_lemma& new_lemma::add(ineq const& ineq) { - if (!c.explain_ineq(ineq.term(), ineq.cmp(), ineq.rs())) { - c.current_lemma().push_back(ineq); +new_lemma& new_lemma::operator|=(ineq const& ineq) { + if (!c.explain_ineq(*this, ineq.term(), ineq.cmp(), ineq.rs())) { CTRACE("nla_solver", c.ineq_holds(ineq), c.print_ineq(ineq, tout) << "\n";); SASSERT(!c.ineq_holds(ineq)); + current().push_back(ineq); } return *this; } @@ -1248,12 +1131,65 @@ new_lemma::~new_lemma() { TRACE("nla_solver", tout << name << "\n" << *this; ); } -lemma& new_lemma::operator()() { - return c.current_lemma(); +lemma& new_lemma::current() const { + return c.m_lemma_vec->back(); } +new_lemma& new_lemma::operator&=(lp::explanation const& e) { + expl().add(e); + return *this; +} + +new_lemma& new_lemma::operator&=(const monic& m) { + for (lpvar j : m.vars()) + *this &= j; + return *this; +} + +new_lemma& new_lemma::operator&=(const factor& f) { + if (f.type() == factor_type::VAR) + *this &= f.var(); + else + *this &= c.m_emons[f.var()]; + return *this; +} + +new_lemma& new_lemma::operator&=(const factorization& f) { + if (f.is_mon()) + return *this; + for (const auto& fc : f) { + *this &= fc; + } + return *this; +} + +new_lemma& new_lemma::operator&=(lpvar j) { + c.m_evars.explain(j, expl()); + return *this; +} + +new_lemma& new_lemma::explain_fixed(lpvar j) { + SASSERT(c.var_is_fixed(j)); + *this &= c.m_lar_solver.get_column_upper_bound_witness(j); + *this &= c.m_lar_solver.get_column_lower_bound_witness(j); + return *this; +} + +new_lemma& new_lemma::explain_equiv(lpvar a, lpvar b) { + SASSERT(abs(c.val(a)) == abs(c.val(b))); + if (c.vars_are_equiv(a, b)) { + *this &= a; + *this &= b; + } else { + explain_fixed(a); + explain_fixed(b); + } + return *this; +} + + std::ostream& new_lemma::display(std::ostream & out) const { - auto const& lemma = c.current_lemma(); + auto const& lemma = current(); for (auto &p : lemma.expl()) { out << "(" << p.second << ") "; @@ -1277,15 +1213,11 @@ std::ostream& new_lemma::display(std::ostream & out) const { return out; } + -void core::negate_relation(unsigned j, const rational& a) { +void core::negate_relation(new_lemma& lemma, unsigned j, const rational& a) { SASSERT(val(j) != a); - if (val(j) < a) { - mk_ineq(j, llc::GE, a); - } - else { - mk_ineq(j, llc::LE, a); - } + lemma |= ineq(j, val(j) < a ? llc::GE : llc::LE, a); } bool core::conflict_found() const { @@ -1555,7 +1487,7 @@ lbool core::check(vector& l_vec) { bool core::no_lemmas_hold() const { for (auto & l : * m_lemma_vec) { if (lemma_holds(l)) { - TRACE("nla_solver", print_specific_lemma(l, tout);); + TRACE("nla_solver", print_lemma(l, tout);); return false; } } @@ -1703,7 +1635,7 @@ bool core::check_pdd_eq(const dd::solver::equation* e) { eval.get_interval(e->poly(), i_wd); std::function f = [this](const lp::explanation& e) { new_lemma lemma(*this, "pdd"); - current_expl().add(e); + lemma &= e; }; if (di.check_interval_for_conflict_on_zero(i_wd, e->dep(), f)) { lp_settings().stats().m_grobner_conflicts++; diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h index d39e2ea94..1f13dc18e 100644 --- a/src/math/lp/nla_core.h +++ b/src/math/lp/nla_core.h @@ -89,17 +89,25 @@ class core; class new_lemma { char const* name; core& c; + lemma& current() const; + lp::explanation& expl() { return current().expl(); } + public: new_lemma(core& c, char const* name); ~new_lemma(); - new_lemma& add(ineq const& ineq); - lemma& operator()(); + lemma& operator()() { return current(); } std::ostream& display(std::ostream& out) const; + new_lemma& operator&=(lp::explanation const& e); + new_lemma& operator&=(const monic& m); + new_lemma& operator&=(const factor& f); + new_lemma& operator&=(const factorization& f); + new_lemma& operator&=(lpvar j); + new_lemma& operator|=(ineq const& i); + new_lemma& explain_fixed(lpvar j); + new_lemma& explain_equiv(lpvar u, lpvar v); + unsigned num_ineqs() const { return current().ineqs().size(); } }; -inline new_lemma& operator|=(new_lemma& lemma, ineq const& i) { - return lemma.add(i); -} inline std::ostream& operator<<(std::ostream& out, new_lemma const& l) { return l.display(out); @@ -238,14 +246,11 @@ public: // return true iff the monic value is equal to the product of the values of the factors bool check_monic(const monic& m) const; - void explain(const monic& m, lp::explanation& exp) const; - void explain(const factor& f, lp::explanation& exp) const; - void explain(lpvar j, lp::explanation& exp) const; - void explain_existing_lower_bound(lpvar j); - void explain_existing_upper_bound(lpvar j); - void explain_separation_from_zero(lpvar j); - void explain_var_separated_from_zero(lpvar j); - void explain_fixed_var(lpvar j); + // NSB review: these should really be methods on new_lemma + void explain_existing_lower_bound(new_lemma& lemma, lpvar j); + void explain_existing_upper_bound(new_lemma& lemma, lpvar j); + void explain_separation_from_zero(new_lemma& lemma, lpvar j); + void explain_var_separated_from_zero(new_lemma& lemma, lpvar j); std::ostream & print_ineq(const ineq & in, std::ostream & out) const; @@ -274,13 +279,12 @@ public: void trace_print_monic_and_factorization(const monic& rm, const factorization& f, std::ostream& out) const; void print_monic_stats(const monic& m, std::ostream& out); void print_stats(std::ostream& out); - std::ostream& print_lemma(std::ostream& out) const; pp_var pp(lpvar j) const { return pp_var(*this, j); } pp_fac pp(factor const& f) const { return pp_fac(*this, f); } pp_factorization pp(factorization const& f) const { return pp_factorization(*this, f); } - std::ostream& print_specific_lemma(const lemma& l, std::ostream& out) const; + std::ostream& print_lemma(const lemma& l, std::ostream& out) const; void trace_print_ol(const monic& ac, @@ -291,22 +295,7 @@ public: std::ostream& out); - - void mk_ineq(lp::lar_term& t, llc cmp, const rational& rs); - void mk_ineq_no_expl_check(lp::lar_term& t, llc cmp, const rational& rs); - void mk_ineq(const rational& a, lpvar j, const rational& b, lpvar k, llc cmp, const rational& rs); - void mk_ineq(bool a, lpvar j, bool b, lpvar k, llc cmp, const rational& rs); - void mk_ineq(bool a, lpvar j, bool b, lpvar k, llc cmp); - void mk_ineq(lpvar j, const rational& b, lpvar k, llc cmp, const rational& rs); - void mk_ineq(lpvar j, const rational& b, lpvar k, llc cmp); - void mk_ineq(const rational& a, lpvar j, const rational& b, lpvar k, llc cmp); - void mk_ineq(const rational& a ,lpvar j, lpvar k, llc cmp, const rational& rs); - void mk_ineq(lpvar j, lpvar k, llc cmp, const rational& rs); - void mk_ineq(lpvar j, llc cmp, const rational& rs); - void mk_ineq(const rational& a, lpvar j, llc cmp, const rational& rs); - void mk_ineq(const rational& a, lpvar j, llc cmp); - void mk_ineq(lpvar j, llc cmp); - + void mk_ineq_no_expl_check(new_lemma& lemma, lp::lar_term& t, llc cmp, const rational& rs); void maybe_add_a_factor(lpvar i, const factor& c, @@ -316,18 +305,12 @@ public: llc apply_minus(llc cmp); - void fill_explanation_and_lemma_sign(const monic& a, const monic & b, rational const& sign); + void fill_explanation_and_lemma_sign(new_lemma& lemma, const monic& a, const monic & b, rational const& sign); svector reduce_monic_to_rooted(const svector & vars, rational & sign) const; monic_coeff canonize_monic(monic const& m) const; - lemma& current_lemma(); - const lemma& current_lemma() const; - vector& current_ineqs(); - lp::explanation& current_expl(); - const lp::explanation& current_expl() const; - int vars_sign(const svector& v); bool has_upper_bound(lpvar j) const; bool has_lower_bound(lpvar j) const; @@ -361,20 +344,12 @@ public: bool var_is_separated_from_zero(lpvar j) const; bool vars_are_equiv(lpvar a, lpvar b) const; - void explain_equiv_vars(lpvar a, lpvar b); - void explain(const factorization& f, lp::explanation& exp); + bool explain_ineq(new_lemma& lemma, const lp::lar_term& t, llc cmp, const rational& rs); bool explain_upper_bound(const lp::lar_term& t, const rational& rs, lp::explanation& e) const; - bool explain_lower_bound(const lp::lar_term& t, const rational& rs, lp::explanation& e) const; - bool explain_coeff_lower_bound(const lp::lar_term::ival& p, rational& bound, lp::explanation& e) const; - bool explain_coeff_upper_bound(const lp::lar_term::ival& p, rational& bound, lp::explanation& e) const; - - bool explain_ineq(const lp::lar_term& t, llc cmp, const rational& rs); - bool explain_by_equiv(const lp::lar_term& t, lp::explanation& e) const; - bool has_zero_factor(const factorization& factorization) const; template @@ -414,26 +389,24 @@ public: void init_to_refine(); bool divide(const monic& bc, const factor& c, factor & b) const; - - void negate_factor_equality(const factor& c, const factor& d); - - void negate_factor_relation(const rational& a_sign, const factor& a, const rational& b_sign, const factor& b); - - void negate_var_relation_strictly(lpvar a, lpvar b); std::unordered_set collect_vars(const lemma& l) const; bool rm_check(const monic&) const; std::unordered_map get_rm_by_arity(); - void add_abs_bound(lpvar v, llc cmp); - void add_abs_bound(lpvar v, llc cmp, rational const& bound); + // 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); + void negate_factor_equality(new_lemma& lemma, const factor& c, const factor& d); + void negate_factor_relation(new_lemma& lemma, const rational& a_sign, const factor& a, const rational& b_sign, const factor& b); + void negate_var_relation_strictly(new_lemma& lemma, lpvar a, lpvar b); bool find_bfc_to_refine_on_monic(const monic&, factorization & bf); bool find_bfc_to_refine(const monic* & m, factorization& bf); - void negate_relation(unsigned j, const rational& a); bool conflict_found() const; lbool inner_check(bool derived); diff --git a/src/math/lp/nla_intervals.cpp b/src/math/lp/nla_intervals.cpp index ae6d64afa..a25c8a30b 100644 --- a/src/math/lp/nla_intervals.cpp +++ b/src/math/lp/nla_intervals.cpp @@ -85,7 +85,7 @@ bool intervals::check_nex(const nex* n, u_dependency* initial_deps) { scoped_dep_interval i(get_dep_intervals()); std::function f = [this](const lp::explanation& e) { new_lemma lemma(*m_core, "check_nex"); - m_core->current_expl().add(e); + lemma &= e; }; if (!interval_of_expr(n, 1, i, f)) { // found a conflict during the interval calculation diff --git a/src/math/lp/nla_monotone_lemmas.cpp b/src/math/lp/nla_monotone_lemmas.cpp index 5d1fecb50..d4d4a19b3 100644 --- a/src/math/lp/nla_monotone_lemmas.cpp +++ b/src/math/lp/nla_monotone_lemmas.cpp @@ -40,11 +40,10 @@ void monotone::monotonicity_lemma_gt(const monic& m, const rational& prod_val) { tout << "m = "; c().print_monic_with_vars(m, tout);); new_lemma lemma(c(), __FUNCTION__); for (lpvar j : m.vars()) { - c().add_abs_bound(j, llc::GT); + c().add_abs_bound(lemma, j, llc::GT); } lpvar m_j = m.var(); - c().add_abs_bound(m_j, llc::LE, prod_val); - TRACE("nla_solver", print_lemma(tout);); + c().add_abs_bound(lemma, m_j, llc::LE, prod_val); } /** \brief enforce the inequality |m| >= product |m[i]| . @@ -56,11 +55,10 @@ void monotone::monotonicity_lemma_gt(const monic& m, const rational& prod_val) { void monotone::monotonicity_lemma_lt(const monic& m, const rational& prod_val) { new_lemma lemma(c(), __FUNCTION__); for (lpvar j : m.vars()) { - c().add_abs_bound(j, llc::LT); + c().add_abs_bound(lemma, j, llc::LT); } lpvar m_j = m.var(); - c().add_abs_bound(m_j, llc::GE, prod_val); - TRACE("nla_solver", print_lemma(tout);); + c().add_abs_bound(lemma, m_j, llc::GE, prod_val); } diff --git a/src/math/lp/nla_order_lemmas.cpp b/src/math/lp/nla_order_lemmas.cpp index d0a47db9c..4b44c8459 100644 --- a/src/math/lp/nla_order_lemmas.cpp +++ b/src/math/lp/nla_order_lemmas.cpp @@ -13,6 +13,8 @@ namespace nla { +typedef lp::lar_term term; + // The order lemma is // a > b && c > 0 => ac > bc void order::order_lemma() { @@ -82,9 +84,9 @@ void order::order_lemma_on_binomial_sign(const monic& xy, lpvar x, lpvar y, int SASSERT(!_().mon_has_zero(xy.vars())); int sy = rat_sign(val(y)); new_lemma lemma(c(), __FUNCTION__); - mk_ineq(y, sy == 1 ? llc::LE : llc::GE); // negate sy - mk_ineq(x, sy*sign == 1 ? llc::GT : llc::LT , val(x)); - mk_ineq(xy.var(), - val(x), y, sign == 1 ? llc::LE : llc::GE); + lemma |= ineq(y, sy == 1 ? llc::LE : llc::GE, 0); // negate sy + lemma |= ineq(x, sy*sign == 1 ? llc::GT : llc::LT , val(x)); + lemma |= ineq(term(xy.var(), - val(x), y), sign == 1 ? llc::LE : llc::GE, 0); } // We look for monics e = m.rvars()[k]*d and see if we can create an order lemma for m and e @@ -165,13 +167,13 @@ void order::generate_mon_ol(const monic& ac, SASSERT(ab_cmp != llc::GT || (var_val(ac) <= var_val(bd) && val(a)*c_sign > val(b)*d_sign)); new_lemma lemma(_(), __FUNCTION__); - mk_ineq(c_sign, c, llc::LE); - explain(c); // this explains c == +- d - mk_ineq(c_sign, a, -d_sign * b.rat_sign(), b.var(), negate(ab_cmp)); - mk_ineq(ac.var(), rational(-1), var(bd), ab_cmp); - explain(bd); - explain(b); - explain(d); + lemma |= ineq(term(c_sign, c), llc::LE, 0); + lemma &= c; // this explains c == +- d + lemma |= ineq(term(c_sign, a, -d_sign * b.rat_sign(), b.var()), negate(ab_cmp), 0); + lemma |= ineq(term(ac.var(), rational(-1), var(bd)), ab_cmp, 0); + lemma &= bd; + lemma &= b; + lemma &= d; } @@ -215,8 +217,8 @@ void order::order_lemma_on_factorization(const monic& m, const factorization& ab for (unsigned j = 0, k = 1; j < 2; j++, k--) { new_lemma lemma(_(), __FUNCTION__); order_lemma_on_ab(lemma, m, rsign, var(ab[k]), var(ab[j]), gt); - explain(ab); - explain(m); + lemma &= ab; + lemma &= m; } } for (unsigned j = 0, k = 1; j < 2; j++, k--) { @@ -230,14 +232,14 @@ bool order::order_lemma_on_ac_explore(const monic& rm, const factorization& ac, if (c.is_var()) { TRACE("nla_solver", tout << "var(c) = " << var(c);); for (monic const& bc : _().emons().get_use_list(c.var())) { - if (order_lemma_on_ac_and_bc(rm ,ac, k, bc)) { + if (order_lemma_on_ac_and_bc(rm, ac, k, bc)) { return true; } } } else { for (monic const& bc : _().emons().get_products_of(c.var())) { - if (order_lemma_on_ac_and_bc(rm , ac, k, bc)) { + if (order_lemma_on_ac_and_bc(rm, ac, k, bc)) { return true; } } @@ -249,7 +251,7 @@ void order::generate_ol_eq(const monic& ac, const factor& a, const factor& c, const monic& bc, - const factor& b) { + const factor& b) { new_lemma lemma(_(), __FUNCTION__); IF_VERBOSE(100, @@ -260,22 +262,21 @@ void order::generate_ol_eq(const monic& ac, << " b " << "*v" << var(b) << " " << val(b) << "\n" << " c " << "*v" << var(c) << " " << val(c) << "\n"); // ac == bc - mk_ineq(c.var(),llc::EQ); // c is not equal to zero - mk_ineq(ac.var(), -rational(1), bc.var(), llc::NE); - mk_ineq(canonize_sign(a), a.var(), !canonize_sign(b), b.var(), llc::EQ); - explain(ac); - explain(a); - explain(bc); - explain(b); - explain(c); - TRACE("nla_solver", _().print_lemma(tout);); + lemma |= ineq(c.var(), llc::EQ, 0); // c is not equal to zero + lemma |= ineq(term(ac.var(), -rational(1), bc.var()), llc::NE, 0); + lemma |= ineq(term(rational(canonize_sign(a)), a.var(), rational(!canonize_sign(b)), b.var()), llc::EQ, 0); + lemma &= ac; + lemma &= a; + lemma &= bc; + lemma &= b; + lemma &= c; } void order::generate_ol(const monic& ac, const factor& a, const factor& c, const monic& bc, - const factor& b) { + const factor& b) { new_lemma lemma(_(), __FUNCTION__); IF_VERBOSE(100, verbose_stream() << var_val(ac) << "(" << mul_val(ac) << "): " << ac @@ -284,15 +285,14 @@ void order::generate_ol(const monic& ac, << " b " << "*v" << var(b) << " " << val(b) << "\n" << " c " << "*v" << var(c) << " " << val(c) << "\n"); // fix the sign of c - _().negate_relation(c.var(), rational(0)); - _().negate_var_relation_strictly(ac.var(), bc.var()); - _().negate_var_relation_strictly(a.var(), b.var()); - explain(ac); - explain(a); - explain(bc); - explain(b); - explain(c); - TRACE("nla_solver", _().print_lemma(tout);); + lemma |= ineq(c.var(), val(c.var()).is_neg() ? llc::GE : llc::LE, 0); + _().negate_var_relation_strictly(lemma, ac.var(), bc.var()); + _().negate_var_relation_strictly(lemma, a.var(), b.var()); + lemma &= ac; + lemma &= a; + lemma &= bc; + lemma &= b; + lemma &= c; } // We have ac = a*c and bc = b*c. @@ -327,9 +327,9 @@ bool order::order_lemma_on_ac_and_bc_and_factors(const monic& ac, void order::order_lemma_on_ab_gt(new_lemma& lemma, const monic& m, const rational& sign, lpvar a, lpvar b) { SASSERT(sign * var_val(m) > val(a) * val(b)); // negate b == val(b) - mk_ineq(b, llc::NE, val(b)); + lemma |= ineq(b, llc::NE, val(b)); // ab <= val(b)a - mk_ineq(sign, m.var(), -val(b), a, llc::LE); + lemma |= ineq(term(sign, m.var(), -val(b), a), llc::LE, 0); } /* given: sign * m = ab @@ -340,9 +340,9 @@ void order::order_lemma_on_ab_lt(new_lemma& lemma, const monic& m, const rationa ", b = "; c().print_var(b, tout) << "\n";); SASSERT(sign * var_val(m) < val(a) * val(b)); // negate b == val(b) - mk_ineq(b, llc::NE, val(b)); + lemma |= ineq(b, llc::NE, val(b)); // ab >= val(b)a - mk_ineq(sign, m.var(), -val(b), a, llc::GE); + lemma |= ineq(term(sign, m.var(), -val(b), a), llc::GE, 0); } void order::order_lemma_on_ab(new_lemma& lemma, const monic& m, const rational& sign, lpvar a, lpvar b, bool gt) { diff --git a/src/math/lp/nla_tangent_lemmas.cpp b/src/math/lp/nla_tangent_lemmas.cpp index 2d6d1691d..42741a07e 100644 --- a/src/math/lp/nla_tangent_lemmas.cpp +++ b/src/math/lp/nla_tangent_lemmas.cpp @@ -11,7 +11,7 @@ namespace nla { -struct imp { +struct tangent_imp { point m_a; point m_b; point m_xy; @@ -26,33 +26,30 @@ struct imp { lpvar m_jx; lpvar m_jy; tangents& m_tang; - imp(point xy, + bool m_is_mon; + tangent_imp(point xy, const rational& v, lpvar j, // the monic variable const monic& m, - const factor& x, - const factor& y, + const factorization& f, tangents& tang) : m_xy(xy), m_correct_v(xy.x * xy.y), m_below(v < m_correct_v), m_v(v), m_j(tang.var(m)), m_m(m), - m_x(x), - m_y(y), - m_jx(tang.var(x)), - m_jy(tang.var(y)), - m_tang(tang) {} + m_x(f[0]), + m_y(f[1]), + m_jx(tang.var(m_x)), + m_jy(tang.var(m_y)), + m_tang(tang), + m_is_mon(f.is_mon()) { + SASSERT(f.size() == 2); + } core & c() { return m_tang.c(); } - void generate_explanations_of_tang_lemma(lp::explanation& exp) { - // here we repeat the same explanation for each lemma - c().explain(m_m, exp); - c().explain(m_x, exp); - c().explain(m_y, exp); - } void tangent_lemma_on_bf() { get_tang_points(); TRACE("nla_solver", tout << "tang domain = "; print_tangent_domain(tout) << std::endl;); @@ -61,11 +58,18 @@ struct imp { generate_tang_plane(m_b); } + void explain(new_lemma& lemma) { + if (!m_is_mon) { + lemma &= m_m; + lemma &= m_x; + lemma &= m_y; + } + } void generate_tang_plane(const point & pl) { new_lemma lemma(c(), "generate tangent plane"); - c().negate_relation(m_jx, m_x.rat_sign()*pl.x); - c().negate_relation(m_jy, m_y.rat_sign()*pl.y); + c().negate_relation(lemma, m_jx, m_x.rat_sign()*pl.x); + c().negate_relation(lemma, m_jy, m_y.rat_sign()*pl.y); #if Z3DEBUG SASSERT(c().val(m_x) == m_xy.x && c().val(m_y) == m_xy.y); int mult_sign = nla::rat_sign(pl.x - m_xy.x)*nla::rat_sign(pl.y - m_xy.y); @@ -79,20 +83,23 @@ struct imp { t.add_monomial(- m_y.rat_sign()*pl.x, m_jy); t.add_monomial(- m_x.rat_sign()*pl.y, m_jx); t.add_var(m_j); - c().mk_ineq(t, m_below? llc::GT : llc::LT, - pl.x*pl.y); + lemma |= ineq(t, m_below? llc::GT : llc::LT, - pl.x*pl.y); + explain(lemma); } void generate_two_tang_lines() { { new_lemma lemma(c(), "two tangent planes 1"); // Should be v = val(m_x)*val(m_y), and val(factor) = factor.rat_sign()*var(factor.var()) - c().mk_ineq(m_jx, llc::NE, c().val(m_jx)); - c().mk_ineq(m_j, - m_y.rat_sign() * m_xy.x, m_jy, llc::EQ); + lemma |= ineq(m_jx, llc::NE, c().val(m_jx)); + lemma |= ineq(lp::lar_term(m_j, - m_y.rat_sign() * m_xy.x, m_jy), llc::EQ, 0); + explain(lemma); } { new_lemma lemma(c(), "two tangent planes 2"); - c().mk_ineq(m_jy, llc::NE, c().val(m_jy)); - c().mk_ineq(m_j, - m_x.rat_sign() * m_xy.y, m_jx, llc::EQ); + lemma |= ineq(m_jy, llc::NE, c().val(m_jy)); + lemma |= ineq(lp::lar_term(m_j, - m_x.rat_sign() * m_xy.y, m_jx), llc::EQ, 0); + explain(lemma); } } // Get two planes tangent to surface z = xy, one at point a, and another at point b, creating a cut @@ -182,36 +189,16 @@ void tangents::tangent_lemma() { factorization bf(nullptr); const monic* m; if (c().find_bfc_to_refine(m, bf)) { - unsigned lemmas_size_was = c().m_lemma_vec->size(); unsigned j = m->var(); - imp i(point(val(bf[0]), val(bf[1])), - c().val(j), - j, - *m, - bf[0], - bf[1], - *this); + tangent_imp i(point(val(bf[0]), val(bf[1])), + c().val(j), + j, + *m, + bf, + *this); i.tangent_lemma_on_bf(); - if (!bf.is_mon()) { - lp::explanation expl; - generate_explanations_of_tang_lemma(*m, bf, expl); - for (unsigned i = lemmas_size_was; i < c().m_lemma_vec->size(); i++) { - auto &l = ((*c().m_lemma_vec)[i]); - l.expl().add(expl); - } - } - TRACE("nla_solver", - for (unsigned i = lemmas_size_was; i < c().m_lemma_vec->size(); i++) - c().print_specific_lemma((*c().m_lemma_vec)[i], tout); ); - } } -void tangents::generate_explanations_of_tang_lemma(const monic& rm, const factorization& bf, lp::explanation& exp) { - // here we repeat the same explanation for each lemma - c().explain(rm, exp); - c().explain(bf[0], exp); - c().explain(bf[1], exp); -} } diff --git a/src/math/lp/nla_tangent_lemmas.h b/src/math/lp/nla_tangent_lemmas.h index 66f9c695b..1895b3fcb 100644 --- a/src/math/lp/nla_tangent_lemmas.h +++ b/src/math/lp/nla_tangent_lemmas.h @@ -43,6 +43,5 @@ inline std::ostream& operator<<(std::ostream& out, point const& a) { return out struct tangents : common { tangents(core *core); void tangent_lemma(); - void generate_explanations_of_tang_lemma(const monic& rm, const factorization& bf, lp::explanation& exp); }; // end of tangents } // end of namespace diff --git a/src/test/lp/nla_solver_test.cpp b/src/test/lp/nla_solver_test.cpp index 6770d36c3..45c719733 100644 --- a/src/test/lp/nla_solver_test.cpp +++ b/src/test/lp/nla_solver_test.cpp @@ -193,9 +193,9 @@ void test_basic_lemma_for_mon_neutral_from_factors_to_monomial_0() { s.set_column_value_test(lp_bde, lp::impq(rational(16))); - SASSERT(nla.get_core().test_check(lv) == l_false); + VERIFY(nla.get_core().test_check(lv) == l_false); - nla.get_core().print_lemma(std::cout); + nla.get_core().print_lemma(lv.back(), std::cout); ineq i0(lp_ac, llc::NE, 1); lp::lar_term t1, t2; @@ -259,9 +259,9 @@ 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)); - SASSERT(nla.get_core().test_check(lemma) == l_false); + VERIFY(nla.get_core().test_check(lemma) == l_false); SASSERT(lemma[0].size() == 4); - nla.get_core().print_lemma(std::cout); + nla.get_core().print_lemma(lemma.back(), std::cout); lp::lar_term t0, t1, t2, t3; t0.add_var(lp_b); @@ -344,8 +344,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)); - SASSERT(nla.get_core().test_check(lemma) == l_false); - nla.get_core().print_lemma(std::cout); + VERIFY(nla.get_core().test_check(lemma) == l_false); + nla.get_core().print_lemma(lemma.back(), std::cout); SASSERT(lemma.size() == 1 && lemma[0].size() == 2); lp::lar_term t0, t1; t0.add_var(lp_b); @@ -395,9 +395,9 @@ void test_basic_lemma_for_mon_zero_from_monomial_to_factors() { s_set_column_value_test(s, lp_d, rational(1)); s_set_column_value_test(s, lp_acd, rational(0)); - SASSERT(nla.get_core().test_check(lemma) == l_false); + VERIFY(nla.get_core().test_check(lemma) == l_false); - nla.get_core().print_lemma(std::cout); + nla.get_core().print_lemma(lemma.back(), std::cout); ineq i0(lp_a, llc::EQ, 0); ineq i1(lp_c, llc::EQ, 0); @@ -471,10 +471,10 @@ 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)); - SASSERT(nla.get_core().test_check(lemma) == l_false); + VERIFY(nla.get_core().test_check(lemma) == l_false); - nla.get_core().print_lemma(std::cout); + nla.get_core().print_lemma(lemma.back(), std::cout); ineq i0(lp_d, llc::EQ, 1); ineq i1(lp_d, llc::EQ, -1); bool found0 = false; @@ -585,14 +585,14 @@ void test_basic_sign_lemma() { s_set_column_value_test(s, lp_acd, rational(3)); vector lemmas; - SASSERT(nla.get_core().test_check(lemmas) == l_false); + VERIFY(nla.get_core().test_check(lemmas) == l_false); lp::lar_term t; t.add_var(lp_bde); t.add_var(lp_acd); ineq q(llc::EQ, t, rational(0)); - nla.get_core().print_lemma(std::cout); + nla.get_core().print_lemma(lemmas.back(), std::cout); } void test_order_lemma_params(bool var_equiv, int sign) { @@ -709,13 +709,13 @@ void test_order_lemma_params(bool var_equiv, int sign) { } vector lemma; - SASSERT(nla.get_core().test_check(lemma) == l_false); + VERIFY(nla.get_core().test_check(lemma) == l_false); // lp::lar_term t; // t.add_monomial(lp_bde); // t.add_monomial(lp_acd); // ineq q(llc::EQ, t, rational(0)); - nla.get_core().print_lemma(std::cout); + nla.get_core().print_lemma(lemma.back(), std::cout); // SASSERT(q == lemma.back()); // ineq i0(llc::EQ, lp::lar_term(), rational(0)); // i0.m_term.add_monomial(lp_bde); @@ -793,8 +793,8 @@ void test_monotone_lemma() { s_set_column_value_test(s, lp_ef, s.get_column_value(lp_ij)); vector lemma; - SASSERT(nla.get_core().test_check(lemma) == l_false); - nla.get_core().print_lemma(std::cout); + VERIFY(nla.get_core().test_check(lemma) == l_false); + nla.get_core().print_lemma(lemma.back(), std::cout); */ } @@ -822,8 +822,8 @@ void test_tangent_lemma_rat() { nla.add_monic(lp_ab, vec.size(), vec.begin()); vector lemma; - SASSERT(nla.get_core().test_check(lemma) == l_false); - nla.get_core().print_lemma(std::cout); + VERIFY(nla.get_core().test_check(lemma) == l_false); + nla.get_core().print_lemma(lemma.back(), std::cout); } void test_tangent_lemma_reg() { @@ -849,8 +849,8 @@ void test_tangent_lemma_reg() { nla.add_monic(lp_ab, vec.size(), vec.begin()); vector lemma; - SASSERT(nla.get_core().test_check(lemma) == l_false); - nla.get_core().print_lemma(std::cout); + VERIFY(nla.get_core().test_check(lemma) == l_false); + nla.get_core().print_lemma(lemma.back(), std::cout); } void test_tangent_lemma_equiv() { @@ -895,8 +895,8 @@ void test_tangent_lemma_equiv() { 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; - SASSERT(nla.get_core().test_check(lemma) == l_false); - nla.get_core().print_lemma(std::cout); + VERIFY(nla.get_core().test_check(lemma) == l_false); + nla.get_core().print_lemma(lemma.back(), std::cout); */ }