1 /*++ 2 Copyright (c) 2006 Microsoft Corporation 3 4 Module Name: 5 6 maximize_ac_sharing.h 7 8 Abstract: 9 10 <abstract> 11 12 Author: 13 14 Leonardo de Moura (leonardo) 2008-10-22. 15 16 Revision History: 17 18 --*/ 19 #pragma once 20 21 #include "util/hashtable.h" 22 #include "util/region.h" 23 #include "ast/bv_decl_plugin.h" 24 #include "ast/rewriter/rewriter.h" 25 26 /** 27 \brief Functor used to maximize the amount of shared terms in an expression. 28 The idea is to rewrite AC terms to maximize sharing. 29 Example: 30 31 (f (bvadd a (bvadd b c)) (bvadd a (bvadd b d))) 32 33 is rewritten to: 34 35 (f (bvadd (bvadd a b) c) (bvadd (bvadd a b) d)) 36 37 \warning This class uses an opportunistic heuristic to maximize sharing. 38 There is no guarantee that the optimal expression will be produced. 39 */ 40 class maximize_ac_sharing : public default_rewriter_cfg { 41 42 struct entry { 43 func_decl * m_decl; 44 expr * m_arg1; 45 expr * m_arg2; 46 m_declentry47 entry(func_decl * d = nullptr, expr * arg1 = nullptr, expr * arg2 = nullptr):m_decl(d), m_arg1(arg1), m_arg2(arg2) { 48 SASSERT((d == 0 && arg1 == 0 && arg2 == 0) || (d != 0 && arg1 != 0 && arg2 != 0)); 49 if (arg1->get_id() > arg2->get_id()) 50 std::swap(m_arg1, m_arg2); 51 } 52 hashentry53 unsigned hash() const { 54 unsigned a = m_decl->get_id(); 55 unsigned b = m_arg1->get_id(); 56 unsigned c = m_arg2->get_id(); 57 mix(a,b,c); 58 return c; 59 } 60 61 bool operator==(entry const & e) const { 62 return m_decl == e.m_decl && m_arg1 == e.m_arg1 && m_arg2 == e.m_arg2; 63 } 64 }; 65 66 typedef ptr_hashtable<entry, obj_ptr_hash<entry>, deref_eq<entry> > cache; 67 68 protected: 69 void register_kind(decl_kind k); 70 71 private: 72 ast_manager & m; 73 bool m_init; 74 region m_region; 75 cache m_cache; 76 ptr_vector<entry> m_entries; 77 unsigned_vector m_scopes; 78 svector<decl_kind> m_kinds; //!< kinds to be processed 79 80 bool contains(func_decl * f, expr * arg1, expr * arg2); 81 void insert(func_decl * f, expr * arg1, expr * arg2); 82 void restore_entries(unsigned old_lim); init()83 void init() { 84 if (!m_init) { 85 init_core(); 86 m_init = true; 87 } 88 } 89 protected: 90 virtual void init_core() = 0; 91 virtual bool is_numeral(expr * n) const = 0; 92 public: 93 maximize_ac_sharing(ast_manager & m); 94 virtual ~maximize_ac_sharing(); 95 void push_scope(); 96 void pop_scope(unsigned num_scopes); 97 void reset(); 98 br_status reduce_app(func_decl* f, unsigned n, expr * const* args, expr_ref& result, proof_ref& result_pr); 99 100 }; 101 102 class maximize_bv_sharing : public maximize_ac_sharing { 103 bv_util m_util; 104 protected: 105 void init_core() override; 106 bool is_numeral(expr * n) const override; 107 public: 108 maximize_bv_sharing(ast_manager & m); 109 }; 110 111 class maximize_bv_sharing_rw : public rewriter_tpl<maximize_bv_sharing> { 112 maximize_bv_sharing m_cfg; 113 public: maximize_bv_sharing_rw(ast_manager & m)114 maximize_bv_sharing_rw(ast_manager& m): 115 rewriter_tpl<maximize_bv_sharing>(m, m.proofs_enabled(), m_cfg), 116 m_cfg(m) 117 {} push_scope()118 void push_scope() { m_cfg.push_scope(); } pop_scope(unsigned n)119 void pop_scope(unsigned n) { m_cfg.pop_scope(n); } reset()120 void reset() { m_cfg.reset(); } 121 }; 122 123 124