From ea02231ef883fb2232ea04da0efd60b200f9464e Mon Sep 17 00:00:00 2001 From: Lev Date: Sat, 22 Dec 2018 10:21:37 -0800 Subject: [PATCH] create a test for order lemma Signed-off-by: Lev --- src/test/lp/lp.cpp | 8 +++++ src/util/lp/nla_solver.cpp | 68 ++++++++++++++++++++++++++++++++++++++ src/util/lp/nla_solver.h | 1 + 3 files changed, 77 insertions(+) diff --git a/src/test/lp/lp.cpp b/src/test/lp/lp.cpp index e023017b2..02e17dd23 100644 --- a/src/test/lp/lp.cpp +++ b/src/test/lp/lp.cpp @@ -1900,6 +1900,7 @@ void setup_args_parser(argument_parser & parser) { parser.add_option_with_help_string("-nla_blfmz_fm", "test_basic_lemma_for_mon_zero_from_monomials_to_factor"); parser.add_option_with_help_string("-nla_fact", "test nla_solver factorization"); parser.add_option_with_help_string("-nla_order", "test nla_solver order lemma"); + parser.add_option_with_help_string("-nla_monot", "test nla_solver order lemma"); parser.add_option_with_help_string("-nla_bsl", "test_basic_sign_lemma"); parser.add_option_with_help_string("-nla_blnt_mf", "test_basic_lemma_for_mon_neutral_from_monomial_to_factors"); parser.add_option_with_help_string("-nla_blnt_fm", "test_basic_lemma_for_mon_neutral_from_factors_to_monomial"); @@ -3597,6 +3598,13 @@ void test_lp_local(int argn, char**argv) { } + if (args_parser.option_is_used("-nla_monot")) { +#ifdef Z3DEBUG + nla::solver::test_monotone_lemma(); +#endif + return finalize(0); + } + if (args_parser.option_is_used("-nla_bsl")) { #ifdef Z3DEBUG nla::solver::test_basic_sign_lemma(); diff --git a/src/util/lp/nla_solver.cpp b/src/util/lp/nla_solver.cpp index af68be743..b16cea0e1 100644 --- a/src/util/lp/nla_solver.cpp +++ b/src/util/lp/nla_solver.cpp @@ -2257,6 +2257,74 @@ void solver::test_order_lemma_params(bool var_equiv, int sign) { // SASSERT(found); } +void solver::test_monotone_lemma() { + enable_trace("nla_solver"); + lp::lar_solver s; + unsigned a = 0, b = 1, c = 2, d = 3, e = 4, f = 5, + i = 8, j = 9, + ab = 10, cd = 11, ef = 12, ij = 17; + + lpvar lp_a = s.add_named_var(a, true, "a"); + lpvar lp_b = s.add_named_var(b, true, "b"); + lpvar lp_c = s.add_named_var(c, true, "c"); + lpvar lp_d = s.add_named_var(d, true, "d"); + lpvar lp_e = s.add_named_var(e, true, "e"); + lpvar lp_f = s.add_named_var(f, true, "f"); + lpvar lp_i = s.add_named_var(i, true, "i"); + lpvar lp_j = s.add_named_var(j, true, "j"); + lpvar lp_ab = s.add_named_var(ab, true, "ab"); + lpvar lp_cd = s.add_named_var(cd, true, "cd"); + lpvar lp_ef = s.add_named_var(ef, true, "ef"); + lpvar lp_ij = s.add_named_var(ij, true, "ij"); + // lpvar lp_abef = s.add_named_var(abef, true, "abef"); + for (unsigned j = 0; j < s.number_of_vars(); j++) { + s.set_column_value(j, rational((j + 2)*(j + 2))); + } + + reslimit l; + params_ref p; + solver nla(s, l, p); + // create monomial ab + vector vec; + vec.push_back(lp_a); + vec.push_back(lp_b); + int mon_ab = nla.add_monomial(lp_ab, vec.size(), vec.begin()); + // create monomial cd + vec.clear(); + vec.push_back(lp_c); + vec.push_back(lp_d); + int mon_cd = nla.add_monomial(lp_cd, vec.size(), vec.begin()); + // create monomial ef + vec.clear(); + vec.push_back(lp_e); + vec.push_back(lp_f); + nla.add_monomial(lp_ef, vec.size(), vec.begin()); + // create monomial ij + vec.clear(); + vec.push_back(lp_i); + vec.push_back(lp_j); + int mon_ij = nla.add_monomial(lp_ij, vec.size(), vec.begin()); + + // set e == i + 1 + s.set_column_value(lp_e, s.get_column_value(lp_i) + rational(1)); + // set f == j + 1 + s.set_column_value(lp_f, s.get_column_value(lp_j) + rational(1)); + // set the values of ab, ef, cd, and ij correctly + s.set_column_value(lp_ab, nla.m_imp->mon_value_by_vars(mon_ab)); + s.set_column_value(lp_cd, nla.m_imp->mon_value_by_vars(mon_cd)); + s.set_column_value(lp_ij, nla.m_imp->mon_value_by_vars(mon_ij)); + + // set ef = ij while it has to be ef > ij + s.set_column_value(lp_ef, s.get_column_value(lp_ij)); + + vector lemma; + lp::explanation exp; + + SASSERT(nla.m_imp->test_check(lemma, exp) == l_false); + + nla.m_imp->print_lemma(std::cout << "lemma: "); +} + void solver::test_order_lemma() { test_order_lemma_params(false, 1); test_order_lemma_params(false, -1); diff --git a/src/util/lp/nla_solver.h b/src/util/lp/nla_solver.h index edd6101a2..d6464ad9d 100644 --- a/src/util/lp/nla_solver.h +++ b/src/util/lp/nla_solver.h @@ -73,5 +73,6 @@ public: static void test_basic_lemma_for_mon_neutral_from_factors_to_monomial_1(); static void test_order_lemma(); static void test_order_lemma_params(bool, int sign); + static void test_monotone_lemma(); }; }