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             */
rel_specrel_spec39             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)
m_inner_colsrel_spec47                 : 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 {
operatorrel_spec::hash54                 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:
get_name()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);
get_relation_kind(const relation_signature & sig,const bool_vector & inner_columns,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.data(), 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);
mk_from_inner(const relation_signature & s,const bool_vector & inner_columns,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.data(), 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:
get_plugin()163         sieve_relation_plugin & get_plugin() const {
164             return static_cast<sieve_relation_plugin &>(relation_base::get_plugin());
165         }
166 
is_inner_col(unsigned idx)167         bool is_inner_col(unsigned idx) const { return m_sig2inner[idx]!=UINT_MAX; }
get_inner_col(unsigned idx)168         unsigned get_inner_col(unsigned idx) const {
169             SASSERT(is_inner_col(idx));
170             return m_sig2inner[idx];
171         }
no_sieved_columns()172         bool no_sieved_columns() const { return m_ignored_cols.empty(); }
no_inner_columns()173         bool no_inner_columns() const { return m_ignored_cols.size()==get_signature().size(); }
174 
get_inner()175         relation_base & get_inner() { return *m_inner; }
get_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 
empty()184         bool empty() const override { return get_inner().empty(); }
reset()185         void reset() override { get_inner().reset(); }
get_size_estimate_rows()186         unsigned get_size_estimate_rows() const override { return get_inner().get_size_estimate_rows(); }
get_size_estimate_bytes()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