mirror of
https://github.com/Z3Prover/z3
synced 2025-11-04 13:29:11 +00:00
Add coalesce transformer
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
d16db63e56
commit
6b414ba5cf
5 changed files with 280 additions and 5 deletions
209
lib/dl_mk_coalesce.cpp
Normal file
209
lib/dl_mk_coalesce.cpp
Normal file
|
|
@ -0,0 +1,209 @@
|
|||
/*++
|
||||
Copyright (c) 2012 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
dl_mk_coalesce.cpp
|
||||
|
||||
Abstract:
|
||||
|
||||
Coalesce rules with shared bodies.
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2012-10-15
|
||||
|
||||
Revision History:
|
||||
|
||||
|
||||
Notes:
|
||||
|
||||
Implements proof rule of the form:
|
||||
|
||||
a(x) & q(x) -> p(x) b(y) & q(y) -> p(y)
|
||||
---------------------------------------------
|
||||
(a(z) \/ b(z)) & q(z) -> p(z)
|
||||
|
||||
|
||||
--*/
|
||||
#include "dl_mk_coalesce.h"
|
||||
#include "bool_rewriter.h"
|
||||
|
||||
namespace datalog {
|
||||
|
||||
mk_coalesce::mk_coalesce(context& ctx):
|
||||
rule_transformer::plugin(50, false),
|
||||
m_ctx(ctx),
|
||||
m(ctx.get_manager()),
|
||||
rm(ctx.get_rule_manager()),
|
||||
m_sub1(m),
|
||||
m_sub2(m),
|
||||
m_idx(0)
|
||||
{}
|
||||
|
||||
void mk_coalesce::mk_pred(app_ref& pred, app* p1, app* p2) {
|
||||
SASSERT(p1->get_decl() == p2->get_decl());
|
||||
unsigned sz = p1->get_num_args();
|
||||
expr_ref_vector args(m);
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
expr* a = p1->get_arg(i);
|
||||
expr* b = p2->get_arg(i);
|
||||
SASSERT(m.get_sort(a) == m.get_sort(b));
|
||||
m_sub1.push_back(a);
|
||||
m_sub2.push_back(b);
|
||||
args.push_back(m.mk_var(m_idx++, m.get_sort(a)));
|
||||
}
|
||||
pred = m.mk_app(p1->get_decl(), args.size(), args.c_ptr());
|
||||
}
|
||||
|
||||
void mk_coalesce::extract_conjs(expr_ref_vector const& sub, rule const& rl, expr_ref& result) {
|
||||
obj_map<expr, unsigned> indices;
|
||||
bool_rewriter bwr(m);
|
||||
rule_ref r(const_cast<rule*>(&rl), rm);
|
||||
sort_ref_vector sorts(m);
|
||||
expr_ref_vector revsub(m), conjs(m);
|
||||
rl.get_vars(sorts);
|
||||
revsub.resize(sorts.size());
|
||||
svector<bool> valid(sorts.size(), true);
|
||||
for (unsigned i = 0; i < sub.size(); ++i) {
|
||||
expr* e = sub[i];
|
||||
sort* s = m.get_sort(e);
|
||||
expr_ref w(m.mk_var(i, s), m);
|
||||
if (is_var(e)) {
|
||||
unsigned v = to_var(e)->get_idx();
|
||||
SASSERT(v < valid.size());
|
||||
if (sorts[v].get()) {
|
||||
SASSERT(s == sorts[v].get());
|
||||
if (valid[v]) {
|
||||
revsub[v] = w;
|
||||
valid[v] = false;
|
||||
}
|
||||
else {
|
||||
SASSERT(revsub[v].get());
|
||||
SASSERT(m.get_sort(revsub[v].get()) == s);
|
||||
conjs.push_back(m.mk_eq(revsub[v].get(), w));
|
||||
}
|
||||
}
|
||||
}
|
||||
else {
|
||||
SASSERT(m.is_value(e));
|
||||
SASSERT(m.get_sort(e) == m.get_sort(w));
|
||||
conjs.push_back(m.mk_eq(e, w));
|
||||
}
|
||||
}
|
||||
for (unsigned i = 0; i < sorts.size(); ++i) {
|
||||
if (valid[i] && sorts[i].get() && !revsub[i].get()) {
|
||||
revsub[i] = m.mk_var(m_idx++, sorts[i].get());
|
||||
}
|
||||
}
|
||||
var_subst vs(m, false);
|
||||
for (unsigned i = r->get_uninterpreted_tail_size(); i < r->get_tail_size(); ++i) {
|
||||
vs(r->get_tail(i), revsub.size(), revsub.c_ptr(), result);
|
||||
conjs.push_back(result);
|
||||
}
|
||||
bwr.mk_and(conjs.size(), conjs.c_ptr(), result);
|
||||
}
|
||||
|
||||
void mk_coalesce::merge_rules(rule_ref& tgt, rule const& src) {
|
||||
SASSERT(same_body(*tgt.get(), src));
|
||||
m_sub1.reset();
|
||||
m_sub2.reset();
|
||||
m_idx = 0;
|
||||
app_ref pred(m), head(m);
|
||||
expr_ref fml1(m), fml2(m), fml(m);
|
||||
app_ref_vector tail(m);
|
||||
sort_ref_vector sorts1(m), sorts2(m);
|
||||
expr_ref_vector conjs1(m), conjs(m);
|
||||
rule_ref res(rm);
|
||||
bool_rewriter bwr(m);
|
||||
svector<bool> is_neg;
|
||||
tgt->get_vars(sorts1);
|
||||
src.get_vars(sorts2);
|
||||
|
||||
mk_pred(head, src.get_head(), tgt->get_head());
|
||||
for (unsigned i = 0; i < src.get_uninterpreted_tail_size(); ++i) {
|
||||
mk_pred(pred, src.get_tail(i), tgt->get_tail(i));
|
||||
tail.push_back(pred);
|
||||
is_neg.push_back(src.is_neg_tail(i));
|
||||
}
|
||||
extract_conjs(m_sub1, src, fml1);
|
||||
extract_conjs(m_sub2, *tgt.get(), fml2);
|
||||
bwr.mk_or(fml1, fml2, fml);
|
||||
SASSERT(is_app(fml));
|
||||
tail.push_back(to_app(fml));
|
||||
is_neg.push_back(false);
|
||||
res = rm.mk(head, tail.size(), tail.c_ptr(), is_neg.c_ptr(), tgt->name());
|
||||
if (m_pc) {
|
||||
src.to_formula(fml1);
|
||||
tgt->to_formula(fml2);
|
||||
res->to_formula(fml);
|
||||
#if 0
|
||||
sort* ps = m.mk_proof_sort();
|
||||
sort* domain[3] = { ps, ps, m.mk_bool_sort() };
|
||||
func_decl* merge = m.mk_func_decl(symbol("merge-clauses"), 3, domain, ps); // TBD: ad-hoc proof rule
|
||||
expr* args[3] = { m.mk_asserted(fml1), m.mk_asserted(fml2), fml };
|
||||
m_pc->insert(m.mk_app(merge, 3, args));
|
||||
#else
|
||||
svector<std::pair<unsigned, unsigned> > pos;
|
||||
vector<expr_ref_vector> substs;
|
||||
proof* p = m.mk_asserted(fml1);
|
||||
m_pc->insert(m.mk_hyper_resolve(1, &p, fml, pos, substs));
|
||||
#endif
|
||||
}
|
||||
tgt = res;
|
||||
}
|
||||
|
||||
bool mk_coalesce::same_body(rule const& r1, rule const& r2) const {
|
||||
SASSERT(r1.get_decl() == r2.get_decl());
|
||||
unsigned sz = r1.get_uninterpreted_tail_size();
|
||||
if (sz != r2.get_uninterpreted_tail_size()) {
|
||||
return false;
|
||||
}
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
if (r1.get_decl(i) != r2.get_decl(i)) {
|
||||
return false;
|
||||
}
|
||||
if (r1.is_neg_tail(i) != r2.is_neg_tail(i)) {
|
||||
return false;
|
||||
}
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
rule_set * mk_coalesce::operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) {
|
||||
m_pc = 0;
|
||||
ref<replace_proof_converter> rpc;
|
||||
if (pc) {
|
||||
rpc = alloc(replace_proof_converter, m);
|
||||
m_pc = rpc.get();
|
||||
}
|
||||
rule_set* rules = alloc(rule_set, m_ctx);
|
||||
rule_set::decl2rules::iterator it = source.begin_grouped_rules(), end = source.end_grouped_rules();
|
||||
bool change = false;
|
||||
for (; it != end; ++it) {
|
||||
func_decl* p = it->m_key;
|
||||
rule_ref_vector d_rules(rm);
|
||||
d_rules.append(it->m_value->size(), it->m_value->c_ptr());
|
||||
for (unsigned i = 0; i < d_rules.size(); ++i) {
|
||||
rule_ref r1(d_rules[i].get(), rm);
|
||||
for (unsigned j = i + 1; j < d_rules.size(); ++j) {
|
||||
if (same_body(*r1.get(), *d_rules[j].get())) {
|
||||
merge_rules(r1, *d_rules[j].get());
|
||||
d_rules[j] = d_rules.back();
|
||||
d_rules.pop_back();
|
||||
change = true;
|
||||
--j;
|
||||
}
|
||||
}
|
||||
rules->add_rule(r1.get());
|
||||
}
|
||||
}
|
||||
if (pc) {
|
||||
pc = concat(pc.get(), rpc.get());
|
||||
}
|
||||
return rules;
|
||||
}
|
||||
|
||||
};
|
||||
|
||||
|
||||
62
lib/dl_mk_coalesce.h
Normal file
62
lib/dl_mk_coalesce.h
Normal file
|
|
@ -0,0 +1,62 @@
|
|||
|
||||
/*++
|
||||
Copyright (c) 2012 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
dl_mk_coalesce.h
|
||||
|
||||
Abstract:
|
||||
|
||||
Coalesce rules with shared bodies.
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2012-10-15
|
||||
|
||||
Revision History:
|
||||
|
||||
--*/
|
||||
#ifndef _DL_MK_COALESCE_H_
|
||||
#define _DL_MK_COALESCE_H_
|
||||
|
||||
#include"dl_context.h"
|
||||
#include"dl_rule_set.h"
|
||||
#include"uint_set.h"
|
||||
#include"dl_rule_transformer.h"
|
||||
#include"dl_mk_rule_inliner.h"
|
||||
|
||||
namespace datalog {
|
||||
|
||||
/**
|
||||
\brief Implements an unfolding transformation.
|
||||
*/
|
||||
class mk_coalesce : public rule_transformer::plugin {
|
||||
context& m_ctx;
|
||||
ast_manager& m;
|
||||
rule_manager& rm;
|
||||
expr_ref_vector m_sub1, m_sub2;
|
||||
unsigned m_idx;
|
||||
replace_proof_converter* m_pc;
|
||||
|
||||
void mk_pred(app_ref& pred, app* p1, app* p2);
|
||||
|
||||
void extract_conjs(expr_ref_vector const& sub, rule const& rl, expr_ref& result);
|
||||
|
||||
bool same_body(rule const& r1, rule const& r2) const;
|
||||
|
||||
void merge_rules(rule_ref& tgt, rule const& src);
|
||||
|
||||
public:
|
||||
/**
|
||||
\brief Create coalesced rules.
|
||||
*/
|
||||
mk_coalesce(context & ctx);
|
||||
|
||||
rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc);
|
||||
};
|
||||
|
||||
};
|
||||
|
||||
#endif /* _DL_MK_COALESCE_H_ */
|
||||
|
||||
|
|
@ -21,7 +21,7 @@ Revision History:
|
|||
namespace datalog {
|
||||
|
||||
mk_unfold::mk_unfold(context& ctx):
|
||||
rule_transformer::plugin(0, false),
|
||||
rule_transformer::plugin(100, false),
|
||||
m_ctx(ctx),
|
||||
m(ctx.get_manager()),
|
||||
rm(ctx.get_rule_manager()),
|
||||
|
|
|
|||
|
|
@ -542,6 +542,7 @@
|
|||
<ClCompile Include="dl_costs.cpp" />
|
||||
<ClCompile Include="dl_cmds.cpp" />
|
||||
<ClCompile Include="dl_decl_plugin.cpp" />
|
||||
<ClCompile Include="dl_mk_coalesce.cpp" />
|
||||
<ClCompile Include="dl_mk_coi_filter.cpp" />
|
||||
<ClCompile Include="dl_mk_explanations.cpp" />
|
||||
<ClCompile Include="dl_mk_partial_equiv.cpp" />
|
||||
|
|
@ -998,6 +999,7 @@
|
|||
<ClInclude Include="diff_logic.h" />
|
||||
<ClInclude Include="dl_decl_plugin.h" />
|
||||
<ClInclude Include="dl_mk_bit_blast.h" />
|
||||
<ClInclude Include="dl_mk_coalesce.h" />
|
||||
<ClInclude Include="dl_mk_slice.h" />
|
||||
<ClInclude Include="dl_mk_coi_filter.h" />
|
||||
<ClInclude Include="dl_mk_explanations.h" />
|
||||
|
|
|
|||
|
|
@ -31,6 +31,7 @@ Revision History:
|
|||
#include "dl_rule_set.h"
|
||||
#include "dl_mk_slice.h"
|
||||
#include "dl_mk_unfold.h"
|
||||
#include "dl_mk_coalesce.h"
|
||||
|
||||
using namespace pdr;
|
||||
|
||||
|
|
@ -120,11 +121,12 @@ lbool dl_interface::query(expr * query) {
|
|||
|
||||
if (m_ctx.get_params().get_uint(":unfold-rules",0) > 0) {
|
||||
unsigned num_unfolds = m_ctx.get_params().get_uint(":unfold-rules",0);
|
||||
datalog::rule_transformer transformer(m_ctx);
|
||||
datalog::mk_unfold* unfold = alloc(datalog::mk_unfold, m_ctx);
|
||||
transformer.register_plugin(unfold);
|
||||
datalog::rule_transformer transformer1(m_ctx), transformer2(m_ctx);
|
||||
transformer1.register_plugin(alloc(datalog::mk_coalesce, m_ctx));
|
||||
m_ctx.transform_rules(transformer1, mc, pc);
|
||||
transformer2.register_plugin(alloc(datalog::mk_unfold, m_ctx));
|
||||
while (num_unfolds > 0) {
|
||||
m_ctx.transform_rules(transformer, mc, pc);
|
||||
m_ctx.transform_rules(transformer2, mc, pc);
|
||||
--num_unfolds;
|
||||
}
|
||||
}
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue