1 /*++ 2 Copyright (c) 2006 Microsoft Corporation 3 4 Module Name: 5 6 dl_instruction.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 #include "ast/ast_pp.h" 21 #include "util/stopwatch.h" 22 #include "muz/base/dl_context.h" 23 #include "muz/base/dl_util.h" 24 #include "muz/rel/dl_instruction.h" 25 #include "muz/rel/rel_context.h" 26 #include "util/debug.h" 27 #include "util/warning.h" 28 29 namespace datalog { 30 31 // ----------------------------------- 32 // 33 // execution_context 34 // 35 // ----------------------------------- 36 execution_context(context & context)37 execution_context::execution_context(context & context) 38 : m_context(context), 39 m_stopwatch(nullptr), 40 m_timelimit_ms(0) {} 41 ~execution_context()42 execution_context::~execution_context() { 43 reset(); 44 } 45 reset()46 void execution_context::reset() { 47 for (relation_base * rel : m_registers) { 48 if (rel) { 49 rel->deallocate(); 50 } 51 } 52 m_registers.reset(); 53 m_reg_annotation.reset(); 54 reset_timelimit(); 55 } 56 get_rel_context()57 rel_context& execution_context::get_rel_context() { 58 return dynamic_cast<rel_context&>(*m_context.get_rel_context()); 59 } 60 get_rel_context() const61 rel_context const& execution_context::get_rel_context() const { 62 return dynamic_cast<rel_context const&>(*m_context.get_rel_context()); 63 } 64 65 struct compare_size_proc { 66 typedef std::pair<unsigned, unsigned> pr; operator ()datalog::compare_size_proc67 bool operator()(pr const& a, pr const& b) const { 68 return a.second > b.second; 69 } 70 }; 71 report_big_relations(unsigned threshold,std::ostream & out) const72 void execution_context::report_big_relations(unsigned threshold, std::ostream & out) const { 73 unsigned n = register_count(); 74 svector<std::pair<unsigned, unsigned> > sizes; 75 size_t total_bytes = 0; 76 for(unsigned i = 0; i < n; i++) { 77 unsigned sz = reg(i) ? reg(i)->get_size_estimate_bytes() : 0; 78 total_bytes += sz; 79 sizes.push_back(std::make_pair(i, sz)); 80 } 81 std::sort(sizes.begin(), sizes.end(), compare_size_proc()); 82 83 out << "bytes " << total_bytes << "\n"; 84 out << "bytes\trows\tannotation\n"; 85 for(unsigned i = 0; i < n; i++) { 86 unsigned sz = sizes[i].second; 87 unsigned rg = sizes[i].first; 88 unsigned rows = reg(rg) ? reg(rg)->get_size_estimate_rows() : 0; 89 if (sz < threshold) { 90 continue; 91 } 92 std::string annotation; 93 get_register_annotation(i, annotation); 94 out << sz << "\t" << rows << "\t" << annotation << "\n"; 95 } 96 } 97 set_timelimit(unsigned time_in_ms)98 void execution_context::set_timelimit(unsigned time_in_ms) { 99 SASSERT(time_in_ms > 0); 100 m_timelimit_ms = time_in_ms; 101 if (!m_stopwatch) { 102 m_stopwatch = alloc(stopwatch); 103 } else { 104 m_stopwatch->stop(); 105 m_stopwatch->reset(); 106 } 107 m_stopwatch->start(); 108 } reset_timelimit()109 void execution_context::reset_timelimit() { 110 dealloc(m_stopwatch); 111 m_stopwatch = nullptr; 112 m_timelimit_ms = 0; 113 } 114 should_terminate()115 bool execution_context::should_terminate() { 116 return 117 m_context.canceled() || 118 memory::above_high_watermark() || 119 (m_stopwatch && 120 m_timelimit_ms != 0 && 121 m_timelimit_ms < static_cast<unsigned>(1000*m_stopwatch->get_current_seconds())); 122 } 123 collect_statistics(statistics & st) const124 void execution_context::collect_statistics(statistics& st) const { 125 st.update("dl.joins", m_stats.m_join); 126 st.update("dl.project", m_stats.m_project); 127 st.update("dl.filter", m_stats.m_filter); 128 st.update("dl.total", m_stats.m_total); 129 st.update("dl.unary_singleton", m_stats.m_unary_singleton); 130 st.update("dl.filter_by_negation", m_stats.m_filter_by_negation); 131 st.update("dl.select_equal_project", m_stats.m_select_equal_project); 132 st.update("dl.join_project", m_stats.m_join_project); 133 st.update("dl.project_rename", m_stats.m_project_rename); 134 st.update("dl.union", m_stats.m_union); 135 st.update("dl.filter_interpreted_project", m_stats.m_filter_interp_project); 136 st.update("dl.filter_id", m_stats.m_filter_id); 137 st.update("dl.filter_eq", m_stats.m_filter_eq); 138 } 139 140 141 // ----------------------------------- 142 // 143 // instruction 144 // 145 // ----------------------------------- 146 ~instruction()147 instruction::~instruction() { 148 for (auto& p : m_fn_cache) { 149 dealloc(p.m_value); 150 } 151 } 152 process_all_costs()153 void instruction::process_all_costs() { 154 process_costs(); 155 } 156 collect_statistics(statistics & st) const157 void instruction::collect_statistics(statistics& st) const { 158 costs c; 159 get_total_cost(c); 160 st.update("instruction", c.instructions); 161 st.update("instruction-time", c.milliseconds); 162 } 163 164 display_indented(execution_context const & _ctx,std::ostream & out,const std::string & indentation) const165 void instruction::display_indented(execution_context const & _ctx, std::ostream & out, const std::string & indentation) const { 166 out << indentation; 167 rel_context const& ctx = _ctx.get_rel_context(); 168 display_head_impl(_ctx, out); 169 if (ctx.output_profile()) { 170 out << " {"; 171 output_profile(out); 172 out << '}'; 173 } 174 out << "\n"; 175 display_body_impl(_ctx, out, indentation); 176 } 177 log_verbose(execution_context & ctx)178 void instruction::log_verbose(execution_context& ctx) { 179 IF_VERBOSE(2, display(ctx, verbose_stream());); 180 } 181 182 class instr_io : public instruction { 183 bool m_store; 184 func_decl_ref m_pred; 185 reg_idx m_reg; 186 public: instr_io(bool store,func_decl_ref const & pred,reg_idx reg)187 instr_io(bool store, func_decl_ref const& pred, reg_idx reg) 188 : m_store(store), m_pred(pred), m_reg(reg) {} perform(execution_context & ctx)189 bool perform(execution_context & ctx) override { 190 log_verbose(ctx); 191 if (m_store) { 192 if (ctx.reg(m_reg)) { 193 ctx.get_rel_context().store_relation(m_pred, ctx.release_reg(m_reg)); 194 } 195 else { 196 rel_context & dctx = ctx.get_rel_context(); 197 relation_base * empty_rel; 198 //the object referenced by sig is valid only until we call dctx.store_relation() 199 const relation_signature & sig = dctx.get_relation(m_pred).get_signature(); 200 empty_rel = dctx.get_rmanager().mk_empty_relation(sig, m_pred.get()); 201 dctx.store_relation(m_pred, empty_rel); 202 } 203 } 204 else { 205 relation_base& rel = ctx.get_rel_context().get_relation(m_pred); 206 if (!rel.fast_empty()) { 207 ctx.set_reg(m_reg, rel.clone()); 208 } 209 else { 210 ctx.make_empty(m_reg); 211 } 212 } 213 return true; 214 } make_annotations(execution_context & ctx)215 void make_annotations(execution_context & ctx) override { 216 ctx.set_register_annotation(m_reg, m_pred->get_name().bare_str()); 217 } display_head_impl(execution_context const & ctx,std::ostream & out) const218 std::ostream& display_head_impl(execution_context const& ctx, std::ostream & out) const override { 219 const char * rel_name = m_pred->get_name().bare_str(); 220 if (m_store) { 221 return out << "store " << m_reg << " into " << rel_name; 222 } 223 else { 224 return out << "load " << rel_name << " into " << m_reg; 225 } 226 } 227 }; 228 mk_load(ast_manager & m,func_decl * pred,reg_idx tgt)229 instruction * instruction::mk_load(ast_manager & m, func_decl * pred, reg_idx tgt) { 230 return alloc(instr_io, false, func_decl_ref(pred, m), tgt); 231 } 232 mk_store(ast_manager & m,func_decl * pred,reg_idx src)233 instruction * instruction::mk_store(ast_manager & m, func_decl * pred, reg_idx src) { 234 return alloc(instr_io, true, func_decl_ref(pred, m), src); 235 } 236 237 238 class instr_dealloc : public instruction { 239 reg_idx m_reg; 240 public: instr_dealloc(reg_idx reg)241 instr_dealloc(reg_idx reg) : m_reg(reg) {} perform(execution_context & ctx)242 bool perform(execution_context & ctx) override { 243 ctx.make_empty(m_reg); 244 return true; 245 } make_annotations(execution_context & ctx)246 void make_annotations(execution_context & ctx) override { 247 ctx.set_register_annotation(m_reg, "alloc"); 248 } display_head_impl(execution_context const & ctx,std::ostream & out) const249 std::ostream& display_head_impl(execution_context const& ctx, std::ostream & out) const override { 250 return out << "dealloc " << m_reg; 251 } 252 }; 253 mk_dealloc(reg_idx reg)254 instruction * instruction::mk_dealloc(reg_idx reg) { 255 return alloc(instr_dealloc, reg); 256 } 257 258 class instr_clone_move : public instruction { 259 bool m_clone; 260 reg_idx m_src; 261 reg_idx m_tgt; 262 public: instr_clone_move(bool clone,reg_idx src,reg_idx tgt)263 instr_clone_move(bool clone, reg_idx src, reg_idx tgt) 264 : m_clone(clone), m_src(src), m_tgt(tgt) {} perform(execution_context & ctx)265 bool perform(execution_context & ctx) override { 266 if (ctx.reg(m_src)) log_verbose(ctx); 267 if (m_clone) { 268 ctx.set_reg(m_tgt, ctx.reg(m_src) ? ctx.reg(m_src)->clone() : nullptr); 269 } 270 else { 271 ctx.set_reg(m_tgt, ctx.reg(m_src) ? ctx.release_reg(m_src) : nullptr); 272 } 273 return true; 274 } make_annotations(execution_context & ctx)275 void make_annotations(execution_context & ctx) override { 276 std::string str; 277 if (ctx.get_register_annotation(m_src, str)) { 278 ctx.set_register_annotation(m_tgt, str); 279 } 280 else if (ctx.get_register_annotation(m_tgt, str)) { 281 ctx.set_register_annotation(m_src, str); 282 } 283 } display_head_impl(execution_context const & ctx,std::ostream & out) const284 std::ostream& display_head_impl(execution_context const& ctx, std::ostream & out) const override { 285 return out << (m_clone ? "clone " : "move ") << m_src << " into " << m_tgt; 286 } 287 }; 288 mk_clone(reg_idx from,reg_idx to)289 instruction * instruction::mk_clone(reg_idx from, reg_idx to) { 290 return alloc(instr_clone_move, true, from, to); 291 } mk_move(reg_idx from,reg_idx to)292 instruction * instruction::mk_move(reg_idx from, reg_idx to) { 293 return alloc(instr_clone_move, false, from, to); 294 } 295 296 297 class instr_while_loop : public instruction { 298 typedef const vector<reg_idx> idx_vector; 299 idx_vector m_controls; 300 instruction_block * m_body; 301 control_is_empty(execution_context & ctx)302 bool control_is_empty(execution_context & ctx) { 303 for (reg_idx r : m_controls) { 304 if (ctx.reg(r) && !ctx.reg(r)->fast_empty()) { 305 return false; 306 } 307 } 308 return true; 309 } 310 protected: process_all_costs()311 void process_all_costs() override { 312 instruction::process_all_costs(); 313 m_body->process_all_costs(); 314 } 315 public: instr_while_loop(unsigned control_reg_cnt,const reg_idx * control_regs,instruction_block * body)316 instr_while_loop(unsigned control_reg_cnt, const reg_idx * control_regs, instruction_block * body) 317 : m_controls(control_reg_cnt, control_regs), m_body(body) {} ~instr_while_loop()318 ~instr_while_loop() override { 319 dealloc(m_body); 320 } perform(execution_context & ctx)321 bool perform(execution_context & ctx) override { 322 log_verbose(ctx); 323 TRACE("dl", tout << "loop entered\n";); 324 unsigned count = 0; 325 while (!control_is_empty(ctx)) { 326 IF_VERBOSE(10, verbose_stream() << "looping ... " << count++ << "\n";); 327 if (!m_body->perform(ctx)) { 328 TRACE("dl", tout << "while loop terminated before completion\n";); 329 return false; 330 } 331 } 332 TRACE("dl", tout << "while loop exited\n";); 333 return true; 334 } make_annotations(execution_context & ctx)335 void make_annotations(execution_context & ctx) override { 336 m_body->make_annotations(ctx); 337 } display_head_impl(execution_context const & ctx,std::ostream & out) const338 std::ostream& display_head_impl(execution_context const & ctx, std::ostream & out) const override { 339 out << "while"; 340 print_container(m_controls, out); 341 return out; 342 } display_body_impl(execution_context const & ctx,std::ostream & out,const std::string & indentation) const343 void display_body_impl(execution_context const & ctx, std::ostream & out, const std::string & indentation) const override { 344 m_body->display_indented(ctx, out, indentation+" "); 345 } 346 }; 347 mk_while_loop(unsigned control_reg_cnt,const reg_idx * control_regs,instruction_block * body)348 instruction * instruction::mk_while_loop(unsigned control_reg_cnt, const reg_idx * control_regs, 349 instruction_block * body) { 350 return alloc(instr_while_loop, control_reg_cnt, control_regs, body); 351 } 352 353 354 class instr_join : public instruction { 355 typedef unsigned_vector column_vector; 356 reg_idx m_rel1; 357 reg_idx m_rel2; 358 column_vector m_cols1; 359 column_vector m_cols2; 360 reg_idx m_res; 361 public: instr_join(reg_idx rel1,reg_idx rel2,unsigned col_cnt,const unsigned * cols1,const unsigned * cols2,reg_idx result)362 instr_join(reg_idx rel1, reg_idx rel2, unsigned col_cnt, const unsigned * cols1, 363 const unsigned * cols2, reg_idx result) 364 : m_rel1(rel1), m_rel2(rel2), m_cols1(col_cnt, cols1), 365 m_cols2(col_cnt, cols2), m_res(result) {} perform(execution_context & ctx)366 bool perform(execution_context & ctx) override { 367 log_verbose(ctx); 368 ++ctx.m_stats.m_join; 369 if (!ctx.reg(m_rel1) || !ctx.reg(m_rel2)) { 370 ctx.make_empty(m_res); 371 return true; 372 } 373 relation_join_fn * fn; 374 const relation_base & r1 = *ctx.reg(m_rel1); 375 const relation_base & r2 = *ctx.reg(m_rel2); 376 if (!find_fn(r1, r2, fn)) { 377 fn = r1.get_manager().mk_join_fn(r1, r2, m_cols1, m_cols2); 378 if (!fn) { 379 throw default_exception(default_exception::fmt(), 380 "trying to perform unsupported join operation on relations of kinds %s and %s", 381 r1.get_plugin().get_name().bare_str(), r2.get_plugin().get_name().bare_str()); 382 } 383 store_fn(r1, r2, fn); 384 } 385 386 TRACE("dl", 387 r1.get_signature().output(ctx.get_rel_context().get_manager(), tout); 388 tout<<":"<<r1.get_size_estimate_rows()<<" x "; 389 r2.get_signature().output(ctx.get_rel_context().get_manager(), tout); 390 tout<<":"<<r2.get_size_estimate_rows()<<" ->\n";); 391 392 ctx.set_reg(m_res, (*fn)(r1, r2)); 393 394 TRACE("dl", 395 ctx.reg(m_res)->get_signature().output(ctx.get_rel_context().get_manager(), tout); 396 tout<<":"<<ctx.reg(m_res)->get_size_estimate_rows()<<"\n";); 397 398 if (ctx.reg(m_res)->fast_empty()) { 399 ctx.make_empty(m_res); 400 } 401 return true; 402 } make_annotations(execution_context & ctx)403 void make_annotations(execution_context & ctx) override { 404 std::string a1 = "rel1", a2 = "rel2"; 405 ctx.get_register_annotation(m_rel1, a1); 406 ctx.get_register_annotation(m_rel1, a1); 407 ctx.set_register_annotation(m_res, "join " + a1 + " " + a2); 408 } display_head_impl(execution_context const & ctx,std::ostream & out) const409 std::ostream& display_head_impl(execution_context const & ctx, std::ostream & out) const override { 410 out << "join " << m_rel1; 411 print_container(m_cols1, out); 412 out << " and " << m_rel2; 413 print_container(m_cols2, out); 414 return out << " into " << m_res; 415 } 416 }; 417 mk_join(reg_idx rel1,reg_idx rel2,unsigned col_cnt,const unsigned * cols1,const unsigned * cols2,reg_idx result)418 instruction * instruction::mk_join(reg_idx rel1, reg_idx rel2, unsigned col_cnt, 419 const unsigned * cols1, const unsigned * cols2, reg_idx result) { 420 return alloc(instr_join, rel1, rel2, col_cnt, cols1, cols2, result); 421 } 422 423 class instr_filter_equal : public instruction { 424 reg_idx m_reg; 425 app_ref m_value; 426 unsigned m_col; 427 public: instr_filter_equal(ast_manager & m,reg_idx reg,const relation_element & value,unsigned col)428 instr_filter_equal(ast_manager & m, reg_idx reg, const relation_element & value, unsigned col) 429 : m_reg(reg), m_value(value, m), m_col(col) {} perform(execution_context & ctx)430 bool perform(execution_context & ctx) override { 431 log_verbose(ctx); 432 ++ctx.m_stats.m_filter_eq; 433 if (!ctx.reg(m_reg)) { 434 return true; 435 } 436 437 relation_mutator_fn * fn; 438 relation_base & r = *ctx.reg(m_reg); 439 if (!find_fn(r, fn)) { 440 fn = r.get_manager().mk_filter_equal_fn(r, m_value, m_col); 441 if (!fn) { 442 throw default_exception(default_exception::fmt(), 443 "trying to perform unsupported filter_equal operation on a relation of kind %s", 444 r.get_plugin().get_name().bare_str()); 445 } 446 store_fn(r, fn); 447 } 448 (*fn)(r); 449 450 if (r.fast_empty()) { 451 ctx.make_empty(m_reg); 452 } 453 return true; 454 } make_annotations(execution_context & ctx)455 void make_annotations(execution_context & ctx) override { 456 std::stringstream a; 457 a << "filter_equal " << m_col << " val: " << ctx.get_rel_context().get_rmanager().to_nice_string(m_value); 458 ctx.set_register_annotation(m_reg, a.str()); 459 } display_head_impl(execution_context const & ctx,std::ostream & out) const460 std::ostream& display_head_impl(execution_context const& ctx, std::ostream & out) const override { 461 return out << "filter_equal " << m_reg << " col: " << m_col << " val: " 462 << ctx.get_rel_context().get_rmanager().to_nice_string(m_value); 463 } 464 }; 465 mk_filter_equal(ast_manager & m,reg_idx reg,const relation_element & value,unsigned col)466 instruction * instruction::mk_filter_equal(ast_manager & m, reg_idx reg, const relation_element & value, 467 unsigned col) { 468 return alloc(instr_filter_equal, m, reg, value, col); 469 } 470 471 472 class instr_filter_identical : public instruction { 473 typedef unsigned_vector column_vector; 474 reg_idx m_reg; 475 column_vector m_cols; 476 public: instr_filter_identical(reg_idx reg,unsigned col_cnt,const unsigned * identical_cols)477 instr_filter_identical(reg_idx reg, unsigned col_cnt, const unsigned * identical_cols) 478 : m_reg(reg), m_cols(col_cnt, identical_cols) {} perform(execution_context & ctx)479 bool perform(execution_context & ctx) override { 480 log_verbose(ctx); 481 ++ctx.m_stats.m_filter_id; 482 if (!ctx.reg(m_reg)) { 483 return true; 484 } 485 486 relation_mutator_fn * fn; 487 relation_base & r = *ctx.reg(m_reg); 488 if (!find_fn(r, fn)) { 489 fn = r.get_manager().mk_filter_identical_fn(r, m_cols.size(), m_cols.c_ptr()); 490 if (!fn) { 491 throw default_exception(default_exception::fmt(), 492 "trying to perform unsupported filter_identical operation on a relation of kind %s", 493 r.get_plugin().get_name().bare_str()); 494 } 495 store_fn(r, fn); 496 } 497 (*fn)(r); 498 499 if (r.fast_empty()) { 500 ctx.make_empty(m_reg); 501 } 502 return true; 503 } display_head_impl(execution_context const & ctx,std::ostream & out) const504 std::ostream& display_head_impl(execution_context const& ctx, std::ostream & out) const override { 505 out << "filter_identical " << m_reg << " "; 506 print_container(m_cols, out); 507 return out; 508 } make_annotations(execution_context & ctx)509 void make_annotations(execution_context & ctx) override { 510 ctx.set_register_annotation(m_reg, "filter_identical"); 511 } 512 }; 513 mk_filter_identical(reg_idx reg,unsigned col_cnt,const unsigned * identical_cols)514 instruction * instruction::mk_filter_identical(reg_idx reg, unsigned col_cnt, const unsigned * identical_cols) { 515 return alloc(instr_filter_identical, reg, col_cnt, identical_cols); 516 } 517 518 519 class instr_filter_interpreted : public instruction { 520 reg_idx m_reg; 521 app_ref m_cond; 522 public: instr_filter_interpreted(reg_idx reg,app_ref & condition)523 instr_filter_interpreted(reg_idx reg, app_ref & condition) 524 : m_reg(reg), m_cond(condition) {} perform(execution_context & ctx)525 bool perform(execution_context & ctx) override { 526 if (!ctx.reg(m_reg)) { 527 return true; 528 } 529 log_verbose(ctx); 530 ++ctx.m_stats.m_filter; 531 532 relation_mutator_fn * fn; 533 relation_base & r = *ctx.reg(m_reg); 534 TRACE("dl_verbose", r.display(tout <<"pre-filter-interpreted:\n");); 535 if (!find_fn(r, fn)) { 536 fn = r.get_manager().mk_filter_interpreted_fn(r, m_cond); 537 if (!fn) { 538 throw default_exception(default_exception::fmt(), 539 "trying to perform unsupported filter_interpreted operation on a relation of kind %s", 540 r.get_plugin().get_name().bare_str()); 541 } 542 store_fn(r, fn); 543 } 544 (*fn)(r); 545 546 if (r.fast_empty()) { 547 ctx.make_empty(m_reg); 548 } 549 //TRACE("dl_verbose", r.display(tout <<"post-filter-interpreted:\n");); 550 551 return true; 552 } display_head_impl(execution_context const & ctx,std::ostream & out) const553 std::ostream& display_head_impl(execution_context const& ctx, std::ostream & out) const override { 554 return 555 out << "filter_interpreted " << m_reg << " using " 556 << mk_pp(m_cond, m_cond.get_manager()); 557 } make_annotations(execution_context & ctx)558 void make_annotations(execution_context & ctx) override { 559 std::stringstream a; 560 a << "filter_interpreted " << mk_pp(m_cond, m_cond.get_manager()); 561 ctx.set_register_annotation(m_reg, a.str()); 562 } 563 564 }; 565 mk_filter_interpreted(reg_idx reg,app_ref & condition)566 instruction * instruction::mk_filter_interpreted(reg_idx reg, app_ref & condition) { 567 return alloc(instr_filter_interpreted, reg, condition); 568 } 569 570 class instr_filter_interpreted_and_project : public instruction { 571 reg_idx m_src; 572 app_ref m_cond; 573 unsigned_vector m_cols; 574 reg_idx m_res; 575 public: instr_filter_interpreted_and_project(reg_idx src,app_ref & condition,unsigned col_cnt,const unsigned * removed_cols,reg_idx result)576 instr_filter_interpreted_and_project(reg_idx src, app_ref & condition, 577 unsigned col_cnt, const unsigned * removed_cols, reg_idx result) 578 : m_src(src), m_cond(condition), m_cols(col_cnt, removed_cols), 579 m_res(result) {} 580 perform(execution_context & ctx)581 bool perform(execution_context & ctx) override { 582 log_verbose(ctx); 583 if (!ctx.reg(m_src)) { 584 ctx.make_empty(m_res); 585 return true; 586 } 587 ++ctx.m_stats.m_filter_interp_project; 588 589 relation_transformer_fn * fn; 590 relation_base & reg = *ctx.reg(m_src); 591 TRACE("dl_verbose", reg.display(tout <<"pre-filter-interpreted-and-project:\n");); 592 if (!find_fn(reg, fn)) { 593 fn = reg.get_manager().mk_filter_interpreted_and_project_fn(reg, m_cond, m_cols.size(), m_cols.c_ptr()); 594 if (!fn) { 595 throw default_exception(default_exception::fmt(), 596 "trying to perform unsupported filter_interpreted_and_project operation on a relation of kind %s", 597 reg.get_plugin().get_name().bare_str()); 598 } 599 store_fn(reg, fn); 600 } 601 602 ctx.set_reg(m_res, (*fn)(reg)); 603 604 if (ctx.reg(m_res)->fast_empty()) { 605 ctx.make_empty(m_res); 606 } 607 // TRACE("dl_verbose", reg.display(tout << "post-filter-interpreted-and-project:\n");); 608 return true; 609 } 610 display_head_impl(execution_context const & ctx,std::ostream & out) const611 std::ostream& display_head_impl(execution_context const& ctx, std::ostream & out) const override { 612 out << "filter_interpreted_and_project " << m_src << " into " << m_res; 613 out << " using " << mk_pp(m_cond, m_cond.get_manager()); 614 out << " deleting columns "; 615 print_container(m_cols, out); 616 return out; 617 } 618 make_annotations(execution_context & ctx)619 void make_annotations(execution_context & ctx) override { 620 std::stringstream s; 621 std::string a = "rel_src"; 622 ctx.get_register_annotation(m_src, a); 623 s << "filter_interpreted_and_project " << mk_pp(m_cond, m_cond.get_manager()); 624 ctx.set_register_annotation(m_res, s.str()); 625 } 626 }; 627 mk_filter_interpreted_and_project(reg_idx reg,app_ref & condition,unsigned col_cnt,const unsigned * removed_cols,reg_idx result)628 instruction * instruction::mk_filter_interpreted_and_project(reg_idx reg, app_ref & condition, 629 unsigned col_cnt, const unsigned * removed_cols, reg_idx result) { 630 return alloc(instr_filter_interpreted_and_project, reg, condition, col_cnt, removed_cols, result); 631 } 632 633 634 class instr_union : public instruction { 635 reg_idx m_src; 636 reg_idx m_tgt; 637 reg_idx m_delta; 638 bool m_widen; //if true, widening is performed instead of an union 639 public: instr_union(reg_idx src,reg_idx tgt,reg_idx delta,bool widen)640 instr_union(reg_idx src, reg_idx tgt, reg_idx delta, bool widen) 641 : m_src(src), m_tgt(tgt), m_delta(delta), m_widen(widen) {} perform(execution_context & ctx)642 bool perform(execution_context & ctx) override { 643 TRACE("dl", tout << "union " << m_src << " into " << m_tgt 644 << " " << ctx.reg(m_src) << " " << ctx.reg(m_tgt) << "\n";); 645 if (!ctx.reg(m_src)) { 646 return true; 647 } 648 log_verbose(ctx); 649 ++ctx.m_stats.m_union; 650 relation_base & r_src = *ctx.reg(m_src); 651 if (!ctx.reg(m_tgt)) { 652 relation_base * new_tgt = r_src.get_plugin().mk_empty(r_src); 653 ctx.set_reg(m_tgt, new_tgt); 654 } 655 relation_base & r_tgt = *ctx.reg(m_tgt); 656 if (m_delta!=execution_context::void_register && !ctx.reg(m_delta)) { 657 relation_base * new_delta = r_tgt.get_plugin().mk_empty(r_tgt); 658 ctx.set_reg(m_delta, new_delta); 659 } 660 relation_base * r_delta = (m_delta!=execution_context::void_register) ? ctx.reg(m_delta) : nullptr; 661 662 relation_union_fn * fn; 663 664 if (r_delta) { 665 if (!find_fn(r_tgt, r_src, *r_delta, fn)) { 666 if (m_widen) { 667 fn = r_src.get_manager().mk_widen_fn(r_tgt, r_src, r_delta); 668 } 669 else { 670 fn = r_src.get_manager().mk_union_fn(r_tgt, r_src, r_delta); 671 } 672 if (!fn) { 673 std::stringstream sstm; 674 sstm << "trying to perform unsupported union operation on relations of kinds "; 675 sstm << r_tgt.get_plugin().get_name() << ", " << r_src.get_plugin().get_name() << " and "; 676 sstm << r_delta->get_plugin().get_name(); 677 throw default_exception(sstm.str()); 678 } 679 store_fn(r_tgt, r_src, *r_delta, fn); 680 } 681 } 682 else { 683 if (!find_fn(r_tgt, r_src, fn)) { 684 if (m_widen) { 685 fn = r_src.get_manager().mk_widen_fn(r_tgt, r_src, nullptr); 686 } 687 else { 688 fn = r_src.get_manager().mk_union_fn(r_tgt, r_src, nullptr); 689 } 690 if (!fn) { 691 std::stringstream sstm; 692 sstm << "trying to perform unsupported union operation on relations of kinds " 693 << r_tgt.get_plugin().get_name() << " and " 694 << r_src.get_plugin().get_name(); 695 throw default_exception(sstm.str()); 696 } 697 store_fn(r_tgt, r_src, fn); 698 } 699 } 700 701 SASSERT(r_src.get_signature().size() == r_tgt.get_signature().size()); 702 TRACE("dl_verbose", r_tgt.display(tout <<"pre-union:");); 703 704 (*fn)(r_tgt, r_src, r_delta); 705 706 TRACE("dl_verbose", 707 r_src.display(tout <<"src:"); 708 r_tgt.display(tout <<"post-union:"); 709 if (r_delta) { 710 r_delta->display(tout <<"delta:"); 711 }); 712 713 if (r_delta && r_delta->fast_empty()) { 714 ctx.make_empty(m_delta); 715 } 716 717 return true; 718 } make_annotations(execution_context & ctx)719 void make_annotations(execution_context & ctx) override { 720 std::string str = "union"; 721 if (!ctx.get_register_annotation(m_tgt, str)) { 722 ctx.set_register_annotation(m_tgt, "union"); 723 } 724 if (m_delta != execution_context::void_register) { 725 str = "delta of " + str; 726 } 727 ctx.set_register_annotation(m_delta, str); 728 } display_head_impl(execution_context const & ctx,std::ostream & out) const729 std::ostream& display_head_impl(execution_context const& ctx, std::ostream & out) const override { 730 out << (m_widen ? "widen " : "union ") << m_src << " into " << m_tgt; 731 if (m_delta!=execution_context::void_register) { 732 out << " with delta " << m_delta; 733 } 734 return out; 735 } 736 }; 737 mk_union(reg_idx src,reg_idx tgt,reg_idx delta)738 instruction * instruction::mk_union(reg_idx src, reg_idx tgt, reg_idx delta) { 739 return alloc(instr_union, src, tgt, delta, false); 740 } 741 mk_widen(reg_idx src,reg_idx tgt,reg_idx delta)742 instruction * instruction::mk_widen(reg_idx src, reg_idx tgt, reg_idx delta) { 743 return alloc(instr_union, src, tgt, delta, true); 744 } 745 746 747 class instr_project_rename : public instruction { 748 typedef unsigned_vector column_vector; 749 bool m_projection; 750 reg_idx m_src; 751 column_vector m_cols; 752 reg_idx m_tgt; 753 public: instr_project_rename(bool projection,reg_idx src,unsigned col_cnt,const unsigned * cols,reg_idx tgt)754 instr_project_rename(bool projection, reg_idx src, unsigned col_cnt, const unsigned * cols, 755 reg_idx tgt) : m_projection(projection), m_src(src), 756 m_cols(col_cnt, cols), m_tgt(tgt) {} perform(execution_context & ctx)757 bool perform(execution_context & ctx) override { 758 if (!ctx.reg(m_src)) { 759 ctx.make_empty(m_tgt); 760 return true; 761 } 762 763 log_verbose(ctx); 764 ++ctx.m_stats.m_project_rename; 765 relation_transformer_fn * fn; 766 relation_base & r_src = *ctx.reg(m_src); 767 if (!find_fn(r_src, fn)) { 768 if (m_projection) { 769 fn = r_src.get_manager().mk_project_fn(r_src, m_cols.size(), m_cols.c_ptr()); 770 } 771 else { 772 fn = r_src.get_manager().mk_rename_fn(r_src, m_cols.size(), m_cols.c_ptr()); 773 } 774 if (!fn) { 775 std::stringstream sstm; 776 sstm << "trying to perform unsupported " << (m_projection ? "project" : "rename"); 777 sstm << " operation on a relation of kind " << r_src.get_plugin().get_name(); 778 throw default_exception(sstm.str()); 779 } 780 store_fn(r_src, fn); 781 } 782 ctx.set_reg(m_tgt, (*fn)(r_src)); 783 784 return true; 785 } display_head_impl(execution_context const & ctx,std::ostream & out) const786 std::ostream& display_head_impl(execution_context const& ctx, std::ostream & out) const override { 787 out << (m_projection ? "project " : "rename ") << m_src << " into " << m_tgt; 788 out << (m_projection ? " deleting columns " : " with cycle "); 789 print_container(m_cols, out); 790 return out; 791 } make_annotations(execution_context & ctx)792 void make_annotations(execution_context & ctx) override { 793 std::stringstream s; 794 std::string a = "rel_src"; 795 ctx.get_register_annotation(m_src, a); 796 s << (m_projection ? "project " : "rename ") << a; 797 ctx.set_register_annotation(m_tgt, s.str()); 798 } 799 }; 800 mk_projection(reg_idx src,unsigned col_cnt,const unsigned * removed_cols,reg_idx tgt)801 instruction * instruction::mk_projection(reg_idx src, unsigned col_cnt, const unsigned * removed_cols, 802 reg_idx tgt) { 803 return alloc(instr_project_rename, true, src, col_cnt, removed_cols, tgt); 804 } mk_rename(reg_idx src,unsigned cycle_len,const unsigned * permutation_cycle,reg_idx tgt)805 instruction * instruction::mk_rename(reg_idx src, unsigned cycle_len, const unsigned * permutation_cycle, 806 reg_idx tgt) { 807 return alloc(instr_project_rename, false, src, cycle_len, permutation_cycle, tgt); 808 } 809 810 811 class instr_join_project : public instruction { 812 typedef unsigned_vector column_vector; 813 reg_idx m_rel1; 814 reg_idx m_rel2; 815 column_vector m_cols1; 816 column_vector m_cols2; 817 column_vector m_removed_cols; 818 reg_idx m_res; 819 public: instr_join_project(reg_idx rel1,reg_idx rel2,unsigned joined_col_cnt,const unsigned * cols1,const unsigned * cols2,unsigned removed_col_cnt,const unsigned * removed_cols,reg_idx result)820 instr_join_project(reg_idx rel1, reg_idx rel2, unsigned joined_col_cnt, const unsigned * cols1, 821 const unsigned * cols2, unsigned removed_col_cnt, const unsigned * removed_cols, reg_idx result) 822 : m_rel1(rel1), m_rel2(rel2), m_cols1(joined_col_cnt, cols1), 823 m_cols2(joined_col_cnt, cols2), m_removed_cols(removed_col_cnt, removed_cols), m_res(result) { 824 } perform(execution_context & ctx)825 bool perform(execution_context & ctx) override { 826 log_verbose(ctx); 827 if (!ctx.reg(m_rel1) || !ctx.reg(m_rel2)) { 828 ctx.make_empty(m_res); 829 return true; 830 } 831 ++ctx.m_stats.m_join_project; 832 relation_join_fn * fn; 833 const relation_base & r1 = *ctx.reg(m_rel1); 834 const relation_base & r2 = *ctx.reg(m_rel2); 835 if (!find_fn(r1, r2, fn)) { 836 fn = r1.get_manager().mk_join_project_fn(r1, r2, m_cols1, m_cols2, m_removed_cols); 837 if (!fn) { 838 throw default_exception(default_exception::fmt(), 839 "trying to perform unsupported join-project operation on relations of kinds %s and %s", 840 r1.get_plugin().get_name().bare_str(), r2.get_plugin().get_name().bare_str()); 841 } 842 store_fn(r1, r2, fn); 843 } 844 TRACE("dl", tout<<r1.get_size_estimate_rows()<<" x "<<r2.get_size_estimate_rows()<<" jp->\n";); 845 ctx.set_reg(m_res, (*fn)(r1, r2)); 846 TRACE("dl", tout<<ctx.reg(m_res)->get_size_estimate_rows()<<"\n";); 847 if (ctx.reg(m_res)->fast_empty()) { 848 ctx.make_empty(m_res); 849 } 850 return true; 851 } display_head_impl(execution_context const & ctx,std::ostream & out) const852 std::ostream& display_head_impl(execution_context const& ctx, std::ostream & out) const override { 853 relation_base const* r1 = ctx.reg(m_rel1); 854 relation_base const* r2 = ctx.reg(m_rel2); 855 out << "join_project " << m_rel1; 856 if (r1) { 857 out << ":" << r1->num_columns(); 858 out << "-" << r1->get_size_estimate_rows(); 859 } 860 print_container(m_cols1, out); 861 out << " and " << m_rel2; 862 if (r2) { 863 out << ":" << r2->num_columns(); 864 out << "-" << r2->get_size_estimate_rows(); 865 } 866 print_container(m_cols2, out); 867 out << " into " << m_res << " removing columns "; 868 print_container(m_removed_cols, out); 869 return out; 870 } make_annotations(execution_context & ctx)871 void make_annotations(execution_context & ctx) override { 872 std::string s1 = "rel1", s2 = "rel2"; 873 ctx.get_register_annotation(m_rel1, s1); 874 ctx.get_register_annotation(m_rel2, s2); 875 ctx.set_register_annotation(m_res, "join project " + s1 + " " + s2); 876 } 877 }; 878 mk_join_project(reg_idx rel1,reg_idx rel2,unsigned joined_col_cnt,const unsigned * cols1,const unsigned * cols2,unsigned removed_col_cnt,const unsigned * removed_cols,reg_idx result)879 instruction * instruction::mk_join_project(reg_idx rel1, reg_idx rel2, unsigned joined_col_cnt, 880 const unsigned * cols1, const unsigned * cols2, unsigned removed_col_cnt, 881 const unsigned * removed_cols, reg_idx result) { 882 return alloc(instr_join_project, rel1, rel2, joined_col_cnt, cols1, cols2, removed_col_cnt, 883 removed_cols, result); 884 } 885 886 class instr_select_equal_and_project : public instruction { 887 reg_idx m_src; 888 reg_idx m_result; 889 app_ref m_value; 890 unsigned m_col; 891 public: instr_select_equal_and_project(ast_manager & m,reg_idx src,const relation_element & value,unsigned col,reg_idx result)892 instr_select_equal_and_project(ast_manager & m, reg_idx src, const relation_element & value, 893 unsigned col, reg_idx result) 894 : m_src(src), m_result(result), m_value(value, m), m_col(col) { 895 // [Leo]: does not compile on gcc 896 // TRACE("dl", tout << "src:" << m_src << " result: " << m_result << " value:" << m_value << " column:" << m_col << "\n";); 897 } 898 perform(execution_context & ctx)899 bool perform(execution_context & ctx) override { 900 if (!ctx.reg(m_src)) { 901 ctx.make_empty(m_result); 902 return true; 903 } 904 log_verbose(ctx); 905 ++ctx.m_stats.m_select_equal_project; 906 relation_transformer_fn * fn; 907 relation_base & r = *ctx.reg(m_src); 908 if (!find_fn(r, fn)) { 909 fn = r.get_manager().mk_select_equal_and_project_fn(r, m_value, m_col); 910 if (!fn) { 911 throw default_exception(default_exception::fmt(), 912 "trying to perform unsupported select_equal_and_project operation on a relation of kind %s", 913 r.get_plugin().get_name().bare_str()); 914 } 915 store_fn(r, fn); 916 } 917 ctx.set_reg(m_result, (*fn)(r)); 918 919 if (ctx.reg(m_result)->fast_empty()) { 920 ctx.make_empty(m_result); 921 } 922 return true; 923 } display_head_impl(execution_context const & ctx,std::ostream & out) const924 std::ostream& display_head_impl(execution_context const& ctx, std::ostream & out) const override { 925 return out << "select_equal_and_project " << m_src <<" into " << m_result << " col: " << m_col 926 << " val: " << ctx.get_rel_context().get_rmanager().to_nice_string(m_value); 927 } make_annotations(execution_context & ctx)928 void make_annotations(execution_context & ctx) override { 929 std::stringstream s; 930 std::string s1 = "src"; 931 ctx.get_register_annotation(m_src, s1); 932 s << "select equal project col " << m_col << " val: " 933 << ctx.get_rel_context().get_rmanager().to_nice_string(m_value) << " " << s1; 934 ctx.set_register_annotation(m_result, s.str()); 935 } 936 }; 937 mk_select_equal_and_project(ast_manager & m,reg_idx src,const relation_element & value,unsigned col,reg_idx result)938 instruction * instruction::mk_select_equal_and_project(ast_manager & m, reg_idx src, 939 const relation_element & value, unsigned col, reg_idx result) { 940 return alloc(instr_select_equal_and_project, m, src, value, col, result); 941 } 942 943 944 class instr_filter_by_negation : public instruction { 945 typedef unsigned_vector column_vector; 946 reg_idx m_tgt; 947 reg_idx m_neg_rel; 948 column_vector m_cols1; 949 column_vector m_cols2; 950 public: instr_filter_by_negation(reg_idx tgt,reg_idx neg_rel,unsigned col_cnt,const unsigned * cols1,const unsigned * cols2)951 instr_filter_by_negation(reg_idx tgt, reg_idx neg_rel, unsigned col_cnt, const unsigned * cols1, 952 const unsigned * cols2) 953 : m_tgt(tgt), m_neg_rel(neg_rel), m_cols1(col_cnt, cols1), m_cols2(col_cnt, cols2) {} perform(execution_context & ctx)954 bool perform(execution_context & ctx) override { 955 log_verbose(ctx); 956 if (!ctx.reg(m_tgt) || !ctx.reg(m_neg_rel)) { 957 return true; 958 } 959 ++ctx.m_stats.m_filter_by_negation; 960 961 relation_intersection_filter_fn * fn; 962 relation_base & r1 = *ctx.reg(m_tgt); 963 const relation_base & r2 = *ctx.reg(m_neg_rel); 964 if (!find_fn(r1, r2, fn)) { 965 fn = r1.get_manager().mk_filter_by_negation_fn(r1, r2, m_cols1.size(), m_cols1.c_ptr(), m_cols2.c_ptr()); 966 if (!fn) { 967 std::stringstream sstm; 968 sstm << "trying to perform unsupported filter_by_negation on relations of kinds "; 969 sstm << r1.get_plugin().get_name() << " and " << r2.get_plugin().get_name(); 970 throw default_exception(sstm.str()); 971 } 972 store_fn(r1, r2, fn); 973 } 974 (*fn)(r1, r2); 975 976 if (r1.fast_empty()) { 977 ctx.make_empty(m_tgt); 978 } 979 return true; 980 } display_head_impl(execution_context const & ctx,std::ostream & out) const981 std::ostream& display_head_impl(execution_context const& ctx, std::ostream & out) const override { 982 out << "filter_by_negation on " << m_tgt; 983 print_container(m_cols1, out); 984 out << " with " << m_neg_rel; 985 print_container(m_cols2, out); 986 return out << " as the negated table"; 987 } make_annotations(execution_context & ctx)988 void make_annotations(execution_context & ctx) override { 989 std::string s = "negated relation"; 990 ctx.get_register_annotation(m_neg_rel, s); 991 ctx.set_register_annotation(m_tgt, "filter by negation " + s); 992 } 993 }; 994 mk_filter_by_negation(reg_idx tgt,reg_idx neg_rel,unsigned col_cnt,const unsigned * cols1,const unsigned * cols2)995 instruction * instruction::mk_filter_by_negation(reg_idx tgt, reg_idx neg_rel, unsigned col_cnt, 996 const unsigned * cols1, const unsigned * cols2) { 997 return alloc(instr_filter_by_negation, tgt, neg_rel, col_cnt, cols1, cols2); 998 } 999 1000 1001 class instr_mk_unary_singleton : public instruction { 1002 relation_signature m_sig; 1003 func_decl* m_pred; 1004 reg_idx m_tgt; 1005 relation_fact m_fact; 1006 public: instr_mk_unary_singleton(ast_manager & m,func_decl * head_pred,const relation_sort & s,const relation_element & val,reg_idx tgt)1007 instr_mk_unary_singleton(ast_manager & m, func_decl* head_pred, const relation_sort & s, const relation_element & val, 1008 reg_idx tgt) : m_pred(head_pred), m_tgt(tgt), m_fact(m) { 1009 m_sig.push_back(s); 1010 m_fact.push_back(val); 1011 } perform(execution_context & ctx)1012 bool perform(execution_context & ctx) override { 1013 log_verbose(ctx); 1014 ++ctx.m_stats.m_unary_singleton; 1015 relation_base * rel = ctx.get_rel_context().get_rmanager().mk_empty_relation(m_sig, m_pred); 1016 rel->add_fact(m_fact); 1017 ctx.set_reg(m_tgt, rel); 1018 return true; 1019 } display_head_impl(execution_context const & ctx,std::ostream & out) const1020 std::ostream& display_head_impl(execution_context const& ctx, std::ostream & out) const override { 1021 return out << "mk_unary_singleton into " << m_tgt << " sort:" 1022 << ctx.get_rel_context().get_rmanager().to_nice_string(m_sig[0]) << " val:" 1023 << ctx.get_rel_context().get_rmanager().to_nice_string(m_sig[0], m_fact[0]); 1024 } make_annotations(execution_context & ctx)1025 void make_annotations(execution_context & ctx) override { 1026 std::string s; 1027 if (!ctx.get_register_annotation(m_tgt, s)) { 1028 ctx.set_register_annotation(m_tgt, "mk unary singleton"); 1029 } 1030 } 1031 }; 1032 mk_unary_singleton(ast_manager & m,func_decl * head_pred,const relation_sort & s,const relation_element & val,reg_idx tgt)1033 instruction * instruction::mk_unary_singleton(ast_manager & m, func_decl* head_pred, const relation_sort & s, 1034 const relation_element & val, reg_idx tgt) { 1035 return alloc(instr_mk_unary_singleton, m, head_pred, s, val, tgt); 1036 } 1037 1038 1039 class instr_mk_total : public instruction { 1040 relation_signature m_sig; 1041 func_decl* m_pred; 1042 reg_idx m_tgt; 1043 public: instr_mk_total(const relation_signature & sig,func_decl * p,reg_idx tgt)1044 instr_mk_total(const relation_signature & sig, func_decl* p, reg_idx tgt) : m_sig(sig), m_pred(p), m_tgt(tgt) {} perform(execution_context & ctx)1045 bool perform(execution_context & ctx) override { 1046 log_verbose(ctx); 1047 ++ctx.m_stats.m_total; 1048 ctx.set_reg(m_tgt, ctx.get_rel_context().get_rmanager().mk_full_relation(m_sig, m_pred)); 1049 return true; 1050 } display_head_impl(execution_context const & ctx,std::ostream & out) const1051 std::ostream& display_head_impl(execution_context const& ctx, std::ostream & out) const override { 1052 return out << "mk_total into " << m_tgt << " sort:" 1053 << ctx.get_rel_context().get_rmanager().to_nice_string(m_sig) 1054 << " " << m_pred->get_name(); 1055 } make_annotations(execution_context & ctx)1056 void make_annotations(execution_context & ctx) override { 1057 std::string s; 1058 if (!ctx.get_register_annotation(m_tgt, s)) { 1059 ctx.set_register_annotation(m_tgt, "mk_total"); 1060 } 1061 } 1062 }; 1063 mk_total(const relation_signature & sig,func_decl * pred,reg_idx tgt)1064 instruction * instruction::mk_total(const relation_signature & sig, func_decl* pred, reg_idx tgt) { 1065 return alloc(instr_mk_total, sig, pred, tgt); 1066 } 1067 1068 class instr_mark_saturated : public instruction { 1069 func_decl_ref m_pred; 1070 public: instr_mark_saturated(ast_manager & m,func_decl * pred)1071 instr_mark_saturated(ast_manager & m, func_decl * pred) 1072 : m_pred(pred, m) {} perform(execution_context & ctx)1073 bool perform(execution_context & ctx) override { 1074 log_verbose(ctx); 1075 ctx.get_rel_context().get_rmanager().mark_saturated(m_pred); 1076 return true; 1077 } display_head_impl(execution_context const & ctx,std::ostream & out) const1078 std::ostream& display_head_impl(execution_context const& ctx, std::ostream & out) const override { 1079 return out << "mark_saturated " << m_pred->get_name().bare_str(); 1080 } make_annotations(execution_context & ctx)1081 void make_annotations(execution_context & ctx) override { 1082 } 1083 }; 1084 mk_mark_saturated(ast_manager & m,func_decl * pred)1085 instruction * instruction::mk_mark_saturated(ast_manager & m, func_decl * pred) { 1086 return alloc(instr_mark_saturated, m, pred); 1087 } 1088 1089 class instr_assert_signature : public instruction { 1090 relation_signature m_sig; 1091 reg_idx m_tgt; 1092 public: instr_assert_signature(const relation_signature & s,reg_idx tgt)1093 instr_assert_signature(const relation_signature & s, reg_idx tgt) 1094 : m_sig(s), m_tgt(tgt) {} perform(execution_context & ctx)1095 bool perform(execution_context & ctx) override { 1096 log_verbose(ctx); 1097 if (ctx.reg(m_tgt)) { 1098 SASSERT(ctx.reg(m_tgt)->get_signature()==m_sig); 1099 } 1100 return true; 1101 } display_head_impl(execution_context const & ctx,std::ostream & out) const1102 std::ostream& display_head_impl(execution_context const& ctx, std::ostream & out) const override { 1103 out << "instr_assert_signature of " << m_tgt << " signature:"; 1104 print_container(m_sig, out); 1105 return out; 1106 } make_annotations(execution_context & ctx)1107 void make_annotations(execution_context & ctx) override { 1108 std::string s; 1109 if (!ctx.get_register_annotation(m_tgt, s)) { 1110 ctx.set_register_annotation(m_tgt, "assert signature"); 1111 } 1112 } 1113 }; 1114 mk_assert_signature(const relation_signature & s,reg_idx tgt)1115 instruction * instruction::mk_assert_signature(const relation_signature & s, reg_idx tgt) { 1116 return alloc(instr_assert_signature, s, tgt); 1117 } 1118 1119 1120 // ----------------------------------- 1121 // 1122 // instruction_block 1123 // 1124 // ----------------------------------- 1125 ~instruction_block()1126 instruction_block::~instruction_block() { 1127 reset(); 1128 } 1129 reset()1130 void instruction_block::reset() { 1131 for (auto* t : m_data) { 1132 dealloc(t); 1133 } 1134 m_data.reset(); 1135 m_observer = nullptr; 1136 } 1137 perform(execution_context & ctx) const1138 bool instruction_block::perform(execution_context & ctx) const { 1139 cost_recorder crec; 1140 for (instruction * instr : m_data) { 1141 crec.start(instr); //finish is performed by the next start() or by the destructor of crec 1142 1143 TRACE("dl", instr->display_head_impl(ctx, tout << "% ") << "\n";); 1144 1145 if (ctx.should_terminate() || !instr->perform(ctx)) { 1146 return false; 1147 } 1148 } 1149 return true; 1150 } 1151 process_all_costs()1152 void instruction_block::process_all_costs() { 1153 for (auto* t : m_data) { 1154 t->process_all_costs(); 1155 } 1156 } 1157 1158 collect_statistics(statistics & st) const1159 void instruction_block::collect_statistics(statistics& st) const { 1160 for (auto* t : m_data) { 1161 t->collect_statistics(st); 1162 } 1163 } 1164 make_annotations(execution_context & ctx)1165 void instruction_block::make_annotations(execution_context & ctx) { 1166 for (auto* t : m_data) { 1167 t->make_annotations(ctx); 1168 } 1169 } 1170 display_indented(execution_context const & _ctx,std::ostream & out,const std::string & indentation) const1171 void instruction_block::display_indented(execution_context const& _ctx, std::ostream & out, const std::string & indentation) const { 1172 rel_context const& ctx = _ctx.get_rel_context(); 1173 for (auto* i : m_data) { 1174 if (i->passes_output_thresholds(ctx.get_context()) || i->being_recorded()) { 1175 i->display_indented(_ctx, out, indentation); 1176 } 1177 } 1178 } 1179 } 1180 1181