From 99043399ceef7eec9c33e0019ba06ead97f76e94 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 10 May 2020 20:28:35 -0700 Subject: [PATCH] na Signed-off-by: Nikolaj Bjorner --- src/math/lp/nla_basics_lemmas.cpp | 78 ++++++++++++------------------- src/math/lp/nla_core.cpp | 58 ++++++++++++----------- src/math/lp/nla_core.h | 13 +++--- 3 files changed, 69 insertions(+), 80 deletions(-) diff --git a/src/math/lp/nla_basics_lemmas.cpp b/src/math/lp/nla_basics_lemmas.cpp index 868f96526..ec4a92a63 100644 --- a/src/math/lp/nla_basics_lemmas.cpp +++ b/src/math/lp/nla_basics_lemmas.cpp @@ -207,11 +207,11 @@ void basics::negate_strict_sign(new_lemma& lemma, lpvar j) { } else { // val(j).is_zero() if (c().has_lower_bound(j) && c().get_lower_bound(j) >= rational(0)) { - c().explain_existing_lower_bound(lemma, j); + lemma.explain_existing_lower_bound(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(lemma, j); + lemma.explain_existing_upper_bound(j); lemma |= ineq(j, llc::LT, 0); } } @@ -302,7 +302,7 @@ bool basics::basic_lemma_for_mon_non_zero_derived(const monic& rm, const factori 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.explain_var_separated_from_zero(var(rm)); lemma &= rm; lemma &= f; return true; @@ -328,7 +328,7 @@ bool basics::basic_lemma_for_mon_neutral_derived(const monic& rm, const factoriz return false; } bool mon_var_is_sep_from_zero = c().var_is_separated_from_zero(mon_var); - lpvar jl = null_lpvar, not_one_j = null_lpvar; + lpvar u = null_lpvar, v = null_lpvar; bool all_int = true; for (auto fc : f) { lpvar j = var(fc); @@ -336,31 +336,22 @@ bool basics::basic_lemma_for_mon_neutral_derived(const monic& rm, const factoriz if (j == null_lpvar && abs(val(j)) == abs_mv && c().vars_are_equiv(j, mon_var) && (mon_var_is_sep_from_zero || c().var_is_separated_from_zero(j))) - jl = j; - else if (j == jl) - return false; + u = j; else if (abs(val(j)) != rational(1)) - not_one_j = j; + v = j; } - if (jl == null_lpvar || not_one_j == null_lpvar) + if (u == null_lpvar || v == null_lpvar) return false; if (!all_int && f.size() > 2) return false; + // (mon_var != 0 || u != 0) & mon_var = +/- u => + // v = 1 or v = -1 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(lemma, mon_var); - else - 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); + lemma.explain_var_separated_from_zero(mon_var_is_sep_from_zero ? mon_var : u); + lemma.explain_equiv(mon_var, u); + lemma |= ineq(v, llc::EQ, 1); + lemma |= ineq(v, llc::EQ, -1); lemma &= rm; lemma &= f; return true; @@ -422,9 +413,6 @@ NSB review: sign_m*m < 0 or f_j = 0 or \/_{i != j} sign_m*m >= sign_i*f_i -- or even, without reference to factor index: - sign_m*m < 0 or \/_i sign_m*m >= sign_i*f_i - */ void basics::generate_pl_on_mon(const monic& m, unsigned factor_index) { SASSERT(!mon_has_real(m)); @@ -529,7 +517,7 @@ 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(lemma, var(j)); + lemma.explain_separation_from_zero(var(j)); } } lemma &= f; @@ -601,8 +589,8 @@ bool basics::basic_lemma_for_mon_neutral_from_factors_to_monic_model_based_fm(co new_lemma lemma(c(), __FUNCTION__); for (auto j : m.vars()) { - if (not_one == j) continue; - lemma |= ineq(j, llc::NE, val(j)); + if (not_one != j) + lemma |= ineq(j, llc::NE, val(j)); } if (not_one == null_lpvar) @@ -613,7 +601,7 @@ bool basics::basic_lemma_for_mon_neutral_from_factors_to_monic_model_based_fm(co } // use the fact that -// |xabc| = |x| and x != 0 -> |a| = |b| = |c| = 1 +// |uvw| = |u| and uvw != 0 -> |v| = 1 bool basics::basic_lemma_for_mon_neutral_monic_to_factor_model_based(const monic& rm, const factorization& f) { lpvar mon_var = c().emons()[rm.var()].var(); TRACE("nla_solver_bl", c().trace_print_monic_and_factorization(rm, f, tout); tout << "\nmon_var = " << mon_var << "\n";); @@ -624,36 +612,32 @@ bool basics::basic_lemma_for_mon_neutral_monic_to_factor_model_based(const monic if (abs_mv == rational::zero()) { return false; } - lpvar jl = null_lpvar, not_one_j = null_lpvar; + lpvar u = null_lpvar, v = null_lpvar; bool all_int = true; for (auto fc : f) { lpvar j = var(fc); all_int &= c().var_is_int(j); if (j == null_lpvar && abs(val(fc)) == abs_mv) - jl = j; - else if (j == jl) - return false; + u = j; else if (abs(val(fc)) != rational(1)) - not_one_j = j; + v = j; } - if (jl == null_lpvar || not_one_j == null_lpvar) + if (u == null_lpvar || v == null_lpvar) return false; if (!all_int && f.size() > 2) return false; - new_lemma lemma(c(), __FUNCTION__); // mon_var = 0 - lemma |= ineq(mon_var, llc::EQ, 0); - - // negate abs(jl) == abs() - lemma |= ineq(term(jl, rational(val(jl) == -val(mon_var) ? 1 : -1), mon_var), llc::NE, 0); + // abs(u) != abs(mon_var) + // v = 1 + // v = -1 - // not_one_j = 1 - lemma |= ineq(not_one_j, llc::EQ, 1); - - // not_one_j = -1 - lemma |= ineq(not_one_j, llc::EQ, -1); - lemma &= rm; + new_lemma lemma(c(), __FUNCTION__); + lemma |= ineq(mon_var, llc::EQ, 0); + 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 &= f; return true; @@ -695,7 +679,7 @@ bool basics::basic_lemma_for_mon_neutral_from_factors_to_monic_model_based(const } if (v == -rational(1)) { - sign = - sign; + sign = -sign; continue; } diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index e2f474526..b0a3dd1ad 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -625,24 +625,6 @@ bool core::is_canonical_monic(lpvar j) const { } -void core::explain_existing_lower_bound(new_lemma& lemma, lpvar j) { - SASSERT(has_lower_bound(j)); - lemma &= m_lar_solver.get_column_lower_bound_witness(j); -} - -void core::explain_existing_upper_bound(new_lemma& lemma, lpvar j) { - SASSERT(has_upper_bound(j)); - lemma &= m_lar_solver.get_column_upper_bound_witness(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(lemma, j); - else - 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) << "\n"; @@ -651,14 +633,6 @@ void core::trace_print_monic_and_factorization(const monic& rm, const factorizat print_factorization(f, out << "fact: ") << "\n"; } -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())) - lemma &= m_lar_solver.get_column_upper_bound_witness(j); - else - lemma &= 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(); @@ -1187,6 +1161,38 @@ new_lemma& new_lemma::explain_equiv(lpvar a, lpvar b) { return *this; } +new_lemma& new_lemma::explain_var_separated_from_zero(lpvar j) { + SASSERT(c.var_is_separated_from_zero(j)); + if (c.m_lar_solver.column_has_upper_bound(j) && + (c.m_lar_solver.get_upper_bound(j)< lp::zero_of_type())) + *this &= c.m_lar_solver.get_column_upper_bound_witness(j); + else + *this &= c.m_lar_solver.get_column_lower_bound_witness(j); + return *this; +} + +new_lemma& new_lemma::explain_existing_lower_bound(lpvar j) { + SASSERT(c.has_lower_bound(j)); + *this &= c.m_lar_solver.get_column_lower_bound_witness(j); + return *this; +} + +new_lemma& new_lemma::explain_existing_upper_bound(lpvar j) { + SASSERT(c.has_upper_bound(j)); + *this &= c.m_lar_solver.get_column_upper_bound_witness(j); + return *this; +} + +new_lemma& new_lemma::explain_separation_from_zero(lpvar j) { + SASSERT(!c.val(j).is_zero()); + if (c.val(j).is_pos()) + explain_existing_lower_bound(j); + else + explain_existing_upper_bound(j); + return *this; +} + + std::ostream& new_lemma::display(std::ostream & out) const { auto const& lemma = current(); diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h index 1f13dc18e..b92c387d7 100644 --- a/src/math/lp/nla_core.h +++ b/src/math/lp/nla_core.h @@ -105,6 +105,11 @@ public: new_lemma& operator|=(ineq const& i); new_lemma& explain_fixed(lpvar j); new_lemma& explain_equiv(lpvar u, lpvar v); + new_lemma& explain_var_separated_from_zero(lpvar j); + new_lemma& explain_existing_lower_bound(lpvar j); + new_lemma& explain_existing_upper_bound(lpvar j); + new_lemma& explain_separation_from_zero(lpvar j); + unsigned num_ineqs() const { return current().ineqs().size(); } }; @@ -245,13 +250,7 @@ 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; - - // 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; std::ostream & print_var(lpvar j, std::ostream & out) const;