From 0daa05aab224dd6e506ca65e2de501f2b703945a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 18 Dec 2023 13:51:45 -0800 Subject: [PATCH] add ability to log selected bv rewrites --- src/ast/rewriter/bv_rewriter.cpp | 73 ++++++++++++++++++++------------ 1 file changed, 47 insertions(+), 26 deletions(-) diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp index fc672584efe..64ecc5f5384 100644 --- a/src/ast/rewriter/bv_rewriter.cpp +++ b/src/ast/rewriter/bv_rewriter.cpp @@ -20,8 +20,9 @@ Module Name: #include "ast/rewriter/bv_rewriter.h" #include "ast/rewriter/poly_rewriter_def.h" #include "ast/rewriter/bool_rewriter.h" -#include "ast/ast_smt2_pp.h" #include "ast/ast_lt.h" +#include "ast/ast_pp.h" + void bv_rewriter::updt_local_params(params_ref const & _p) { @@ -54,45 +55,58 @@ void bv_rewriter::get_param_descrs(param_descrs & r) { br_status bv_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) { SASSERT(f->get_family_id() == get_fid()); + br_status st = BR_FAILED; switch(f->get_decl_kind()) { case OP_BIT0: SASSERT(num_args == 0); result = mk_zero(1); return BR_DONE; case OP_BIT1: SASSERT(num_args == 0); result = mk_one(1); return BR_DONE; case OP_ULEQ: SASSERT(num_args == 2); - return mk_ule(args[0], args[1], result); + st = mk_ule(args[0], args[1], result); + break; case OP_UGEQ: SASSERT(num_args == 2); - return mk_uge(args[0], args[1], result); + st = mk_uge(args[0], args[1], result); + break; case OP_ULT: SASSERT(num_args == 2); - return mk_ult(args[0], args[1], result); + st = mk_ult(args[0], args[1], result); + break; case OP_UGT: SASSERT(num_args == 2); - return mk_ult(args[1], args[0], result); + st = mk_ult(args[1], args[0], result); + break; case OP_SLEQ: SASSERT(num_args == 2); - return mk_sle(args[0], args[1], result); + st = mk_sle(args[0], args[1], result); + break; case OP_SGEQ: SASSERT(num_args == 2); - return mk_sge(args[0], args[1], result); + st = mk_sge(args[0], args[1], result); + break; case OP_SLT: SASSERT(num_args == 2); - return mk_slt(args[0], args[1], result); + st = mk_slt(args[0], args[1], result); + break; case OP_SGT: SASSERT(num_args == 2); - return mk_slt(args[1], args[0], result); + st = mk_slt(args[1], args[0], result); + break; case OP_BADD: SASSERT(num_args > 0); - return mk_bv_add(num_args, args, result); + st = mk_bv_add(num_args, args, result); + break; case OP_BMUL: SASSERT(num_args > 0); - return mk_bv_mul(num_args, args, result); + st = mk_bv_mul(num_args, args, result); + break; case OP_BSUB: SASSERT(num_args > 0); - return mk_sub(num_args, args, result); + st = mk_sub(num_args, args, result); + break; case OP_BNEG: SASSERT(num_args == 1); - return mk_uminus(args[0], result); + st = mk_uminus(args[0], result); + break; case OP_BNEG_OVFL: SASSERT(num_args == 1); return mk_bvneg_overflow(args[0], result); @@ -220,6 +234,13 @@ br_status bv_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * cons default: return BR_FAILED; } + + CTRACE("bv", st != BR_FAILED, tout << mk_pp(f, m) << "\n"; + for (unsigned i = 0; i < num_args; ++i) + tout << " " << mk_bounded_pp(args[i], m) << "\n"; + tout << mk_bounded_pp(result, m, 3) << "\n"); + + return st; } br_status bv_rewriter::mk_ule(expr * a, expr * b, expr_ref & result) { @@ -534,6 +555,7 @@ br_status bv_rewriter::mk_leq_core(bool is_signed, expr * a, expr * b, expr_ref result = m.mk_and(result, m_util.mk_ule(m_util.mk_numeral(r1-r2, sz), a2)); else if (r1 < r2) result = m.mk_or(result, m_util.mk_ule(m_util.mk_numeral(r1-r2, sz), a2)); + verbose_stream() << result << "\n"; return BR_REWRITE2; } @@ -541,7 +563,7 @@ br_status bv_rewriter::mk_leq_core(bool is_signed, expr * a, expr * b, expr_ref const br_status cst = rw_leq_concats(is_signed, a, b, result); if (cst != BR_FAILED) { TRACE("le_extra", tout << (is_signed ? "bv_sle\n" : "bv_ule\n") - << mk_ismt2_pp(a, m, 2) << "\n" << mk_ismt2_pp(b, m, 2) << "\n--->\n"<< mk_ismt2_pp(result, m, 2) << "\n";); + << mk_pp(a, m, 2) << "\n" << mk_pp(b, m, 2) << "\n--->\n"<< mk_pp(result, m, 2) << "\n";); return cst; } } @@ -550,7 +572,7 @@ br_status bv_rewriter::mk_leq_core(bool is_signed, expr * a, expr * b, expr_ref const br_status cst = rw_leq_overflow(is_signed, a, b, result); if (cst != BR_FAILED) { TRACE("le_extra", tout << (is_signed ? "bv_sle\n" : "bv_ule\n") - << mk_ismt2_pp(a, m, 2) << "\n" << mk_ismt2_pp(b, m, 2) << "\n--->\n"<< mk_ismt2_pp(result, m, 2) << "\n";); + << mk_pp(a, m, 2) << "\n" << mk_pp(b, m, 2) << "\n--->\n"<< mk_pp(result, m, 2) << "\n";); return cst; } } @@ -802,8 +824,8 @@ br_status bv_rewriter::mk_extract(unsigned high, unsigned low, expr * arg, expr_ const unsigned ep_rm = propagate_extract(high, arg, ep_res); if (ep_rm != 0) { result = m_mk_extract(high, low, ep_res); - TRACE("extract_prop", tout << mk_ismt2_pp(arg, m) << "\n[" << high <<"," << low << "]\n" << ep_rm << "---->\n" - << mk_ismt2_pp(result.get(), m) << "\n";); + TRACE("extract_prop", tout << mk_pp(arg, m) << "\n[" << high <<"," << low << "]\n" << ep_rm << "---->\n" + << mk_pp(result.get(), m) << "\n";); return BR_REWRITE2; } } @@ -1132,7 +1154,7 @@ br_status bv_rewriter::mk_bv_udiv_core(expr * arg1, expr * arg2, bool hi_div0, e m_util.mk_bv_udiv0(arg1), m_util.mk_bv_udiv_i(arg1, arg2)); - TRACE("bv_udiv", tout << mk_ismt2_pp(arg1, m) << "\n" << mk_ismt2_pp(arg2, m) << "\n---->\n" << mk_ismt2_pp(result, m) << "\n";); + TRACE("bv_udiv", tout << mk_pp(arg1, m) << "\n" << mk_pp(arg2, m) << "\n---->\n" << mk_pp(result, m) << "\n";); return BR_REWRITE2; } @@ -1792,8 +1814,8 @@ br_status bv_rewriter::mk_bv_or(unsigned num, expr * const * args, expr_ref & re std::reverse(exs.begin(), exs.end()); result = m_util.mk_concat(exs.size(), exs.data()); TRACE("mask_bug", - tout << "(assert (distinct (bvor (_ bv" << old_v1 << " " << sz << ")\n" << mk_ismt2_pp(t, m) << ")\n"; - tout << mk_ismt2_pp(result, m) << "))\n";); + tout << "(assert (distinct (bvor (_ bv" << old_v1 << " " << sz << ")\n" << mk_pp(t, m) << ")\n"; + tout << mk_pp(result, m) << "))\n";); return BR_REWRITE2; } @@ -2463,7 +2485,7 @@ br_status bv_rewriter::mk_blast_eq_value(expr * lhs, expr * rhs, expr_ref & resu unsigned sz = get_bv_size(lhs); if (sz == 1) return BR_FAILED; - TRACE("blast_eq_value", tout << "sz: " << sz << "\n" << mk_ismt2_pp(lhs, m) << "\n";); + TRACE("blast_eq_value", tout << "sz: " << sz << "\n" << mk_pp(lhs, m) << "\n";); if (is_numeral(lhs)) std::swap(lhs, rhs); @@ -2573,7 +2595,6 @@ void bv_rewriter::mk_t1_add_t2_eq_c(expr * t1, expr * t2, expr * c, expr_ref & r result = m.mk_eq(t1, m_util.mk_bv_sub(c, t2)); } -#include "ast/ast_pp.h" bool bv_rewriter::isolate_term(expr* lhs, expr* rhs, expr_ref& result) { if (!m_util.is_numeral(lhs) || !is_add(rhs)) { @@ -2730,13 +2751,13 @@ br_status bv_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) { st = mk_mul_eq(lhs, rhs, result); if (st != BR_FAILED) { - TRACE("mk_mul_eq", tout << mk_ismt2_pp(lhs, m) << "\n=\n" << mk_ismt2_pp(rhs, m) << "\n----->\n" << mk_ismt2_pp(result,m) << "\n";); + TRACE("mk_mul_eq", tout << mk_pp(lhs, m) << "\n=\n" << mk_pp(rhs, m) << "\n----->\n" << mk_pp(result,m) << "\n";); return st; } st = mk_mul_eq(rhs, lhs, result); if (st != BR_FAILED) { - TRACE("mk_mul_eq", tout << mk_ismt2_pp(lhs, m) << "\n=\n" << mk_ismt2_pp(rhs, m) << "\n----->\n" << mk_ismt2_pp(result,m) << "\n";); + TRACE("mk_mul_eq", tout << mk_pp(lhs, m) << "\n=\n" << mk_pp(rhs, m) << "\n----->\n" << mk_pp(result,m) << "\n";); return st; } @@ -2851,8 +2872,8 @@ bool bv_rewriter::is_eq_bit(expr * t, expr * & x, unsigned & val) { br_status bv_rewriter::mk_ite_core(expr * c, expr * t, expr * e, expr_ref & result) { - TRACE("bv_ite", tout << "mk_ite_core:\n" << mk_ismt2_pp(c, m) << "?\n" - << mk_ismt2_pp(t, m) << "\n:" << mk_ismt2_pp(e, m) << "\n";); + TRACE("bv_ite", tout << "mk_ite_core:\n" << mk_pp(c, m) << "?\n" + << mk_pp(t, m) << "\n:" << mk_pp(e, m) << "\n";); if (m.are_equal(t, e)) { result = e; return BR_REWRITE1;