1 /*++ 2 Copyright (c) 2012 Microsoft Corporation 3 4 Module Name: 5 6 rel_context.cpp 7 8 Abstract: 9 10 context for relational datalog engine. 11 12 Author: 13 14 Nikolaj Bjorner (nbjorner) 2012-12-3. 15 16 Revision History: 17 18 Extracted from dl_context 19 20 --*/ 21 22 23 #include "muz/rel/rel_context.h" 24 #include "util/stopwatch.h" 25 #include "muz/base/dl_context.h" 26 #include "muz/rel/dl_compiler.h" 27 #include "muz/rel/dl_instruction.h" 28 #include "muz/rel/dl_mk_explanations.h" 29 #include "muz/transforms/dl_mk_magic_sets.h" 30 #include "muz/rel/dl_product_relation.h" 31 #include "muz/rel/dl_bound_relation.h" 32 #include "muz/rel/dl_interval_relation.h" 33 #include "muz/rel/karr_relation.h" 34 #include "muz/rel/dl_finite_product_relation.h" 35 #include "muz/rel/udoc_relation.h" 36 #include "muz/rel/check_relation.h" 37 #include "muz/rel/dl_lazy_table.h" 38 #include "muz/rel/dl_sparse_table.h" 39 #include "muz/rel/dl_table.h" 40 #include "muz/rel/dl_table_relation.h" 41 #include "muz/rel/aig_exporter.h" 42 #include "muz/rel/dl_mk_simple_joins.h" 43 #include "muz/rel/dl_mk_similarity_compressor.h" 44 #include "muz/transforms/dl_mk_unbound_compressor.h" 45 #include "muz/transforms/dl_mk_subsumption_checker.h" 46 #include "muz/transforms/dl_mk_coi_filter.h" 47 #include "muz/transforms/dl_mk_filter_rules.h" 48 #include "muz/transforms/dl_mk_rule_inliner.h" 49 #include "muz/transforms/dl_mk_interp_tail_simplifier.h" 50 #include "muz/transforms/dl_mk_bit_blast.h" 51 #include "muz/transforms/dl_mk_separate_negated_tails.h" 52 #include "ast/ast_util.h" 53 54 55 namespace datalog { 56 57 class rel_context::scoped_query { 58 context& m_ctx; 59 rule_set m_rules; 60 decl_set m_preds; 61 bool m_was_closed; 62 63 public: 64 scoped_query(context & ctx)65 scoped_query(context& ctx): 66 m_ctx(ctx), 67 m_rules(ctx.get_rules()), 68 m_preds(ctx.get_predicates()), 69 m_was_closed(ctx.is_closed()) 70 { 71 if (m_was_closed) { 72 ctx.reopen(); 73 } 74 } 75 ~scoped_query()76 ~scoped_query() { 77 m_ctx.ensure_opened(); 78 m_ctx.restrict_predicates(m_preds); 79 m_ctx.replace_rules(m_rules); 80 if (m_was_closed) { 81 m_ctx.close(); 82 } 83 } 84 reset()85 void reset() { 86 m_ctx.reopen(); 87 m_ctx.restrict_predicates(m_preds); 88 m_ctx.replace_rules(m_rules); 89 m_ctx.close(); 90 } 91 }; 92 rel_context(context & ctx)93 rel_context::rel_context(context& ctx) 94 : rel_context_base(ctx.get_manager(), "datalog"), 95 m_context(ctx), 96 m(ctx.get_manager()), 97 m_rmanager(ctx), 98 m_answer(m), 99 m_last_result_relation(nullptr), 100 m_ectx(ctx), 101 m_sw(0) { 102 103 // register plugins for builtin tables 104 105 relation_manager& rm = get_rmanager(); 106 107 rm.register_plugin(alloc(sparse_table_plugin, rm)); 108 rm.register_plugin(alloc(hashtable_table_plugin, rm)); 109 rm.register_plugin(alloc(bitvector_table_plugin, rm)); 110 rm.register_plugin(lazy_table_plugin::mk_sparse(rm)); 111 112 // register plugins for builtin relations 113 114 rm.register_plugin(alloc(bound_relation_plugin, rm)); 115 rm.register_plugin(alloc(interval_relation_plugin, rm)); 116 if (m_context.karr()) rm.register_plugin(alloc(karr_relation_plugin, rm)); 117 rm.register_plugin(alloc(udoc_plugin, rm)); 118 rm.register_plugin(alloc(check_relation_plugin, rm)); 119 } 120 ~rel_context()121 rel_context::~rel_context() { 122 if (m_last_result_relation) { 123 m_last_result_relation->deallocate(); 124 m_last_result_relation = nullptr; 125 } 126 } 127 saturate()128 lbool rel_context::saturate() { 129 scoped_query sq(m_context); 130 return saturate(sq); 131 } 132 saturate(scoped_query & sq)133 lbool rel_context::saturate(scoped_query& sq) { 134 m_context.ensure_closed(); 135 unsigned remaining_time_limit = m_context.soft_timeout(); 136 unsigned restart_time = m_context.initial_restart_timeout(); 137 bool time_limit = remaining_time_limit != 0; 138 139 instruction_block termination_code; 140 141 lbool result; 142 143 TRACE("dl", m_context.display(tout);); 144 145 while (true) { 146 m_ectx.reset(); 147 m_code.reset(); 148 termination_code.reset(); 149 m_context.ensure_closed(); 150 transform_rules(); 151 if (m_context.canceled()) { 152 TRACE("dl", tout << "canceled\n";); 153 result = l_undef; 154 break; 155 } 156 TRACE("dl", m_context.display(tout);); 157 //IF_VERBOSE(3, m_context.display_smt2(0,0,verbose_stream());); 158 159 if (m_context.print_aig().is_non_empty_string()) { 160 const char *filename = m_context.print_aig().bare_str(); 161 aig_exporter aig(m_context.get_rules(), get_context(), &m_table_facts); 162 std::ofstream strm(filename, std::ios_base::binary); 163 aig(strm); 164 exit(0); 165 } 166 167 ::stopwatch sw; 168 sw.start(); 169 170 compiler::compile(m_context, m_context.get_rules(), m_code, termination_code); 171 172 bool timeout_after_this_round = time_limit && (restart_time==0 || remaining_time_limit<=restart_time); 173 174 if (time_limit || restart_time!=0) { 175 unsigned timeout = time_limit ? (restart_time!=0) ? 176 std::min(remaining_time_limit, restart_time) 177 : remaining_time_limit : restart_time; 178 m_ectx.set_timelimit(timeout); 179 } 180 181 bool early_termination = !m_code.perform(m_ectx); 182 m_ectx.reset_timelimit(); 183 VERIFY( termination_code.perform(m_ectx) || m_context.canceled()); 184 185 m_code.process_all_costs(); 186 sw.stop(); 187 m_sw += sw.get_seconds(); 188 189 190 IF_VERBOSE(10, m_ectx.report_big_relations(1000, verbose_stream());); 191 192 if (m_context.canceled()) { 193 TRACE("dl", tout << "canceled\n";); 194 result = l_undef; 195 break; 196 } 197 if (!early_termination) { 198 m_context.set_status(OK); 199 result = l_true; 200 break; 201 } 202 if (memory::above_high_watermark()) { 203 m_context.set_status(MEMOUT); 204 result = l_undef; 205 break; 206 } 207 if (timeout_after_this_round) { 208 m_context.set_status(TIMEOUT); 209 TRACE("dl", tout << "timeout\n";); 210 result = l_undef; 211 break; 212 } 213 SASSERT(restart_time != 0); 214 if (time_limit) { 215 SASSERT(remaining_time_limit>restart_time); 216 remaining_time_limit -= restart_time; 217 } 218 uint64_t new_restart_time = static_cast<uint64_t>(restart_time)*m_context.initial_restart_timeout(); 219 if (new_restart_time > UINT_MAX) { 220 restart_time = UINT_MAX; 221 } 222 else { 223 restart_time = static_cast<unsigned>(new_restart_time); 224 } 225 sq.reset(); 226 } 227 m_context.record_transformed_rules(); 228 TRACE("dl", display_profile(tout);); 229 return result; 230 } 231 query(unsigned num_rels,func_decl * const * rels)232 lbool rel_context::query(unsigned num_rels, func_decl * const* rels) { 233 setup_default_relation(); 234 get_rmanager().reset_saturated_marks(); 235 scoped_query _scoped_query(m_context); 236 for (unsigned i = 0; i < num_rels; ++i) { 237 m_context.set_output_predicate(rels[i]); 238 } 239 m_context.close(); 240 reset_negated_tables(); 241 lbool res = saturate(_scoped_query); 242 243 switch(res) { 244 case l_true: { 245 const rule_set& rules = m_context.get_rules(); 246 expr_ref_vector ans(m); 247 expr_ref e(m); 248 bool some_non_empty = num_rels == 0; 249 bool is_approx = false; 250 for (unsigned i = 0; i < num_rels; ++i) { 251 func_decl* q = rules.get_pred(rels[i]); 252 relation_base& rel = get_relation(q); 253 if (!rel.empty()) { 254 some_non_empty = true; 255 } 256 if (!rel.is_precise()) { 257 is_approx = true; 258 } 259 rel.to_formula(e); 260 ans.push_back(e); 261 } 262 SASSERT(!m_last_result_relation); 263 if (some_non_empty) { 264 m_answer = mk_and(m, ans.size(), ans.data()); 265 if (is_approx) { 266 TRACE("dl", tout << "approx\n";); 267 res = l_undef; 268 m_context.set_status(APPROX); 269 } 270 } 271 else { 272 m_answer = m.mk_false(); 273 res = l_false; 274 } 275 break; 276 } 277 case l_false: 278 m_answer = m.mk_false(); 279 break; 280 case l_undef: 281 TRACE("dl", tout << "saturation in undef\n";); 282 break; 283 } 284 return res; 285 } 286 get_model()287 model_ref rel_context::get_model() { 288 model_ref md = alloc(model, m); 289 auto& rm = get_rmanager(); 290 func_decl_set decls = rm.collect_predicates(); 291 expr_ref fml(m); 292 for (func_decl* p : decls) { 293 rm.get_relation(p).to_formula(fml); 294 md->register_decl(p, fml); 295 } 296 (*m_context.get_model_converter())(md); 297 return md; 298 } 299 transform_rules()300 void rel_context::transform_rules() { 301 rule_transformer transf(m_context); 302 transf.register_plugin(alloc(mk_coi_filter, m_context)); 303 transf.register_plugin(alloc(mk_filter_rules, m_context)); 304 transf.register_plugin(alloc(mk_simple_joins, m_context)); 305 if (m_context.unbound_compressor()) { 306 transf.register_plugin(alloc(mk_unbound_compressor, m_context)); 307 } 308 if (m_context.similarity_compressor()) { 309 transf.register_plugin(alloc(mk_similarity_compressor, m_context)); 310 } 311 transf.register_plugin(alloc(mk_rule_inliner, m_context)); 312 transf.register_plugin(alloc(mk_interp_tail_simplifier, m_context)); 313 transf.register_plugin(alloc(mk_separate_negated_tails, m_context)); 314 315 if (m_context.xform_bit_blast()) { 316 transf.register_plugin(alloc(mk_bit_blast, m_context, 22000)); 317 transf.register_plugin(alloc(mk_interp_tail_simplifier, m_context, 21000)); 318 } 319 m_context.transform_rules(transf); 320 } 321 try_get_size(func_decl * p,unsigned & rel_size) const322 bool rel_context::try_get_size(func_decl* p, unsigned& rel_size) const { 323 relation_base* rb = try_get_relation(p); 324 if (rb && rb->knows_exact_size()) { 325 rel_size = rb->get_size_estimate_rows(); 326 return true; 327 } 328 else { 329 return false; 330 } 331 } 332 query(expr * query)333 lbool rel_context::query(expr* query) { 334 setup_default_relation(); 335 get_rmanager().reset_saturated_marks(); 336 scoped_query _scoped_query(m_context); 337 rule_manager& rm = m_context.get_rule_manager(); 338 func_decl_ref query_pred(m); 339 try { 340 query_pred = rm.mk_query(query, m_context.get_rules()); 341 } 342 catch (default_exception& exn) { 343 m_context.set_status(INPUT_ERROR); 344 throw exn; 345 } 346 347 m_context.close(); 348 reset_negated_tables(); 349 350 if (m_context.generate_explanations()) { 351 m_context.transform_rules(alloc(mk_explanations, m_context)); 352 } 353 354 query_pred = m_context.get_rules().get_pred(query_pred); 355 356 if (m_context.magic_sets_for_queries()) { 357 m_context.transform_rules(alloc(mk_magic_sets, m_context, query_pred)); 358 query_pred = m_context.get_rules().get_pred(query_pred); 359 } 360 361 lbool res = saturate(_scoped_query); 362 363 query_pred = m_context.get_rules().get_pred(query_pred); 364 365 if (res != l_undef) { 366 m_last_result_relation = get_relation(query_pred).clone(); 367 if (m_last_result_relation->empty()) { 368 res = l_false; 369 m_answer = m.mk_false(); 370 } 371 else { 372 m_last_result_relation->to_formula(m_answer); 373 if (!m_last_result_relation->is_precise()) { 374 m_context.set_status(APPROX); 375 TRACE("dl", tout << "approx\n";); 376 res = l_undef; 377 } 378 } 379 } 380 381 return res; 382 } 383 reset_negated_tables()384 void rel_context::reset_negated_tables() { 385 const rule_set& all_rules = m_context.get_rules(); 386 rule_set::pred_set_vector const & pred_sets = all_rules.get_strats(); 387 bool non_empty = false; 388 for (unsigned i = 1; i < pred_sets.size(); ++i) { 389 func_decl_set::iterator it = pred_sets[i]->begin(), end = pred_sets[i]->end(); 390 for (; it != end; ++it) { 391 func_decl* pred = *it; 392 relation_base & rel = get_relation(pred); 393 if (!rel.fast_empty()) { 394 non_empty = true; 395 break; 396 } 397 } 398 } 399 if (!non_empty) { 400 return; 401 } 402 // collect predicates that depend on negation. 403 func_decl_set depends_on_negation; 404 for (unsigned i = 1; i < pred_sets.size(); ++i) { 405 bool change = true; 406 while (change) { 407 change = false; 408 func_decl_set::iterator it = pred_sets[i]->begin(), end = pred_sets[i]->end(); 409 for (; it != end; ++it) { 410 func_decl* pred = *it; 411 if (depends_on_negation.contains(pred)) { 412 continue; 413 } 414 rule_vector const& rules = all_rules.get_predicate_rules(pred); 415 bool inserted = false; 416 for (unsigned j = 0; !inserted && j < rules.size(); ++j) { 417 rule* r = rules[j]; 418 unsigned psz = r->get_positive_tail_size(); 419 unsigned tsz = r->get_uninterpreted_tail_size(); 420 if (psz < tsz) { 421 depends_on_negation.insert(pred); 422 change = true; 423 inserted = true; 424 } 425 for (unsigned k = 0; !inserted && k < tsz; ++k) { 426 func_decl* tail_decl = r->get_tail(k)->get_decl(); 427 if (depends_on_negation.contains(tail_decl)) { 428 depends_on_negation.insert(pred); 429 change = true; 430 inserted = true; 431 } 432 } 433 } 434 } 435 } 436 } 437 func_decl_set::iterator it = depends_on_negation.begin(), end = depends_on_negation.end(); 438 for (; it != end; ++it) { 439 func_decl* pred = *it; 440 relation_base & rel = get_relation(pred); 441 442 if (!rel.empty()) { 443 TRACE("dl", tout << "Resetting: " << mk_ismt2_pp(pred, m) << "\n";); 444 rel.reset(); 445 } 446 } 447 } 448 restrict_predicates(func_decl_set const & predicates)449 void rel_context::restrict_predicates(func_decl_set const& predicates) { 450 get_rmanager().restrict_predicates(predicates); 451 } 452 get_relation(func_decl * pred)453 relation_base & rel_context::get_relation(func_decl * pred) { return get_rmanager().get_relation(pred); } try_get_relation(func_decl * pred) const454 relation_base * rel_context::try_get_relation(func_decl * pred) const { return get_rmanager().try_get_relation(pred); } 455 try_get_formula(func_decl * p) const456 expr_ref rel_context::try_get_formula(func_decl* p) const { 457 expr_ref result(m); 458 relation_base* rb = try_get_relation(p); 459 if (rb) { 460 rb->to_formula(result); 461 } 462 return result; 463 } 464 is_empty_relation(func_decl * pred) const465 bool rel_context::is_empty_relation(func_decl* pred) const { 466 relation_base* rb = try_get_relation(pred); 467 return !rb || rb->fast_empty(); 468 } 469 get_rmanager()470 relation_manager & rel_context::get_rmanager() { return m_rmanager; } 471 get_rmanager() const472 const relation_manager & rel_context::get_rmanager() const { return m_rmanager; } 473 output_profile() const474 bool rel_context::output_profile() const { return m_context.output_profile(); } 475 476 set_predicate_representation(func_decl * pred,unsigned relation_name_cnt,symbol const * relation_names)477 void rel_context::set_predicate_representation(func_decl * pred, unsigned relation_name_cnt, 478 symbol const * relation_names) { 479 480 TRACE("dl", 481 tout << pred->get_name() << ": "; 482 for (unsigned i = 0; i < relation_name_cnt; ++i) { 483 tout << relation_names[i] << " "; 484 } 485 tout << "\n"; 486 ); 487 488 relation_manager & rmgr = get_rmanager(); 489 family_id target_kind = null_family_id; 490 switch (relation_name_cnt) { 491 case 0: 492 return; 493 case 1: 494 target_kind = get_ordinary_relation_plugin(relation_names[0]).get_kind(); 495 break; 496 default: { 497 rel_spec rel_kinds; // kinds of plugins that are not table plugins 498 family_id rel_kind; // the aggregate kind of non-table plugins 499 for (unsigned i = 0; i < relation_name_cnt; i++) { 500 relation_plugin & p = get_ordinary_relation_plugin(relation_names[i]); 501 rel_kinds.push_back(p.get_kind()); 502 } 503 if (rel_kinds.size() == 1) { 504 rel_kind = rel_kinds[0]; 505 } 506 else { 507 relation_signature rel_sig; 508 rmgr.from_predicate(pred, rel_sig); 509 product_relation_plugin & prod_plugin = product_relation_plugin::get_plugin(rmgr); 510 rel_kind = prod_plugin.get_relation_kind(rel_sig, rel_kinds); 511 } 512 target_kind = rel_kind; 513 break; 514 } 515 } 516 517 SASSERT(target_kind != null_family_id); 518 get_rmanager().set_predicate_kind(pred, target_kind); 519 } 520 521 setup_default_relation()522 void rel_context::setup_default_relation() { 523 if (m_context.default_relation() == symbol("doc")) { 524 m_context.set_unbound_compressor(false); 525 } 526 } 527 get_ordinary_relation_plugin(symbol relation_name)528 relation_plugin & rel_context::get_ordinary_relation_plugin(symbol relation_name) { 529 relation_plugin * plugin = get_rmanager().get_relation_plugin(relation_name); 530 if (!plugin) { 531 std::stringstream sstm; 532 sstm << "relation plugin " << relation_name << " does not exist"; 533 throw default_exception(sstm.str()); 534 } 535 if (plugin->is_product_relation()) { 536 throw default_exception("cannot request product relation directly"); 537 } 538 if (plugin->is_sieve_relation()) { 539 throw default_exception("cannot request sieve relation directly"); 540 } 541 if (plugin->is_finite_product_relation()) { 542 throw default_exception("cannot request finite product relation directly"); 543 } 544 return *plugin; 545 } 546 result_contains_fact(relation_fact const & f)547 bool rel_context::result_contains_fact(relation_fact const& f) { 548 SASSERT(m_last_result_relation); 549 return m_last_result_relation->contains_fact(f); 550 } 551 add_fact(func_decl * pred,relation_fact const & fact)552 void rel_context::add_fact(func_decl* pred, relation_fact const& fact) { 553 get_rmanager().reset_saturated_marks(); 554 get_relation(pred).add_fact(fact); 555 if (!m_context.print_aig().is_null()) { 556 m_table_facts.push_back(std::make_pair(pred, fact)); 557 } 558 } 559 add_fact(func_decl * pred,table_fact const & fact)560 void rel_context::add_fact(func_decl* pred, table_fact const& fact) { 561 get_rmanager().reset_saturated_marks(); 562 relation_base & rel0 = get_relation(pred); 563 if (rel0.from_table()) { 564 table_relation & rel = static_cast<table_relation &>(rel0); 565 rel.add_table_fact(fact); 566 // TODO: table facts? 567 } 568 else { 569 relation_fact rfact(m); 570 for (unsigned i = 0; i < fact.size(); ++i) { 571 rfact.push_back(m_context.get_decl_util().mk_numeral(fact[i], pred->get_domain()[i])); 572 } 573 add_fact(pred, rfact); 574 } 575 } 576 has_facts(func_decl * pred) const577 bool rel_context::has_facts(func_decl * pred) const { 578 relation_base* r = try_get_relation(pred); 579 return r && !r->empty(); 580 } 581 store_relation(func_decl * pred,relation_base * rel)582 void rel_context::store_relation(func_decl * pred, relation_base * rel) { 583 get_rmanager().store_relation(pred, rel); 584 } 585 collect_statistics(statistics & st) const586 void rel_context::collect_statistics(statistics& st) const { 587 st.update("saturation time", m_sw); 588 m_code.collect_statistics(st); 589 m_ectx.collect_statistics(st); 590 } 591 updt_params()592 void rel_context::updt_params() { 593 if (m_context.check_relation() != symbol::null && 594 m_context.check_relation() != symbol("null")) { 595 symbol cr("check_relation"); 596 m_context.set_default_relation(cr); 597 relation_plugin* p = get_rmanager().get_relation_plugin(cr); 598 SASSERT(p); 599 check_relation_plugin* p1 = dynamic_cast<check_relation_plugin*>(p); 600 relation_plugin* p2 = get_rmanager().get_relation_plugin(m_context.check_relation()); 601 SASSERT(p2); 602 SASSERT(p1 != p2); 603 p1->set_plugin(p2); 604 get_rmanager().set_favourite_plugin(p1); 605 if (m_context.check_relation() == symbol("doc")) { 606 m_context.set_unbound_compressor(false); 607 } 608 } 609 } 610 inherit_predicate_kind(func_decl * new_pred,func_decl * orig_pred)611 void rel_context::inherit_predicate_kind(func_decl* new_pred, func_decl* orig_pred) { 612 if (orig_pred) { 613 family_id target_kind = get_rmanager().get_requested_predicate_kind(orig_pred); 614 if (target_kind != null_family_id) { 615 get_rmanager().set_predicate_kind(new_pred, target_kind); 616 } 617 } 618 } 619 display_output_facts(rule_set const & rules,std::ostream & out) const620 void rel_context::display_output_facts(rule_set const& rules, std::ostream & out) const { 621 get_rmanager().display_output_tables(rules, out); 622 } 623 display_facts(std::ostream & out) const624 void rel_context::display_facts(std::ostream& out) const { 625 get_rmanager().display(out); 626 } 627 display_profile(std::ostream & out)628 void rel_context::display_profile(std::ostream& out) { 629 m_code.make_annotations(m_ectx); 630 m_code.process_all_costs(); 631 632 out << "Big relations\n"; 633 m_ectx.report_big_relations(1000, out); 634 635 get_rmanager().display_relation_sizes(out); 636 } 637 638 639 }; 640