mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 14:13:23 +00:00
Code Activity

horn rule bit blaster: fix propagation of output predicates when arity == 0

Browse source 
Signed-off-by: Nuno Lopes <t-nclaud@microsoft.com>
This commit is contained in:
Nuno Lopes 2013-05-15 10:50:46 -07:00
parent 878d57d139
commit e6c8149873
1 changed files with 10 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/muz_qe/dl_mk_bit_blast.cpp
View file

@ -141,13 +141,17 @@ namespace datalog {
func_decl_ref_vector const& new_funcs() const { return m_new_funcs; } func_decl_ref_vector const& new_funcs() const { return m_new_funcs; }
br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
bool found = false; if (num == 0) {
for (unsigned j = 0; !found && j < num; ++j) { if (m_src->is_output_predicate(f))
found = m_util.is_mkbv(args[j]); m_dst->set_output_predicate(f);
}
if (!found) {
return BR_FAILED; return BR_FAILED;
} }
for (unsigned i = 0; i < num; ++i) {
if (!m_util.is_mkbv(args[i]))
return BR_FAILED;
}
// //
// f(mk_bv(args),...) // f(mk_bv(args),...)
// //
@ -260,7 +264,7 @@ namespace datalog {
m_rewriter.m_cfg.set_dst(result); m_rewriter.m_cfg.set_dst(result);
for (unsigned i = 0; !m_context.canceled() && i < sz; ++i) { for (unsigned i = 0; !m_context.canceled() && i < sz; ++i) {
rule * r = source.get_rule(i); rule * r = source.get_rule(i);
r->to_formula(fml); r->to_formula(fml);
if (blast(r, fml)) { if (blast(r, fml)) {
proof_ref pr(m); proof_ref pr(m);
if (m_context.generate_proof_trace()) { if (m_context.generate_proof_trace()) {