From caee936af56b185cd3726c196d5f74ca09e7a8cb Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 10 May 2020 13:42:19 -0700 Subject: [PATCH] build Signed-off-by: Nikolaj Bjorner --- src/math/lp/lar_term.h | 3 ++ src/math/lp/nla_basics_lemmas.cpp | 62 ++++++++++++++++--------------- src/test/lp/nla_solver_test.cpp | 58 ++++++++++++++--------------- 3 files changed, 64 insertions(+), 59 deletions(-) diff --git a/src/math/lp/lar_term.h b/src/math/lp/lar_term.h index 8bee7ba7a..2e8117d51 100644 --- a/src/math/lp/lar_term.h +++ b/src/math/lp/lar_term.h @@ -70,6 +70,9 @@ public: lar_term(lpvar v1) { add_monomial(rational::one(), v1); } + lar_term(rational const& a, lpvar v1) { + add_monomial(a, v1); + } lar_term(lpvar v1, rational const& b, lpvar v2) { add_monomial(rational::one(), v1); add_monomial(b, v2); diff --git a/src/math/lp/nla_basics_lemmas.cpp b/src/math/lp/nla_basics_lemmas.cpp index 00440a6a2..673839d42 100644 --- a/src/math/lp/nla_basics_lemmas.cpp +++ b/src/math/lp/nla_basics_lemmas.cpp @@ -290,7 +290,7 @@ bool basics::basic_lemma_for_mon_derived(const monic& rm) { // 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))) + if (!c().var_is_separated_from_zero(var(rm))) return false; lpvar zero_j = null_lpvar; for (auto j : f) { @@ -309,6 +309,7 @@ bool basics::basic_lemma_for_mon_non_zero_derived(const monic& rm, const factori explain(rm); return true; } + // use the fact that // |xabc| = |x| and x != 0 -> |a| = |b| = |c| = 1 // it holds for integers, and for reals for a pair of factors @@ -423,8 +424,8 @@ 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 +- 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) { @@ -448,9 +449,15 @@ 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| + +/** + none of the factors is zero and the product is not zero + -> |fc[factor_index]| <= |rm| + + m := f1 * .. * f_n + + 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; @@ -467,23 +474,21 @@ void basics::generate_pl(const monic& m, const factorization& fc, int factor_ind rational mv = var_val(m); rational sm = rational(nla::rat_sign(mv)); unsigned mon_var = var(m); - c().mk_ineq(sm, mon_var, llc::LT); + lemma |= ineq(term(sm, mon_var), llc::LT, 0); for (factor f : fc) { if (fi++ != factor_index) { - c().mk_ineq(var(f), llc::EQ); + lemma |= ineq(var(f), llc::EQ, 0); } else { lpvar j = var(f); 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: 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); } } - if (!fc.is_mon()) { - explain(fc); - explain(m); - } + explain(fc); + explain(m); } bool basics::is_separated_from_zero(const factorization& f) const { @@ -520,12 +525,12 @@ void basics::basic_lemma_for_mon_zero_model_based(const monic& rm, const factori SASSERT(var_val(rm).is_zero() && !c().rm_check(rm)); new_lemma lemma(c(), "xy = 0 -> x = 0 or y = 0"); if (!is_separated_from_zero(f)) { - c().mk_ineq(var(rm), llc::NE); + lemma |= ineq(var(rm), llc::NE, 0); for (auto j : f) { - c().mk_ineq(var(j), llc::EQ); + lemma |= ineq(var(j), llc::EQ, 0); } } else { - c().mk_ineq(var(rm), llc::NE); + lemma |= ineq(var(rm), llc::NE, 0); for (auto j : f) { c().explain_separation_from_zero(var(j)); } @@ -583,19 +588,19 @@ bool basics::basic_lemma_for_mon_neutral_monic_to_factor_model_based_fm(const mo 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, rational::zero()); + 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); return true; } @@ -641,14 +646,13 @@ 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; - c().mk_ineq(j, llc::NE, val(j)); + lemma |= ineq(j, llc::NE, val(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); return true; } diff --git a/src/test/lp/nla_solver_test.cpp b/src/test/lp/nla_solver_test.cpp index 1687c912b..6770d36c3 100644 --- a/src/test/lp/nla_solver_test.cpp +++ b/src/test/lp/nla_solver_test.cpp @@ -197,14 +197,14 @@ void test_basic_lemma_for_mon_neutral_from_factors_to_monomial_0() { nla.get_core().print_lemma(std::cout); - ineq i0(llc::NE, lp::lar_term(), rational(1)); - i0.m_term.add_var(lp_ac); - ineq i1(llc::EQ, lp::lar_term(), rational(0)); - i1.m_term.add_var(lp_bde); - i1.m_term.add_monomial(-rational(1), lp_abcde); - ineq i2(llc::EQ, lp::lar_term(), rational(0)); - i2.m_term.add_var(lp_abcde); - i2.m_term.add_monomial(-rational(1), lp_bde); + ineq i0(lp_ac, llc::NE, 1); + lp::lar_term t1, t2; + t1.add_var(lp_bde); + t1.add_monomial(-rational(1), lp_abcde); + ineq i1(llc::EQ, t1, rational(0)); + t2.add_var(lp_abcde); + t2.add_monomial(-rational(1), lp_bde); + ineq i2(llc::EQ, t2, rational(0)); bool found0 = false; bool found1 = false; bool found2 = false; @@ -263,14 +263,15 @@ void test_basic_lemma_for_mon_neutral_from_factors_to_monomial_1() { SASSERT(lemma[0].size() == 4); nla.get_core().print_lemma(std::cout); - ineq i0(llc::NE, lp::lar_term(), rational(1)); - i0.m_term.add_var(lp_b); - ineq i1(llc::NE, lp::lar_term(), rational(1)); - i1.m_term.add_var(lp_d); - ineq i2(llc::NE, lp::lar_term(), rational(1)); - i2.m_term.add_var(lp_e); - ineq i3(llc::EQ, lp::lar_term(), rational(1)); - i3.m_term.add_var(lp_bde); + lp::lar_term t0, t1, t2, t3; + t0.add_var(lp_b); + t1.add_var(lp_d); + t2.add_var(lp_e); + t3.add_var(lp_bde); + ineq i0(llc::NE, t0, rational(1)); + ineq i1(llc::NE, t1, rational(1)); + ineq i2(llc::NE, t2, rational(1)); + ineq i3(llc::EQ, t3, rational(1)); bool found0 = false; bool found1 = false; bool found2 = false; @@ -346,10 +347,12 @@ void test_basic_lemma_for_mon_zero_from_factors_to_monomial() { SASSERT(nla.get_core().test_check(lemma) == l_false); nla.get_core().print_lemma(std::cout); SASSERT(lemma.size() == 1 && lemma[0].size() == 2); - ineq i0(llc::NE, lp::lar_term(), rational(0)); - i0.m_term.add_var(lp_b); - ineq i1(llc::EQ, lp::lar_term(), rational(0)); - i1.m_term.add_var(lp_be); + lp::lar_term t0, t1; + t0.add_var(lp_b); + t1.add_var(lp_be); + + ineq i0(llc::NE, t0, rational(0)); + ineq i1(llc::EQ, t1, rational(0)); bool found0 = false; bool found1 = false; @@ -396,12 +399,9 @@ void test_basic_lemma_for_mon_zero_from_monomial_to_factors() { nla.get_core().print_lemma(std::cout); - ineq i0(llc::EQ, lp::lar_term(), rational(0)); - i0.m_term.add_var(lp_a); - ineq i1(llc::EQ, lp::lar_term(), rational(0)); - i1.m_term.add_var(lp_c); - ineq i2(llc::EQ, lp::lar_term(), rational(0)); - i2.m_term.add_var(lp_d); + ineq i0(lp_a, llc::EQ, 0); + ineq i1(lp_c, llc::EQ, 0); + ineq i2(lp_d, llc::EQ, 0); bool found0 = false; bool found1 = false; bool found2 = false; @@ -475,10 +475,8 @@ void test_basic_lemma_for_mon_neutral_from_monomial_to_factors() { nla.get_core().print_lemma(std::cout); - ineq i0(llc::EQ, lp::lar_term(), rational(1)); - i0.m_term.add_var(lp_d); - ineq i1(llc::EQ, lp::lar_term(), -rational(1)); - i1.m_term.add_var(lp_d); + ineq i0(lp_d, llc::EQ, 1); + ineq i1(lp_d, llc::EQ, -1); bool found0 = false; bool found1 = false;