1 /*++ 2 Copyright (c) 2006 Microsoft Corporation 3 4 Module Name: 5 6 dl_table_relation.h 7 8 Abstract: 9 10 <abstract> 11 12 Author: 13 14 Krystof Hoder (t-khoder) 2010-09-24. 15 16 Revision History: 17 18 --*/ 19 #pragma once 20 21 22 #include "muz/rel/dl_base.h" 23 #include "muz/base/dl_util.h" 24 25 namespace datalog { 26 27 class table_relation; 28 29 class table_relation_plugin : public relation_plugin { 30 friend class table_relation; 31 32 class tr_join_project_fn; 33 class tr_transformer_fn; 34 class universal_target_union_fn; 35 class tr_union_fn; 36 class tr_mutator_fn; 37 class tr_intersection_filter_fn; 38 39 table_plugin & m_table_plugin; 40 41 static symbol create_plugin_name(const table_plugin & p); 42 public: table_relation_plugin(table_plugin & tp,relation_manager & manager)43 table_relation_plugin(table_plugin & tp, relation_manager & manager) 44 : relation_plugin(create_plugin_name(tp), manager, ST_TABLE_RELATION), m_table_plugin(tp) {} 45 get_table_plugin()46 table_plugin & get_table_plugin() { return m_table_plugin; } 47 48 bool can_handle_signature(const relation_signature & s) override; 49 50 relation_base * mk_empty(const relation_signature & s) override; 51 virtual relation_base * mk_full_relation(const relation_signature & s, func_decl* p, family_id kind); 52 relation_base * mk_from_table(const relation_signature & s, table_base * t); 53 54 protected: 55 relation_join_fn * mk_join_fn(const relation_base & t1, const relation_base & t2, 56 unsigned col_cnt, const unsigned * cols1, const unsigned * cols2) override; 57 relation_join_fn * mk_join_project_fn(const relation_base & t1, const relation_base & t2, 58 unsigned joined_col_cnt, const unsigned * cols1, const unsigned * cols2, unsigned removed_col_cnt, 59 const unsigned * removed_cols) override; 60 relation_transformer_fn * mk_project_fn(const relation_base & t, unsigned col_cnt, 61 const unsigned * removed_cols) override; 62 relation_transformer_fn * mk_rename_fn(const relation_base & t, unsigned permutation_cycle_len, 63 const unsigned * permutation_cycle) override; 64 relation_transformer_fn * mk_permutation_rename_fn(const relation_base & t, 65 const unsigned * permutation) override; 66 relation_union_fn * mk_union_fn(const relation_base & tgt, const relation_base & src, 67 const relation_base * delta) override; 68 relation_mutator_fn * mk_filter_identical_fn(const relation_base & t, unsigned col_cnt, 69 const unsigned * identical_cols) override; 70 relation_mutator_fn * mk_filter_equal_fn(const relation_base & t, const relation_element & value, 71 unsigned col) override; 72 relation_mutator_fn * mk_filter_interpreted_fn(const relation_base & t, app * condition) override; 73 relation_transformer_fn * mk_filter_interpreted_and_project_fn(const relation_base & t, 74 app * condition, unsigned removed_col_cnt, const unsigned * removed_cols) override; 75 relation_intersection_filter_fn * mk_filter_by_intersection_fn(const relation_base & t, 76 const relation_base & src, unsigned joined_col_cnt, const unsigned * t_cols, const unsigned * src_cols) override; 77 relation_intersection_filter_fn * mk_filter_by_negation_fn(const relation_base & t, 78 const relation_base & negated_obj, unsigned joined_col_cnt, 79 const unsigned * t_cols, const unsigned * negated_cols) override; 80 relation_transformer_fn * mk_select_equal_and_project_fn(const relation_base & t, 81 const relation_element & value, unsigned col) override; 82 }; 83 84 class table_relation : public relation_base { 85 friend class table_relation_plugin; 86 friend class table_relation_plugin::tr_join_project_fn; 87 friend class table_relation_plugin::tr_transformer_fn; 88 89 scoped_rel<table_base> m_table; 90 91 /** 92 \brief Create a \c table_relation object. 93 94 The newly created object takes ownership of the \c table object. 95 */ table_relation(table_relation_plugin & p,const relation_signature & s,table_base * table)96 table_relation(table_relation_plugin & p, const relation_signature & s, table_base * table) 97 : relation_base(p, s), m_table(table) { 98 SASSERT(s.size()==table->get_signature().size()); 99 } 100 public: 101 get_plugin()102 table_relation_plugin & get_plugin() const { 103 return static_cast<table_relation_plugin &>(relation_base::get_plugin()); 104 } 105 get_table()106 table_base & get_table() { return *m_table; } get_table()107 const table_base & get_table() const { return *m_table; } 108 empty()109 bool empty() const override { return m_table->empty(); } 110 111 void add_table_fact(const table_fact & f); 112 113 void add_fact(const relation_fact & f) override; 114 bool contains_fact(const relation_fact & f) const override; 115 relation_base * clone() const override; 116 relation_base * complement(func_decl* p) const override; to_formula(expr_ref & fml)117 void to_formula(expr_ref& fml) const override { get_table().to_formula(get_signature(), fml); } 118 display(std::ostream & out)119 void display(std::ostream & out) const override { 120 get_table().display(out); 121 } 122 void display_tuples(func_decl & pred, std::ostream & out) const override; 123 get_size_estimate_rows()124 unsigned get_size_estimate_rows() const override { return m_table->get_size_estimate_rows(); } get_size_estimate_bytes()125 unsigned get_size_estimate_bytes() const override { return m_table->get_size_estimate_bytes(); } knows_exact_size()126 bool knows_exact_size() const override { return m_table->knows_exact_size(); } 127 }; 128 129 }; 130 131 132