mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-03 21:09:11 +00:00
Code Activity

add ability to log selected bv rewrites

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-12-18 13:51:45 -08:00
parent dff419a7cb
commit 0daa05aab2
1 changed files with 47 additions and 26 deletions
Download patch file Download diff file Expand all files Collapse all files

73
src/ast/rewriter/bv_rewriter.cpp
View file

@ -20,8 +20,9 @@ Notes:
#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;