From 6e000547e32e251226306ebcd3938e599fe60385 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 24 Jul 2019 15:59:08 -0700 Subject: [PATCH] work on test of horner's heuristic Signed-off-by: Lev Nachmanson --- src/test/lp/lp.cpp | 28 ++++++++++----- src/test/lp/nla_solver_test.cpp | 61 +++++++++++++++++++++++++-------- 2 files changed, 66 insertions(+), 23 deletions(-) diff --git a/src/test/lp/lp.cpp b/src/test/lp/lp.cpp index b3d7603e0..d523faa1c 100644 --- a/src/test/lp/lp.cpp +++ b/src/test/lp/lp.cpp @@ -58,6 +58,7 @@ #include "math/lp/horner.h" #include "math/lp/cross_nested.h" namespace nla { +void test_horner(); void test_order_lemma(); void test_monotone_lemma(); void test_basic_sign_lemma(); @@ -80,16 +81,17 @@ void test_cn() { enable_trace("nla_cn"); // enable_trace("nla_cn_details"); nex a = nex::var(0), b = nex::var(1), c = nex::var(2), d = nex::var(3), e = nex::var(4); - //test_cn_on_expr(a*b + a*c + b*c); - //TRACE("nla_cn", tout << "done\n";); + nex min_1 = nex::scalar(rational(-1)); + test_cn_on_expr(min_1*c*e + min_1*b*d + min_1*a*b + a*c); + TRACE("nla_cn", tout << "done\n";); + test_cn_on_expr(a*a*d + a*b*c*d + a*a*c*c*d + a*d*d + e*a*e + e*a*c + e*d); - TRACE("nla_cn", tout << "done\n";); - test_cn_on_expr(a*b*d + a*b*c + c*b*d + a*c*d); - TRACE("nla_cn", tout << "done\n";); - test_cn_on_expr(a*b*b*d*d + a*b*b*c*d + c*b*b*d); - TRACE("nla_cn", tout << "done\n";); - test_cn_on_expr(a*b*d + a*b*c + c*b*d); - + // TRACE("nla_cn", tout << "done\n";); + // test_cn_on_expr(a*b*d + a*b*c + c*b*d + a*c*d); + // TRACE("nla_cn", tout << "done\n";); + // test_cn_on_expr(a*b*b*d*d + a*b*b*c*d + c*b*b*d); + // TRACE("nla_cn", tout << "done\n";); + // test_cn_on_expr(a*b*d + a*b*c + c*b*d); } } // end of namespace nla @@ -1942,6 +1944,7 @@ void setup_args_parser(argument_parser & parser) { parser.add_option_with_help_string("-nla_monot", "test nla_solver order lemma"); parser.add_option_with_help_string("-nla_tan", "test_tangent_lemma"); parser.add_option_with_help_string("-nla_bsl", "test_basic_sign_lemma"); + parser.add_option_with_help_string("-horner", "test horner's heuristic"); 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"); parser.add_option_with_help_string("-hnf", "test hermite normal form"); @@ -3645,6 +3648,13 @@ void test_lp_local(int argn, char**argv) { return finalize(0); } + if (args_parser.option_is_used("-nla_horner")) { +#ifdef Z3DEBUG + nla::test_horner(); +#endif + return finalize(0); + } + if (args_parser.option_is_used("-nla_tan")) { #ifdef Z3DEBUG nla::test_tangent_lemma(); diff --git a/src/test/lp/nla_solver_test.cpp b/src/test/lp/nla_solver_test.cpp index fcaa6b2d6..b24965b89 100644 --- a/src/test/lp/nla_solver_test.cpp +++ b/src/test/lp/nla_solver_test.cpp @@ -410,6 +410,51 @@ void test_basic_lemma_for_mon_neutral_from_monomial_to_factors() { SASSERT(found0 && found1); } +void test_horner() { + enable_trace("nla_solver"); + lp::lar_solver s; + unsigned a = 0, b = 1, c = 2, d = 3, e = 4, + ce = 5, bd = 6, ab = 7, ac = 8, c_min_b = 9; + + 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_ab = s.add_named_var(ab, true, "ab"); + lpvar lp_ce = s.add_named_var(ce, true, "ce"); + lpvar lp_bd = s.add_named_var(bd, true, "ab"); + lpvar lp_ac = s.add_named_var(ac, true, "ce"); + + lp::lar_term t; + t.add_var(lp_c); + t.add_coeff_var(rational(-1), lp_b); + lpvar lp_c_min_b = s.add_term(t.coeffs_as_vector(), c_min_b); + + reslimit l; + params_ref p; + solver nla(s); + vector v; + v.push_back(a); v.push_back(b); + nla.add_monomial(lp_ab, v.size(), v.begin()); + v.clear(); + + v.push_back(c); v.push_back(e); + nla.add_monomial(lp_ce, v.size(), v.begin()); + v.clear(); + + v.push_back(b); v.push_back(d); + nla.add_monomial(lp_bd, v.size(), v.begin()); + v.clear(); + + v.push_back(a); v.push_back(c); + nla.add_monomial(lp_ac, v.size(), v.begin()); + v.clear(); + + + + +} void test_basic_sign_lemma() { enable_trace("nla_solver"); lp::lar_solver s; @@ -458,8 +503,8 @@ void test_basic_sign_lemma() { s_set_column_value(s, lp_bde, rational(5)); s_set_column_value(s, lp_acd, rational(3)); - vector lemma; - SASSERT(nla.get_core()->test_check(lemma) == l_false); + vector lemmas; + SASSERT(nla.get_core()->test_check(lemmas) == l_false); lp::lar_term t; t.add_var(lp_bde); @@ -467,18 +512,6 @@ void test_basic_sign_lemma() { ineq q(llc::EQ, t, rational(0)); nla.get_core()->print_lemma(std::cout); - SASSERT(q == lemma[0].ineqs().back()); - ineq i0(llc::EQ, lp::lar_term(), rational(0)); - i0.m_term.add_var(lp_bde); - i0.m_term.add_var(lp_acd); - bool found = false; - for (const auto& k : lemma[0].ineqs()){ - if (k == i0) { - found = true; - } - } - - SASSERT(found); } void test_order_lemma_params(bool var_equiv, int sign) {