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