mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Code Activity

Transformation to eliminate term-ite expressions from DL rules

Browse source
This commit is contained in:
Arie Gurfinkel 2018-06-30 14:33:04 -04:00
parent 6d75c31468
commit 5d1149adb2
6 changed files with 107 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/muz/base/dl_context.cpp
View file

@ -308,6 +308,9 @@ namespace datalog {
bool context::array_blast() const { return m_params->xform_array_blast(); }
bool context::array_blast_full() const { return m_params->xform_array_blast_full(); }
bool context::elim_term_ite() const {return m_params->xform_elim_term_ite();}
unsigned context::blast_term_ite_inflation() const {
return m_params->xform_elim_term_ite_inflation();
}
void context::register_finite_sort(sort * s, sort_kind k) {

1
src/muz/base/dl_context.h
View file

@ -281,6 +281,7 @@ namespace datalog {
bool array_blast() const;
bool array_blast_full() const;
bool elim_term_ite() const;
unsigned blast_term_ite_inflation() const;
void register_finite_sort(sort * s, sort_kind k);

3
src/muz/base/fp_params.pyg
View file

@ -132,7 +132,8 @@ def_module_params('fp',
('spacer.use_derivations', BOOL, True, 'SPACER: using derivation mechanism to cache intermediate results for non-linear rules'),
('xform.array_blast', BOOL, False, "try to eliminate local array terms using Ackermannization -- some array terms may remain"),
('xform.array_blast_full', BOOL, False, "eliminate all local array variables by QE"),
('xform.elim_term_ite', BOOL, False, "Eliminate term-ite expressions"),
('xform.elim_term_ite', BOOL, False, 'Eliminate term-ite expressions'),
('xform.elim_term_ite.inflation', UINT, 3, 'Maximum inflation for non-Boolean ite-terms blasting: 0 (none), k (multiplicative)'),
('spacer.propagate', BOOL, True, 'Enable propagate/pushing phase'),
('spacer.max_level', UINT, UINT_MAX, "Maximum level to explore"),
('spacer.elim_aux', BOOL, True, "Eliminate auxiliary variables in reachability facts"),

108
src/muz/transforms/dl_mk_elim_term_ite.cpp
View file

@ -20,43 +20,117 @@ Revision History:
#include "muz/transforms/dl_mk_elim_term_ite.h"
#include "tactic/core/blast_term_ite_tactic.h"
#include "ast/ast_util.h"
#include "ast/expr_abstract.h"
#include "tactic/tactic.h"
#include "tactic/core/elim_term_ite_tactic.h"
namespace {
struct uninterp_const_collector {
app_ref_vector &m_consts;
uninterp_const_collector(app_ref_vector &v) : m_consts(v) {}
void operator()(var *v) {}
void operator()(quantifier *n) {}
void operator()(expr *a){}
void operator()(app *a){
if (is_uninterp_const(a)) {m_consts.push_back(a);};
}
};
void collect_uninterp_consts(expr *e, app_ref_vector &v) {
uninterp_const_collector c(v);
quick_for_each_expr(c, e);
}
struct term_ite_proc {
class found{};
ast_manager &m;
term_ite_proc(ast_manager &m) : m(m) {}
void operator()(var *v) {}
void operator()(quantifier *n) {}
void operator()(expr *a){}
void operator()(app *a){
if (m.is_term_ite(a)) throw found();
}
};
bool has_term_ite(expr *e, ast_manager& m) {
term_ite_proc f(m);
try {
quick_for_each_expr(f, e);
} catch (term_ite_proc::found) {
return true;
}
return false;
}
bool has_term_ite(expr_ref &e) { return has_term_ite(e, e.m());}
}
namespace datalog {
mk_elim_term_ite::mk_elim_term_ite(context & ctx, unsigned priority) :
rule_transformer::plugin(priority, false),
m_ctx(ctx),
m(ctx.get_manager()),
rm(ctx.get_rule_manager()) {}
rm(ctx.get_rule_manager()),
m_ground(m) {}
mk_elim_term_ite::~mk_elim_term_ite() {}
expr_ref mk_elim_term_ite::ground(expr_ref &e) {
expr_free_vars fv;
fv(e);
if (m_ground.size() < fv.size())
m_ground.resize(fv.size());
for (unsigned i = 0, sz = fv.size(); i < sz; ++i) {
if (fv[i] && !m_ground.get(i))
m_ground[i] = m.mk_fresh_const("c", fv[i]);
}
var_subst vsub(m, false);
return vsub(e, m_ground.size(), m_ground.c_ptr());
}
bool mk_elim_term_ite::elim(rule &r, rule_set &new_rules){
m_ground.reset();
th_rewriter rw(m);
unsigned utsz = r.get_uninterpreted_tail_size();
unsigned tsz = r.get_tail_size();
expr_ref_vector new_conjs(m);
expr_ref tmp(m);
bool change = false;
for (unsigned i = utsz; i < tsz; ++i)
new_conjs.push_back(r.get_tail(i));
flatten_and(new_conjs);
expr_ref fml1(m), fml2(m), old_body(m), body(m), head(m);
expr_ref fml1(m), fml2(m), body(m), head(m);
// blast ite
old_body = m.mk_and(new_conjs.size(), new_conjs.c_ptr());
body = old_body;
blast_term_ite(body, 2);
change = old_body != body;
if (!change) {
body = m.mk_and(new_conjs.size(), new_conjs.c_ptr());
if (!has_term_ite(body)) {
TRACE("dl_term_ite", tout << "No term-ite, skipping a rule\n";);
new_rules.add_rule(&r);
return false;
}
new_conjs.reset();
blast_term_ite(body, m_ctx.blast_term_ite_inflation());
// simplify body
rw(body);
if (!has_term_ite(body)) {
head = r.get_head();
fml2 = m.mk_implies(body, head);
proof_ref p(m);
rm.mk_rule(fml2, p, new_rules, r.name());
rm.mk_rule_rewrite_proof(r, *new_rules.last());
TRACE("dl_term_ite", tout << "No term-ite after blast_term_ite\n";);
return true;
}
TRACE("dl_term_ite",
tout << "Rule has term-ite after blasting, starting elimination\n";);
body = ground(body);
// elim ite
tactic_ref elim_term_ite = mk_elim_term_ite_tactic(m);
goal_ref goal = alloc(class goal, m);
@ -72,21 +146,33 @@ namespace datalog {
if (new_goal->num_exprs() != sz) {
new_conjs.reset();
new_goal->get_formulas(new_conjs);
flatten_and(new_conjs);
}
}
expr_ref_vector conjs(m);
for (unsigned i = 0; i < utsz; ++i)
conjs.push_back(r.get_tail(i));
for (unsigned i = 0; i < utsz; ++i) {
tmp = r.get_tail(i);
tmp = ground(tmp);
conjs.push_back(tmp);
}
conjs.append(new_conjs);
body = mk_and(conjs);
rw(body);
head = r.get_head();
head = ground(head);
fml2 = m.mk_implies(body, head);
SASSERT(!has_term_ite(fml2));
app_ref_vector consts(m);
collect_uninterp_consts(fml2, consts);
fml2 = mk_forall(m, consts.size(), consts.c_ptr(), fml2);
proof_ref p(m);
rm.mk_rule(fml2, p, new_rules, r.name());
rm.mk_rule_rewrite_proof(r, *new_rules.last());
TRACE("dl_term_ite", tout << "New rule: " << fml2 << "\n";);
return true;
}

3
src/muz/transforms/dl_mk_elim_term_ite.h
View file

@ -29,7 +29,10 @@ namespace datalog {
ast_manager &m;
rule_manager &rm;
expr_ref_vector m_ground;
bool elim(rule &r, rule_set &new_rules);
expr_ref ground(expr_ref &e);
public:
mk_elim_term_ite(context &ctx, unsigned priority);
~mk_elim_term_ite() override;

2
src/muz/transforms/dl_transforms.cpp
View file

@ -97,7 +97,7 @@ namespace datalog {
transf.register_plugin(alloc(datalog::mk_magic_symbolic, ctx, 36020));
}
transf.register_plugin(alloc(datalog::mk_elim_term_ite, ctx, 34999));
transf.register_plugin(alloc(datalog::mk_elim_term_ite, ctx, 35010));
ctx.transform_rules(transf);
}
}