1 /*++ 2 Copyright (c) 2006 Microsoft Corporation 3 4 Module Name: 5 6 dl_sieve_relation.h 7 8 Abstract: 9 10 <abstract> 11 12 Author: 13 14 Krystof Hoder (t-khoder) 2010-11-11. 15 16 Revision History: 17 18 --*/ 19 20 #pragma once 21 22 #include "muz/base/dl_context.h" 23 #include "muz/rel/dl_relation_manager.h" 24 25 namespace datalog { 26 27 class sieve_relation; 28 29 class sieve_relation_plugin : public relation_plugin { 30 friend class sieve_relation; 31 public: 32 struct rel_spec { 33 bool_vector m_inner_cols; 34 family_id m_inner_kind; 35 36 /** 37 Create uninitialized rel_spec. 38 */ 39 rel_spec() {} 40 /** 41 \c inner_kind==null_family_id means we will not specify a relation kind when requesting 42 the relation object from the relation_manager. 43 44 \c inner_kind==null_family_id cannot hold in a specification of existing relation object. 45 */ 46 rel_spec(unsigned sig_sz, const bool * inner_cols, family_id inner_kind=null_family_id) 47 : m_inner_cols(sig_sz, inner_cols), m_inner_kind(inner_kind) {} 48 49 bool operator==(const rel_spec & o) const { 50 return m_inner_kind==o.m_inner_kind && vectors_equal(m_inner_cols, o.m_inner_cols); 51 } 52 53 struct hash { 54 unsigned operator()(const rel_spec & s) const { 55 return svector_hash<bool_hash>()(s.m_inner_cols)^s.m_inner_kind; 56 } 57 }; 58 }; 59 private: 60 61 class join_fn; 62 class transformer_fn; 63 class union_fn; 64 class filter_fn; 65 class negation_filter_fn; 66 67 rel_spec_store<rel_spec, rel_spec::hash, default_eq<rel_spec> > m_spec_store; 68 69 family_id get_relation_kind(sieve_relation & r, const bool * inner_columns); 70 71 void extract_inner_columns(const relation_signature & s, relation_plugin & inner, 72 bool_vector & inner_columns); 73 void extract_inner_signature(const relation_signature & s, relation_signature & inner_sig); 74 void collect_inner_signature(const relation_signature & s, const bool_vector & inner_columns, 75 relation_signature & inner_sig); 76 public: 77 static symbol get_name() { return symbol("sieve_relation"); } 78 static sieve_relation_plugin& get_plugin(relation_manager & rmgr); 79 80 static sieve_relation& get(relation_base& r); 81 static sieve_relation const & get(relation_base const& r); 82 static sieve_relation* get(relation_base* r); 83 static sieve_relation const* get(relation_base const* r); 84 85 sieve_relation_plugin(relation_manager & manager); 86 87 void initialize(family_id fid) override; 88 89 family_id get_relation_kind(const relation_signature & sig, const bool * inner_columns, 90 family_id inner_kind); 91 family_id get_relation_kind(const relation_signature & sig, const bool_vector & inner_columns, 92 family_id inner_kind) { 93 SASSERT(sig.size()==inner_columns.size()); 94 return get_relation_kind(sig, inner_columns.c_ptr(), inner_kind); 95 } 96 97 bool can_handle_signature(const relation_signature & s) override; 98 99 relation_base * mk_empty(const relation_signature & s) override; 100 sieve_relation * mk_empty(const sieve_relation & original); 101 relation_base * mk_empty(const relation_base & original) override; 102 relation_base * mk_empty(const relation_signature & s, family_id kind) override; 103 sieve_relation * mk_empty(const relation_signature & s, relation_plugin & inner_plugin); 104 105 relation_base * mk_full(func_decl* p, const relation_signature & s) override; 106 sieve_relation * full(func_decl* p, const relation_signature & s, relation_plugin & inner_plugin); 107 108 sieve_relation * mk_from_inner(const relation_signature & s, const bool * inner_columns, 109 relation_base * inner_rel); 110 sieve_relation * mk_from_inner(const relation_signature & s, const bool_vector & inner_columns, 111 relation_base * inner_rel) { 112 SASSERT(inner_columns.size()==s.size()); 113 return mk_from_inner(s, inner_columns.c_ptr(), inner_rel); 114 } 115 116 protected: 117 118 relation_join_fn * mk_join_fn(const relation_base & t1, const relation_base & t2, 119 unsigned col_cnt, const unsigned * cols1, const unsigned * cols2) override; 120 relation_transformer_fn * mk_project_fn(const relation_base & t, unsigned col_cnt, 121 const unsigned * removed_cols) override; 122 relation_transformer_fn * mk_rename_fn(const relation_base & t, unsigned permutation_cycle_len, 123 const unsigned * permutation_cycle) override; 124 relation_union_fn * mk_union_fn(const relation_base & tgt, const relation_base & src, 125 const relation_base * delta) override; 126 relation_mutator_fn * mk_filter_identical_fn(const relation_base & t, unsigned col_cnt, 127 const unsigned * identical_cols) override; 128 relation_mutator_fn * mk_filter_equal_fn(const relation_base & t, const relation_element & value, 129 unsigned col) override; 130 relation_mutator_fn * mk_filter_interpreted_fn(const relation_base & t, app * condition) override; 131 relation_intersection_filter_fn * mk_filter_by_negation_fn(const relation_base & t, 132 const relation_base & negated_obj, unsigned joined_col_cnt, 133 const unsigned * t_cols, const unsigned * negated_cols) override; 134 }; 135 136 137 // ----------------------------------- 138 // 139 // sieve_relation 140 // 141 // ----------------------------------- 142 143 class sieve_relation : public relation_base { 144 friend class sieve_relation_plugin; 145 friend class sieve_relation_plugin::join_fn; 146 friend class sieve_relation_plugin::transformer_fn; 147 friend class sieve_relation_plugin::union_fn; 148 friend class sieve_relation_plugin::filter_fn; 149 150 bool_vector m_inner_cols; 151 152 unsigned_vector m_sig2inner; 153 unsigned_vector m_inner2sig; 154 unsigned_vector m_ignored_cols; //in ascending order, so that it can be used in project-like functions 155 156 scoped_rel<relation_base> m_inner; 157 158 159 sieve_relation(sieve_relation_plugin & p, const relation_signature & s, 160 const bool * inner_columns, relation_base * inner); 161 162 public: 163 sieve_relation_plugin & get_plugin() const { 164 return static_cast<sieve_relation_plugin &>(relation_base::get_plugin()); 165 } 166 167 bool is_inner_col(unsigned idx) const { return m_sig2inner[idx]!=UINT_MAX; } 168 unsigned get_inner_col(unsigned idx) const { 169 SASSERT(is_inner_col(idx)); 170 return m_sig2inner[idx]; 171 } 172 bool no_sieved_columns() const { return m_ignored_cols.empty(); } 173 bool no_inner_columns() const { return m_ignored_cols.size()==get_signature().size(); } 174 175 relation_base & get_inner() { return *m_inner; } 176 const relation_base & get_inner() const { return *m_inner; } 177 178 void add_fact(const relation_fact & f) override; 179 bool contains_fact(const relation_fact & f) const override; 180 sieve_relation * clone() const override; 181 relation_base * complement(func_decl*p) const override; 182 void to_formula(expr_ref& fml) const override; 183 184 bool empty() const override { return get_inner().empty(); } 185 void reset() override { get_inner().reset(); } 186 unsigned get_size_estimate_rows() const override { return get_inner().get_size_estimate_rows(); } 187 unsigned get_size_estimate_bytes() const override { return get_inner().get_size_estimate_bytes(); } 188 189 void display(std::ostream & out) const override; 190 }; 191 192 193 }; 194 195 196