From a8dd908fa01a0f4b82a778bacbfdbd26e992e5a3 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Mon, 30 Sep 2019 17:27:05 -0700 Subject: [PATCH] debug cross_nested form with new expressions Signed-off-by: Lev Nachmanson --- src/math/lp/cross_nested.h | 10 ++------ src/math/lp/nex_creator.cpp | 5 ++-- src/math/lp/nex_creator.h | 7 ++++++ src/test/lp/lp.cpp | 49 ++++++++++++++++++++----------------- 4 files changed, 38 insertions(+), 33 deletions(-) diff --git a/src/math/lp/cross_nested.h b/src/math/lp/cross_nested.h index 4dfd1034f..f8fbe8dcf 100644 --- a/src/math/lp/cross_nested.h +++ b/src/math/lp/cross_nested.h @@ -268,12 +268,6 @@ public: explore_expr_on_front_elem_vars(c, front, vars); } } - static std::string ch(unsigned j) { - std::stringstream s; - s << "v" << j; - return s.str(); - // return (char)('a'+j); - } std::ostream& print_front(const vector& front, std::ostream& out) const { for (auto e : front) { @@ -284,7 +278,7 @@ public: // c is the sub expressiond which is going to be changed from sum to the cross nested form // front will be explored more void explore_of_expr_on_sum_and_var(nex** c, lpvar j, vector front) { - TRACE("nla_cn", tout << "m_e=" << *m_e << "\nc=" << **c << "\nj = " << ch(j) << "\nfront="; print_front(front, tout) << "\n";); + TRACE("nla_cn", tout << "m_e=" << *m_e << "\nc=" << **c << "\nj = " << nex_creator::ch(j) << "\nfront="; print_front(front, tout) << "\n";); if (!split_with_var(*c, j, front)) return; TRACE("nla_cn", tout << "after split c=" << **c << "\nfront="; print_front(front, tout) << "\n";); @@ -428,7 +422,7 @@ public: // it returns true if the recursion brings a cross-nested form bool split_with_var(nex*& e, lpvar j, vector & front) { SASSERT(e->is_sum()); - TRACE("nla_cn", tout << "e = " << *e << ", j=" << ch(j) << "\n";); + TRACE("nla_cn", tout << "e = " << *e << ", j=" << nex_creator::ch(j) << "\n";); nex_sum* a; nex * b; pre_split(to_sum(e), j, a, b); /* diff --git a/src/math/lp/nex_creator.cpp b/src/math/lp/nex_creator.cpp index aaf685e88..15756b0cb 100644 --- a/src/math/lp/nex_creator.cpp +++ b/src/math/lp/nex_creator.cpp @@ -22,7 +22,7 @@ namespace nla { nex * nex_creator::mk_div(const nex* a, lpvar j) { SASSERT(is_simplified(a)); - TRACE("nla_cn_details", tout << "a=" << *a << ", v" << j << "\n";); + TRACE("nla_cn_details", tout << "a=" << *a << ", " << ch(j) << "\n";); SASSERT((a->is_mul() && a->contains(j)) || (a->is_var() && to_var(a)->var() == j)); if (a->is_var()) return mk_scalar(rational(1)); @@ -391,8 +391,7 @@ nex* nex_creator::create_child_from_nex_and_coeff(nex *e, return mk_mul(mk_scalar(coeff), e); } case expr_type::SCALAR: { - UNREACHABLE(); - return nullptr; + return mk_scalar(coeff); } case expr_type::MUL: { nex_mul * em = to_mul(e); diff --git a/src/math/lp/nex_creator.h b/src/math/lp/nex_creator.h index ad95f08de..7e9806417 100644 --- a/src/math/lp/nex_creator.h +++ b/src/math/lp/nex_creator.h @@ -57,6 +57,13 @@ class nex_creator { svector m_active_vars_weights; public: + static char ch(unsigned j) { + // std::stringstream s; + // s << "v" << j; + // return s.str(); + return (char)('a'+j); + } + svector& active_vars_weights() { return m_active_vars_weights;} const svector& active_vars_weights() const { return m_active_vars_weights;} diff --git a/src/test/lp/lp.cpp b/src/test/lp/lp.cpp index 5e365ce7a..75fd86638 100644 --- a/src/test/lp/lp.cpp +++ b/src/test/lp/lp.cpp @@ -131,34 +131,39 @@ void test_cn() { []{ return 1; }); enable_trace("nla_cn"); enable_trace("nla_cn_details"); - nex_var* a = cn.get_nex_creator().mk_var(0); - nex_var* b = cn.get_nex_creator().mk_var(1); - nex_var* c = cn.get_nex_creator().mk_var(2); - nex_var* d = cn.get_nex_creator().mk_var(3); - nex_var* e = cn.get_nex_creator().mk_var(4); - nex_var* g = cn.get_nex_creator().mk_var(6); - nex* min_1 = cn.get_nex_creator().mk_scalar(rational(-1)); + auto & cr = cn.get_nex_creator(); + cr.active_vars_weights().resize(20); + for (unsigned j = 0; j < cr.active_vars_weights().size(); j++) + cr.active_vars_weights()[j] = static_cast(1); + + nex_var* a = cr.mk_var(0); + nex_var* b = cr.mk_var(1); + nex_var* c = cr.mk_var(2); + nex_var* d = cr.mk_var(3); + nex_var* e = cr.mk_var(4); + nex_var* g = cr.mk_var(6); + nex* min_1 = cr.mk_scalar(rational(-1)); // test_cn_on_expr(min_1*c*e + min_1*b*d + min_1*a*b + a*c); - nex* bcd = cn.get_nex_creator().mk_mul(b, c, d); - nex_mul* bcg = cn.get_nex_creator().mk_mul(b, c, g); + nex* bcd = cr.mk_mul(b, c, d); + nex_mul* bcg = cr.mk_mul(b, c, g); bcg->add_child(min_1); - nex_sum* t = cn.get_nex_creator().mk_sum(bcd, bcg); + nex_sum* t = cr.mk_sum(bcd, bcg); test_cn_on_expr(t, cn); - nex* aad = cn.get_nex_creator().mk_mul(a, a, d); - nex* abcd = cn.get_nex_creator().mk_mul(a, b, c, d); - nex* aaccd = cn.get_nex_creator().mk_mul(a, a, c, c, d); - nex* add = cn.get_nex_creator().mk_mul(a, d, d); - nex* eae = cn.get_nex_creator().mk_mul(e, a, e); - nex* eac = cn.get_nex_creator().mk_mul(e, a, c); - nex* ed = cn.get_nex_creator().mk_mul(e, d); - nex* _6aad = cn.get_nex_creator().mk_mul(cn.get_nex_creator().mk_scalar(rational(6)), a, a, d); + nex* aad = cr.mk_mul(a, a, d); + nex* abcd = cr.mk_mul(a, b, c, d); + nex* aaccd = cr.mk_mul(a, a, c, c, d); + nex* add = cr.mk_mul(a, d, d); + nex* eae = cr.mk_mul(e, a, e); + nex* eac = cr.mk_mul(e, a, c); + nex* ed = cr.mk_mul(e, d); + nex* _6aad = cr.mk_mul(cr.mk_scalar(rational(6)), a, a, d); #ifdef Z3DEBUG - nex * clone = cn.get_nex_creator().clone(cn.get_nex_creator().mk_sum(_6aad, abcd, aaccd, add, eae, eac, ed)); - clone = cn.get_nex_creator().simplify(clone); - SASSERT(cn.get_nex_creator().is_simplified(clone)); + nex * clone = cr.clone(cr.mk_sum(_6aad, abcd, aaccd, add, eae, eac, ed)); + clone = cr.simplify(clone); + SASSERT(cr.is_simplified(clone)); TRACE("nla_cn", tout << "clone = " << *clone << "\n";); #endif - // test_cn_on_expr(cn.get_nex_creator().mk_sum(aad, abcd, aaccd, add, eae, eac, ed), cn); + // test_cn_on_expr(cr.mk_sum(aad, abcd, aaccd, add, eae, eac, ed), cn); test_cn_on_expr(to_sum(clone), cn); // TRACE("nla_cn", tout << "done\n";); // test_cn_on_expr(a*b*d + a*b*c + c*b*d + a*c*d);