From db9d6d12fc1dfa4cf7240f9e88c64dfb6dfa21e7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 11 Apr 2020 15:27:18 -0700 Subject: [PATCH] fix #3836 remove unused and buggy hoist_cmul Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/poly_rewriter.h | 3 - src/ast/rewriter/poly_rewriter_def.h | 78 ++--------------------- src/ast/rewriter/poly_rewriter_params.pyg | 1 - src/smt/theory_recfun.cpp | 2 +- src/tactic/sls/sls_tactic.cpp | 1 - 5 files changed, 6 insertions(+), 79 deletions(-) diff --git a/src/ast/rewriter/poly_rewriter.h b/src/ast/rewriter/poly_rewriter.h index 9a83ac729..424b684a0 100644 --- a/src/ast/rewriter/poly_rewriter.h +++ b/src/ast/rewriter/poly_rewriter.h @@ -35,7 +35,6 @@ protected: unsigned m_som_blowup; bool m_sort_sums; bool m_hoist_mul; - bool m_hoist_cmul; bool m_ast_order; bool m_hoist_ite; @@ -88,9 +87,7 @@ protected: bool hoist_multiplication(expr_ref& som); expr* merge_muls(expr* x, expr* y); - struct hoist_cmul_lt; bool is_mul(expr * t, numeral & c, expr * & pp); - void hoist_cmul(expr_ref_buffer & args); class mon_lt { poly_rewriter& rw; diff --git a/src/ast/rewriter/poly_rewriter_def.h b/src/ast/rewriter/poly_rewriter_def.h index c4493d8ac..442e20e2d 100644 --- a/src/ast/rewriter/poly_rewriter_def.h +++ b/src/ast/rewriter/poly_rewriter_def.h @@ -32,7 +32,6 @@ void poly_rewriter::updt_params(params_ref const & _p) { m_flat = p.flat(); m_som = p.som(); m_hoist_mul = p.hoist_mul(); - m_hoist_cmul = p.hoist_cmul(); m_hoist_ite = p.hoist_ite(); m_som_blowup = p.som_blowup(); if (!m_flat) m_som = false; @@ -270,8 +269,8 @@ br_status poly_rewriter::mk_nflat_mul_core(unsigned num_args, expr * con } } - if (num_add == 0 || m_hoist_cmul) { - SASSERT(!is_add(var) || m_hoist_cmul); + if (num_add == 0) { + SASSERT(!is_add(var)); if (num_args == 2 && args[1] == var) { DEBUG_CODE({ numeral c_prime; @@ -452,67 +451,6 @@ bool poly_rewriter::is_mul(expr * t, numeral & c, expr * & pp) { return true; } -template -struct poly_rewriter::hoist_cmul_lt { - poly_rewriter & m_r; - hoist_cmul_lt(poly_rewriter & r):m_r(r) {} - - bool operator()(expr * t1, expr * t2) const { - expr * pp1 = nullptr; - expr * pp2 = nullptr; - numeral c1, c2; - bool is_mul1 = m_r.is_mul(t1, c1, pp1); - bool is_mul2 = m_r.is_mul(t2, c2, pp2); - if (!is_mul1 && is_mul2) - return true; - if (is_mul1 && !is_mul2) - return false; - if (!is_mul1 && !is_mul2) - return t1->get_id() < t2->get_id(); - if (c1 < c2) - return true; - if (c1 > c2) - return false; - return pp1->get_id() < pp2->get_id(); - } -}; - -template -void poly_rewriter::hoist_cmul(expr_ref_buffer & args) { - unsigned sz = args.size(); - std::sort(args.c_ptr(), args.c_ptr() + sz, hoist_cmul_lt(*this)); - numeral c, c_prime; - ptr_buffer pps; - expr * pp, * pp_prime; - unsigned j = 0; - unsigned i = 0; - while (i < sz) { - expr * mon = args[i]; - if (is_mul(mon, c, pp) && i < sz - 1) { - expr * mon_prime = args[i+1]; - if (is_mul(mon_prime, c_prime, pp_prime) && c == c_prime) { - // found target - pps.reset(); - pps.push_back(pp); - pps.push_back(pp_prime); - i += 2; - while (i < sz && is_mul(args[i], c_prime, pp_prime) && c == c_prime) { - pps.push_back(pp_prime); - i++; - } - SASSERT(is_numeral(to_app(mon)->get_arg(0), c_prime) && c == c_prime); - expr * mul_args[2] = { to_app(mon)->get_arg(0), mk_add_app(pps.size(), pps.c_ptr()) }; - args.set(j, mk_mul_app(2, mul_args)); - j++; - continue; - } - } - args.set(j, mon); - j++; - i++; - } - args.resize(j); -} template bool poly_rewriter::mon_lt::operator()(expr* e1, expr * e2) const { @@ -638,10 +576,7 @@ br_status poly_rewriter::mk_nflat_add_core(unsigned num_args, expr * con new_args.push_back(mk_mul_app(a, pp)); } } - if (m_hoist_cmul) { - hoist_cmul(new_args); - } - else if (m_sort_sums) { + if (m_sort_sums) { TRACE("rewriter_bug", tout << "new_args.size(): " << new_args.size() << "\n";); if (c.is_zero()) std::sort(new_args.c_ptr(), new_args.c_ptr() + new_args.size(), mon_lt(*this)); @@ -660,7 +595,7 @@ br_status poly_rewriter::mk_nflat_add_core(unsigned num_args, expr * con } else { SASSERT(!has_multiple); - if (ordered && !m_hoist_mul && !m_hoist_cmul && !m_hoist_ite) { + if (ordered && !m_hoist_mul && !m_hoist_ite) { if (num_coeffs == 0) return BR_FAILED; if (num_coeffs == 1 && is_numeral(args[0], a) && !a.is_zero()) @@ -675,10 +610,7 @@ br_status poly_rewriter::mk_nflat_add_core(unsigned num_args, expr * con continue; new_args.push_back(arg); } - if (m_hoist_cmul) { - hoist_cmul(new_args); - } - else if (!ordered) { + if (!ordered) { if (c.is_zero()) std::sort(new_args.c_ptr(), new_args.c_ptr() + new_args.size(), lt); else diff --git a/src/ast/rewriter/poly_rewriter_params.pyg b/src/ast/rewriter/poly_rewriter_params.pyg index c2b90a95b..05500b948 100644 --- a/src/ast/rewriter/poly_rewriter_params.pyg +++ b/src/ast/rewriter/poly_rewriter_params.pyg @@ -4,6 +4,5 @@ def_module_params(module_name='rewriter', params=(("som", BOOL, False, "put polynomials in sum-of-monomials form"), ("som_blowup", UINT, 10, "maximum increase of monomials generated when putting a polynomial in sum-of-monomials normal form"), ("hoist_mul", BOOL, False, "hoist multiplication over summation to minimize number of multiplications"), - ("hoist_cmul", BOOL, False, "hoist constant multiplication over summation to minimize number of multiplications"), ("hoist_ite", BOOL, False, "hoist shared summands under ite expressions"), ("flat", BOOL, True, "create nary applications for and,or,+,*,bvadd,bvmul,bvand,bvor,bvxor"))) diff --git a/src/smt/theory_recfun.cpp b/src/smt/theory_recfun.cpp index 226b6b00a..745d235a8 100644 --- a/src/smt/theory_recfun.cpp +++ b/src/smt/theory_recfun.cpp @@ -308,7 +308,7 @@ namespace smt { */ void theory_recfun::assert_macro_axiom(case_expansion & e) { m_stats.m_macro_expansions++; - TRACEFN("case expansion " << pp_case_expansion(e, m) << "\n"); + TRACEFN("case expansion " << pp_case_expansion(e, m) << "\n"); SASSERT(e.m_def->is_fun_macro()); auto & vars = e.m_def->get_vars(); expr_ref lhs(e.m_lhs, m); diff --git a/src/tactic/sls/sls_tactic.cpp b/src/tactic/sls/sls_tactic.cpp index 12c6083a8..613b8276d 100644 --- a/src/tactic/sls/sls_tactic.cpp +++ b/src/tactic/sls/sls_tactic.cpp @@ -113,7 +113,6 @@ static tactic * mk_preamble(ast_manager & m, params_ref const & p) { params_ref hoist_p; hoist_p.set_bool("hoist_mul", true); - // hoist_p.set_bool("hoist_cmul", true); hoist_p.set_bool("som", false); params_ref gaussian_p;