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