1 /*++ 2 Copyright (c) 2006 Microsoft Corporation 3 4 Module Name: 5 6 dl_base.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 "ast/ast_pp.h" 22 #include "util/union_find.h" 23 #include "util/vector.h" 24 #include "muz/base/dl_context.h" 25 #include "muz/rel/dl_base.h" 26 #include "ast/rewriter/bool_rewriter.h" 27 #include "muz/rel/dl_relation_manager.h" 28 #include<sstream> 29 30 31 namespace datalog { 32 universal_delete(relation_base * ptr)33 void universal_delete(relation_base* ptr) { 34 ptr->deallocate(); 35 } 36 universal_delete(table_base * ptr)37 void universal_delete(table_base* ptr) { 38 ptr->deallocate(); 39 } 40 dealloc_ptr_vector_content(ptr_vector<relation_base> & v)41 void dealloc_ptr_vector_content(ptr_vector<relation_base> & v) { 42 for (auto& r : v) { 43 r->deallocate(); 44 } 45 } 46 get_renaming_args(const unsigned_vector & map,const relation_signature & orig_sig,expr_ref_vector & renaming_arg)47 void get_renaming_args(const unsigned_vector & map, const relation_signature & orig_sig, 48 expr_ref_vector & renaming_arg) { 49 ast_manager & m = renaming_arg.get_manager(); 50 unsigned sz = map.size(); 51 unsigned ofs = sz-1; 52 renaming_arg.resize(sz, static_cast<expr *>(nullptr)); 53 for (unsigned i = 0; i < sz; i++) { 54 if (map[i] != UINT_MAX) { 55 renaming_arg.set(ofs-i, m.mk_var(map[i], orig_sig[i])); 56 } 57 } 58 } 59 60 get_context_from_rel_manager(const relation_manager & rm)61 context & get_context_from_rel_manager(const relation_manager & rm) { 62 return rm.get_context(); 63 } 64 get_ast_manager_from_rel_manager(const relation_manager & rm)65 ast_manager & get_ast_manager_from_rel_manager(const relation_manager & rm) { 66 return rm.get_context().get_manager(); 67 } 68 69 #if DL_LEAK_HUNTING leak_guard_check(const symbol & s)70 void leak_guard_check(const symbol & s) { 71 } 72 #endif 73 output(ast_manager & m,std::ostream & out) const74 void relation_signature::output(ast_manager & m, std::ostream & out) const { 75 unsigned sz = size(); 76 out << "("; 77 for (unsigned i = 0; i < sz; i++) { 78 if (i != 0) out << ","; 79 out << mk_pp((*this)[i], m); 80 } 81 out << ")"; 82 } 83 84 relation_fact(context & ctx)85 relation_fact::relation_fact(context & ctx) : app_ref_vector(ctx.get_manager()) {} 86 reset()87 void relation_base::reset() { 88 ast_manager & m = get_plugin().get_ast_manager(); 89 app_ref bottom_ref(m.mk_false(), m); 90 scoped_ptr<relation_mutator_fn> reset_fn = get_manager().mk_filter_interpreted_fn(*this, bottom_ref); 91 if (!reset_fn) { 92 throw default_exception("filter function does not exist"); 93 } 94 (*reset_fn)(*this); 95 } 96 97 98 from_join(const table_signature & s1,const table_signature & s2,unsigned col_cnt,const unsigned * cols1,const unsigned * cols2,table_signature & result)99 void table_signature::from_join(const table_signature & s1, const table_signature & s2, unsigned col_cnt, 100 const unsigned * cols1, const unsigned * cols2, table_signature & result) { 101 result.reset(); 102 103 unsigned s1sz=s1.size(); 104 unsigned s2sz=s2.size(); 105 unsigned s1first_func=s1sz-s1.functional_columns(); 106 unsigned s2first_func=s2sz-s2.functional_columns(); 107 for (unsigned i=0; i<s1first_func; i++) { 108 result.push_back(s1[i]); 109 } 110 for (unsigned i=0; i<s2first_func; i++) { 111 result.push_back(s2[i]); 112 } 113 for (unsigned i=s1first_func; i<s1sz; i++) { 114 result.push_back(s1[i]); 115 } 116 for (unsigned i=s2first_func; i<s2sz; i++) { 117 result.push_back(s2[i]); 118 } 119 result.set_functional_columns(s1.functional_columns()+s2.functional_columns()); 120 } 121 from_project(const table_signature & src,unsigned col_cnt,const unsigned * removed_cols,table_signature & result)122 void table_signature::from_project(const table_signature & src, unsigned col_cnt, 123 const unsigned * removed_cols, table_signature & result) { 124 signature_base::from_project(src, col_cnt, removed_cols, result); 125 126 unsigned func_cnt = src.functional_columns(); 127 128 if (removed_cols==nullptr) { 129 result.set_functional_columns(func_cnt); 130 return; 131 } 132 133 unsigned first_src_fun = src.first_functional(); 134 if (removed_cols[0]<first_src_fun) { 135 //if we remove at least one non-functional column, all the columns in the result are non-functional 136 result.set_functional_columns(0); 137 } 138 else { 139 //all columns we are removing are functional 140 SASSERT(func_cnt>=col_cnt); 141 result.set_functional_columns(func_cnt-col_cnt); 142 } 143 } 144 from_project_with_reduce(const table_signature & src,unsigned col_cnt,const unsigned * removed_cols,table_signature & result)145 void table_signature::from_project_with_reduce(const table_signature & src, unsigned col_cnt, 146 const unsigned * removed_cols, table_signature & result) { 147 signature_base::from_project(src, col_cnt, removed_cols, result); 148 149 unsigned remaining_fun = src.functional_columns(); 150 unsigned first_src_fun = src.first_functional(); 151 for (int i=col_cnt-1; i>=0; i--) { 152 if (removed_cols[i]<first_src_fun) { 153 break; 154 } 155 remaining_fun--; 156 } 157 result.set_functional_columns(remaining_fun); 158 } 159 from_join_project(const table_signature & s1,const table_signature & s2,unsigned joined_col_cnt,const unsigned * cols1,const unsigned * cols2,unsigned removed_col_cnt,const unsigned * removed_cols,table_signature & result)160 void table_signature::from_join_project(const table_signature & s1, const table_signature & s2, 161 unsigned joined_col_cnt, const unsigned * cols1, const unsigned * cols2, unsigned removed_col_cnt, 162 const unsigned * removed_cols, table_signature & result) { 163 table_signature aux; 164 from_join(s1, s2, joined_col_cnt, cols1, cols2, aux); 165 166 //after the join the column order is 167 //(non-functional of s1)(non-functional of s2)(functional of s1)(functional of s2) 168 169 if (s1.functional_columns()==0 && s2.functional_columns()==0) { 170 from_project(aux, removed_col_cnt, removed_cols, result); 171 SASSERT(result.functional_columns()==0); 172 return; 173 } 174 175 unsigned join_sig_sz = s1.size()+s2.size(); 176 unsigned s1_first_func = s1.first_functional(); 177 unsigned s2_first_func = s2.first_functional(); 178 unsigned second_ofs = s1_first_func; 179 unsigned first_func_ofs = second_ofs + s2_first_func; 180 unsigned second_func_ofs = second_ofs + s1.functional_columns(); 181 182 svector<unsigned> remaining_in_equivalence_class; 183 remaining_in_equivalence_class.resize(join_sig_sz, 0); 184 bool merging_rows_can_happen = false; 185 186 union_find_default_ctx uf_ctx; 187 union_find<> uf(uf_ctx); //the numbers in uf correspond to column indexes after the join 188 for (unsigned i=0; i<join_sig_sz; i++) { 189 VERIFY(uf.mk_var() == i); 190 } 191 192 for (unsigned i=0; i<joined_col_cnt; i++) { 193 unsigned idx1 = (s1_first_func>cols1[i]) ? cols1[i] : (first_func_ofs+cols1[i]-s1_first_func); 194 unsigned idx2 = (s2_first_func>cols2[i]) ? (second_ofs+cols2[i]) : (second_func_ofs+cols2[i]-s2_first_func); 195 uf.merge(idx1, idx2); 196 } 197 for (unsigned i=0; i<first_func_ofs; i++) { //we only count the non-functional columns 198 remaining_in_equivalence_class[uf.find(i)]++; 199 } 200 201 for (unsigned i=0; i<removed_col_cnt; i++) { 202 unsigned rc = removed_cols[i]; 203 if (rc>=first_func_ofs) { 204 //removing functional columns won't make us merge rows 205 continue; 206 } 207 unsigned eq_class_idx = uf.find(rc); 208 if (remaining_in_equivalence_class[eq_class_idx]>1) { 209 remaining_in_equivalence_class[eq_class_idx]--; 210 } 211 else { 212 merging_rows_can_happen = true; 213 break; 214 } 215 } 216 217 if (merging_rows_can_happen) { 218 //this one marks all columns as non-functional 219 from_project(aux, removed_col_cnt, removed_cols, result); 220 SASSERT(result.functional_columns()==0); 221 } 222 else { 223 //this one preserves columns to be functional 224 from_project_with_reduce(aux, removed_col_cnt, removed_cols, result); 225 } 226 } 227 228 // ----------------------------------- 229 // 230 // table_base 231 // 232 // ----------------------------------- 233 234 //here we give generic implementation of table operations using iterators 235 empty() const236 bool table_base::empty() const { 237 return begin() == end(); 238 } 239 remove_facts(unsigned fact_cnt,const table_fact * facts)240 void table_base::remove_facts(unsigned fact_cnt, const table_fact * facts) { 241 for (unsigned i = 0; i < fact_cnt; i++) { 242 remove_fact(facts[i]); 243 } 244 } 245 remove_facts(unsigned fact_cnt,const table_element * facts)246 void table_base::remove_facts(unsigned fact_cnt, const table_element * facts) { 247 for (unsigned i = 0; i < fact_cnt; i++) { 248 remove_fact(facts + i*get_signature().size()); 249 } 250 } 251 252 reset()253 void table_base::reset() { 254 vector<table_fact> to_remove; 255 table_fact row; 256 for (auto& k : *this) { 257 k.get_fact(row); 258 to_remove.push_back(row); 259 } 260 remove_facts(to_remove.size(), to_remove.c_ptr()); 261 } 262 contains_fact(const table_fact & f) const263 bool table_base::contains_fact(const table_fact & f) const { 264 table_fact row; 265 for (auto const& k : *this) { 266 k.get_fact(row); 267 if (vectors_equal(row, f)) { 268 return true; 269 } 270 } 271 return false; 272 } 273 fetch_fact(table_fact & f) const274 bool table_base::fetch_fact(table_fact & f) const { 275 if (get_signature().functional_columns() == 0) { 276 return contains_fact(f); 277 } 278 else { 279 unsigned sig_sz = get_signature().size(); 280 unsigned non_func_cnt = sig_sz-get_signature().functional_columns(); 281 table_fact row; 282 for (auto& k : *this) { 283 k.get_fact(row); 284 bool differs = false; 285 for (unsigned i=0; i<non_func_cnt; i++) { 286 if (row[i]!=f[i]) { 287 differs = true; 288 } 289 } 290 if (differs) { 291 continue; 292 } 293 for (unsigned i=non_func_cnt; i<sig_sz; i++) { 294 f[i]=row[i]; 295 } 296 return true; 297 } 298 return false; 299 } 300 } 301 suggest_fact(table_fact & f)302 bool table_base::suggest_fact(table_fact & f) { 303 if (get_signature().functional_columns()==0) { 304 if (contains_fact(f)) { 305 return false; 306 } 307 add_new_fact(f); 308 return true; 309 } 310 else { 311 if (fetch_fact(f)) { 312 return false; 313 } 314 add_new_fact(f); 315 return true; 316 } 317 } 318 ensure_fact(const table_fact & f)319 void table_base::ensure_fact(const table_fact & f) { 320 if (get_signature().functional_columns() == 0) { 321 add_fact(f); 322 } 323 else { 324 remove_fact(f); 325 add_fact(f); 326 } 327 } 328 clone() const329 table_base * table_base::clone() const { 330 table_base * res = get_plugin().mk_empty(get_signature()); 331 table_fact row; 332 for (auto& k : *this) { 333 k.get_fact(row); 334 res->add_new_fact(row); 335 } 336 return res; 337 } 338 339 /** 340 \brief Default method for complementation. 341 342 It assumes that the compiler creates only tables with 343 at most one column (0 or 1 columns). 344 Complementation of tables with more than one columns 345 is transformed into a cross product of complements and/or 346 difference. 347 348 */ complement(func_decl * p,const table_element * func_columns) const349 table_base * table_base::complement(func_decl* p, const table_element * func_columns) const { 350 const table_signature & sig = get_signature(); 351 SASSERT(sig.functional_columns() == 0 || func_columns != 0); 352 SASSERT(sig.first_functional() <= 1); 353 354 table_base * res = get_plugin().mk_empty(sig); 355 356 table_fact fact; 357 fact.resize(sig.first_functional()); 358 fact.append(sig.functional_columns(), func_columns); 359 360 if (sig.first_functional() == 0) { 361 if (empty()) { 362 res->add_fact(fact); 363 } 364 return res; 365 } 366 367 VERIFY(sig.first_functional() == 1); 368 369 uint64_t upper_bound = get_signature()[0]; 370 bool empty_table = empty(); 371 372 if (upper_bound > (1 << 18)) { 373 std::ostringstream buffer; 374 buffer << "creating large table of size " << upper_bound; 375 if (p) buffer << " for relation " << p->get_name(); 376 auto str = buffer.str(); 377 warning_msg("%s", str.c_str()); 378 } 379 380 for (table_element i = 0; i < upper_bound; i++) { 381 fact[0] = i; 382 if (empty_table || !contains_fact(fact)) { 383 res->add_fact(fact); 384 } 385 } 386 return res; 387 } 388 display(std::ostream & out) const389 void table_base::display(std::ostream & out) const { 390 out << "table with signature "; 391 print_container(get_signature(), out); 392 out << ":\n"; 393 394 for (auto& k : *this) { 395 k.display(out); 396 } 397 398 out << "\n"; 399 } 400 401 402 class table_base::row_interface::fact_row_iterator : public table_base::row_iterator_core { 403 const row_interface & m_parent; 404 unsigned m_index; 405 protected: is_finished() const406 bool is_finished() const override { return m_index==m_parent.size(); } 407 public: fact_row_iterator(const row_interface & row,bool finished)408 fact_row_iterator(const row_interface & row, bool finished) 409 : m_parent(row), m_index(finished ? row.size() : 0) {} 410 operator *()411 table_element operator*() override { 412 SASSERT(!is_finished()); 413 return m_parent[m_index]; 414 } 415 operator ++()416 void operator++() override { 417 m_index++; 418 SASSERT(m_index<=m_parent.size()); 419 } 420 }; 421 begin() const422 table_base::row_iterator table_base::row_interface::begin() const { 423 return row_iterator(alloc(fact_row_iterator, *this, false)); 424 } end() const425 table_base::row_iterator table_base::row_interface::end() const { 426 return row_iterator(alloc(fact_row_iterator, *this, true)); 427 } 428 get_fact(table_fact & result) const429 void table_base::row_interface::get_fact(table_fact & result) const { 430 result.reset(); 431 unsigned n = size(); 432 for (unsigned i = 0; i < n; i++) { 433 result.push_back((*this)[i]); 434 } 435 } 436 437 display(std::ostream & out) const438 void table_base::row_interface::display(std::ostream & out) const { 439 table_fact fact; 440 get_fact(fact); 441 print_container(fact, out); 442 out << "\n"; 443 } 444 to_formula(relation_signature const & sig,expr_ref & fml) const445 void table_base::to_formula(relation_signature const& sig, expr_ref& fml) const { 446 // iterate over rows and build disjunction 447 ast_manager & m = fml.get_manager(); 448 expr_ref_vector disjs(m); 449 expr_ref_vector conjs(m); 450 dl_decl_util util(m); 451 bool_rewriter brw(m); 452 table_fact fact; 453 for (row_interface const& r : *this) { 454 r.get_fact(fact); 455 conjs.reset(); 456 for (unsigned i = 0; i < fact.size(); ++i) { 457 conjs.push_back(m.mk_eq(m.mk_var(i, sig[i]), util.mk_numeral(fact[i], sig[i]))); 458 } 459 brw.mk_and(conjs.size(), conjs.c_ptr(), fml); 460 disjs.push_back(fml); 461 } 462 brw.mk_or(disjs.size(), disjs.c_ptr(), fml); 463 } 464 } 465