1 /*++ 2 Copyright (c) 2006 Microsoft Corporation 3 4 Module Name: 5 6 dl_table.cpp 7 8 Abstract: 9 10 <abstract> 11 12 Author: 13 14 Krystof Hoder (t-khoder) 2010-09-01. 15 16 Revision History: 17 18 --*/ 19 20 #include "muz/base/dl_context.h" 21 #include "muz/base/dl_util.h" 22 #include "muz/rel/dl_table.h" 23 #include "muz/rel/dl_relation_manager.h" 24 25 namespace datalog { 26 27 // ----------------------------------- 28 // 29 // hashtable_table 30 // 31 // ----------------------------------- 32 mk_empty(const table_signature & s)33 table_base * hashtable_table_plugin::mk_empty(const table_signature & s) { 34 SASSERT(can_handle_signature(s)); 35 return alloc(hashtable_table, *this, s); 36 } 37 38 39 class hashtable_table_plugin::join_fn : public convenient_table_join_fn { 40 unsigned m_joined_col_cnt; 41 public: join_fn(const table_signature & t1_sig,const table_signature & t2_sig,unsigned col_cnt,const unsigned * cols1,const unsigned * cols2)42 join_fn(const table_signature & t1_sig, const table_signature & t2_sig, unsigned col_cnt, const unsigned * cols1, const unsigned * cols2) 43 : convenient_table_join_fn(t1_sig, t2_sig, col_cnt, cols1, cols2), 44 m_joined_col_cnt(col_cnt) {} 45 operator ()(const table_base & t1,const table_base & t2)46 table_base * operator()(const table_base & t1, const table_base & t2) override { 47 48 const hashtable_table & ht1 = static_cast<const hashtable_table &>(t1); 49 const hashtable_table & ht2 = static_cast<const hashtable_table &>(t2); 50 51 hashtable_table_plugin & plugin = ht1.get_plugin(); 52 53 hashtable_table * res = static_cast<hashtable_table *>(plugin.mk_empty(get_result_signature())); 54 55 hashtable_table::storage::iterator els1it = ht1.m_data.begin(); 56 hashtable_table::storage::iterator els1end = ht1.m_data.end(); 57 hashtable_table::storage::iterator els2end = ht2.m_data.end(); 58 59 table_fact acc; 60 61 for(; els1it!=els1end; ++els1it) { 62 const table_fact & row1 = *els1it; 63 64 hashtable_table::storage::iterator els2it = ht2.m_data.begin(); 65 for(; els2it!=els2end; ++els2it) { 66 const table_fact & row2 = *els2it; 67 68 bool match=true; 69 for(unsigned i=0; i<m_joined_col_cnt; i++) { 70 if(row1[m_cols1[i]]!=row2[m_cols2[i]]) { 71 match=false; 72 break; 73 } 74 } 75 if(!match) { 76 continue; 77 } 78 79 acc.reset(); 80 acc.append(row1); 81 acc.append(row2); 82 res->m_data.insert(acc); 83 } 84 } 85 return res; 86 } 87 }; 88 mk_join_fn(const table_base & t1,const table_base & t2,unsigned col_cnt,const unsigned * cols1,const unsigned * cols2)89 table_join_fn * hashtable_table_plugin::mk_join_fn(const table_base & t1, const table_base & t2, 90 unsigned col_cnt, const unsigned * cols1, const unsigned * cols2) { 91 if(t1.get_kind()!=get_kind() || t2.get_kind()!=get_kind()) { 92 return nullptr; 93 } 94 return alloc(join_fn, t1.get_signature(), t2.get_signature(), col_cnt, cols1, cols2); 95 } 96 97 98 class hashtable_table::our_iterator_core : public iterator_core { 99 const hashtable_table & m_parent; 100 storage::iterator m_inner; 101 storage::iterator m_end; 102 103 class our_row : public row_interface { 104 const our_iterator_core & m_parent; 105 public: our_row(const our_iterator_core & parent)106 our_row(const our_iterator_core & parent) : row_interface(parent.m_parent), m_parent(parent) {} 107 get_fact(table_fact & result) const108 void get_fact(table_fact & result) const override { 109 result = *m_parent.m_inner; 110 } operator [](unsigned col) const111 table_element operator[](unsigned col) const override { 112 return (*m_parent.m_inner)[col]; 113 } 114 115 }; 116 117 our_row m_row_obj; 118 119 public: our_iterator_core(const hashtable_table & t,bool finished)120 our_iterator_core(const hashtable_table & t, bool finished) : 121 m_parent(t), m_inner(finished ? t.m_data.end() : t.m_data.begin()), 122 m_end(t.m_data.end()), m_row_obj(*this) {} 123 is_finished() const124 bool is_finished() const override { 125 return m_inner==m_end; 126 } 127 operator *()128 row_interface & operator*() override { 129 SASSERT(!is_finished()); 130 return m_row_obj; 131 } operator ++()132 void operator++() override { 133 SASSERT(!is_finished()); 134 ++m_inner; 135 } 136 }; 137 138 139 begin() const140 table_base::iterator hashtable_table::begin() const { 141 return mk_iterator(alloc(our_iterator_core, *this, false)); 142 } 143 end() const144 table_base::iterator hashtable_table::end() const { 145 return mk_iterator(alloc(our_iterator_core, *this, true)); 146 } 147 148 // ----------------------------------- 149 // 150 // bitvector_table 151 // 152 // ----------------------------------- 153 can_handle_signature(const table_signature & sig)154 bool bitvector_table_plugin::can_handle_signature(const table_signature & sig) { 155 if(sig.functional_columns()!=0) { 156 return false; 157 } 158 unsigned cols = sig.size(); 159 unsigned shift = 0; 160 for (unsigned i = 0; i < cols; ++i) { 161 unsigned s = static_cast<unsigned>(sig[i]); 162 if (s != sig[i] || !is_power_of_two(s)) { 163 return false; 164 } 165 unsigned num_bits = 0; 166 unsigned bit_pos = 1; 167 for (num_bits = 1; num_bits < 32; ++num_bits) { 168 if (bit_pos & s) { 169 break; 170 } 171 bit_pos <<= 1; 172 } 173 shift += num_bits; 174 if (shift >= 32) { 175 return false; 176 } 177 } 178 return true; 179 } 180 mk_empty(const table_signature & s)181 table_base * bitvector_table_plugin::mk_empty(const table_signature & s) { 182 SASSERT(can_handle_signature(s)); 183 return alloc(bitvector_table, *this, s); 184 } 185 186 class bitvector_table::bv_iterator : public iterator_core { 187 188 bitvector_table const& m_bv; 189 unsigned m_offset; 190 191 class our_row : public caching_row_interface { 192 const bv_iterator& m_parent; 193 public: our_row(const bv_iterator & p)194 our_row(const bv_iterator & p) : caching_row_interface(p.m_bv), m_parent(p) {} get_fact(table_fact & result) const195 void get_fact(table_fact& result) const override { 196 if (result.size() < size()) { 197 result.resize(size(), 0); 198 } 199 m_parent.m_bv.offset2fact(m_parent.m_offset, result); 200 } 201 }; 202 our_row m_row_obj; 203 204 public: bv_iterator(const bitvector_table & bv,bool end)205 bv_iterator(const bitvector_table& bv, bool end): 206 m_bv(bv), m_offset(end?m_bv.m_bv.size():0), m_row_obj(*this) 207 { 208 if (!is_finished() && !m_bv.m_bv.get(m_offset)) { 209 ++(*this); 210 } 211 } 212 is_finished() const213 bool is_finished() const override { 214 return m_offset == m_bv.m_bv.size(); 215 } 216 operator *()217 row_interface & operator*() override { 218 SASSERT(!is_finished()); 219 return m_row_obj; 220 } operator ++()221 void operator++() override { 222 SASSERT(!is_finished()); 223 ++m_offset; 224 while (!is_finished() && !m_bv.m_bv.get(m_offset)) { 225 ++m_offset; 226 } 227 m_row_obj.reset(); 228 } 229 }; 230 bitvector_table(bitvector_table_plugin & plugin,const table_signature & sig)231 bitvector_table::bitvector_table(bitvector_table_plugin & plugin, const table_signature & sig) 232 : table_base(plugin, sig){ 233 SASSERT(plugin.can_handle_signature(sig)); 234 235 m_num_cols = sig.size(); 236 unsigned shift = 0; 237 for (unsigned i = 0; i < m_num_cols; ++i) { 238 unsigned s = static_cast<unsigned>(sig[i]); 239 if (s != sig[i] || !is_power_of_two(s)) { 240 throw default_exception("bit-vector table is specialized to small domains that are powers of two"); 241 } 242 m_shift.push_back(shift); 243 m_mask.push_back(s - 1); 244 unsigned num_bits = 0; 245 unsigned bit_pos = 1; 246 for (num_bits = 1; num_bits < 32; ++num_bits) { 247 if (bit_pos & s) { 248 break; 249 } 250 bit_pos <<= 1; 251 } 252 shift += num_bits; 253 if (shift >= 32) { 254 throw default_exception("bit-vector table is specialized to small domains that are powers of two"); 255 } 256 } 257 m_bv.reserve(1 << shift); 258 } 259 fact2offset(const table_element * f) const260 unsigned bitvector_table::fact2offset(const table_element* f) const { 261 unsigned result = 0; 262 for (unsigned i = 0; i < m_num_cols; ++i) { 263 SASSERT(f[i] < get_signature()[i]); 264 result += ((unsigned)f[i]) << m_shift[i]; 265 } 266 return result; 267 } 268 offset2fact(unsigned offset,table_fact & f) const269 void bitvector_table::offset2fact(unsigned offset, table_fact& f) const { 270 SASSERT(m_num_cols == f.size()); 271 for (unsigned i = 0; i < m_num_cols; ++i) { 272 f[i] = m_mask[i] & (offset >> m_shift[i]); 273 } 274 } 275 add_fact(const table_fact & f)276 void bitvector_table::add_fact(const table_fact & f) { 277 m_bv.set(fact2offset(f.data())); 278 } 279 remove_fact(const table_element * fact)280 void bitvector_table::remove_fact(const table_element* fact) { 281 m_bv.unset(fact2offset(fact)); 282 } 283 contains_fact(const table_fact & f) const284 bool bitvector_table::contains_fact(const table_fact & f) const { 285 return m_bv.get(fact2offset(f.data())); 286 } 287 begin() const288 table_base::iterator bitvector_table::begin() const { 289 return mk_iterator(alloc(bv_iterator, *this, false)); 290 } 291 end() const292 table_base::iterator bitvector_table::end() const { 293 return mk_iterator(alloc(bv_iterator, *this, true)); 294 } 295 }; 296 297