1 /*++ 2 Copyright (c) 2006 Microsoft Corporation 3 4 Module Name: 5 6 dl_finite_product_relation.cpp 7 8 Abstract: 9 10 <abstract> 11 12 Author: 13 14 Krystof Hoder (t-khoder) 2010-09-14. 15 16 Revision History: 17 18 --*/ 19 20 21 #include<string> 22 #include "muz/base/dl_context.h" 23 #include "muz/rel/dl_relation_manager.h" 24 #include "muz/rel/dl_table_relation.h" 25 #include "muz/rel/dl_finite_product_relation.h" 26 #include "ast/rewriter/bool_rewriter.h" 27 #include "ast/rewriter/th_rewriter.h" 28 29 namespace datalog { 30 31 //static variables 32 33 const table_sort finite_product_relation::s_rel_idx_sort = INT_MAX; 34 universal_delete(finite_product_relation * ptr)35 void universal_delete(finite_product_relation* ptr) { 36 ptr->deallocate(); 37 } 38 39 40 // ----------------------------------- 41 // 42 // finite_product_relation_plugin 43 // 44 // ----------------------------------- 45 get(relation_base & r)46 finite_product_relation & finite_product_relation_plugin::get(relation_base & r) { 47 SASSERT(r.get_plugin().is_finite_product_relation()); 48 return static_cast<finite_product_relation &>(r); 49 } 50 get(const relation_base & r)51 const finite_product_relation & finite_product_relation_plugin::get(const relation_base & r) { 52 SASSERT(r.get_plugin().is_finite_product_relation()); 53 return static_cast<const finite_product_relation &>(r); 54 } 55 get(relation_base * r)56 finite_product_relation * finite_product_relation_plugin::get(relation_base * r) { 57 SASSERT(!r || r->get_plugin().is_finite_product_relation()); 58 return static_cast<finite_product_relation *>(r); 59 } 60 get(const relation_base * r)61 const finite_product_relation * finite_product_relation_plugin::get(const relation_base * r) { 62 SASSERT(!r || r->get_plugin().is_finite_product_relation()); 63 return static_cast<const finite_product_relation *>(r); 64 } 65 get_name(relation_plugin & inner_plugin)66 symbol finite_product_relation_plugin::get_name(relation_plugin & inner_plugin) { 67 std::string str = std::string("fpr_")+inner_plugin.get_name().bare_str(); 68 return symbol(str.c_str()); 69 } 70 get_plugin(relation_manager & rmgr,relation_plugin & inner)71 finite_product_relation_plugin & finite_product_relation_plugin::get_plugin(relation_manager & rmgr, 72 relation_plugin & inner) { 73 finite_product_relation_plugin * res; 74 if(!rmgr.try_get_finite_product_relation_plugin(inner, res)) { 75 res = alloc(finite_product_relation_plugin, inner, rmgr); 76 rmgr.register_plugin(res); 77 } 78 return *res; 79 } 80 finite_product_relation_plugin(relation_plugin & inner_plugin,relation_manager & manager)81 finite_product_relation_plugin::finite_product_relation_plugin(relation_plugin & inner_plugin, 82 relation_manager & manager) 83 : relation_plugin(get_name(inner_plugin), manager, ST_FINITE_PRODUCT_RELATION), 84 m_inner_plugin(inner_plugin), m_spec_store(*this) { 85 } 86 initialize(family_id fid)87 void finite_product_relation_plugin::initialize(family_id fid) { 88 relation_plugin::initialize(fid); 89 m_spec_store.add_available_kind(get_kind()); 90 } 91 get_relation_kind(finite_product_relation & r,const bool * table_columns)92 family_id finite_product_relation_plugin::get_relation_kind(finite_product_relation & r, 93 const bool * table_columns) { 94 const relation_signature & sig = r.get_signature(); 95 bool_vector table_cols_vect(sig.size(), table_columns); 96 return m_spec_store.get_relation_kind(sig, rel_spec(table_cols_vect)); 97 } 98 get_all_possible_table_columns(relation_manager & rmgr,const relation_signature & s,bool_vector & table_columns)99 void finite_product_relation_plugin::get_all_possible_table_columns(relation_manager & rmgr, 100 const relation_signature & s, bool_vector & table_columns) { 101 SASSERT(table_columns.empty()); 102 unsigned s_sz = s.size(); 103 for(unsigned i=0; i<s_sz; i++) { 104 table_sort t_sort; 105 //we don't care about the result of the conversion, just that it can be converted 106 bool can_be_table_column = rmgr.relation_sort_to_table(s[i], t_sort); 107 table_columns.push_back(can_be_table_column); 108 } 109 } 110 split_signatures(const relation_signature & s,table_signature & table_sig,relation_signature & remaining_sig)111 void finite_product_relation_plugin::split_signatures(const relation_signature & s, 112 table_signature & table_sig, relation_signature & remaining_sig) { 113 relation_manager & rmgr = get_manager(); 114 unsigned n = s.size(); 115 for(unsigned i=0; i<n; i++) { 116 table_sort t_sort; 117 if(rmgr.relation_sort_to_table(s[i], t_sort)) { 118 table_sig.push_back(t_sort); 119 } 120 else { 121 remaining_sig.push_back(s[i]); 122 } 123 } 124 } 125 split_signatures(const relation_signature & s,const bool * table_columns,table_signature & table_sig,relation_signature & remaining_sig)126 void finite_product_relation_plugin::split_signatures(const relation_signature & s, const bool * table_columns, 127 table_signature & table_sig, relation_signature & remaining_sig) { 128 relation_manager & rmgr = get_manager(); 129 unsigned n = s.size(); 130 for(unsigned i=0; i<n; i++) { 131 if(table_columns[i]) { 132 table_sort t_sort; 133 VERIFY( rmgr.relation_sort_to_table(s[i], t_sort) ); 134 table_sig.push_back(t_sort); 135 } 136 else { 137 remaining_sig.push_back(s[i]); 138 } 139 } 140 } 141 can_handle_signature(const relation_signature & s)142 bool finite_product_relation_plugin::can_handle_signature(const relation_signature & s) { 143 table_signature table_sig; 144 relation_signature remaining_sig; 145 split_signatures(s, table_sig, remaining_sig); 146 return m_inner_plugin.can_handle_signature(remaining_sig) 147 && get_manager().try_get_appropriate_plugin(table_sig); 148 } 149 mk_empty(const relation_signature & s)150 relation_base * finite_product_relation_plugin::mk_empty(const relation_signature & s) { 151 bool_vector table_columns; 152 get_all_possible_table_columns(s, table_columns); 153 #ifndef _EXTERNAL_RELEASE 154 unsigned s_sz = s.size(); 155 unsigned rel_col_cnt = 0; 156 for(unsigned i=0; i<s_sz; i++) { 157 if(!table_columns[i]) { 158 rel_col_cnt++; 159 } 160 } 161 if(get_manager().get_context().dbg_fpr_nonempty_relation_signature() && rel_col_cnt==0) { 162 //if the relation is empty, we will use the second half of the signature for the relation 163 relation_signature candidate_rel_sig; 164 unsigned rel_sig_ofs = s.size()/2; 165 unsigned rel_sig_sz = s.size()-rel_sig_ofs; 166 candidate_rel_sig.append(rel_sig_sz, s.data()+rel_sig_ofs); 167 if(m_inner_plugin.can_handle_signature(candidate_rel_sig)) { 168 for(unsigned i=rel_sig_ofs; i<s_sz; i++) { 169 table_columns[i] = false; 170 } 171 } 172 173 } 174 #endif 175 return mk_empty(s, table_columns.data()); 176 } 177 mk_empty(const relation_signature & s,const bool * table_columns,family_id inner_kind)178 finite_product_relation * finite_product_relation_plugin::mk_empty(const relation_signature & s, 179 const bool * table_columns, family_id inner_kind) { 180 //find table_plugin that can handle the table signature 181 table_signature table_sig; 182 relation_signature remaining_sig; 183 split_signatures(s, table_columns, table_sig, remaining_sig); 184 table_sig.push_back(finite_product_relation::s_rel_idx_sort); 185 table_sig.set_functional_columns(1); 186 table_plugin & tplugin = get_manager().get_appropriate_plugin(table_sig); 187 return alloc(finite_product_relation, *this, s, table_columns, tplugin, m_inner_plugin, inner_kind); 188 } 189 mk_empty(const finite_product_relation & original)190 finite_product_relation * finite_product_relation_plugin::mk_empty(const finite_product_relation & original) { 191 return get(mk_empty(original.get_signature(), original.get_kind())); 192 } 193 mk_empty(const relation_base & original)194 relation_base * finite_product_relation_plugin::mk_empty(const relation_base & original) { 195 SASSERT(&original.get_plugin()==this); 196 return mk_empty(get(original)); 197 } 198 mk_empty(const relation_signature & s,family_id kind)199 relation_base * finite_product_relation_plugin::mk_empty(const relation_signature & s, family_id kind) { 200 rel_spec spec; 201 m_spec_store.get_relation_spec(s, kind, spec); 202 return mk_empty(s, spec.m_table_cols.data(), spec.m_inner_kind); 203 } 204 205 mk_full(func_decl * p,const relation_signature & s)206 relation_base * finite_product_relation_plugin::mk_full(func_decl* p, const relation_signature & s) { 207 finite_product_relation * res = get(mk_empty(s)); 208 res->complement_self(p); 209 return res; 210 } 211 can_convert_to_table_relation(const finite_product_relation & r)212 bool finite_product_relation_plugin::can_convert_to_table_relation(const finite_product_relation & r) { 213 return r.m_other_sig.empty(); 214 } 215 to_table_relation(const finite_product_relation & r)216 table_relation * finite_product_relation_plugin::to_table_relation(const finite_product_relation & r) { 217 SASSERT(can_convert_to_table_relation(r)); 218 r.garbage_collect(true); 219 //now all rows in the table will correspond to rows in the resulting table_relation 220 221 const table_base & t = r.get_table(); 222 223 unsigned removed_col = t.get_signature().size()-1; 224 scoped_ptr<table_transformer_fn> project_fun = 225 get_manager().mk_project_fn(r.get_table(), 1, &removed_col); 226 227 table_base * res_table = (*project_fun)(t); 228 SASSERT(res_table->get_signature().functional_columns()==0); 229 return static_cast<table_relation *>(get_manager().mk_table_relation(r.get_signature(), res_table)); 230 } 231 232 can_be_converted(const relation_base & r)233 bool finite_product_relation_plugin::can_be_converted(const relation_base & r) { 234 if(&r.get_plugin()==&get_inner_plugin()) { 235 //can be converted by mk_from_inner_relation 236 return true; 237 } 238 if(r.from_table()) { 239 //We can convert directly from table plugin only if the inner plugin can handle empty signatures. 240 241 //TODO: If the inner plugin cannot handle empty signatures, we may try to move some of the 242 //table columns into the inner relation signature. 243 return get_inner_plugin().can_handle_signature(relation_signature()); 244 } 245 return false; 246 } 247 mk_from_table_relation(const table_relation & r)248 finite_product_relation * finite_product_relation_plugin::mk_from_table_relation(const table_relation & r) { 249 func_decl* pred = nullptr; 250 const relation_signature & sig = r.get_signature(); 251 const table_base & t = r.get_table(); 252 table_plugin & tplugin = r.get_table().get_plugin(); 253 254 relation_signature inner_sig; //empty signature for the inner relation 255 if(!get_inner_plugin().can_handle_signature(inner_sig)) { 256 return nullptr; 257 } 258 259 table_signature idx_singleton_sig; 260 idx_singleton_sig.push_back(finite_product_relation::s_rel_idx_sort); 261 idx_singleton_sig.set_functional_columns(1); 262 263 scoped_rel<table_base> idx_singleton; 264 if(tplugin.can_handle_signature(idx_singleton_sig)) { 265 idx_singleton = tplugin.mk_empty(idx_singleton_sig); 266 } 267 else { 268 idx_singleton = get_manager().mk_empty_table(idx_singleton_sig); 269 } 270 table_fact idx_singleton_fact; 271 idx_singleton_fact.push_back(0); 272 idx_singleton->add_fact(idx_singleton_fact); 273 274 scoped_ptr<table_join_fn> join_fun = get_manager().mk_join_fn(t, *idx_singleton, 0, nullptr, nullptr); 275 SASSERT(join_fun); 276 scoped_rel<table_base> res_table = (*join_fun)(t, *idx_singleton); 277 278 bool_vector table_cols(sig.size(), true); 279 finite_product_relation * res = mk_empty(sig, table_cols.data()); 280 281 //this one does not need to be deleted -- it will be taken over by \c res in the \c init function 282 relation_base * inner_rel = get_inner_plugin().mk_full(pred, inner_sig, get_inner_plugin().get_kind()); 283 284 relation_vector rels; 285 rels.push_back(inner_rel); 286 287 res->init(*res_table, rels, true); 288 return res; 289 } 290 mk_from_inner_relation(const relation_base & r)291 finite_product_relation * finite_product_relation_plugin::mk_from_inner_relation(const relation_base & r) { 292 SASSERT(&r.get_plugin()==&get_inner_plugin()); 293 const relation_signature & sig = r.get_signature(); 294 295 table_signature idx_singleton_sig; 296 idx_singleton_sig.push_back(finite_product_relation::s_rel_idx_sort); 297 idx_singleton_sig.set_functional_columns(1); 298 299 scoped_rel<table_base> idx_singleton = get_manager().mk_empty_table(idx_singleton_sig); 300 table_fact idx_singleton_fact; 301 idx_singleton_fact.push_back(0); 302 idx_singleton->add_fact(idx_singleton_fact); 303 304 bool_vector table_cols(sig.size(), false); 305 finite_product_relation * res = mk_empty(sig, table_cols.data()); 306 307 relation_vector rels; 308 rels.push_back(r.clone()); 309 310 res->init(*idx_singleton, rels, true); 311 return res; 312 } 313 314 class finite_product_relation_plugin::converting_join_fn : public convenient_relation_join_fn { 315 finite_product_relation_plugin & m_plugin; 316 scoped_ptr<relation_join_fn> m_native_join; 317 convert(const relation_base & r)318 finite_product_relation * convert(const relation_base & r) { 319 SASSERT(&r.get_plugin()!=&m_plugin); 320 if(&r.get_plugin()==&m_plugin.get_inner_plugin()) { 321 return m_plugin.mk_from_inner_relation(r); 322 } 323 SASSERT(r.from_table()); 324 const table_relation & tr = static_cast<const table_relation &>(r); 325 finite_product_relation * res = m_plugin.mk_from_table_relation(tr); 326 SASSERT(res); 327 return res; 328 } 329 330 public: converting_join_fn(finite_product_relation_plugin & plugin,const relation_signature & sig1,const relation_signature & sig2,unsigned col_cnt,const unsigned * cols1,const unsigned * cols2)331 converting_join_fn(finite_product_relation_plugin & plugin, const relation_signature & sig1, 332 const relation_signature & sig2, unsigned col_cnt, const unsigned * cols1, 333 const unsigned * cols2) 334 : convenient_relation_join_fn(sig1, sig2, col_cnt, cols1, cols2), 335 m_plugin(plugin) {} 336 operator ()(const relation_base & r1,const relation_base & r2)337 relation_base * operator()(const relation_base & r1, const relation_base & r2) override { 338 scoped_rel<finite_product_relation> r1_conv; 339 if(&r1.get_plugin()!=&m_plugin) { 340 r1_conv = convert(r1); 341 } 342 scoped_rel<finite_product_relation> r2_conv; 343 if(&r2.get_plugin()!=&m_plugin) { 344 r2_conv = convert(r2); 345 } 346 347 const finite_product_relation & fpr1 = r1_conv ? *r1_conv : get(r1); 348 const finite_product_relation & fpr2 = r2_conv ? *r2_conv : get(r2); 349 350 SASSERT(&fpr1.get_plugin()==&m_plugin); 351 SASSERT(&fpr2.get_plugin()==&m_plugin); 352 353 if(!m_native_join) { 354 m_native_join = m_plugin.get_manager().mk_join_fn(fpr1, fpr2, m_cols1, m_cols2, false); 355 } 356 return (*m_native_join)(fpr1, fpr2); 357 } 358 }; 359 360 361 class finite_product_relation_plugin::join_fn : public convenient_relation_join_fn { 362 scoped_ptr<table_join_fn> m_tjoin_fn; 363 scoped_ptr<relation_join_fn> m_rjoin_fn; 364 365 unsigned_vector m_t_joined_cols1; 366 unsigned_vector m_t_joined_cols2; 367 unsigned_vector m_r_joined_cols1; 368 unsigned_vector m_r_joined_cols2; 369 370 //Column equalities betweet table and inner relations. 371 //The columns numbers correspont to the columns of the table/inner relation 372 //in the result of the join operation 373 unsigned_vector m_tr_table_joined_cols; 374 unsigned_vector m_tr_rel_joined_cols; 375 376 scoped_ptr<relation_mutator_fn> m_filter_tr_identities; 377 378 scoped_ptr<table_transformer_fn> m_tjoined_second_rel_remover; 379 380 //determines which columns of the result are table columns and which are in the inner relation 381 bool_vector m_res_table_columns; 382 383 public: 384 class join_maker : public table_row_mutator_fn { 385 join_fn & m_parent; 386 const finite_product_relation & m_r1; 387 const finite_product_relation & m_r2; 388 relation_vector & m_rjoins; 389 public: join_maker(join_fn & parent,const finite_product_relation & r1,const finite_product_relation & r2,relation_vector & rjoins)390 join_maker(join_fn & parent, const finite_product_relation & r1, const finite_product_relation & r2, 391 relation_vector & rjoins) 392 : m_parent(parent), m_r1(r1), m_r2(r2), m_rjoins(rjoins) {} 393 operator ()(table_element * func_columns)394 bool operator()(table_element * func_columns) override { 395 const relation_base & or1 = m_r1.get_inner_rel(func_columns[0]); 396 const relation_base & or2 = m_r2.get_inner_rel(func_columns[1]); 397 unsigned new_rel_num = m_rjoins.size(); 398 m_rjoins.push_back(m_parent.do_rjoin(or1, or2)); 399 func_columns[0]=new_rel_num; 400 return true; 401 } 402 }; 403 join_fn(const finite_product_relation & r1,const finite_product_relation & r2,unsigned col_cnt,const unsigned * cols1,const unsigned * cols2)404 join_fn(const finite_product_relation & r1, const finite_product_relation & r2, unsigned col_cnt, 405 const unsigned * cols1, const unsigned * cols2) 406 : convenient_relation_join_fn(r1.get_signature(), r2.get_signature(), col_cnt, cols1, cols2) { 407 unsigned second_table_after_join_ofs = r1.m_table2sig.size(); 408 unsigned second_inner_rel_after_join_ofs = r1.m_other2sig.size(); 409 for(unsigned i=0;i<col_cnt; i++) { 410 if(!r1.is_table_column(cols1[i]) && !r2.is_table_column(cols2[i])) { 411 m_r_joined_cols1.push_back(r1.m_sig2other[cols1[i]]); 412 m_r_joined_cols2.push_back(r2.m_sig2other[cols2[i]]); 413 } 414 else if(r1.is_table_column(cols1[i]) && r2.is_table_column(cols2[i])) { 415 m_t_joined_cols1.push_back(r1.m_sig2table[cols1[i]]); 416 m_t_joined_cols2.push_back(r2.m_sig2table[cols2[i]]); 417 } 418 else if(!r1.is_table_column(cols1[i]) && r2.is_table_column(cols2[i])) { 419 m_tr_rel_joined_cols.push_back(r1.m_sig2other[cols1[i]]); 420 m_tr_table_joined_cols.push_back(second_table_after_join_ofs + r2.m_sig2table[cols2[i]]); 421 } 422 else { 423 SASSERT(r1.is_table_column(cols1[i]) && !r2.is_table_column(cols2[i])); 424 m_tr_table_joined_cols.push_back(r1.m_sig2table[cols1[i]]); 425 m_tr_rel_joined_cols.push_back(second_inner_rel_after_join_ofs + r2.m_sig2other[cols2[i]]); 426 } 427 } 428 m_tjoin_fn = r1.get_manager().mk_join_fn(r1.get_table(), r2.get_table(), m_t_joined_cols1.size(), 429 m_t_joined_cols1.data(), m_t_joined_cols2.data()); 430 SASSERT(m_tjoin_fn); 431 432 433 unsigned r1_sig_sz = r1.get_signature().size(); 434 unsigned r2_sig_sz = r2.get_signature().size(); 435 for(unsigned i=0; i<r1_sig_sz; i++) { 436 m_res_table_columns.push_back(r1.is_table_column(i)); 437 } 438 for(unsigned i=0; i<r2_sig_sz; i++) { 439 m_res_table_columns.push_back(r2.is_table_column(i)); 440 } 441 442 } 443 do_rjoin(const relation_base & r1,const relation_base & r2)444 relation_base * do_rjoin(const relation_base & r1, const relation_base & r2) { 445 if(!m_rjoin_fn) { 446 m_rjoin_fn = r1.get_manager().mk_join_fn(r1, r2, m_r_joined_cols1, m_r_joined_cols2, false); 447 } 448 SASSERT(m_rjoin_fn); 449 return (*m_rjoin_fn)(r1, r2); 450 } 451 operator ()(const relation_base & rb1,const relation_base & rb2)452 relation_base * operator()(const relation_base & rb1, const relation_base & rb2) override { 453 finite_product_relation_plugin & plugin = get(rb1).get_plugin(); 454 relation_manager & rmgr = plugin.get_manager(); 455 456 const finite_product_relation & r1 = get(rb1); 457 const finite_product_relation & r2 = get(rb2); 458 459 scoped_rel<table_base> tjoined = (*m_tjoin_fn)(r1.get_table(), r2.get_table()); 460 461 relation_vector joined_orelations; 462 463 { 464 join_maker * mutator = alloc(join_maker, *this, r1, r2, joined_orelations); //dealocated in inner_join_mapper 465 scoped_ptr<table_mutator_fn> inner_join_mapper = rmgr.mk_map_fn(*tjoined, mutator); 466 (*inner_join_mapper)(*tjoined); 467 } 468 469 470 if(!m_tjoined_second_rel_remover) { 471 unsigned removed_col = tjoined->get_signature().size()-1; 472 m_tjoined_second_rel_remover = rmgr.mk_project_fn(*tjoined, 1, &removed_col); 473 } 474 //remove the second functional column from tjoined to get a table that corresponds 475 //to the table signature of the resulting relation 476 scoped_rel<table_base> res_table = (*m_tjoined_second_rel_remover)(*tjoined); 477 478 relation_plugin & res_oplugin = 479 joined_orelations.empty() ? r1.m_other_plugin : joined_orelations.back()->get_plugin(); 480 481 //TODO: Maybe we might want to specify a particular relation kind, instead of just null_family_id. 482 //It would however need to be somehow inferred for the new signature. 483 484 finite_product_relation * res = alloc(finite_product_relation, r1.get_plugin(), get_result_signature(), 485 m_res_table_columns.data(), res_table->get_plugin(), res_oplugin, null_family_id); 486 487 res->init(*res_table, joined_orelations, true); 488 489 if(!m_tr_table_joined_cols.empty()) { 490 //There were some shared variables between the table and the relation part. 491 //We enforce those equalities here. 492 if(!m_filter_tr_identities) { 493 m_filter_tr_identities = plugin.mk_filter_identical_pairs(*res, m_tr_table_joined_cols.size(), 494 m_tr_table_joined_cols.data(), m_tr_rel_joined_cols.data()); 495 SASSERT(m_filter_tr_identities); 496 } 497 (*m_filter_tr_identities)(*res); 498 } 499 return res; 500 } 501 }; 502 503 504 505 mk_join_fn(const relation_base & rb1,const relation_base & rb2,unsigned col_cnt,const unsigned * cols1,const unsigned * cols2)506 relation_join_fn * finite_product_relation_plugin::mk_join_fn(const relation_base & rb1, const relation_base & rb2, 507 unsigned col_cnt, const unsigned * cols1, const unsigned * cols2) { 508 if(!check_kind(rb1) || !check_kind(rb2)) { 509 bool r1foreign = &rb1.get_plugin()!=this; 510 bool r2foreign = &rb2.get_plugin()!=this; 511 if( (!r1foreign || can_be_converted(rb1)) && (!r2foreign || can_be_converted(rb2))) { 512 return alloc(converting_join_fn, *this, rb1.get_signature(), rb2.get_signature(), col_cnt, cols1, 513 cols2); 514 } 515 return nullptr; 516 } 517 const finite_product_relation & r1 = get(rb1); 518 const finite_product_relation & r2 = get(rb2); 519 520 return alloc(join_fn, r1, r2, col_cnt, cols1, cols2); 521 } 522 523 524 class finite_product_relation_plugin::project_fn : public convenient_relation_project_fn { 525 unsigned_vector m_removed_table_cols; 526 unsigned_vector m_removed_rel_cols; 527 528 scoped_ptr<relation_transformer_fn> m_rel_projector; 529 scoped_ptr<relation_union_fn> m_inner_rel_union; 530 531 //determines which columns of the result are table columns and which are in the inner relation 532 bool_vector m_res_table_columns; 533 public: project_fn(const finite_product_relation & r,unsigned col_cnt,const unsigned * removed_cols)534 project_fn(const finite_product_relation & r, unsigned col_cnt, const unsigned * removed_cols) 535 : convenient_relation_project_fn(r.get_signature(), col_cnt, removed_cols) { 536 SASSERT(col_cnt>0); 537 for(unsigned i=0; i<col_cnt; i++) { 538 unsigned col = removed_cols[i]; 539 if(r.is_table_column(col)) { 540 m_removed_table_cols.push_back(r.m_sig2table[col]); 541 } 542 else { 543 m_removed_rel_cols.push_back(r.m_sig2other[col]); 544 } 545 } 546 547 unsigned sig_sz = r.get_signature().size(); 548 unsigned removed_idx = 0; 549 for(unsigned i=0; i<sig_sz; i++) { 550 if(removed_idx<col_cnt && removed_cols[removed_idx]==i) { 551 removed_idx++; 552 continue; 553 } 554 SASSERT(removed_idx==col_cnt || removed_cols[removed_idx]>i); 555 m_res_table_columns.push_back(r.is_table_column(i)); 556 } 557 } 558 559 class project_reducer : public table_row_pair_reduce_fn { 560 project_fn & m_parent; 561 relation_vector & m_relations; 562 public: 563 project_reducer(project_fn & parent,relation_vector & relations)564 project_reducer(project_fn & parent, relation_vector & relations) 565 : m_parent(parent), m_relations(relations) {} 566 operator ()(table_element * func_columns,const table_element * merged_func_columns)567 void operator()(table_element * func_columns, const table_element * merged_func_columns) override { 568 relation_base * tgt = m_relations[static_cast<unsigned>(func_columns[0])]->clone(); 569 relation_base & src = *m_relations[static_cast<unsigned>(merged_func_columns[0])]; 570 if(!m_parent.m_inner_rel_union) { 571 m_parent.m_inner_rel_union = tgt->get_manager().mk_union_fn(*tgt, src); 572 } 573 (*m_parent.m_inner_rel_union)(*tgt, src); 574 575 unsigned new_idx = m_relations.size(); 576 m_relations.push_back(tgt); 577 func_columns[0] = new_idx; 578 } 579 }; 580 operator ()(const relation_base & rb)581 relation_base * operator()(const relation_base & rb) override { 582 const finite_product_relation & r = get(rb); 583 finite_product_relation_plugin & plugin = r.get_plugin(); 584 const table_base & rtable = r.get_table(); 585 relation_manager & rmgr = plugin.get_manager(); 586 587 r.garbage_collect(false); 588 relation_vector res_relations; 589 unsigned orig_rel_cnt = r.m_others.size(); 590 for(unsigned i=0; i<orig_rel_cnt; i++) { 591 relation_base * orig_rel = r.m_others[i]; 592 res_relations.push_back(orig_rel ? orig_rel->clone() : nullptr); 593 } 594 SASSERT(res_relations.size()==orig_rel_cnt); 595 596 bool shared_res_table = false; 597 const table_base * res_table; 598 599 if(m_removed_table_cols.empty()) { 600 shared_res_table = true; 601 res_table = &rtable; 602 } 603 else { 604 project_reducer * preducer = alloc(project_reducer, *this, res_relations); 605 scoped_ptr<table_transformer_fn> tproject = 606 rmgr.mk_project_with_reduce_fn(rtable, m_removed_table_cols.size(), m_removed_table_cols.data(), preducer); 607 res_table = (*tproject)(rtable); 608 } 609 610 relation_plugin * res_oplugin = nullptr; 611 612 if(!m_removed_rel_cols.empty()) { 613 unsigned res_rel_cnt = res_relations.size(); 614 for(unsigned i=0; i<res_rel_cnt; i++) { 615 if(res_relations[i]==0) { 616 continue; 617 } 618 relation_base * inner_rel = res_relations[i]; 619 if(!m_rel_projector) { 620 m_rel_projector = rmgr.mk_project_fn(*inner_rel, m_removed_rel_cols); 621 } 622 res_relations[i] = (*m_rel_projector)(*inner_rel); 623 inner_rel->deallocate(); 624 if(!res_oplugin) { 625 res_oplugin = &res_relations[i]->get_plugin(); 626 } 627 } 628 } 629 630 if(!res_oplugin) { 631 res_oplugin = &r.m_other_plugin; 632 } 633 634 //TODO: Maybe we might want to specify a particular relation kind, instead of just null_family_id. 635 //It would however need to be somehow inferred for the new signature. 636 637 finite_product_relation * res = alloc(finite_product_relation, r.get_plugin(), get_result_signature(), 638 m_res_table_columns.data(), res_table->get_plugin(), *res_oplugin, null_family_id); 639 640 res->init(*res_table, res_relations, false); 641 642 if(!shared_res_table) { 643 const_cast<table_base *>(res_table)->deallocate(); 644 } 645 646 return res; 647 } 648 }; 649 mk_project_fn(const relation_base & rb,unsigned col_cnt,const unsigned * removed_cols)650 relation_transformer_fn * finite_product_relation_plugin::mk_project_fn(const relation_base & rb, unsigned col_cnt, 651 const unsigned * removed_cols) { 652 if(&rb.get_plugin()!=this) { 653 return nullptr; 654 } 655 return alloc(project_fn, get(rb), col_cnt, removed_cols); 656 } 657 658 659 660 class finite_product_relation_plugin::rename_fn : public convenient_relation_rename_fn { 661 scoped_ptr<table_transformer_fn> m_table_renamer; 662 scoped_ptr<relation_transformer_fn> m_rel_renamer; 663 bool m_rel_identity; 664 665 unsigned_vector m_rel_permutation; 666 667 //determines which columns of the result are table columns and which are in the inner relation 668 bool_vector m_res_table_columns; 669 public: rename_fn(const finite_product_relation & r,unsigned cycle_len,const unsigned * permutation_cycle)670 rename_fn(const finite_product_relation & r, unsigned cycle_len, const unsigned * permutation_cycle) 671 : convenient_relation_rename_fn(r.get_signature(), cycle_len, permutation_cycle) { 672 SASSERT(cycle_len>1); 673 674 unsigned sig_sz = r.get_signature().size(); 675 unsigned_vector permutation; 676 add_sequence(0, sig_sz, permutation); 677 permutate_by_cycle(permutation, cycle_len, permutation_cycle); 678 679 unsigned_vector table_permutation; 680 681 bool table_identity = true; 682 m_rel_identity = true; 683 for(unsigned new_i=0; new_i<sig_sz; new_i++) { 684 unsigned idx = permutation[new_i]; 685 bool is_orig_table = r.is_table_column(idx); 686 m_res_table_columns.push_back(is_orig_table); 687 } 688 collect_sub_permutation(permutation, r.m_sig2table, table_permutation, table_identity); 689 table_permutation.push_back(table_permutation.size()); //the functional column stays where it is 690 collect_sub_permutation(permutation, r.m_sig2other, m_rel_permutation, m_rel_identity); 691 692 if(!table_identity) { 693 m_table_renamer = r.get_manager().mk_permutation_rename_fn(r.get_table(), table_permutation); 694 } 695 696 } 697 operator ()(const relation_base & rb)698 relation_base * operator()(const relation_base & rb) override { 699 const finite_product_relation & r = get(rb); 700 const table_base & rtable = r.get_table(); 701 702 r.garbage_collect(false); 703 relation_vector res_relations; 704 unsigned orig_rel_cnt = r.m_others.size(); 705 for(unsigned i=0; i<orig_rel_cnt; i++) { 706 relation_base * orig_rel = r.m_others[i]; 707 res_relations.push_back(orig_rel ? orig_rel->clone() : nullptr); 708 } 709 710 if(!m_rel_identity) { 711 unsigned res_rel_cnt = res_relations.size(); 712 for(unsigned i=0; i<res_rel_cnt; i++) { 713 if(res_relations[i]==0) { 714 continue; 715 } 716 scoped_rel<relation_base> inner_rel = res_relations[i]; 717 if(!m_rel_renamer) { 718 m_rel_renamer = r.get_manager().mk_permutation_rename_fn(*inner_rel, m_rel_permutation); 719 } 720 721 res_relations[i] = (*m_rel_renamer)(*inner_rel); 722 } 723 } 724 scoped_rel<table_base> res_table_scoped; 725 const table_base * res_table = &rtable; 726 727 if(m_table_renamer) { 728 res_table_scoped = (*m_table_renamer)(*res_table); 729 res_table = res_table_scoped.get(); 730 } 731 732 //TODO: Maybe we might want to specify a particular relation kind, instead of just null_family_id. 733 //It would however need to be somehow inferred for the new signature. 734 735 finite_product_relation * res = alloc(finite_product_relation, r.get_plugin(), get_result_signature(), 736 m_res_table_columns.data(), res_table->get_plugin(), r.m_other_plugin, null_family_id); 737 738 res->init(*res_table, res_relations, false); 739 740 return res; 741 } 742 }; 743 mk_rename_fn(const relation_base & rb,unsigned permutation_cycle_len,const unsigned * permutation_cycle)744 relation_transformer_fn * finite_product_relation_plugin::mk_rename_fn(const relation_base & rb, 745 unsigned permutation_cycle_len, const unsigned * permutation_cycle) { 746 747 if(&rb.get_plugin()!=this) { 748 return nullptr; 749 } 750 const finite_product_relation & r = get(rb); 751 return alloc(rename_fn, r, permutation_cycle_len, permutation_cycle); 752 } 753 754 755 class finite_product_relation_plugin::union_fn : public relation_union_fn { 756 bool m_use_delta; 757 unsigned_vector m_data_cols;//non-functional columns in the product-relation table (useful for creating operations) 758 scoped_ptr<table_join_fn> m_common_join; //result of the join contains (data columns), tgt_rel_idx, src_rel_idx 759 scoped_ptr<relation_union_fn> m_rel_union; 760 scoped_ptr<table_union_fn> m_table_union; 761 scoped_ptr<table_intersection_filter_fn> m_remove_overlaps; 762 scoped_ptr<table_transformer_fn> m_remove_src_column_from_overlap; 763 764 //this one is populated only if we're doing union with delta 765 scoped_ptr<relation_union_fn> m_delta_merging_union; 766 767 scoped_ptr<table_join_fn> m_overlap_delta_table_builder; 768 public: union_fn(const finite_product_relation & tgt,bool use_delta)769 union_fn(const finite_product_relation & tgt, bool use_delta) : m_use_delta(use_delta) {} 770 get_inner_rel_union_op(relation_base & r)771 relation_union_fn & get_inner_rel_union_op(relation_base & r) { 772 if(!m_rel_union) { 773 m_rel_union = r.get_manager().mk_union_fn(r, r, m_use_delta ? &r : nullptr); 774 } 775 return *m_rel_union; 776 } 777 778 class union_mapper : public table_row_mutator_fn { 779 union_fn & m_parent; 780 finite_product_relation & m_tgt; 781 const finite_product_relation & m_src; 782 table_base * m_delta_indexes; //table with signature (updated tgt rel index, delta_index in m_delta_rels) 783 relation_vector * m_delta_rels; 784 table_fact m_di_fact; //auxiliary fact for inserting into \c m_delta_indexes 785 public: 786 /** 787 If \c delta_indexes is 0, it means we are not collecting indexes. 788 */ union_mapper(union_fn & parent,finite_product_relation & tgt,const finite_product_relation & src,table_base * delta_indexes,relation_vector * delta_rels)789 union_mapper(union_fn & parent, finite_product_relation & tgt, const finite_product_relation & src, 790 table_base * delta_indexes, relation_vector * delta_rels) 791 : m_parent(parent), 792 m_tgt(tgt), 793 m_src(src), 794 m_delta_indexes(delta_indexes), 795 m_delta_rels(delta_rels) {} 796 ~union_mapper()797 ~union_mapper() override {} 798 operator ()(table_element * func_columns)799 bool operator()(table_element * func_columns) override { 800 relation_base & otgt_orig = m_tgt.get_inner_rel(func_columns[0]); 801 const relation_base & osrc = m_src.get_inner_rel(func_columns[1]); 802 803 relation_base * otgt = otgt_orig.clone(); 804 unsigned new_tgt_idx = m_tgt.get_next_rel_idx(); 805 m_tgt.set_inner_rel(new_tgt_idx, otgt); 806 if(m_delta_indexes) { 807 relation_base * odelta = otgt->get_plugin().mk_empty(otgt->get_signature()); 808 m_parent.get_inner_rel_union_op(*otgt)(*otgt, osrc, odelta); 809 810 unsigned delta_idx = m_delta_rels->size(); 811 m_delta_rels->push_back(odelta); 812 m_di_fact.reset(); 813 m_di_fact.push_back(new_tgt_idx); 814 m_di_fact.push_back(delta_idx); 815 m_delta_indexes->add_fact(m_di_fact); 816 } 817 else { 818 m_parent.get_inner_rel_union_op(*otgt)(*otgt, osrc); 819 } 820 821 func_columns[0]=new_tgt_idx; 822 return true; 823 } 824 }; 825 826 /** 827 Makes a table whose last column has indexes to relations in \c src into a table 828 with indexes to relation \c tgt. 829 */ 830 class src_copying_mapper : public table_row_mutator_fn { 831 finite_product_relation & m_tgt; 832 const finite_product_relation & m_src; 833 public: 834 /** 835 If \c delta_indexes is 0, it means we are not collecting indexes. 836 */ src_copying_mapper(finite_product_relation & tgt,const finite_product_relation & src)837 src_copying_mapper(finite_product_relation & tgt, const finite_product_relation & src) 838 : m_tgt(tgt), m_src(src) {} 839 operator ()(table_element * func_columns)840 bool operator()(table_element * func_columns) override { 841 const relation_base & osrc = m_src.get_inner_rel(func_columns[0]); 842 unsigned new_tgt_idx = m_tgt.get_next_rel_idx(); 843 m_tgt.set_inner_rel(new_tgt_idx, osrc.clone()); 844 func_columns[0]=new_tgt_idx; 845 return true; 846 } 847 }; 848 operator ()(relation_base & tgtb,const relation_base & srcb,relation_base * deltab)849 void operator()(relation_base & tgtb, const relation_base & srcb, relation_base * deltab) override { 850 finite_product_relation & tgt = get(tgtb); 851 const finite_product_relation & src0 = get(srcb); 852 finite_product_relation * delta = get(deltab); 853 854 relation_manager & rmgr = tgt.get_manager(); 855 856 scoped_rel<finite_product_relation> src_aux_copy; //copy of src in case its specification needs to be modified 857 858 if(!vectors_equal(tgt.m_table2sig, src0.m_table2sig) 859 || (delta && !vectors_equal(tgt.m_table2sig, delta->m_table2sig)) ) { 860 src_aux_copy = src0.clone(); 861 ptr_vector<finite_product_relation> orig_rels; 862 orig_rels.push_back(src_aux_copy.get()); 863 orig_rels.push_back(&tgt); 864 if(delta) { 865 orig_rels.push_back(delta); 866 } 867 if(!finite_product_relation::try_unify_specifications(orig_rels)) { 868 throw default_exception("finite_product_relation union: cannot convert relations to common specification"); 869 } 870 } 871 872 const finite_product_relation & src = src_aux_copy ? *src_aux_copy : src0; 873 874 table_plugin & tplugin = tgt.get_table_plugin(); 875 876 if(!m_common_join) { 877 unsigned data_cols_cnt = tgt.m_table_sig.size()-1; 878 for(unsigned i=0; i<data_cols_cnt; i++) { 879 m_data_cols.push_back(i); 880 } 881 m_common_join = rmgr.mk_join_project_fn(tgt.get_table(), tgt.get_table(), m_data_cols, m_data_cols, 882 m_data_cols); 883 } 884 885 886 scoped_rel<table_base> table_overlap = (*m_common_join)(tgt.get_table(), src.get_table()); 887 888 scoped_rel<table_base> delta_indexes; 889 relation_vector delta_rels; 890 if(m_use_delta) { 891 table_signature di_sig; 892 di_sig.push_back(finite_product_relation::s_rel_idx_sort); 893 di_sig.push_back(finite_product_relation::s_rel_idx_sort); 894 di_sig.set_functional_columns(1); 895 delta_indexes = tplugin.mk_empty(di_sig); 896 } 897 898 { 899 union_mapper * umapper = alloc(union_mapper, *this, tgt, src, delta_indexes.get(), &delta_rels); 900 scoped_ptr<table_mutator_fn> mapping_fn = rmgr.mk_map_fn(*table_overlap, umapper); 901 (*mapping_fn)(*table_overlap); 902 } 903 904 if(!m_remove_src_column_from_overlap) { 905 unsigned removed_cols[] = { table_overlap->get_signature().size()-1 }; 906 m_remove_src_column_from_overlap = rmgr.mk_project_fn(*table_overlap, 1, removed_cols); 907 } 908 //transform table_overlap into the signature of tgt.get_table(), so that the functional 909 //column contains indexes of the united relations 910 scoped_rel<table_base> regular_overlap = (*m_remove_src_column_from_overlap)(*table_overlap); 911 912 913 if(!m_remove_overlaps) { 914 m_remove_overlaps = rmgr.mk_filter_by_negation_fn(tgt.get_table(), *regular_overlap, m_data_cols, 915 m_data_cols); 916 } 917 918 //in tgt keep only the rows that are in tgt only 919 (*m_remove_overlaps)(tgt.get_table(), *regular_overlap); 920 921 //add rows in which tgt and src overlapped 922 if(!m_table_union) { 923 m_table_union = rmgr.mk_union_fn(tgt.get_table(), tgt.get_table()); 924 } 925 (*m_table_union)(tgt.get_table(), *regular_overlap); 926 927 scoped_rel<table_base> src_only = src.get_table().clone(); 928 (*m_remove_overlaps)(*src_only, *regular_overlap); 929 930 scoped_rel<table_base> src_only2; //a copy of src_only for use in building the delta 931 if(m_use_delta) { 932 src_only2 = src_only->clone(); 933 } 934 935 { 936 src_copying_mapper * cpmapper = alloc(src_copying_mapper, tgt, src); 937 scoped_ptr<table_mutator_fn> mapping_fn = rmgr.mk_map_fn(*src_only, cpmapper); 938 (*mapping_fn)(*src_only); 939 } 940 941 //add rows that were only in src 942 (*m_table_union)(tgt.get_table(), *src_only); 943 944 if(m_use_delta) { 945 bool extending_delta = !delta->empty(); 946 //current delta, we will add it to the deltab argument later if it was not given to us empty 947 finite_product_relation * cdelta; 948 if(extending_delta) { 949 cdelta = delta->get_plugin().mk_empty(*delta); 950 } 951 else { 952 cdelta = delta; 953 } 954 955 if(!m_overlap_delta_table_builder) { 956 unsigned table_fn_col = regular_overlap->get_signature().size()-1; 957 unsigned first_col = 0; 958 unsigned removed_cols[] = { table_fn_col, table_fn_col+1 }; 959 m_overlap_delta_table_builder = rmgr.mk_join_project_fn(*regular_overlap, *delta_indexes, 1, 960 &table_fn_col, &first_col, 2, removed_cols); 961 } 962 963 scoped_rel<table_base> overlap_delta_table = 964 (*m_overlap_delta_table_builder)(*regular_overlap, *delta_indexes); 965 966 cdelta->init(*overlap_delta_table, delta_rels, true); 967 968 { 969 src_copying_mapper * cpmapper = alloc(src_copying_mapper, *cdelta, src); 970 scoped_ptr<table_mutator_fn> mapping_fn = rmgr.mk_map_fn(*src_only2, cpmapper); 971 (*mapping_fn)(*src_only2); 972 } 973 974 //add rows that were only in src 975 (*m_table_union)(cdelta->get_table(), *src_only2); 976 977 if(extending_delta) { 978 if(!m_delta_merging_union) { 979 m_delta_merging_union = rmgr.mk_union_fn(*delta, *cdelta); 980 } 981 (*m_delta_merging_union)(*delta, *cdelta); 982 cdelta->deallocate(); 983 } 984 } 985 } 986 }; 987 988 #if 0 989 /** 990 Union operation taking advantage of the fact that the inner relation of all the arguments 991 is a singleton relation. 992 */ 993 class finite_product_relation_plugin::inner_singleton_union_fn : public relation_union_fn { 994 995 class offset_row_mapper : public table_row_mutator_fn { 996 public: 997 unsigned m_ofs; 998 virtual bool operator()(table_element * func_columns) { 999 func_columns[0] += m_ofs; 1000 return true; 1001 } 1002 }; 1003 1004 // [Leo]: gcc complained about the following class. 1005 // It does not have a constructor and uses a reference 1006 1007 class inner_relation_copier : public table_row_mutator_fn { 1008 finite_product_relation & m_tgt; 1009 const finite_product_relation & m_src; 1010 finite_product_relation * m_delta; 1011 unsigned m_tgt_ofs; 1012 unsigned m_delta_ofs; 1013 public: 1014 virtual bool operator()(table_element * func_columns) { 1015 unsigned src_idx = static_cast<unsigned>(func_columns[0]); 1016 unsigned tgt_idx = src_idx + m_tgt_ofs; 1017 unsigned delta_idx = m_delta ? (src_idx + m_delta_ofs) : 0; 1018 SASSERT(!m_delta || m_tgt.m_others[tgt_idx]==m_delta->m_others[delta_idx]); 1019 SASSERT(m_tgt.m_others[tgt_idx]==0 || m_tgt.m_others[tgt_idx]==m_src.m_others[src_idx]); 1020 if(m_tgt.m_others[tgt_idx]==0) { 1021 m_tgt.m_others[tgt_idx] = m_src.m_others[src_idx]->clone(); 1022 if(m_delta) { 1023 m_delta->m_others[delta_idx] = m_src.m_others[src_idx]->clone(); 1024 } 1025 } 1026 return true; 1027 } 1028 }; 1029 1030 scoped_ptr<table_union_fn> m_t_union_fun; 1031 offset_row_mapper * m_offset_mapper_obj; //initialized together with m_offset_mapper_fun, and deallocated by it 1032 scoped_ptr<table_mutator_fn> m_offset_mapper_fun; 1033 1034 1035 1036 public: 1037 virtual void operator()(relation_base & tgtb, const relation_base & srcb, relation_base * deltab) { 1038 finite_product_relation & tgt = get(tgtb); 1039 const finite_product_relation & src = get(srcb); 1040 finite_product_relation * delta = get(deltab); 1041 1042 finite_product_relation_plugin & plugin = tgt.get_plugin(); 1043 relation_manager & rmgr = plugin.get_manager(); 1044 1045 //we want only non-empty inner relations to remain 1046 tgt.garbage_collect(true); 1047 src.garbage_collect(true); 1048 1049 table_base & tgt_table = tgt.get_table(); 1050 const table_base & src_table = src.get_table(); 1051 1052 scoped_rel<table_base> offsetted_src = src_table.clone(); 1053 1054 if(!m_offset_mapper_fun) { 1055 m_offset_mapper_obj = alloc(offset_row_mapper); 1056 m_offset_mapper_fun = rmgr.mk_map_fn(*offsetted_src, m_offset_mapper_obj); 1057 } 1058 unsigned src_rel_offset = tgt.m_others.size(); 1059 m_offset_mapper_obj->m_ofs = src_rel_offset; 1060 1061 (*m_offset_mapper_fun)(*offsetted_src); 1062 1063 //if we need to generate a delta, we get collect it into an empty relation and then union 1064 //it with the delta passed in as argument. 1065 scoped_rel<finite_product_relation> loc_delta = delta ? get(plugin.mk_empty(*delta)) : 0; 1066 //even if we don't need to generate the delta for the caller, we still want to have a delta 1067 //table to know which relations to copy. 1068 scoped_rel<table_base> loc_delta_table_scoped; 1069 if(!loc_delta) { 1070 loc_delta_table_scoped = tgt_table.get_plugin().mk_empty(tgt_table); 1071 } 1072 table_base * loc_delta_table = loc_delta ? &loc_delta->get_table() : loc_delta_table_scoped.get(); 1073 1074 if(!m_t_union_fun) { 1075 m_t_union_fun = rmgr.mk_union_fn(tgt_table, *offsetted_src, loc_delta_table); 1076 } 1077 (*m_t_union_fun)(tgt_table, *offsetted_src, loc_delta_table); 1078 1079 1080 //TODO: copy the relations into tgt and (possibly) delta using inner_relation_copier 1081 //TODO: unite the local delta with the delta passed in as an argument 1082 NOT_IMPLEMENTED_YET(); 1083 } 1084 }; 1085 #endif 1086 1087 class finite_product_relation_plugin::converting_union_fn : public relation_union_fn { 1088 scoped_ptr<relation_union_fn> m_tr_union_fun; 1089 public: operator ()(relation_base & tgtb,const relation_base & srcb,relation_base * deltab)1090 void operator()(relation_base & tgtb, const relation_base & srcb, relation_base * deltab) override { 1091 SASSERT(srcb.get_plugin().is_finite_product_relation()); 1092 const finite_product_relation & src = get(srcb); 1093 finite_product_relation_plugin & plugin = src.get_plugin(); 1094 scoped_rel<table_relation> tr_src = plugin.to_table_relation(src); 1095 if(!m_tr_union_fun) { 1096 m_tr_union_fun = plugin.get_manager().mk_union_fn(tgtb, *tr_src, deltab); 1097 SASSERT(m_tr_union_fun); 1098 } 1099 (*m_tr_union_fun)(tgtb, *tr_src, deltab); 1100 } 1101 }; 1102 mk_union_fn(const relation_base & tgtb,const relation_base & srcb,const relation_base * deltab)1103 relation_union_fn * finite_product_relation_plugin::mk_union_fn(const relation_base & tgtb, const relation_base & srcb, 1104 const relation_base * deltab) { 1105 if(&srcb.get_plugin()!=this) { 1106 return nullptr; 1107 } 1108 const finite_product_relation & src = get(srcb); 1109 if(&tgtb.get_plugin()!=this || (deltab && &deltab->get_plugin()!=this) ) { 1110 if(can_convert_to_table_relation(src)) { 1111 return alloc(converting_union_fn); 1112 } 1113 return nullptr; 1114 } 1115 1116 const finite_product_relation * delta = get(deltab); 1117 1118 return alloc(union_fn, get(tgtb), delta!=nullptr); 1119 } 1120 1121 1122 class finite_product_relation_plugin::filter_identical_fn : public relation_mutator_fn { 1123 //the table and relation columns that should be identical 1124 //the column numbering is local to the table or inner relation 1125 unsigned_vector m_table_cols; 1126 unsigned_vector m_rel_cols; 1127 1128 scoped_ptr<table_mutator_fn> m_table_filter; 1129 scoped_ptr<relation_mutator_fn> m_rel_filter; 1130 scoped_ptr<relation_mutator_fn> m_tr_filter; 1131 public: filter_identical_fn(const finite_product_relation & r,unsigned col_cnt,const unsigned * identical_cols)1132 filter_identical_fn(const finite_product_relation & r, unsigned col_cnt, const unsigned * identical_cols) 1133 : m_table_filter(nullptr), m_rel_filter(nullptr), m_tr_filter(nullptr) { 1134 finite_product_relation_plugin & plugin = r.get_plugin(); 1135 for(unsigned i=0; i<col_cnt; i++) { 1136 unsigned col = identical_cols[i]; 1137 if(r.is_table_column(col)) { 1138 m_table_cols.push_back(r.m_sig2table[col]); 1139 } 1140 else { 1141 m_rel_cols.push_back(r.m_sig2other[col]); 1142 } 1143 } 1144 if(m_table_cols.size()>1) { 1145 m_table_filter = r.get_manager().mk_filter_identical_fn(r.get_table(), m_table_cols.size(), 1146 m_table_cols.data()); 1147 SASSERT(m_table_filter); 1148 } 1149 if(!m_table_cols.empty() && !m_rel_cols.empty()) { 1150 unsigned tr_filter_table_cols[] = { m_table_cols[0] }; 1151 unsigned tr_filter_rel_cols[] = { m_rel_cols[0] }; 1152 m_tr_filter = plugin.mk_filter_identical_pairs(r, 1, tr_filter_table_cols, tr_filter_rel_cols); 1153 SASSERT(m_tr_filter); 1154 } 1155 } 1156 ensure_rel_filter(const relation_base & orel)1157 void ensure_rel_filter(const relation_base & orel) { 1158 SASSERT(m_rel_cols.size()>1); 1159 if(m_rel_filter) { 1160 return; 1161 } 1162 m_rel_filter = orel.get_manager().mk_filter_identical_fn(orel, m_rel_cols.size(), m_rel_cols.data()); 1163 SASSERT(m_rel_filter); 1164 } 1165 operator ()(relation_base & rb)1166 void operator()(relation_base & rb) override { 1167 finite_product_relation & r = get(rb); 1168 1169 if(m_table_cols.size()>1) { 1170 (*m_table_filter)(r.get_table()); 1171 } 1172 1173 if(m_rel_cols.size()>1) { 1174 r.garbage_collect(true); 1175 unsigned rel_cnt = r.m_others.size(); 1176 for(unsigned rel_idx=0; rel_idx<rel_cnt; rel_idx++) { 1177 if(r.m_others[rel_idx]==0) { 1178 continue; 1179 } 1180 ensure_rel_filter(*r.m_others[rel_idx]); 1181 (*m_rel_filter)(*r.m_others[rel_idx]); 1182 } 1183 } 1184 1185 if(!m_table_cols.empty() && !m_rel_cols.empty()) { 1186 (*m_tr_filter)(r); 1187 } 1188 } 1189 }; 1190 mk_filter_identical_fn(const relation_base & rb,unsigned col_cnt,const unsigned * identical_cols)1191 relation_mutator_fn * finite_product_relation_plugin::mk_filter_identical_fn(const relation_base & rb, 1192 unsigned col_cnt, const unsigned * identical_cols) { 1193 if(&rb.get_plugin()!=this) { 1194 return nullptr; 1195 } 1196 return alloc(filter_identical_fn, get(rb), col_cnt, identical_cols); 1197 } 1198 1199 class finite_product_relation_plugin::filter_equal_fn : public relation_mutator_fn { 1200 scoped_ptr<table_mutator_fn> m_table_filter; 1201 scoped_ptr<relation_mutator_fn> m_rel_filter; 1202 unsigned m_col; 1203 app_ref m_value; 1204 public: filter_equal_fn(const finite_product_relation & r,const relation_element & value,unsigned col)1205 filter_equal_fn(const finite_product_relation & r, const relation_element & value, unsigned col) 1206 : m_col(col), m_value(value, r.get_context().get_manager()) { 1207 if(r.is_table_column(col)) { 1208 table_element tval; 1209 r.get_manager().relation_to_table(r.get_signature()[col], value, tval); 1210 m_table_filter = r.get_manager().mk_filter_equal_fn(r.get_table(), tval, r.m_sig2table[col]); 1211 } 1212 } 1213 operator ()(relation_base & rb)1214 void operator()(relation_base & rb) override { 1215 finite_product_relation & r = get(rb); 1216 1217 if(m_table_filter) { 1218 (*m_table_filter)(r.get_table()); 1219 return; 1220 } 1221 r.garbage_collect(false); 1222 relation_vector & inner_rels = r.m_others; 1223 unsigned rel_cnt = inner_rels.size(); 1224 for(unsigned i=0; i<rel_cnt; i++) { 1225 if(inner_rels[i]==0) { 1226 continue; 1227 } 1228 if(!m_rel_filter) { 1229 m_rel_filter = r.get_manager().mk_filter_equal_fn(*inner_rels[i], m_value, r.m_sig2other[m_col]); 1230 } 1231 (*m_rel_filter)(*inner_rels[i]); 1232 } 1233 } 1234 }; 1235 1236 mk_filter_equal_fn(const relation_base & rb,const relation_element & value,unsigned col)1237 relation_mutator_fn * finite_product_relation_plugin::mk_filter_equal_fn(const relation_base & rb, 1238 const relation_element & value, unsigned col) { 1239 if(&rb.get_plugin()!=this) { 1240 return nullptr; 1241 } 1242 return alloc(filter_equal_fn, get(rb), value, col); 1243 } 1244 1245 1246 class finite_product_relation_plugin::filter_interpreted_fn : public relation_mutator_fn { 1247 ast_manager & m_manager; 1248 var_subst & m_subst; 1249 1250 scoped_ptr<table_mutator_fn> m_table_filter; 1251 scoped_ptr<relation_mutator_fn> m_rel_filter; 1252 app_ref m_cond; 1253 1254 idx_set m_table_cond_columns; 1255 idx_set m_rel_cond_columns; 1256 1257 //like m_table_cond_columns and m_rel_cond_columns, only the indexes are local to the 1258 //table/relation, not to the signature of the whole relation 1259 idx_set m_table_local_cond_columns; 1260 idx_set m_rel_local_cond_columns; 1261 1262 /** 1263 If equal to 0, it means the interpreted condition uses all table columns. Then the original 1264 table is used instead of the result of the projection. 1265 */ 1266 scoped_ptr<table_transformer_fn> m_table_cond_columns_project; 1267 /** 1268 \brief Column indexes of the global relations to which correspond the data columns in the table 1269 that is result of applying the \c m_table_cond_columns_project functor. 1270 */ 1271 unsigned_vector m_global_origins_of_projected_columns; 1272 1273 scoped_ptr<table_join_fn> m_assembling_join_project; 1274 1275 1276 /** 1277 \brief Renaming that transforms the variable numbers pointing to the global relation into 1278 variables that point to the inner relation variables. 1279 1280 The elements that do not correspond to columns of the inner relation (but rather to the table 1281 columns) is modified in \c operator() when evaluating the condition for all the relevant 1282 combinations of table values. 1283 */ 1284 expr_ref_vector m_renaming_for_inner_rel; 1285 public: filter_interpreted_fn(const finite_product_relation & r,app * condition)1286 filter_interpreted_fn(const finite_product_relation & r, app * condition) 1287 : m_manager(r.get_context().get_manager()), 1288 m_subst(r.get_context().get_var_subst()), 1289 m_cond(condition, m_manager), 1290 m_renaming_for_inner_rel(m_manager) { 1291 relation_manager & rmgr = r.get_manager(); 1292 1293 rule_manager& rm = r.get_context().get_rule_manager(); 1294 idx_set& cond_columns = rm.collect_vars(m_cond); 1295 1296 unsigned sig_sz = r.get_signature().size(); 1297 for(unsigned i=0; i<sig_sz; i++) { 1298 if(r.is_table_column(i)) { 1299 m_table_cond_columns.insert(i); 1300 } 1301 else { 1302 m_rel_cond_columns.insert(i); 1303 } 1304 } 1305 set_intersection(m_table_cond_columns, cond_columns); 1306 set_intersection(m_rel_cond_columns, cond_columns); 1307 transform_set(r.m_sig2table, m_table_cond_columns, m_table_local_cond_columns); 1308 transform_set(r.m_sig2other, m_rel_cond_columns, m_rel_local_cond_columns); 1309 1310 if(m_rel_cond_columns.empty()) { 1311 expr_ref_vector renaming(m_manager); 1312 get_renaming_args(r.m_sig2table, r.get_signature(), renaming); 1313 expr_ref table_cond = m_subst(condition, renaming.size(), renaming.data()); 1314 m_table_filter = rmgr.mk_filter_interpreted_fn(r.get_table(), to_app(table_cond)); 1315 } 1316 else { 1317 get_renaming_args(r.m_sig2other, r.get_signature(), m_renaming_for_inner_rel); 1318 1319 if(!m_table_cond_columns.empty()) { 1320 //We will keep the table variables that appear in the condition together 1321 //with the index column and then iterate through the tuples, evaluating 1322 //the rest of the condition on the inner relations. 1323 unsigned_vector removed_cols; 1324 unsigned table_data_col_cnt = r.m_table_sig.size()-1; 1325 for(unsigned i=0; i<table_data_col_cnt; i++) { 1326 if(m_table_local_cond_columns.contains(i)) { 1327 m_global_origins_of_projected_columns.push_back(r.m_table2sig[i]); 1328 } 1329 else { 1330 removed_cols.push_back(i); 1331 } 1332 } 1333 if(!removed_cols.empty()) { 1334 m_table_cond_columns_project = rmgr.mk_project_fn(r.get_table(), removed_cols); 1335 } 1336 } 1337 } 1338 } 1339 operator ()(relation_base & rb)1340 void operator()(relation_base & rb) override { 1341 finite_product_relation & r = get(rb); 1342 table_base & rtable = r.get_table(); 1343 table_plugin & tplugin = r.get_table_plugin(); 1344 const relation_signature & osig = r.get_signature(); 1345 relation_manager & rmgr = r.get_manager(); 1346 unsigned rsig_sz = r.get_signature().size(); 1347 1348 if(m_rel_cond_columns.empty()) { 1349 SASSERT(m_table_filter); 1350 (*m_table_filter)(rtable); 1351 return; 1352 } 1353 if(m_table_cond_columns.empty()) { 1354 r.garbage_collect(false); 1355 unsigned rel_cnt = r.m_others.size(); 1356 for(unsigned i=0; i<rel_cnt; i++) { 1357 relation_base * inner = r.m_others[i]; 1358 if(inner==nullptr) { 1359 continue; 1360 } 1361 if(!m_rel_filter) { 1362 expr_ref inner_cond = m_subst(m_cond, m_renaming_for_inner_rel.size(), m_renaming_for_inner_rel.data()); 1363 m_rel_filter = rmgr.mk_filter_interpreted_fn(*inner, to_app(inner_cond)); 1364 } 1365 (*m_rel_filter)(*inner); 1366 } 1367 return; 1368 } 1369 1370 //get table without the data columns on which we don't enforce identities 1371 //The relation index column may be non-functional. 1372 scoped_rel<table_base> tproj_scope; 1373 const table_base * tproj; 1374 if(m_table_cond_columns_project) { 1375 tproj_scope = (*m_table_cond_columns_project)(rtable); 1376 tproj = tproj_scope.get(); 1377 } 1378 else { 1379 tproj = &rtable; 1380 } 1381 unsigned projected_data_cols = tproj->get_signature().size()-1; 1382 SASSERT(m_table_cond_columns.num_elems()==projected_data_cols); 1383 1384 table_signature filtered_sig = tproj->get_signature(); 1385 filtered_sig.push_back(finite_product_relation::s_rel_idx_sort); 1386 filtered_sig.set_functional_columns(1); 1387 1388 relation_vector new_rels; 1389 1390 scoped_rel<table_base> filtered_table = tplugin.mk_empty(filtered_sig); 1391 table_fact f; 1392 unsigned renaming_ofs = m_renaming_for_inner_rel.size()-1; 1393 table_base::iterator pit = tproj->begin(); 1394 table_base::iterator pend = tproj->end(); 1395 for(; pit!=pend; ++pit) { 1396 pit->get_fact(f); 1397 unsigned old_rel_idx = static_cast<unsigned>(f.back()); 1398 const relation_base & old_rel = r.get_inner_rel(old_rel_idx); 1399 1400 //put the table values into the substitution 1401 for(unsigned i=0; i<projected_data_cols; i++) { 1402 unsigned orig_col_idx = m_global_origins_of_projected_columns[i]; 1403 relation_element r_el; 1404 rmgr.table_to_relation(osig[orig_col_idx], f[i], r_el); 1405 m_renaming_for_inner_rel.set(renaming_ofs-orig_col_idx, r_el); 1406 } 1407 1408 //create the condition with table values substituted in and relation values properly renamed 1409 expr_ref inner_cond(m_manager); 1410 inner_cond = m_subst(m_cond, m_renaming_for_inner_rel.size(), m_renaming_for_inner_rel.data()); 1411 th_rewriter rw(m_manager); 1412 rw(inner_cond); 1413 if (m_manager.is_false(inner_cond)) { 1414 continue; 1415 } 1416 1417 relation_base * new_rel = old_rel.clone(); 1418 1419 scoped_ptr<relation_mutator_fn> filter = rmgr.mk_filter_interpreted_fn(*new_rel, to_app(inner_cond)); 1420 if (!filter) 1421 throw default_exception("rules do not belong to supported finite domain fragment"); 1422 (*filter)(*new_rel); 1423 1424 if(new_rel->empty()) { 1425 new_rel->deallocate(); 1426 continue; 1427 } 1428 1429 unsigned new_rel_idx = new_rels.size(); 1430 new_rels.push_back(new_rel); 1431 f.push_back(new_rel_idx); 1432 filtered_table->add_fact(f); 1433 } 1434 1435 if(!m_assembling_join_project) { 1436 unsigned_vector table_cond_columns_vect; 1437 for(unsigned i=0; i<rsig_sz; i++) { 1438 if(m_table_local_cond_columns.contains(i)) { 1439 table_cond_columns_vect.push_back(i); 1440 } 1441 } 1442 1443 m_assembling_join_project = mk_assembler_of_filter_result(rtable, *filtered_table, 1444 table_cond_columns_vect); 1445 } 1446 1447 scoped_rel<table_base> new_table = (*m_assembling_join_project)(rtable, *filtered_table); 1448 r.reset(); 1449 r.init(*new_table, new_rels, true); 1450 } 1451 }; 1452 mk_filter_interpreted_fn(const relation_base & rb,app * condition)1453 relation_mutator_fn * finite_product_relation_plugin::mk_filter_interpreted_fn(const relation_base & rb, 1454 app * condition) { 1455 if(&rb.get_plugin()!=this) { 1456 return nullptr; 1457 } 1458 return alloc(filter_interpreted_fn, get(rb), condition); 1459 } 1460 1461 class finite_product_relation_plugin::negation_filter_fn : public relation_intersection_filter_fn { 1462 1463 unsigned_vector m_r_cols; 1464 unsigned_vector m_neg_cols; 1465 1466 scoped_ptr<table_intersection_filter_fn> m_table_neg_filter; 1467 scoped_ptr<table_join_fn> m_table_neg_complement_selector; 1468 scoped_ptr<relation_join_fn> m_neg_intersection_join; 1469 scoped_ptr<table_join_fn> m_table_intersection_join; 1470 scoped_ptr<table_union_fn> m_table_overlap_union; 1471 scoped_ptr<table_intersection_filter_fn> m_table_subtract; 1472 scoped_ptr<relation_intersection_filter_fn> m_inner_subtract; 1473 scoped_ptr<table_transformer_fn> m_overlap_table_last_column_remover; 1474 scoped_ptr<table_union_fn> m_r_table_union; 1475 1476 bool m_table_overlaps_only; 1477 1478 unsigned_vector m_r_shared_table_cols; 1479 unsigned_vector m_neg_shared_table_cols; 1480 1481 unsigned_vector m_r_shared_rel_cols; 1482 unsigned_vector m_neg_shared_rel_cols; 1483 public: negation_filter_fn(const finite_product_relation & r,const finite_product_relation & neg,unsigned joined_col_cnt,const unsigned * r_cols,const unsigned * neg_cols)1484 negation_filter_fn(const finite_product_relation & r, const finite_product_relation & neg, 1485 unsigned joined_col_cnt, const unsigned * r_cols, const unsigned * neg_cols) 1486 : m_r_cols(joined_col_cnt, r_cols), 1487 m_neg_cols(joined_col_cnt, neg_cols), 1488 m_table_overlaps_only(true) { 1489 const table_signature & tsig = r.m_table_sig; 1490 const table_base & rtable = r.get_table(); 1491 relation_manager & rmgr = r.get_manager(); 1492 1493 for(unsigned i=0; i<joined_col_cnt; i++) { 1494 if(r.is_table_column(r_cols[i]) && neg.is_table_column(neg_cols[i])) { 1495 m_r_shared_table_cols.push_back(r.m_sig2table[r_cols[i]]); 1496 m_neg_shared_table_cols.push_back(neg.m_sig2table[neg_cols[i]]); 1497 } 1498 else { 1499 m_table_overlaps_only = false; 1500 } 1501 } 1502 if(m_table_overlaps_only) { 1503 m_table_neg_filter = rmgr.mk_filter_by_negation_fn(rtable, neg.get_table(), 1504 m_r_shared_table_cols, m_neg_shared_table_cols); 1505 SASSERT(m_table_neg_filter); 1506 } 1507 else { 1508 unsigned_vector removed_cols; 1509 add_sequence(r.get_signature().size(), neg.get_signature().size(), removed_cols); 1510 m_neg_intersection_join = rmgr.mk_join_project_fn(r, neg, m_r_cols, m_neg_cols, removed_cols, false); 1511 SASSERT(m_neg_intersection_join); 1512 1513 unsigned_vector data_cols; 1514 add_sequence(0, tsig.size()-1, data_cols); 1515 removed_cols.reset(); 1516 //remove the second copy of table data columns 1517 add_sequence(tsig.size()-1, tsig.size()-1, removed_cols); 1518 m_table_intersection_join = rmgr.mk_join_project_fn(rtable, rtable, data_cols, data_cols, 1519 removed_cols); 1520 SASSERT(m_table_intersection_join); 1521 1522 m_table_subtract = rmgr.mk_filter_by_negation_fn(rtable, rtable, data_cols, data_cols); 1523 SASSERT(m_table_subtract); 1524 } 1525 } 1526 handle_only_tables_overlap_case(finite_product_relation & r,const finite_product_relation & neg)1527 void handle_only_tables_overlap_case(finite_product_relation & r, const finite_product_relation & neg) { 1528 SASSERT(m_table_overlaps_only); 1529 (*m_table_neg_filter)(r.get_table(), neg.get_table()); 1530 } 1531 1532 1533 class rel_subtractor : public table_row_mutator_fn { 1534 negation_filter_fn & m_parent; 1535 finite_product_relation & m_r; 1536 const finite_product_relation & m_inters; //intersection of the relation and the negated one 1537 public: rel_subtractor(negation_filter_fn & parent,finite_product_relation & r,const finite_product_relation & inters)1538 rel_subtractor(negation_filter_fn & parent, finite_product_relation & r, 1539 const finite_product_relation & inters) 1540 : m_parent(parent), m_r(r), m_inters(inters) {} 1541 operator ()(table_element * func_columns)1542 bool operator()(table_element * func_columns) override { 1543 relation_base * r_inner = m_r.get_inner_rel(func_columns[0]).clone(); 1544 const relation_base & inters_inner = m_inters.get_inner_rel(func_columns[1]); 1545 1546 if(!m_parent.m_inner_subtract) { 1547 unsigned_vector all_rel_cols; 1548 add_sequence(0, r_inner->get_signature().size() , all_rel_cols); 1549 m_parent.m_inner_subtract = m_r.get_manager().mk_filter_by_negation_fn(*r_inner, 1550 inters_inner, all_rel_cols, all_rel_cols); 1551 } 1552 (*m_parent.m_inner_subtract)(*r_inner, inters_inner); 1553 1554 unsigned new_rel_num = m_r.get_next_rel_idx(); 1555 m_r.set_inner_rel(new_rel_num, r_inner); 1556 func_columns[0]=new_rel_num; 1557 return true; 1558 } 1559 }; 1560 1561 operator ()(relation_base & rb,const relation_base & negb)1562 void operator()(relation_base & rb, const relation_base & negb) override { 1563 finite_product_relation & r = get(rb); 1564 const finite_product_relation & neg = get(negb); 1565 1566 if(m_table_overlaps_only) { 1567 handle_only_tables_overlap_case(r, neg); 1568 return; 1569 } 1570 1571 scoped_rel<finite_product_relation> intersection = get((*m_neg_intersection_join)(r, neg)); 1572 1573 DEBUG_CODE( 1574 finite_product_relation_plugin & plugin = r.get_plugin(); 1575 SASSERT(&intersection->get_plugin()==&plugin); //the result of join is also finite product 1576 SASSERT(r.get_signature()==intersection->get_signature());); 1577 table_base & r_table = r.get_table(); 1578 table_plugin & tplugin = r_table.get_plugin(); 1579 relation_manager & rmgr = r.get_manager(); 1580 1581 //we need to do this before we perform the \c m_table_subtract 1582 //the sigrature of the \c table_overlap0 relation is 1583 //(data_columns)(original rel idx)(subtracted rel idx) 1584 scoped_rel<table_base> table_overlap0 = (*m_table_intersection_join)(r_table, 1585 intersection->get_table()); 1586 1587 //the rows that don't appear in the table of the intersection are safe to stay 1588 (*m_table_subtract)(r_table, intersection->get_table()); 1589 1590 //now we will examine the rows that do appear in the intersection 1591 1592 //There are no functional columns in the \c table_overlap0 relation (because of 1593 //the project we did). We need to make both rel idx columns functional. 1594 //We do not lose any rows, since the data columns by themselves are unique. 1595 1596 table_signature table_overlap_sig(table_overlap0->get_signature()); 1597 table_overlap_sig.set_functional_columns(2); 1598 scoped_rel<table_base> table_overlap = tplugin.mk_empty(table_overlap_sig); 1599 1600 if(!m_table_overlap_union) { 1601 m_table_overlap_union = rmgr.mk_union_fn(*table_overlap, *table_overlap0); 1602 SASSERT(m_table_overlap_union); 1603 } 1604 (*m_table_overlap_union)(*table_overlap, *table_overlap0); 1605 1606 { 1607 rel_subtractor * mutator = alloc(rel_subtractor, *this, r, *intersection); 1608 scoped_ptr<table_mutator_fn> mapper = rmgr.mk_map_fn(*table_overlap, mutator); 1609 (*mapper)(*table_overlap); 1610 } 1611 1612 if(!m_overlap_table_last_column_remover) { 1613 unsigned removed_col = table_overlap->get_signature().size()-1; 1614 m_overlap_table_last_column_remover = rmgr.mk_project_fn(*table_overlap, 1, &removed_col); 1615 } 1616 scoped_rel<table_base> final_overlapping_rows_table = 1617 (*m_overlap_table_last_column_remover)(*table_overlap); 1618 1619 if(!m_r_table_union) { 1620 m_r_table_union = rmgr.mk_union_fn(r_table, *final_overlapping_rows_table); 1621 } 1622 1623 (*m_r_table_union)(r_table, *final_overlapping_rows_table); 1624 } 1625 }; 1626 mk_filter_by_negation_fn(const relation_base & rb,const relation_base & negb,unsigned joined_col_cnt,const unsigned * r_cols,const unsigned * negated_cols)1627 relation_intersection_filter_fn * finite_product_relation_plugin::mk_filter_by_negation_fn(const relation_base & rb, 1628 const relation_base & negb, unsigned joined_col_cnt, 1629 const unsigned * r_cols, const unsigned * negated_cols) { 1630 if(&rb.get_plugin()!=this || &negb.get_plugin()!=this) { 1631 return nullptr; 1632 } 1633 1634 return alloc(negation_filter_fn, get(rb), get(negb), joined_col_cnt, r_cols, negated_cols); 1635 } 1636 1637 1638 class finite_product_relation_plugin::filter_identical_pairs_fn : public relation_mutator_fn { 1639 scoped_ptr<table_transformer_fn> m_tproject_fn; //if zero, no columns need to be projected away 1640 unsigned m_col_cnt; 1641 unsigned_vector m_table_cols; 1642 unsigned_vector m_rel_cols; 1643 1644 scoped_ptr<table_join_fn> m_assembling_join_project; 1645 scoped_ptr<table_union_fn> m_updating_union; 1646 public: filter_identical_pairs_fn(const finite_product_relation & r,unsigned col_cnt,const unsigned * table_cols,const unsigned * rel_cols)1647 filter_identical_pairs_fn(const finite_product_relation & r, unsigned col_cnt, const unsigned * table_cols, 1648 const unsigned * rel_cols) : 1649 m_col_cnt(col_cnt), 1650 m_table_cols(col_cnt, table_cols), 1651 m_rel_cols(col_cnt, rel_cols) { 1652 SASSERT(col_cnt>0); 1653 const table_signature & tsig = r.m_table_sig; 1654 unsigned t_sz = tsig.size(); 1655 1656 sort_two_arrays(col_cnt, m_table_cols.begin(), m_rel_cols.begin()); 1657 SASSERT(m_table_cols.back()<t_sz-1); //check the table columns aren't outside the table data columns 1658 SASSERT(*std::max_element(m_rel_cols.begin(), m_rel_cols.end())<r.m_other_sig.size()); //the same for relation 1659 1660 unsigned_vector removed_cols; 1661 add_sequence_without_set(0, t_sz-1, m_table_cols, removed_cols); 1662 if(!removed_cols.empty()) { 1663 m_tproject_fn = r.get_manager().mk_project_fn(r.get_table(), removed_cols.size(), removed_cols.data()); 1664 } 1665 } 1666 operator ()(relation_base & rb)1667 void operator()(relation_base & rb) override { 1668 finite_product_relation & r = get(rb); 1669 finite_product_relation_plugin & plugin = r.get_plugin(); 1670 table_plugin & tplugin = r.get_table_plugin(); 1671 relation_signature & osig = r.m_other_sig; 1672 relation_manager & rmgr = tplugin.get_manager(); 1673 table_base & rtable = r.get_table(); 1674 ast_manager & m = plugin.get_ast_manager(); 1675 1676 //get table without the data columns on which we don't enforce identities 1677 //The relation index column may or may not be non-functional (according to whether we do the projection) 1678 scoped_rel<table_base> tproj; 1679 if(m_tproject_fn) { 1680 tproj = (*m_tproject_fn)(r.get_table()); 1681 } 1682 else { 1683 tproj = r.get_table().clone(); 1684 } 1685 SASSERT(m_col_cnt+1==tproj->get_signature().size()); 1686 1687 table_signature filtered_sig = tproj->get_signature(); 1688 filtered_sig.push_back(finite_product_relation::s_rel_idx_sort); 1689 filtered_sig.set_functional_columns(1); 1690 1691 relation_vector new_rels; 1692 scoped_rel<table_base> filtered_table = tplugin.mk_empty(filtered_sig); 1693 table_fact f; 1694 table_base::iterator pit = tproj->begin(); 1695 table_base::iterator pend = tproj->end(); 1696 for(; pit!=pend; ++pit) { 1697 pit->get_fact(f); 1698 unsigned old_rel_idx = static_cast<unsigned>(f.back()); 1699 const relation_base & old_rel = r.get_inner_rel(old_rel_idx); 1700 relation_base * new_rel = old_rel.clone(); 1701 for(unsigned i=0; i<m_col_cnt; i++) { 1702 relation_element_ref r_el(m); 1703 rmgr.table_to_relation(osig[m_rel_cols[i]], f[i], r_el); 1704 scoped_ptr<relation_mutator_fn> filter = rmgr.mk_filter_equal_fn(*new_rel, r_el, m_rel_cols[i]); 1705 (*filter)(*new_rel); 1706 } 1707 1708 if(new_rel->empty()) { 1709 new_rel->deallocate(); 1710 continue; 1711 } 1712 1713 unsigned new_rel_idx = new_rels.size(); 1714 new_rels.push_back(new_rel); 1715 f.push_back(new_rel_idx); 1716 filtered_table->add_fact(f); 1717 } 1718 1719 if(!m_assembling_join_project) { 1720 m_assembling_join_project = mk_assembler_of_filter_result(rtable, *filtered_table, m_table_cols); 1721 } 1722 1723 scoped_rel<table_base> new_table = (*m_assembling_join_project)(r.get_table(), *filtered_table); 1724 1725 r.reset(); 1726 r.init(*new_table, new_rels, true); 1727 } 1728 }; 1729 mk_filter_identical_pairs(const finite_product_relation & r,unsigned col_cnt,const unsigned * table_cols,const unsigned * rel_cols)1730 relation_mutator_fn * finite_product_relation_plugin::mk_filter_identical_pairs(const finite_product_relation & r, 1731 unsigned col_cnt, const unsigned * table_cols, const unsigned * rel_cols) { 1732 return alloc(filter_identical_pairs_fn, r, col_cnt, table_cols, rel_cols); 1733 } 1734 mk_assembler_of_filter_result(const table_base & relation_table,const table_base & filtered_table,const unsigned_vector & selected_columns)1735 table_join_fn * finite_product_relation_plugin::mk_assembler_of_filter_result(const table_base & relation_table, 1736 const table_base & filtered_table, const unsigned_vector & selected_columns) { 1737 1738 table_plugin & tplugin = relation_table.get_plugin(); 1739 const table_signature & rtable_sig = relation_table.get_signature(); 1740 unsigned rtable_sig_sz = rtable_sig.size(); 1741 unsigned selected_col_cnt = selected_columns.size(); 1742 SASSERT(selected_col_cnt+2==filtered_table.get_signature().size()); 1743 SASSERT(rtable_sig.functional_columns()==1); 1744 SASSERT(filtered_table.get_signature().functional_columns()==1); 1745 1746 unsigned_vector rtable_joined_cols; 1747 rtable_joined_cols.append(selected_col_cnt, selected_columns.data()); //filtered table cols 1748 rtable_joined_cols.push_back(rtable_sig_sz-1); //unfiltered relation indexes 1749 1750 unsigned_vector filtered_joined_cols; 1751 add_sequence(0, selected_col_cnt, filtered_joined_cols); //filtered table cols 1752 filtered_joined_cols.push_back(selected_col_cnt); //unfiltered relation indexes 1753 SASSERT(rtable_joined_cols.size()==filtered_joined_cols.size()); 1754 1755 //the signature after join: 1756 //(all relation table columns)(all filtered relation table columns)(unfiltered rel idx non-func from 'filtered') 1757 // (unfiltered rel idx func from 'rtable')(filtered rel idx) 1758 unsigned_vector removed_cols; 1759 unsigned filtered_nonfunc_ofs = rtable_sig_sz-1; 1760 add_sequence(filtered_nonfunc_ofs, selected_col_cnt, removed_cols); //data columns from 'filtered' 1761 unsigned idx_ofs = filtered_nonfunc_ofs+selected_col_cnt; 1762 removed_cols.push_back(idx_ofs); //unfiltered relation indexes from 'filtered' 1763 removed_cols.push_back(idx_ofs+1); //unfiltered relation indexes from rtable 1764 1765 table_join_fn * res = tplugin.get_manager().mk_join_project_fn(relation_table, filtered_table, 1766 rtable_joined_cols, filtered_joined_cols, removed_cols); 1767 SASSERT(res); 1768 return res; 1769 } 1770 1771 // ----------------------------------- 1772 // 1773 // finite_product_relation 1774 // 1775 // ----------------------------------- 1776 finite_product_relation(finite_product_relation_plugin & p,const relation_signature & s,const bool * table_columns,table_plugin & tplugin,relation_plugin & oplugin,family_id other_kind)1777 finite_product_relation::finite_product_relation(finite_product_relation_plugin & p, 1778 const relation_signature & s, const bool * table_columns, table_plugin & tplugin, 1779 relation_plugin & oplugin, family_id other_kind) 1780 : relation_base(p, s), 1781 m_other_plugin(oplugin), 1782 m_other_kind(other_kind), 1783 m_full_rel_idx(UINT_MAX) { 1784 const relation_signature & rel_sig = get_signature(); 1785 unsigned sz = rel_sig.size(); 1786 m_sig2table.resize(sz, UINT_MAX); 1787 m_sig2other.resize(sz, UINT_MAX); 1788 for(unsigned i=0; i<sz; i++) { 1789 if(table_columns[i]) { 1790 m_sig2table[i]=m_table_sig.size(); 1791 table_sort srt; 1792 //the table columns must have table-friendly sorts 1793 VERIFY( get_manager().relation_sort_to_table(rel_sig[i], srt) ); 1794 m_table_sig.push_back(srt); 1795 m_table2sig.push_back(i); 1796 } 1797 else { 1798 m_sig2other[i]=m_other_sig.size(); 1799 m_other_sig.push_back(rel_sig[i]); 1800 m_other2sig.push_back(i); 1801 } 1802 } 1803 SASSERT(m_table_sig.size()+m_other_sig.size()==sz); 1804 1805 m_table_sig.push_back(s_rel_idx_sort); 1806 m_table_sig.set_functional_columns(1); 1807 1808 m_table = tplugin.mk_empty(m_table_sig); 1809 1810 set_kind(p.get_relation_kind(*this, table_columns)); 1811 } 1812 finite_product_relation(const finite_product_relation & r)1813 finite_product_relation::finite_product_relation(const finite_product_relation & r) 1814 : relation_base(r), 1815 m_table_sig(r.m_table_sig), 1816 m_table2sig(r.m_table2sig), 1817 m_sig2table(r.m_sig2table), 1818 m_other_sig(r.m_other_sig), 1819 m_other2sig(r.m_other2sig), 1820 m_sig2other(r.m_sig2other), 1821 m_other_plugin(r.m_other_plugin), 1822 m_other_kind(r.m_other_kind), 1823 m_table(r.m_table->clone()), 1824 m_others(r.m_others), 1825 m_available_rel_indexes(r.m_available_rel_indexes), 1826 m_full_rel_idx(r.m_full_rel_idx), 1827 m_live_rel_collection_project(), 1828 m_empty_rel_removal_filter() { 1829 //m_others is now just a shallow copy, we need use clone of the relations that in it now 1830 unsigned other_sz = m_others.size(); 1831 for(unsigned i=0; i<other_sz; i++) { 1832 if(m_others[i]==0) { 1833 //unreferenced relation index 1834 continue; 1835 } 1836 m_others[i] = get_inner_rel(i).clone(); 1837 } 1838 } 1839 swap(relation_base & r0)1840 void finite_product_relation::swap(relation_base & r0) { 1841 SASSERT(can_swap(r0)); 1842 finite_product_relation & r = finite_product_relation_plugin::get(r0); 1843 SASSERT(get_signature()==r.get_signature()); 1844 SASSERT(&get_plugin()==&r.get_plugin()); 1845 SASSERT(&m_other_plugin==&r.m_other_plugin); 1846 1847 m_table_sig.swap(r.m_table_sig); 1848 m_table2sig.swap(r.m_table2sig); 1849 m_sig2table.swap(r.m_sig2table); 1850 m_other_sig.swap(r.m_other_sig); 1851 m_other2sig.swap(r.m_other2sig); 1852 m_sig2other.swap(r.m_sig2other); 1853 std::swap(m_table, r.m_table); 1854 m_others.swap(r.m_others); 1855 m_available_rel_indexes.swap(r.m_available_rel_indexes); 1856 std::swap(m_full_rel_idx,r.m_full_rel_idx); 1857 m_live_rel_collection_project=nullptr; 1858 m_empty_rel_removal_filter=nullptr; 1859 1860 relation_base::swap(r0); 1861 } 1862 ~finite_product_relation()1863 finite_product_relation::~finite_product_relation() { 1864 m_table->deallocate(); 1865 relation_vector::iterator it = m_others.begin(); 1866 relation_vector::iterator end = m_others.end(); 1867 for(; it!=end; ++it) { 1868 relation_base * rel= *it; 1869 if(rel) { 1870 rel->deallocate(); 1871 } 1872 } 1873 } 1874 get_context() const1875 context & finite_product_relation::get_context() const { 1876 return get_manager().get_context(); 1877 } 1878 get_next_rel_idx() const1879 unsigned finite_product_relation::get_next_rel_idx() const { 1880 unsigned res; 1881 if(!m_available_rel_indexes.empty()) { 1882 res = m_available_rel_indexes.back(); 1883 m_available_rel_indexes.pop_back(); 1884 } 1885 else { 1886 res = m_others.size(); 1887 m_others.push_back(0); 1888 } 1889 SASSERT(m_others[res]==0); 1890 return res; 1891 } 1892 recycle_rel_idx(unsigned idx) const1893 void finite_product_relation::recycle_rel_idx(unsigned idx) const { 1894 SASSERT(m_others[idx]==0); 1895 m_available_rel_indexes.push_back(idx); 1896 } 1897 get_full_rel_idx()1898 unsigned finite_product_relation::get_full_rel_idx() { 1899 if(m_full_rel_idx==UINT_MAX) { 1900 m_full_rel_idx = get_next_rel_idx(); 1901 relation_base * full_other = mk_full_inner(nullptr); 1902 m_others[m_full_rel_idx] = full_other; 1903 } 1904 return m_full_rel_idx; 1905 } 1906 init(const table_base & table_vals,const relation_vector & others,bool contiguous)1907 void finite_product_relation::init(const table_base & table_vals, const relation_vector & others, bool contiguous) { 1908 SASSERT(m_table_sig.equal_up_to_fn_mark(table_vals.get_signature())); 1909 SASSERT(empty()); 1910 if(!m_others.empty()) { 1911 garbage_collect(false); 1912 } 1913 SASSERT(m_others.empty()); 1914 1915 m_others = others; 1916 scoped_ptr<table_union_fn> table_union = get_manager().mk_union_fn(get_table(), table_vals); 1917 (*table_union)(get_table(), table_vals); 1918 1919 if(!contiguous) { 1920 unsigned rel_cnt = m_others.size(); 1921 for(unsigned i=0; i<rel_cnt; i++) { 1922 if(m_others[i]==0) { 1923 m_available_rel_indexes.push_back(i); 1924 } 1925 } 1926 } 1927 } 1928 extract_table_fact(const relation_fact & rf,table_fact & tf) const1929 void finite_product_relation::extract_table_fact(const relation_fact & rf, table_fact & tf) const { 1930 const relation_signature & sig = get_signature(); 1931 relation_manager & rmgr = get_manager(); 1932 1933 tf.reset(); 1934 //this is m_table_sig.size()-1 since the last column in table signature if index of the other relation 1935 unsigned t_rel_sz = m_table2sig.size(); 1936 for(unsigned i=0; i<t_rel_sz; i++) { 1937 table_element el; 1938 unsigned sig_idx = m_table2sig[i]; 1939 rmgr.relation_to_table(sig[sig_idx], rf[sig_idx], el); 1940 tf.push_back(el); 1941 } 1942 tf.push_back(0); 1943 } 1944 extract_other_fact(const relation_fact & rf,relation_fact & of) const1945 void finite_product_relation::extract_other_fact(const relation_fact & rf, relation_fact & of) const { 1946 of.reset(); 1947 unsigned o_sz = m_other_sig.size(); 1948 for(unsigned i=0; i<o_sz; i++) { 1949 unsigned sig_idx = m_other2sig[i]; 1950 of.push_back(rf[sig_idx]); 1951 } 1952 } 1953 mk_empty_inner()1954 relation_base * finite_product_relation::mk_empty_inner() { 1955 if(m_other_kind==null_family_id) { 1956 return m_other_plugin.mk_empty(m_other_sig); 1957 } 1958 else { 1959 return m_other_plugin.mk_empty(m_other_sig, m_other_kind); 1960 } 1961 } mk_full_inner(func_decl * pred)1962 relation_base * finite_product_relation::mk_full_inner(func_decl* pred) { 1963 return m_other_plugin.mk_full(pred, m_other_sig, m_other_kind); 1964 } 1965 1966 add_fact(const relation_fact & f)1967 void finite_product_relation::add_fact(const relation_fact & f) { 1968 SASSERT(f.size()==get_signature().size()); 1969 1970 table_fact t_f; 1971 extract_table_fact(f, t_f); 1972 1973 relation_fact o_f(get_manager().get_context()); 1974 extract_other_fact(f, o_f); 1975 1976 unsigned new_rel_idx = get_next_rel_idx(); 1977 t_f.back()=new_rel_idx; 1978 1979 relation_base * new_rel; 1980 if(m_table->suggest_fact(t_f)) { 1981 SASSERT(t_f.back()==new_rel_idx); 1982 new_rel = mk_empty_inner(); 1983 } else { 1984 new_rel = get_inner_rel(t_f.back()).clone(); 1985 1986 t_f[t_f.size()-1]=new_rel_idx; 1987 m_table->ensure_fact(t_f); 1988 } 1989 new_rel->add_fact(o_f); 1990 set_inner_rel(new_rel_idx, new_rel); 1991 } 1992 contains_fact(const relation_fact & f) const1993 bool finite_product_relation::contains_fact(const relation_fact & f) const { 1994 table_fact t_f; 1995 extract_table_fact(f, t_f); 1996 1997 if(!m_table->fetch_fact(t_f)) { 1998 return false; 1999 } 2000 2001 relation_fact o_f(get_context()); 2002 extract_other_fact(f, o_f); 2003 2004 const relation_base & other = get_inner_rel(t_f.back()); 2005 2006 return other.contains_fact(o_f); 2007 } 2008 empty() const2009 bool finite_product_relation::empty() const { 2010 garbage_collect(true); 2011 return m_table->empty(); 2012 } 2013 clone() const2014 finite_product_relation * finite_product_relation::clone() const { 2015 return alloc(finite_product_relation, *this); 2016 } 2017 complement_self(func_decl * p)2018 void finite_product_relation::complement_self(func_decl* p) { 2019 unsigned other_sz = m_others.size(); 2020 for(unsigned i=0; i<other_sz; i++) { 2021 if(m_others[i]==0) { 2022 //unreferenced relation index 2023 continue; 2024 } 2025 relation_base * r = m_others[i]->complement(p); 2026 std::swap(m_others[i],r); 2027 r->deallocate(); 2028 } 2029 table_element full_rel_idx = get_full_rel_idx(); 2030 scoped_rel<table_base> complement_table = m_table->complement(p, &full_rel_idx); 2031 2032 scoped_ptr<table_union_fn> u_fn = get_manager().mk_union_fn(*m_table, *complement_table, nullptr); 2033 SASSERT(u_fn); 2034 (*u_fn)(*m_table, *complement_table, nullptr); 2035 } 2036 complement(func_decl * p) const2037 finite_product_relation * finite_product_relation::complement(func_decl* p) const { 2038 finite_product_relation * res = clone(); 2039 res->complement_self(p); 2040 return res; 2041 } 2042 2043 class finite_product_relation::live_rel_collection_reducer : public table_row_pair_reduce_fn { 2044 idx_set & m_accumulator; 2045 public: live_rel_collection_reducer(idx_set & accumulator)2046 live_rel_collection_reducer(idx_set & accumulator) : m_accumulator(accumulator) {} 2047 operator ()(table_element * func_columns,const table_element * merged_func_columns)2048 void operator()(table_element * func_columns, const table_element * merged_func_columns) override { 2049 m_accumulator.insert(static_cast<unsigned>(merged_func_columns[0])); 2050 } 2051 }; 2052 collect_live_relation_indexes(idx_set & res) const2053 void finite_product_relation::collect_live_relation_indexes(idx_set & res) const { 2054 SASSERT(res.empty()); 2055 unsigned table_data_col_cnt = m_table_sig.size()-1; 2056 2057 if(table_data_col_cnt==0) { 2058 if(!get_table().empty()) { 2059 table_base::iterator iit = get_table().begin(); 2060 table_base::iterator iend = get_table().end(); 2061 2062 SASSERT(iit!=iend); 2063 res.insert(static_cast<unsigned>((*iit)[0])); 2064 SASSERT((++iit)==iend); 2065 } 2066 return; 2067 } 2068 2069 if(!m_live_rel_collection_project) { 2070 buffer<unsigned, false> removed_cols; 2071 removed_cols.resize(table_data_col_cnt); 2072 for(unsigned i=0; i<table_data_col_cnt; i++) { 2073 removed_cols[i] = i; 2074 } 2075 live_rel_collection_reducer * reducer = alloc(live_rel_collection_reducer, m_live_rel_collection_acc); 2076 m_live_rel_collection_project = get_manager().mk_project_with_reduce_fn(get_table(), removed_cols.size(), removed_cols.data(), reducer); 2077 SASSERT(m_live_rel_collection_project); 2078 } 2079 2080 m_live_rel_collection_acc.reset(); 2081 scoped_rel<table_base> live_indexes_table = (*m_live_rel_collection_project)(get_table()); 2082 res.swap(m_live_rel_collection_acc); 2083 2084 SASSERT(live_indexes_table->get_signature().size()==1); 2085 SASSERT(live_indexes_table->get_signature().functional_columns()==1); 2086 if(!live_indexes_table->empty()) { 2087 table_base::iterator iit = live_indexes_table->begin(); 2088 table_base::iterator iend = live_indexes_table->end(); 2089 2090 SASSERT(iit!=iend); 2091 res.insert(static_cast<unsigned>((*iit)[0])); 2092 SASSERT((++iit)==iend); 2093 } 2094 } 2095 garbage_collect(bool remove_empty) const2096 void finite_product_relation::garbage_collect(bool remove_empty) const { 2097 idx_set live_indexes; 2098 collect_live_relation_indexes(live_indexes); 2099 2100 scoped_rel<table_base> empty_rel_indexes; //populated only if \c remove_empty==true 2101 table_fact empty_rel_fact; 2102 2103 unsigned rel_cnt = m_others.size(); 2104 #if Z3DEBUG 2105 unsigned encountered_live_indexes = 0; 2106 #endif 2107 for(unsigned rel_idx=0; rel_idx<rel_cnt; rel_idx++) { 2108 if(m_others[rel_idx]==0) { 2109 continue; 2110 } 2111 if(live_indexes.contains(rel_idx)) { 2112 DEBUG_CODE( encountered_live_indexes++; ); 2113 if(!remove_empty) { 2114 continue; 2115 } 2116 if(!m_others[rel_idx]->empty()) { 2117 continue; 2118 } 2119 if(empty_rel_indexes==0) { 2120 table_signature empty_rel_indexes_sig; 2121 empty_rel_indexes_sig.push_back(s_rel_idx_sort); 2122 empty_rel_indexes = get_table_plugin().mk_empty(empty_rel_indexes_sig); 2123 } 2124 empty_rel_fact.reset(); 2125 empty_rel_fact.push_back(rel_idx); 2126 empty_rel_indexes->add_fact(empty_rel_fact); 2127 } 2128 m_others[rel_idx]->deallocate(); 2129 m_others[rel_idx] = 0; 2130 if(rel_idx==m_full_rel_idx) { 2131 m_full_rel_idx = UINT_MAX; 2132 } 2133 recycle_rel_idx(rel_idx); 2134 } 2135 SASSERT(encountered_live_indexes==live_indexes.num_elems()); 2136 2137 if(m_available_rel_indexes.size()==m_others.size()) { 2138 m_available_rel_indexes.reset(); 2139 m_others.reset(); 2140 } 2141 2142 if(empty_rel_indexes) { 2143 SASSERT(remove_empty); 2144 2145 if(!m_empty_rel_removal_filter) { 2146 unsigned t_joined_cols[] = { m_table_sig.size()-1 }; 2147 unsigned ei_joined_cols[] = { 0 }; 2148 m_empty_rel_removal_filter = get_manager().mk_filter_by_negation_fn(get_table(), *empty_rel_indexes, 2149 1, t_joined_cols, ei_joined_cols); 2150 } 2151 2152 (*m_empty_rel_removal_filter)(*m_table, *empty_rel_indexes); 2153 } 2154 } 2155 try_unify_specifications(ptr_vector<finite_product_relation> & rels)2156 bool finite_product_relation::try_unify_specifications(ptr_vector<finite_product_relation> & rels) { 2157 if(rels.empty()) { 2158 return true; 2159 } 2160 unsigned sig_sz = rels.back()->get_signature().size(); 2161 bool_vector table_cols(sig_sz, true); 2162 2163 ptr_vector<finite_product_relation>::iterator it = rels.begin(); 2164 ptr_vector<finite_product_relation>::iterator end = rels.end(); 2165 for(; it!=end; ++it) { 2166 finite_product_relation & rel = **it; 2167 for(unsigned i=0; i<sig_sz; i++) { 2168 table_cols[i] &= rel.is_table_column(i); 2169 } 2170 } 2171 2172 it = rels.begin(); 2173 for(; it!=end; ++it) { 2174 finite_product_relation & rel = **it; 2175 if(!rel.try_modify_specification(table_cols.data())) { 2176 return false; 2177 } 2178 } 2179 return true; 2180 } 2181 try_modify_specification(const bool * table_cols)2182 bool finite_product_relation::try_modify_specification(const bool * table_cols) { 2183 relation_manager & rmgr = get_manager(); 2184 const relation_signature & sig = get_signature(); 2185 2186 unsigned_vector new_rel_columns; //in global signature 2187 unsigned_vector to_project_away; //in table signature 2188 relation_signature moved_cols_sig; 2189 unsigned sig_sz = get_signature().size(); 2190 for(unsigned i=0; i<sig_sz; i++) { 2191 if(table_cols[i] && !is_table_column(i)) { 2192 //we cannot move columns from relation into the table, only the other way round 2193 return false; 2194 } 2195 if(is_table_column(i)) { 2196 if(!table_cols[i]) { 2197 new_rel_columns.push_back(i); 2198 moved_cols_sig.push_back(sig[i]); 2199 } 2200 else { 2201 to_project_away.push_back(m_sig2table[i]); 2202 } 2203 } 2204 } 2205 //remove also the last column with inner relation index 2206 to_project_away.push_back(get_table().get_signature().size()-1); 2207 2208 if(new_rel_columns.empty()) { 2209 //the specifications are the same 2210 return true; 2211 } 2212 if(!m_other_plugin.can_handle_signature(moved_cols_sig)) { 2213 return false; 2214 } 2215 2216 //we will create a finite_product_relation that contains only relation columns and contains tuples 2217 //that appear in the table columns we are making into relation ones. Then we join this table 2218 //to the current one, and project and reorder the columns as needed to get the right result. 2219 //It the end we swap the content of the resulting table with the current one. 2220 2221 scoped_ptr<table_transformer_fn> pr_fun = get_manager().mk_project_fn(get_table(), to_project_away); 2222 table_base * moved_cols_table = (*pr_fun)(get_table()); //gets destroyed inside moved_cols_trel 2223 scoped_rel<relation_base> moved_cols_trel = 2224 rmgr.get_table_relation_plugin(moved_cols_table->get_plugin()).mk_from_table(moved_cols_sig, moved_cols_table); 2225 2226 bool_vector moved_cols_table_flags(moved_cols_sig.size(), false); 2227 2228 scoped_rel<finite_product_relation> moved_cols_rel = get_plugin().mk_empty(moved_cols_sig, 2229 moved_cols_table_flags.data()); 2230 2231 scoped_ptr<relation_union_fn> union_fun = 2232 get_manager().mk_union_fn(*moved_cols_rel, *moved_cols_trel); 2233 SASSERT(union_fun); //the table_relation should be able to be 'unioned into' any relation 2234 2235 (*union_fun)(*moved_cols_rel, *moved_cols_trel); 2236 2237 unsigned_vector all_moved_cols_indexes; 2238 add_sequence(0, moved_cols_sig.size(), all_moved_cols_indexes); 2239 2240 scoped_ptr<relation_join_fn> join_fun = get_manager().mk_join_project_fn(*this, *moved_cols_rel, new_rel_columns, 2241 all_moved_cols_indexes, new_rel_columns, false); 2242 2243 scoped_rel<relation_base> unordered_rel = (*join_fun)(*this, *moved_cols_rel); 2244 SASSERT(unordered_rel->get_signature().size()==sig_sz); //the signature size should be the same as original 2245 2246 //now we need to reorder the columns in the \c new_rel to match the original table 2247 unsigned_vector permutation; 2248 unsigned moved_cols_cnt = new_rel_columns.size(); 2249 unsigned next_replaced_idx = 0; 2250 unsigned next_orig_idx = 0; 2251 for(unsigned i=0; i<sig_sz; i++) { 2252 if(next_replaced_idx<moved_cols_cnt && new_rel_columns[next_replaced_idx]==i) { 2253 permutation.push_back(sig_sz-moved_cols_cnt+next_replaced_idx); 2254 next_replaced_idx++; 2255 } 2256 else { 2257 permutation.push_back(next_orig_idx++); 2258 } 2259 } 2260 2261 unsigned_vector cycle; 2262 while(try_remove_cycle_from_permutation(permutation, cycle)) { 2263 scoped_ptr<relation_transformer_fn> perm_fun = get_manager().mk_rename_fn(*unordered_rel, cycle); 2264 //the scoped_rel wrapper does the destruction of the old object 2265 unordered_rel = (*perm_fun)(*unordered_rel); 2266 cycle.reset(); 2267 } 2268 2269 finite_product_relation & new_rel = finite_product_relation_plugin::get(*unordered_rel); 2270 2271 //Swap the content of the current object and new_rel. On exitting the function new_rel will be destroyed 2272 //since it points to the content of scoped_rel<relation_base> unordered_rel. 2273 swap(new_rel); 2274 2275 return true; 2276 } 2277 display(std::ostream & out) const2278 void finite_product_relation::display(std::ostream & out) const { 2279 2280 garbage_collect(true); 2281 2282 out << "finite_product_relation:\n"; 2283 2284 out << " table:\n"; 2285 get_table().display(out); 2286 2287 unsigned other_sz = m_others.size(); 2288 for(unsigned i=0; i<other_sz; i++) { 2289 if(m_others[i]==0) { 2290 //unreferenced relation index 2291 continue; 2292 } 2293 out << " inner relation " << i << ":\n"; 2294 get_inner_rel(i).display(out); 2295 } 2296 } 2297 display_tuples(func_decl & pred,std::ostream & out) const2298 void finite_product_relation::display_tuples(func_decl & pred, std::ostream & out) const { 2299 out << "Tuples in " << pred.get_name() << ": \n"; 2300 if(!m_other_plugin.from_table()) { 2301 display(out); 2302 return; 2303 } 2304 2305 context & ctx = get_context(); 2306 2307 table_fact tfact; 2308 table_fact ofact; 2309 2310 unsigned sig_sz = get_signature().size(); 2311 unsigned rel_idx_col = m_table_sig.size()-1; 2312 2313 table_base::iterator it = get_table().begin(); 2314 table_base::iterator end = get_table().end(); 2315 for(; it!=end ; ++it) { 2316 it->get_fact(tfact); 2317 2318 const table_relation & orel = static_cast<const table_relation &>(get_inner_rel(tfact[rel_idx_col])); 2319 const table_base & otable = orel.get_table(); 2320 table_base::iterator oit = otable.begin(); 2321 table_base::iterator oend = otable.end(); 2322 for(; oit!=oend; ++oit) { 2323 oit->get_fact(ofact); 2324 2325 out << "\t("; 2326 for(unsigned i=0; i<sig_sz; i++) { 2327 if(i!=0) { 2328 out << ','; 2329 } 2330 2331 table_element sym_num; 2332 if(is_table_column(i)) { 2333 sym_num = tfact[m_sig2table[i]]; 2334 } 2335 else { 2336 sym_num = ofact[m_sig2other[i]]; 2337 } 2338 relation_sort sort = pred.get_domain(i); 2339 2340 out << ctx.get_argument_name(&pred, i) << '='; 2341 ctx.print_constant_name(sort, sym_num, out); 2342 out << '(' << sym_num << ')'; 2343 } 2344 out << ")\n"; 2345 2346 } 2347 } 2348 } 2349 to_formula(expr_ref & fml) const2350 void finite_product_relation::to_formula(expr_ref& fml) const { 2351 relation_signature const& sig = get_signature(); 2352 ast_manager& m = fml.get_manager(); 2353 expr_ref_vector disjs(m), conjs(m); 2354 expr_ref tmp(m); 2355 dl_decl_util util(m); 2356 shift_vars sh(m); 2357 table_fact fact; 2358 table_base::iterator it = get_table().begin(); 2359 table_base::iterator end = get_table().end(); 2360 unsigned fact_sz = m_table_sig.size(); 2361 for(; it!=end ; ++it) { 2362 it->get_fact(fact); 2363 conjs.reset(); 2364 SASSERT(fact.size() == fact_sz); 2365 unsigned rel_idx = static_cast<unsigned>(fact[fact_sz-1]); 2366 m_others[rel_idx]->to_formula(tmp); 2367 for (unsigned i = 0; i + 1 < fact_sz; ++i) { 2368 conjs.push_back(m.mk_eq(m.mk_var(i, sig[i]), util.mk_numeral(fact[i], sig[i]))); 2369 } 2370 sh(tmp, fact_sz-1, tmp); 2371 conjs.push_back(tmp); 2372 disjs.push_back(m.mk_and(conjs.size(), conjs.data())); 2373 } 2374 bool_rewriter(m).mk_or(disjs.size(), disjs.data(), fml); 2375 } 2376 2377 }; 2378