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