1 /*++ 2 Copyright (c) 2019 Microsoft Corporation 3 4 Module Name: 5 6 hoist_rewriter.h 7 8 Abstract: 9 10 Hoist predicates over disjunctions 11 12 Author: 13 14 Nikolaj Bjorner (nbjorner) 2019-2-4 15 16 Notes: 17 18 --*/ 19 #pragma once 20 21 #include "ast/ast.h" 22 #include "ast/rewriter/rewriter.h" 23 #include "ast/rewriter/expr_safe_replace.h" 24 #include "util/params.h" 25 #include "util/union_find.h" 26 #include "util/obj_hashtable.h" 27 28 class hoist_rewriter { 29 ast_manager & m_manager; 30 expr_ref_vector m_args1, m_args2; 31 obj_hashtable<expr> m_preds1, m_preds2; 32 basic_union_find m_uf1, m_uf2, m_uf0; 33 ptr_vector<expr> m_es; 34 svector<std::pair<expr*,expr*>> m_eqs; 35 u_map<expr*> m_roots; 36 expr_safe_replace m_subst; 37 obj_map<expr, unsigned> m_expr2var; 38 ptr_vector<expr> m_var2expr; 39 expr_mark m_mark; 40 41 br_status mk_or(unsigned num_args, expr * const * args, expr_ref & result); 42 43 bool is_and(expr* e, expr_ref_vector* args); 44 is_var(expr * e)45 bool is_var(expr* e) { return m_expr2var.contains(e); } mk_expr(unsigned v)46 expr* mk_expr(unsigned v) { return m_var2expr[v]; } 47 unsigned mk_var(expr* e); 48 49 void reset(basic_union_find& uf); 50 51 expr_ref hoist_predicates(obj_hashtable<expr> const& p, unsigned num_args, expr* const* args); 52 53 public: 54 hoist_rewriter(ast_manager & m, params_ref const & p = params_ref()); m()55 ast_manager& m() const { return m_manager; } get_fid()56 family_id get_fid() const { return m().get_basic_family_id(); } is_eq(expr * t)57 bool is_eq(expr * t) const { return m().is_eq(t); } updt_params(params_ref const & p)58 void updt_params(params_ref const & p) {} get_param_descrs(param_descrs & r)59 static void get_param_descrs(param_descrs & r) {} 60 br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result); 61 }; 62 63 struct hoist_rewriter_cfg : public default_rewriter_cfg { 64 hoist_rewriter m_r; rewrite_patternshoist_rewriter_cfg65 bool rewrite_patterns() const { return false; } reduce_apphoist_rewriter_cfg66 br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { 67 result_pr = nullptr; 68 if (f->get_family_id() != m_r.get_fid()) 69 return BR_FAILED; 70 return m_r.mk_app_core(f, num, args, result); 71 } hoist_rewriter_cfghoist_rewriter_cfg72 hoist_rewriter_cfg(ast_manager & m, params_ref const & p):m_r(m, p) {} 73 }; 74 75 class hoist_rewriter_star : public rewriter_tpl<hoist_rewriter_cfg> { 76 hoist_rewriter_cfg m_cfg; 77 public: 78 hoist_rewriter_star(ast_manager & m, params_ref const & p = params_ref()): 79 rewriter_tpl<hoist_rewriter_cfg>(m, false, m_cfg), 80 m_cfg(m, p) {} 81 }; 82 83