From 14f00b37496eacf17f5adc91d380ad02d4394891 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 16 Apr 2019 14:06:49 -0700 Subject: [PATCH] remove a test Signed-off-by: Lev Nachmanson --- src/test/lp/lp.cpp | 13 ------------ src/test/lp/nla_solver_test.cpp | 37 --------------------------------- src/util/lp/nla_core.cpp | 21 +------------------ src/util/lp/nla_core.h | 2 -- 4 files changed, 1 insertion(+), 72 deletions(-) diff --git a/src/test/lp/lp.cpp b/src/test/lp/lp.cpp index 49a8a2d28..01a9f16c6 100644 --- a/src/test/lp/lp.cpp +++ b/src/test/lp/lp.cpp @@ -56,7 +56,6 @@ #include "util/lp/bound_propagator.h" #include "util/lp/nla_solver.h" namespace nla { -void test_factorization(); void test_order_lemma(); void test_monotone_lemma(); void test_basic_sign_lemma(); @@ -1910,7 +1909,6 @@ void test_replace_column() { void setup_args_parser(argument_parser & parser) { parser.add_option_with_help_string("-nla_blfmz_mf", "test_basic_lemma_for_mon_zero_from_factor_to_monomial"); 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_tan", "test_tangent_lemma"); @@ -3568,10 +3566,6 @@ void test_gomory_cut() { test_gomory_cut_1(); } -void test_nla_factorization() { - nla::test_factorization(); -} - void test_nla_order_lemma() { nla::test_order_lemma(); } @@ -3592,13 +3586,6 @@ void test_lp_local(int argn, char**argv) { args_parser.print(); - if (args_parser.option_is_used("-nla_fact")) { -#ifdef Z3DEBUG - test_nla_factorization(); -#endif - return finalize(0); - } - if (args_parser.option_is_used("-nla_order")) { #ifdef Z3DEBUG test_nla_order_lemma(); diff --git a/src/test/lp/nla_solver_test.cpp b/src/test/lp/nla_solver_test.cpp index 5c92dc054..0363c58de 100644 --- a/src/test/lp/nla_solver_test.cpp +++ b/src/test/lp/nla_solver_test.cpp @@ -67,43 +67,6 @@ void create_abcde(solver & nla, nla.add_monomial(lp_be, vec.size(), vec.begin()); } -void 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_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_abcde = s.add_named_var(abcde, true, "abcde"); - lpvar lp_ac = s.add_named_var(ac, true, "ac"); - lpvar lp_bde = s.add_named_var(bde, true, "bde"); - lpvar lp_acd = s.add_named_var(acd, true, "acd"); - lpvar lp_be = s.add_named_var(be, true, "be"); - - solver nla(s); - - create_abcde(nla, - lp_a, - lp_b, - lp_c, - lp_d, - lp_e, - lp_abcde, - lp_ac, - lp_bde, - lp_acd, - lp_be); - nla.get_core()->register_monomials_in_tables(); - nla.get_core()->print_monomials(std::cout); - nla.get_core()->test_factorization(1, // 0 is the index of monomial abcde - 1); // 3 is the number of expected factorizations - nla.get_core()->test_factorization(0, // 0 is the index of monomial abcde - 3); // 3 is the number of expected factorizations - - -} void test_basic_lemma_for_mon_neutral_from_factors_to_monomial_0() { std::cout << "test_basic_lemma_for_mon_neutral_from_factors_to_monomial_0\n"; diff --git a/src/util/lp/nla_core.cpp b/src/util/lp/nla_core.cpp index 910414414..0f862da28 100644 --- a/src/util/lp/nla_core.cpp +++ b/src/util/lp/nla_core.cpp @@ -2194,26 +2194,7 @@ bool core:: no_lemmas_hold() const { return true; } -void core::test_factorization(unsigned /*mon_index*/, unsigned /*number_of_factorizations*/) { - // vector lemma; - - // unsigned_vector vars = m_monomials[mon_index].vars(); - - // factorization_factory_imp fc(vars, // 0 is the index of "abcde" - // *this); - - // std::cout << "factorizations = of "; print_monomial(m_monomials[mon_index], std::cout) << "\n"; - // unsigned found_factorizations = 0; - // for (auto f : fc) { - // if (f.is_empty()) continue; - // found_factorizations ++; - // print_factorization(f, std::cout); - // std::cout << std::endl; - // } - // SASSERT(found_factorizations == number_of_factorizations); -} - -lbool core:: test_check( +lbool core::test_check( vector& l) { m_lar_solver.set_status(lp::lp_status::OPTIMAL); return check(l); diff --git a/src/util/lp/nla_core.h b/src/util/lp/nla_core.h index d9fa7a576..d89dbab02 100644 --- a/src/util/lp/nla_core.h +++ b/src/util/lp/nla_core.h @@ -354,8 +354,6 @@ struct core { bool no_lemmas_hold() const; - void test_factorization(unsigned /*mon_index*/, unsigned /*number_of_factorizations*/); - lbool test_check(vector& l); }; // end of core } // end of namespace nla