From 48fcd66bb97cce892ff220f75748542b37ad5423 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 16 Apr 2019 14:03:09 -0700 Subject: [PATCH] refactor tests from nla_solver Signed-off-by: Lev Nachmanson --- src/test/lp/CMakeLists.txt | 2 +- src/test/lp/lp.cpp | 30 +- src/test/lp/nla_solver_test.cpp | 815 ++++++++++++++++++++++++++++++++ src/util/lp/nla_solver.cpp | 793 ------------------------------- src/util/lp/nla_solver.h | 17 +- 5 files changed, 838 insertions(+), 819 deletions(-) create mode 100644 src/test/lp/nla_solver_test.cpp diff --git a/src/test/lp/CMakeLists.txt b/src/test/lp/CMakeLists.txt index 32d55bca8..e2873102d 100644 --- a/src/test/lp/CMakeLists.txt +++ b/src/test/lp/CMakeLists.txt @@ -1,6 +1,6 @@ add_executable(lp_tst EXCLUDE_FROM_ALL -lp_main.cpp lp.cpp $ $ $ $ ) +lp_main.cpp lp.cpp nla_solver_test.cpp $ $ $ $ ) target_compile_definitions(lp_tst PRIVATE ${Z3_COMPONENT_CXX_DEFINES}) target_compile_options(lp_tst PRIVATE ${Z3_COMPONENT_CXX_FLAGS}) target_include_directories(lp_tst PRIVATE ${Z3_COMPONENT_EXTRA_INCLUDE_DIRS}) diff --git a/src/test/lp/lp.cpp b/src/test/lp/lp.cpp index 155819287..49a8a2d28 100644 --- a/src/test/lp/lp.cpp +++ b/src/test/lp/lp.cpp @@ -55,6 +55,18 @@ #include "util/lp/general_matrix.h" #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(); +void test_tangent_lemma(); +void test_basic_lemma_for_mon_zero_from_monomial_to_factors(); +void test_basic_lemma_for_mon_zero_from_factors_to_monomial(); +void test_basic_lemma_for_mon_neutral_from_monomial_to_factors(); +void test_basic_lemma_for_mon_neutral_from_factors_to_monomial(); +} + namespace lp { unsigned seed = 1; @@ -3557,11 +3569,11 @@ void test_gomory_cut() { } void test_nla_factorization() { - nla::solver::test_factorization(); + nla::test_factorization(); } void test_nla_order_lemma() { - nla::solver::test_order_lemma(); + nla::test_order_lemma(); } void test_lp_local(int argn, char**argv) { @@ -3597,49 +3609,49 @@ void test_lp_local(int argn, char**argv) { if (args_parser.option_is_used("-nla_monot")) { #ifdef Z3DEBUG - nla::solver::test_monotone_lemma(); + nla::test_monotone_lemma(); #endif return finalize(0); } if (args_parser.option_is_used("-nla_bsl")) { #ifdef Z3DEBUG - nla::solver::test_basic_sign_lemma(); + nla::test_basic_sign_lemma(); #endif return finalize(0); } if (args_parser.option_is_used("-nla_tan")) { #ifdef Z3DEBUG - nla::solver::test_tangent_lemma(); + nla::test_tangent_lemma(); #endif return finalize(0); } if (args_parser.option_is_used("-nla_blfmz_mf")) { #ifdef Z3DEBUG - nla::solver::test_basic_lemma_for_mon_zero_from_monomial_to_factors(); + nla::test_basic_lemma_for_mon_zero_from_monomial_to_factors(); #endif return finalize(0); } if (args_parser.option_is_used("-nla_blfmz_fm")) { #ifdef Z3DEBUG - nla::solver::test_basic_lemma_for_mon_zero_from_factors_to_monomial(); + nla::test_basic_lemma_for_mon_zero_from_factors_to_monomial(); #endif return finalize(0); } if (args_parser.option_is_used("-nla_blnt_mf")) { #ifdef Z3DEBUG - nla::solver::test_basic_lemma_for_mon_neutral_from_monomial_to_factors(); + nla::test_basic_lemma_for_mon_neutral_from_monomial_to_factors(); #endif return finalize(0); } if (args_parser.option_is_used("-nla_blnt_fm")) { #ifdef Z3DEBUG - nla::solver::test_basic_lemma_for_mon_neutral_from_factors_to_monomial(); + nla::test_basic_lemma_for_mon_neutral_from_factors_to_monomial(); #endif return finalize(0); } diff --git a/src/test/lp/nla_solver_test.cpp b/src/test/lp/nla_solver_test.cpp new file mode 100644 index 000000000..5c92dc054 --- /dev/null +++ b/src/test/lp/nla_solver_test.cpp @@ -0,0 +1,815 @@ +/*++ +Copyright (c) 2017 Microsoft Corporation + +Module Name: + + + +Abstract: + + + +Author: + Nikolaj Bjorner (nbjorner) + Lev Nachmanson (levnach) + +Revision History: + + +--*/ +#include "util/lp/nla_solver.h" +namespace nla { +void create_abcde(solver & nla, + unsigned lp_a, + unsigned lp_b, + unsigned lp_c, + unsigned lp_d, + unsigned lp_e, + unsigned lp_abcde, + unsigned lp_ac, + unsigned lp_bde, + unsigned lp_acd, + unsigned lp_be) { + // create monomial abcde + vector vec; + vec.push_back(lp_a); + vec.push_back(lp_b); + vec.push_back(lp_c); + vec.push_back(lp_d); + vec.push_back(lp_e); + + nla.add_monomial(lp_abcde, vec.size(), vec.begin()); + + // create monomial ac + vec.clear(); + vec.push_back(lp_a); + vec.push_back(lp_c); + nla.add_monomial(lp_ac, vec.size(), vec.begin()); + + // create monomial bde + vec.clear(); + vec.push_back(lp_b); + vec.push_back(lp_d); + vec.push_back(lp_e); + nla.add_monomial(lp_bde, vec.size(), vec.begin()); + + // create monomial acd + vec.clear(); + vec.push_back(lp_a); + vec.push_back(lp_c); + vec.push_back(lp_d); + nla.add_monomial(lp_acd, vec.size(), vec.begin()); + + // create monomial be + vec.clear(); + vec.push_back(lp_b); + vec.push_back(lp_e); + 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"; + enable_trace("nla_solver"); + TRACE("nla_solver",); + lp::lar_solver s; + unsigned a = 0, b = 1, c = 2, d = 3, e = 4, + abcde = 5, ac = 6, bde = 7; + 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"); + + reslimit l; + params_ref p; + solver nla(s); + svector v; v.push_back(lp_b);v.push_back(lp_d);v.push_back(lp_e); + nla.add_monomial(lp_bde, v.size(), v.begin()); + v.clear(); + v.push_back(lp_a);v.push_back(lp_b);v.push_back(lp_c);v.push_back(lp_d);v.push_back(lp_e); + nla.add_monomial(lp_abcde, v.size(), v.begin()); + v.clear(); + v.push_back(lp_a);v.push_back(lp_c); + nla.add_monomial(lp_ac, v.size(), v.begin()); + + vector lv; + + // set abcde = ac * bde + // ac = 1 then abcde = bde, but we have abcde < bde + s.set_column_value(lp_a, lp::impq(rational(4))); + s.set_column_value(lp_b, lp::impq(rational(4))); + s.set_column_value(lp_c, lp::impq(rational(4))); + s.set_column_value(lp_d, lp::impq(rational(4))); + s.set_column_value(lp_e, lp::impq(rational(4))); + s.set_column_value(lp_abcde, lp::impq(rational(15))); + s.set_column_value(lp_ac, lp::impq(rational(1))); + s.set_column_value(lp_bde, lp::impq(rational(16))); + + + SASSERT(nla.get_core()->test_check(lv) == l_false); + + nla.get_core()->print_lemma(std::cout); + + ineq i0(llc::NE, lp::lar_term(), rational(1)); + i0.m_term.add_var(lp_ac); + ineq i1(llc::EQ, lp::lar_term(), rational(0)); + i1.m_term.add_var(lp_bde); + i1.m_term.add_coeff_var(-rational(1), lp_abcde); + ineq i2(llc::EQ, lp::lar_term(), rational(0)); + i2.m_term.add_var(lp_abcde); + i2.m_term.add_coeff_var(-rational(1), lp_bde); + bool found0 = false; + bool found1 = false; + bool found2 = false; + for (const auto& k : lv[0].ineqs()){ + if (k == i0) { + found0 = true; + } else if (k == i1) { + found1 = true; + } else if (k == i2) { + found2 = true; + } + } + + SASSERT(found0 && (found1 || found2)); + + +} + +void s_set_column_value(lp::lar_solver&s, lpvar j, const rational & v) { + s.set_column_value(j, lp::impq(v)); +} + +void s_set_column_value(lp::lar_solver&s, lpvar j, const lp::impq & v) { + s.set_column_value(j, v); +} + +void test_basic_lemma_for_mon_neutral_from_factors_to_monomial_1() { + std::cout << "test_basic_lemma_for_mon_neutral_from_factors_to_monomial_1\n"; + TRACE("nla_solver",); + lp::lar_solver s; + unsigned a = 0, b = 1, c = 2, d = 3, e = 4, + bde = 7; + 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_bde = s.add_var(bde, true); + + reslimit l; + params_ref p; + solver nla(s); + svector v; v.push_back(lp_b);v.push_back(lp_d);v.push_back(lp_e); + nla.add_monomial(lp_bde, v.size(), v.begin()); + + vector lemma; + + s_set_column_value(s, lp_a, rational(1)); + s_set_column_value(s, lp_b, rational(1)); + s_set_column_value(s, lp_c, rational(1)); + s_set_column_value(s, lp_d, rational(1)); + s_set_column_value(s, lp_e, rational(1)); + s_set_column_value(s, lp_bde, rational(3)); + + SASSERT(nla.get_core()->test_check(lemma) == l_false); + SASSERT(lemma[0].size() == 4); + nla.get_core()->print_lemma(std::cout); + + ineq i0(llc::NE, lp::lar_term(), rational(1)); + i0.m_term.add_var(lp_b); + ineq i1(llc::NE, lp::lar_term(), rational(1)); + i1.m_term.add_var(lp_d); + ineq i2(llc::NE, lp::lar_term(), rational(1)); + i2.m_term.add_var(lp_e); + ineq i3(llc::EQ, lp::lar_term(), rational(1)); + i3.m_term.add_var(lp_bde); + bool found0 = false; + bool found1 = false; + bool found2 = false; + bool found3 = false; + for (const auto& k : lemma[0].ineqs()){ + if (k == i0) { + found0 = true; + } else if (k == i1) { + found1 = true; + } else if (k == i2) { + found2 = true; + } else if (k == i3) { + found3 = true; + } + + } + + SASSERT(found0 && found1 && found2 && found3); + +} +void test_basic_lemma_for_mon_neutral_from_factors_to_monomial() { + test_basic_lemma_for_mon_neutral_from_factors_to_monomial_0(); + test_basic_lemma_for_mon_neutral_from_factors_to_monomial_1(); +} + + +void test_basic_lemma_for_mon_zero_from_factors_to_monomial() { + std::cout << "test_basic_lemma_for_mon_zero_from_factors_to_monomial\n"; + enable_trace("nla_solver"); + 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"); + + reslimit l; + params_ref p; + 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); + vector lemma; + + // set vars + s_set_column_value(s, lp_a, rational(1)); + s_set_column_value(s, lp_b, rational(0)); + s_set_column_value(s, lp_c, rational(1)); + s_set_column_value(s, lp_d, rational(1)); + s_set_column_value(s, lp_e, rational(1)); + s_set_column_value(s, lp_abcde, rational(0)); + s_set_column_value(s, lp_ac, rational(1)); + s_set_column_value(s, lp_bde, rational(0)); + s_set_column_value(s, lp_acd, rational(1)); + s_set_column_value(s, lp_be, rational(1)); + + SASSERT(nla.get_core()->test_check(lemma) == l_false); + nla.get_core()->print_lemma(std::cout); + SASSERT(lemma.size() == 1 && lemma[0].size() == 2); + ineq i0(llc::NE, lp::lar_term(), rational(0)); + i0.m_term.add_var(lp_b); + ineq i1(llc::EQ, lp::lar_term(), rational(0)); + i1.m_term.add_var(lp_be); + bool found0 = false; + bool found1 = false; + + for (const auto& k : lemma[0].ineqs()){ + if (k == i0) { + found0 = true; + } else if (k == i1) { + found1 = true; + } + } + + SASSERT(found0 && found1); +} + +void test_basic_lemma_for_mon_zero_from_monomial_to_factors() { + std::cout << "test_basic_lemma_for_mon_zero_from_monomial_to_factors\n"; + enable_trace("nla_solver"); + lp::lar_solver s; + unsigned a = 0, c = 2, d = 3, acd = 8; + lpvar lp_a = s.add_named_var(a, true, "a"); + lpvar lp_c = s.add_named_var(c, true, "c"); + lpvar lp_d = s.add_named_var(d, true, "d"); + lpvar lp_acd = s.add_named_var(acd, true, "acd"); + + reslimit l; + params_ref p; + solver nla(s); + + // create monomial acd + unsigned_vector vec; + vec.clear(); + vec.push_back(lp_a); + vec.push_back(lp_c); + vec.push_back(lp_d); + nla.add_monomial(lp_acd, vec.size(), vec.begin()); + + vector lemma; + s_set_column_value(s, lp_a, rational(1)); + s_set_column_value(s, lp_c, rational(1)); + s_set_column_value(s, lp_d, rational(1)); + s_set_column_value(s, lp_acd, rational(0)); + + SASSERT(nla.get_core()->test_check(lemma) == l_false); + + nla.get_core()->print_lemma(std::cout); + + ineq i0(llc::EQ, lp::lar_term(), rational(0)); + i0.m_term.add_var(lp_a); + ineq i1(llc::EQ, lp::lar_term(), rational(0)); + i1.m_term.add_var(lp_c); + ineq i2(llc::EQ, lp::lar_term(), rational(0)); + i2.m_term.add_var(lp_d); + bool found0 = false; + bool found1 = false; + bool found2 = false; + + for (const auto& k : lemma[0].ineqs()){ + if (k == i0) { + found0 = true; + } else if (k == i1) { + found1 = true; + } else if (k == i2){ + found2 = true; + } + } + + SASSERT(found0 && found1 && found2); + +} + +void test_basic_lemma_for_mon_neutral_from_monomial_to_factors() { + std::cout << "test_basic_lemma_for_mon_neutral_from_monomial_to_factors\n"; + enable_trace("nla_solver"); + 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"); + + reslimit l; + params_ref p; + 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); + vector lemma; + + // set all vars to 1 + s_set_column_value(s, lp_a, rational(1)); + s_set_column_value(s, lp_b, rational(1)); + s_set_column_value(s, lp_c, rational(1)); + s_set_column_value(s, lp_d, rational(1)); + s_set_column_value(s, lp_e, rational(1)); + s_set_column_value(s, lp_abcde, rational(1)); + s_set_column_value(s, lp_ac, rational(1)); + s_set_column_value(s, lp_bde, rational(1)); + s_set_column_value(s, lp_acd, rational(1)); + s_set_column_value(s, lp_be, rational(1)); + + // set bde to 2, b to minus 2 + s_set_column_value(s, lp_bde, rational(2)); + s_set_column_value(s, lp_b, - rational(2)); + // we have bde = -b, therefore d = +-1 and e = +-1 + s_set_column_value(s, lp_d, rational(3)); + SASSERT(nla.get_core()->test_check(lemma) == l_false); + + + nla.get_core()->print_lemma(std::cout); + ineq i0(llc::EQ, lp::lar_term(), rational(1)); + i0.m_term.add_var(lp_d); + ineq i1(llc::EQ, lp::lar_term(), -rational(1)); + i1.m_term.add_var(lp_d); + bool found0 = false; + bool found1 = false; + + for (const auto& k : lemma[0].ineqs()){ + if (k == i0) { + found0 = true; + } else if (k == i1) { + found1 = true; + } + } + + SASSERT(found0 && found1); +} + +void test_basic_sign_lemma() { + enable_trace("nla_solver"); + lp::lar_solver s; + unsigned a = 0, b = 1, c = 2, d = 3, e = 4, + bde = 7, acd = 8; + 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_bde = s.add_named_var(bde, true, "bde"); + lpvar lp_acd = s.add_named_var(acd, true, "acd"); + + reslimit l; + params_ref p; + solver nla(s); + // create monomial bde + vector vec; + + vec.push_back(lp_b); + vec.push_back(lp_d); + vec.push_back(lp_e); + + nla.add_monomial(lp_bde, vec.size(), vec.begin()); + vec.clear(); + + vec.push_back(lp_a); + vec.push_back(lp_c); + vec.push_back(lp_d); + + nla.add_monomial(lp_acd, vec.size(), vec.begin()); + + // set the values of the factors so it should be bde = -acd according to the model + + // b = -a + s_set_column_value(s, lp_a, rational(7)); + s_set_column_value(s, lp_b, rational(-7)); + + // e - c = 0 + s_set_column_value(s, lp_e, rational(4)); + s_set_column_value(s, lp_c, rational(4)); + + s_set_column_value(s, lp_d, rational(6)); + + // make bde != -acd according to the model + 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); + + lp::lar_term t; + t.add_var(lp_bde); + t.add_var(lp_acd); + 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) { + 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, abef = 13, cdij = 16, ij = 17, + k = 18; + + + 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_k = s.add_named_var(k, true, "k"); + 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"); + lpvar lp_cdij = s.add_named_var(cdij, true, "cdij"); + + for (unsigned j = 0; j < s.number_of_vars(); j++) { + s_set_column_value(s, j, rational(j + 2)); + } + + reslimit l; + params_ref p; + solver nla(s); + // 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); + int mon_ef = nla.add_monomial(lp_ef, vec.size(), vec.begin()); + // create monomial ij + vec.clear(); + vec.push_back(lp_i); + if (var_equiv) + vec.push_back(lp_k); + else + vec.push_back(lp_j); + int mon_ij = nla.add_monomial(lp_ij, vec.size(), vec.begin()); + + if (var_equiv) { // make k equivalent to j + lp::lar_term t; + t.add_var(lp_k); + t.add_coeff_var(-rational(1), lp_j); + lpvar kj = s.add_term(t.coeffs_as_vector(), -1); + s.add_var_bound(kj, llc::LE, rational(0)); + s.add_var_bound(kj, llc::GE, rational(0)); + } + + //create monomial (ab)(ef) + vec.clear(); + vec.push_back(lp_e); + vec.push_back(lp_a); + vec.push_back(lp_b); + vec.push_back(lp_f); + nla.add_monomial(lp_abef, vec.size(), vec.begin()); + + //create monomial (cd)(ij) + vec.clear(); + vec.push_back(lp_i); + vec.push_back(lp_j); + vec.push_back(lp_c); + vec.push_back(lp_d); + auto mon_cdij = nla.add_monomial(lp_cdij, vec.size(), vec.begin()); + + // set i == e + s_set_column_value(s, lp_e, s.get_column_value(lp_i)); + // set f == sign*j + s_set_column_value(s, lp_f, rational(sign) * s.get_column_value(lp_j)); + if (var_equiv) { + s_set_column_value(s, lp_k, s.get_column_value(lp_j)); + } + // set the values of ab, ef, cd, and ij correctly + s_set_column_value(s, lp_ab, nla.get_core()->mon_value_by_vars(mon_ab)); + s_set_column_value(s, lp_ef, nla.get_core()->mon_value_by_vars(mon_ef)); + s_set_column_value(s, lp_cd, nla.get_core()->mon_value_by_vars(mon_cd)); + s_set_column_value(s, lp_ij, nla.get_core()->mon_value_by_vars(mon_ij)); + + // set abef = cdij, while it has to be abef < cdij + if (sign > 0) { + SASSERT(s.get_column_value(lp_ab) < s.get_column_value(lp_cd)); + // we have ab < cd + + // we need to have ab*ef < cd*ij, so let us make ab*ef > cd*ij + s_set_column_value(s, lp_cdij, nla.get_core()->mon_value_by_vars(mon_cdij)); + s_set_column_value(s, lp_abef, nla.get_core()->mon_value_by_vars(mon_cdij) + + rational(1)); + + } + else { + SASSERT(-s.get_column_value(lp_ab) < s.get_column_value(lp_cd)); + // we need to have abef < cdij, so let us make abef < cdij + s_set_column_value(s, lp_cdij, nla.get_core()->mon_value_by_vars(mon_cdij)); + s_set_column_value(s, lp_abef, nla.get_core()->mon_value_by_vars(mon_cdij) + + rational(1)); + } + vector lemma; + + SASSERT(nla.get_core()->test_check(lemma) == l_false); + // lp::lar_term t; + // t.add_coeff_var(lp_bde); + // t.add_coeff_var(lp_acd); + // ineq q(llc::EQ, t, rational(0)); + + nla.get_core()->print_lemma(std::cout); + // SASSERT(q == lemma.back()); + // ineq i0(llc::EQ, lp::lar_term(), rational(0)); + // i0.m_term.add_coeff_var(lp_bde); + // i0.m_term.add_coeff_var(rational(1), lp_acd); + // bool found = false; + // for (const auto& k : lemma){ + // if (k == i0) { + // found = true; + // } + // } + + // SASSERT(found); +} + +void 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"); + for (unsigned j = 0; j < s.number_of_vars(); j++) { + s_set_column_value(s, j, rational((j + 2)*(j + 2))); + } + + reslimit l; + params_ref p; + solver nla(s); + // 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(s, lp_e, s.get_column_value(lp_i) + lp::impq(rational(1))); + // set f == j + 1 + s_set_column_value(s, lp_f, s.get_column_value(lp_j) +lp::impq( rational(1))); + // set the values of ab, ef, cd, and ij correctly + + s_set_column_value(s, lp_ab, nla.get_core()->mon_value_by_vars(mon_ab)); + s_set_column_value(s, lp_cd, nla.get_core()->mon_value_by_vars(mon_cd)); + s_set_column_value(s, lp_ij, nla.get_core()->mon_value_by_vars(mon_ij)); + + // set ef = ij while it has to be ef > ij + s_set_column_value(s, lp_ef, s.get_column_value(lp_ij)); + + vector lemma; + SASSERT(nla.get_core()->test_check(lemma) == l_false); + nla.get_core()->print_lemma(std::cout); +} + +void test_tangent_lemma_reg() { + enable_trace("nla_solver"); + lp::lar_solver s; + unsigned a = 0, b = 1, ab = 10; + + 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"); + int sign = 1; + for (unsigned j = 0; j < s.number_of_vars(); j++) { + sign *= -1; + s_set_column_value(s, j, sign * rational((j + 2) * (j + 2))); + } + + reslimit l; + params_ref p; + solver nla(s); + // 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()); + + s_set_column_value(s, lp_ab, nla.get_core()->mon_value_by_vars(mon_ab) + rational(10)); // greater by ten than the correct value + vector lemma; + SASSERT(nla.get_core()->test_check(lemma) == l_false); + nla.get_core()->print_lemma(std::cout); +} + +void test_tangent_lemma_equiv() { + enable_trace("nla_solver"); + lp::lar_solver s; + unsigned a = 0, b = 1, k = 2, ab = 10; + + lpvar lp_a = s.add_named_var(a, true, "a"); + lpvar lp_k = s.add_named_var(k, true, "k"); + 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"); + int sign = 1; + for (unsigned j = 0; j < s.number_of_vars(); j++) { + sign *= -1; + s_set_column_value(s, j, sign * rational((j + 2) * (j + 2))); + } + + // make k == -a + lp::lar_term t; + t.add_var(lp_k); + t.add_var(lp_a); + lpvar kj = s.add_term(t.coeffs_as_vector(), -1); + s.add_var_bound(kj, llc::LE, rational(0)); + s.add_var_bound(kj, llc::GE, rational(0)); + s_set_column_value(s, lp_a, - s.get_column_value(lp_k)); + reslimit l; + params_ref p; + solver nla(s); + // 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()); + + s_set_column_value(s, lp_ab, nla.get_core()->mon_value_by_vars(mon_ab) + rational(10)); // greater by ten than the correct value + vector lemma; + + SASSERT(nla.get_core()->test_check(lemma) == l_false); + nla.get_core()->print_lemma(std::cout); +} + + +void test_tangent_lemma() { + test_tangent_lemma_reg(); + test_tangent_lemma_equiv(); +} + +void test_order_lemma() { + test_order_lemma_params(false, 1); + test_order_lemma_params(false, -1); + test_order_lemma_params(true, 1); + test_order_lemma_params(true, -1); +} + + +} // end of namespace nla diff --git a/src/util/lp/nla_solver.cpp b/src/util/lp/nla_solver.cpp index f96e9e944..d782dfe8d 100644 --- a/src/util/lp/nla_solver.cpp +++ b/src/util/lp/nla_solver.cpp @@ -54,797 +54,4 @@ solver::~solver() { dealloc(m_core); } -void create_abcde(solver & nla, - unsigned lp_a, - unsigned lp_b, - unsigned lp_c, - unsigned lp_d, - unsigned lp_e, - unsigned lp_abcde, - unsigned lp_ac, - unsigned lp_bde, - unsigned lp_acd, - unsigned lp_be) { - // create monomial abcde - vector vec; - vec.push_back(lp_a); - vec.push_back(lp_b); - vec.push_back(lp_c); - vec.push_back(lp_d); - vec.push_back(lp_e); - - nla.add_monomial(lp_abcde, vec.size(), vec.begin()); - - // create monomial ac - vec.clear(); - vec.push_back(lp_a); - vec.push_back(lp_c); - nla.add_monomial(lp_ac, vec.size(), vec.begin()); - - // create monomial bde - vec.clear(); - vec.push_back(lp_b); - vec.push_back(lp_d); - vec.push_back(lp_e); - nla.add_monomial(lp_bde, vec.size(), vec.begin()); - - // create monomial acd - vec.clear(); - vec.push_back(lp_a); - vec.push_back(lp_c); - vec.push_back(lp_d); - nla.add_monomial(lp_acd, vec.size(), vec.begin()); - - // create monomial be - vec.clear(); - vec.push_back(lp_b); - vec.push_back(lp_e); - nla.add_monomial(lp_be, vec.size(), vec.begin()); -} - -void solver::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"); - - 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); - nla.m_core->register_monomials_in_tables(); - nla.m_core->print_monomials(std::cout); - nla.m_core->test_factorization(1, // 0 is the index of monomial abcde - 1); // 3 is the number of expected factorizations - nla.m_core->test_factorization(0, // 0 is the index of monomial abcde - 3); // 3 is the number of expected factorizations - - -} - -void solver::test_basic_lemma_for_mon_neutral_from_factors_to_monomial() { - test_basic_lemma_for_mon_neutral_from_factors_to_monomial_0(); - test_basic_lemma_for_mon_neutral_from_factors_to_monomial_1(); -} - -void solver::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"; - enable_trace("nla_solver"); - TRACE("nla_solver",); - lp::lar_solver s; - unsigned a = 0, b = 1, c = 2, d = 3, e = 4, - abcde = 5, ac = 6, bde = 7; - 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"); - - reslimit l; - params_ref p; - solver nla(s, l, p); - svector v; v.push_back(lp_b);v.push_back(lp_d);v.push_back(lp_e); - nla.add_monomial(lp_bde, v.size(), v.begin()); - v.clear(); - v.push_back(lp_a);v.push_back(lp_b);v.push_back(lp_c);v.push_back(lp_d);v.push_back(lp_e); - nla.add_monomial(lp_abcde, v.size(), v.begin()); - v.clear(); - v.push_back(lp_a);v.push_back(lp_c); - nla.add_monomial(lp_ac, v.size(), v.begin()); - - vector lv; - - // set abcde = ac * bde - // ac = 1 then abcde = bde, but we have abcde < bde - s.set_column_value(lp_a, lp::impq(rational(4))); - s.set_column_value(lp_b, lp::impq(rational(4))); - s.set_column_value(lp_c, lp::impq(rational(4))); - s.set_column_value(lp_d, lp::impq(rational(4))); - s.set_column_value(lp_e, lp::impq(rational(4))); - s.set_column_value(lp_abcde, lp::impq(rational(15))); - s.set_column_value(lp_ac, lp::impq(rational(1))); - s.set_column_value(lp_bde, lp::impq(rational(16))); - - - SASSERT(nla.m_core->test_check(lv) == l_false); - - nla.m_core->print_lemma(std::cout); - - ineq i0(llc::NE, lp::lar_term(), rational(1)); - i0.m_term.add_var(lp_ac); - ineq i1(llc::EQ, lp::lar_term(), rational(0)); - i1.m_term.add_var(lp_bde); - i1.m_term.add_coeff_var(-rational(1), lp_abcde); - ineq i2(llc::EQ, lp::lar_term(), rational(0)); - i2.m_term.add_var(lp_abcde); - i2.m_term.add_coeff_var(-rational(1), lp_bde); - bool found0 = false; - bool found1 = false; - bool found2 = false; - for (const auto& k : lv[0].ineqs()){ - if (k == i0) { - found0 = true; - } else if (k == i1) { - found1 = true; - } else if (k == i2) { - found2 = true; - } - } - - SASSERT(found0 && (found1 || found2)); - - -} - -void solver::s_set_column_value(lp::lar_solver&s, lpvar j, const rational & v) { - s.set_column_value(j, lp::impq(v)); -} - -void solver::s_set_column_value(lp::lar_solver&s, lpvar j, const lp::impq & v) { - s.set_column_value(j, v); -} - -void solver::test_basic_lemma_for_mon_neutral_from_factors_to_monomial_1() { - std::cout << "test_basic_lemma_for_mon_neutral_from_factors_to_monomial_1\n"; - TRACE("nla_solver",); - lp::lar_solver s; - unsigned a = 0, b = 1, c = 2, d = 3, e = 4, - bde = 7; - 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_bde = s.add_var(bde, true); - - reslimit l; - params_ref p; - solver nla(s, l, p); - svector v; v.push_back(lp_b);v.push_back(lp_d);v.push_back(lp_e); - nla.add_monomial(lp_bde, v.size(), v.begin()); - - vector lemma; - - s_set_column_value(s, lp_a, rational(1)); - s_set_column_value(s, lp_b, rational(1)); - s_set_column_value(s, lp_c, rational(1)); - s_set_column_value(s, lp_d, rational(1)); - s_set_column_value(s, lp_e, rational(1)); - s_set_column_value(s, lp_bde, rational(3)); - - SASSERT(nla.m_core->test_check(lemma) == l_false); - SASSERT(lemma[0].size() == 4); - nla.m_core->print_lemma(std::cout); - - ineq i0(llc::NE, lp::lar_term(), rational(1)); - i0.m_term.add_var(lp_b); - ineq i1(llc::NE, lp::lar_term(), rational(1)); - i1.m_term.add_var(lp_d); - ineq i2(llc::NE, lp::lar_term(), rational(1)); - i2.m_term.add_var(lp_e); - ineq i3(llc::EQ, lp::lar_term(), rational(1)); - i3.m_term.add_var(lp_bde); - bool found0 = false; - bool found1 = false; - bool found2 = false; - bool found3 = false; - for (const auto& k : lemma[0].ineqs()){ - if (k == i0) { - found0 = true; - } else if (k == i1) { - found1 = true; - } else if (k == i2) { - found2 = true; - } else if (k == i3) { - found3 = true; - } - - } - - SASSERT(found0 && found1 && found2 && found3); - -} - -void solver::test_basic_lemma_for_mon_zero_from_factors_to_monomial() { - std::cout << "test_basic_lemma_for_mon_zero_from_factors_to_monomial\n"; - enable_trace("nla_solver"); - 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"); - - 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; - - // set vars - s_set_column_value(s, lp_a, rational(1)); - s_set_column_value(s, lp_b, rational(0)); - s_set_column_value(s, lp_c, rational(1)); - s_set_column_value(s, lp_d, rational(1)); - s_set_column_value(s, lp_e, rational(1)); - s_set_column_value(s, lp_abcde, rational(0)); - s_set_column_value(s, lp_ac, rational(1)); - s_set_column_value(s, lp_bde, rational(0)); - s_set_column_value(s, lp_acd, rational(1)); - s_set_column_value(s, lp_be, rational(1)); - - SASSERT(nla.m_core->test_check(lemma) == l_false); - nla.m_core->print_lemma(std::cout); - SASSERT(lemma.size() == 1 && lemma[0].size() == 2); - ineq i0(llc::NE, lp::lar_term(), rational(0)); - i0.m_term.add_var(lp_b); - ineq i1(llc::EQ, lp::lar_term(), rational(0)); - i1.m_term.add_var(lp_be); - bool found0 = false; - bool found1 = false; - - for (const auto& k : lemma[0].ineqs()){ - if (k == i0) { - found0 = true; - } else if (k == i1) { - found1 = true; - } - } - - SASSERT(found0 && found1); -} - -void solver::test_basic_lemma_for_mon_zero_from_monomial_to_factors() { - std::cout << "test_basic_lemma_for_mon_zero_from_monomial_to_factors\n"; - enable_trace("nla_solver"); - lp::lar_solver s; - unsigned a = 0, c = 2, d = 3, acd = 8; - lpvar lp_a = s.add_named_var(a, true, "a"); - lpvar lp_c = s.add_named_var(c, true, "c"); - lpvar lp_d = s.add_named_var(d, true, "d"); - lpvar lp_acd = s.add_named_var(acd, true, "acd"); - - reslimit l; - params_ref p; - solver nla(s, l, p); - - // create monomial acd - unsigned_vector vec; - vec.clear(); - vec.push_back(lp_a); - vec.push_back(lp_c); - vec.push_back(lp_d); - nla.add_monomial(lp_acd, vec.size(), vec.begin()); - - vector lemma; - s_set_column_value(s, lp_a, rational(1)); - s_set_column_value(s, lp_c, rational(1)); - s_set_column_value(s, lp_d, rational(1)); - s_set_column_value(s, lp_acd, rational(0)); - - SASSERT(nla.m_core->test_check(lemma) == l_false); - - nla.m_core->print_lemma(std::cout); - - ineq i0(llc::EQ, lp::lar_term(), rational(0)); - i0.m_term.add_var(lp_a); - ineq i1(llc::EQ, lp::lar_term(), rational(0)); - i1.m_term.add_var(lp_c); - ineq i2(llc::EQ, lp::lar_term(), rational(0)); - i2.m_term.add_var(lp_d); - bool found0 = false; - bool found1 = false; - bool found2 = false; - - for (const auto& k : lemma[0].ineqs()){ - if (k == i0) { - found0 = true; - } else if (k == i1) { - found1 = true; - } else if (k == i2){ - found2 = true; - } - } - - SASSERT(found0 && found1 && found2); - -} - -void solver::test_basic_lemma_for_mon_neutral_from_monomial_to_factors() { - std::cout << "test_basic_lemma_for_mon_neutral_from_monomial_to_factors\n"; - enable_trace("nla_solver"); - 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"); - - 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; - - // set all vars to 1 - s_set_column_value(s, lp_a, rational(1)); - s_set_column_value(s, lp_b, rational(1)); - s_set_column_value(s, lp_c, rational(1)); - s_set_column_value(s, lp_d, rational(1)); - s_set_column_value(s, lp_e, rational(1)); - s_set_column_value(s, lp_abcde, rational(1)); - s_set_column_value(s, lp_ac, rational(1)); - s_set_column_value(s, lp_bde, rational(1)); - s_set_column_value(s, lp_acd, rational(1)); - s_set_column_value(s, lp_be, rational(1)); - - // set bde to 2, b to minus 2 - s_set_column_value(s, lp_bde, rational(2)); - s_set_column_value(s, lp_b, - rational(2)); - // we have bde = -b, therefore d = +-1 and e = +-1 - s_set_column_value(s, lp_d, rational(3)); - SASSERT(nla.m_core->test_check(lemma) == l_false); - - - nla.m_core->print_lemma(std::cout); - ineq i0(llc::EQ, lp::lar_term(), rational(1)); - i0.m_term.add_var(lp_d); - ineq i1(llc::EQ, lp::lar_term(), -rational(1)); - i1.m_term.add_var(lp_d); - bool found0 = false; - bool found1 = false; - - for (const auto& k : lemma[0].ineqs()){ - if (k == i0) { - found0 = true; - } else if (k == i1) { - found1 = true; - } - } - - SASSERT(found0 && found1); -} - -void solver::test_basic_sign_lemma() { - enable_trace("nla_solver"); - lp::lar_solver s; - unsigned a = 0, b = 1, c = 2, d = 3, e = 4, - bde = 7, acd = 8; - 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_bde = s.add_named_var(bde, true, "bde"); - lpvar lp_acd = s.add_named_var(acd, true, "acd"); - - reslimit l; - params_ref p; - solver nla(s, l, p); - // create monomial bde - vector vec; - - vec.push_back(lp_b); - vec.push_back(lp_d); - vec.push_back(lp_e); - - nla.add_monomial(lp_bde, vec.size(), vec.begin()); - vec.clear(); - - vec.push_back(lp_a); - vec.push_back(lp_c); - vec.push_back(lp_d); - - nla.add_monomial(lp_acd, vec.size(), vec.begin()); - - // set the values of the factors so it should be bde = -acd according to the model - - // b = -a - s_set_column_value(s, lp_a, rational(7)); - s_set_column_value(s, lp_b, rational(-7)); - - // e - c = 0 - s_set_column_value(s, lp_e, rational(4)); - s_set_column_value(s, lp_c, rational(4)); - - s_set_column_value(s, lp_d, rational(6)); - - // make bde != -acd according to the model - s_set_column_value(s, lp_bde, rational(5)); - s_set_column_value(s, lp_acd, rational(3)); - - vector lemma; - SASSERT(nla.m_core->test_check(lemma) == l_false); - - lp::lar_term t; - t.add_var(lp_bde); - t.add_var(lp_acd); - ineq q(llc::EQ, t, rational(0)); - - nla.m_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 solver::test_order_lemma_params(bool var_equiv, int sign) { - 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, abef = 13, cdij = 16, ij = 17, - k = 18; - - - 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_k = s.add_named_var(k, true, "k"); - 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"); - lpvar lp_cdij = s.add_named_var(cdij, true, "cdij"); - - for (unsigned j = 0; j < s.number_of_vars(); j++) { - s_set_column_value(s, j, rational(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); - int mon_ef = nla.add_monomial(lp_ef, vec.size(), vec.begin()); - // create monomial ij - vec.clear(); - vec.push_back(lp_i); - if (var_equiv) - vec.push_back(lp_k); - else - vec.push_back(lp_j); - int mon_ij = nla.add_monomial(lp_ij, vec.size(), vec.begin()); - - if (var_equiv) { // make k equivalent to j - lp::lar_term t; - t.add_var(lp_k); - t.add_coeff_var(-rational(1), lp_j); - lpvar kj = s.add_term(t.coeffs_as_vector(), -1); - s.add_var_bound(kj, llc::LE, rational(0)); - s.add_var_bound(kj, llc::GE, rational(0)); - } - - //create monomial (ab)(ef) - vec.clear(); - vec.push_back(lp_e); - vec.push_back(lp_a); - vec.push_back(lp_b); - vec.push_back(lp_f); - nla.add_monomial(lp_abef, vec.size(), vec.begin()); - - //create monomial (cd)(ij) - vec.clear(); - vec.push_back(lp_i); - vec.push_back(lp_j); - vec.push_back(lp_c); - vec.push_back(lp_d); - auto mon_cdij = nla.add_monomial(lp_cdij, vec.size(), vec.begin()); - - // set i == e - s_set_column_value(s, lp_e, s.get_column_value(lp_i)); - // set f == sign*j - s_set_column_value(s, lp_f, rational(sign) * s.get_column_value(lp_j)); - if (var_equiv) { - s_set_column_value(s, lp_k, s.get_column_value(lp_j)); - } - // set the values of ab, ef, cd, and ij correctly - s_set_column_value(s, lp_ab, nla.m_core->mon_value_by_vars(mon_ab)); - s_set_column_value(s, lp_ef, nla.m_core->mon_value_by_vars(mon_ef)); - s_set_column_value(s, lp_cd, nla.m_core->mon_value_by_vars(mon_cd)); - s_set_column_value(s, lp_ij, nla.m_core->mon_value_by_vars(mon_ij)); - - // set abef = cdij, while it has to be abef < cdij - if (sign > 0) { - SASSERT(s.get_column_value(lp_ab) < s.get_column_value(lp_cd)); - // we have ab < cd - - // we need to have ab*ef < cd*ij, so let us make ab*ef > cd*ij - s_set_column_value(s, lp_cdij, nla.m_core->mon_value_by_vars(mon_cdij)); - s_set_column_value(s, lp_abef, nla.m_core->mon_value_by_vars(mon_cdij) - + rational(1)); - - } - else { - SASSERT(-s.get_column_value(lp_ab) < s.get_column_value(lp_cd)); - // we need to have abef < cdij, so let us make abef < cdij - s_set_column_value(s, lp_cdij, nla.m_core->mon_value_by_vars(mon_cdij)); - s_set_column_value(s, lp_abef, nla.m_core->mon_value_by_vars(mon_cdij) - + rational(1)); - } - vector lemma; - - SASSERT(nla.m_core->test_check(lemma) == l_false); - // lp::lar_term t; - // t.add_coeff_var(lp_bde); - // t.add_coeff_var(lp_acd); - // ineq q(llc::EQ, t, rational(0)); - - nla.m_core->print_lemma(std::cout); - // SASSERT(q == lemma.back()); - // ineq i0(llc::EQ, lp::lar_term(), rational(0)); - // i0.m_term.add_coeff_var(lp_bde); - // i0.m_term.add_coeff_var(rational(1), lp_acd); - // bool found = false; - // for (const auto& k : lemma){ - // if (k == i0) { - // found = true; - // } - // } - - // 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"); - for (unsigned j = 0; j < s.number_of_vars(); j++) { - s_set_column_value(s, 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(s, lp_e, s.get_column_value(lp_i) + lp::impq(rational(1))); - // set f == j + 1 - s_set_column_value(s, lp_f, s.get_column_value(lp_j) +lp::impq( rational(1))); - // set the values of ab, ef, cd, and ij correctly - - s_set_column_value(s, lp_ab, nla.m_core->mon_value_by_vars(mon_ab)); - s_set_column_value(s, lp_cd, nla.m_core->mon_value_by_vars(mon_cd)); - s_set_column_value(s, lp_ij, nla.m_core->mon_value_by_vars(mon_ij)); - - // set ef = ij while it has to be ef > ij - s_set_column_value(s, lp_ef, s.get_column_value(lp_ij)); - - vector lemma; - SASSERT(nla.m_core->test_check(lemma) == l_false); - nla.m_core->print_lemma(std::cout); -} - -void solver::test_tangent_lemma_reg() { - enable_trace("nla_solver"); - lp::lar_solver s; - unsigned a = 0, b = 1, ab = 10; - - 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"); - int sign = 1; - for (unsigned j = 0; j < s.number_of_vars(); j++) { - sign *= -1; - s_set_column_value(s, j, sign * 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()); - - s_set_column_value(s, lp_ab, nla.m_core->mon_value_by_vars(mon_ab) + rational(10)); // greater by ten than the correct value - vector lemma; - SASSERT(nla.m_core->test_check(lemma) == l_false); - nla.m_core->print_lemma(std::cout); -} - -void solver::test_tangent_lemma_equiv() { - enable_trace("nla_solver"); - lp::lar_solver s; - unsigned a = 0, b = 1, k = 2, ab = 10; - - lpvar lp_a = s.add_named_var(a, true, "a"); - lpvar lp_k = s.add_named_var(k, true, "k"); - 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"); - int sign = 1; - for (unsigned j = 0; j < s.number_of_vars(); j++) { - sign *= -1; - s_set_column_value(s, j, sign * rational((j + 2) * (j + 2))); - } - - // make k == -a - lp::lar_term t; - t.add_var(lp_k); - t.add_var(lp_a); - lpvar kj = s.add_term(t.coeffs_as_vector(), -1); - s.add_var_bound(kj, llc::LE, rational(0)); - s.add_var_bound(kj, llc::GE, rational(0)); - s_set_column_value(s, lp_a, - s.get_column_value(lp_k)); - 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()); - - s_set_column_value(s, lp_ab, nla.m_core->mon_value_by_vars(mon_ab) + rational(10)); // greater by ten than the correct value - vector lemma; - - SASSERT(nla.m_core->test_check(lemma) == l_false); - nla.m_core->print_lemma(std::cout); -} - - -void solver::test_tangent_lemma() { - test_tangent_lemma_reg(); - test_tangent_lemma_equiv(); -} - -void solver::test_order_lemma() { - test_order_lemma_params(false, 1); - test_order_lemma_params(false, -1); - test_order_lemma_params(true, 1); - test_order_lemma_params(true, -1); -} } diff --git a/src/util/lp/nla_solver.h b/src/util/lp/nla_solver.h index dfd84e7d3..7261f587f 100644 --- a/src/util/lp/nla_solver.h +++ b/src/util/lp/nla_solver.h @@ -37,25 +37,10 @@ public: solver(lp::lar_solver& s, reslimit& lim, params_ref const& p); ~solver(); + inline core * get_core() { return m_core; } void push(); void pop(unsigned scopes); bool need_check(); lbool check(vector&); - static void test_factorization(); - static void test_basic_sign_lemma(); - 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(); - static void test_basic_lemma_for_mon_neutral_from_factors_to_monomial_0(); - 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(); - static void test_tangent_lemma(); - static void test_tangent_lemma_reg(); - static void test_tangent_lemma_equiv(); - static void s_set_column_value(lp::lar_solver&, unsigned, const rational &); - static void s_set_column_value(lp::lar_solver&, unsigned, const lp::impq &); }; }