1 /*++ 2 Copyright (c) 2006 Microsoft Corporation 3 4 Module Name: 5 6 dl_compiler.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 <sstream> 22 #include "util/ref_vector.h" 23 #include "muz/base/dl_context.h" 24 #include "muz/rel/rel_context.h" 25 #include "muz/base/dl_rule.h" 26 #include "muz/base/dl_util.h" 27 #include "muz/rel/dl_compiler.h" 28 #include "ast/ast_pp.h" 29 // include"ast_smt2_pp.h" 30 #include "ast/ast_util.h" 31 32 33 namespace datalog { 34 reset()35 void compiler::reset() { 36 m_pred_regs.reset(); 37 } 38 ensure_predicate_loaded(func_decl * pred,instruction_block & acc)39 void compiler::ensure_predicate_loaded(func_decl * pred, instruction_block & acc) { 40 auto& value = m_pred_regs.insert_if_not_there(pred, UINT_MAX); 41 if (value != UINT_MAX) { 42 //predicate is already loaded 43 return; 44 } 45 relation_signature sig; 46 m_context.get_rel_context()->get_rmanager().from_predicate(pred, sig); 47 reg_idx reg = get_fresh_register(sig); 48 value = reg; 49 50 acc.push_back(instruction::mk_load(m_context.get_manager(), pred, reg)); 51 } 52 make_join(reg_idx t1,reg_idx t2,const variable_intersection & vars,reg_idx & result,bool reuse_t1,instruction_block & acc)53 void compiler::make_join(reg_idx t1, reg_idx t2, const variable_intersection & vars, reg_idx & result, 54 bool reuse_t1, instruction_block & acc) { 55 relation_signature res_sig; 56 relation_signature::from_join(m_reg_signatures[t1], m_reg_signatures[t2], vars.size(), 57 vars.get_cols1(), vars.get_cols2(), res_sig); 58 result = get_register(res_sig, reuse_t1, t1); 59 acc.push_back(instruction::mk_join(t1, t2, vars.size(), vars.get_cols1(), vars.get_cols2(), result)); 60 } 61 make_join_project(reg_idx t1,reg_idx t2,const variable_intersection & vars,const unsigned_vector & removed_cols,reg_idx & result,bool reuse_t1,instruction_block & acc)62 void compiler::make_join_project(reg_idx t1, reg_idx t2, const variable_intersection & vars, 63 const unsigned_vector & removed_cols, reg_idx & result, bool reuse_t1, instruction_block & acc) { 64 relation_signature aux_sig; 65 relation_signature sig1 = m_reg_signatures[t1]; 66 relation_signature sig2 = m_reg_signatures[t2]; 67 relation_signature::from_join(sig1, sig2, vars.size(), vars.get_cols1(), vars.get_cols2(), aux_sig); 68 relation_signature res_sig; 69 relation_signature::from_project(aux_sig, removed_cols.size(), removed_cols.data(), 70 res_sig); 71 result = get_register(res_sig, reuse_t1, t1); 72 73 acc.push_back(instruction::mk_join_project(t1, t2, vars.size(), vars.get_cols1(), 74 vars.get_cols2(), removed_cols.size(), removed_cols.data(), result)); 75 } 76 make_filter_interpreted_and_project(reg_idx src,app_ref & cond,const unsigned_vector & removed_cols,reg_idx & result,bool reuse,instruction_block & acc)77 void compiler::make_filter_interpreted_and_project(reg_idx src, app_ref & cond, 78 const unsigned_vector & removed_cols, reg_idx & result, bool reuse, instruction_block & acc) { 79 SASSERT(!removed_cols.empty()); 80 relation_signature res_sig; 81 relation_signature::from_project(m_reg_signatures[src], removed_cols.size(), 82 removed_cols.data(), res_sig); 83 result = get_register(res_sig, reuse, src); 84 85 acc.push_back(instruction::mk_filter_interpreted_and_project(src, cond, 86 removed_cols.size(), removed_cols.data(), result)); 87 } 88 make_select_equal_and_project(reg_idx src,const relation_element val,unsigned col,reg_idx & result,bool reuse,instruction_block & acc)89 void compiler::make_select_equal_and_project(reg_idx src, const relation_element val, unsigned col, 90 reg_idx & result, bool reuse, instruction_block & acc) { 91 relation_signature res_sig; 92 relation_signature::from_project(m_reg_signatures[src], 1, &col, res_sig); 93 result = get_register(res_sig, reuse, src); 94 acc.push_back(instruction::mk_select_equal_and_project(m_context.get_manager(), 95 src, val, col, result)); 96 } 97 make_clone(reg_idx src,reg_idx & result,instruction_block & acc)98 void compiler::make_clone(reg_idx src, reg_idx & result, instruction_block & acc) { 99 relation_signature sig = m_reg_signatures[src]; 100 result = get_fresh_register(sig); 101 acc.push_back(instruction::mk_clone(src, result)); 102 } 103 make_union(reg_idx src,reg_idx tgt,reg_idx delta,bool use_widening,instruction_block & acc)104 void compiler::make_union(reg_idx src, reg_idx tgt, reg_idx delta, bool use_widening, 105 instruction_block & acc) { 106 SASSERT(m_reg_signatures[src]==m_reg_signatures[tgt]); 107 SASSERT(delta==execution_context::void_register || m_reg_signatures[src]==m_reg_signatures[delta]); 108 109 if (use_widening) { 110 acc.push_back(instruction::mk_widen(src, tgt, delta)); 111 } 112 else { 113 acc.push_back(instruction::mk_union(src, tgt, delta)); 114 } 115 } 116 make_projection(reg_idx src,unsigned col_cnt,const unsigned * removed_cols,reg_idx & result,bool reuse,instruction_block & acc)117 void compiler::make_projection(reg_idx src, unsigned col_cnt, const unsigned * removed_cols, 118 reg_idx & result, bool reuse, instruction_block & acc) { 119 SASSERT(col_cnt>0); 120 121 relation_signature res_sig; 122 relation_signature::from_project(m_reg_signatures[src], col_cnt, removed_cols, res_sig); 123 result = get_register(res_sig, reuse, src); 124 acc.push_back(instruction::mk_projection(src, col_cnt, removed_cols, result)); 125 } 126 get_fresh_register(const relation_signature & sig)127 compiler::reg_idx compiler::get_fresh_register(const relation_signature & sig) { 128 //since we might be resizing the m_reg_signatures vector, the argument must not point inside it 129 SASSERT((&sig>=m_reg_signatures.end()) || (&sig<m_reg_signatures.begin())); 130 reg_idx result = m_reg_signatures.size(); 131 m_reg_signatures.push_back(sig); 132 return result; 133 } 134 get_register(const relation_signature & sig,bool reuse,compiler::reg_idx r)135 compiler::reg_idx compiler::get_register(const relation_signature & sig, bool reuse, compiler::reg_idx r) { 136 if (!reuse) 137 return get_fresh_register(sig); 138 SASSERT(r != execution_context::void_register); 139 m_reg_signatures[r] = sig; 140 return r; 141 } 142 get_single_column_register(const relation_sort s)143 compiler::reg_idx compiler::get_single_column_register(const relation_sort s) { 144 relation_signature singl_sig; 145 singl_sig.push_back(s); 146 return get_fresh_register(singl_sig); 147 } 148 get_fresh_registers(const func_decl_set & preds,pred2idx & regs)149 void compiler::get_fresh_registers(const func_decl_set & preds, pred2idx & regs) { 150 func_decl_set::iterator pit = preds.begin(); 151 func_decl_set::iterator pend = preds.end(); 152 for(; pit!=pend; ++pit) { 153 func_decl * pred = *pit; 154 reg_idx reg = m_pred_regs.find(pred); 155 156 SASSERT(!regs.contains(pred)); 157 relation_signature sig = m_reg_signatures[reg]; 158 reg_idx delta_reg = get_fresh_register(sig); 159 regs.insert(pred, delta_reg); 160 } 161 } 162 make_dealloc_non_void(reg_idx r,instruction_block & acc)163 void compiler::make_dealloc_non_void(reg_idx r, instruction_block & acc) { 164 if(r!=execution_context::void_register) { 165 acc.push_back(instruction::mk_dealloc(r)); 166 } 167 } 168 make_add_constant_column(func_decl * head_pred,reg_idx src,const relation_sort s,const relation_element val,reg_idx & result,bool & dealloc,instruction_block & acc)169 void compiler::make_add_constant_column(func_decl* head_pred, reg_idx src, const relation_sort s, const relation_element val, 170 reg_idx & result, bool & dealloc, instruction_block & acc) { 171 reg_idx singleton_table; 172 if(!m_constant_registers.find(s, val, singleton_table)) { 173 singleton_table = get_single_column_register(s); 174 m_top_level_code.push_back( 175 instruction::mk_unary_singleton(m_context.get_manager(), head_pred, s, val, singleton_table)); 176 m_constant_registers.insert(s, val, singleton_table); 177 } 178 if(src==execution_context::void_register) { 179 result = singleton_table; 180 SASSERT(dealloc == false); 181 } 182 else { 183 variable_intersection empty_vars(m_context.get_manager()); 184 make_join(src, singleton_table, empty_vars, result, dealloc, acc); 185 dealloc = true; 186 } 187 } 188 make_add_unbound_column(rule * compiled_rule,unsigned col_idx,func_decl * pred,reg_idx src,const relation_sort & s,reg_idx & result,bool & dealloc,instruction_block & acc)189 void compiler::make_add_unbound_column(rule* compiled_rule, unsigned col_idx, func_decl* pred, reg_idx src, const relation_sort& s, reg_idx & result, 190 bool & dealloc, instruction_block & acc) { 191 192 TRACE("dl", tout << "Adding unbound column " << mk_pp(pred, m_context.get_manager()) 193 << " " << m_context.get_rel_context()->get_rmanager().to_nice_string(s) << "\n";); 194 IF_VERBOSE(3, { 195 expr_ref e(m_context.get_manager()); 196 m_context.get_rule_manager().to_formula(*compiled_rule, e); 197 verbose_stream() << "Compiling unsafe rule column " << col_idx << "\n" 198 << mk_ismt2_pp(e, m_context.get_manager()) << "\n"; 199 }); 200 reg_idx total_table; 201 if (!m_total_registers.find(s, pred, total_table)) { 202 total_table = get_single_column_register(s); 203 relation_signature sig; 204 sig.push_back(s); 205 m_top_level_code.push_back(instruction::mk_total(sig, pred, total_table)); 206 m_total_registers.insert(s, pred, total_table); 207 } 208 if(src == execution_context::void_register) { 209 result = total_table; 210 SASSERT(dealloc == false); 211 } 212 else { 213 variable_intersection empty_vars(m_context.get_manager()); 214 make_join(src, total_table, empty_vars, result, dealloc, acc); 215 dealloc = true; 216 } 217 } 218 make_full_relation(func_decl * pred,const relation_signature & sig,reg_idx & result,instruction_block & acc)219 void compiler::make_full_relation(func_decl* pred, const relation_signature & sig, reg_idx & result, 220 instruction_block & acc) { 221 SASSERT(sig.empty()); 222 TRACE("dl", tout << "Adding unbound column " << mk_pp(pred, m_context.get_manager()) << "\n";); 223 if (m_empty_tables_registers.find(pred, result)) 224 return; 225 226 result = get_fresh_register(sig); 227 m_top_level_code.push_back(instruction::mk_total(sig, pred, result)); 228 m_empty_tables_registers.insert(pred, result); 229 } 230 231 make_duplicate_column(reg_idx src,unsigned col,reg_idx & result,bool reuse,instruction_block & acc)232 void compiler::make_duplicate_column(reg_idx src, unsigned col, reg_idx & result, 233 bool reuse, instruction_block & acc) { 234 235 relation_signature & src_sig = m_reg_signatures[src]; 236 reg_idx single_col_reg; 237 unsigned src_col_cnt = src_sig.size(); 238 if(src_col_cnt==1) { 239 single_col_reg = src; 240 } 241 else { 242 unsigned_vector removed_cols; 243 for(unsigned i=0; i<src_col_cnt; i++) { 244 if(i!=col) { 245 removed_cols.push_back(i); 246 } 247 } 248 make_projection(src, removed_cols.size(), removed_cols.data(), single_col_reg, false, acc); 249 } 250 variable_intersection vi(m_context.get_manager()); 251 vi.add_pair(col, 0); 252 make_join(src, single_col_reg, vi, result, reuse, acc); 253 if (src_col_cnt != 1) 254 make_dealloc_non_void(single_col_reg, acc); 255 } 256 make_rename(reg_idx src,unsigned cycle_len,const unsigned * permutation_cycle,reg_idx & result,bool reuse,instruction_block & acc)257 void compiler::make_rename(reg_idx src, unsigned cycle_len, const unsigned * permutation_cycle, 258 reg_idx & result, bool reuse, instruction_block & acc) { 259 relation_signature res_sig; 260 relation_signature::from_rename(m_reg_signatures[src], cycle_len, permutation_cycle, res_sig); 261 result = get_register(res_sig, reuse, src); 262 acc.push_back(instruction::mk_rename(src, cycle_len, permutation_cycle, result)); 263 } 264 make_assembling_code(rule * compiled_rule,func_decl * head_pred,reg_idx src,const svector<assembling_column_info> & acis0,reg_idx & result,bool & dealloc,instruction_block & acc)265 void compiler::make_assembling_code( 266 rule* compiled_rule, 267 func_decl* head_pred, 268 reg_idx src, 269 const svector<assembling_column_info> & acis0, 270 reg_idx & result, 271 bool & dealloc, 272 instruction_block & acc) { 273 274 TRACE("dl", tout << mk_pp(head_pred, m_context.get_manager()) << "\n";); 275 276 unsigned col_cnt = acis0.size(); 277 reg_idx curr = src; 278 279 relation_signature empty_signature; 280 281 relation_signature * curr_sig; 282 if(curr!=execution_context::void_register) { 283 curr_sig = & m_reg_signatures[curr]; 284 } 285 else { 286 curr_sig = & empty_signature; 287 } 288 unsigned src_col_cnt=curr_sig->size(); 289 290 svector<assembling_column_info> acis(acis0); 291 int2int handled_unbound; 292 293 //first remove unused source columns 294 int_set referenced_src_cols; 295 for(unsigned i=0; i<col_cnt; i++) { 296 if(acis[i].kind==ACK_BOUND_VAR) { 297 SASSERT(acis[i].source_column<src_col_cnt); //we refer only to existing columns 298 referenced_src_cols.insert(acis[i].source_column); 299 } 300 } 301 302 //if an ACK_BOUND_VAR pointed to column i, after projection it will point to 303 //i-new_src_col_offset[i] due to removal of some of earlier columns 304 unsigned_vector new_src_col_offset; 305 306 unsigned_vector src_cols_to_remove; 307 for(unsigned i=0; i<src_col_cnt; i++) { 308 if(!referenced_src_cols.contains(i)) { 309 src_cols_to_remove.push_back(i); 310 } 311 new_src_col_offset.push_back(src_cols_to_remove.size()); 312 } 313 if(!src_cols_to_remove.empty()) { 314 make_projection(curr, src_cols_to_remove.size(), src_cols_to_remove.data(), curr, dealloc, acc); 315 dealloc = true; 316 curr_sig = & m_reg_signatures[curr]; 317 318 //update ACK_BOUND_VAR references 319 for(unsigned i=0; i<col_cnt; i++) { 320 if(acis[i].kind==ACK_BOUND_VAR) { 321 unsigned col = acis[i].source_column; 322 acis[i].source_column = col-new_src_col_offset[col]; 323 } 324 } 325 } 326 327 //convert all result columns into bound variables by extending the source table 328 for(unsigned i=0; i<col_cnt; i++) { 329 if(acis[i].kind==ACK_BOUND_VAR) { 330 continue; 331 } 332 unsigned bound_column_index; 333 if(acis[i].kind != ACK_UNBOUND_VAR || !handled_unbound.find(acis[i].var_index,bound_column_index)) { 334 bound_column_index=curr_sig->size(); 335 if(acis[i].kind==ACK_CONSTANT) { 336 make_add_constant_column(head_pred, curr, acis[i].domain, acis[i].constant, curr, dealloc, acc); 337 } 338 else { 339 SASSERT(acis[i].kind==ACK_UNBOUND_VAR); 340 TRACE("dl", tout << head_pred->get_name() << " index: " << i 341 << " " << m_context.get_rel_context()->get_rmanager().to_nice_string(acis[i].domain) << "\n";); 342 make_add_unbound_column(compiled_rule, i, head_pred, curr, acis[i].domain, curr, dealloc, acc); 343 handled_unbound.insert(acis[i].var_index,bound_column_index); 344 } 345 curr_sig = & m_reg_signatures[curr]; 346 SASSERT(bound_column_index==curr_sig->size()-1); 347 } 348 SASSERT((*curr_sig)[bound_column_index]==acis[i].domain); 349 acis[i].kind=ACK_BOUND_VAR; 350 acis[i].source_column=bound_column_index; 351 } 352 353 //duplicate needed source columns 354 int_set used_cols; 355 for(unsigned i=0; i<col_cnt; i++) { 356 SASSERT(acis[i].kind==ACK_BOUND_VAR); 357 unsigned col=acis[i].source_column; 358 if(!used_cols.contains(col)) { 359 used_cols.insert(col); 360 continue; 361 } 362 make_duplicate_column(curr, col, curr, dealloc, acc); 363 dealloc = true; 364 curr_sig = & m_reg_signatures[curr]; 365 unsigned bound_column_index=curr_sig->size()-1; 366 SASSERT((*curr_sig)[bound_column_index]==acis[i].domain); 367 acis[i].source_column=bound_column_index; 368 } 369 370 //reorder source columns to match target 371 SASSERT(curr_sig->size()==col_cnt); //now the intermediate table is a permutation 372 for(unsigned i=0; i<col_cnt; i++) { 373 if(acis[i].source_column==i) { 374 continue; 375 } 376 unsigned_vector permutation; 377 unsigned next=i; 378 do { 379 permutation.push_back(next); 380 unsigned prev=next; 381 next=acis[prev].source_column; 382 SASSERT(next>=i); //columns below i are already reordered 383 SASSERT(next<col_cnt); 384 acis[prev].source_column=prev; 385 SASSERT(permutation.size()<=col_cnt); //this should not be an infinite loop 386 } while(next!=i); 387 388 make_rename(curr, permutation.size(), permutation.data(), curr, dealloc, acc); 389 dealloc = true; 390 curr_sig = & m_reg_signatures[curr]; 391 } 392 393 if(curr==execution_context::void_register) { 394 SASSERT(src==execution_context::void_register); 395 SASSERT(acis0.size()==0); 396 make_full_relation(head_pred, empty_signature, curr, acc); 397 dealloc = false; 398 } 399 400 result=curr; 401 } 402 get_local_indexes_for_projection(app * t,var_counter & globals,unsigned ofs,unsigned_vector & res)403 void compiler::get_local_indexes_for_projection(app * t, var_counter & globals, unsigned ofs, 404 unsigned_vector & res) { 405 // TODO: this can be optimized to avoid renames in some cases 406 unsigned n = t->get_num_args(); 407 for(unsigned i = 0; i<n; i++) { 408 expr * e = t->get_arg(i); 409 if (is_var(e) && globals.get(to_var(e)->get_idx()) > 0) { 410 globals.update(to_var(e)->get_idx(), -1); 411 res.push_back(i + ofs); 412 } 413 } 414 } 415 get_local_indexes_for_projection(rule * r,unsigned_vector & res)416 void compiler::get_local_indexes_for_projection(rule * r, unsigned_vector & res) { 417 SASSERT(r->get_positive_tail_size()==2); 418 rule_counter counter; 419 // leave one column copy per var in the head (avoids later duplication) 420 counter.count_vars(r->get_head(), -1); 421 422 // take interp & neg preds into account (at least 1 column copy if referenced) 423 unsigned n = r->get_tail_size(); 424 if (n > 2) { 425 rule_counter counter_tail; 426 for (unsigned i = 2; i < n; ++i) { 427 counter_tail.count_vars(r->get_tail(i)); 428 } 429 430 rule_counter::iterator I = counter_tail.begin(), E = counter_tail.end(); 431 for (; I != E; ++I) { 432 int& n = counter.get(I->m_key); 433 if (n == 0) 434 n = -1; 435 } 436 } 437 438 app * t1 = r->get_tail(0); 439 app * t2 = r->get_tail(1); 440 counter.count_vars(t1); 441 counter.count_vars(t2); 442 443 get_local_indexes_for_projection(t1, counter, 0, res); 444 get_local_indexes_for_projection(t2, counter, t1->get_num_args(), res); 445 } 446 447 448 compile_rule_evaluation_run(rule * r,reg_idx head_reg,const reg_idx * tail_regs,reg_idx delta_reg,bool use_widening,instruction_block & acc)449 void compiler::compile_rule_evaluation_run(rule * r, reg_idx head_reg, const reg_idx * tail_regs, 450 reg_idx delta_reg, bool use_widening, instruction_block & acc) { 451 452 ast_manager & m = m_context.get_manager(); 453 m_instruction_observer.start_rule(r); 454 455 const app * h = r->get_head(); 456 unsigned head_len = h->get_num_args(); 457 func_decl * head_pred = h->get_decl(); 458 459 TRACE("dl", r->display(m_context, tout); ); 460 461 unsigned pt_len = r->get_positive_tail_size(); 462 SASSERT(pt_len<=2); //we require rules to be processed by the mk_simple_joins rule transformer plugin 463 464 reg_idx single_res; 465 expr_ref_vector single_res_expr(m); 466 467 //used to save on filter_identical instructions where the check is already done 468 //by the join operation 469 unsigned second_tail_arg_ofs = 0; 470 471 // whether to dealloc the previous result 472 bool dealloc = true; 473 474 if(pt_len == 2) { 475 reg_idx t1_reg=tail_regs[0]; 476 reg_idx t2_reg=tail_regs[1]; 477 app * a1 = r->get_tail(0); 478 app * a2 = r->get_tail(1); 479 SASSERT(m_reg_signatures[t1_reg].size()==a1->get_num_args()); 480 SASSERT(m_reg_signatures[t2_reg].size()==a2->get_num_args()); 481 482 variable_intersection a1a2(m_context.get_manager()); 483 a1a2.populate(a1,a2); 484 485 unsigned_vector removed_cols; 486 get_local_indexes_for_projection(r, removed_cols); 487 488 if(removed_cols.empty()) { 489 make_join(t1_reg, t2_reg, a1a2, single_res, false, acc); 490 } 491 else { 492 make_join_project(t1_reg, t2_reg, a1a2, removed_cols, single_res, false, acc); 493 } 494 495 unsigned rem_index = 0; 496 unsigned rem_sz = removed_cols.size(); 497 unsigned a1len=a1->get_num_args(); 498 for(unsigned i=0; i<a1len; i++) { 499 SASSERT(rem_index==rem_sz || removed_cols[rem_index]>=i); 500 if(rem_index<rem_sz && removed_cols[rem_index]==i) { 501 rem_index++; 502 continue; 503 } 504 single_res_expr.push_back(a1->get_arg(i)); 505 } 506 second_tail_arg_ofs = single_res_expr.size(); 507 unsigned a2len=a2->get_num_args(); 508 for(unsigned i=0; i<a2len; i++) { 509 SASSERT(rem_index==rem_sz || removed_cols[rem_index]>=i+a1len); 510 if(rem_index<rem_sz && removed_cols[rem_index]==i+a1len) { 511 rem_index++; 512 continue; 513 } 514 single_res_expr.push_back(a2->get_arg(i)); 515 } 516 SASSERT(rem_index==rem_sz); 517 } 518 else if(pt_len==1) { 519 app * a = r->get_tail(0); 520 single_res = tail_regs[0]; 521 dealloc = false; 522 523 524 SASSERT(m_reg_signatures[single_res].size() == a->get_num_args()); 525 526 unsigned n=a->get_num_args(); 527 for(unsigned i=0; i<n; i++) { 528 expr * arg = a->get_arg(i); 529 if(is_app(arg)) { 530 app * c = to_app(arg); //argument is a constant 531 SASSERT(m.is_value(c)); 532 make_select_equal_and_project(single_res, c, single_res_expr.size(), single_res, dealloc, acc); 533 dealloc = true; 534 } 535 else { 536 SASSERT(is_var(arg)); 537 single_res_expr.push_back(arg); 538 } 539 } 540 541 } 542 else { 543 SASSERT(pt_len==0); 544 545 //single_res register should never be used in this case 546 single_res=execution_context::void_register; 547 dealloc = false; 548 } 549 550 add_unbound_columns_for_negation(r, head_pred, single_res, single_res_expr, dealloc, acc); 551 552 int2ints var_indexes; 553 554 reg_idx filtered_res = single_res; 555 556 { 557 //enforce equality to constants 558 unsigned srlen=single_res_expr.size(); 559 SASSERT((single_res==execution_context::void_register) ? (srlen==0) : (srlen==m_reg_signatures[single_res].size())); 560 for(unsigned i=0; i<srlen; i++) { 561 expr * exp = single_res_expr[i].get(); 562 if(is_app(exp)) { 563 SASSERT(m_context.get_decl_util().is_numeral_ext(exp)); 564 relation_element value = to_app(exp); 565 if (!dealloc) 566 make_clone(filtered_res, filtered_res, acc); 567 acc.push_back(instruction::mk_filter_equal(m_context.get_manager(), filtered_res, value, i)); 568 dealloc = true; 569 } 570 else { 571 SASSERT(is_var(exp)); 572 unsigned var_num=to_var(exp)->get_idx(); 573 auto& value = var_indexes.insert_if_not_there(var_num, unsigned_vector()); 574 value.push_back(i); 575 } 576 } 577 } 578 579 //enforce equality of columns 580 int2ints::iterator vit=var_indexes.begin(); 581 int2ints::iterator vend=var_indexes.end(); 582 for(; vit!=vend; ++vit) { 583 int2ints::key_data & k = *vit; 584 unsigned_vector & indexes = k.m_value; 585 if(indexes.size()==1) { 586 continue; 587 } 588 SASSERT(indexes.size()>1); 589 if(pt_len==2 && indexes[0]<second_tail_arg_ofs && indexes.back()>=second_tail_arg_ofs) { 590 //If variable appears in multiple tails, the identicity will already be enforced by join. 591 //(If behavior the join changes so that it is not enforced anymore, remove this 592 //condition!) 593 continue; 594 } 595 if (!dealloc) 596 make_clone(filtered_res, filtered_res, acc); 597 acc.push_back(instruction::mk_filter_identical(filtered_res, indexes.size(), indexes.data())); 598 dealloc = true; 599 } 600 601 602 // add unbounded columns for interpreted filter 603 unsigned ut_len = r->get_uninterpreted_tail_size(); 604 unsigned ft_len = r->get_tail_size(); // full tail 605 expr_ref_vector tail(m); 606 for (unsigned tail_index = ut_len; tail_index < ft_len; ++tail_index) { 607 tail.push_back(r->get_tail(tail_index)); 608 } 609 610 expr_ref_vector binding(m); 611 if (!tail.empty()) { 612 expr_ref filter_cond = mk_and(tail); 613 m_free_vars.reset(); 614 m_free_vars(filter_cond); 615 // create binding 616 binding.resize(m_free_vars.size()+1); 617 for (unsigned v = 0; v < m_free_vars.size(); ++v) { 618 if (!m_free_vars[v]) 619 continue; 620 621 int2ints::entry * entry = var_indexes.find_core(v); 622 unsigned src_col; 623 if (entry) { 624 src_col = entry->get_data().m_value.back(); 625 } else { 626 // we have an unbound variable, so we add an unbound column for it 627 relation_sort unbound_sort = m_free_vars[v]; 628 TRACE("dl", tout << "unbound: " << v << "\n" << filter_cond << " " << mk_pp(unbound_sort, m) << "\n";); 629 make_add_unbound_column(r, 0, head_pred, filtered_res, unbound_sort, filtered_res, dealloc, acc); 630 631 src_col = single_res_expr.size(); 632 single_res_expr.push_back(m.mk_var(v, unbound_sort)); 633 634 635 var_indexes.insert_if_not_there(v, unsigned_vector()).push_back(src_col); 636 } 637 relation_sort var_sort = m_reg_signatures[filtered_res][src_col]; 638 binding[m_free_vars.size()-v] = m.mk_var(src_col, var_sort); 639 } 640 } 641 642 // add at least one column for the negative filter 643 if (pt_len != ut_len && filtered_res == execution_context::void_register) { 644 relation_signature empty_signature; 645 make_full_relation(head_pred, empty_signature, filtered_res, acc); 646 } 647 648 //enforce negative predicates 649 for (unsigned i = pt_len; i<ut_len; i++) { 650 app * neg_tail = r->get_tail(i); 651 func_decl * neg_pred = neg_tail->get_decl(); 652 variable_intersection neg_intersection(m_context.get_manager()); 653 neg_intersection.populate(single_res_expr, neg_tail); 654 unsigned_vector t_cols(neg_intersection.size(), neg_intersection.get_cols1()); 655 unsigned_vector neg_cols(neg_intersection.size(), neg_intersection.get_cols2()); 656 657 unsigned neg_len = neg_tail->get_num_args(); 658 for (unsigned i = 0; i<neg_len; i++) { 659 expr * e = neg_tail->get_arg(i); 660 if (is_var(e)) { 661 continue; 662 } 663 SASSERT(is_app(e)); 664 relation_sort arg_sort; 665 m_context.get_rel_context()->get_rmanager().from_predicate(neg_pred, i, arg_sort); 666 make_add_constant_column(head_pred, filtered_res, arg_sort, to_app(e), filtered_res, dealloc, acc); 667 668 t_cols.push_back(single_res_expr.size()); 669 neg_cols.push_back(i); 670 single_res_expr.push_back(e); 671 } 672 SASSERT(t_cols.size() == neg_cols.size()); 673 674 reg_idx neg_reg = m_pred_regs.find(neg_pred); 675 if (!dealloc) 676 make_clone(filtered_res, filtered_res, acc); 677 acc.push_back(instruction::mk_filter_by_negation(filtered_res, neg_reg, t_cols.size(), 678 t_cols.data(), neg_cols.data())); 679 dealloc = true; 680 } 681 682 // enforce interpreted tail predicates 683 if (!tail.empty()) { 684 app_ref filter_cond(tail.size() == 1 ? to_app(tail.back()) : m.mk_and(tail.size(), tail.data()), m); 685 686 // check if there are any columns to remove 687 unsigned_vector remove_columns; 688 { 689 unsigned_vector var_idx_to_remove; 690 m_free_vars(r->get_head()); 691 for (int2ints::iterator I = var_indexes.begin(), E = var_indexes.end(); 692 I != E; ++I) { 693 unsigned var_idx = I->m_key; 694 if (!m_free_vars.contains(var_idx)) { 695 unsigned_vector & cols = I->m_value; 696 for (unsigned i = 0; i < cols.size(); ++i) { 697 remove_columns.push_back(cols[i]); 698 } 699 var_idx_to_remove.push_back(var_idx); 700 } 701 } 702 703 for (unsigned i = 0; i < var_idx_to_remove.size(); ++i) { 704 var_indexes.remove(var_idx_to_remove[i]); 705 } 706 707 // update column idx for after projection state 708 if (!remove_columns.empty()) { 709 unsigned_vector offsets; 710 offsets.resize(single_res_expr.size(), 0); 711 712 for (unsigned i = 0; i < remove_columns.size(); ++i) { 713 for (unsigned col = remove_columns[i]; col < offsets.size(); ++col) { 714 ++offsets[col]; 715 } 716 } 717 718 for (int2ints::iterator I = var_indexes.begin(), E = var_indexes.end(); 719 I != E; ++I) { 720 unsigned_vector & cols = I->m_value; 721 for (unsigned i = 0; i < cols.size(); ++i) { 722 cols[i] -= offsets[cols[i]]; 723 } 724 } 725 } 726 } 727 728 expr_ref renamed = m_context.get_var_subst()(filter_cond, binding.size(), binding.data()); 729 app_ref app_renamed(to_app(renamed), m); 730 if (remove_columns.empty()) { 731 if (!dealloc && filtered_res != UINT_MAX) 732 make_clone(filtered_res, filtered_res, acc); 733 acc.push_back(instruction::mk_filter_interpreted(filtered_res, app_renamed)); 734 } else { 735 std::sort(remove_columns.begin(), remove_columns.end()); 736 make_filter_interpreted_and_project(filtered_res, app_renamed, remove_columns, filtered_res, dealloc, acc); 737 } 738 dealloc = true; 739 } 740 741 #if 0 742 // this version is potentially better for non-symbolic tables, 743 // since it constraints each unbound column at a time (reducing the 744 // size of intermediate results). 745 unsigned ft_len=r->get_tail_size(); //full tail 746 for(unsigned tail_index=ut_len; tail_index<ft_len; tail_index++) { 747 app * t = r->get_tail(tail_index); 748 m_free_vars(t); 749 750 if (m_free_vars.empty()) { 751 expr_ref simplified(m); 752 m_context.get_rewriter()(t, simplified); 753 if(m.is_true(simplified)) { 754 //this tail element is always true 755 continue; 756 } 757 //the tail of this rule is never satisfied 758 SASSERT(m.is_false(simplified)); 759 goto finish; 760 } 761 762 //determine binding size 763 764 unsigned max_var = m_free_vars.size(); 765 while (max_var > 0 && !m_free_vars[max_var-1]) --max_var; 766 767 //create binding 768 expr_ref_vector binding(m); 769 binding.resize(max_var); 770 771 for(unsigned v = 0; v < max_var; ++v) { 772 if (!m_free_vars[v]) { 773 continue; 774 } 775 int2ints::entry * e = var_indexes.find_core(v); 776 if(!e) { 777 //we have an unbound variable, so we add an unbound column for it 778 relation_sort unbound_sort = m_free_vars[v]; 779 780 reg_idx new_reg; 781 TRACE("dl", tout << mk_pp(head_pred, m_context.get_manager()) << "\n";); 782 bool new_dealloc; 783 make_add_unbound_column(r, 0, head_pred, filtered_res, unbound_sort, new_reg, new_dealloc, acc); 784 785 if (dealloc) 786 make_dealloc_non_void(filtered_res, acc); 787 dealloc = new_dealloc; 788 filtered_res = new_reg; // here filtered_res value gets changed !! 789 790 unsigned unbound_column_index = single_res_expr.size(); 791 single_res_expr.push_back(m.mk_var(v, unbound_sort)); 792 793 e = var_indexes.insert_if_not_there3(v, unsigned_vector()); 794 e->get_data().m_value.push_back(unbound_column_index); 795 } 796 unsigned src_col=e->get_data().m_value.back(); 797 relation_sort var_sort = m_reg_signatures[filtered_res][src_col]; 798 binding[max_var-v]=m.mk_var(src_col, var_sort); 799 } 800 801 802 expr_ref renamed(m); 803 m_context.get_var_subst()(t, binding.size(), binding.c_ptr(), renamed); 804 app_ref app_renamed(to_app(renamed), m); 805 if (!dealloc) 806 make_clone(filtered_res, filtered_res, acc); 807 acc.push_back(instruction::mk_filter_interpreted(filtered_res, app_renamed)); 808 dealloc = true; 809 } 810 #endif 811 812 { 813 //put together the columns of head relation 814 relation_signature & head_sig = m_reg_signatures[head_reg]; 815 svector<assembling_column_info> head_acis; 816 unsigned_vector head_src_cols; 817 for(unsigned i=0; i<head_len; i++) { 818 assembling_column_info aci; 819 aci.domain=head_sig[i]; 820 821 expr * exp = h->get_arg(i); 822 if (is_var(exp)) { 823 unsigned var_num = to_var(exp)->get_idx(); 824 int2ints::entry* e = var_indexes.find_core(var_num); 825 if (e) { 826 unsigned_vector& binding_indexes = e->get_data().m_value; 827 aci.kind = ACK_BOUND_VAR; 828 aci.source_column = binding_indexes.back(); 829 SASSERT(aci.source_column < single_res_expr.size()); //we bind only to existing columns 830 if (binding_indexes.size() > 1) { 831 //if possible, we do not want multiple head columns 832 //point to a single column in the intermediate table, 833 //since then we would have to duplicate the column 834 //(and remove columns we did not point to at all) 835 binding_indexes.pop_back(); 836 } 837 } 838 else { 839 aci.kind = ACK_UNBOUND_VAR; 840 aci.var_index = var_num; 841 } 842 } 843 else { 844 SASSERT(is_app(exp)); 845 if (!m_context.get_decl_util().is_numeral_ext(exp)) 846 throw default_exception("could not process non-numeral in Datalog engine"); 847 aci.kind=ACK_CONSTANT; 848 aci.constant=to_app(exp); 849 } 850 head_acis.push_back(aci); 851 } 852 SASSERT(head_acis.size()==head_len); 853 854 reg_idx new_head_reg; 855 make_assembling_code(r, head_pred, filtered_res, head_acis, new_head_reg, dealloc, acc); 856 857 //update the head relation 858 make_union(new_head_reg, head_reg, delta_reg, use_widening, acc); 859 if (dealloc) 860 make_dealloc_non_void(new_head_reg, acc); 861 } 862 863 // finish: 864 m_instruction_observer.finish_rule(); 865 } 866 add_unbound_columns_for_negation(rule * r,func_decl * pred,reg_idx & single_res,expr_ref_vector & single_res_expr,bool & dealloc,instruction_block & acc)867 void compiler::add_unbound_columns_for_negation(rule* r, func_decl* pred, reg_idx& single_res, expr_ref_vector& single_res_expr, 868 bool & dealloc, instruction_block & acc) { 869 uint_set pos_vars; 870 u_map<expr*> neg_vars; 871 unsigned pt_len = r->get_positive_tail_size(); 872 unsigned ut_len = r->get_uninterpreted_tail_size(); 873 874 // no negated predicates 875 if (pt_len == ut_len) 876 return; 877 878 // populate negative variables: 879 for (unsigned i = pt_len; i < ut_len; ++i) { 880 app * neg_tail = r->get_tail(i); 881 unsigned neg_len = neg_tail->get_num_args(); 882 for (unsigned j = 0; j < neg_len; ++j) { 883 expr * e = neg_tail->get_arg(j); 884 if (is_var(e)) { 885 unsigned idx = to_var(e)->get_idx(); 886 neg_vars.insert(idx, e); 887 } 888 } 889 } 890 // populate positive variables: 891 for (unsigned i = 0; i < single_res_expr.size(); ++i) { 892 expr* e = single_res_expr[i].get(); 893 if (is_var(e)) { 894 pos_vars.insert(to_var(e)->get_idx()); 895 } 896 } 897 // add negative variables that are not in positive 898 u_map<expr*>::iterator it = neg_vars.begin(), end = neg_vars.end(); 899 for (; it != end; ++it) { 900 unsigned v = it->m_key; 901 expr* e = it->m_value; 902 if (!pos_vars.contains(v)) { 903 single_res_expr.push_back(e); 904 make_add_unbound_column(r, v, pred, single_res, e->get_sort(), single_res, dealloc, acc); 905 TRACE("dl", tout << "Adding unbound column: " << mk_pp(e, m_context.get_manager()) << "\n";); 906 } 907 } 908 } 909 compile_rule_evaluation(rule * r,const pred2idx * input_deltas,reg_idx output_delta,bool use_widening,instruction_block & acc)910 void compiler::compile_rule_evaluation(rule * r, const pred2idx * input_deltas, 911 reg_idx output_delta, bool use_widening, instruction_block & acc) { 912 typedef std::pair<reg_idx, unsigned> tail_delta_info; //(delta register, tail index) 913 typedef svector<tail_delta_info> tail_delta_infos; 914 915 unsigned rule_len = r->get_uninterpreted_tail_size(); 916 reg_idx head_reg = m_pred_regs.find(r->get_decl()); 917 918 svector<reg_idx> tail_regs; 919 tail_delta_infos tail_deltas; 920 for(unsigned j=0;j<rule_len;j++) { 921 func_decl * tail_pred = r->get_tail(j)->get_decl(); 922 reg_idx tail_reg = m_pred_regs.find(tail_pred); 923 tail_regs.push_back(tail_reg); 924 925 if(input_deltas && !all_or_nothing_deltas()) { 926 reg_idx tail_delta_idx; 927 if(input_deltas->find(tail_pred, tail_delta_idx)) { 928 tail_deltas.push_back(tail_delta_info(tail_delta_idx, j)); 929 } 930 } 931 } 932 933 if(!input_deltas || all_or_nothing_deltas()) { 934 compile_rule_evaluation_run(r, head_reg, tail_regs.data(), output_delta, use_widening, acc); 935 } 936 else { 937 tail_delta_infos::iterator tdit = tail_deltas.begin(); 938 tail_delta_infos::iterator tdend = tail_deltas.end(); 939 for(; tdit!=tdend; ++tdit) { 940 tail_delta_info tdinfo = *tdit; 941 flet<reg_idx> flet_tail_reg(tail_regs[tdinfo.second], tdinfo.first); 942 compile_rule_evaluation_run(r, head_reg, tail_regs.data(), output_delta, use_widening, acc); 943 } 944 } 945 } 946 947 class cycle_breaker 948 { 949 typedef func_decl * T; 950 typedef rule_dependencies::item_set item_set; //set of T 951 952 rule_dependencies & m_deps; 953 item_set & m_removed; 954 svector<T> m_stack; 955 ast_mark m_stack_content; 956 ast_mark m_visited; 957 traverse(T v)958 void traverse(T v) { 959 SASSERT(!m_stack_content.is_marked(v)); 960 if(m_visited.is_marked(v) || m_removed.contains(v)) { 961 return; 962 } 963 964 m_stack.push_back(v); 965 m_stack_content.mark(v, true); 966 m_visited.mark(v, true); 967 968 const item_set & deps = m_deps.get_deps(v); 969 item_set::iterator it = deps.begin(); 970 item_set::iterator end = deps.end(); 971 for(; it!=end; ++it) { 972 T d = *it; 973 if(m_stack_content.is_marked(d)) { 974 //TODO: find the best vertex to remove in the cycle 975 m_removed.insert(v); 976 break; 977 } 978 traverse(d); 979 } 980 SASSERT(m_stack.back()==v); 981 982 m_stack.pop_back(); 983 m_stack_content.mark(v, false); 984 } 985 986 public: cycle_breaker(rule_dependencies & deps,item_set & removed)987 cycle_breaker(rule_dependencies & deps, item_set & removed) 988 : m_deps(deps), m_removed(removed) { SASSERT(removed.empty()); } 989 operator ()()990 void operator()() { 991 rule_dependencies::iterator it = m_deps.begin(); 992 rule_dependencies::iterator end = m_deps.end(); 993 for(; it!=end; ++it) { 994 T v = it->m_key; 995 traverse(v); 996 } 997 m_deps.remove(m_removed); 998 } 999 }; 1000 detect_chains(const func_decl_set & preds,func_decl_vector & ordered_preds,func_decl_set & global_deltas)1001 void compiler::detect_chains(const func_decl_set & preds, func_decl_vector & ordered_preds, 1002 func_decl_set & global_deltas) { 1003 1004 SASSERT(ordered_preds.empty()); 1005 SASSERT(global_deltas.empty()); 1006 1007 rule_dependencies deps(m_rule_set.get_dependencies()); 1008 deps.restrict_dependencies(preds); 1009 cycle_breaker(deps, global_deltas)(); 1010 VERIFY( deps.sort_deps(ordered_preds) ); 1011 1012 //the predicates that were removed to get acyclic induced subgraph are put last 1013 //so that all their local input deltas are already populated 1014 func_decl_set::iterator gdit = global_deltas.begin(); 1015 func_decl_set::iterator gend = global_deltas.end(); 1016 for(; gdit!=gend; ++gdit) { 1017 ordered_preds.push_back(*gdit); 1018 } 1019 } 1020 compile_preds(const func_decl_vector & head_preds,const func_decl_set & widened_preds,const pred2idx * input_deltas,const pred2idx & output_deltas,instruction_block & acc)1021 void compiler::compile_preds(const func_decl_vector & head_preds, const func_decl_set & widened_preds, 1022 const pred2idx * input_deltas, const pred2idx & output_deltas, instruction_block & acc) { 1023 func_decl_vector::const_iterator hpit = head_preds.begin(); 1024 func_decl_vector::const_iterator hpend = head_preds.end(); 1025 for(; hpit!=hpend; ++hpit) { 1026 func_decl * head_pred = *hpit; 1027 1028 bool widen_predicate_in_loop = widened_preds.contains(head_pred); 1029 1030 reg_idx d_head_reg; //output delta for the initial rule execution 1031 if(!output_deltas.find(head_pred, d_head_reg)) { 1032 d_head_reg = execution_context::void_register; 1033 } 1034 1035 const rule_vector & pred_rules = m_rule_set.get_predicate_rules(head_pred); 1036 rule_vector::const_iterator rit = pred_rules.begin(); 1037 rule_vector::const_iterator rend = pred_rules.end(); 1038 for(; rit!=rend; ++rit) { 1039 rule * r = *rit; 1040 SASSERT(head_pred==r->get_decl()); 1041 1042 compile_rule_evaluation(r, input_deltas, d_head_reg, widen_predicate_in_loop, acc); 1043 } 1044 } 1045 } 1046 compile_preds_init(const func_decl_vector & head_preds,const func_decl_set & widened_preds,const pred2idx * input_deltas,const pred2idx & output_deltas,instruction_block & acc)1047 void compiler::compile_preds_init(const func_decl_vector & head_preds, const func_decl_set & widened_preds, 1048 const pred2idx * input_deltas, const pred2idx & output_deltas, instruction_block & acc) { 1049 func_decl_vector::const_iterator hpit = head_preds.begin(); 1050 func_decl_vector::const_iterator hpend = head_preds.end(); 1051 reg_idx void_reg = execution_context::void_register; 1052 for(; hpit!=hpend; ++hpit) { 1053 func_decl * head_pred = *hpit; 1054 const rule_vector & pred_rules = m_rule_set.get_predicate_rules(head_pred); 1055 rule_vector::const_iterator rit = pred_rules.begin(); 1056 rule_vector::const_iterator rend = pred_rules.end(); 1057 unsigned stratum = m_rule_set.get_predicate_strat(head_pred); 1058 1059 for(; rit != rend; ++rit) { 1060 rule * r = *rit; 1061 SASSERT(head_pred==r->get_decl()); 1062 1063 for (unsigned i = 0; i < r->get_uninterpreted_tail_size(); ++i) { 1064 unsigned stratum1 = m_rule_set.get_predicate_strat(r->get_decl(i)); 1065 if (stratum1 >= stratum) { 1066 goto next_loop; 1067 } 1068 } 1069 compile_rule_evaluation(r, input_deltas, void_reg, false, acc); 1070 next_loop: 1071 ; 1072 } 1073 1074 reg_idx d_head_reg; 1075 if (output_deltas.find(head_pred, d_head_reg)) { 1076 acc.push_back(instruction::mk_clone(m_pred_regs.find(head_pred), d_head_reg)); 1077 } 1078 } 1079 } 1080 make_inloop_delta_transition(const pred2idx & global_head_deltas,const pred2idx & global_tail_deltas,const pred2idx & local_deltas,instruction_block & acc)1081 void compiler::make_inloop_delta_transition(const pred2idx & global_head_deltas, 1082 const pred2idx & global_tail_deltas, const pred2idx & local_deltas, instruction_block & acc) { 1083 //move global head deltas into tail ones 1084 pred2idx::iterator gdit = global_head_deltas.begin(); 1085 pred2idx::iterator gend = global_head_deltas.end(); 1086 for(; gdit!=gend; ++gdit) { 1087 func_decl * pred = gdit->m_key; 1088 reg_idx head_reg = gdit->m_value; 1089 reg_idx tail_reg = global_tail_deltas.find(pred); 1090 acc.push_back(instruction::mk_move(head_reg, tail_reg)); 1091 } 1092 //empty local deltas 1093 pred2idx::iterator lit = local_deltas.begin(); 1094 pred2idx::iterator lend = local_deltas.end(); 1095 for(; lit!=lend; ++lit) { 1096 acc.push_back(instruction::mk_dealloc(lit->m_value)); 1097 } 1098 } 1099 compile_loop(const func_decl_vector & head_preds,const func_decl_set & widened_preds,const pred2idx & global_head_deltas,const pred2idx & global_tail_deltas,const pred2idx & local_deltas,instruction_block & acc)1100 void compiler::compile_loop(const func_decl_vector & head_preds, const func_decl_set & widened_preds, 1101 const pred2idx & global_head_deltas, const pred2idx & global_tail_deltas, 1102 const pred2idx & local_deltas, instruction_block & acc) { 1103 instruction_block * loop_body = alloc(instruction_block); 1104 loop_body->set_observer(&m_instruction_observer); 1105 1106 pred2idx all_head_deltas(global_head_deltas); 1107 unite_disjoint_maps(all_head_deltas, local_deltas); 1108 pred2idx all_tail_deltas(global_tail_deltas); 1109 unite_disjoint_maps(all_tail_deltas, local_deltas); 1110 1111 //generate code for the iterative fixpoint search 1112 //The order in which we iterate the preds_vector matters, since rules can depend on 1113 //deltas generated earlier in the same iteration. 1114 compile_preds(head_preds, widened_preds, &all_tail_deltas, all_head_deltas, *loop_body); 1115 1116 svector<reg_idx> loop_control_regs; //loop is controlled by global src regs 1117 collect_map_range(loop_control_regs, global_tail_deltas); 1118 //move target deltas into source deltas at the end of the loop 1119 //and clear local deltas 1120 make_inloop_delta_transition(global_head_deltas, global_tail_deltas, local_deltas, *loop_body); 1121 1122 loop_body->set_observer(nullptr); 1123 acc.push_back(instruction::mk_while_loop(loop_control_regs.size(), 1124 loop_control_regs.data(), loop_body)); 1125 } 1126 compile_dependent_rules(const func_decl_set & head_preds,const pred2idx * input_deltas,const pred2idx & output_deltas,bool add_saturation_marks,instruction_block & acc)1127 void compiler::compile_dependent_rules(const func_decl_set & head_preds, 1128 const pred2idx * input_deltas, const pred2idx & output_deltas, 1129 bool add_saturation_marks, instruction_block & acc) { 1130 1131 if (!output_deltas.empty()) { 1132 func_decl_set::iterator hpit = head_preds.begin(); 1133 func_decl_set::iterator hpend = head_preds.end(); 1134 for(; hpit!=hpend; ++hpit) { 1135 if(output_deltas.contains(*hpit)) { 1136 //we do not support retrieving deltas for rules that are inside a recursive 1137 //stratum, since we would have to maintain this 'global' delta through the loop 1138 //iterations 1139 NOT_IMPLEMENTED_YET(); 1140 } 1141 } 1142 } 1143 1144 func_decl_vector preds_vector; 1145 func_decl_set global_deltas_dummy; 1146 1147 detect_chains(head_preds, preds_vector, global_deltas_dummy); 1148 1149 /* 1150 FIXME: right now we use all preds as global deltas for correctness purposes 1151 func_decl_set local_deltas(head_preds); 1152 set_difference(local_deltas, global_deltas); 1153 */ 1154 func_decl_set local_deltas; 1155 func_decl_set global_deltas(head_preds); 1156 1157 pred2idx d_global_src; //these deltas serve as sources of tuples for rule evaluation inside the loop 1158 get_fresh_registers(global_deltas, d_global_src); 1159 pred2idx d_global_tgt; //these deltas are targets for new tuples in rule evaluation inside the loop 1160 get_fresh_registers(global_deltas, d_global_tgt); 1161 pred2idx d_local; 1162 get_fresh_registers(local_deltas, d_local); 1163 1164 pred2idx d_all_src(d_global_src); //src together with local deltas 1165 unite_disjoint_maps(d_all_src, d_local); 1166 pred2idx d_all_tgt(d_global_tgt); //tgt together with local deltas 1167 unite_disjoint_maps(d_all_tgt, d_local); 1168 1169 1170 func_decl_set empty_func_decl_set; 1171 1172 //generate code for the initial run 1173 // compile_preds(preds_vector, empty_func_decl_set, input_deltas, d_global_src, acc); 1174 compile_preds_init(preds_vector, empty_func_decl_set, input_deltas, d_global_src, acc); 1175 1176 if (compile_with_widening()) { 1177 compile_loop(preds_vector, global_deltas, d_global_tgt, d_global_src, d_local, acc); 1178 } 1179 else { 1180 compile_loop(preds_vector, empty_func_decl_set, d_global_tgt, d_global_src, d_local, acc); 1181 } 1182 1183 1184 if(add_saturation_marks) { 1185 //after the loop finishes, all predicates in the group are saturated, 1186 //so we may mark them as such 1187 func_decl_set::iterator fdit = head_preds.begin(); 1188 func_decl_set::iterator fdend = head_preds.end(); 1189 for(; fdit!=fdend; ++fdit) { 1190 acc.push_back(instruction::mk_mark_saturated(m_context.get_manager(), *fdit)); 1191 } 1192 } 1193 } 1194 is_nonrecursive_stratum(const func_decl_set & preds) const1195 bool compiler::is_nonrecursive_stratum(const func_decl_set & preds) const { 1196 SASSERT(preds.size()>0); 1197 if(preds.size()>1) { 1198 return false; 1199 } 1200 func_decl * head_pred = *preds.begin(); 1201 const rule_vector & rules = m_rule_set.get_predicate_rules(head_pred); 1202 rule_vector::const_iterator it = rules.begin(); 1203 rule_vector::const_iterator end = rules.end(); 1204 for(; it!=end; ++it) { 1205 //it is sufficient to check just for presence of the first head predicate, 1206 //since if the rules are recursive and their heads are strongly connected by dependence, 1207 //this predicate must appear in some tail 1208 if((*it)->is_in_tail(head_pred)) { 1209 return false; 1210 } 1211 } 1212 return true; 1213 } 1214 compile_nonrecursive_stratum(const func_decl_set & preds,const pred2idx * input_deltas,const pred2idx & output_deltas,bool add_saturation_marks,instruction_block & acc)1215 void compiler::compile_nonrecursive_stratum(const func_decl_set & preds, 1216 const pred2idx * input_deltas, const pred2idx & output_deltas, 1217 bool add_saturation_marks, instruction_block & acc) { 1218 //non-recursive stratum always has just one head predicate 1219 SASSERT(preds.size()==1); 1220 SASSERT(is_nonrecursive_stratum(preds)); 1221 func_decl * head_pred = *preds.begin(); 1222 const rule_vector & rules = m_rule_set.get_predicate_rules(head_pred); 1223 1224 1225 1226 reg_idx output_delta; 1227 if (!output_deltas.find(head_pred, output_delta)) { 1228 output_delta = execution_context::void_register; 1229 } 1230 1231 rule_vector::const_iterator it = rules.begin(); 1232 rule_vector::const_iterator end = rules.end(); 1233 for (; it != end; ++it) { 1234 rule * r = *it; 1235 SASSERT(r->get_decl()==head_pred); 1236 1237 compile_rule_evaluation(r, input_deltas, output_delta, false, acc); 1238 } 1239 1240 if (add_saturation_marks) { 1241 //now the predicate is saturated, so we may mark it as such 1242 acc.push_back(instruction::mk_mark_saturated(m_context.get_manager(), head_pred)); 1243 } 1244 } 1245 all_saturated(const func_decl_set & preds) const1246 bool compiler::all_saturated(const func_decl_set & preds) const { 1247 func_decl_set::iterator fdit = preds.begin(); 1248 func_decl_set::iterator fdend = preds.end(); 1249 for(; fdit!=fdend; ++fdit) { 1250 if(!m_context.get_rel_context()->get_rmanager().is_saturated(*fdit)) { 1251 return false; 1252 } 1253 } 1254 return true; 1255 } 1256 compile_strats(const rule_stratifier & stratifier,const pred2idx * input_deltas,const pred2idx & output_deltas,bool add_saturation_marks,instruction_block & acc)1257 void compiler::compile_strats(const rule_stratifier & stratifier, 1258 const pred2idx * input_deltas, const pred2idx & output_deltas, 1259 bool add_saturation_marks, instruction_block & acc) { 1260 rule_set::pred_set_vector strats = stratifier.get_strats(); 1261 rule_set::pred_set_vector::const_iterator sit = strats.begin(); 1262 rule_set::pred_set_vector::const_iterator send = strats.end(); 1263 for(; sit!=send; ++sit) { 1264 func_decl_set & strat_preds = **sit; 1265 1266 if (all_saturated(strat_preds)) { 1267 //all predicates in stratum are saturated, so no need to compile rules for them 1268 continue; 1269 } 1270 1271 TRACE("dl", 1272 tout << "Stratum: "; 1273 func_decl_set::iterator pit = strat_preds.begin(); 1274 func_decl_set::iterator pend = strat_preds.end(); 1275 for(; pit!=pend; ++pit) { 1276 func_decl * pred = *pit; 1277 tout << pred->get_name() << " "; 1278 } 1279 tout << "\n"; 1280 ); 1281 1282 if (is_nonrecursive_stratum(strat_preds)) { 1283 //this stratum contains just a single non-recursive rule 1284 compile_nonrecursive_stratum(strat_preds, input_deltas, output_deltas, add_saturation_marks, acc); 1285 } 1286 else { 1287 compile_dependent_rules(strat_preds, input_deltas, output_deltas, 1288 add_saturation_marks, acc); 1289 } 1290 } 1291 } 1292 do_compilation(instruction_block & execution_code,instruction_block & termination_code)1293 void compiler::do_compilation(instruction_block & execution_code, 1294 instruction_block & termination_code) { 1295 1296 unsigned rule_cnt=m_rule_set.get_num_rules(); 1297 if(rule_cnt==0) { 1298 return; 1299 } 1300 1301 instruction_block & acc = execution_code; 1302 acc.set_observer(&m_instruction_observer); 1303 1304 1305 //load predicate data 1306 for(unsigned i=0;i<rule_cnt;i++) { 1307 const rule * r = m_rule_set.get_rule(i); 1308 ensure_predicate_loaded(r->get_decl(), acc); 1309 1310 unsigned rule_len = r->get_uninterpreted_tail_size(); 1311 for(unsigned j=0;j<rule_len;j++) { 1312 ensure_predicate_loaded(r->get_tail(j)->get_decl(), acc); 1313 } 1314 } 1315 1316 pred2idx empty_pred2idx_map; 1317 1318 compile_strats(m_rule_set.get_stratifier(), static_cast<pred2idx *>(nullptr), 1319 empty_pred2idx_map, true, execution_code); 1320 1321 1322 1323 //store predicate data 1324 pred2idx::iterator pit = m_pred_regs.begin(); 1325 pred2idx::iterator pend = m_pred_regs.end(); 1326 for(; pit!=pend; ++pit) { 1327 pred2idx::key_data & e = *pit; 1328 func_decl * pred = e.m_key; 1329 reg_idx reg = e.m_value; 1330 termination_code.push_back(instruction::mk_store(m_context.get_manager(), pred, reg)); 1331 } 1332 1333 acc.set_observer(nullptr); 1334 1335 TRACE("dl", execution_code.display(execution_context(m_context), tout);); 1336 } 1337 1338 1339 } 1340 1341