mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

remove a test

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-04-16 14:06:49 -07:00
parent be5170fc3b
commit 14f00b3749
4 changed files with 1 additions and 72 deletions
Download patch file Download diff file Expand all files Collapse all files

13
src/test/lp/lp.cpp
View file

@ -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();

37
src/test/lp/nla_solver_test.cpp
View file

@ -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";

21
src/util/lp/nla_core.cpp
View file

@ -2194,26 +2194,7 @@ bool core:: no_lemmas_hold() const {
return true;
}
void core::test_factorization(unsigned /*mon_index*/, unsigned /*number_of_factorizations*/) {
// vector<ineq> 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<lemma>& l) {
m_lar_solver.set_status(lp::lp_status::OPTIMAL);
return check(l);

2
src/util/lp/nla_core.h
View file

@ -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<lemma>& l);
}; // end of core
} // end of namespace nla