mirror of
https://github.com/Z3Prover/z3
synced 2025-04-05 09:04:07 +00:00
remove hoist functionality
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
bd8bed1759
commit
ea3628e50b
|
|
@ -23,7 +23,6 @@ z3_add_component(rewriter
|
|||
factor_rewriter.cpp
|
||||
fpa_rewriter.cpp
|
||||
func_decl_replace.cpp
|
||||
hoist_rewriter.cpp
|
||||
inj_axiom.cpp
|
||||
label_rewriter.cpp
|
||||
macro_replacer.cpp
|
||||
|
|
|
|||
|
|
@ -34,7 +34,6 @@ void bool_rewriter::updt_params(params_ref const & _p) {
|
|||
m_blast_distinct = p.blast_distinct();
|
||||
m_blast_distinct_threshold = p.blast_distinct_threshold();
|
||||
m_ite_extra_rules = p.ite_extra_rules();
|
||||
m_hoist.set_elim_and(m_elim_and);
|
||||
}
|
||||
|
||||
void bool_rewriter::get_param_descrs(param_descrs & r) {
|
||||
|
|
@ -270,28 +269,6 @@ br_status bool_rewriter::mk_nflat_or_core(unsigned num_args, expr * const * args
|
|||
return BR_DONE;
|
||||
}
|
||||
|
||||
#if 0
|
||||
br_status st;
|
||||
expr_ref r(m());
|
||||
st = m_hoist.mk_or(buffer.size(), buffer.data(), r);
|
||||
if (st != BR_FAILED) {
|
||||
m_counts1.reserve(m().get_num_asts() + 1);
|
||||
m_counts2.reserve(m().get_num_asts() + 1);
|
||||
get_num_internal_exprs(m_counts1, m_todo1, r);
|
||||
for (unsigned i = 0; i < num_args; ++i)
|
||||
get_num_internal_exprs(m_counts2, m_todo2, args[i]);
|
||||
unsigned count1 = count_internal_nodes(m_counts1, m_todo1);
|
||||
unsigned count2 = count_internal_nodes(m_counts2, m_todo2);
|
||||
if (count1 > count2)
|
||||
st = BR_FAILED;
|
||||
}
|
||||
if (st != BR_FAILED)
|
||||
result = r;
|
||||
if (st == BR_DONE)
|
||||
return BR_REWRITE1;
|
||||
if (st != BR_FAILED)
|
||||
return st;
|
||||
#endif
|
||||
if (s) {
|
||||
if (m_sort_disjunctions) {
|
||||
ast_lt lt;
|
||||
|
|
|
|||
|
|
@ -20,7 +20,6 @@ Notes:
|
|||
|
||||
#include "ast/ast.h"
|
||||
#include "ast/rewriter/rewriter.h"
|
||||
#include "ast/rewriter/hoist_rewriter.h"
|
||||
#include "util/params.h"
|
||||
|
||||
/**
|
||||
|
|
@ -51,7 +50,6 @@ Notes:
|
|||
*/
|
||||
class bool_rewriter {
|
||||
ast_manager & m_manager;
|
||||
hoist_rewriter m_hoist;
|
||||
bool m_flat_and_or = false;
|
||||
bool m_sort_disjunctions = true;
|
||||
bool m_local_ctx = false;
|
||||
|
|
@ -84,7 +82,7 @@ class bool_rewriter {
|
|||
void push_new_arg(expr* arg, expr_ref_vector& new_args, expr_fast_mark1& neg_lits, expr_fast_mark2& pos_lits);
|
||||
|
||||
public:
|
||||
bool_rewriter(ast_manager & m, params_ref const & p = params_ref()):m_manager(m), m_hoist(m), m_local_ctx_cost(0) {
|
||||
bool_rewriter(ast_manager & m, params_ref const & p = params_ref()):m_manager(m), m_local_ctx_cost(0) {
|
||||
updt_params(p);
|
||||
}
|
||||
ast_manager & m() const { return m_manager; }
|
||||
|
|
|
|||
|
|
@ -1,256 +0,0 @@
|
|||
/*++
|
||||
Copyright (c) 2019 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
hoist_rewriter.cpp
|
||||
|
||||
Abstract:
|
||||
|
||||
Hoist predicates over disjunctions
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2019-2-4
|
||||
|
||||
--*/
|
||||
|
||||
|
||||
#include "ast/rewriter/hoist_rewriter.h"
|
||||
#include "ast/rewriter/bool_rewriter.h"
|
||||
#include "ast/ast_util.h"
|
||||
#include "ast/ast_pp.h"
|
||||
#include "ast/ast_ll_pp.h"
|
||||
|
||||
hoist_rewriter::hoist_rewriter(ast_manager & m, params_ref const & p):
|
||||
m(m), m_args1(m), m_args2(m), m_refs(m), m_subst(m) {
|
||||
updt_params(p);
|
||||
}
|
||||
|
||||
expr_ref hoist_rewriter::mk_and(expr_ref_vector const& args) {
|
||||
if (m_elim_and) {
|
||||
expr_ref_vector negs(m);
|
||||
for (expr* a : args)
|
||||
if (m.is_false(a))
|
||||
return expr_ref(m.mk_false(), m);
|
||||
else if (m.is_true(a))
|
||||
continue;
|
||||
else
|
||||
negs.push_back(::mk_not(m, a));
|
||||
return ::mk_not(mk_or(negs));
|
||||
}
|
||||
else
|
||||
return ::mk_and(args);
|
||||
}
|
||||
|
||||
expr_ref hoist_rewriter::mk_or(expr_ref_vector const& args) {
|
||||
return ::mk_or(args);
|
||||
}
|
||||
|
||||
br_status hoist_rewriter::mk_or(unsigned num_args, expr * const * es, expr_ref & result) {
|
||||
if (num_args < 2)
|
||||
return BR_FAILED;
|
||||
|
||||
for (unsigned i = 0; i < num_args; ++i)
|
||||
if (!is_and(es[i], nullptr))
|
||||
return BR_FAILED;
|
||||
|
||||
bool turn = false;
|
||||
m_preds1.reset();
|
||||
m_preds2.reset();
|
||||
m_uf1.reset();
|
||||
m_uf2.reset();
|
||||
m_expr2var.reset();
|
||||
m_var2expr.reset();
|
||||
basic_union_find* uf[2] = { &m_uf1, &m_uf2 };
|
||||
obj_hashtable<expr>* preds[2] = { &m_preds1, &m_preds2 };
|
||||
expr_ref_vector* args[2] = { &m_args1, &m_args2 };
|
||||
VERIFY(is_and(es[0], args[turn]));
|
||||
expr* e1, *e2;
|
||||
for (expr* e : *(args[turn])) {
|
||||
if (m.is_eq(e, e1, e2))
|
||||
(*uf)[turn].merge(mk_var(e1), mk_var(e2));
|
||||
else
|
||||
(*preds)[turn].insert(e);
|
||||
}
|
||||
unsigned round = 0;
|
||||
for (unsigned j = 1; j < num_args; ++j) {
|
||||
++round;
|
||||
m_es.reset();
|
||||
m_mark.reset();
|
||||
|
||||
bool last = turn;
|
||||
turn = !turn;
|
||||
(*preds)[turn].reset();
|
||||
reset(m_uf0);
|
||||
VERIFY(is_and(es[j], args[turn]));
|
||||
|
||||
for (expr* e : *args[turn]) {
|
||||
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))
|
||||
(*preds)[turn].insert(e);
|
||||
}
|
||||
|
||||
if ((*preds)[turn].empty() && m_es.empty())
|
||||
return BR_FAILED;
|
||||
|
||||
m_eqs.reset();
|
||||
for (expr* e : m_es) {
|
||||
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({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& [e1, e2] : m_eqs)
|
||||
(*uf)[turn].merge(mk_var(e1), mk_var(e2));
|
||||
if ((*preds)[turn].empty() && m_eqs.empty())
|
||||
return BR_FAILED;
|
||||
}
|
||||
if (m_eqs.empty()) {
|
||||
result = hoist_predicates((*preds)[turn], num_args, es);
|
||||
return BR_DONE;
|
||||
}
|
||||
// p & eqs & (or fmls)
|
||||
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());
|
||||
fmls.push_back(p);
|
||||
}
|
||||
bool new_eq = false;
|
||||
for (auto& [a, b] : m_eqs) {
|
||||
if (m.is_value(a))
|
||||
std::swap(a, b);
|
||||
if (m.are_equal(a, b))
|
||||
continue;
|
||||
if (m.are_distinct(a, b)) {
|
||||
result = m.mk_false();
|
||||
return BR_DONE;
|
||||
}
|
||||
new_eq = true;
|
||||
m_subst.insert(a, b);
|
||||
fmls.push_back(m.mk_eq(a, b));
|
||||
}
|
||||
expr_ref ors(::mk_or(m, num_args, es), m);
|
||||
m_subst(ors);
|
||||
fmls.push_back(ors);
|
||||
result = mk_and(fmls);
|
||||
TRACE("hoist", tout << ors << " => " << result << "\n";);
|
||||
return new_eq ? BR_REWRITE3 : BR_DONE;
|
||||
}
|
||||
|
||||
unsigned hoist_rewriter::mk_var(expr* e) {
|
||||
unsigned v = 0;
|
||||
if (m_expr2var.find(e, v))
|
||||
return v;
|
||||
m_uf1.mk_var();
|
||||
v = m_uf2.mk_var();
|
||||
SASSERT(v == m_var2expr.size());
|
||||
m_expr2var.insert(e, v);
|
||||
m_var2expr.push_back(e);
|
||||
return v;
|
||||
}
|
||||
|
||||
expr_ref hoist_rewriter::hoist_predicates(obj_hashtable<expr> const& preds, unsigned num_args, expr* const* es) {
|
||||
expr_ref_vector args(m), args1(m), fmls(m);
|
||||
for (unsigned i = 0; i < num_args; ++i) {
|
||||
VERIFY(is_and(es[i], &args1));
|
||||
fmls.reset();
|
||||
for (expr* e : args1)
|
||||
if (!preds.contains(e))
|
||||
fmls.push_back(e);
|
||||
args.push_back(mk_and(fmls));
|
||||
}
|
||||
fmls.reset();
|
||||
fmls.push_back(mk_or(args));
|
||||
for (auto* p : preds)
|
||||
fmls.push_back(p);
|
||||
return mk_and(fmls);
|
||||
}
|
||||
|
||||
|
||||
br_status hoist_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
|
||||
switch (f->get_decl_kind()) {
|
||||
case OP_OR:
|
||||
return mk_or(num_args, args, result);
|
||||
default:
|
||||
return BR_FAILED;
|
||||
}
|
||||
}
|
||||
|
||||
bool hoist_rewriter::is_and(expr * e, expr_ref_vector* args) {
|
||||
#if 0
|
||||
if (!args)
|
||||
return m.is_and(e) || (m.is_not(e, e) && m.is_or(e));
|
||||
expr_fast_mark1 visited;
|
||||
args->reset();
|
||||
args->push_back(e);
|
||||
m_refs.reset();
|
||||
for (unsigned i = 0; i < args->size(); ++i) {
|
||||
e = args->get(i);
|
||||
if (visited.is_marked(e))
|
||||
goto drop;
|
||||
m_refs.push_back(e);
|
||||
visited.mark(e, true);
|
||||
if (m.is_and(e))
|
||||
args->append(to_app(e)->get_num_args(), to_app(e)->get_args());
|
||||
else if (m.is_not(e, e) && m.is_or(e))
|
||||
for (expr* arg : *to_app(e))
|
||||
args->push_back(::mk_not(m, arg));
|
||||
else
|
||||
continue;
|
||||
drop:
|
||||
(*args)[i] = args->back();
|
||||
args->pop_back();
|
||||
--i;
|
||||
}
|
||||
return args->size() > 1;
|
||||
#else
|
||||
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 (args) {
|
||||
args->reset();
|
||||
for (expr* arg : *to_app(e))
|
||||
args->push_back(::mk_not(m, arg));
|
||||
TRACE("hoist", tout << args << " " << * args << "\n");
|
||||
}
|
||||
return true;
|
||||
}
|
||||
#endif
|
||||
return false;
|
||||
}
|
||||
|
||||
|
||||
void hoist_rewriter::reset(basic_union_find& uf) {
|
||||
uf.reset();
|
||||
for (expr* e : m_var2expr) {
|
||||
(void)e;
|
||||
uf.mk_var();
|
||||
}
|
||||
}
|
||||
|
|
@ -1,87 +0,0 @@
|
|||
/*++
|
||||
Copyright (c) 2019 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
hoist_rewriter.h
|
||||
|
||||
Abstract:
|
||||
|
||||
Hoist predicates over disjunctions
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2019-2-4
|
||||
|
||||
Notes:
|
||||
|
||||
--*/
|
||||
#pragma once
|
||||
|
||||
#include "ast/ast.h"
|
||||
#include "ast/rewriter/rewriter.h"
|
||||
#include "ast/rewriter/expr_safe_replace.h"
|
||||
#include "util/params.h"
|
||||
#include "util/union_find.h"
|
||||
#include "util/obj_hashtable.h"
|
||||
|
||||
class bool_rewriter;
|
||||
|
||||
class hoist_rewriter {
|
||||
ast_manager & m;
|
||||
expr_ref_vector m_args1, m_args2, m_refs;
|
||||
obj_hashtable<expr> m_preds1, m_preds2;
|
||||
basic_union_find m_uf1, m_uf2, m_uf0;
|
||||
ptr_vector<expr> m_es;
|
||||
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;
|
||||
bool m_elim_and = false;
|
||||
|
||||
bool is_and(expr* e, expr_ref_vector* args);
|
||||
expr_ref mk_and(expr_ref_vector const& args);
|
||||
expr_ref mk_or(expr_ref_vector const& args);
|
||||
|
||||
bool is_var(expr* e) { return m_expr2var.contains(e); }
|
||||
expr* mk_expr(unsigned v) { return m_var2expr[v]; }
|
||||
unsigned mk_var(expr* e);
|
||||
|
||||
void reset(basic_union_find& uf);
|
||||
|
||||
expr_ref hoist_predicates(obj_hashtable<expr> const& p, unsigned num_args, expr* const* args);
|
||||
|
||||
|
||||
public:
|
||||
hoist_rewriter(ast_manager & m, params_ref const & p = params_ref());
|
||||
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);
|
||||
void set_elim_and(bool b) { m_elim_and = b; }
|
||||
};
|
||||
|
||||
struct hoist_rewriter_cfg : public default_rewriter_cfg {
|
||||
hoist_rewriter m_r;
|
||||
bool rewrite_patterns() const { return false; }
|
||||
br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
|
||||
result_pr = nullptr;
|
||||
if (f->get_family_id() != m_r.get_fid())
|
||||
return BR_FAILED;
|
||||
return m_r.mk_app_core(f, num, args, result);
|
||||
}
|
||||
hoist_rewriter_cfg(ast_manager & m, params_ref const & p):m_r(m, p) {}
|
||||
};
|
||||
|
||||
class hoist_rewriter_star : public rewriter_tpl<hoist_rewriter_cfg> {
|
||||
hoist_rewriter_cfg m_cfg;
|
||||
public:
|
||||
hoist_rewriter_star(ast_manager & m, params_ref const & p = params_ref()):
|
||||
rewriter_tpl<hoist_rewriter_cfg>(m, false, m_cfg),
|
||||
m_cfg(m, p) {}
|
||||
};
|
||||
|
||||
Loading…
Reference in a new issue