From e74faf42ad263539c744856d34eafd2ac18a1eba Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 10 May 2020 12:58:05 -0700 Subject: [PATCH] code review --- src/math/lp/lar_term.h | 15 +++++ src/math/lp/nla_basics_lemmas.cpp | 98 +++++++++++++++++++++---------- src/math/lp/nla_basics_lemmas.h | 1 + src/math/lp/nla_core.cpp | 20 ++++--- src/math/lp/nla_core.h | 15 ++++- src/smt/theory_lra.cpp | 6 +- 6 files changed, 110 insertions(+), 45 deletions(-) diff --git a/src/math/lp/lar_term.h b/src/math/lp/lar_term.h index 662ed0410..8bee7ba7a 100644 --- a/src/math/lp/lar_term.h +++ b/src/math/lp/lar_term.h @@ -63,6 +63,21 @@ public: add_monomial(p.first, p.second); } } + lar_term(lpvar v1, lpvar v2) { + add_monomial(rational::one(), v1); + add_monomial(rational::one(), v2); + } + lar_term(lpvar v1) { + add_monomial(rational::one(), v1); + } + lar_term(lpvar v1, rational const& b, lpvar v2) { + add_monomial(rational::one(), v1); + add_monomial(b, v2); + } + lar_term(rational const& a, lpvar v1, rational const& b, lpvar v2) { + add_monomial(a, v1); + add_monomial(b, v2); + } bool operator==(const lar_term & a) const { return false; } // take care not to create identical terms bool operator!=(const lar_term & a) const { return ! (*this == a);} // some terms get used in add constraint diff --git a/src/math/lp/nla_basics_lemmas.cpp b/src/math/lp/nla_basics_lemmas.cpp index 4de3674da..00440a6a2 100644 --- a/src/math/lp/nla_basics_lemmas.cpp +++ b/src/math/lp/nla_basics_lemmas.cpp @@ -12,6 +12,8 @@ #include "math/lp/factorization_factory_imp.h" namespace nla { +typedef lp::lar_term term; + basics::basics(core * c) : common(c) {} // Monomials m and n vars have the same values, up to "sign" @@ -85,7 +87,7 @@ void basics::basic_sign_lemma_model_based_one_mon(const monic& m, int product_si for (lpvar j: m.vars()) { negate_strict_sign(j); } - c().mk_ineq(m.var(), product_sign == 1? llc::GT : llc::LT); + lemma |= ineq(m.var(), product_sign == 1? llc::GT : llc::LT, 0); } } @@ -152,7 +154,7 @@ void basics::generate_sign_lemma(const monic& m, const monic& n, const rational& tout << "m = " << pp_mon_with_vars(_(), m); tout << "n = " << pp_mon_with_vars(_(), n); ); - c().mk_ineq(m.var(), -sign, n.var(), llc::EQ); + lemma |= ineq(term(m.var(), -sign, n.var()), llc::EQ, 0); explain(m); explain(n); } @@ -174,15 +176,15 @@ lpvar basics::find_best_zero(const monic& m, unsigned_vector & fixed_zeros) cons void basics::add_trivial_zero_lemma(lpvar zero_j, const monic& m) { new_lemma lemma(c(), "x = 0 => x*y = 0"); - c().mk_ineq(zero_j, llc::NE); - c().mk_ineq(m.var(), llc::EQ); + lemma |= ineq(zero_j, llc::NE, 0); + lemma |= ineq(m.var(), llc::EQ, 0); } void basics::generate_strict_case_zero_lemma(const monic& m, unsigned zero_j, int sign_of_zj) { TRACE("nla_solver_bl", tout << "sign_of_zj = " << sign_of_zj << "\n";); // we know all the signs new_lemma lemma(c(), "strict case 0"); - c().mk_ineq(zero_j, (sign_of_zj == 1? llc::GT : llc::LT)); + 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); @@ -190,11 +192,13 @@ void basics::generate_strict_case_zero_lemma(const monic& m, unsigned zero_j, in } negate_strict_sign(m.var()); } + void basics::add_fixed_zero_lemma(const monic& m, lpvar j) { new_lemma lemma(c(), "fixed zero"); c().explain_fixed_var(j); - c().mk_ineq(m.var(), llc::EQ); + lemma |= ineq(m.var(), llc::EQ, 0); } + void basics::negate_strict_sign(lpvar j) { TRACE("nla_solver_details", tout << pp_var(c(), j) << "\n";); if (!val(j).is_zero()) { @@ -224,7 +228,7 @@ bool basics::basic_lemma_for_mon_zero(const monic& rm, const factorization& f) { std::unordered_set processed; for (auto j : f) { if (try_insert(var(j), processed)) - c().mk_ineq(var(j), llc::EQ); + lemma |= ineq(var(j), llc::EQ, 0); } explain(rm); return true; @@ -290,7 +294,7 @@ bool basics::basic_lemma_for_mon_non_zero_derived(const monic& rm, const factori return false; lpvar zero_j = null_lpvar; for (auto j : f) { - if ( c().var_is_fixed_to_zero(var(j))) { + if (c().var_is_fixed_to_zero(var(j))) { zero_j = var(j); break; } @@ -352,10 +356,10 @@ bool basics::basic_lemma_for_mon_neutral_monic_to_factor_derived(const monic& rm c().explain_equiv_vars(mon_var, jl); // not_one_j = 1 - c().mk_ineq(not_one_j, llc::EQ, rational(1)); + lemma |= ineq(not_one_j, llc::EQ, 1); // not_one_j = -1 - c().mk_ineq(not_one_j, llc::EQ, -rational(1)); + lemma |= ineq(not_one_j, llc::EQ, -1); explain(rm); return true; } @@ -385,6 +389,7 @@ void basics::proportion_lemma_model_based(const monic& rm, const factorization& } // 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; rational rmv = abs(var_val(rm)); if (rmv.is_zero()) { @@ -401,8 +406,30 @@ bool basics::proportion_lemma_derived(const monic& rm, const factorization& fact } return false; } -// if there are no zero factors then |m| >= |m[factor_index]| + +/** + 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 + +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 + +- 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) { + if (mon_has_real(m)) + return; new_lemma lemma(c(), "generate_pl_on_mon"); unsigned mon_var = m.var(); rational mv = val(mon_var); @@ -411,13 +438,13 @@ void basics::generate_pl_on_mon(const monic& m, unsigned factor_index) { for (unsigned fi = 0; fi < m.size(); fi ++) { lpvar j = m.vars()[fi]; if (fi != factor_index) { - c().mk_ineq(j, llc::EQ); + lemma |= ineq(j, llc::EQ, 0); } else { rational jv = val(j); rational sj = rational(nla::rat_sign(jv)); - SASSERT(sm*mv < sj*jv); - c().mk_ineq(sj, j, llc::LT); - c().mk_ineq(sm, mon_var, -sj, j, llc::GE); + // NSB review: what is the justification for this assert: SASSERT(sm*mv < sj*jv); + // NSB review: removed c().mk_ineq(sj, j, llc::LT); + lemma |= ineq(term(sm, mon_var, -sj, j), llc::GE, 0); } } } @@ -425,6 +452,8 @@ void basics::generate_pl_on_mon(const monic& m, unsigned factor_index) { // none of the factors is zero and the product is not zero // -> |fc[factor_index]| <= |rm| void basics::generate_pl(const monic& m, const factorization& fc, int factor_index) { + if (factorization_has_real(fc)) + return; TRACE("nla_solver", tout << "factor_index = " << factor_index << ", m = " << pp_mon(c(), m); tout << ", fc = " << c().pp(fc); @@ -476,6 +505,14 @@ bool basics::factorization_has_real(const factorization& f) const { return false; } +bool basics::mon_has_real(const monic& m) const { + for (lpvar j : m.vars()) + if (!c().var_is_int(j)) + return true; + return false; +} + + // here we use the fact xy = 0 -> x = 0 or y = 0 void basics::basic_lemma_for_mon_zero_model_based(const monic& rm, const factorization& f) { @@ -550,7 +587,7 @@ bool basics::basic_lemma_for_mon_neutral_monic_to_factor_model_based_fm(const mo // negate abs(jl) == abs() if (val(jl) == - val(mon_var)) - c().mk_ineq(jl, mon_var, llc::NE, c().current_lemma()); + c().mk_ineq(jl, mon_var, llc::NE, rational::zero()); else // jl == mon_var c().mk_ineq(jl, -rational(1), mon_var, llc::NE); @@ -618,8 +655,6 @@ 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 bool basics::basic_lemma_for_mon_neutral_monic_to_factor_model_based(const monic& rm, const factorization& f) { - TRACE("nla_solver_bl", c().trace_print_monic_and_factorization(rm, f, tout);); - 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";); @@ -648,19 +683,19 @@ bool basics::basic_lemma_for_mon_neutral_monic_to_factor_model_based(const monic new_lemma lemma(c(), __FUNCTION__); // mon_var = 0 - c().mk_ineq(mon_var, llc::EQ); + lemma |= ineq(mon_var, llc::EQ, 0); // negate abs(jl) == abs() if (val(jl) == - val(mon_var)) - c().mk_ineq(jl, mon_var, llc::NE, c().current_lemma()); + lemma |= ineq(term(jl, mon_var), llc::NE, 0); else // jl == mon_var - c().mk_ineq(jl, -rational(1), mon_var, llc::NE); + lemma |= ineq(term(jl, -rational(1), mon_var), llc::NE, 0); // not_one_j = 1 - c().mk_ineq(not_one_j, llc::EQ, rational(1)); + lemma |= ineq(not_one_j, llc::EQ, 1); // not_one_j = -1 - c().mk_ineq(not_one_j, llc::EQ, -rational(1)); + lemma |= ineq(not_one_j, llc::EQ, -1); explain(rm); explain(f); @@ -732,15 +767,14 @@ bool basics::basic_lemma_for_mon_neutral_from_factors_to_monic_model_based(const for (auto j : f) { lpvar var_j = var(j); if (not_one == var_j) continue; - TRACE("nla_solver_bl", tout << "j = "; c().print_factor_with_vars(j, tout);); - c().mk_ineq(var_j, llc::NE, val(var_j)); + TRACE("nla_solver_bl", tout << "j = "; c().print_factor_with_vars(j, tout);); + lemma |= ineq(var_j, llc::NE, val(var_j)); } - if (not_one == null_lpvar) { - c().mk_ineq(m.var(), llc::EQ, sign); - } else { - c().mk_ineq(m.var(), -sign, not_one, llc::EQ); - } + if (not_one == null_lpvar) + lemma |= ineq(m.var(), llc::EQ, sign); + else + lemma |= ineq(term(m.var(), -sign, not_one), llc::EQ, 0); explain(m); explain(f); TRACE("nla_solver", tout << "m = " << pp_mon_with_vars(c(), m);); @@ -754,8 +788,8 @@ void basics::basic_lemma_for_mon_non_zero_model_based_mf(const factorization& f) if (val(j).is_zero()) { lpvar zero_j = var(j); new_lemma lemma(c(), "x = 0 => x*... = 0"); - c().mk_ineq(zero_j, llc::NE); - c().mk_ineq(f.mon().var(), llc::EQ); + lemma |= ineq(zero_j, llc::NE, 0); + lemma |= ineq(f.mon().var(), llc::EQ, 0); return; } } diff --git a/src/math/lp/nla_basics_lemmas.h b/src/math/lp/nla_basics_lemmas.h index 56ea73e6d..9baa4336c 100644 --- a/src/math/lp/nla_basics_lemmas.h +++ b/src/math/lp/nla_basics_lemmas.h @@ -93,5 +93,6 @@ struct basics: common { void generate_pl(const monic& rm, const factorization& fc, int factor_index); bool is_separated_from_zero(const factorization&) const; bool factorization_has_real(const factorization&) const; + bool mon_has_real(const monic& m) const; }; } diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index c3a80309d..66fac9195 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -487,9 +487,6 @@ void core::mk_ineq(const rational& a, lpvar j, llc cmp) { mk_ineq(a, j, cmp, rational::zero()); } -void core::mk_ineq(lpvar j, lpvar k, llc cmp, lemma& _l) { - mk_ineq(rational(1), j, rational(1), k, cmp, rational::zero()); -} void core::mk_ineq(lpvar j, llc cmp) { mk_ineq(j, cmp, rational::zero()); @@ -633,8 +630,8 @@ bool core::var_is_free(lpvar j) const { } std::ostream & core::print_ineq(const ineq & in, std::ostream & out) const { - m_lar_solver.print_term_as_indices(in.m_term, out); - out << " " << lconstraint_kind_string(in.m_cmp) << " " << in.m_rs; + m_lar_solver.print_term_as_indices(in.term(), out); + out << " " << lconstraint_kind_string(in.cmp()) << " " << in.rs(); return out; } @@ -671,7 +668,7 @@ std::ostream & core::print_ineqs(const lemma& l, std::ostream & out) const { auto & in = l.ineqs()[i]; print_ineq(in, out); if (i + 1 < l.ineqs().size()) out << " or "; - for (const auto & p: in.m_term) + for (const auto & p: in.term()) vars.insert(p.column()); } out << std::endl; @@ -1049,7 +1046,7 @@ void core::negate_factor_equality(const factor& c, if (iv == jv) { mk_ineq(i, -rational(1), j, llc::NE); } else { // iv == -jv - mk_ineq(i, j, llc::NE, current_lemma()); + mk_ineq(i, j, llc::NE, rational::zero()); } } @@ -1237,6 +1234,15 @@ 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); + CTRACE("nla_solver", c.ineq_holds(ineq), c.print_ineq(ineq, tout) << "\n";); + SASSERT(!c.ineq_holds(ineq)); + } + return *this; +} + new_lemma::~new_lemma() { // code for checking lemma can be added here TRACE("nla_solver", tout << name << "\n" << *this; ); diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h index 4b594b15d..d39e2ea94 100644 --- a/src/math/lp/nla_core.h +++ b/src/math/lp/nla_core.h @@ -47,12 +47,17 @@ const lpvar null_lpvar = UINT_MAX; inline int rat_sign(const rational& r) { return r.is_pos()? 1 : ( r.is_neg()? -1 : 0); } inline rational rrat_sign(const rational& r) { return rational(rat_sign(r)); } inline bool is_set(unsigned j) { return j != null_lpvar; } -inline bool is_even(unsigned k) { return (k >> 1) << 1 == k; } -struct ineq { +inline bool is_even(unsigned k) { return (k & 1) == 0; } +class ineq { lp::lconstraint_kind m_cmp; lp::lar_term m_term; rational m_rs; +public: ineq(lp::lconstraint_kind cmp, const lp::lar_term& term, const rational& rs) : m_cmp(cmp), m_term(term), m_rs(rs) {} + ineq(const lp::lar_term& term, lp::lconstraint_kind cmp, int i) : m_cmp(cmp), m_term(term), m_rs(rational(i)) {} + ineq(const lp::lar_term& term, lp::lconstraint_kind cmp, const rational& rs) : m_cmp(cmp), m_term(term), m_rs(rs) {} + ineq(lpvar v, lp::lconstraint_kind cmp, int i): m_cmp(cmp), m_term(v), m_rs(rational(i)) {} + ineq(lpvar v, lp::lconstraint_kind cmp, rational const& r): m_cmp(cmp), m_term(v), m_rs(r) {} bool operator==(const ineq& a) const { return m_cmp == a.m_cmp && m_term == a.m_term && m_rs == a.m_rs; } @@ -87,10 +92,15 @@ class new_lemma { public: new_lemma(core& c, char const* name); ~new_lemma(); + new_lemma& add(ineq const& ineq); lemma& operator()(); std::ostream& display(std::ostream& out) const; }; +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); } @@ -295,7 +305,6 @@ public: 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, lpvar k, llc cmp, lemma& l); void mk_ineq(lpvar j, llc cmp); diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 42a437d4d..57a36d0e9 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -2169,7 +2169,7 @@ public: literal_vector core; for (auto const& ineq : m_lemma.ineqs()) { bool is_lower = true, pos = true, is_eq = false; - switch (ineq.m_cmp) { + switch (ineq.cmp()) { case lp::LE: is_lower = false; pos = false; break; case lp::LT: is_lower = true; pos = true; break; case lp::GE: is_lower = true; pos = false; break; @@ -2183,11 +2183,11 @@ public: // TBD utility: lp::lar_term term = mk_term(ineq.m_poly); // then term is used instead of ineq.m_term if (is_eq) { - atom = mk_eq(ineq.m_term, ineq.m_rs); + atom = mk_eq(ineq.term(), ineq.rs()); } else { // create term >= 0 (or term <= 0) - atom = mk_bound(ineq.m_term, ineq.m_rs, is_lower); + atom = mk_bound(ineq.term(), ineq.rs(), is_lower); } literal lit(ctx().get_bool_var(atom), pos); core.push_back(~lit);