1
2 /*++
3 Copyright (c) 2015 Microsoft Corporation
4
5 --*/
6
7 #ifdef _WINDOWS
8 #include "ast/reg_decl_plugins.h"
9 #include "muz/base/dl_context.h"
10 #include "muz/fp/dl_register_engine.h"
11 #include "muz/rel/dl_finite_product_relation.h"
12 #include "muz/rel/dl_sparse_table.h"
13 #include "muz/rel/rel_context.h"
14
15 namespace datalog {
16
17
18 typedef scoped_rel<table_base> table_aptr;
19
20 class collector_of_reduced : public table_row_pair_reduce_fn {
21 idx_set & m_acc;
22 public:
collector_of_reduced(idx_set & accumulator)23 collector_of_reduced(idx_set & accumulator) : m_acc(accumulator) {}
24
operator ()(table_element * func_columns,const table_element * merged_func_columns)25 virtual void operator()(table_element * func_columns, const table_element * merged_func_columns) {
26 m_acc.insert(static_cast<unsigned>(merged_func_columns[0]));
27 }
28 };
29
30
test_functional_columns(smt_params fparams,params_ref & params)31 void test_functional_columns(smt_params fparams, params_ref& params) {
32 ast_manager m;
33 reg_decl_plugins(m);
34 register_engine re;
35 context ctx(m, re, fparams);
36 rel_context_base& rctx = *ctx.get_rel_context();
37 ctx.updt_params(params);
38 relation_manager & rmgr(rctx.get_rmanager());
39
40 sparse_table_plugin & plugin =
41 static_cast<sparse_table_plugin &>(*rctx.get_rmanager().get_table_plugin(symbol("sparse")));
42 ENSURE(&plugin);
43 table_signature sig2;
44 sig2.push_back(2);
45 sig2.push_back(2);
46 sig2.set_functional_columns(1);
47 ENSURE(plugin.can_handle_signature(sig2));
48
49 table_fact f00;
50 f00.push_back(0);
51 f00.push_back(0);
52 table_fact f01;
53 f01.push_back(0);
54 f01.push_back(1);
55 table_fact f11;
56 f11.push_back(1);
57 f11.push_back(1);
58
59 {
60 table_aptr t0 = plugin.mk_empty(sig2);
61 ENSURE(t0->empty());
62 t0->add_fact(f00);
63 ENSURE(!t0->empty());
64 ENSURE(t0->get_size_estimate_rows()==1);
65 t0->add_fact(f01);
66 ENSURE(t0->get_size_estimate_rows()==1);
67 t0->add_fact(f11);
68 ENSURE(t0->get_size_estimate_rows()==2);
69
70 unsigned rem_cols0[]={0};
71 scoped_ptr<table_transformer_fn> project0 = rmgr.mk_project_fn(*t0, 1, rem_cols0);
72 table_aptr t1 = (*project0)(*t0);
73 ENSURE(t1->get_size_estimate_rows()==2);
74 ENSURE(t1->get_signature().functional_columns()==0); //project on non-functional column cancels functional
75
76 unsigned rem_cols1[]={1};
77 scoped_ptr<table_transformer_fn> project1 = rmgr.mk_project_fn(*t0, 1, rem_cols1);
78 table_aptr t2 = (*project1)(*t0);
79 ENSURE(t2->get_size_estimate_rows()==2);
80
81 idx_set acc;
82 collector_of_reduced * reducer = alloc(collector_of_reduced, acc);
83 scoped_ptr<table_transformer_fn> rproject = rmgr.mk_project_with_reduce_fn(*t0, 1, rem_cols0, reducer);
84 table_aptr rt = (*rproject)(*t0);
85 ENSURE(acc.num_elems()==1);
86 ENSURE(rt->get_size_estimate_rows()==1);
87 }
88 {
89 table_aptr t0 = plugin.mk_empty(sig2);
90 t0->add_fact(f01);
91
92 unsigned join_cols[]={1};
93 scoped_ptr<table_join_fn> join0 = rmgr.mk_join_fn(*t0, *t0, 1, join_cols, join_cols);
94 table_aptr t1 = (*join0)(*t0, *t0);
95 ENSURE(t1->get_signature().size()==4);
96 ENSURE(t1->get_signature().functional_columns()==2);
97
98 table_fact f0011;
99 f0011.push_back(0);
100 f0011.push_back(0);
101 f0011.push_back(1);
102 f0011.push_back(1);
103 ENSURE(t1->contains_fact(f0011));
104 table_fact f0111 = f0011;
105 f0111[1] = 1;
106 ENSURE(!t1->contains_fact(f0111));
107 }
108
109 {
110 table_aptr t0 = plugin.mk_empty(sig2);
111 t0->display(std::cout<<"0:");
112 ENSURE(t0->get_signature().functional_columns()==1);
113
114 table_fact aux_fact;
115
116 aux_fact = f01;
117 TRUSTME( t0->suggest_fact(aux_fact) );
118 t0->display(std::cout<<"1:");
119 ENSURE(t0->contains_fact(f01));
120 ENSURE(aux_fact[1]==1);
121
122 aux_fact = f00;
123 TRUSTME( !t0->suggest_fact(aux_fact) );
124 t0->display(std::cout<<"2:");
125 ENSURE(t0->contains_fact(f01));
126 ENSURE(!t0->contains_fact(f00));
127 ENSURE(aux_fact[1]==1);
128
129 t0->ensure_fact(f00);
130 t0->display(std::cout<<"3:");
131 ENSURE(t0->contains_fact(f00));
132 ENSURE(!t0->contains_fact(f01));
133 }
134 }
135
test_finite_product_relation(smt_params fparams,params_ref & params)136 void test_finite_product_relation(smt_params fparams, params_ref& params) {
137 ast_manager m;
138 reg_decl_plugins(m);
139 register_engine re;
140 context ctx(m, re, fparams);
141 ctx.updt_params(params);
142 dl_decl_util dl_util(m);
143 relation_manager & rmgr = ctx.get_rel_context()->get_rmanager();
144
145 relation_plugin & rel_plugin = *rmgr.get_relation_plugin(params.get_sym("default_relation", symbol("sparse")));
146 ENSURE(&rel_plugin);
147 finite_product_relation_plugin plg(rel_plugin, rmgr);
148
149 sort_ref byte_srt_ref(dl_util.mk_sort(symbol("BYTE"), 256), m);
150 relation_sort byte_srt = byte_srt_ref;
151
152 relation_signature sig2;
153 sig2.push_back(byte_srt);
154 sig2.push_back(byte_srt);
155 relation_signature sig3(sig2);
156 sig3.push_back(byte_srt);
157 relation_signature sig4(sig3);
158 sig4.push_back(byte_srt);
159
160 app_ref seven_ref(dl_util.mk_numeral(7, byte_srt), m);
161 app_ref nine_ref(dl_util.mk_numeral(9, byte_srt), m);
162
163 relation_element seven = seven_ref;
164 relation_element nine = nine_ref;
165
166 relation_fact f7(m);
167 f7.push_back(seven);
168 relation_fact f9(m);
169 f9.push_back(nine);
170
171 relation_fact f77(f7);
172 f77.push_back(seven);
173 relation_fact f79(f7);
174 f79.push_back(nine);
175 relation_fact f97(f9);
176 f97.push_back(seven);
177 relation_fact f99(f9);
178 f99.push_back(nine);
179
180 relation_fact f779(f77);
181 f779.push_back(nine);
182 relation_fact f799(f79);
183 f799.push_back(nine);
184 relation_fact f977(f97);
185 f977.push_back(seven);
186
187 relation_fact f7797(f779);
188 f7797.push_back(seven);
189 relation_fact f7997(f799);
190 f7997.push_back(seven);
191
192
193 bool table_cols2[] = { true, false };
194 bool table_cols3[] = { true, false, false };
195 bool table_cols4[] = { true, true, false, false };
196 scoped_rel<relation_base> r1 = plg.mk_empty(sig2, table_cols2);
197 scoped_rel<relation_base> r2 = r1->clone();
198 scoped_rel<relation_base> r3 = r2->clone();
199
200 ENSURE(!r1->contains_fact(f77));
201 r1->add_fact(f77);
202 ENSURE(r1->contains_fact(f77));
203
204 r2->add_fact(f79);
205 r3->add_fact(f99);
206
207
208 r2->display( std::cout << "r2 0\n");
209 scoped_rel<relation_base> r4 = r2->clone();
210 r2->display( std::cout << "r2 1\n");
211
212 r4->display( std::cout << "r4 0\n");
213 ENSURE(!r4->contains_fact(f77));
214 ENSURE(r4->contains_fact(f79));
215 r4->add_fact(f77);
216 r4->display( std::cout << "r4 1\n");
217 ENSURE(r4->contains_fact(f77));
218 ENSURE(r4->contains_fact(f79));
219 r4->add_fact(f99);
220 r4->display( std::cout << "r4 2\n");
221 ENSURE(r4->contains_fact(f99));
222
223
224 std::cout << "------ testing union ------\n";
225 r2->display( std::cout << "r2\n");
226 scoped_ptr<relation_union_fn> union_op = rmgr.mk_union_fn(*r1, *r2, r3.get());
227 ENSURE(union_op);
228 (*union_op)(*r1, *r2, r3.get());
229
230 r1->display( std::cout << "r1\n");
231 r2->display( std::cout << "r2\n");
232 r3->display( std::cout << "r3\n");
233
234 ENSURE(r1->contains_fact(f77));
235 ENSURE(r1->contains_fact(f79));
236 ENSURE(!r1->contains_fact(f99));
237
238 ENSURE(!r3->contains_fact(f77));
239 ENSURE(r3->contains_fact(f79));
240 ENSURE(r3->contains_fact(f99));
241
242 std::cout << "------ testing join ------\n";
243
244 r1->reset();
245 r1->add_fact(f77);
246 r1->add_fact(f79);
247 r1->add_fact(f97);
248 r2->reset();
249 r2->add_fact(f97);
250 r2->add_fact(f99);
251
252 unsigned col0[] = { 0 };
253 unsigned col1[] = { 1 };
254 scoped_ptr<relation_join_fn> join_tt = rmgr.mk_join_fn(*r1, *r2, 1, col0, col0);
255 scoped_ptr<relation_join_fn> join_tr = rmgr.mk_join_fn(*r1, *r2, 1, col0, col1);
256 scoped_ptr<relation_join_fn> join_rr = rmgr.mk_join_fn(*r1, *r2, 1, col1, col1);
257
258 r1->display( std::cout << "r1\n");
259 r2->display( std::cout << "r2\n");
260
261 scoped_rel<relation_base> jr_tt = (*join_tt)(*r1, *r2);
262 scoped_rel<relation_base> jr_tr = (*join_tr)(*r1, *r2);
263 scoped_rel<relation_base> jr_rr = (*join_rr)(*r1, *r2);
264
265 jr_tt->display( std::cout << "tt\n");
266 jr_tr->display( std::cout << "tr\n");
267 jr_rr->display( std::cout << "rr\n");
268
269
270 ENSURE(!jr_tt->contains_fact(f7797));
271 ENSURE(jr_tr->contains_fact(f7797));
272 ENSURE(jr_rr->contains_fact(f7797));
273
274
275 std::cout << "------ testing project ------\n";
276
277 scoped_rel<relation_base> r31 = plg.mk_empty(sig3, table_cols3);
278 r31->add_fact(f779);
279 r31->add_fact(f977);
280 r31->add_fact(f799);
281
282 unsigned rem_1_rel[] = { 1 };
283 unsigned rem_2_rel[] = { 1, 2 };
284 unsigned rem_1_table[] = { 0 };
285
286 scoped_ptr<relation_transformer_fn> proj_1r = rmgr.mk_project_fn(*r31, 1, rem_1_rel);
287 scoped_ptr<relation_transformer_fn> proj_2r = rmgr.mk_project_fn(*r31, 2, rem_2_rel);
288 scoped_ptr<relation_transformer_fn> proj_1t = rmgr.mk_project_fn(*r31, 1, rem_1_table);
289
290 scoped_rel<relation_base> sr_1r = (*proj_1r)(*r31);
291 scoped_rel<relation_base> sr_2r = (*proj_2r)(*r31);
292 scoped_rel<relation_base> sr_1t = (*proj_1t)(*r31);
293
294 ENSURE(sr_1r->contains_fact(f79));
295 ENSURE(sr_1r->contains_fact(f97));
296 ENSURE(!sr_1r->contains_fact(f77));
297
298 ENSURE(sr_2r->contains_fact(f7));
299 ENSURE(sr_2r->contains_fact(f9));
300
301 ENSURE(sr_1t->contains_fact(f79));
302 ENSURE(!sr_1t->contains_fact(f97));
303 ENSURE(sr_1t->contains_fact(f77));
304 ENSURE(sr_1t->contains_fact(f99));
305
306 std::cout << "------ testing filter_interpreted ------\n";
307
308 scoped_rel<relation_base> r41 = plg.mk_empty(sig4, table_cols4);
309
310 r41->add_fact(f7797);
311 r41->add_fact(f7997);
312
313 app_ref cond(m.mk_and(
314 m.mk_not(m.mk_eq(m.mk_var(1,byte_srt), m.mk_var(2,byte_srt))), //#1!=#2
315 m.mk_not(m.mk_eq(m.mk_var(3,byte_srt), m.mk_var(2,byte_srt))) //#3!=#2
316 ), m);
317 scoped_ptr<relation_mutator_fn> i_filter = rmgr.mk_filter_interpreted_fn(*r41, cond);
318 (*i_filter)(*r41);
319
320 ENSURE(r41->contains_fact(f7797));
321 ENSURE(!r41->contains_fact(f7997));
322
323 std::cout << "------ testing filter_by_negation ------\n";
324
325 r31->reset();
326 r31->add_fact(f779);
327 r31->add_fact(f977);
328 r31->add_fact(f799);
329
330 r1->reset();
331 r1->add_fact(f77);
332 r1->add_fact(f79);
333
334 unsigned nf_r31_cols[] = {1, 0, 1};
335 unsigned nf_r1_cols[] = {0, 0, 1};
336 scoped_ptr<relation_intersection_filter_fn> neg_filter = rmgr.mk_filter_by_negation_fn(*r31, *r1, 3,
337 nf_r31_cols, nf_r1_cols);
338 (*neg_filter)(*r31, *r1);
339
340 ENSURE(!r31->contains_fact(f779));
341 ENSURE(r31->contains_fact(f977));
342 ENSURE(r31->contains_fact(f799));
343
344
345 }
346 }
347
348
349
350
351
352 using namespace datalog;
353
tst_dl_product_relation()354 void tst_dl_product_relation() {
355 smt_params fparams;
356 params_ref params;
357
358 test_functional_columns(fparams, params);
359
360 params.set_sym("default_relation", symbol("tr_sparse"));
361 test_finite_product_relation(fparams, params);
362
363 }
364 #else
tst_dl_product_relation()365 void tst_dl_product_relation() {
366 }
367 #endif
368