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.c_ptr(), 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.c_ptr(), 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.c_ptr(), 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.c_ptr(), 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.c_ptr(), 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.c_ptr(), 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.c_ptr(), 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.c_ptr())); 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.c_ptr(), neg_cols.c_ptr())); 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.c_ptr()), 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.c_ptr()); 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 ast_manager& m = m_context.get_manager(); 872 unsigned pt_len = r->get_positive_tail_size(); 873 unsigned ut_len = r->get_uninterpreted_tail_size(); 874 875 // no negated predicates 876 if (pt_len == ut_len) 877 return; 878 879 // populate negative variables: 880 for (unsigned i = pt_len; i < ut_len; ++i) { 881 app * neg_tail = r->get_tail(i); 882 unsigned neg_len = neg_tail->get_num_args(); 883 for (unsigned j = 0; j < neg_len; ++j) { 884 expr * e = neg_tail->get_arg(j); 885 if (is_var(e)) { 886 unsigned idx = to_var(e)->get_idx(); 887 neg_vars.insert(idx, e); 888 } 889 } 890 } 891 // populate positive variables: 892 for (unsigned i = 0; i < single_res_expr.size(); ++i) { 893 expr* e = single_res_expr[i].get(); 894 if (is_var(e)) { 895 pos_vars.insert(to_var(e)->get_idx()); 896 } 897 } 898 // add negative variables that are not in positive 899 u_map<expr*>::iterator it = neg_vars.begin(), end = neg_vars.end(); 900 for (; it != end; ++it) { 901 unsigned v = it->m_key; 902 expr* e = it->m_value; 903 if (!pos_vars.contains(v)) { 904 single_res_expr.push_back(e); 905 make_add_unbound_column(r, v, pred, single_res, m.get_sort(e), single_res, dealloc, acc); 906 TRACE("dl", tout << "Adding unbound column: " << mk_pp(e, m) << "\n";); 907 } 908 } 909 } 910 compile_rule_evaluation(rule * r,const pred2idx * input_deltas,reg_idx output_delta,bool use_widening,instruction_block & acc)911 void compiler::compile_rule_evaluation(rule * r, const pred2idx * input_deltas, 912 reg_idx output_delta, bool use_widening, instruction_block & acc) { 913 typedef std::pair<reg_idx, unsigned> tail_delta_info; //(delta register, tail index) 914 typedef svector<tail_delta_info> tail_delta_infos; 915 916 unsigned rule_len = r->get_uninterpreted_tail_size(); 917 reg_idx head_reg = m_pred_regs.find(r->get_decl()); 918 919 svector<reg_idx> tail_regs; 920 tail_delta_infos tail_deltas; 921 for(unsigned j=0;j<rule_len;j++) { 922 func_decl * tail_pred = r->get_tail(j)->get_decl(); 923 reg_idx tail_reg = m_pred_regs.find(tail_pred); 924 tail_regs.push_back(tail_reg); 925 926 if(input_deltas && !all_or_nothing_deltas()) { 927 reg_idx tail_delta_idx; 928 if(input_deltas->find(tail_pred, tail_delta_idx)) { 929 tail_deltas.push_back(tail_delta_info(tail_delta_idx, j)); 930 } 931 } 932 } 933 934 if(!input_deltas || all_or_nothing_deltas()) { 935 compile_rule_evaluation_run(r, head_reg, tail_regs.c_ptr(), output_delta, use_widening, acc); 936 } 937 else { 938 tail_delta_infos::iterator tdit = tail_deltas.begin(); 939 tail_delta_infos::iterator tdend = tail_deltas.end(); 940 for(; tdit!=tdend; ++tdit) { 941 tail_delta_info tdinfo = *tdit; 942 flet<reg_idx> flet_tail_reg(tail_regs[tdinfo.second], tdinfo.first); 943 compile_rule_evaluation_run(r, head_reg, tail_regs.c_ptr(), output_delta, use_widening, acc); 944 } 945 } 946 } 947 948 class cycle_breaker 949 { 950 typedef func_decl * T; 951 typedef rule_dependencies::item_set item_set; //set of T 952 953 rule_dependencies & m_deps; 954 item_set & m_removed; 955 svector<T> m_stack; 956 ast_mark m_stack_content; 957 ast_mark m_visited; 958 traverse(T v)959 void traverse(T v) { 960 SASSERT(!m_stack_content.is_marked(v)); 961 if(m_visited.is_marked(v) || m_removed.contains(v)) { 962 return; 963 } 964 965 m_stack.push_back(v); 966 m_stack_content.mark(v, true); 967 m_visited.mark(v, true); 968 969 const item_set & deps = m_deps.get_deps(v); 970 item_set::iterator it = deps.begin(); 971 item_set::iterator end = deps.end(); 972 for(; it!=end; ++it) { 973 T d = *it; 974 if(m_stack_content.is_marked(d)) { 975 //TODO: find the best vertex to remove in the cycle 976 m_removed.insert(v); 977 break; 978 } 979 traverse(d); 980 } 981 SASSERT(m_stack.back()==v); 982 983 m_stack.pop_back(); 984 m_stack_content.mark(v, false); 985 } 986 987 public: cycle_breaker(rule_dependencies & deps,item_set & removed)988 cycle_breaker(rule_dependencies & deps, item_set & removed) 989 : m_deps(deps), m_removed(removed) { SASSERT(removed.empty()); } 990 operator ()()991 void operator()() { 992 rule_dependencies::iterator it = m_deps.begin(); 993 rule_dependencies::iterator end = m_deps.end(); 994 for(; it!=end; ++it) { 995 T v = it->m_key; 996 traverse(v); 997 } 998 m_deps.remove(m_removed); 999 } 1000 }; 1001 detect_chains(const func_decl_set & preds,func_decl_vector & ordered_preds,func_decl_set & global_deltas)1002 void compiler::detect_chains(const func_decl_set & preds, func_decl_vector & ordered_preds, 1003 func_decl_set & global_deltas) { 1004 1005 SASSERT(ordered_preds.empty()); 1006 SASSERT(global_deltas.empty()); 1007 1008 rule_dependencies deps(m_rule_set.get_dependencies()); 1009 deps.restrict_dependencies(preds); 1010 cycle_breaker(deps, global_deltas)(); 1011 VERIFY( deps.sort_deps(ordered_preds) ); 1012 1013 //the predicates that were removed to get acyclic induced subgraph are put last 1014 //so that all their local input deltas are already populated 1015 func_decl_set::iterator gdit = global_deltas.begin(); 1016 func_decl_set::iterator gend = global_deltas.end(); 1017 for(; gdit!=gend; ++gdit) { 1018 ordered_preds.push_back(*gdit); 1019 } 1020 } 1021 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)1022 void compiler::compile_preds(const func_decl_vector & head_preds, const func_decl_set & widened_preds, 1023 const pred2idx * input_deltas, const pred2idx & output_deltas, instruction_block & acc) { 1024 func_decl_vector::const_iterator hpit = head_preds.begin(); 1025 func_decl_vector::const_iterator hpend = head_preds.end(); 1026 for(; hpit!=hpend; ++hpit) { 1027 func_decl * head_pred = *hpit; 1028 1029 bool widen_predicate_in_loop = widened_preds.contains(head_pred); 1030 1031 reg_idx d_head_reg; //output delta for the initial rule execution 1032 if(!output_deltas.find(head_pred, d_head_reg)) { 1033 d_head_reg = execution_context::void_register; 1034 } 1035 1036 const rule_vector & pred_rules = m_rule_set.get_predicate_rules(head_pred); 1037 rule_vector::const_iterator rit = pred_rules.begin(); 1038 rule_vector::const_iterator rend = pred_rules.end(); 1039 for(; rit!=rend; ++rit) { 1040 rule * r = *rit; 1041 SASSERT(head_pred==r->get_decl()); 1042 1043 compile_rule_evaluation(r, input_deltas, d_head_reg, widen_predicate_in_loop, acc); 1044 } 1045 } 1046 } 1047 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)1048 void compiler::compile_preds_init(const func_decl_vector & head_preds, const func_decl_set & widened_preds, 1049 const pred2idx * input_deltas, const pred2idx & output_deltas, instruction_block & acc) { 1050 func_decl_vector::const_iterator hpit = head_preds.begin(); 1051 func_decl_vector::const_iterator hpend = head_preds.end(); 1052 reg_idx void_reg = execution_context::void_register; 1053 for(; hpit!=hpend; ++hpit) { 1054 func_decl * head_pred = *hpit; 1055 const rule_vector & pred_rules = m_rule_set.get_predicate_rules(head_pred); 1056 rule_vector::const_iterator rit = pred_rules.begin(); 1057 rule_vector::const_iterator rend = pred_rules.end(); 1058 unsigned stratum = m_rule_set.get_predicate_strat(head_pred); 1059 1060 for(; rit != rend; ++rit) { 1061 rule * r = *rit; 1062 SASSERT(head_pred==r->get_decl()); 1063 1064 for (unsigned i = 0; i < r->get_uninterpreted_tail_size(); ++i) { 1065 unsigned stratum1 = m_rule_set.get_predicate_strat(r->get_decl(i)); 1066 if (stratum1 >= stratum) { 1067 goto next_loop; 1068 } 1069 } 1070 compile_rule_evaluation(r, input_deltas, void_reg, false, acc); 1071 next_loop: 1072 ; 1073 } 1074 1075 reg_idx d_head_reg; 1076 if (output_deltas.find(head_pred, d_head_reg)) { 1077 acc.push_back(instruction::mk_clone(m_pred_regs.find(head_pred), d_head_reg)); 1078 } 1079 } 1080 } 1081 make_inloop_delta_transition(const pred2idx & global_head_deltas,const pred2idx & global_tail_deltas,const pred2idx & local_deltas,instruction_block & acc)1082 void compiler::make_inloop_delta_transition(const pred2idx & global_head_deltas, 1083 const pred2idx & global_tail_deltas, const pred2idx & local_deltas, instruction_block & acc) { 1084 //move global head deltas into tail ones 1085 pred2idx::iterator gdit = global_head_deltas.begin(); 1086 pred2idx::iterator gend = global_head_deltas.end(); 1087 for(; gdit!=gend; ++gdit) { 1088 func_decl * pred = gdit->m_key; 1089 reg_idx head_reg = gdit->m_value; 1090 reg_idx tail_reg = global_tail_deltas.find(pred); 1091 acc.push_back(instruction::mk_move(head_reg, tail_reg)); 1092 } 1093 //empty local deltas 1094 pred2idx::iterator lit = local_deltas.begin(); 1095 pred2idx::iterator lend = local_deltas.end(); 1096 for(; lit!=lend; ++lit) { 1097 acc.push_back(instruction::mk_dealloc(lit->m_value)); 1098 } 1099 } 1100 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)1101 void compiler::compile_loop(const func_decl_vector & head_preds, const func_decl_set & widened_preds, 1102 const pred2idx & global_head_deltas, const pred2idx & global_tail_deltas, 1103 const pred2idx & local_deltas, instruction_block & acc) { 1104 instruction_block * loop_body = alloc(instruction_block); 1105 loop_body->set_observer(&m_instruction_observer); 1106 1107 pred2idx all_head_deltas(global_head_deltas); 1108 unite_disjoint_maps(all_head_deltas, local_deltas); 1109 pred2idx all_tail_deltas(global_tail_deltas); 1110 unite_disjoint_maps(all_tail_deltas, local_deltas); 1111 1112 //generate code for the iterative fixpoint search 1113 //The order in which we iterate the preds_vector matters, since rules can depend on 1114 //deltas generated earlier in the same iteration. 1115 compile_preds(head_preds, widened_preds, &all_tail_deltas, all_head_deltas, *loop_body); 1116 1117 svector<reg_idx> loop_control_regs; //loop is controlled by global src regs 1118 collect_map_range(loop_control_regs, global_tail_deltas); 1119 //move target deltas into source deltas at the end of the loop 1120 //and clear local deltas 1121 make_inloop_delta_transition(global_head_deltas, global_tail_deltas, local_deltas, *loop_body); 1122 1123 loop_body->set_observer(nullptr); 1124 acc.push_back(instruction::mk_while_loop(loop_control_regs.size(), 1125 loop_control_regs.c_ptr(), loop_body)); 1126 } 1127 compile_dependent_rules(const func_decl_set & head_preds,const pred2idx * input_deltas,const pred2idx & output_deltas,bool add_saturation_marks,instruction_block & acc)1128 void compiler::compile_dependent_rules(const func_decl_set & head_preds, 1129 const pred2idx * input_deltas, const pred2idx & output_deltas, 1130 bool add_saturation_marks, instruction_block & acc) { 1131 1132 if (!output_deltas.empty()) { 1133 func_decl_set::iterator hpit = head_preds.begin(); 1134 func_decl_set::iterator hpend = head_preds.end(); 1135 for(; hpit!=hpend; ++hpit) { 1136 if(output_deltas.contains(*hpit)) { 1137 //we do not support retrieving deltas for rules that are inside a recursive 1138 //stratum, since we would have to maintain this 'global' delta through the loop 1139 //iterations 1140 NOT_IMPLEMENTED_YET(); 1141 } 1142 } 1143 } 1144 1145 func_decl_vector preds_vector; 1146 func_decl_set global_deltas_dummy; 1147 1148 detect_chains(head_preds, preds_vector, global_deltas_dummy); 1149 1150 /* 1151 FIXME: right now we use all preds as global deltas for correctness purposes 1152 func_decl_set local_deltas(head_preds); 1153 set_difference(local_deltas, global_deltas); 1154 */ 1155 func_decl_set local_deltas; 1156 func_decl_set global_deltas(head_preds); 1157 1158 pred2idx d_global_src; //these deltas serve as sources of tuples for rule evaluation inside the loop 1159 get_fresh_registers(global_deltas, d_global_src); 1160 pred2idx d_global_tgt; //these deltas are targets for new tuples in rule evaluation inside the loop 1161 get_fresh_registers(global_deltas, d_global_tgt); 1162 pred2idx d_local; 1163 get_fresh_registers(local_deltas, d_local); 1164 1165 pred2idx d_all_src(d_global_src); //src together with local deltas 1166 unite_disjoint_maps(d_all_src, d_local); 1167 pred2idx d_all_tgt(d_global_tgt); //tgt together with local deltas 1168 unite_disjoint_maps(d_all_tgt, d_local); 1169 1170 1171 func_decl_set empty_func_decl_set; 1172 1173 //generate code for the initial run 1174 // compile_preds(preds_vector, empty_func_decl_set, input_deltas, d_global_src, acc); 1175 compile_preds_init(preds_vector, empty_func_decl_set, input_deltas, d_global_src, acc); 1176 1177 if (compile_with_widening()) { 1178 compile_loop(preds_vector, global_deltas, d_global_tgt, d_global_src, d_local, acc); 1179 } 1180 else { 1181 compile_loop(preds_vector, empty_func_decl_set, d_global_tgt, d_global_src, d_local, acc); 1182 } 1183 1184 1185 if(add_saturation_marks) { 1186 //after the loop finishes, all predicates in the group are saturated, 1187 //so we may mark them as such 1188 func_decl_set::iterator fdit = head_preds.begin(); 1189 func_decl_set::iterator fdend = head_preds.end(); 1190 for(; fdit!=fdend; ++fdit) { 1191 acc.push_back(instruction::mk_mark_saturated(m_context.get_manager(), *fdit)); 1192 } 1193 } 1194 } 1195 is_nonrecursive_stratum(const func_decl_set & preds) const1196 bool compiler::is_nonrecursive_stratum(const func_decl_set & preds) const { 1197 SASSERT(preds.size()>0); 1198 if(preds.size()>1) { 1199 return false; 1200 } 1201 func_decl * head_pred = *preds.begin(); 1202 const rule_vector & rules = m_rule_set.get_predicate_rules(head_pred); 1203 rule_vector::const_iterator it = rules.begin(); 1204 rule_vector::const_iterator end = rules.end(); 1205 for(; it!=end; ++it) { 1206 //it is sufficient to check just for presence of the first head predicate, 1207 //since if the rules are recursive and their heads are strongly connected by dependence, 1208 //this predicate must appear in some tail 1209 if((*it)->is_in_tail(head_pred)) { 1210 return false; 1211 } 1212 } 1213 return true; 1214 } 1215 compile_nonrecursive_stratum(const func_decl_set & preds,const pred2idx * input_deltas,const pred2idx & output_deltas,bool add_saturation_marks,instruction_block & acc)1216 void compiler::compile_nonrecursive_stratum(const func_decl_set & preds, 1217 const pred2idx * input_deltas, const pred2idx & output_deltas, 1218 bool add_saturation_marks, instruction_block & acc) { 1219 //non-recursive stratum always has just one head predicate 1220 SASSERT(preds.size()==1); 1221 SASSERT(is_nonrecursive_stratum(preds)); 1222 func_decl * head_pred = *preds.begin(); 1223 const rule_vector & rules = m_rule_set.get_predicate_rules(head_pred); 1224 1225 1226 1227 reg_idx output_delta; 1228 if (!output_deltas.find(head_pred, output_delta)) { 1229 output_delta = execution_context::void_register; 1230 } 1231 1232 rule_vector::const_iterator it = rules.begin(); 1233 rule_vector::const_iterator end = rules.end(); 1234 for (; it != end; ++it) { 1235 rule * r = *it; 1236 SASSERT(r->get_decl()==head_pred); 1237 1238 compile_rule_evaluation(r, input_deltas, output_delta, false, acc); 1239 } 1240 1241 if (add_saturation_marks) { 1242 //now the predicate is saturated, so we may mark it as such 1243 acc.push_back(instruction::mk_mark_saturated(m_context.get_manager(), head_pred)); 1244 } 1245 } 1246 all_saturated(const func_decl_set & preds) const1247 bool compiler::all_saturated(const func_decl_set & preds) const { 1248 func_decl_set::iterator fdit = preds.begin(); 1249 func_decl_set::iterator fdend = preds.end(); 1250 for(; fdit!=fdend; ++fdit) { 1251 if(!m_context.get_rel_context()->get_rmanager().is_saturated(*fdit)) { 1252 return false; 1253 } 1254 } 1255 return true; 1256 } 1257 compile_strats(const rule_stratifier & stratifier,const pred2idx * input_deltas,const pred2idx & output_deltas,bool add_saturation_marks,instruction_block & acc)1258 void compiler::compile_strats(const rule_stratifier & stratifier, 1259 const pred2idx * input_deltas, const pred2idx & output_deltas, 1260 bool add_saturation_marks, instruction_block & acc) { 1261 rule_set::pred_set_vector strats = stratifier.get_strats(); 1262 rule_set::pred_set_vector::const_iterator sit = strats.begin(); 1263 rule_set::pred_set_vector::const_iterator send = strats.end(); 1264 for(; sit!=send; ++sit) { 1265 func_decl_set & strat_preds = **sit; 1266 1267 if (all_saturated(strat_preds)) { 1268 //all predicates in stratum are saturated, so no need to compile rules for them 1269 continue; 1270 } 1271 1272 TRACE("dl", 1273 tout << "Stratum: "; 1274 func_decl_set::iterator pit = strat_preds.begin(); 1275 func_decl_set::iterator pend = strat_preds.end(); 1276 for(; pit!=pend; ++pit) { 1277 func_decl * pred = *pit; 1278 tout << pred->get_name() << " "; 1279 } 1280 tout << "\n"; 1281 ); 1282 1283 if (is_nonrecursive_stratum(strat_preds)) { 1284 //this stratum contains just a single non-recursive rule 1285 compile_nonrecursive_stratum(strat_preds, input_deltas, output_deltas, add_saturation_marks, acc); 1286 } 1287 else { 1288 compile_dependent_rules(strat_preds, input_deltas, output_deltas, 1289 add_saturation_marks, acc); 1290 } 1291 } 1292 } 1293 do_compilation(instruction_block & execution_code,instruction_block & termination_code)1294 void compiler::do_compilation(instruction_block & execution_code, 1295 instruction_block & termination_code) { 1296 1297 unsigned rule_cnt=m_rule_set.get_num_rules(); 1298 if(rule_cnt==0) { 1299 return; 1300 } 1301 1302 instruction_block & acc = execution_code; 1303 acc.set_observer(&m_instruction_observer); 1304 1305 1306 //load predicate data 1307 for(unsigned i=0;i<rule_cnt;i++) { 1308 const rule * r = m_rule_set.get_rule(i); 1309 ensure_predicate_loaded(r->get_decl(), acc); 1310 1311 unsigned rule_len = r->get_uninterpreted_tail_size(); 1312 for(unsigned j=0;j<rule_len;j++) { 1313 ensure_predicate_loaded(r->get_tail(j)->get_decl(), acc); 1314 } 1315 } 1316 1317 pred2idx empty_pred2idx_map; 1318 1319 compile_strats(m_rule_set.get_stratifier(), static_cast<pred2idx *>(nullptr), 1320 empty_pred2idx_map, true, execution_code); 1321 1322 1323 1324 //store predicate data 1325 pred2idx::iterator pit = m_pred_regs.begin(); 1326 pred2idx::iterator pend = m_pred_regs.end(); 1327 for(; pit!=pend; ++pit) { 1328 pred2idx::key_data & e = *pit; 1329 func_decl * pred = e.m_key; 1330 reg_idx reg = e.m_value; 1331 termination_code.push_back(instruction::mk_store(m_context.get_manager(), pred, reg)); 1332 } 1333 1334 acc.set_observer(nullptr); 1335 1336 TRACE("dl", execution_code.display(execution_context(m_context), tout);); 1337 } 1338 1339 1340 } 1341 1342