1 /*++ 2 Copyright (c) 2017 Microsoft Corporation 3 4 Module Name: 5 6 dom_simplify_tactic.cpp 7 8 9 Abstract: 10 11 Dominator-based context simplifer. 12 13 Author: 14 15 Nikolaj and Nuno 16 17 Notes: 18 19 --*/ 20 21 #pragma once 22 23 #include "ast/ast.h" 24 #include "ast/expr_substitution.h" 25 #include "tactic/tactic.h" 26 #include "tactic/tactical.h" 27 #include "util/obj_pair_hashtable.h" 28 29 30 class expr_dominators { 31 public: 32 typedef obj_map<expr, ptr_vector<expr>> tree_t; 33 private: 34 ast_manager& m; 35 expr_ref m_root; 36 obj_map<expr, unsigned> m_expr2post; // reverse post-order number 37 ptr_vector<expr> m_post2expr; 38 tree_t m_parents; 39 obj_map<expr, expr*> m_doms; 40 tree_t m_tree; 41 add_edge(tree_t & tree,expr * src,expr * dst)42 void add_edge(tree_t& tree, expr * src, expr* dst) { 43 tree.insert_if_not_there(src, ptr_vector<expr>()).push_back(dst); 44 } 45 46 void compute_post_order(); 47 expr* intersect(expr* x, expr * y); 48 bool compute_dominators(); 49 void extract_tree(); 50 51 std::ostream& display(std::ostream& out, unsigned indent, expr* r); 52 53 public: expr_dominators(ast_manager & m)54 expr_dominators(ast_manager& m): m(m), m_root(m) {} 55 56 bool compile(expr * e); 57 bool compile(unsigned sz, expr * const* es); get_tree()58 tree_t const& get_tree() { return m_tree; } 59 void reset(); idom(expr * e)60 expr* idom(expr *e) const { return m_doms[e]; } 61 62 std::ostream& display(std::ostream& out); 63 }; 64 65 class dom_simplifier { 66 public: dom_simplifier()67 dom_simplifier() {} 68 ~dom_simplifier()69 virtual ~dom_simplifier() {} 70 /** 71 \brief assert_expr performs an implicit push 72 */ 73 virtual bool assert_expr(expr * t, bool sign) = 0; 74 75 /** 76 \brief apply simplification. 77 */ 78 virtual void operator()(expr_ref& r) = 0; 79 80 /** 81 \brief pop scopes accumulated from assertions. 82 */ 83 virtual void pop(unsigned num_scopes) = 0; 84 85 virtual dom_simplifier * translate(ast_manager & m) = 0; 86 87 virtual unsigned scope_level() const = 0; 88 89 }; 90 91 class dom_simplify_tactic : public tactic { 92 ast_manager& m; 93 dom_simplifier* m_simplifier; 94 params_ref m_params; 95 expr_ref_vector m_trail, m_args; 96 obj_map<expr, expr*> m_result; 97 expr_dominators m_dominators; 98 unsigned m_depth; 99 unsigned m_max_depth; 100 ptr_vector<expr> m_empty; 101 obj_pair_map<expr, expr, bool> m_subexpr_cache; 102 bool m_forward; 103 104 expr_ref simplify_rec(expr* t); 105 expr_ref simplify_arg(expr* t); 106 expr_ref simplify_ite(app * ite); simplify_and(app * e)107 expr_ref simplify_and(app * e) { return simplify_and_or(true, e); } simplify_or(app * e)108 expr_ref simplify_or(app * e) { return simplify_and_or(false, e); } 109 expr_ref simplify_and_or(bool is_and, app * e); 110 expr_ref simplify_not(app * e); 111 void simplify_goal(goal& g); 112 113 bool is_subexpr(expr * a, expr * b); 114 get_cached(expr * t)115 expr_ref get_cached(expr* t) { expr* r = nullptr; if (!m_result.find(t, r)) r = t; return expr_ref(r, m); } cache(expr * t,expr * r)116 void cache(expr *t, expr* r) { m_result.insert(t, r); m_trail.push_back(r); } reset_cache()117 void reset_cache() { m_result.reset(); } 118 119 ptr_vector<expr> const & tree(expr * e); idom(expr * e)120 expr* idom(expr *e) const { return m_dominators.idom(e); } 121 scope_level()122 unsigned scope_level() { return m_simplifier->scope_level(); } pop(unsigned n)123 void pop(unsigned n) { SASSERT(n <= m_simplifier->scope_level()); m_simplifier->pop(n); } assert_expr(expr * f,bool sign)124 bool assert_expr(expr* f, bool sign) { return m_simplifier->assert_expr(f, sign); } 125 126 bool init(goal& g); 127 128 public: 129 dom_simplify_tactic(ast_manager & m, dom_simplifier* s, params_ref const & p = params_ref()): m(m)130 m(m), m_simplifier(s), m_params(p), 131 m_trail(m), m_args(m), 132 m_dominators(m), m_depth(0), m_max_depth(1024), m_forward(true) {} 133 134 ~dom_simplify_tactic() override; 135 136 tactic * translate(ast_manager & m) override; updt_params(params_ref const & p)137 void updt_params(params_ref const & p) override {} get_param_descrs(param_descrs & r)138 static void get_param_descrs(param_descrs & r) {} collect_param_descrs(param_descrs & r)139 void collect_param_descrs(param_descrs & r) override { get_param_descrs(r); } 140 void operator()(goal_ref const & in, goal_ref_buffer & result) override; 141 void cleanup() override; 142 }; 143 144 tactic * mk_dom_simplify_tactic(ast_manager & m, params_ref const & p = params_ref()); 145 146 /* 147 ADD_TACTIC("dom-simplify", "apply dominator simplification rules.", "mk_dom_simplify_tactic(m, p)") 148 */ 149 150