1
2 /*++
3 Copyright (c) 2015 Microsoft Corporation
4
5 --*/
6
7 #ifdef _WINDOWS
8
9 #include "ast/reg_decl_plugins.h"
10 #include "muz/base/dl_context.h"
11 #include "muz/fp/dl_register_engine.h"
12 #include "muz/rel/dl_relation_manager.h"
13 #include "muz/rel/dl_interval_relation.h"
14 #include "muz/rel/dl_bound_relation.h"
15 #include "muz/rel/dl_product_relation.h"
16 #include "util/util.h"
17
18 namespace datalog {
19
test_interval_relation()20 static void test_interval_relation() {
21 smt_params params;
22 ast_manager ast_m;
23 reg_decl_plugins(ast_m);
24 register_engine re;
25 context ctx(ast_m, re, params);
26 arith_util autil(ast_m);
27 relation_manager & m = ctx.get_rel_context()->get_rmanager();
28 m.register_plugin(alloc(interval_relation_plugin, m));
29 interval_relation_plugin& ip = dynamic_cast<interval_relation_plugin&>(*m.get_relation_plugin(symbol("interval_relation")));
30 ENSURE(&ip);
31
32 relation_signature sig;
33 sort* int_sort = autil.mk_int();
34 sig.push_back(int_sort);
35 sig.push_back(int_sort);
36 sig.push_back(int_sort);
37 sig.push_back(int_sort);
38
39 interval_relation& i1 = dynamic_cast<interval_relation&>(*ip.mk_empty(sig));
40 interval_relation& i2 = dynamic_cast<interval_relation&>(*ip.mk_full(0, sig));
41
42 i1.display(std::cout);
43 i2.display(std::cout);
44 ENSURE(i1.empty());
45 ENSURE(!i2.empty());
46
47 app_ref cond1(ast_m), cond2(ast_m), cond3(ast_m);
48 app_ref cond4(ast_m), cond5(ast_m), cond6(ast_m);
49 app_ref num1(ast_m);
50 cond1 = autil.mk_le(ast_m.mk_var(0, int_sort), autil.mk_numeral(rational(0), true));
51 cond2 = autil.mk_le(ast_m.mk_var(1, int_sort), autil.mk_numeral(rational(1), true));
52 cond3 = autil.mk_le(ast_m.mk_var(2, int_sort), autil.mk_numeral(rational(2), true));
53 cond4 = autil.mk_ge(ast_m.mk_var(0, int_sort), autil.mk_numeral(rational(0), true));
54 cond5 = autil.mk_ge(ast_m.mk_var(1, int_sort), autil.mk_numeral(rational(0), true));
55 cond6 = autil.mk_ge(ast_m.mk_var(2, int_sort), autil.mk_numeral(rational(5), true));
56 num1 = autil.mk_numeral(rational(4), true);
57 i2.filter_interpreted(cond1);
58 i2.display(std::cout);
59 // x0 <= 0
60
61 unsigned cols1[2] = { 1, 2};
62 unsigned cols2[2] = { 2, 3};
63 relation_join_fn* join1 = ip.mk_join_fn(i1, i2, 2, cols1, cols2);
64 relation_transformer_fn* proj1 = ip.mk_project_fn(i1, 2, cols2);
65 relation_transformer_fn* ren1 = ip.mk_rename_fn(i1, 2, cols2);
66 relation_union_fn* union1 = ip.mk_union_fn(i1, i2, &i1);
67 relation_mutator_fn* filterId1 = ip.mk_filter_identical_fn(i1, 2, cols1);
68 relation_mutator_fn* filterEq1 = ip.mk_filter_equal_fn(i1, num1, 2);
69 relation_mutator_fn* filterCond1 = ip.mk_filter_interpreted_fn(i1, cond2);
70
71 relation_base* i3 = (*join1)(i2, i2);
72 i3->display(std::cout);
73
74 relation_transformer_fn* proj2 = ip.mk_project_fn(*i3, 2, cols2);
75
76 (*filterEq1)(i2);
77 i2.display(std::cout);
78 // x0 <= 0
79 // x2 = 4
80
81 (*filterId1)(i2);
82 i2.display(std::cout);
83 // x0 <= 0
84 // x1 = x2 = 4
85 relation_fact fact1(ast_m);
86 fact1.push_back(autil.mk_numeral(rational(0), true));
87 fact1.push_back(autil.mk_numeral(rational(4), true));
88 fact1.push_back(autil.mk_numeral(rational(4), true));
89 fact1.push_back(autil.mk_numeral(rational(5), true));
90 ENSURE(i2.contains_fact(fact1));
91 fact1[0] = autil.mk_numeral(rational(-1), true);
92 ENSURE(i2.contains_fact(fact1));
93 fact1[0] = autil.mk_numeral(rational(1), true);
94 ENSURE(!i2.contains_fact(fact1));
95
96 relation_base* i5 = (*ren1)(i2);
97 i2.display(std::cout << "Orig\n");
98 i5->display(std::cout << "renamed 2 |-> 3 |-> 2\n");
99
100 (*filterCond1)(i2);
101 i2.display(std::cout);
102 // empty
103 ENSURE(i2.empty());
104
105 relation_base* i4 = (*proj2)(*i3);
106 i4->display(std::cout);
107
108 i1.deallocate();
109 i2.deallocate();
110 i3->deallocate();
111 i4->deallocate();
112 i5->deallocate();
113 dealloc(join1);
114 dealloc(proj1);
115 dealloc(ren1);
116 dealloc(union1);
117 dealloc(filterId1);
118 dealloc(filterEq1);
119 dealloc(filterCond1);
120 }
121
test_bound_relation()122 static void test_bound_relation() {
123
124 std::cout << "bound relation\n";
125
126 smt_params params;
127 ast_manager ast_m;
128 reg_decl_plugins(ast_m);
129 register_engine re;
130 context ctx(ast_m, re, params);
131 arith_util autil(ast_m);
132 relation_manager & m = ctx.get_rel_context()->get_rmanager();
133 m.register_plugin(alloc(bound_relation_plugin, m));
134 bound_relation_plugin& br = dynamic_cast<bound_relation_plugin&>(*m.get_relation_plugin(symbol("bound_relation")));
135 ENSURE(&br);
136
137 relation_signature sig;
138 sort* int_sort = autil.mk_int();
139 sig.push_back(int_sort);
140 sig.push_back(int_sort);
141 sig.push_back(int_sort);
142 sig.push_back(int_sort);
143
144 bound_relation& i1 = dynamic_cast<bound_relation&>(*br.mk_empty(sig));
145 bound_relation& i2 = dynamic_cast<bound_relation&>(*br.mk_full(0, sig));
146
147 i1.display(std::cout << "empty:\n");
148 i2.display(std::cout << "full:\n");
149 ENSURE(i1.empty());
150 ENSURE(!i2.empty());
151
152 app_ref cond1(ast_m), cond2(ast_m), cond3(ast_m);
153 app_ref cond4(ast_m), cond5(ast_m), cond6(ast_m);
154 app_ref num1(ast_m);
155 cond1 = autil.mk_lt(ast_m.mk_var(0, int_sort), autil.mk_numeral(rational(0), true));
156 cond2 = autil.mk_lt(ast_m.mk_var(1, int_sort), autil.mk_numeral(rational(1), true));
157 cond3 = autil.mk_lt(ast_m.mk_var(2, int_sort), ast_m.mk_var(3, int_sort));
158 cond4 = autil.mk_ge(ast_m.mk_var(0, int_sort), autil.mk_numeral(rational(0), true));
159 cond5 = autil.mk_ge(ast_m.mk_var(1, int_sort), autil.mk_numeral(rational(0), true));
160 cond6 = autil.mk_ge(ast_m.mk_var(2, int_sort), autil.mk_numeral(rational(5), true));
161
162 app_ref lt_x0x1(ast_m), lt_x1x2(ast_m), lt_x0x3(ast_m), lt_x0x2(ast_m);
163 lt_x0x1 = autil.mk_lt(ast_m.mk_var(0, int_sort), ast_m.mk_var(1, int_sort));
164 lt_x1x2 = autil.mk_lt(ast_m.mk_var(1, int_sort), ast_m.mk_var(2, int_sort));
165 lt_x0x2 = autil.mk_lt(ast_m.mk_var(0, int_sort), ast_m.mk_var(2, int_sort));
166 lt_x0x3 = autil.mk_lt(ast_m.mk_var(0, int_sort), ast_m.mk_var(3, int_sort));
167
168 num1 = autil.mk_numeral(rational(4), true);
169
170 unsigned cols1[2] = { 1, 2};
171 unsigned cols2[2] = { 2, 3};
172 unsigned cols3[3] = { 0, 2, 3 };
173 relation_join_fn* join1 = br.mk_join_fn(i1, i2, 2, cols1, cols2);
174 relation_transformer_fn* proj1 = br.mk_project_fn(i1, 2, cols2);
175 relation_transformer_fn* ren1 = br.mk_rename_fn(i1, 3, cols3);
176 relation_union_fn* union1 = br.mk_union_fn(i1, i2, &i1);
177 relation_mutator_fn* filterId1 = br.mk_filter_identical_fn(i1, 2, cols1);
178 relation_mutator_fn* filterEq1 = br.mk_filter_equal_fn(i1, num1, 2);
179 relation_mutator_fn* filterCond1 = br.mk_filter_interpreted_fn(i1, cond3);
180
181 relation_base* i3 = (*join1)(i2, i2);
182 i3->display(std::cout);
183
184 relation_transformer_fn* proj2 = br.mk_project_fn(*i3, 2, cols2);
185
186 (*filterEq1)(i2);
187 i2.display(std::cout << "no-op still full\n");
188 // no-op
189
190 (*filterCond1)(i2);
191 i2.display(std::cout << "x2 < x3\n");
192 // x2 < x3
193
194 (*filterId1)(i2);
195 i2.display(std::cout << "id\n");
196 // x1 = x2 < x3
197 relation_fact fact1(ast_m);
198
199 i2.display(std::cout << "Orig\n");
200 std::cout << "renamed ";
201 for (unsigned i = 0; i < 3; ++i) {
202 std::cout << cols3[i] << " ";
203 }
204 std::cout << "\n";
205 relation_base* i5 = (*ren1)(i2);
206 i5->display(std::cout);
207
208 //ENSURE(i2.empty());
209
210 relation_base* i4 = (*proj2)(*i3);
211 i4->display(std::cout);
212
213 // test that equivalence classes are expanded.
214 // { x1 = x3, x0 < x1 x1 < x2} u { x2 = x3, x0 < x3 } = { x0 < x3 }
215 {
216 relation_base* b1 = br.mk_full(0, sig);
217 relation_base* b2 = br.mk_full(0, sig);
218 unsigned x1x3[2] = { 1, 3 };
219 unsigned x2x3[2] = { 2, 3 };
220 scoped_ptr<relation_mutator_fn> id1 = br.mk_filter_identical_fn(*b1, 2, x1x3);
221 scoped_ptr<relation_mutator_fn> ltx0x1 = br.mk_filter_interpreted_fn(*b1, lt_x0x1);
222 scoped_ptr<relation_mutator_fn> ltx1x2 = br.mk_filter_interpreted_fn(*b1, lt_x1x2);
223 scoped_ptr<relation_mutator_fn> ltx0x3 = br.mk_filter_interpreted_fn(*b2, lt_x0x3);
224 scoped_ptr<relation_mutator_fn> id2 = br.mk_filter_identical_fn(*b2, 2, x2x3);
225 (*id1)(*b1);
226 (*ltx0x1)(*b1);
227 (*ltx1x2)(*b1);
228 b2->display(std::cout << "b2:\n");
229 (*id2)(*b2);
230 b2->display(std::cout << "b2:\n");
231 (*ltx0x3)(*b2);
232 b2->display(std::cout << "b2:\n");
233 scoped_ptr<relation_union_fn> u = br.mk_union_fn(*b1, *b2, 0);
234 b1->display(std::cout << "b1:\n");
235 b2->display(std::cout << "b2:\n");
236 (*u)(*b1, *b2, 0);
237
238 b1->display(std::cout << "b1 u b2:\n");
239
240 // TBD check property;
241
242 b1->deallocate();
243 b2->deallocate();
244 }
245
246 // test that equivalence classes are expanded.
247 // { x1 = x2 = x3, x0 < x1} u { x1 = x3, x0 < x3, x0 < x2 } = { x0 < x2, x0 < x3 }
248 {
249 relation_base* b1 = br.mk_full(0, sig);
250 relation_base* b2 = br.mk_full(0, sig);
251 unsigned x0x3[2] = { 0, 3 };
252 unsigned x1x3[2] = { 1, 3 };
253 unsigned x2x3[2] = { 2, 3 };
254 scoped_ptr<relation_mutator_fn> id1 = br.mk_filter_identical_fn(*b1, 2, x1x3);
255 scoped_ptr<relation_mutator_fn> id2 = br.mk_filter_identical_fn(*b1, 2, x2x3);
256 scoped_ptr<relation_mutator_fn> ltx0x1 = br.mk_filter_interpreted_fn(*b1, lt_x0x1);
257 scoped_ptr<relation_mutator_fn> ltx0x2 = br.mk_filter_interpreted_fn(*b2, lt_x0x2);
258 scoped_ptr<relation_mutator_fn> ltx0x3 = br.mk_filter_interpreted_fn(*b2, lt_x0x3);
259 scoped_ptr<relation_mutator_fn> id3 = br.mk_filter_identical_fn(*b2, 2, x1x3);
260 (*id1)(*b1);
261 (*id2)(*b1);
262 (*ltx0x1)(*b1);
263 (*id3)(*b2);
264 (*ltx0x2)(*b2);
265 (*ltx0x3)(*b2);
266 scoped_ptr<relation_union_fn> u = br.mk_union_fn(*b1, *b2, 0);
267 b1->display(std::cout << "b1:\n");
268 b2->display(std::cout << "b2:\n");
269 (*u)(*b1, *b2, 0);
270 b1->display(std::cout << "b1 u b2:\n");
271
272 // TBD check property;
273
274 b1->deallocate();
275 b2->deallocate();
276 }
277
278 i1.deallocate();
279 i2.deallocate();
280 i3->deallocate();
281 i4->deallocate();
282 i5->deallocate();
283 dealloc(join1);
284 dealloc(proj1);
285 dealloc(ren1);
286 dealloc(union1);
287 dealloc(filterId1);
288 dealloc(filterEq1);
289 dealloc(filterCond1);
290 }
291
292 }
293
tst_dl_relation()294 void tst_dl_relation() {
295 datalog::test_interval_relation();
296 datalog::test_bound_relation();
297 }
298
299 #else
tst_dl_relation()300 void tst_dl_relation() {
301 }
302 #endif
303