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

dl_bit_blasting: run simplifier before bit-blasting, in order to comply with its precondition

Browse source 
Signed-off-by: Nuno Lopes <t-nclaud@microsoft.com>
This commit is contained in:
Nuno Lopes 2013-03-25 14:48:22 -07:00
parent df35da1acf
commit da83a6b28c
1 changed files with 16 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

23
src/muz_qe/dl_mk_bit_blast.cpp
View file

@ -23,6 +23,7 @@ Revision History:
#include "ast_pp.h" #include "ast_pp.h"
#include "expr_safe_replace.h" #include "expr_safe_replace.h"
#include "filter_model_converter.h" #include "filter_model_converter.h"
#include "dl_mk_interp_tail_simplifier.h"
namespace datalog { namespace datalog {
@ -212,18 +213,23 @@ namespace datalog {
ast_manager & m; ast_manager & m;
params_ref m_params; params_ref m_params;
rule_ref_vector m_rules; rule_ref_vector m_rules;
mk_interp_tail_simplifier m_simplifier;
bit_blaster_rewriter m_blaster; bit_blaster_rewriter m_blaster;
expand_mkbv m_rewriter; expand_mkbv m_rewriter;
bool blast(expr_ref& fml) { bool blast(rule *r, expr_ref& fml) {
proof_ref pr(m); proof_ref pr(m);
expr_ref fml1(m), fml2(m); expr_ref fml1(m), fml2(m), fml3(m);
m_blaster(fml, fml1, pr); rule_ref r2(m_context.get_rule_manager());
m_rewriter(fml1, fml2); // We need to simplify rule before bit-blasting.
TRACE("dl", tout << mk_pp(fml, m) << " -> " << mk_pp(fml1, m) << " -> " << mk_pp(fml2, m) << "\n";); m_simplifier.transform_rule(r, r2);
if (fml2 != fml) { r2->to_formula(fml1);
fml = fml2; m_blaster(fml1, fml2, pr);
m_rewriter(fml2, fml3);
TRACE("dl", tout << mk_pp(fml, m) << " -> " << mk_pp(fml2, m) << " -> " << mk_pp(fml3, m) << "\n";);
if (fml3 != fml) {
fml = fml3;
return true; return true;
} }
else { else {
@ -241,6 +247,7 @@ namespace datalog {
m(ctx.get_manager()), m(ctx.get_manager()),
m_params(ctx.get_params().p), m_params(ctx.get_params().p),
m_rules(ctx.get_rule_manager()), m_rules(ctx.get_rule_manager()),
m_simplifier(ctx),
m_blaster(ctx.get_manager(), m_params), m_blaster(ctx.get_manager(), m_params),
m_rewriter(ctx.get_manager(), ctx, m_rules) { m_rewriter(ctx.get_manager(), ctx, m_rules) {
m_params.set_bool("blast_full", true); m_params.set_bool("blast_full", true);
@ -261,7 +268,7 @@ namespace datalog {
for (unsigned i = 0; i < sz; ++i) { for (unsigned i = 0; 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(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()) {
pr = m.mk_asserted(fml); // loses original proof of r. pr = m.mk_asserted(fml); // loses original proof of r.