1
2 /*++
3 Copyright (c) 2015 Microsoft Corporation
4
5 --*/
6
7 #include "muz/rel/udoc_relation.h"
8 #include "util/trace.h"
9 #include "util/vector.h"
10 #include "ast/ast.h"
11 #include "ast/ast_pp.h"
12 #include "ast/reg_decl_plugins.h"
13 #include "util/sorting_network.h"
14 #include "smt/smt_kernel.h"
15 #include "model/model_smt2_pp.h"
16 #include "smt/params/smt_params.h"
17 #include "ast/ast_util.h"
18 #include "ast/rewriter/expr_safe_replace.h"
19 #include "ast/rewriter/th_rewriter.h"
20 #include "muz/rel/dl_relation_manager.h"
21 #include "muz/fp/dl_register_engine.h"
22 #include "muz/rel/rel_context.h"
23 #include "ast/bv_decl_plugin.h"
24 #include "muz/rel/check_relation.h"
25
26
27 class udoc_tester {
28 typedef datalog::relation_base relation_base;
29 typedef datalog::udoc_relation udoc_relation;
30 typedef datalog::udoc_plugin udoc_plugin;
31 typedef datalog::relation_signature relation_signature;
32 typedef datalog::relation_fact relation_fact;
33 typedef scoped_ptr<datalog::relation_mutator_fn> rel_mut;
34 typedef scoped_ptr<datalog::relation_union_fn> rel_union;
35
36 struct init {
initudoc_tester::init37 init(ast_manager& m) {
38 reg_decl_plugins(m);
39 }
40 };
41 random_gen m_rand;
42 ast_manager m;
43 init m_init;
44 bv_util bv;
45 expr_ref_vector m_vars;
46 smt_params m_smt_params;
47 datalog::register_engine m_reg;
48 datalog::context m_ctx;
49 datalog::rel_context rc;
50 udoc_plugin& p;
51 datalog::check_relation_plugin& cr;
52
53
choose_tbit()54 tbit choose_tbit() {
55 switch (m_rand(3)) {
56 case 0: return BIT_0;
57 case 1: return BIT_1;
58 default : return BIT_x;
59 }
60 }
61
mk_rand_tbv(doc_manager & dm)62 tbv* mk_rand_tbv(doc_manager& dm) {
63 tbv* result = dm.tbvm().allocate();
64 for (unsigned i = 0; i < dm.num_tbits(); ++i) {
65 dm.tbvm().set(*result, i, choose_tbit());
66 }
67 return result;
68 }
69
mk_rand_tbv(doc_manager & dm,tbv const & pos)70 tbv* mk_rand_tbv(doc_manager& dm, tbv const& pos) {
71 tbv* result = dm.tbvm().allocate();
72 for (unsigned i = 0; i < dm.num_tbits(); ++i) {
73 if (pos[i] == BIT_x) {
74 dm.tbvm().set(*result, i, choose_tbit());
75 }
76 else {
77 dm.tbvm().set(*result, i, pos[i]);
78 }
79 }
80 return result;
81 }
82
mk_rand_doc(doc_manager & dm,unsigned num_diff)83 doc* mk_rand_doc(doc_manager& dm, unsigned num_diff) {
84 tbv_ref t(dm.tbvm());
85 doc_ref result(dm);
86 t = mk_rand_tbv(dm);
87 result = dm.allocate(*t);
88 ENSURE(dm.tbvm().equals(*t, result->pos()));
89 for (unsigned i = 0; i < num_diff; ++i) {
90 t = mk_rand_tbv(dm, result->pos());
91 if (dm.tbvm().equals(*t, result->pos())) {
92 return nullptr;
93 }
94 if (!result->neg().is_empty() &&
95 dm.tbvm().equals(*t, result->neg()[0])) {
96 continue;
97 }
98 result->neg().push_back(t.detach());
99 }
100 ENSURE(dm.well_formed(*result));
101 return result.detach();
102 }
103
mk_rand_udoc(doc_manager & dm,unsigned num_elems,unsigned num_diff,udoc & result)104 void mk_rand_udoc(doc_manager& dm, unsigned num_elems, unsigned num_diff, udoc& result) {
105 result.reset(dm);
106 for (unsigned i = 0; i < num_elems; ++i) {
107 doc* d = mk_rand_doc(dm, num_diff);
108 if (d) {
109 result.push_back(d);
110 }
111 }
112 }
113
114 public:
udoc_tester()115 udoc_tester():
116 m_init(m), bv(m), m_vars(m), m_ctx(m, m_reg, m_smt_params), rc(m_ctx),
117 p(dynamic_cast<udoc_plugin&>(*rc.get_rmanager().get_relation_plugin(symbol("doc")))),
118 cr(dynamic_cast<datalog::check_relation_plugin&>(*rc.get_rmanager().get_relation_plugin(symbol("check_relation"))))
119 {
120 cr.set_plugin(&p);
121 }
122
mk_empty(relation_signature const & sig)123 udoc_relation* mk_empty(relation_signature const& sig) {
124 ENSURE(p.can_handle_signature(sig));
125 relation_base* empty = p.mk_empty(sig);
126 return dynamic_cast<udoc_relation*>(empty);
127 }
128
mk_full(relation_signature const & sig)129 udoc_relation* mk_full(relation_signature const& sig) {
130 func_decl_ref fn(m);
131 fn = m.mk_func_decl(symbol("full"), sig.size(), sig.data(), m.mk_bool_sort());
132 relation_base* full = p.mk_full(fn, sig);
133 return dynamic_cast<udoc_relation*>(full);
134 }
135
test1()136 void test1() {
137 datalog::relation_signature sig;
138 sig.push_back(bv.mk_sort(12));
139 sig.push_back(bv.mk_sort(6));
140 sig.push_back(bv.mk_sort(12));
141
142
143 datalog::relation_fact fact1(m), fact2(m), fact3(m);
144 fact1.push_back(bv.mk_numeral(rational(1), 12));
145 fact1.push_back(bv.mk_numeral(rational(6), 6));
146 fact1.push_back(bv.mk_numeral(rational(56), 12));
147 fact2.push_back(bv.mk_numeral(rational(8), 12));
148 fact2.push_back(bv.mk_numeral(rational(16), 6));
149 fact2.push_back(bv.mk_numeral(rational(32), 12));
150 fact3.push_back(bv.mk_numeral(rational(32), 12));
151 fact3.push_back(bv.mk_numeral(rational(16), 6));
152 fact3.push_back(bv.mk_numeral(rational(4), 12));
153
154 relation_signature sig2;
155 sig2.push_back(bv.mk_sort(3));
156 sig2.push_back(bv.mk_sort(6));
157 sig2.push_back(bv.mk_sort(3));
158 sig2.push_back(bv.mk_sort(3));
159 sig2.push_back(bv.mk_sort(3));
160
161 relation_base* t;
162 udoc_relation* t1, *t2, *t3;
163 expr_ref fml(m);
164
165 test_filter_neg2();
166
167 test_join_project();
168 test_join_project2();
169 test_join_project3();
170
171 test_filter_neg4(false);
172 test_filter_neg4(true);
173 test_filter_neg5(false);
174 test_filter_neg5(true);
175
176 test_filter_neg();
177 test_filter_neg3();
178
179 test_join(1000);
180
181 test_rename();
182
183
184 // empty
185 {
186 std::cout << "empty\n";
187 t = mk_empty(sig);
188 t->display(std::cout); std::cout << "\n";
189 t->to_formula(fml);
190 std::cout << fml << "\n";
191 t->deallocate();
192 }
193
194 // full
195 {
196 std::cout << "full\n";
197 t = mk_full(sig);
198 t->display(std::cout); std::cout << "\n";
199 t->to_formula(fml);
200 std::cout << fml << "\n";
201 t->deallocate();
202 }
203
204 // join
205 {
206 t1 = mk_full(sig);
207 t2 = mk_full(sig);
208 t3 = mk_empty(sig);
209 unsigned_vector jc1, jc2;
210 jc1.push_back(1);
211 jc2.push_back(1);
212 datalog::relation_join_fn* join_fn = p.mk_join_fn(*t1, *t2, jc1.size(), jc1.data(), jc2.data());
213 ENSURE(join_fn);
214 t = (*join_fn)(*t1, *t2);
215 cr.verify_join(*t1, *t2, *t, jc1, jc2);
216 t->display(std::cout); std::cout << "\n";
217 t->deallocate();
218
219 t = (*join_fn)(*t1, *t3);
220 cr.verify_join(*t1, *t3, *t, jc1, jc2);
221 ENSURE(t->empty());
222 t->display(std::cout); std::cout << "\n";
223 t->deallocate();
224
225 t = (*join_fn)(*t3, *t3);
226 cr.verify_join(*t3, *t3, *t, jc1, jc2);
227 ENSURE(t->empty());
228 t->display(std::cout); std::cout << "\n";
229 t->deallocate();
230
231 dealloc(join_fn);
232 t1->deallocate();
233 t2->deallocate();
234 t3->deallocate();
235 }
236
237 // project
238 {
239 std::cout << "project\n";
240 t1 = mk_full(sig);
241 unsigned_vector pc;
242 pc.push_back(0);
243 datalog::relation_transformer_fn* proj_fn = p.mk_project_fn(*t1, pc.size(), pc.data());
244 t = (*proj_fn)(*t1);
245 cr.verify_project(*t1, *t, pc);
246 t->display(std::cout); std::cout << "\n";
247 t->deallocate();
248
249 t1->reset();
250 t = (*proj_fn)(*t1);
251 cr.verify_project(*t1, *t, pc);
252 t->display(std::cout); std::cout << "\n";
253 t->deallocate();
254
255 t1->add_fact(fact1);
256 t1->add_fact(fact2);
257 t1->add_fact(fact3);
258 t = (*proj_fn)(*t1);
259 cr.verify_project(*t1, *t, pc);
260 t1->display(std::cout); std::cout << "\n";
261 t->display(std::cout); std::cout << "\n";
262 t->deallocate();
263
264 dealloc(proj_fn);
265 t1->deallocate();
266 }
267
268 // union
269 {
270 t1 = mk_empty(sig);
271 t2 = mk_empty(sig);
272 udoc_relation* delta = mk_full(sig);
273 t2->add_fact(fact1);
274 t2->add_fact(fact2);
275 t1->add_fact(fact3);
276
277 expr_ref t10(m);
278 t1->to_formula(t10);
279 expr_ref delta0(m);
280 delta->to_formula(delta0);
281 rel_union union_fn = p.mk_union_fn(*t1, *t2, nullptr);
282
283 t1->display(std::cout << "t1 before:"); std::cout << "\n";
284 (*union_fn)(*t1, *t2, delta);
285 cr.verify_union(t10, *t2, *t1, delta0, delta);
286 t1->display(std::cout << "t1 after:"); std::cout << "\n";
287 delta->display(std::cout << "delta:"); std::cout << "\n";
288
289 t1->deallocate();
290 t2->deallocate();
291 delta->deallocate();
292 }
293
294 // filter_identical
295 {
296 t1 = mk_empty(sig2);
297 unsigned_vector id;
298 id.push_back(0);
299 id.push_back(2);
300 id.push_back(4);
301 rel_mut filter_id = p.mk_filter_identical_fn(*t1, id.size(), id.data());
302 relation_fact f1(m);
303 f1.push_back(bv.mk_numeral(rational(1),3));
304 f1.push_back(bv.mk_numeral(rational(1),6));
305 f1.push_back(bv.mk_numeral(rational(1),3));
306 f1.push_back(bv.mk_numeral(rational(1),3));
307 f1.push_back(bv.mk_numeral(rational(1),3));
308 t1->add_fact(f1);
309 f1[4] = bv.mk_numeral(rational(2),3);
310 t1->add_fact(f1);
311 t1->display(std::cout); std::cout << "\n";
312 (*filter_id)(*t1);
313 t1->display(std::cout); std::cout << "\n";
314 t1->deallocate();
315 }
316
317 // tbv_manager::debug_alloc();
318 {
319 relation_signature sig3;
320 sig3.push_back(m.mk_bool_sort());
321 sig3.push_back(m.mk_bool_sort());
322 sig3.push_back(m.mk_bool_sort());
323 var_ref v0(m.mk_var(0, m.mk_bool_sort()),m);
324 var_ref v1(m.mk_var(1, m.mk_bool_sort()),m);
325 var_ref v2(m.mk_var(2, m.mk_bool_sort()),m);
326 app_ref cond1(m);
327 t1 = mk_full(sig3);
328 cond1 = m.mk_eq(v0,v1);
329 apply_filter(*t1, cond1);
330 t1->deallocate();
331 }
332
333 {
334 relation_signature sig3;
335 sig3.push_back(m.mk_bool_sort());
336 sig3.push_back(m.mk_bool_sort());
337 sig3.push_back(m.mk_bool_sort());
338 var_ref v0(m.mk_var(0, m.mk_bool_sort()),m);
339 var_ref v1(m.mk_var(1, m.mk_bool_sort()),m);
340 var_ref v2(m.mk_var(2, m.mk_bool_sort()),m);
341 app_ref cond1(m);
342 t1 = mk_full(sig3);
343 cond1 = m.mk_or(m.mk_eq(v0,v1),m.mk_eq(v0,v2));
344 apply_filter(*t1, cond1);
345 t1->deallocate();
346 }
347
348 {
349 relation_signature sig3;
350 sig3.push_back(bv.mk_sort(1));
351 sig3.push_back(bv.mk_sort(1));
352 sig3.push_back(bv.mk_sort(1));
353 var_ref v0(m.mk_var(0, bv.mk_sort(1)),m);
354 var_ref v1(m.mk_var(1, bv.mk_sort(1)),m);
355 var_ref v2(m.mk_var(2, bv.mk_sort(1)),m);
356 app_ref cond1(m);
357 cond1 = m.mk_or(m.mk_eq(v0,v1),m.mk_eq(v0,v2));
358 t1 = mk_full(sig3);
359 apply_filter(*t1, cond1);
360 t1->deallocate();
361 }
362
363
364 app_ref_vector conds(m);
365 app_ref cond1(m);
366 var_ref v0(m.mk_var(0, bv.mk_sort(3)),m);
367 var_ref v1(m.mk_var(1, bv.mk_sort(6)),m);
368 var_ref v2(m.mk_var(2, bv.mk_sort(3)),m);
369 var_ref v3(m.mk_var(3, bv.mk_sort(3)),m);
370 var_ref v4(m.mk_var(4, bv.mk_sort(3)),m);
371 conds.push_back(m.mk_true());
372 conds.push_back(m.mk_false());
373 conds.push_back(m.mk_eq(v0, v2));
374 conds.push_back(m.mk_not(m.mk_eq(v0, v2)));
375 conds.push_back(m.mk_eq(v0, bv.mk_numeral(rational(2), 3)));
376 cond1 = m.mk_eq(ex(2,1,v0),bv.mk_numeral(rational(3),2));
377 conds.push_back(cond1);
378 conds.push_back(m.mk_or(cond1,m.mk_eq(v3,v4)));
379 conds.push_back(m.mk_eq(ex(2,1,v3),ex(1,0,v4)));
380 conds.push_back(m.mk_or(cond1,m.mk_eq(ex(2,1,v3),ex(1,0,v4))));
381 conds.push_back(m.mk_or(m.mk_eq(v0,v2),m.mk_eq(v0,v4)));
382 conds.push_back(m.mk_or(m.mk_eq(v0,v2),m.mk_eq(v3,v4)));
383 conds.push_back(m.mk_or(m.mk_eq(ex(2,1,v0),ex(1,0,v2)),m.mk_eq(v3,v4)));
384 conds.push_back(m.mk_or(m.mk_eq(ex(2,1,v0),bv.mk_numeral(rational(3),2)),
385 m.mk_eq(v3,v4)));
386 conds.push_back(m.mk_or(m.mk_eq(ex(2,1,v0),bv.mk_numeral(rational(3),2)),
387 m.mk_eq(v3,bv.mk_numeral(rational(3),3))));
388 conds.push_back(m.mk_or(m.mk_eq(v0,bv.mk_numeral(rational(5),3)),
389 m.mk_eq(v3,bv.mk_numeral(rational(5),3))));
390 conds.push_back(m.mk_or(m.mk_eq(v0,bv.mk_numeral(rational(7),3)),
391 m.mk_eq(v3,bv.mk_numeral(rational(7),3))));
392 conds.push_back(m.mk_not(m.mk_or(m.mk_eq(v0,v2),m.mk_eq(v3,v4))));
393
394
395 // filter_interpreted
396 {
397 std::cout << "filter interpreted\n";
398 t1 = mk_full(sig2);
399
400 for (unsigned i = 0; i < conds.size(); ++i) {
401 apply_filter(*t1, conds[i].get());
402 }
403
404 t1->deallocate();
405
406 }
407
408 // filter_interpreted_project
409 {
410 unsigned_vector remove;
411 remove.push_back(0);
412 remove.push_back(2);
413
414 t1 = mk_full(sig2);
415 apply_filter(*t1, conds[2].get());
416 apply_filter_project(*t1, remove, conds[2].get());
417 apply_filter_project(*t1, remove, conds[3].get());
418 t1->deallocate();
419
420 t1 = mk_full(sig2);
421 apply_filter(*t1, conds[3].get());
422 apply_filter_project(*t1, remove, conds[2].get());
423 apply_filter_project(*t1, remove, conds[3].get());
424 t1->deallocate();
425
426 for (unsigned i = 0; i < conds.size(); ++i) {
427 t1 = mk_full(sig2);
428 apply_filter_project(*t1, remove, conds[i].get());
429 t1->deallocate();
430 }
431
432 remove[1] = 1;
433 for (unsigned i = 0; i < conds.size(); ++i) {
434 t1 = mk_full(sig2);
435 apply_filter_project(*t1, remove, conds[i].get());
436 t1->deallocate();
437 }
438 }
439
440
441 }
442
443 // {11xx \ {111x}, x011 \ {x011}, 0111}
444 // {xx11 \ {0011, 1111, x111}}
445 // 0111
446 // {1x1x \ {1x1x}, 1111 \ {1111}, x1x1 \ {x1x1}}
447
test_join_project()448 void test_join_project()
449 {
450 datalog::relation_signature sig;
451 sig.push_back(bv.mk_sort(2));
452 sig.push_back(bv.mk_sort(2));
453 //sig.push_back(bv.mk_sort(3));
454
455 unsigned_vector jc1, jc2, pc;
456 jc1.push_back(0);
457 jc2.push_back(0);
458 pc.push_back(1);
459 pc.push_back(3);
460 //pc.push_back(4);
461 udoc_relation* t1, *t2;
462 relation_base* t;
463
464 scoped_ptr<datalog::relation_join_fn> join_project_fn;
465
466 for (unsigned i = 0; i < 200; ++i) {
467 t1 = mk_rand(sig);
468 t2 = mk_rand(sig);
469 t1->display(std::cout);
470 t2->display(std::cout);
471 join_project_fn = p.mk_join_project_fn(*t1, *t2, jc1.size(), jc1.data(), jc2.data(), pc.size(), pc.data());
472 t = (*join_project_fn)(*t1, *t2);
473 t->display(std::cout);
474 cr.verify_join_project(*t1, *t2, *t, jc1, jc2, pc);
475 t->deallocate();
476 t1->deallocate();
477 t2->deallocate();
478 }
479 }
480
test_join_project2()481 void test_join_project2()
482 {
483 relation_signature sig3;
484 sig3.push_back(bv.mk_sort(1));
485 sig3.push_back(bv.mk_sort(1));
486 sig3.push_back(bv.mk_sort(1));
487
488 /// xxx \ x11
489 udoc_relation *t1 = mk_full(sig3);
490 {
491 udoc_relation *neg = mk_full(sig3);
492 doc& n = neg->get_udoc()[0];
493 neg->get_dm().set(n, 1, BIT_1);
494 neg->get_dm().set(n, 2, BIT_1);
495
496 unsigned_vector allcols;
497 allcols.push_back(0);
498 allcols.push_back(1);
499 allcols.push_back(2);
500 apply_filter_neg(*t1, *neg, allcols, allcols);
501 neg->deallocate();
502 }
503
504 // 11x
505 udoc_relation *t2 = mk_full(sig3);
506 {
507 doc& n = t2->get_udoc()[0];
508 t2->get_dm().set(n, 0, BIT_1);
509 t2->get_dm().set(n, 1, BIT_1);
510 }
511
512 unsigned_vector jc1, jc2, pc;
513 jc1.push_back(1);
514 jc1.push_back(2);
515 jc2.push_back(0);
516 jc2.push_back(1);
517 pc.push_back(1);
518 pc.push_back(2);
519
520 scoped_ptr<datalog::relation_join_fn> join_project_fn;
521 join_project_fn = p.mk_join_project_fn(*t1, *t2, jc1.size(), jc1.data(), jc2.data(), pc.size(), pc.data());
522 relation_base *t = (*join_project_fn)(*t1, *t2);
523 cr.verify_join_project(*t1, *t2, *t, jc1, jc2, pc);
524 t->deallocate();
525 t1->deallocate();
526 t2->deallocate();
527 }
528
test_join_project3()529 void test_join_project3()
530 {
531 datalog::relation_signature sig;
532 sig.push_back(bv.mk_sort(2));
533 sig.push_back(bv.mk_sort(2));
534
535 unsigned_vector jc1, jc2, pc;
536 jc1.push_back(0);
537 jc1.push_back(1);
538 jc2.push_back(1);
539 jc2.push_back(0);
540 pc.push_back(0);
541 pc.push_back(1);
542
543 scoped_ptr<datalog::relation_join_fn> join_project_fn;
544
545 udoc_relation* t1 = mk_empty(sig);
546 {
547 datalog::relation_fact fact1(m);
548 fact1.push_back(bv.mk_numeral(rational(3), 2));
549 fact1.push_back(bv.mk_numeral(rational(1), 2));
550 t1->add_fact(fact1);
551 }
552
553 udoc_relation *t2 = mk_empty(sig);
554 {
555 datalog::relation_fact fact1(m);
556 fact1.push_back(bv.mk_numeral(rational(0), 2));
557 fact1.push_back(bv.mk_numeral(rational(3), 2));
558 t2->add_fact(fact1);
559 fact1.reset();
560 fact1.push_back(bv.mk_numeral(rational(1), 2));
561 fact1.push_back(bv.mk_numeral(rational(3), 2));
562 t2->add_fact(fact1);
563 }
564
565 t1->display(std::cout << "t1:");
566 t2->display(std::cout << "t2:");
567 join_project_fn = p.mk_join_project_fn(*t1, *t2, jc1.size(), jc1.data(), jc2.data(), pc.size(), pc.data());
568
569 relation_base* t;
570 t = (*join_project_fn)(*t1, *t2);
571 t->display(std::cout << "t:");
572 cr.verify_join_project(*t1, *t2, *t, jc1, jc2, pc);
573 t->deallocate();
574 t1->deallocate();
575 t2->deallocate();
576 }
577
test_rename()578 void test_rename() {
579 udoc_relation* t1;
580 // rename
581 datalog::relation_signature sig;
582 sig.push_back(bv.mk_sort(12));
583 sig.push_back(bv.mk_sort(6));
584 sig.push_back(bv.mk_sort(2));
585 datalog::relation_fact fact1(m);
586 fact1.push_back(bv.mk_numeral(rational(1), 12));
587 fact1.push_back(bv.mk_numeral(rational(6), 6));
588 fact1.push_back(bv.mk_numeral(rational(3), 2));
589 t1 = mk_empty(sig);
590 t1->add_fact(fact1);
591 unsigned_vector cycle;
592 cycle.push_back(0);
593 cycle.push_back(2);
594 check_permutation(t1, cycle);
595
596 sig.reset();
597 sig.push_back(bv.mk_sort(2));
598 sig.push_back(bv.mk_sort(6));
599 sig.push_back(bv.mk_sort(12));
600 fact1.reset();
601 fact1.push_back(bv.mk_numeral(rational(3), 2));
602 fact1.push_back(bv.mk_numeral(rational(6), 6));
603 fact1.push_back(bv.mk_numeral(rational(1), 12));
604 t1 = mk_empty(sig);
605 t1->add_fact(fact1);
606 cycle.reset();
607 cycle.push_back(0);
608 cycle.push_back(2);
609 check_permutation(t1, cycle);
610
611 t1 = mk_empty(sig);
612 t1->add_fact(fact1);
613 cycle.reset();
614 cycle.push_back(0);
615 cycle.push_back(1);
616 cycle.push_back(2);
617 check_permutation(t1, cycle);
618 }
619
test_join(unsigned num_rounds)620 void test_join(unsigned num_rounds) {
621 for (unsigned i = 0; i < num_rounds; ++i) {
622 test_join();
623 }
624 }
625
test_join()626 void test_join() {
627 relation_signature sig;
628 sig.push_back(bv.mk_sort(2));
629 sig.push_back(bv.mk_sort(3));
630 udoc_relation* t1, *t2;
631 relation_base* t;
632
633 t1 = mk_rand(sig);
634 t2 = mk_rand(sig);
635
636 unsigned_vector jc1, jc2;
637 jc1.push_back(0);
638 jc2.push_back(0);
639 scoped_ptr<datalog::relation_join_fn> join_fn;
640
641 join_fn = p.mk_join_fn(*t1, *t2, jc1.size(), jc1.data(), jc2.data());
642 t = (*join_fn)(*t1, *t2);
643
644 cr.verify_join(*t1, *t2, *t, jc1, jc2);
645 t1->display(std::cout);
646 t2->display(std::cout);
647 t->display(std::cout);
648 std::cout << "\n";
649 t1->deallocate();
650 t2->deallocate();
651 t->deallocate();
652 }
653
mk_rand(relation_signature const & sig)654 udoc_relation* mk_rand(relation_signature const& sig) {
655 udoc_relation* t = mk_empty(sig);
656 mk_rand_udoc(t->get_dm(), 3, 3, t->get_udoc());
657 return t;
658 }
659
check_permutation(relation_base * t1,unsigned_vector const & cycle)660 void check_permutation(relation_base* t1, unsigned_vector const& cycle) {
661 scoped_ptr<datalog::relation_transformer_fn> rename;
662 rename = p.mk_rename_fn(*t1, cycle.size(), cycle.data());
663 relation_base* t = (*rename)(*t1);
664 cr.verify_permutation(*t1,*t, cycle);
665 t1->display(std::cout); std::cout << "\n";
666 t->display(std::cout); std::cout << "\n";
667 t->deallocate();
668 t1->deallocate();
669 }
670
671 /*
672 The filter_by_negation postcondition:
673 filter_by_negation(tgt, neg, columns in tgt: c1,...,cN,
674 corresponding columns in neg: d1,...,dN):
675 tgt_1:={x: x\in tgt_0 && ! \exists y: ( y \in neg & pi_c1(x)= pi_d1(y) & ... & pi_cN(x)= pi_dN(y) ) }
676 */
677
test_filter_neg()678 void test_filter_neg() {
679 // filter_by_negation
680
681 relation_signature sig4;
682 sig4.push_back(bv.mk_sort(1));
683 sig4.push_back(bv.mk_sort(1));
684 sig4.push_back(bv.mk_sort(1));
685 udoc_relation* t1 = mk_empty(sig4);
686 udoc_relation* t2 = mk_empty(sig4);
687 unsigned_vector cols1, cols2;
688 unsigned num_bits = t1->get_dm().num_tbits();
689
690 cols1.push_back(0);
691 cols2.push_back(1);
692 for (unsigned i = 0; i < 100; ++i) {
693 set_random(*t1, 2*num_bits/3);
694 set_random(*t2, 2*num_bits/3);
695 apply_filter_neg(*t1,*t2, cols1, cols2);
696 }
697 cols1.push_back(1);
698 cols2.push_back(2);
699 for (unsigned i = 0; i < 200; ++i) {
700 set_random(*t1, 2*num_bits/3);
701 set_random(*t2, 2*num_bits/3);
702 apply_filter_neg(*t1,*t2, cols1, cols2);
703 }
704 t1->deallocate();
705 t2->deallocate();
706 }
707
test_filter_neg2()708 void test_filter_neg2() {
709 // filter_by_negation
710 relation_signature sig4;
711 sig4.push_back(bv.mk_sort(1));
712 sig4.push_back(bv.mk_sort(1));
713 sig4.push_back(bv.mk_sort(1));
714 unsigned_vector cols, allcols;
715
716 cols.push_back(0);
717 cols.push_back(2);
718 allcols.push_back(0);
719 allcols.push_back(1);
720 allcols.push_back(2);
721
722 /// xxx \ 1x0
723 udoc_relation* t1 = mk_full(sig4);
724 {
725 udoc_relation* neg = mk_full(sig4);
726 doc& n = neg->get_udoc()[0];
727 neg->get_dm().set(n, 0, BIT_1);
728 neg->get_dm().set(n, 2, BIT_0);
729 apply_filter_neg(*t1, *neg, allcols, allcols);
730 neg->deallocate();
731 }
732
733 /// xxx \ (1x1 u 0x0)
734 udoc_relation* t2 = mk_full(sig4);
735 {
736 udoc_relation* neg = mk_full(sig4);
737 doc& n = neg->get_udoc()[0];
738 neg->get_dm().set(n, 0, BIT_0);
739 neg->get_dm().set(n, 2, BIT_0);
740 apply_filter_neg(*t2, *neg, allcols, allcols);
741 neg->deallocate();
742 }
743 {
744 udoc_relation* neg = mk_full(sig4);
745 doc& n = neg->get_udoc()[0];
746 neg->get_dm().set(n, 0, BIT_1);
747 neg->get_dm().set(n, 2, BIT_1);
748 apply_filter_neg(*t2, *neg, allcols, allcols);
749 neg->deallocate();
750 }
751 t1->display(std::cout);
752 t2->display(std::cout);
753
754 apply_filter_neg(*t2, *t1, cols, cols);
755 t1->deallocate();
756 t2->deallocate();
757 }
758
test_filter_neg3()759 void test_filter_neg3() {
760 // filter_by_negation
761 relation_signature sig;
762 sig.push_back(bv.mk_sort(1));
763 sig.push_back(bv.mk_sort(1));
764 sig.push_back(bv.mk_sort(1));
765 unsigned_vector cols1, cols2;
766
767 cols1.push_back(0);
768 cols1.push_back(0);
769 cols2.push_back(0);
770 cols2.push_back(1);
771
772 /// 1xx
773 udoc_relation* t1 = mk_full(sig);
774 {
775 doc& d = t1->get_udoc()[0];
776 t1->get_dm().set(d, 0, BIT_1);
777 }
778
779 /// 10x
780 udoc_relation* t2 = mk_full(sig);
781 {
782 doc& d = t2->get_udoc()[0];
783 t1->get_dm().set(d, 0, BIT_1);
784 t1->get_dm().set(d, 1, BIT_0);
785 }
786
787 apply_filter_neg(*t1, *t2, cols1, cols2);
788 t1->deallocate();
789 t2->deallocate();
790 }
791
test_filter_neg4(bool disable_fast)792 void test_filter_neg4(bool disable_fast) {
793 relation_signature sig1, sig2;
794 sig1.push_back(bv.mk_sort(2));
795 sig1.push_back(bv.mk_sort(2));
796 sig2.push_back(bv.mk_sort(2));
797 unsigned_vector cols1, cols2;
798
799 cols1.push_back(0);
800 cols1.push_back(1);
801 cols2.push_back(0);
802 cols2.push_back(0);
803 udoc_relation* tgt = mk_full(sig1);
804 udoc_relation* neg = mk_full(sig2);
805 if (disable_fast) p.disable_fast_pass();
806 apply_filter_neg(*tgt, *neg, cols1, cols2);
807 tgt->deallocate();
808
809 tgt = mk_full(sig1);
810 apply_filter_neg(*neg, *tgt, cols2, cols1);
811 tgt->deallocate();
812 neg->deallocate();
813 }
814
test_filter_neg5(bool disable_fast)815 void test_filter_neg5(bool disable_fast) {
816 relation_signature sig1, sig2;
817 sig1.push_back(bv.mk_sort(2));
818 sig1.push_back(bv.mk_sort(2));
819 sig2.push_back(bv.mk_sort(2));
820 sig2.push_back(bv.mk_sort(2));
821 sig2.push_back(bv.mk_sort(2));
822 unsigned_vector cols1, cols2, cols3;
823
824 cols1.push_back(0);
825 cols1.push_back(1);
826 cols2.push_back(0);
827 cols2.push_back(2);
828 cols3.push_back(0);
829 cols3.push_back(1);
830 udoc_relation* tgt = mk_full(sig1);
831 udoc_relation* neg = mk_full(sig2);
832 rel_mut filter_id = p.mk_filter_identical_fn(*tgt, cols3.size(), cols3.data());
833 (*filter_id)(*tgt);
834 if (disable_fast) p.disable_fast_pass();
835 apply_filter_neg(*tgt, *neg, cols1, cols2);
836 tgt->deallocate();
837 neg->deallocate();
838 }
839
set_random(udoc_relation & r,unsigned num_vals)840 void set_random(udoc_relation& r, unsigned num_vals) {
841 unsigned num_bits = r.get_dm().num_tbits();
842 udoc_relation* full = mk_full(r.get_signature());
843 rel_union union_fn = p.mk_union_fn(r, r, nullptr);
844 (*union_fn)(r, *full);
845 doc_manager& dm = r.get_dm();
846 ENSURE(r.get_udoc().size() == 1);
847 doc& d0 = r.get_udoc()[0];
848 ENSURE(dm.is_full(d0));
849 for (unsigned i = 0; i < num_vals; ++i) {
850 unsigned idx = m_rand(num_bits);
851 unsigned val = m_rand(2);
852 tbit b = (val == 0)?BIT_0:BIT_1;
853 dm.set(d0, idx, b);
854 }
855 full->deallocate();
856 }
857
apply_filter_neg(udoc_relation & dst,udoc_relation & neg,unsigned_vector const & cols1,unsigned_vector const & cols2)858 void apply_filter_neg(udoc_relation& dst, udoc_relation& neg,
859 unsigned_vector const& cols1, unsigned_vector const& cols2) {
860
861 scoped_ptr<datalog::relation_intersection_filter_fn> negf;
862 negf = p.mk_filter_by_negation_fn(dst, neg, cols1.size(), cols1.data(), cols2.data());
863 expr_ref dst0(m);
864 dst.to_formula(dst0);
865 (*negf)(dst, neg);
866 cr.verify_filter_by_negation(dst0, dst, neg, cols1, cols2);
867
868 /*
869
870 tgt_1:={ x: x\in tgt_0 && ! \exists y:
871 ( y \in neg & pi_c1(x)= pi_d1(y) & ... & pi_cN(x)= pi_dN(y) ) }
872 */
873 }
874
ex(unsigned hi,unsigned lo,expr * e)875 expr_ref ex(unsigned hi, unsigned lo, expr* e) {
876 expr_ref result(m);
877 result = bv.mk_extract(hi, lo, e);
878 return result;
879 }
880
apply_filter_project(udoc_relation & t,unsigned_vector const & rm,app * cond)881 void apply_filter_project(udoc_relation& t, unsigned_vector const& rm, app* cond) {
882 scoped_ptr<datalog::relation_transformer_fn> rt;
883 rt = p.mk_filter_interpreted_and_project_fn(t, cond, rm.size(), rm.data());
884 datalog::relation_base* result = (*rt)(t);
885 cr.verify_filter_project(t, *result, cond, rm);
886 result->deallocate();
887 }
888
project_var(unsigned i,sort * s,expr_ref & fml)889 void project_var(unsigned i, sort* s, expr_ref& fml) {
890 var_ref v(m);
891 v = m.mk_var(i, s);
892 unsigned num_bits = bv.get_bv_size(s);
893 unsigned p = 1 << num_bits;
894 expr_ref_vector disj(m);
895 expr_ref tmp(m);
896 for (unsigned i = 0; i < p; ++i) {
897 expr_safe_replace repl(m);
898 repl.insert(v, bv.mk_numeral(rational(i), s));
899 tmp = fml;
900 repl(tmp);
901 disj.push_back(tmp);
902 }
903 fml = mk_or(m, disj.size(), disj.data());
904 }
905
apply_filter(udoc_relation & t,app * cond)906 void apply_filter(udoc_relation& t, app* cond) {
907 udoc_relation* full = mk_full(t.get_signature());
908 rel_union union_fn = p.mk_union_fn(t, *full, nullptr);
909 (*union_fn)(t, *full, nullptr);
910 expr_ref fml0(m);
911 t.to_formula(fml0);
912 rel_mut fint = p.mk_filter_interpreted_fn(t, cond);
913 (*fint)(t);
914 t.display(std::cout << "filter: " << mk_pp(cond, m) << " "); std::cout << "\n";
915 cr.verify_filter(fml0, t, cond);
916 full->deallocate();
917 }
918
919
920 };
921
tst_udoc_relation()922 void tst_udoc_relation() {
923 udoc_tester tester;
924
925 try {
926 tester.test1();
927 }
928 catch (z3_exception& ex) {
929 std::cout << ex.msg() << "\n";
930 }
931 }
932