1 /*++
2 Copyright (c) 2012 Microsoft Corporation
3 
4 Module Name:
5 
6     polynomial_cache.cpp
7 
8 Abstract:
9 
10     "Hash-consing" for polynomials
11 
12 Author:
13 
14     Leonardo (leonardo) 2012-01-07
15 
16 Notes:
17 
18 --*/
19 #include "math/polynomial/polynomial_cache.h"
20 #include "util/chashtable.h"
21 
22 namespace polynomial {
23 
24     struct poly_hash_proc {
25         manager & m;
poly_hash_procpolynomial::poly_hash_proc26         poly_hash_proc(manager & _m):m(_m) {}
operator ()polynomial::poly_hash_proc27         unsigned operator()(polynomial const * p) const { return m.hash(p); }
28     };
29 
30     struct poly_eq_proc {
31         manager & m;
poly_eq_procpolynomial::poly_eq_proc32         poly_eq_proc(manager & _m):m(_m) {}
operator ()polynomial::poly_eq_proc33         bool operator()(polynomial const * p1, polynomial const * p2) const { return m.eq(p1, p2); }
34     };
35 
36     struct psc_chain_entry {
37         polynomial const * m_p;
38         polynomial const * m_q;
39         var                m_x;
40         unsigned           m_hash;
41         unsigned           m_result_sz;
42         polynomial **      m_result;
43 
psc_chain_entrypolynomial::psc_chain_entry44         psc_chain_entry(polynomial const * p, polynomial const * q, var x, unsigned h):
45             m_p(p),
46             m_q(q),
47             m_x(x),
48             m_hash(h),
49             m_result_sz(0),
50             m_result(nullptr) {
51         }
52 
operator ()polynomial::psc_chain_entry::hash_proc53         struct hash_proc { unsigned operator()(psc_chain_entry const * entry) const { return entry->m_hash; } };
54 
55         struct eq_proc {
operator ()polynomial::psc_chain_entry::eq_proc56             bool operator()(psc_chain_entry const * e1, psc_chain_entry const * e2) const {
57                 return e1->m_p == e2->m_p && e1->m_q == e2->m_q && e1->m_x == e2->m_x;
58             }
59         };
60     };
61 
62     struct factor_entry {
63         polynomial const * m_p;
64         unsigned           m_hash;
65         unsigned           m_result_sz;
66         polynomial **      m_result;
67 
factor_entrypolynomial::factor_entry68         factor_entry(polynomial const * p, unsigned h):
69             m_p(p),
70             m_hash(h),
71             m_result_sz(0),
72             m_result(nullptr) {
73         }
74 
operator ()polynomial::factor_entry::hash_proc75         struct hash_proc { unsigned operator()(factor_entry const * entry) const { return entry->m_hash; } };
76 
77         struct eq_proc {
operator ()polynomial::factor_entry::eq_proc78             bool operator()(factor_entry const * e1, factor_entry const * e2) const {
79                 return e1->m_p == e2->m_p;
80             }
81         };
82     };
83 
84     typedef chashtable<polynomial*, poly_hash_proc, poly_eq_proc> polynomial_table;
85     typedef chashtable<psc_chain_entry*, psc_chain_entry::hash_proc, psc_chain_entry::eq_proc> psc_chain_cache;
86     typedef chashtable<factor_entry*, factor_entry::hash_proc, factor_entry::eq_proc> factor_cache;
87 
88     struct cache::imp {
89         manager &                m;
90         polynomial_table         m_poly_table;
91         psc_chain_cache          m_psc_chain_cache;
92         factor_cache             m_factor_cache;
93         polynomial_ref_vector    m_cached_polys;
94         svector<char>            m_in_cache;
95         small_object_allocator & m_allocator;
96 
imppolynomial::cache::imp97         imp(manager & _m):m(_m), m_poly_table(poly_hash_proc(m), poly_eq_proc(m)), m_cached_polys(m), m_allocator(m.allocator()) {
98         }
99 
~imppolynomial::cache::imp100         ~imp() {
101             reset_psc_chain_cache();
102             reset_factor_cache();
103         }
104 
del_psc_chain_entrypolynomial::cache::imp105         void del_psc_chain_entry(psc_chain_entry * entry) {
106             if (entry->m_result_sz != 0)
107                 m_allocator.deallocate(sizeof(polynomial*)*entry->m_result_sz, entry->m_result);
108             entry->~psc_chain_entry();
109             m_allocator.deallocate(sizeof(psc_chain_entry), entry);
110         }
111 
del_factor_entrypolynomial::cache::imp112         void del_factor_entry(factor_entry * entry) {
113             if (entry->m_result_sz != 0)
114                 m_allocator.deallocate(sizeof(polynomial*)*entry->m_result_sz, entry->m_result);
115             entry->~factor_entry();
116             m_allocator.deallocate(sizeof(factor_entry), entry);
117         }
118 
reset_psc_chain_cachepolynomial::cache::imp119         void reset_psc_chain_cache() {
120             psc_chain_cache::iterator it  = m_psc_chain_cache.begin();
121             psc_chain_cache::iterator end = m_psc_chain_cache.end();
122             for (; it != end; ++it) {
123                 del_psc_chain_entry(*it);
124             }
125             m_psc_chain_cache.reset();
126         }
127 
reset_factor_cachepolynomial::cache::imp128         void reset_factor_cache() {
129             factor_cache::iterator it  = m_factor_cache.begin();
130             factor_cache::iterator end = m_factor_cache.end();
131             for (; it != end; ++it) {
132                 del_factor_entry(*it);
133             }
134             m_factor_cache.reset();
135         }
136 
pidpolynomial::cache::imp137         unsigned pid(polynomial * p) const { return m.id(p); }
138 
mk_uniquepolynomial::cache::imp139         polynomial * mk_unique(polynomial * p) {
140             if (m_in_cache.get(pid(p), false))
141                 return p;
142             // m.gcd_simplify(p);
143             polynomial * p_prime = m_poly_table.insert_if_not_there(p);
144             if (p == p_prime) {
145                 m_cached_polys.push_back(p_prime);
146                 m_in_cache.setx(pid(p_prime), true, false);
147             }
148             return p_prime;
149         }
150 
psc_chainpolynomial::cache::imp151         void psc_chain(polynomial * p, polynomial * q, var x, polynomial_ref_vector & S) {
152             p = mk_unique(p);
153             q = mk_unique(q);
154             unsigned h = hash_u_u(pid(p), pid(q));
155             psc_chain_entry * entry = new (m_allocator.allocate(sizeof(psc_chain_entry))) psc_chain_entry(p, q, x, h);
156             psc_chain_entry * old_entry = m_psc_chain_cache.insert_if_not_there(entry);
157             if (entry != old_entry) {
158                 entry->~psc_chain_entry();
159                 m_allocator.deallocate(sizeof(psc_chain_entry), entry);
160                 S.reset();
161                 for (unsigned i = 0; i < old_entry->m_result_sz; i++) {
162                     S.push_back(old_entry->m_result[i]);
163                 }
164             }
165             else {
166                 m.psc_chain(p, q, x, S);
167                 unsigned sz = S.size();
168                 entry->m_result_sz = sz;
169                 entry->m_result    = static_cast<polynomial**>(m_allocator.allocate(sizeof(polynomial*)*sz));
170                 for (unsigned i = 0; i < sz; i++) {
171                     polynomial * h = mk_unique(S.get(i));
172                     S.set(i, h);
173                     entry->m_result[i] = h;
174                 }
175             }
176         }
177 
factorpolynomial::cache::imp178         void factor(polynomial * p, polynomial_ref_vector & distinct_factors) {
179             distinct_factors.reset();
180             p = mk_unique(p);
181             unsigned h = hash_u(pid(p));
182             factor_entry * entry = new (m_allocator.allocate(sizeof(factor_entry))) factor_entry(p, h);
183             factor_entry * old_entry = m_factor_cache.insert_if_not_there(entry);
184             if (entry != old_entry) {
185                 entry->~factor_entry();
186                 m_allocator.deallocate(sizeof(factor_entry), entry);
187                 distinct_factors.reset();
188                 for (unsigned i = 0; i < old_entry->m_result_sz; i++) {
189                     distinct_factors.push_back(old_entry->m_result[i]);
190                 }
191             }
192             else {
193                 factors fs(m);
194                 m.factor(p, fs);
195                 unsigned sz = fs.distinct_factors();
196                 entry->m_result_sz = sz;
197                 entry->m_result    = static_cast<polynomial**>(m_allocator.allocate(sizeof(polynomial*)*sz));
198                 for (unsigned i = 0; i < sz; i++) {
199                     polynomial * h = mk_unique(fs[i]);
200                     distinct_factors.push_back(h);
201                     entry->m_result[i] = h;
202                 }
203             }
204         }
205     };
206 
cache(manager & m)207     cache::cache(manager & m) {
208         m_imp = alloc(imp, m);
209     }
210 
~cache()211     cache::~cache() {
212         dealloc(m_imp);
213     }
214 
m() const215     manager & cache::m() const {
216         return m_imp->m;
217     }
218 
mk_unique(polynomial * p)219     polynomial * cache::mk_unique(polynomial * p) {
220         return m_imp->mk_unique(p);
221     }
222 
psc_chain(polynomial const * p,polynomial const * q,var x,polynomial_ref_vector & S)223     void cache::psc_chain(polynomial const * p, polynomial const * q, var x, polynomial_ref_vector & S) {
224         m_imp->psc_chain(const_cast<polynomial*>(p), const_cast<polynomial*>(q), x, S);
225     }
226 
factor(polynomial const * p,polynomial_ref_vector & distinct_factors)227     void cache::factor(polynomial const * p, polynomial_ref_vector & distinct_factors) {
228         m_imp->factor(const_cast<polynomial*>(p), distinct_factors);
229     }
230 
reset()231     void cache::reset() {
232         manager & _m = m();
233         dealloc(m_imp);
234         m_imp = alloc(imp, _m);
235     }
236 };
237