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