1 /*++
2 Copyright (c) 2006 Microsoft Corporation
3
4 Module Name:
5
6 maximize_ac_sharing.cpp
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
20 #include "ast/rewriter/maximize_ac_sharing.h"
21 #include "ast/ast_pp.h"
22
23
register_kind(decl_kind k)24 void maximize_ac_sharing::register_kind(decl_kind k) {
25 m_kinds.push_back(k);
26 }
27
28
reduce_app(func_decl * f,unsigned num_args,expr * const * args,expr_ref & result,proof_ref & result_pr)29 br_status maximize_ac_sharing::reduce_app(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result, proof_ref& result_pr) {
30 decl_kind k = f->get_kind();
31 if (!f->is_associative())
32 return BR_FAILED;
33 if (num_args <= 2)
34 return BR_FAILED;
35 if (std::find(m_kinds.begin(), m_kinds.end(), k) == m_kinds.end())
36 return BR_FAILED;
37 ptr_buffer<expr, 128> _args;
38 expr * numeral = nullptr;
39 if (is_numeral(args[0])) {
40 numeral = args[0];
41 for (unsigned i = 1; i < num_args; i++)
42 _args.push_back(args[i]);
43 num_args--;
44 }
45 else {
46 _args.append(num_args, args);
47 }
48
49 TRACE("ac_sharing_detail", tout << "before-reuse: num_args: " << num_args << "\n";);
50
51 #define MAX_NUM_ARGS_FOR_OPT 128
52
53 // Try to reuse already created circuits.
54 TRACE("ac_sharing_detail", tout << "args: "; for (unsigned i = 0; i < num_args; i++) tout << mk_pp(_args[i], m) << "\n";);
55 try_to_reuse:
56 if (num_args > 1 && num_args < MAX_NUM_ARGS_FOR_OPT) {
57 for (unsigned i = 0; i + 1 < num_args; i++) {
58 for (unsigned j = i + 1; j < num_args; j++) {
59 if (contains(f, _args[i], _args[j])) {
60 TRACE("ac_sharing_detail", tout << "reusing args: " << i << " " << j << "\n";);
61 _args[i] = m.mk_app(f, _args[i], _args[j]);
62 SASSERT(num_args > 1);
63 for (unsigned w = j; w + 1 < num_args; w++) {
64 _args[w] = _args[w+1];
65 }
66 num_args--;
67 goto try_to_reuse;
68 }
69 }
70 }
71 }
72
73
74 // Create "tree-like circuit"
75 while (true) {
76 TRACE("ac_sharing_detail", tout << "tree-loop: num_args: " << num_args << "\n";);
77 unsigned j = 0;
78 for (unsigned i = 0; i < num_args; i += 2, j++) {
79 if (i == num_args - 1) {
80 _args[j] = _args[i];
81 }
82 else {
83 insert(f, _args[i], _args[i+1]);
84 _args[j] = m.mk_app(f, _args[i], _args[i+1]);
85 }
86 }
87 num_args = j;
88 if (num_args == 1) {
89 if (numeral == nullptr) {
90 result = _args[0];
91 }
92 else {
93 result = m.mk_app(f, numeral, _args[0]);
94 }
95 TRACE("ac_sharing_detail", tout << "result: " << mk_pp(result, m) << "\n";);
96 return BR_DONE;
97 }
98 }
99
100 UNREACHABLE();
101 return BR_FAILED;
102 }
103
contains(func_decl * f,expr * arg1,expr * arg2)104 bool maximize_ac_sharing::contains(func_decl * f, expr * arg1, expr * arg2) {
105 entry e(f, arg1, arg2);
106 return m_cache.contains(&e);
107 }
108
insert(func_decl * f,expr * arg1,expr * arg2)109 void maximize_ac_sharing::insert(func_decl * f, expr * arg1, expr * arg2) {
110 entry * e = new (m_region) entry(f, arg1, arg2);
111 m_entries.push_back(e);
112 m_cache.insert(e);
113 m.inc_ref(arg1);
114 m.inc_ref(arg2);
115 }
116
maximize_ac_sharing(ast_manager & m)117 maximize_ac_sharing::maximize_ac_sharing(ast_manager & m):
118 m(m),
119 m_init(false) {
120 }
121
~maximize_ac_sharing()122 maximize_ac_sharing::~maximize_ac_sharing() {
123 restore_entries(0);
124 }
125
126
push_scope()127 void maximize_ac_sharing::push_scope() {
128 init();
129 m_scopes.push_back(m_entries.size());
130 m_region.push_scope();
131 }
132
pop_scope(unsigned num_scopes)133 void maximize_ac_sharing::pop_scope(unsigned num_scopes) {
134 SASSERT(num_scopes <= m_scopes.size());
135 unsigned new_lvl = m_scopes.size() - num_scopes;
136 unsigned old_lim = m_scopes[new_lvl];
137 restore_entries(old_lim);
138 m_region.pop_scope(num_scopes);
139 m_scopes.shrink(new_lvl);
140 }
141
restore_entries(unsigned old_lim)142 void maximize_ac_sharing::restore_entries(unsigned old_lim) {
143 unsigned i = m_entries.size();
144 while (i != old_lim) {
145 --i;
146 entry * e = m_entries[i];
147 m_cache.remove(e);
148 m.dec_ref(e->m_arg1);
149 m.dec_ref(e->m_arg2);
150 }
151 m_entries.shrink(old_lim);
152 }
153
reset()154 void maximize_ac_sharing::reset() {
155 m_cache.reset();
156 }
157
init_core()158 void maximize_bv_sharing::init_core() {
159 register_kind(OP_BADD);
160 register_kind(OP_BMUL);
161 register_kind(OP_BOR);
162 register_kind(OP_BAND);
163 }
164
is_numeral(expr * n) const165 bool maximize_bv_sharing::is_numeral(expr * n) const {
166 return m_util.is_numeral(n);
167 }
168
maximize_bv_sharing(ast_manager & m)169 maximize_bv_sharing::maximize_bv_sharing(ast_manager & m):
170 maximize_ac_sharing(m),
171 m_util(m) {
172 }
173