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