From 81b3c440cee416aed56e0457408f883a0860d541 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 11 May 2020 13:07:28 -0700 Subject: [PATCH] fix mixup between constraint indices and lpvar explanations fixes various newly reported unsoundness bugs Signed-off-by: Nikolaj Bjorner --- src/math/lp/lar_constraints.h | 4 +-- src/math/lp/nla_basics_lemmas.cpp | 4 +-- src/math/lp/nla_core.cpp | 53 ++++++++++++++++++++----------- src/math/lp/nla_core.h | 3 +- 4 files changed, 40 insertions(+), 24 deletions(-) diff --git a/src/math/lp/lar_constraints.h b/src/math/lp/lar_constraints.h index dbc682b6d..8cbd83801 100644 --- a/src/math/lp/lar_constraints.h +++ b/src/math/lp/lar_constraints.h @@ -251,8 +251,8 @@ public: std::ostream& display(std::ostream& out) const { out << "number of constraints = " << m_constraints.size() << std::endl; - for (auto const& c : active()) { - display(out, c); + for (auto const& c : indices()) { + display(out << "(" << c << ") ", *m_constraints[c]); } return out; } diff --git a/src/math/lp/nla_basics_lemmas.cpp b/src/math/lp/nla_basics_lemmas.cpp index ec4a92a63..dea499fbf 100644 --- a/src/math/lp/nla_basics_lemmas.cpp +++ b/src/math/lp/nla_basics_lemmas.cpp @@ -200,7 +200,7 @@ void basics::add_fixed_zero_lemma(const monic& m, lpvar j) { } void basics::negate_strict_sign(new_lemma& lemma, lpvar j) { - TRACE("nla_solver_details", tout << pp_var(c(), j) << "\n";); + TRACE("nla_solver_details", tout << pp_var(c(), j) << " " << val(j).is_zero() << "\n";); if (!val(j).is_zero()) { int sign = nla::rat_sign(val(j)); lemma |= ineq(j, (sign == 1? llc::LE : llc::GE), 0); @@ -635,7 +635,7 @@ bool basics::basic_lemma_for_mon_neutral_monic_to_factor_model_based(const monic 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 |= ineq(v, llc::EQ, -1); lemma &= rm; // NSB review: is this dependency required? lemma &= f; diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index 084009611..a5cbfb8f5 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -1100,8 +1100,9 @@ new_lemma& new_lemma::operator|=(ineq const& ineq) { } new_lemma::~new_lemma() { + static int i = 0; // code for checking lemma can be added here - TRACE("nla_solver", tout << name << "\n" << *this; ); + TRACE("nla_solver", tout << name << " " << (++i) << "\n" << *this; ); } lemma& new_lemma::current() const { @@ -1143,8 +1144,8 @@ new_lemma& new_lemma::operator&=(lpvar j) { 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); + explain_existing_lower_bound(j); + explain_existing_upper_bound(j); return *this; } @@ -1164,21 +1165,26 @@ 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); + explain_existing_upper_bound(j); else - *this &= c.m_lar_solver.get_column_lower_bound_witness(j); + explain_existing_lower_bound(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); + lp::explanation ex; + ex.add(c.m_lar_solver.get_column_lower_bound_witness(j)); + *this &= ex; + TRACE("nla_solver", tout << j << ": " << *this << "\n";); 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); + lp::explanation ex; + ex.add(c.m_lar_solver.get_column_upper_bound_witness(j)); + *this &= ex; return *this; } @@ -1468,14 +1474,28 @@ lbool core::check(vector& l_vec) { } } - if (!done()) - incremental_linearization(true); + TRACE("nla_solver_details", print_terms(tout); tout << m_lar_solver.constraints();); + if (!done()) + m_basics.basic_lemma(true); - if (!done() && m_lemma_vec->empty()) - incremental_linearization(false); + TRACE("nla_solver", tout << "passed constraint_derived and basic lemmas\n";); + SASSERT(elists_are_consistent(true)); - lbool ret = !m_lemma_vec->empty() && !lp_settings().get_cancel_flag() ? l_false : l_undef; - TRACE("nla_solver", tout << "ret = " << ret << ", lemmas count = " << m_lemma_vec->size() << "\n";); + if (l_vec.empty() && !done()) + m_basics.basic_lemma(false); + + if (l_vec.empty() && !done()) + m_order.order_lemma(); + + if (l_vec.empty() && !done()) { + if (!done()) + m_monotone.monotonicity_lemma(); + if (!done()) + m_tangents.tangent_lemma(); + } + + lbool ret = !l_vec.empty() && !lp_settings().get_cancel_flag() ? l_false : l_undef; + TRACE("nla_solver", tout << "ret = " << ret << ", lemmas count = " << l_vec.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; @@ -1840,15 +1860,10 @@ unsigned core::get_var_weight(lpvar j) const { return k; } - bool core::is_nl_var(lpvar j) const { - if (is_monic_var(j)) - return true; - return m_emons.is_used_in_monic(j); + return is_monic_var(j) || m_emons.is_used_in_monic(j); } - - bool core::influences_nl_var(lpvar j) const { if (lp::tv::is_term(j)) j = lp::tv::unmask_term(j); diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h index fcadd8a75..a0985c376 100644 --- a/src/math/lp/nla_core.h +++ b/src/math/lp/nla_core.h @@ -90,7 +90,6 @@ 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); @@ -110,6 +109,8 @@ public: new_lemma& explain_existing_upper_bound(lpvar j); new_lemma& explain_separation_from_zero(lpvar j); + lp::explanation& expl() { return current().expl(); } + unsigned num_ineqs() const { return current().ineqs().size(); } };