1 /*++ 2 Copyright (c) 2014 Microsoft Corporation 3 4 Module Name: 5 6 udoc_relation.cpp 7 8 Abstract: 9 10 Relation based on union of DOCs. 11 12 Author: 13 14 Nuno Lopes (a-nlopes) 2013-03-01 15 Nikolaj Bjorner (nbjorner) 2014-09-15 16 17 Revision History: 18 19 Revised version of dl_hassel_diff facilities. 20 21 Notes: 22 23 --*/ 24 #include "muz/rel/udoc_relation.h" 25 #include "muz/rel/dl_relation_manager.h" 26 #include "ast/ast_util.h" 27 #include "smt/smt_kernel.h" 28 29 30 namespace datalog { 31 udoc_relation(udoc_plugin & p,relation_signature const & sig)32 udoc_relation::udoc_relation(udoc_plugin& p, relation_signature const& sig): 33 relation_base(p, sig), 34 dm(p.dm(p.num_signature_bits(sig))) { 35 unsigned column = 0; 36 for (unsigned i = 0; i < sig.size(); ++i) { 37 m_column_info.push_back(column); 38 column += p.num_sort_bits(sig[i]); 39 } 40 m_column_info.push_back(column); 41 } ~udoc_relation()42 udoc_relation::~udoc_relation() { 43 reset(); 44 } reset()45 void udoc_relation::reset() { 46 m_elems.reset(dm); 47 } expand_column_vector(unsigned_vector & v,const udoc_relation * other) const48 void udoc_relation::expand_column_vector(unsigned_vector& v, const udoc_relation* other) const { 49 unsigned_vector orig; 50 orig.swap(v); 51 for (unsigned i = 0; i < orig.size(); ++i) { 52 unsigned col, limit; 53 if (orig[i] < get_num_cols()) { 54 col = column_idx(orig[i]); 55 limit = col + column_num_bits(orig[i]); 56 } else { 57 unsigned idx = orig[i] - get_num_cols(); 58 col = get_num_bits() + other->column_idx(idx); 59 limit = col + other->column_num_bits(idx); 60 } 61 for (; col < limit; ++col) { 62 v.push_back(col); 63 } 64 } 65 } 66 fact2doc(const relation_fact & f) const67 doc* udoc_relation::fact2doc(const relation_fact & f) const { 68 doc* d = dm.allocate0(); 69 for (unsigned i = 0; i < f.size(); ++i) { 70 unsigned bv_size; 71 rational val; 72 VERIFY(get_plugin().is_numeral(f[i], val, bv_size)); 73 SASSERT(bv_size == column_num_bits(i)); 74 unsigned lo = column_idx(i); 75 unsigned hi = column_idx(i + 1); 76 dm.tbvm().set(d->pos(),val, hi-1, lo); 77 } 78 return d; 79 } add_fact(const relation_fact & f)80 void udoc_relation::add_fact(const relation_fact & f) { 81 doc* d = fact2doc(f); 82 m_elems.insert(dm, d); 83 } add_new_fact(const relation_fact & f)84 void udoc_relation::add_new_fact(const relation_fact & f) { 85 m_elems.push_back(fact2doc(f)); 86 } empty() const87 bool udoc_relation::empty() const { 88 return m_elems.is_empty_complete(get_plugin().m, dm); 89 } contains_fact(const relation_fact & f) const90 bool udoc_relation::contains_fact(const relation_fact & f) const { 91 doc_ref d(dm, fact2doc(f)); 92 return m_elems.contains(dm, *d); 93 } clone() const94 udoc_relation * udoc_relation::clone() const { 95 udoc_relation* result = udoc_plugin::get(get_plugin().mk_empty(get_signature())); 96 for (unsigned i = 0; i < m_elems.size(); ++i) { 97 result->m_elems.push_back(dm.allocate(m_elems[i])); 98 } 99 return result; 100 } complement(func_decl * f) const101 udoc_relation * udoc_relation::complement(func_decl* f) const { 102 udoc_relation* result = udoc_plugin::get(get_plugin().mk_empty(get_signature())); 103 m_elems.complement(dm, result->m_elems); 104 return result; 105 } to_formula(expr_ref & fml) const106 void udoc_relation::to_formula(expr_ref& fml) const { 107 ast_manager& m = fml.get_manager(); 108 expr_ref_vector disj(m); 109 for (unsigned i = 0; i < m_elems.size(); ++i) { 110 disj.push_back(to_formula(m_elems[i])); 111 } 112 fml = mk_or(m, disj.size(), disj.data()); 113 } to_formula(doc const & d) const114 expr_ref udoc_relation::to_formula(doc const& d) const { 115 ast_manager& m = get_plugin().get_ast_manager(); 116 expr_ref result(m); 117 expr_ref_vector conjs(m); 118 conjs.push_back(to_formula(d.pos())); 119 for (unsigned i = 0; i < d.neg().size(); ++i) { 120 conjs.push_back(m.mk_not(to_formula(d.neg()[i]))); 121 } 122 result = mk_and(m, conjs.size(), conjs.data()); 123 return result; 124 } to_formula(tbv const & t) const125 expr_ref udoc_relation::to_formula(tbv const& t) const { 126 udoc_plugin& p = get_plugin(); 127 ast_manager& m = p.get_ast_manager(); 128 expr_ref result(m); 129 expr_ref_vector conjs(m); 130 for (unsigned i = 0; i < get_num_cols(); ++i) { 131 var_ref v(m); 132 v = m.mk_var(i, get_signature()[i]); 133 unsigned lo = column_idx(i); 134 unsigned hi = column_idx(i+1); 135 rational r(0); 136 unsigned lo1 = lo; 137 bool is_x = true; 138 for (unsigned j = lo; j < hi; ++j) { 139 switch(t[j]) { 140 case BIT_0: 141 if (is_x) is_x = false, lo1 = j, r.reset(); 142 break; 143 case BIT_1: 144 if (is_x) is_x = false, lo1 = j, r.reset(); 145 r += rational::power_of_two(j - lo1); 146 break; 147 case BIT_x: 148 if (!is_x) { 149 SASSERT(p.bv.is_bv_sort(get_signature()[i])); 150 conjs.push_back(m.mk_eq(p.bv.mk_extract(j-1-lo,lo1-lo,v), 151 p.bv.mk_numeral(r,j-lo1))); 152 } 153 is_x = true; 154 break; 155 default: 156 UNREACHABLE(); 157 } 158 } 159 if (!is_x) { 160 expr_ref num(m); 161 if (lo1 == lo) { 162 num = p.mk_numeral(r, get_signature()[i]); 163 conjs.push_back(m.mk_eq(v, num)); 164 } 165 else { 166 num = p.bv.mk_numeral(r, hi-lo1); 167 conjs.push_back(m.mk_eq(p.bv.mk_extract(hi-1-lo,lo1-lo,v), num)); 168 } 169 } 170 } 171 result = mk_and(m, conjs.size(), conjs.data()); 172 return result; 173 } 174 get_plugin() const175 udoc_plugin& udoc_relation::get_plugin() const { 176 return static_cast<udoc_plugin&>(relation_base::get_plugin()); 177 } 178 display(std::ostream & out) const179 void udoc_relation::display(std::ostream& out) const { 180 m_elems.display(dm, out); out << "\n"; 181 } 182 get_size_estimate_bytes() const183 unsigned udoc_relation::get_size_estimate_bytes() const { 184 return sizeof(*this) + m_elems.get_size_estimate_bytes(dm); 185 } 186 187 // ------------- 188 udoc_plugin(relation_manager & rm)189 udoc_plugin::udoc_plugin(relation_manager& rm): 190 relation_plugin(udoc_plugin::get_name(), rm), 191 m(rm.get_context().get_manager()), 192 bv(m), 193 dl(m), 194 m_disable_fast_pass(false) { 195 } ~udoc_plugin()196 udoc_plugin::~udoc_plugin() { 197 u_map<doc_manager*>::iterator it = m_dms.begin(), end = m_dms.end(); 198 for (; it != end; ++it) { 199 dealloc(it->m_value); 200 } 201 } get(relation_base & r)202 udoc_relation& udoc_plugin::get(relation_base& r) { 203 return dynamic_cast<udoc_relation&>(r); 204 } get(relation_base * r)205 udoc_relation* udoc_plugin::get(relation_base* r) { 206 return r?dynamic_cast<udoc_relation*>(r):nullptr; 207 } get(relation_base const & r)208 udoc_relation const & udoc_plugin::get(relation_base const& r) { 209 return dynamic_cast<udoc_relation const&>(r); 210 } 211 dm(relation_signature const & sig)212 doc_manager& udoc_plugin::dm(relation_signature const& sig) { 213 return dm(num_signature_bits(sig)); 214 } 215 dm(unsigned n)216 doc_manager& udoc_plugin::dm(unsigned n) { 217 doc_manager* r; 218 if (!m_dms.find(n, r)) { 219 r = alloc(doc_manager, n); 220 m_dms.insert(n, r); 221 } 222 return *r; 223 } is_var_range(expr * e,unsigned & hi,unsigned & lo,unsigned & v) const224 bool udoc_relation::is_var_range(expr* e, unsigned& hi, unsigned& lo, unsigned& v) const { 225 udoc_plugin& p = get_plugin(); 226 if (is_var(e)) { 227 v = to_var(e)->get_idx(); 228 hi = p.num_sort_bits(e)-1; 229 lo = 0; 230 return true; 231 } 232 expr* e2; 233 if (p.bv.is_extract(e, lo, hi, e2) && is_var(e2)) { 234 v = to_var(e2)->get_idx(); 235 SASSERT(lo <= hi); 236 return true; 237 } 238 return false; 239 } 240 mk_numeral(rational const & r,sort * s)241 expr* udoc_plugin::mk_numeral(rational const& r, sort* s) { 242 if (bv.is_bv_sort(s)) { 243 return bv.mk_numeral(r, s); 244 } 245 if (m.is_bool(s)) { 246 if (r.is_zero()) return m.mk_false(); 247 return m.mk_true(); 248 } 249 SASSERT(dl.is_finite_sort(s)); 250 return dl.mk_numeral(r.get_uint64(), s); 251 } is_numeral(expr * e,rational & r,unsigned & num_bits)252 bool udoc_plugin::is_numeral(expr* e, rational& r, unsigned& num_bits) { 253 if (bv.is_numeral(e, r, num_bits)) return true; 254 if (m.is_true(e)) { 255 r = rational(1); 256 num_bits = 1; 257 return true; 258 } 259 if (m.is_false(e)) { 260 r = rational(0); 261 num_bits = 1; 262 return true; 263 } 264 uint64_t n, sz; 265 if (dl.is_numeral(e, n) && dl.try_get_size(e->get_sort(), sz)) { 266 num_bits = 0; 267 while (sz > 0) ++num_bits, sz = sz/2; 268 r = rational(n, rational::ui64()); 269 return true; 270 } 271 return false; 272 } num_sort_bits(sort * s) const273 unsigned udoc_plugin::num_sort_bits(sort* s) const { 274 unsigned num_bits = 0; 275 if (bv.is_bv_sort(s)) 276 return bv.get_bv_size(s); 277 if (m.is_bool(s)) 278 return 1; 279 uint64_t sz; 280 if (dl.try_get_size(s, sz)) { 281 while (sz > 0) ++num_bits, sz /= 2; 282 return num_bits; 283 } 284 UNREACHABLE(); 285 return 0; 286 } num_signature_bits(relation_signature const & sig)287 unsigned udoc_plugin::num_signature_bits(relation_signature const& sig) { 288 unsigned result = 0; 289 for (unsigned i = 0; i < sig.size(); ++i) { 290 result += num_sort_bits(sig[i]); 291 } 292 return result; 293 } 294 is_finite_sort(sort * s) const295 bool udoc_plugin::is_finite_sort(sort* s) const { 296 return bv.is_bv_sort(s) || dl.is_finite_sort(s); 297 } 298 299 can_handle_signature(const relation_signature & sig)300 bool udoc_plugin::can_handle_signature(const relation_signature & sig) { 301 for (unsigned i = 0; i < sig.size(); ++i) { 302 if (!is_finite_sort(sig[i])) 303 return false; 304 } 305 return true; 306 } mk_empty(const relation_signature & sig)307 relation_base * udoc_plugin::mk_empty(const relation_signature & sig) { 308 return alloc(udoc_relation, *this, sig); 309 } mk_full(func_decl * p,const relation_signature & s)310 relation_base * udoc_plugin::mk_full(func_decl* p, const relation_signature & s) { 311 udoc_relation* r = get(mk_empty(s)); 312 r->get_udoc().push_back(dm(s).allocateX()); 313 return r; 314 } 315 class udoc_plugin::join_fn : public convenient_relation_join_fn { 316 doc_manager& dm; 317 doc_manager& dm1; 318 doc_manager& dm2; 319 public: join_fn(udoc_plugin & p,udoc_relation const & t1,udoc_relation const & t2,unsigned col_cnt,const unsigned * cols1,const unsigned * cols2)320 join_fn(udoc_plugin& p, udoc_relation const& t1, udoc_relation const& t2, unsigned col_cnt, 321 const unsigned * cols1, const unsigned * cols2) 322 : convenient_relation_join_fn(t1.get_signature(), t2.get_signature(), col_cnt, cols1, cols2), 323 dm(p.dm(get_result_signature())), 324 dm1(t1.get_dm()), 325 dm2(t2.get_dm()) { 326 t1.expand_column_vector(m_cols1); 327 t2.expand_column_vector(m_cols2); 328 } 329 operator ()(const relation_base & _r1,const relation_base & _r2)330 relation_base * operator()(const relation_base & _r1, const relation_base & _r2) override { 331 udoc_relation const& r1 = get(_r1); 332 udoc_relation const& r2 = get(_r2); 333 TRACE("doc", r1.display(tout << "r1:\n"); r2.display(tout << "r2:\n");); 334 udoc_plugin& p = r1.get_plugin(); 335 relation_signature const& sig = get_result_signature(); 336 udoc_relation * result = alloc(udoc_relation, p, sig); 337 udoc const& d1 = r1.get_udoc(); 338 udoc const& d2 = r2.get_udoc(); 339 udoc& r = result->get_udoc(); 340 r.join(d1, d2, dm, dm1, m_cols1, m_cols2); 341 TRACE("doc", result->display(tout << "result:\n");); 342 IF_VERBOSE(3, result->display(verbose_stream() << "join result:\n");); 343 SASSERT(r.well_formed(result->get_dm())); 344 return result; 345 } 346 }; 347 348 mk_join_fn(const relation_base & t1,const relation_base & t2,unsigned col_cnt,const unsigned * cols1,const unsigned * cols2)349 relation_join_fn * udoc_plugin::mk_join_fn( 350 const relation_base & t1, const relation_base & t2, 351 unsigned col_cnt, const unsigned * cols1, const unsigned * cols2) { 352 if (!check_kind(t1) || !check_kind(t2)) { 353 return nullptr; 354 } 355 return alloc(join_fn, *this, get(t1), get(t2), col_cnt, cols1, cols2); 356 } 357 358 class udoc_plugin::project_fn : public convenient_relation_project_fn { 359 bit_vector m_to_delete; 360 public: project_fn(udoc_relation const & t,unsigned removed_col_cnt,const unsigned * removed_cols)361 project_fn(udoc_relation const & t, unsigned removed_col_cnt, const unsigned * removed_cols) 362 : convenient_relation_project_fn(t.get_signature(), removed_col_cnt, removed_cols) { 363 t.expand_column_vector(m_removed_cols); 364 unsigned n = t.get_dm().num_tbits(); 365 m_to_delete.resize(n, false); 366 for (unsigned i = 0; i < m_removed_cols.size(); ++i) { 367 m_to_delete.set(m_removed_cols[i], true); 368 } 369 } 370 operator ()(const relation_base & tb)371 relation_base * operator()(const relation_base & tb) override { 372 TRACE("doc", tb.display(tout << "src:\n");); 373 udoc_relation const& t = get(tb); 374 udoc_plugin& p = t.get_plugin(); 375 udoc_relation* r = udoc_plugin::get(p.mk_empty(get_result_signature())); 376 doc_manager& dm1 = t.get_dm(); 377 doc_manager& dm2 = r->get_dm(); 378 doc_ref d2(dm2); 379 udoc const& ud1 = t.get_udoc(); 380 udoc& ud2 = r->get_udoc(); 381 for (unsigned i = 0; i < ud1.size(); ++i) { 382 d2 = dm1.project(dm2, m_to_delete, ud1[i]); 383 ud2.push_back(d2.detach()); 384 } 385 TRACE("doc", tout << "final size: " << r->get_size_estimate_rows() << '\n';); 386 SASSERT(ud2.well_formed(dm2)); 387 return r; 388 } 389 }; 390 391 mk_project_fn(const relation_base & t,unsigned col_cnt,const unsigned * removed_cols)392 relation_transformer_fn * udoc_plugin::mk_project_fn( 393 const relation_base & t, unsigned col_cnt, 394 const unsigned * removed_cols) { 395 if (!check_kind(t)) 396 return nullptr; 397 return alloc(project_fn, get(t), col_cnt, removed_cols); 398 } 399 400 class udoc_plugin::rename_fn : public convenient_relation_rename_fn { 401 unsigned_vector m_permutation; 402 public: rename_fn(udoc_relation const & t,unsigned cycle_len,const unsigned * cycle)403 rename_fn(udoc_relation const& t, unsigned cycle_len, const unsigned * cycle) 404 : convenient_relation_rename_fn(t.get_signature(), cycle_len, cycle) { 405 udoc_plugin& p = t.get_plugin(); 406 407 relation_signature const& sig1 = t.get_signature(); 408 relation_signature const& sig2 = get_result_signature(); 409 unsigned_vector permutation0, column_info; 410 for (unsigned i = 0; i < t.get_num_bits(); ++i) { 411 m_permutation.push_back(i); 412 } 413 for (unsigned i = 0; i < sig1.size(); ++i) { 414 permutation0.push_back(i); 415 } 416 for (unsigned i = 0; i < cycle_len; ++i) { 417 unsigned j = (i + 1)%cycle_len; 418 unsigned col1 = cycle[i]; 419 unsigned col2 = cycle[j]; 420 permutation0[col2] = col1; 421 } 422 unsigned column = 0; 423 for (unsigned i = 0; i < sig2.size(); ++i) { 424 column_info.push_back(column); 425 column += p.num_sort_bits(sig2[i]); 426 } 427 column_info.push_back(column); 428 SASSERT(column == t.get_num_bits()); 429 430 TRACE("doc", 431 ast_manager& m = p.get_ast_manager(); 432 sig1.output(m, tout << "sig1: "); tout << "\n"; 433 sig2.output(m, tout << "sig2: "); tout << "\n"; 434 tout << "permute: "; 435 for (unsigned i = 0; i < permutation0.size(); ++i) { 436 tout << permutation0[i] << " "; 437 } 438 tout << "\n"; 439 tout << "cycle: "; 440 for (unsigned i = 0; i < cycle_len; ++i) { 441 tout << cycle[i] << " "; 442 } 443 tout << "\n"; 444 ); 445 446 447 // 0 -> 2 448 // [3:2:1] -> [1:2:3] 449 // [3,4,5,1,2,0] 450 451 for (unsigned i = 0; i < sig1.size(); ++i) { 452 unsigned len = t.column_num_bits(i); 453 unsigned lo1 = t.column_idx(i); 454 unsigned col2 = permutation0[i]; 455 unsigned lo2 = column_info[col2]; 456 SASSERT(lo2 + len <= t.get_num_bits()); 457 SASSERT(lo1 + len <= t.get_num_bits()); 458 for (unsigned k = 0; k < len; ++k) { 459 m_permutation[k + lo1] = k + lo2; 460 } 461 } 462 } 463 operator ()(const relation_base & _r)464 relation_base * operator()(const relation_base & _r) override { 465 udoc_relation const& r = get(_r); 466 TRACE("doc", r.display(tout << "r:\n");); 467 udoc_plugin& p = r.get_plugin(); 468 relation_signature const& sig = get_result_signature(); 469 udoc_relation* result = alloc(udoc_relation, p, sig); 470 udoc const& src = r.get_udoc(); 471 udoc& dst = result->get_udoc(); 472 doc_manager& dm = r.get_dm(); 473 SASSERT(&result->get_dm() == &dm); 474 for (unsigned i = 0; i < src.size(); ++i) { 475 dst.push_back(dm.allocate(src[i], m_permutation.data())); 476 } 477 TRACE("doc", result->display(tout << "result:\n");); 478 SASSERT(dst.well_formed(dm)); 479 return result; 480 } 481 }; mk_rename_fn(const relation_base & r,unsigned cycle_len,const unsigned * permutation_cycle)482 relation_transformer_fn * udoc_plugin::mk_rename_fn( 483 const relation_base & r, 484 unsigned cycle_len, const unsigned * permutation_cycle) { 485 if (check_kind(r)) { 486 return alloc(rename_fn, get(r), cycle_len, permutation_cycle); 487 } 488 else { 489 return nullptr; 490 } 491 } 492 class udoc_plugin::union_fn : public relation_union_fn { 493 public: union_fn()494 union_fn() {} 495 operator ()(relation_base & _r,const relation_base & _src,relation_base * _delta)496 void operator()(relation_base & _r, const relation_base & _src, relation_base * _delta) override { 497 TRACE("doc", _r.display(tout << "dst:\n"); _src.display(tout << "src:\n");); 498 udoc_relation& r = get(_r); 499 udoc_relation const& src = get(_src); 500 udoc_relation* d = get(_delta); 501 doc_manager& dm = r.get_dm(); 502 udoc* d1 = nullptr; 503 if (d) d1 = &d->get_udoc(); 504 IF_VERBOSE(3, r.display(verbose_stream() << "orig: ");); 505 r.get_plugin().mk_union(dm, r.get_udoc(), src.get_udoc(), d1); 506 SASSERT(r.get_udoc().well_formed(dm)); 507 SASSERT(!d1 || d1->well_formed(dm)); 508 TRACE("doc", _r.display(tout << "dst':\n"); ); 509 IF_VERBOSE(3, r.display(verbose_stream() << "union: ");); 510 IF_VERBOSE(3, if (d) d->display(verbose_stream() << "delta: ");); 511 } 512 }; mk_union(doc_manager & dm,udoc & dst,udoc const & src,udoc * delta)513 void udoc_plugin::mk_union(doc_manager& dm, udoc& dst, udoc const& src, udoc* delta) { 514 bool deltaempty = delta ? delta->is_empty() : false; 515 516 if (dst.is_empty()) { 517 for (unsigned i = 0; i < src.size(); ++i) { 518 dst.push_back(dm.allocate(src[i])); 519 if (delta) { 520 if (deltaempty) 521 delta->push_back(dm.allocate(src[i])); 522 else 523 delta->insert(dm, dm.allocate(src[i])); 524 } 525 } 526 } else { 527 for (unsigned i = 0; i < src.size(); ++i) { 528 if (dst.insert(dm, dm.allocate(src[i])) && delta) { 529 if (deltaempty) 530 delta->push_back(dm.allocate(src[i])); 531 else 532 delta->insert(dm, dm.allocate(src[i])); 533 } 534 } 535 } 536 } mk_union_fn(const relation_base & tgt,const relation_base & src,const relation_base * delta)537 relation_union_fn * udoc_plugin::mk_union_fn( 538 const relation_base & tgt, const relation_base & src, 539 const relation_base * delta) { 540 if (!check_kind(tgt) || !check_kind(src) || (delta && !check_kind(*delta))) { 541 return nullptr; 542 } 543 return alloc(union_fn); 544 } mk_widen_fn(const relation_base & tgt,const relation_base & src,const relation_base * delta)545 relation_union_fn * udoc_plugin::mk_widen_fn( 546 const relation_base & tgt, const relation_base & src, 547 const relation_base * delta) { 548 return mk_union_fn(tgt, src, delta); 549 } 550 551 class udoc_plugin::filter_identical_fn : public relation_mutator_fn { 552 unsigned_vector m_cols; 553 unsigned m_size; 554 bit_vector m_empty_bv; 555 union_find_default_ctx union_ctx; 556 union_find<> m_equalities; 557 public: filter_identical_fn(const relation_base & _r,unsigned col_cnt,const unsigned * identical_cols)558 filter_identical_fn(const relation_base & _r, unsigned col_cnt, const unsigned *identical_cols) 559 : m_cols(col_cnt), m_equalities(union_ctx) { 560 udoc_relation const& r = get(_r); 561 m_size = r.column_num_bits(identical_cols[0]); 562 m_empty_bv.resize(r.get_num_bits(), false); 563 for (unsigned i = 0; i < col_cnt; ++i) { 564 m_cols[i] = r.column_idx(identical_cols[i]); 565 } 566 for (unsigned i = 0, e = m_empty_bv.size(); i < e; ++i) { 567 m_equalities.mk_var(); 568 } 569 for (unsigned i = 1; i < col_cnt; ++i) { 570 for (unsigned j = 0; j < m_size; ++j) { 571 m_equalities.merge(m_cols[0]+j ,m_cols[i]+j); 572 } 573 } 574 } 575 operator ()(relation_base & _r)576 void operator()(relation_base & _r) override { 577 udoc_relation& r = get(_r); 578 udoc& d = r.get_udoc(); 579 doc_manager& dm = r.get_dm(); 580 d.merge(dm, m_cols[0], m_size, m_equalities, m_empty_bv); 581 SASSERT(d.well_formed(dm)); 582 TRACE("doc", tout << "final size: " << r.get_size_estimate_rows() << '\n';); 583 } 584 }; mk_filter_identical_fn(const relation_base & t,unsigned col_cnt,const unsigned * identical_cols)585 relation_mutator_fn * udoc_plugin::mk_filter_identical_fn( 586 const relation_base & t, unsigned col_cnt, const unsigned * identical_cols) { 587 return check_kind(t)?alloc(filter_identical_fn, t, col_cnt, identical_cols):nullptr; 588 } 589 class udoc_plugin::filter_equal_fn : public relation_mutator_fn { 590 doc_manager& dm; 591 doc* m_filter; 592 public: filter_equal_fn(udoc_plugin & p,const udoc_relation & t,const relation_element val,unsigned col)593 filter_equal_fn(udoc_plugin& p, const udoc_relation & t, const relation_element val, unsigned col): 594 dm(p.dm(t.get_signature())) { 595 rational r; 596 unsigned num_bits; 597 VERIFY(p.is_numeral(val, r, num_bits)); 598 m_filter = dm.allocateX(); 599 unsigned lo = t.column_idx(col); 600 unsigned hi = t.column_idx(col+1); 601 SASSERT(num_bits == hi - lo); 602 dm.tbvm().set(m_filter->pos(), r, hi-1, lo); 603 } ~filter_equal_fn()604 ~filter_equal_fn() override { 605 dm.deallocate(m_filter); 606 } operator ()(relation_base & tb)607 void operator()(relation_base & tb) override { 608 udoc_relation & t = get(tb); 609 t.get_udoc().intersect(dm, *m_filter); 610 SASSERT(t.get_udoc().well_formed(t.get_dm())); 611 } 612 }; mk_filter_equal_fn(const relation_base & t,const relation_element & value,unsigned col)613 relation_mutator_fn * udoc_plugin::mk_filter_equal_fn( 614 const relation_base & t, const relation_element & value, unsigned col) { 615 if (!check_kind(t)) 616 return nullptr; 617 return alloc(filter_equal_fn, *this, get(t), value, col); 618 } 619 is_guard(unsigned n,expr * const * gs) const620 bool udoc_relation::is_guard(unsigned n, expr* const* gs) const { 621 for (unsigned i = 0; i < n; ++i) { 622 if (!is_guard(gs[i])) return false; 623 } 624 return true; 625 } is_guard(expr * g) const626 bool udoc_relation::is_guard(expr* g) const { 627 udoc_plugin& p = get_plugin(); 628 ast_manager& m = p.get_ast_manager(); 629 bv_util& bv = p.bv; 630 expr* e1, *e2; 631 unsigned hi, lo, v; 632 if (m.is_and(g) || m.is_or(g) || m.is_not(g) || m.is_true(g) || m.is_false(g)) { 633 return is_guard(to_app(g)->get_num_args(), to_app(g)->get_args()); 634 } 635 if (m.is_eq(g, e1, e2) && bv.is_bv(e1)) { 636 if (is_var_range(e1, hi, lo, v) && is_ground(e2)) return true; 637 if (is_var_range(e2, hi, lo, v) && is_ground(e1)) return true; 638 } 639 if (is_var(g)) { 640 return true; 641 } 642 return false; 643 } 644 extract_guard(expr * cond,expr_ref & guard,expr_ref & rest) const645 void udoc_relation::extract_guard(expr* cond, expr_ref& guard, expr_ref& rest) const { 646 rest.reset(); 647 ast_manager& m = get_plugin().get_ast_manager(); 648 expr_ref_vector conds(m), guards(m), rests(m); 649 conds.push_back(cond); 650 flatten_and(conds); 651 for (unsigned i = 0; i < conds.size(); ++i) { 652 expr* g = conds[i].get(); 653 if (is_guard(g)) { 654 guards.push_back(g); 655 } 656 else { 657 rests.push_back(g); 658 } 659 } 660 guard = mk_and(m, guards.size(), guards.data()); 661 rest = mk_and(m, rests.size(), rests.data()); 662 } extract_equalities(expr * g,expr_ref & rest,subset_ints & equalities,unsigned_vector & roots) const663 void udoc_relation::extract_equalities(expr* g, expr_ref& rest, subset_ints& equalities, 664 unsigned_vector& roots) const { 665 rest.reset(); 666 ast_manager& m = get_plugin().get_ast_manager(); 667 expr_ref_vector conds(m); 668 conds.push_back(g); 669 flatten_and(conds); 670 expr* e1, *e2; 671 for (unsigned i = 0; i < conds.size(); ++i) { 672 expr* g = conds[i].get(); 673 if (m.is_eq(g, e1, e2)) { 674 extract_equalities(e1, e2, conds, equalities, roots); 675 conds[i] = conds.back(); 676 conds.pop_back(); 677 } 678 } 679 rest = mk_and(m, conds.size(), conds.data()); 680 } 681 extract_equalities(expr * e1,expr * e2,expr_ref_vector & conds,subset_ints & equalities,unsigned_vector & roots) const682 void udoc_relation::extract_equalities( 683 expr* e1, expr* e2, expr_ref_vector& conds, 684 subset_ints& equalities, unsigned_vector& roots) const { 685 udoc_plugin& p = get_plugin(); 686 ast_manager& m = p.get_ast_manager(); 687 bv_util& bv = p.bv; 688 th_rewriter rw(m); 689 unsigned hi, lo1, lo2, hi1, hi2, v1, v2; 690 if (bv.is_concat(e2)) { 691 std::swap(e1, e2); 692 } 693 if (bv.is_concat(e1)) { 694 expr_ref e3(m); 695 app* a1 = to_app(e1); 696 hi = p.num_sort_bits(e1)-1; 697 unsigned n = a1->get_num_args(); 698 for (unsigned i = 0; i < n; ++i) { 699 expr* e = a1->get_arg(i); 700 unsigned sz = p.num_sort_bits(e); 701 e3 = bv.mk_extract(hi, hi-sz+1, e2); 702 rw(e3); 703 extract_equalities(e, e3, conds, equalities, roots); 704 hi -= sz; 705 } 706 return; 707 } 708 if (is_var_range(e1, hi1, lo1, v1) && 709 is_var_range(e2, hi2, lo2, v2)) { 710 unsigned col1 = column_idx(v1); 711 lo1 += col1; 712 hi1 += col1; 713 unsigned col2 = column_idx(v2); 714 lo2 += col2; 715 hi2 += col2; 716 for (unsigned j = 0; j <= hi1-lo1; ++j) { 717 roots.push_back(lo1 + j); 718 equalities.merge(lo1 + j, lo2 + j); 719 } 720 return; 721 } 722 conds.push_back(m.mk_eq(e1, e2)); 723 } 724 compile_guard(expr * g,udoc & result,bit_vector const & discard_cols) const725 void udoc_relation::compile_guard(expr* g, udoc& result, bit_vector const& discard_cols) const { 726 result.push_back(dm.allocateX()); 727 728 // datastructure to store equalities with columns that will be projected out 729 union_find_default_ctx union_ctx; 730 subset_ints equalities(union_ctx); 731 for (unsigned i = 0, e = discard_cols.size(); i < e; ++i) { 732 equalities.mk_var(); 733 } 734 apply_guard(g, result, equalities, discard_cols); 735 } 736 apply_ground_eq(doc_ref & d,unsigned v,unsigned hi,unsigned lo,expr * c) const737 bool udoc_relation::apply_ground_eq(doc_ref& d, unsigned v, unsigned hi, unsigned lo, expr* c) const { 738 udoc_plugin& p = get_plugin(); 739 unsigned num_bits; 740 rational r; 741 unsigned col = column_idx(v); 742 lo += col; 743 hi += col; 744 if (p.is_numeral(c, r, num_bits)) { 745 d = dm.allocateX(); 746 dm.tbvm().set(d->pos(), r, hi, lo); 747 return true; 748 } 749 // other cases? 750 return false; 751 } 752 apply_bv_eq(expr * e1,expr * e2,bit_vector const & discard_cols,udoc & result) const753 bool udoc_relation::apply_bv_eq( 754 expr* e1, expr* e2, bit_vector const& discard_cols, udoc& result) const { 755 udoc_plugin& p = get_plugin(); 756 ast_manager& m = p.get_ast_manager(); 757 bv_util& bv = p.bv; 758 th_rewriter rw(m); 759 doc_ref d(get_dm()); 760 unsigned hi, lo, lo1, lo2, hi1, hi2, v, v1, v2; 761 if (bv.is_concat(e2)) { 762 std::swap(e1, e2); 763 } 764 if (bv.is_concat(e1)) { 765 expr_ref e3(m); 766 app* a1 = to_app(e1); 767 hi = p.num_sort_bits(e1)-1; 768 unsigned n = a1->get_num_args(); 769 for (unsigned i = 0; i < n; ++i) { 770 expr* e = a1->get_arg(i); 771 unsigned sz = p.num_sort_bits(e); 772 e3 = bv.mk_extract(hi, hi-sz+1, e2); 773 rw(e3); 774 if (!apply_bv_eq(e, e3, discard_cols, result)) return false; 775 hi -= sz; 776 } 777 return true; 778 } 779 if (is_ground(e1)) { 780 std::swap(e1, e2); 781 } 782 if (is_var_range(e1, hi, lo, v) && is_ground(e2) && 783 apply_ground_eq(d, v, hi, lo, e2)) { 784 result.intersect(dm, *d); 785 return true; 786 } 787 if (is_var_range(e1, hi1, lo1, v1) && 788 is_var_range(e2, hi2, lo2, v2)) { 789 unsigned idx1 = lo1 + column_idx(v1); 790 unsigned idx2 = lo2 + column_idx(v2); 791 unsigned length = hi1-lo1+1; 792 result.merge(dm, idx1, idx2, length, discard_cols); 793 return true; 794 } 795 796 return false; 797 } 798 apply_guard(expr * g,udoc & result,subset_ints const & equalities,bit_vector const & discard_cols) const799 void udoc_relation::apply_guard( 800 expr* g, udoc& result, subset_ints const& equalities, bit_vector const& discard_cols) const { 801 ast_manager& m = get_plugin().get_ast_manager(); 802 bv_util& bv = get_plugin().bv; 803 expr *e0, *e1, *e2; 804 unsigned hi, lo, v; 805 doc_ref d(get_dm()); 806 if (result.is_empty()) { 807 } 808 else if (m.is_true(g)) { 809 } 810 else if (m.is_false(g)) { 811 result.reset(dm); 812 } 813 else if (m.is_and(g)) { 814 for (unsigned i = 0; !result.is_empty() && i < to_app(g)->get_num_args(); ++i) { 815 apply_guard(to_app(g)->get_arg(i), result, equalities, discard_cols); 816 } 817 } 818 else if (m.is_not(g, e0) && 819 m.is_eq(e0, e1, e2) && bv.is_bv(e1) && 820 is_var_range(e1, hi, lo, v) && is_ground(e2) && 821 apply_ground_eq(d, v, hi, lo, e2)) { 822 result.subtract(dm, *d); 823 } 824 else if (m.is_not(g, e0) && 825 m.is_eq(e0, e2, e1) && bv.is_bv(e1) && 826 is_var_range(e1, hi, lo, v) && is_ground(e2) && 827 apply_ground_eq(d, v, hi, lo, e2)) { 828 result.subtract(dm, *d); 829 } 830 else if (m.is_not(g, e1)) { 831 udoc sub; 832 sub.push_back(dm.allocateX()); 833 // TODO: right now we state that no columns are discarded to avoid 834 // silent column merging. This can be optimized if the set of merged 835 // columns is returned so that here we remove different columns. 836 bit_vector empty; 837 empty.resize(discard_cols.size(), false); 838 apply_guard(e1, sub, equalities, empty); 839 result.subtract(dm, sub); 840 result.simplify(dm); 841 TRACE("doc", 842 result.display(dm, tout << "result0:") << "\n"; 843 sub.display(dm, tout << "sub:") << "\n";); 844 sub.reset(dm); 845 TRACE("doc", result.display(dm, tout << "result:") << "\n";); 846 } 847 else if (m.is_or(g)) { 848 udoc sub; 849 sub.push_back(dm.allocateX()); 850 for (unsigned i = 0; !sub.is_empty() && i < to_app(g)->get_num_args(); ++i) { 851 expr_ref arg(m); 852 arg = mk_not(m, to_app(g)->get_arg(i)); 853 apply_guard(arg, sub, equalities, discard_cols); 854 } 855 TRACE("doc", result.display(dm, tout << "result0:") << "\n";); 856 result.subtract(dm, sub); 857 TRACE("doc", 858 sub.display(dm, tout << "sub:") << "\n"; 859 result.display(dm, tout << "result:") << "\n";); 860 sub.reset(dm); 861 } 862 else if (is_var(g)) { 863 SASSERT(m.is_bool(g)); 864 unsigned v = to_var(g)->get_idx(); 865 unsigned idx = column_idx(v); 866 doc_ref d(dm); 867 d = dm.allocateX(); 868 dm.set(*d, idx, BIT_1); 869 result.intersect(dm, *d); 870 } 871 else if (m.is_iff(g, e1, e2)) { 872 udoc diff1, diff2; 873 diff1.push_back(dm.allocateX()); 874 diff2.push_back(dm.allocateX()); 875 expr_ref f1(m), f2(m); 876 f1 = mk_not(m, e1); 877 f2 = mk_not(m, e2); 878 apply_guard(e1, diff1, equalities, discard_cols); 879 apply_guard(f2, diff1, equalities, discard_cols); 880 result.subtract(dm, diff1); 881 diff1.reset(dm); 882 apply_guard(f1, diff2, equalities, discard_cols); 883 apply_guard(e2, diff2, equalities, discard_cols); 884 result.subtract(dm, diff2); 885 diff2.reset(dm); 886 } 887 else if (m.is_eq(g, e1, e2) && bv.is_bv(e1)) { 888 if (apply_bv_eq(e1, e2, discard_cols, result)) { 889 // done 890 } 891 else { 892 goto failure_case; 893 } 894 } 895 else { 896 failure_case: 897 std::ostringstream strm; 898 strm << "Guard expression is not handled" << mk_pp(g, m); 899 throw default_exception(strm.str()); 900 } 901 } 902 903 class udoc_plugin::filter_interpreted_fn : public relation_mutator_fn { 904 union_find_default_ctx union_ctx; 905 doc_manager& dm; 906 expr_ref m_original_condition; 907 expr_ref m_reduced_condition; 908 udoc m_udoc; 909 bit_vector m_empty_bv; 910 subset_ints m_equalities; 911 912 public: filter_interpreted_fn(const udoc_relation & t,ast_manager & m,app * condition)913 filter_interpreted_fn(const udoc_relation & t, ast_manager& m, app *condition) : 914 dm(t.get_dm()), 915 m_original_condition(condition, m), 916 m_reduced_condition(m), 917 m_equalities(union_ctx) { 918 unsigned num_bits = t.get_num_bits(); 919 m_empty_bv.resize(num_bits, false); 920 expr_ref guard(m); 921 for (unsigned i = 0; i < num_bits; ++i) { 922 m_equalities.mk_var(); 923 } 924 t.extract_guard(condition, guard, m_reduced_condition); 925 m_udoc.push_back(dm.allocateX()); 926 t.apply_guard(guard, m_udoc, m_equalities, m_empty_bv); 927 928 TRACE("doc", 929 tout << "original condition: " << mk_pp(condition, m) << "\n"; 930 tout << "remaining condition: " << m_reduced_condition << "\n"; 931 m_udoc.display(dm, tout) << "\n";); 932 } 933 ~filter_interpreted_fn()934 ~filter_interpreted_fn() override { 935 m_udoc.reset(dm); 936 } 937 operator ()(relation_base & tb)938 void operator()(relation_base & tb) override { 939 udoc_relation & t = get(tb); 940 udoc& u = t.get_udoc(); 941 SASSERT(u.well_formed(dm)); 942 u.intersect(dm, m_udoc); 943 SASSERT(u.well_formed(dm)); 944 t.apply_guard(m_reduced_condition, u, m_equalities, m_empty_bv); 945 SASSERT(u.well_formed(dm)); 946 u.simplify(dm); 947 SASSERT(u.well_formed(dm)); 948 TRACE("doc", tout << "final size: " << t.get_size_estimate_rows() << '\n';); 949 IF_VERBOSE(3, t.display(verbose_stream());); 950 } 951 }; mk_filter_interpreted_fn(const relation_base & t,app * condition)952 relation_mutator_fn * udoc_plugin::mk_filter_interpreted_fn(const relation_base & t, app * condition) { 953 return check_kind(t)?alloc(filter_interpreted_fn, get(t), get_ast_manager(), condition):nullptr; 954 } 955 956 class udoc_plugin::join_project_fn : public convenient_relation_join_project_fn { 957 #if 0 958 udoc_plugin::join_fn m_joiner; 959 #endif 960 bit_vector m_to_delete; 961 962 public: join_project_fn(udoc_relation const & t1,udoc_relation const & t2,unsigned col_cnt,const unsigned * cols1,const unsigned * cols2,unsigned removed_col_cnt,unsigned const * rm_cols)963 join_project_fn( 964 udoc_relation const& t1, udoc_relation const& t2, unsigned col_cnt, 965 const unsigned * cols1, const unsigned * cols2, 966 unsigned removed_col_cnt, unsigned const* rm_cols) 967 : convenient_relation_join_project_fn( 968 t1.get_signature(), t2.get_signature(), 969 col_cnt, cols1, cols2, 970 removed_col_cnt, rm_cols) 971 #if 0 972 , m_joiner(t1.get_plugin(), t1, t2, col_cnt, cols1, cols2) 973 #endif 974 { 975 unsigned num_bits1 = t1.get_num_bits(); 976 unsigned num_bits = num_bits1 + t2.get_num_bits(); 977 unsigned_vector removed_cols(removed_col_cnt, rm_cols); 978 t1.expand_column_vector(removed_cols, &t2); 979 t1.expand_column_vector(m_cols1); 980 t2.expand_column_vector(m_cols2); 981 m_to_delete.resize(num_bits, false); 982 for (unsigned i = 0; i < removed_cols.size(); ++i) { 983 m_to_delete.set(removed_cols[i], true); 984 } 985 } 986 987 988 // TBD: replace this by "join" given below. operator ()(relation_base const & t1,relation_base const & t2)989 relation_base* operator()(relation_base const& t1, relation_base const& t2) override { 990 #if 1 991 return join(get(t1), get(t2)); 992 #else 993 udoc_relation *joined = get(m_joiner(t1, t2)); 994 relation_base* result = 0; 995 if (joined->fast_empty()) { 996 result = t1.get_plugin().mk_empty(get_result_signature()); 997 } 998 else { 999 project_fn projector(*joined, m_removed_cols.size(), m_removed_cols.c_ptr()); 1000 result = projector(*joined); 1001 } 1002 joined->deallocate(); 1003 return result; 1004 #endif 1005 } 1006 private: 1007 join(udoc_relation const & t1,udoc_relation const & t2)1008 udoc_relation* join(udoc_relation const& t1, udoc_relation const& t2) { 1009 relation_signature prod_signature; 1010 prod_signature.append(t1.get_signature()); 1011 prod_signature.append(t2.get_signature()); 1012 udoc const& d1 = t1.get_udoc(); 1013 udoc const& d2 = t2.get_udoc(); 1014 doc_manager& dm1 = t1.get_dm(); 1015 udoc_plugin& p = t1.get_plugin(); 1016 doc_manager& dm_prod = p.dm(prod_signature); 1017 udoc_relation* result = get(p.mk_empty(get_result_signature())); 1018 udoc& res = result->get_udoc(); 1019 doc_manager& dm_res = result->get_dm(); 1020 1021 for (unsigned i = 0; i < d1.size(); ++i) { 1022 for (unsigned j = 0; j < d2.size(); ++j) { 1023 doc_ref d(dm_prod, dm_prod.join(d1[i], d2[j], dm1, m_cols1, m_cols2)); 1024 if (d) { 1025 res.insert(dm_res, dm_prod.project(dm_res, m_to_delete, *d)); 1026 IF_VERBOSE(2, 1027 if (res.size() > 0 && 0 == res.size() % 10000) { 1028 verbose_stream() << "result size: " << res.size() 1029 << " i:" << i << " j:" << j << " " 1030 << 100*i/d1.size() << "% complete\n"; 1031 }); 1032 } 1033 } 1034 } 1035 TRACE("doc", result->display(tout);); 1036 return result; 1037 } 1038 }; 1039 1040 1041 class udoc_plugin::join_project_and_fn : public relation_join_fn { 1042 public: join_project_and_fn()1043 join_project_and_fn() {} 1044 operator ()(relation_base const & t1,relation_base const & t2)1045 relation_base* operator()(relation_base const& t1, relation_base const& t2) override { 1046 udoc_relation *result = get(t1.clone()); 1047 result->get_udoc().intersect(result->get_dm(), get(t2).get_udoc()); 1048 return result; 1049 } 1050 }; 1051 mk_join_project_fn(relation_base const & t1,relation_base const & t2,unsigned joined_col_cnt,const unsigned * cols1,const unsigned * cols2,unsigned removed_col_cnt,const unsigned * removed_cols)1052 relation_join_fn * udoc_plugin::mk_join_project_fn( 1053 relation_base const& t1, relation_base const& t2, 1054 unsigned joined_col_cnt, const unsigned * cols1, const unsigned * cols2, 1055 unsigned removed_col_cnt, const unsigned * removed_cols) { 1056 if (!check_kind(t1) || !check_kind(t2)) 1057 return nullptr; 1058 // special case where we have h(X) :- f(X), g(X). 1059 if (joined_col_cnt == removed_col_cnt && 1060 t1.get_signature().size() == joined_col_cnt && 1061 t2.get_signature().size() == joined_col_cnt) { 1062 for (unsigned i = 0; i < removed_col_cnt; ++i) { 1063 if (removed_cols[i] != i || cols1[i] != cols2[i]) 1064 goto general_fn; 1065 } 1066 return alloc(join_project_and_fn); 1067 } 1068 1069 general_fn: 1070 return alloc(join_project_fn, get(t1), get(t2), 1071 joined_col_cnt, cols1, cols2, 1072 removed_col_cnt, removed_cols); 1073 } 1074 1075 1076 // 1077 // Notes: 1078 // 1. this code could use some cleanup and simplification. 1079 // 2. It is also not very efficient in the copy routines. 1080 // They fall back to copying each bit instead of a chunk. 1081 // 3. Argument about correctness is needed as comments. 1082 // 4. Unit/stress test cases are needed. 1083 // 1084 class udoc_plugin::negation_filter_fn : public relation_intersection_filter_fn { 1085 struct mk_remove_cols { mk_remove_colsdatalog::udoc_plugin::negation_filter_fn::mk_remove_cols1086 mk_remove_cols(relation_base const& t1, relation_base const& t2, unsigned_vector& remove_cols) { 1087 unsigned sz1 = t1.get_signature().size(); 1088 unsigned sz2 = t2.get_signature().size(); 1089 for (unsigned i = 0; i < sz2; ++i) { 1090 remove_cols.push_back(sz1 + i); 1091 } 1092 } 1093 }; 1094 unsigned_vector m_t_cols; 1095 unsigned_vector m_neg_cols; 1096 unsigned_vector m_remove_cols; 1097 mk_remove_cols m_mk_remove_cols; 1098 join_project_fn m_join_project; 1099 bool m_is_subtract; 1100 //bool m_is_aliased; 1101 public: negation_filter_fn(const udoc_relation & t,const udoc_relation & neg,unsigned joined_col_cnt,const unsigned * t_cols,const unsigned * neg_cols)1102 negation_filter_fn(const udoc_relation & t, const udoc_relation & neg, unsigned joined_col_cnt, 1103 const unsigned *t_cols, const unsigned *neg_cols) 1104 : m_t_cols(joined_col_cnt, t_cols), 1105 m_neg_cols(joined_col_cnt, neg_cols), 1106 m_mk_remove_cols(t, neg, m_remove_cols), 1107 m_join_project(t, neg, joined_col_cnt, t_cols, neg_cols, 1108 m_remove_cols.size(), m_remove_cols.data()), 1109 m_is_subtract(false)//, 1110 /*m_is_aliased(true) */{ 1111 SASSERT(joined_col_cnt > 0 || neg.get_signature().size() == 0); 1112 m_is_subtract = (joined_col_cnt == t.get_signature().size()); 1113 m_is_subtract &= (joined_col_cnt == neg.get_signature().size()); 1114 bool_vector found(joined_col_cnt, false); 1115 for (unsigned i = 0; m_is_subtract && i < joined_col_cnt; ++i) { 1116 m_is_subtract = !found[t_cols[i]] && (t_cols[i] == neg_cols[i]); 1117 found[t_cols[i]] = true; 1118 } 1119 t.expand_column_vector(m_t_cols); 1120 neg.expand_column_vector(m_neg_cols); 1121 } 1122 operator ()(relation_base & tb,const relation_base & negb)1123 void operator()(relation_base& tb, const relation_base& negb) override { 1124 udoc_relation& t = get(tb); 1125 udoc_relation const& n = get(negb); 1126 IF_VERBOSE(3, t.display(verbose_stream() << "dst:");); 1127 IF_VERBOSE(3, n.display(verbose_stream() << "neg:");); 1128 if (t.fast_empty() || n.fast_empty()) 1129 return; 1130 1131 /* TODO: double check 1132 if (!m_is_aliased && !p.m_disable_fast_pass) { 1133 // fast_pass(t, n); 1134 } 1135 */ 1136 if (n.get_signature().empty()) 1137 t.get_udoc().reset(t.get_dm()); 1138 else if (m_is_subtract) 1139 t.get_udoc().subtract(t.get_dm(), n.get_udoc()); 1140 else 1141 slow_pass(t, n); 1142 } 1143 1144 private: 1145 /* 1146 void fast_pass(udoc_relation& t, const udoc_relation& n) { 1147 SASSERT(!m_is_aliased); 1148 udoc & dst = t.get_udoc(); 1149 udoc const & neg = n.get_udoc(); 1150 doc_manager& dmt = t.get_dm(); 1151 doc_manager& dmn = n.get_dm(); 1152 udoc result; 1153 for (unsigned i = 0; i < dst.size(); ++i) { 1154 bool subsumed = false; 1155 for (unsigned j = 0; j < neg.size(); ++j) { 1156 if (dmn.contains(neg[j], m_neg_cols, dst[i], m_t_cols)) { 1157 dmt.deallocate(&dst[i]); 1158 subsumed = true; 1159 break; 1160 } 1161 } 1162 if (!subsumed) 1163 result.push_back(&dst[i]); 1164 } 1165 std::swap(dst, result); 1166 } 1167 */ 1168 slow_pass(udoc_relation & t,udoc_relation const & n)1169 void slow_pass(udoc_relation& t, udoc_relation const& n) { 1170 doc_manager& dmt = t.get_dm(); 1171 udoc_relation* jp = get(m_join_project(t, n)); 1172 if (!jp->fast_empty()) { 1173 t.get_udoc().subtract(dmt, jp->get_udoc()); 1174 } 1175 TRACE("doc", t.display(tout); tout << "\n"; jp->display(tout); tout << "\n";); 1176 jp->deallocate(); 1177 } 1178 }; 1179 mk_filter_by_negation_fn(const relation_base & t,const relation_base & neg,unsigned joined_col_cnt,const unsigned * t_cols,const unsigned * negated_cols)1180 relation_intersection_filter_fn * udoc_plugin::mk_filter_by_negation_fn( 1181 const relation_base& t, 1182 const relation_base& neg, unsigned joined_col_cnt, const unsigned *t_cols, 1183 const unsigned *negated_cols) { 1184 if (!check_kind(t) || !check_kind(neg)) 1185 return nullptr; 1186 return alloc(negation_filter_fn, get(t), get(neg), joined_col_cnt, t_cols, negated_cols); 1187 } 1188 1189 1190 1191 class udoc_plugin::filter_proj_fn : public convenient_relation_project_fn { 1192 union_find_default_ctx union_ctx; 1193 doc_manager& dm; 1194 expr_ref m_original_condition; 1195 expr_ref m_reduced_condition; 1196 udoc m_udoc; 1197 udoc m_udoc2; 1198 bit_vector m_to_delete; // map: col idx -> bool (whether the column is to be removed) 1199 subset_ints m_equalities; 1200 unsigned_vector m_roots; 1201 1202 public: filter_proj_fn(const udoc_relation & t,ast_manager & m,app * condition,unsigned col_cnt,const unsigned * removed_cols)1203 filter_proj_fn(const udoc_relation & t, ast_manager& m, app *condition, 1204 unsigned col_cnt, const unsigned * removed_cols) : 1205 convenient_relation_project_fn(t.get_signature(), col_cnt, removed_cols), 1206 dm(t.get_dm()), 1207 m_original_condition(condition, m), 1208 m_reduced_condition(m), 1209 m_equalities(union_ctx) { 1210 unsigned num_bits = t.get_num_bits(); 1211 t.expand_column_vector(m_removed_cols); 1212 m_to_delete.resize(num_bits, false); 1213 for (unsigned i = 0; i < num_bits; ++i) { 1214 m_equalities.mk_var(); 1215 } 1216 for (unsigned i = 0; i < m_removed_cols.size(); ++i) { 1217 m_to_delete.set(m_removed_cols[i], true); 1218 } 1219 expr_ref guard(m), non_eq_cond(condition, m); 1220 t.extract_equalities(condition, non_eq_cond, m_equalities, m_roots); 1221 t.extract_guard(non_eq_cond, guard, m_reduced_condition); 1222 t.compile_guard(guard, m_udoc, m_to_delete); 1223 } 1224 ~filter_proj_fn()1225 ~filter_proj_fn() override { 1226 m_udoc.reset(dm); 1227 } operator ()(const relation_base & tb)1228 relation_base* operator()(const relation_base & tb) override { 1229 udoc_relation const & t = get(tb); 1230 udoc const& u1 = t.get_udoc(); 1231 doc_manager& dm = t.get_dm(); 1232 m_udoc2.copy(dm, u1); 1233 m_udoc2.intersect(dm, m_udoc); 1234 t.apply_guard(m_reduced_condition, m_udoc2, m_equalities, m_to_delete); 1235 m_udoc2.merge(dm, m_roots, m_equalities, m_to_delete); 1236 SASSERT(m_udoc2.well_formed(dm)); 1237 udoc_relation* r = get(t.get_plugin().mk_empty(get_result_signature())); 1238 doc_manager& dm2 = r->get_dm(); 1239 for (unsigned i = 0; i < m_udoc2.size(); ++i) { 1240 doc* d = dm.project(dm2, m_to_delete, m_udoc2[i]); 1241 r->get_udoc().insert(dm2, d); 1242 SASSERT(r->get_udoc().well_formed(dm2)); 1243 } 1244 m_udoc2.reset(dm); 1245 IF_VERBOSE(3, r->display(verbose_stream() << "filter project result:\n");); 1246 return r; 1247 } 1248 }; mk_filter_interpreted_and_project_fn(const relation_base & t,app * condition,unsigned removed_col_cnt,const unsigned * removed_cols)1249 relation_transformer_fn * udoc_plugin::mk_filter_interpreted_and_project_fn( 1250 const relation_base & t, app * condition, 1251 unsigned removed_col_cnt, const unsigned * removed_cols) { 1252 return check_kind(t)?alloc(filter_proj_fn, get(t), get_ast_manager(), condition, removed_col_cnt, removed_cols):nullptr; 1253 } 1254 1255 1256 1257 1258 1259 } 1260