mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 18:05:21 +00:00
Code Activity

report which operator bit-blast failed on (#5459)

Browse source
This commit is contained in:
Jamey Sharp 2021-08-08 15:53:07 -07:00 committed by GitHub
parent 1d3ee70af4
commit 5de5f5a442
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 7 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp
View file

@ -358,8 +358,11 @@ MK_PARAMETRIC_UNARY_REDUCE(reduce_sign_extend, mk_sign_extend);
result = mk_mkbv(m_out);
}
void throw_unsupported() {
throw rewriter_exception("operator is not supported, you must simplify the goal before applying bit-blasting");
void throw_unsupported(func_decl * f) {
std::string msg = "operator ";
msg += f->get_name().str();
msg += " is not supported, you must simplify the goal before applying bit-blasting";
throw rewriter_exception(std::move(msg));
}
void blast_bv_term(expr * t, expr_ref & result, proof_ref & result_pr) {
@ -425,7 +428,7 @@ MK_PARAMETRIC_UNARY_REDUCE(reduce_sign_extend, mk_sign_extend);
case OP_BUREM:
case OP_BSMOD:
if (m_blast_mul)
throw_unsupported(); // must simplify to DIV_I AND DIV0
throw_unsupported(f); // must simplify to DIV_I AND DIV0
return BR_FAILED; // keep them
case OP_BSDIV0:
@ -549,7 +552,7 @@ MK_PARAMETRIC_UNARY_REDUCE(reduce_sign_extend, mk_sign_extend);
default:
TRACE("bit_blaster", tout << "non-supported operator: " << f->get_name() << "\n";
for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m()) << std::endl;);
throw_unsupported();
throw_unsupported(f);
}
}