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

remove dependency on bool-rewriter in hoist rewriter

Browse source 
deal with regression reported in
cac5052685 (commitcomment-100606067)
and unit tests doc.cpp
This commit is contained in:
Nikolaj Bjorner 2023-02-14 17:48:02 -08:00
parent a976b781a0
commit c2fe76569f
4 changed files with 19 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/ast/rewriter/bool_rewriter.cpp
View file

@ -32,6 +32,7 @@ void bool_rewriter::updt_params(params_ref const & _p) {
m_blast_distinct = p.blast_distinct(); m_blast_distinct = p.blast_distinct();
m_blast_distinct_threshold = p.blast_distinct_threshold(); m_blast_distinct_threshold = p.blast_distinct_threshold();
m_ite_extra_rules = p.ite_extra_rules(); 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) { void bool_rewriter::get_param_descrs(param_descrs & r) {

1
src/ast/rewriter/bool_rewriter.h
View file

@ -83,7 +83,6 @@ class bool_rewriter {
public: 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_hoist(m), m_local_ctx_cost(0) {
updt_params(p); updt_params(p);
m_hoist.set(*this);
} }
ast_manager & m() const { return m_manager; } ast_manager & m() const { return m_manager; }
family_id get_fid() const { return m().get_basic_family_id(); } family_id get_fid() const { return m().get_basic_family_id(); }

25
src/ast/rewriter/hoist_rewriter.cpp
View file

@ -28,17 +28,23 @@ hoist_rewriter::hoist_rewriter(ast_manager & m, params_ref const & p):
} }
expr_ref hoist_rewriter::mk_and(expr_ref_vector const& args) { expr_ref hoist_rewriter::mk_and(expr_ref_vector const& args) {
if (m_rewriter) if (m_elim_and) {
return m_rewriter->mk_and(args); 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 expr_ref(::mk_not(m, mk_or(negs)), m);
}
else else
return ::mk_and(args); return ::mk_and(args);
} }
expr_ref hoist_rewriter::mk_or(expr_ref_vector const& args) { expr_ref hoist_rewriter::mk_or(expr_ref_vector const& args) {
if (false && m_rewriter) return ::mk_or(args);
return m_rewriter->mk_or(args);
else
return ::mk_or(args);
} }
br_status hoist_rewriter::mk_or(unsigned num_args, expr * const * es, expr_ref & result) { br_status hoist_rewriter::mk_or(unsigned num_args, expr * const * es, expr_ref & result) {
@ -159,11 +165,11 @@ 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 hoist_rewriter::hoist_predicates(obj_hashtable<expr> const& preds, unsigned num_args, expr* const* es) {
expr_ref result(m); expr_ref result(m);
expr_ref_vector args(m), fmls(m); expr_ref_vector args(m), args1(m), fmls(m);
for (unsigned i = 0; i < num_args; ++i) { for (unsigned i = 0; i < num_args; ++i) {
VERIFY(is_and(es[i], &m_args1)); VERIFY(is_and(es[i], &args1));
fmls.reset(); fmls.reset();
for (expr* e : m_args1) for (expr* e : args1)
if (!preds.contains(e)) if (!preds.contains(e))
fmls.push_back(e); fmls.push_back(e);
args.push_back(mk_and(fmls)); args.push_back(mk_and(fmls));
@ -199,6 +205,7 @@ bool hoist_rewriter::is_and(expr * e, expr_ref_vector* args) {
args->reset(); args->reset();
for (expr* arg : *to_app(e)) for (expr* arg : *to_app(e))
args->push_back(::mk_not(m, arg)); args->push_back(::mk_not(m, arg));
TRACE("hoist", tout << args << " " << * args << "\n");
} }
return true; return true;
} }

4
src/ast/rewriter/hoist_rewriter.h
View file

@ -29,7 +29,6 @@ class bool_rewriter;
class hoist_rewriter { class hoist_rewriter {
ast_manager & m; ast_manager & m;
bool_rewriter* m_rewriter = nullptr;
expr_ref_vector m_args1, m_args2; expr_ref_vector m_args1, m_args2;
obj_hashtable<expr> m_preds1, m_preds2; obj_hashtable<expr> m_preds1, m_preds2;
basic_union_find m_uf1, m_uf2, m_uf0; basic_union_find m_uf1, m_uf2, m_uf0;
@ -40,6 +39,7 @@ class hoist_rewriter {
obj_map<expr, unsigned> m_expr2var; obj_map<expr, unsigned> m_expr2var;
ptr_vector<expr> m_var2expr; ptr_vector<expr> m_var2expr;
expr_mark m_mark; expr_mark m_mark;
bool m_elim_and = false;
bool is_and(expr* e, expr_ref_vector* args); bool is_and(expr* e, expr_ref_vector* args);
expr_ref mk_and(expr_ref_vector const& args); expr_ref mk_and(expr_ref_vector const& args);
@ -62,7 +62,7 @@ public:
static void get_param_descrs(param_descrs & r) {} 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_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); br_status mk_or(unsigned num_args, expr * const * args, expr_ref & result);
void set(bool_rewriter& r) { m_rewriter = &r; } void set_elim_and(bool b) { m_elim_and = b; }
}; };
struct hoist_rewriter_cfg : public default_rewriter_cfg { struct hoist_rewriter_cfg : public default_rewriter_cfg {