From 9c8d5ddffbcc8bd4e71ecb0cfd8b2ff7ec1d80a4 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 15 Jan 2020 11:40:15 -0800 Subject: [PATCH] enable test_tangent_lemma_reg Signed-off-by: Lev Nachmanson --- src/math/lp/nla_core.cpp | 7 ++++--- src/test/lp/CMakeLists.txt | 2 +- src/test/lp/nla_solver_test.cpp | 24 +++++++----------------- 3 files changed, 12 insertions(+), 21 deletions(-) diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index b07abc9e6..0d15fd0be 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -165,8 +165,9 @@ rational core::product_value(const unsigned_vector & m) const { // return true iff the monic value is equal to the product of the values of the factors bool core::check_monic(const monic& m) const { SASSERT((!m_lar_solver.column_is_int(m.var())) || m_lar_solver.get_column_value(m.var()).is_int()); - TRACE("nla_solver", print_monic_with_vars(m, tout) << '\n';); - return product_value(m.vars()) == m_lar_solver.get_column_value_rational(m.var()); + bool ret = product_value(m.vars()) == m_lar_solver.get_column_value_rational(m.var()); + CTRACE("nla_solver", !ret, print_monic(m, tout) << '\n';); + return ret; } void core::explain(const monic& m, lp::explanation& exp) const { @@ -1257,7 +1258,7 @@ bool core::done() const { } lbool core::incremental_linearization(bool constraint_derived) { - TRACE("nla_solver", print_terms(tout); m_lar_solver.print_constraints(tout);); + TRACE("nla_solver_details", print_terms(tout); m_lar_solver.print_constraints(tout);); for (int search_level = 0; search_level < 3 && !done(); search_level++) { TRACE("nla_solver", tout << "constraint_derived = " << constraint_derived << ", search_level = " << search_level << "\n";); if (search_level == 0) { diff --git a/src/test/lp/CMakeLists.txt b/src/test/lp/CMakeLists.txt index 76bb92e58..f10e240bf 100644 --- a/src/test/lp/CMakeLists.txt +++ b/src/test/lp/CMakeLists.txt @@ -2,7 +2,7 @@ add_executable(lp_tst EXCLUDE_FROM_ALL 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}) diff --git a/src/test/lp/nla_solver_test.cpp b/src/test/lp/nla_solver_test.cpp index d8ab6d978..e7d36bbd3 100644 --- a/src/test/lp/nla_solver_test.cpp +++ b/src/test/lp/nla_solver_test.cpp @@ -718,26 +718,18 @@ void test_monotone_lemma() { } void test_tangent_lemma_reg() { - /* enable_trace("nla_solver"); lp::lar_solver s; - unsigned a = 0, b = 1, ab = 10; + unsigned a = s.number_of_vars(); + unsigned b = a + 1; + unsigned ab = b + 1; 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))); - } - + s_set_column_value(s, lp_a, rational(3)); + s_set_column_value(s, lp_b, rational(4)); + s_set_column_value(s, lp_ab, rational(11)); reslimit l; params_ref p; solver nla(s); @@ -745,13 +737,11 @@ void test_tangent_lemma_reg() { vector vec; vec.push_back(lp_a); vec.push_back(lp_b); - int mon_ab = nla.add_monic(lp_ab, vec.size(), vec.begin()); + nla.add_monic(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() {