mirror of
https://github.com/Z3Prover/z3
synced 2025-04-27 10:55:50 +00:00
clean up hoist rewriter
This commit is contained in:
Nikolaj Bjorner
parent
ab36f86843
commit
a34701471f
2 changed files with 39 additions and 57 deletions
|
|
@ -13,8 +13,6 @@ Author:
|
|||
|
||||
Nikolaj Bjorner (nbjorner) 2019-2-4
|
||||
|
||||
Notes:
|
||||
|
||||
--*/
|
||||
|
||||
|
||||
|
|
@ -25,19 +23,17 @@ Notes:
|
|||
|
||||
|
||||
hoist_rewriter::hoist_rewriter(ast_manager & m, params_ref const & p):
|
||||
m_manager(m), m_args1(m), m_args2(m), m_subst(m) {
|
||||
m(m), m_args1(m), m_args2(m), m_subst(m) {
|
||||
updt_params(p);
|
||||
}
|
||||
|
||||
br_status hoist_rewriter::mk_or(unsigned num_args, expr * const * es, expr_ref & result) {
|
||||
if (num_args < 2) {
|
||||
if (num_args < 2)
|
||||
return BR_FAILED;
|
||||
}
|
||||
for (unsigned i = 0; i < num_args; ++i) {
|
||||
if (!is_and(es[i], nullptr)) {
|
||||
|
||||
for (unsigned i = 0; i < num_args; ++i)
|
||||
if (!is_and(es[i], nullptr))
|
||||
return BR_FAILED;
|
||||
}
|
||||
}
|
||||
|
||||
bool turn = false;
|
||||
m_preds1.reset();
|
||||
|
|
@ -52,12 +48,10 @@ br_status hoist_rewriter::mk_or(unsigned num_args, expr * const * es, expr_ref &
|
|||
VERIFY(is_and(es[0], args[turn]));
|
||||
expr* e1, *e2;
|
||||
for (expr* e : *(args[turn])) {
|
||||
if (m().is_eq(e, e1, e2)) {
|
||||
if (m.is_eq(e, e1, e2))
|
||||
(*uf)[turn].merge(mk_var(e1), mk_var(e2));
|
||||
}
|
||||
else {
|
||||
else
|
||||
(*preds)[turn].insert(e);
|
||||
}
|
||||
}
|
||||
unsigned round = 0;
|
||||
for (unsigned j = 1; j < num_args; ++j) {
|
||||
|
|
@ -72,44 +66,39 @@ br_status hoist_rewriter::mk_or(unsigned num_args, expr * const * es, expr_ref &
|
|||
VERIFY(is_and(es[j], args[turn]));
|
||||
|
||||
for (expr* e : *args[turn]) {
|
||||
if (m().is_eq(e, e1, e2)) {
|
||||
if (m.is_eq(e, e1, e2)) {
|
||||
m_es.push_back(e1);
|
||||
m_uf0.merge(mk_var(e1), mk_var(e2));
|
||||
}
|
||||
else if ((*preds)[last].contains(e)) {
|
||||
else if ((*preds)[last].contains(e))
|
||||
(*preds)[turn].insert(e);
|
||||
}
|
||||
}
|
||||
|
||||
if ((*preds)[turn].empty() && m_es.empty()) {
|
||||
if ((*preds)[turn].empty() && m_es.empty())
|
||||
return BR_FAILED;
|
||||
}
|
||||
|
||||
m_eqs.reset();
|
||||
for (expr* e : m_es) {
|
||||
if (m_mark.is_marked(e)) {
|
||||
if (m_mark.is_marked(e))
|
||||
continue;
|
||||
}
|
||||
unsigned u = mk_var(e);
|
||||
unsigned v = u;
|
||||
m_roots.reset();
|
||||
do {
|
||||
m_mark.mark(e);
|
||||
unsigned r = (*uf)[last].find(v);
|
||||
if (m_roots.find(r, e2)) {
|
||||
m_eqs.push_back(std::make_pair(e, e2));
|
||||
}
|
||||
else {
|
||||
if (m_roots.find(r, e2))
|
||||
m_eqs.push_back({e, e2});
|
||||
else
|
||||
m_roots.insert(r, e);
|
||||
}
|
||||
v = m_uf0.next(v);
|
||||
e = mk_expr(v);
|
||||
}
|
||||
while (u != v);
|
||||
}
|
||||
reset((*uf)[turn]);
|
||||
for (auto const& p : m_eqs)
|
||||
(*uf)[turn].merge(mk_var(p.first), mk_var(p.second));
|
||||
for (auto const& [e1, e2] : m_eqs)
|
||||
(*uf)[turn].merge(mk_var(e1), mk_var(e2));
|
||||
if ((*preds)[turn].empty() && m_eqs.empty())
|
||||
return BR_FAILED;
|
||||
}
|
||||
|
|
@ -118,25 +107,23 @@ br_status hoist_rewriter::mk_or(unsigned num_args, expr * const * es, expr_ref &
|
|||
return BR_DONE;
|
||||
}
|
||||
// p & eqs & (or fmls)
|
||||
expr_ref_vector fmls(m());
|
||||
expr_ref_vector fmls(m);
|
||||
m_subst.reset();
|
||||
for (expr * p : (*preds)[turn]) {
|
||||
expr* q = nullptr;
|
||||
if (m().is_not(p, q)) {
|
||||
m_subst.insert(q, m().mk_false());
|
||||
}
|
||||
else {
|
||||
m_subst.insert(p, m().mk_true());
|
||||
}
|
||||
if (m.is_not(p, q))
|
||||
m_subst.insert(q, m.mk_false());
|
||||
else
|
||||
m_subst.insert(p, m.mk_true());
|
||||
fmls.push_back(p);
|
||||
}
|
||||
for (auto& p : m_eqs) {
|
||||
if (m().is_value(p.first))
|
||||
if (m.is_value(p.first))
|
||||
std::swap(p.first, p.second);
|
||||
m_subst.insert(p.first, p.second);
|
||||
fmls.push_back(m().mk_eq(p.first, p.second));
|
||||
fmls.push_back(m.mk_eq(p.first, p.second));
|
||||
}
|
||||
expr_ref ors(::mk_or(m(), num_args, es), m());
|
||||
expr_ref ors(::mk_or(m, num_args, es), m);
|
||||
m_subst(ors);
|
||||
fmls.push_back(ors);
|
||||
result = mk_and(fmls);
|
||||
|
|
@ -146,9 +133,8 @@ br_status hoist_rewriter::mk_or(unsigned num_args, expr * const * es, expr_ref &
|
|||
|
||||
unsigned hoist_rewriter::mk_var(expr* e) {
|
||||
unsigned v = 0;
|
||||
if (m_expr2var.find(e, v)) {
|
||||
if (m_expr2var.find(e, v))
|
||||
return v;
|
||||
}
|
||||
m_uf1.mk_var();
|
||||
v = m_uf2.mk_var();
|
||||
SASSERT(v == m_var2expr.size());
|
||||
|
|
@ -158,15 +144,14 @@ unsigned hoist_rewriter::mk_var(expr* e) {
|
|||
}
|
||||
|
||||
expr_ref hoist_rewriter::hoist_predicates(obj_hashtable<expr> const& preds, unsigned num_args, expr* const* es) {
|
||||
expr_ref result(m());
|
||||
expr_ref_vector args(m()), fmls(m());
|
||||
expr_ref result(m);
|
||||
expr_ref_vector args(m), fmls(m);
|
||||
for (unsigned i = 0; i < num_args; ++i) {
|
||||
VERIFY(is_and(es[i], &m_args1));
|
||||
fmls.reset();
|
||||
for (expr* e : m_args1) {
|
||||
for (expr* e : m_args1)
|
||||
if (!preds.contains(e))
|
||||
fmls.push_back(e);
|
||||
}
|
||||
args.push_back(::mk_and(fmls));
|
||||
}
|
||||
fmls.reset();
|
||||
|
|
@ -188,19 +173,18 @@ br_status hoist_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * c
|
|||
}
|
||||
|
||||
bool hoist_rewriter::is_and(expr * e, expr_ref_vector* args) {
|
||||
if (m().is_and(e)) {
|
||||
if (m.is_and(e)) {
|
||||
if (args) {
|
||||
args->reset();
|
||||
args->append(to_app(e)->get_num_args(), to_app(e)->get_args());
|
||||
}
|
||||
return true;
|
||||
}
|
||||
if (m().is_not(e, e) && m().is_or(e)) {
|
||||
if (m.is_not(e, e) && m.is_or(e)) {
|
||||
if (args) {
|
||||
args->reset();
|
||||
for (expr* arg : *to_app(e)) {
|
||||
args->push_back(::mk_not(m(), arg));
|
||||
}
|
||||
for (expr* arg : *to_app(e))
|
||||
args->push_back(::mk_not(m, arg));
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -26,7 +26,7 @@ Notes:
|
|||
#include "util/obj_hashtable.h"
|
||||
|
||||
class hoist_rewriter {
|
||||
ast_manager & m_manager;
|
||||
ast_manager & m;
|
||||
expr_ref_vector m_args1, m_args2;
|
||||
obj_hashtable<expr> m_preds1, m_preds2;
|
||||
basic_union_find m_uf1, m_uf2, m_uf0;
|
||||
|
|
@ -34,11 +34,9 @@ class hoist_rewriter {
|
|||
svector<std::pair<expr*,expr*>> m_eqs;
|
||||
u_map<expr*> m_roots;
|
||||
expr_safe_replace m_subst;
|
||||
obj_map<expr, unsigned> m_expr2var;
|
||||
ptr_vector<expr> m_var2expr;
|
||||
expr_mark m_mark;
|
||||
|
||||
br_status mk_or(unsigned num_args, expr * const * args, expr_ref & result);
|
||||
obj_map<expr, unsigned> m_expr2var;
|
||||
ptr_vector<expr> m_var2expr;
|
||||
expr_mark m_mark;
|
||||
|
||||
bool is_and(expr* e, expr_ref_vector* args);
|
||||
|
||||
|
|
@ -52,12 +50,12 @@ class hoist_rewriter {
|
|||
|
||||
public:
|
||||
hoist_rewriter(ast_manager & m, params_ref const & p = params_ref());
|
||||
ast_manager& m() const { return m_manager; }
|
||||
family_id get_fid() const { return m().get_basic_family_id(); }
|
||||
bool is_eq(expr * t) const { return m().is_eq(t); }
|
||||
family_id get_fid() const { return m.get_basic_family_id(); }
|
||||
bool is_eq(expr * t) const { return m.is_eq(t); }
|
||||
void updt_params(params_ref const & p) {}
|
||||
static void get_param_descrs(param_descrs & r) {}
|
||||
br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);
|
||||
br_status mk_or(unsigned num_args, expr * const * args, expr_ref & result);
|
||||
};
|
||||
|
||||
struct hoist_rewriter_cfg : public default_rewriter_cfg {
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue