From d1da26e1764c5edab500cd582c4e43c92bff5da2 Mon Sep 17 00:00:00 2001 From: Lev Date: Tue, 9 Oct 2018 16:35:30 -0700 Subject: [PATCH] add a unit test for the basic sign lemma with constraints Signed-off-by: Lev --- src/test/lp/lp.cpp | 8 +++ src/util/lp/lar_solver.h | 4 ++ src/util/lp/lar_term.h | 5 -- src/util/lp/nla_solver.cpp | 136 +++++++++++++++++++++++++++++++------ src/util/lp/nla_solver.h | 2 + 5 files changed, 129 insertions(+), 26 deletions(-) diff --git a/src/test/lp/lp.cpp b/src/test/lp/lp.cpp index a4bd66d2f..db5346d79 100644 --- a/src/test/lp/lp.cpp +++ b/src/test/lp/lp.cpp @@ -1897,6 +1897,7 @@ void test_replace_column() { void setup_args_parser(argument_parser & parser) { parser.add_option_with_help_string("-nla_fact", "test nla_solver"); + parser.add_option_with_help_string("-nla_bslwct", "test_basic_sign_lemma_with_constraints"); parser.add_option_with_help_string("-hnf", "test hermite normal form"); parser.add_option_with_help_string("-gomory", "gomory"); parser.add_option_with_help_string("-intd", "test integer_domain"); @@ -3575,6 +3576,13 @@ void test_lp_local(int argn, char**argv) { return finalize(0); } + if (args_parser.option_is_used("-nla_bslwct")) { +#ifdef Z3DEBUG + nla::solver::test_basic_sign_lemma_with_constraints(); +#endif + return finalize(0); + } + if (args_parser.option_is_used("-hnf")) { #ifdef Z3DEBUG diff --git a/src/util/lp/lar_solver.h b/src/util/lp/lar_solver.h index 444e564f4..2b2438f56 100644 --- a/src/util/lp/lar_solver.h +++ b/src/util/lp/lar_solver.h @@ -144,6 +144,10 @@ public : return m_mpq_lar_core_solver.m_r_x[j]; } + void set_column_value(unsigned j, const impq& v) { + m_mpq_lar_core_solver.m_r_x[j] = v; + } + const mpq& get_column_value_rational(unsigned j) const { return m_mpq_lar_core_solver.m_r_x[j].x; } diff --git a/src/util/lp/lar_term.h b/src/util/lp/lar_term.h index 9b1f84217..4d5257a08 100644 --- a/src/util/lp/lar_term.h +++ b/src/util/lp/lar_term.h @@ -57,11 +57,6 @@ public: return m_coeffs; } - lar_term(const vector>& coeffs) { - for (const auto & p : coeffs) { - add_coeff_var(p.first, p.second); - } - } 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/util/lp/nla_solver.cpp b/src/util/lp/nla_solver.cpp index 086065f90..250ae4c4c 100644 --- a/src/util/lp/nla_solver.cpp +++ b/src/util/lp/nla_solver.cpp @@ -37,6 +37,7 @@ struct solver::imp { mono_index_with_sign() {} }; + //fields vars_equivalence m_vars_equivalence; vector m_monomials; // maps the vector of the rooted monomial vars to the list of the indices of monomials having the same rooted monomial @@ -1263,6 +1264,17 @@ struct solver::imp { } SASSERT(found_factorizations == number_of_factorizations); } + + lbool test_basic_sign_lemma_with_constraints( + vector& lemma, + lp::explanation& exp ) + { + m_lar_solver.set_status(lp::lp_status::OPTIMAL); + m_lemma = & lemma; + m_expl = & exp; + + return check(exp, lemma); + } }; // end of imp @@ -1293,27 +1305,17 @@ solver::~solver() { dealloc(m_imp); } -void solver::test_factorization() { - 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; - lpvar lp_a = s.add_var(a, true); - lpvar lp_b = s.add_var(b, true); - lpvar lp_c = s.add_var(c, true); - lpvar lp_d = s.add_var(d, true); - lpvar lp_e = s.add_var(e, true); - lpvar lp_abcde = s.add_var(abcde, true); - lpvar lp_ac = s.add_var(ac, true); - lpvar lp_bde = s.add_var(bde, true); - lpvar lp_acd = s.add_var(acd, true); - lpvar lp_be = s.add_var(be, true); - - reslimit l; - params_ref p; - solver nla(s, l, p); - - - +void create_abcde(solver & nla, + unsigned lp_a, + unsigned lp_b, + unsigned lp_c, + unsigned lp_d, + unsigned lp_e, + unsigned lp_abcde, + unsigned lp_ac, + unsigned lp_bde, + unsigned lp_acd, + unsigned lp_be) { // create monomial abcde vector vec; vec.push_back(lp_a); @@ -1349,11 +1351,103 @@ void solver::test_factorization() { vec.push_back(lp_b); vec.push_back(lp_e); nla.add_monomial(lp_be, vec.size(), vec.begin()); +} + +void solver::test_factorization() { + 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; + lpvar lp_a = s.add_var(a, true); + lpvar lp_b = s.add_var(b, true); + lpvar lp_c = s.add_var(c, true); + lpvar lp_d = s.add_var(d, true); + lpvar lp_e = s.add_var(e, true); + lpvar lp_abcde = s.add_var(abcde, true); + lpvar lp_ac = s.add_var(ac, true); + lpvar lp_bde = s.add_var(bde, true); + lpvar lp_acd = s.add_var(acd, true); + lpvar lp_be = s.add_var(be, true); + + reslimit l; + params_ref p; + solver nla(s, l, p); + + create_abcde(nla, + lp_a, + lp_b, + lp_c, + lp_d, + lp_e, + lp_abcde, + lp_ac, + lp_bde, + lp_acd, + lp_be); nla.m_imp->test_factorization(0, // 0 is the index of monomial abcde 3); // 3 is the number of expected factorizations +} +void solver::test_basic_sign_lemma_with_constraints() { + 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; + lpvar lp_a = s.add_var(a, true); + lpvar lp_b = s.add_var(b, true); + lpvar lp_c = s.add_var(c, true); + lpvar lp_d = s.add_var(d, true); + lpvar lp_e = s.add_var(e, true); + lpvar lp_abcde = s.add_var(abcde, true); + lpvar lp_ac = s.add_var(ac, true); + lpvar lp_bde = s.add_var(bde, true); + lpvar lp_acd = s.add_var(acd, true); + lpvar lp_be = s.add_var(be, true); + + reslimit l; + params_ref p; + solver nla(s, l, p); + + // make bde = -acd + + + vector> t; + + // b + a = 0 + t.push_back(std::make_pair(rational(1), lp_a)); t.push_back(std::make_pair(rational(1), lp_b)); + lpvar b_plus_a = s.add_term(t); + s.add_var_bound(b_plus_a, lp::lconstraint_kind::GE, rational::zero()); + s.add_var_bound(b_plus_a, lp::lconstraint_kind::LE, rational::zero()); + t.clear(); + // now b = -a + + // e - c = 0 + t.push_back(std::make_pair(-rational(1), lp_c)); t.push_back(std::make_pair(rational(1), lp_e)); + lpvar e_min_c = s.add_term(t); + s.add_var_bound(e_min_c, lp::lconstraint_kind::GE, rational::zero()); + s.add_var_bound(e_min_c, lp::lconstraint_kind::LE, rational::zero()); + t.clear(); + // now e = c + s.set_column_value(lp_bde, lp::impq(rational(0))); + s.set_column_value(lp_acd, lp::impq(rational(1))); + create_abcde(nla, + lp_a, + lp_b, + lp_c, + lp_d, + lp_e, + lp_abcde, + lp_ac, + lp_bde, + lp_acd, + lp_be); + vector lemma; + lp::explanation exp; + + SASSERT(nla.m_imp->test_basic_sign_lemma_with_constraints(lemma, exp) == l_false); + + nla.m_imp->print_explanation_and_lemma(std::cout << "expl & lemma: "); + } } diff --git a/src/util/lp/nla_solver.h b/src/util/lp/nla_solver.h index 1de009013..199d689e6 100644 --- a/src/util/lp/nla_solver.h +++ b/src/util/lp/nla_solver.h @@ -47,5 +47,7 @@ public: bool need_check(); lbool check(lp::explanation&, lemma&); static void test_factorization(); + static void test_basic_sign_lemma_with_constraints(); + }; }