diff --git a/src/test/lp/lp.cpp b/src/test/lp/lp.cpp index cfd9f28cf..daef87884 100644 --- a/src/test/lp/lp.cpp +++ b/src/test/lp/lp.cpp @@ -1900,6 +1900,8 @@ 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"); parser.add_option_with_help_string("-nla_bslwct", "test_basic_sign_lemma_with_constraints"); + 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"); parser.add_option_with_help_string("-gomory", "gomory"); parser.add_option_with_help_string("-intd", "test integer_domain"); @@ -3587,7 +3589,7 @@ void test_lp_local(int argn, char**argv) { if (args_parser.option_is_used("-nla_blfmz_mf")) { #ifdef Z3DEBUG - nla::solver::test_basic_lemma_for_mon_zero_from_monomial_to_factor(); + nla::solver::test_basic_lemma_for_mon_zero_from_monomial_to_factors(); #endif return finalize(0); } @@ -3599,7 +3601,20 @@ void test_lp_local(int argn, char**argv) { return finalize(0); } - + if (args_parser.option_is_used("-nla_blnt_mf")) { +#ifdef Z3DEBUG + nla::solver::test_basic_lemma_for_mon_zero_from_monomial_to_factors(); +#endif + return finalize(0); + } + + if (args_parser.option_is_used("-nla_bnt_fm")) { +#ifdef Z3DEBUG + nla::solver::test_basic_lemma_for_mon_zero_from_factors_to_monomial(); +#endif + return finalize(0); + } + if (args_parser.option_is_used("-hnf")) { #ifdef Z3DEBUG test_hnf(); diff --git a/src/util/lp/nla_solver.cpp b/src/util/lp/nla_solver.cpp index 7391fca61..89aff4d26 100644 --- a/src/util/lp/nla_solver.cpp +++ b/src/util/lp/nla_solver.cpp @@ -1104,18 +1104,28 @@ struct solver::imp { } - bool basic_lemma_for_mon_zero(lpvar i_mon, const factorization& factorization) { + bool basic_lemma_for_mon_zero(unsigned i_mon, const factorization& factorization) { return basic_lemma_for_mon_zero_from_monomial_to_factor(i_mon, factorization) || basic_lemma_for_mon_zero_from_factors_to_monomial(i_mon, factorization); } - - bool basic_lemma_for_mon_neutral(const factorization& factorization) { - // NOT_IMPLEMENTED_YET(); + + bool basic_lemma_for_mon_neutral_monomial_to_factor(unsigned i_mon, const factorization& factorization) { + return false; + } + + bool basic_lemma_for_mon_neutral_from_factors_to_monomial(unsigned i_mon, const factorization& factorization) { + return false; + } + + bool basic_lemma_for_mon_neutral(unsigned i_mon, const factorization& factorization) { + return + basic_lemma_for_mon_neutral_monomial_to_factor(i_mon, factorization) || + basic_lemma_for_mon_neutral_from_factors_to_monomial(i_mon, factorization); return false; } - bool basic_lemma_for_mon_proportionality(const factorization& factorization) { + bool basic_lemma_for_mon_proportionality(unsigned i_mon, const factorization& factorization) { // NOT_IMPLEMENTED_YET(); return false; } @@ -1125,8 +1135,8 @@ struct solver::imp { bool basic_lemma_for_mon(unsigned i_mon) { for (auto factorization : factorization_factory_imp(i_mon, *this)) { if (basic_lemma_for_mon_zero(i_mon, factorization) || - basic_lemma_for_mon_neutral(factorization) || - basic_lemma_for_mon_proportionality(factorization)) + basic_lemma_for_mon_neutral(i_mon, factorization) || + basic_lemma_for_mon_proportionality(i_mon, factorization)) return true; } @@ -1295,29 +1305,7 @@ 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); - } - - lbool test_basic_lemma_for_mon_zero_from_monomial_to_factor( - vector& lemma, - lp::explanation& exp ) - { - m_lar_solver.set_status(lp::lp_status::OPTIMAL); - m_lemma = & lemma; - m_expl = & exp; - - return check(exp, lemma); - } - - lbool test_basic_lemma_for_mon_zero_from_factors_to_monomial( + lbool test_check( vector& lemma, lp::explanation& exp ) { @@ -1442,7 +1430,7 @@ void solver::test_factorization() { } -void solver::test_basic_lemma_for_mon_zero_from_monomial_to_factor() { +void solver::test_basic_lemma_for_mon_neutral_from_factors_to_monomial() { 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; @@ -1491,7 +1479,7 @@ void solver::test_basic_lemma_for_mon_zero_from_monomial_to_factor() { // set bde to zero s.set_column_value(lp_bde, rational(0)); - SASSERT(nla.m_imp->test_basic_lemma_for_mon_zero_from_monomial_to_factor(lemma, exp) == l_false); + SASSERT(nla.m_imp->test_check(lemma, exp) == l_false); nla.m_imp->print_explanation_and_lemma(std::cout << "expl & lemma: "); @@ -1530,6 +1518,116 @@ void solver::test_basic_lemma_for_mon_zero_from_factors_to_monomial() { vector lemma; lp::explanation exp; + + // set all vars to 1 + s.set_column_value(lp_a, rational(1)); + s.set_column_value(lp_b, rational(1)); + s.set_column_value(lp_c, rational(1)); + s.set_column_value(lp_d, rational(1)); + s.set_column_value(lp_e, rational(1)); + s.set_column_value(lp_abcde, rational(1)); + s.set_column_value(lp_ac, rational(1)); + s.set_column_value(lp_bde, rational(1)); + s.set_column_value(lp_acd, rational(1)); + s.set_column_value(lp_be, rational(1)); + + // set bde to zero + s.set_column_value(lp_bde, rational(0)); + + SASSERT(nla.m_imp->test_check(lemma, exp) == l_false); + + nla.m_imp->print_explanation_and_lemma(std::cout << "expl & lemma: "); + +} + +void solver::test_basic_lemma_for_mon_zero_from_monomial_to_factors() { + 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); + vector lemma; + lp::explanation exp; + + + // set all vars to 1 + s.set_column_value(lp_a, rational(1)); + s.set_column_value(lp_b, rational(1)); + s.set_column_value(lp_c, rational(1)); + s.set_column_value(lp_d, rational(1)); + s.set_column_value(lp_e, rational(1)); + s.set_column_value(lp_abcde, rational(1)); + s.set_column_value(lp_ac, rational(1)); + s.set_column_value(lp_bde, rational(1)); + s.set_column_value(lp_acd, rational(1)); + s.set_column_value(lp_be, rational(1)); + + // set bde to zero + s.set_column_value(lp_bde, rational(0)); + + SASSERT(nla.m_imp->test_check(lemma, exp) == l_false); + + nla.m_imp->print_explanation_and_lemma(std::cout << "expl & lemma: "); + +} + +void solver::test_basic_lemma_for_mon_neutral_from_monomial_to_factors() { + 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); + vector lemma; + lp::explanation exp; + // set all vars to 0 s.set_column_value(lp_a, rational(0)); s.set_column_value(lp_b, rational(0)); @@ -1542,10 +1640,12 @@ void solver::test_basic_lemma_for_mon_zero_from_factors_to_monomial() { s.set_column_value(lp_acd, rational(0)); s.set_column_value(lp_be, rational(0)); - // set bde to one + // set bde, b, and e to one s.set_column_value(lp_bde, rational(1)); + s.set_column_value(lp_b, rational(1)); + s.set_column_value(lp_e, rational(1)); - SASSERT(nla.m_imp->test_basic_lemma_for_mon_zero_from_factors_to_monomial(lemma, exp) == l_false); + SASSERT(nla.m_imp->test_check(lemma, exp) == l_false); nla.m_imp->print_explanation_and_lemma(std::cout << "expl & lemma: "); @@ -1606,7 +1706,7 @@ void solver::test_basic_sign_lemma_with_constraints() { vector lemma; lp::explanation exp; - SASSERT(nla.m_imp->test_basic_sign_lemma_with_constraints(lemma, exp) == l_false); + SASSERT(nla.m_imp->test_check(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 0f3ff27a5..e65974e86 100644 --- a/src/util/lp/nla_solver.h +++ b/src/util/lp/nla_solver.h @@ -48,7 +48,9 @@ public: lbool check(lp::explanation&, lemma&); static void test_factorization(); static void test_basic_sign_lemma_with_constraints(); - static void test_basic_lemma_for_mon_zero_from_monomial_to_factor(); + static void test_basic_lemma_for_mon_zero_from_monomial_to_factors(); static void test_basic_lemma_for_mon_zero_from_factors_to_monomial(); + static void test_basic_lemma_for_mon_neutral_from_monomial_to_factors(); + static void test_basic_lemma_for_mon_neutral_from_factors_to_monomial(); }; }