From 29710020a56391c1f32df6bd6749246e1554e034 Mon Sep 17 00:00:00 2001 From: Lev Date: Tue, 30 Oct 2018 16:57:58 -0700 Subject: [PATCH] strengthening test cases Signed-off-by: Lev --- src/util/lp/lar_term.h | 2 +- src/util/lp/nla_solver.cpp | 62 +++++++++++++++++++++++++++++--------- src/util/lp/nla_solver.h | 5 ++- 3 files changed, 53 insertions(+), 16 deletions(-) diff --git a/src/util/lp/lar_term.h b/src/util/lp/lar_term.h index 4d5257a08..534896d4c 100644 --- a/src/util/lp/lar_term.h +++ b/src/util/lp/lar_term.h @@ -57,7 +57,7 @@ public: return m_coeffs; } - bool operator==(const lar_term & a) const { return false; } // take care not to create identical terms + bool operator==(const lar_term & a) const { return m_coeffs == a.m_coeffs; } bool operator!=(const lar_term & a) const { return ! (*this == a);} // some terms get used in add constraint // it is the same as the offset in the m_constraints diff --git a/src/util/lp/nla_solver.cpp b/src/util/lp/nla_solver.cpp index 08b71c10b..055a997e5 100644 --- a/src/util/lp/nla_solver.cpp +++ b/src/util/lp/nla_solver.cpp @@ -1199,17 +1199,9 @@ void solver::test_basic_lemma_for_mon_zero_from_monomial_to_factors() { lp::explanation exp; - // set all vars to 1 - s.set_column_value(lp_a, rational(1)); s.set_column_value(lp_b, rational(1)); - s.set_column_value(lp_c, rational(1)); s.set_column_value(lp_d, rational(1)); s.set_column_value(lp_e, rational(1)); - s.set_column_value(lp_abcde, rational(1)); - s.set_column_value(lp_ac, rational(1)); - s.set_column_value(lp_bde, rational(1)); - s.set_column_value(lp_acd, rational(1)); - s.set_column_value(lp_be, rational(1)); // set bde to zero s.set_column_value(lp_bde, rational(0)); @@ -1217,10 +1209,33 @@ void solver::test_basic_lemma_for_mon_zero_from_monomial_to_factors() { SASSERT(nla.m_imp->test_check(lemma, exp) == l_false); nla.m_imp->print_explanation_and_lemma(std::cout << "expl & lemma: "); + + ineq i0(lp::lconstraint_kind::EQ, lp::lar_term(), rational(0)); + i0.m_term.add_coeff_var(lp_b); + ineq i1(lp::lconstraint_kind::EQ, lp::lar_term(), rational(0)); + i1.m_term.add_coeff_var(lp_d); + ineq i2(lp::lconstraint_kind::EQ, lp::lar_term(), rational(0)); + i2.m_term.add_coeff_var(lp_e); + bool found0 = false; + bool found1 = false; + bool found2 = false; + + for (const auto& k : lemma){ + if (k == i0) { + found0 = true; + } else if (k == i1) { + found1 = true; + } else if (k == i2){ + found2 = true; + } + } + + SASSERT(found0 && found1 && found2); } void solver::test_basic_lemma_for_mon_neutral_from_monomial_to_factors() { + std::cout << "test_basic_lemma_for_mon_neutral_from_monomial_to_factors\n"; lp::lar_solver s; unsigned a = 0, b = 1, c = 2, d = 3, e = 4, abcde = 5, ac = 6, bde = 7, acd = 8, be = 9; @@ -1265,15 +1280,29 @@ void solver::test_basic_lemma_for_mon_neutral_from_monomial_to_factors() { s.set_column_value(lp_acd, rational(1)); s.set_column_value(lp_be, rational(1)); - // set bde te 2, b to minus 2 + // set bde to 2, b to minus 2 s.set_column_value(lp_bde, rational(2)); s.set_column_value(lp_b, - rational(2)); - // we have bde = -b, therefore d = +-1 and c = +-1 - + // we have bde = -b, therefore d = +-1 and e = +-1 SASSERT(nla.m_imp->test_check(lemma, exp) == l_false); nla.m_imp->print_explanation_and_lemma(std::cout << "expl & lemma: "); - + ineq i0(lp::lconstraint_kind::EQ, lp::lar_term(), rational(1)); + i0.m_term.add_coeff_var(lp_b); + ineq i1(lp::lconstraint_kind::EQ, lp::lar_term(), -rational(1)); + i1.m_term.add_coeff_var(lp_b); + bool found0 = false; + bool found1 = false; + + for (const auto& k : lemma){ + if (k == i0) { + found0 = true; + } else if (k == i1) { + found1 = true; + } + } + + SASSERT(found0 && found1); } void solver::test_basic_sign_lemma() { @@ -1327,8 +1356,13 @@ void solver::test_basic_sign_lemma() { lp::explanation exp; SASSERT(nla.m_imp->test_check(lemma, exp) == l_false); - + + lp::lar_term t; + t.add_coeff_var(lp_bde); + t.add_coeff_var(lp_acd); + ineq q(lp::lconstraint_kind::EQ, t, rational(0)); + nla.m_imp->print_explanation_and_lemma(std::cout << "expl & lemma: "); - + SASSERT(q == lemma.back()); } } diff --git a/src/util/lp/nla_solver.h b/src/util/lp/nla_solver.h index a126be298..8e04458e1 100644 --- a/src/util/lp/nla_solver.h +++ b/src/util/lp/nla_solver.h @@ -29,7 +29,10 @@ struct ineq { lp::lconstraint_kind m_cmp; lp::lar_term m_term; rational m_rs; - ineq(lp::lconstraint_kind cmp, const lp::lar_term& term, const rational& rs) : m_cmp(cmp), m_term(term), m_rs(rs) {} + ineq(lp::lconstraint_kind cmp, const lp::lar_term& term, const rational& rs) : m_cmp(cmp), m_term(term), m_rs(rs) {} + bool operator==(const ineq& a) const { + return m_cmp == a.m_cmp && m_term == a.m_term && m_rs == a.m_rs; + } }; typedef vector lemma;