From 56598037b67f03c59f09a45573432f50389b2001 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 6 Feb 2019 19:42:40 +0100 Subject: [PATCH] new rewriter Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/hoist_rewriter.cpp | 178 ++++++++++++++++++++++++++++ src/ast/rewriter/hoist_rewriter.h | 80 +++++++++++++ 2 files changed, 258 insertions(+) create mode 100644 src/ast/rewriter/hoist_rewriter.cpp create mode 100644 src/ast/rewriter/hoist_rewriter.h diff --git a/src/ast/rewriter/hoist_rewriter.cpp b/src/ast/rewriter/hoist_rewriter.cpp new file mode 100644 index 000000000..ad7dffbdb --- /dev/null +++ b/src/ast/rewriter/hoist_rewriter.cpp @@ -0,0 +1,178 @@ +/*++ +Copyright (c) 2019 Microsoft Corporation + +Module Name: + + hoist_rewriter.cpp + +Abstract: + + Hoist predicates over disjunctions + +Author: + + Nikolaj Bjorner (nbjorner) 2019-2-4 + +Notes: + +--*/ + + +#include "ast/rewriter/hoist_rewriter.h" +#include "ast/ast_util.h" +#include "ast/rewriter/expr_safe_replace.h" +#include "ast/ast_pp.h" + + +hoist_rewriter::hoist_rewriter(ast_manager & m, params_ref const & p): + m_manager(m), m_args(m) { + updt_params(p); +} + +br_status hoist_rewriter::mk_or(unsigned num_args, expr * const * args, expr_ref & result) { + if (num_args < 2) { + return BR_FAILED; + } + for (unsigned i = 0; i < num_args; ++i) { + if (!is_and(args[i])) { + 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* preds[2] = { &m_preds1, &m_preds2 }; + VERIFY(is_and(args[0])); + expr* e1, *e2; + for (expr* e : m_args) { + 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); + unsigned v1 = 0, v2 = 0; + VERIFY(is_and(args[j])); + for (expr* e : m_args) { + 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(std::make_pair(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)); + } + } + // p & eqs & (or fmls) + expr_ref_vector fmls(m()), ors(m()); + expr_safe_replace subst(m()); + for (expr * p : (*preds)[turn]) { + subst.insert(p, m().mk_true()); + fmls.push_back(p); + } + for (auto const& p : m_eqs) { + subst.insert(p.first, p.second); + fmls.push_back(m().mk_eq(p.first, p.second)); + } + + for (unsigned i = 0; i < num_args; ++i) { + expr_ref tmp(m()); + subst(args[i], tmp); + ors.push_back(tmp); + } + fmls.push_back(m().mk_or(ors.size(), ors.c_ptr())); + result = m().mk_and(fmls.size(), fmls.c_ptr()); + return BR_DONE; +} + +unsigned hoist_rewriter::mk_var(expr* e) { + unsigned v = 0; + if (m_expr2var.find(e, v)) { + return v; + } + 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; +} + +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) { + m_args.reset(); + if (m().is_and(e)) { + m_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)) { + for (expr* arg : *to_app(e)) { + m_args.push_back(::mk_not(m(), arg)); + } + return true; + } + return false; +} + + +void hoist_rewriter::reset(basic_union_find& uf) { + uf.reset(); + for (expr* e : m_var2expr) { + uf.mk_var(); + } +} diff --git a/src/ast/rewriter/hoist_rewriter.h b/src/ast/rewriter/hoist_rewriter.h new file mode 100644 index 000000000..dbaeebd4d --- /dev/null +++ b/src/ast/rewriter/hoist_rewriter.h @@ -0,0 +1,80 @@ +/*++ +Copyright (c) 2019 Microsoft Corporation + +Module Name: + + hoist_rewriter.h + +Abstract: + + Hoist predicates over disjunctions + +Author: + + Nikolaj Bjorner (nbjorner) 2019-2-4 + +Notes: + +--*/ +#ifndef HOIST_REWRITER_H_ +#define HOIST_REWRITER_H_ + +#include "ast/ast.h" +#include "ast/rewriter/rewriter.h" +#include "util/params.h" +#include "util/union_find.h" +#include "util/obj_hashtable.h" + +class hoist_rewriter { + ast_manager & m_manager; + expr_ref_vector m_args; + obj_hashtable m_preds1, m_preds2; + basic_union_find m_uf1, m_uf2, m_uf0; + ptr_vector m_es; + svector> m_eqs; + u_map m_roots; + obj_map m_expr2var; + ptr_vector m_var2expr; + expr_mark m_mark; + + br_status mk_or(unsigned num_args, expr * const * args, expr_ref & result); + + bool is_and(expr* e); + + 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); + +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); } + 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); +}; + +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 m_cfg; +public: + hoist_rewriter_star(ast_manager & m, params_ref const & p = params_ref()): + rewriter_tpl(m, false, m_cfg), + m_cfg(m, p) {} +}; + +#endif