1 /*++
2 Copyright (c) 2006 Microsoft Corporation
3 
4 Module Name:
5 
6     dl_table.h
7 
8 Abstract:
9 
10     <abstract>
11 
12 Author:
13 
14     Krystof Hoder (t-khoder) 2010-09-01.
15 
16 Revision History:
17 
18 --*/
19 #pragma once
20 
21 #include<iostream>
22 #include<list>
23 #include<utility>
24 
25 #include "ast/ast.h"
26 #include "util/bit_vector.h"
27 #include "util/buffer.h"
28 #include "util/hashtable.h"
29 #include "util/map.h"
30 #include "util/ref_vector.h"
31 #include "util/vector.h"
32 #include "util/union_find.h"
33 #include "muz/rel/dl_base.h"
34 #include "muz/base/dl_util.h"
35 #include "util/bit_vector.h"
36 
37 
38 namespace datalog {
rel_specrel_spec39 
40     class context;
41     class variable_intersection;
42 
43 
44 
45     // -----------------------------------
46     //
m_inner_colsrel_spec47     // hashtable_table
48     //
49     // -----------------------------------
50 
51     class hashtable_table;
52 
53     class hashtable_table_plugin : public table_plugin {
operatorrel_spec::hash54         friend class hashtable_table;
55     protected:
56         class join_fn;
57     public:
58         typedef hashtable_table table;
59 
60         hashtable_table_plugin(relation_manager & manager)
61             : table_plugin(symbol("hashtable"), manager) {}
62 
63         table_base * mk_empty(const table_signature & s) override;
64 
65         table_join_fn * mk_join_fn(const table_base & t1, const table_base & t2,
66             unsigned col_cnt, const unsigned * cols1, const unsigned * cols2) override;
67     };
68 
69     class hashtable_table : public table_base {
70         friend class hashtable_table_plugin;
71         friend class hashtable_table_plugin::join_fn;
72 
73         class our_iterator_core;
74 
75         typedef hashtable<table_fact, svector_hash_proc<table_element_hash>,
76             vector_eq_proc<table_fact> > storage;
get_name()77 
78         storage m_data;
79 
80         hashtable_table(hashtable_table_plugin & plugin, const table_signature & sig)
81             : table_base(plugin, sig) {}
82     public:
83         hashtable_table_plugin & get_plugin() const
84         { return static_cast<hashtable_table_plugin &>(table_base::get_plugin()); }
85 
86         void add_fact(const table_fact & f) override {
87             m_data.insert(f);
88         }
89         void remove_fact(const table_element* fact) override {
90             table_fact f(get_signature().size(), fact);
get_relation_kind(const relation_signature & sig,const bool_vector & inner_columns,family_id inner_kind)91             m_data.remove(f);
92         }
93         bool contains_fact(const table_fact & f) const override {
94             return m_data.contains(f);
95         }
96 
97         iterator begin() const override;
98         iterator end() const override;
99 
100         unsigned get_size_estimate_rows() const override { return m_data.size(); }
101         unsigned get_size_estimate_bytes() const override { return m_data.size()*get_signature().size()*8; }
102         bool knows_exact_size() const override { return true; }
103     };
104 
105     // -----------------------------------
106     //
107     // bitvector_table
108     //
109     // -----------------------------------
mk_from_inner(const relation_signature & s,const bool_vector & inner_columns,relation_base * inner_rel)110 
111     class bitvector_table;
112 
113     class bitvector_table_plugin : public table_plugin {
114     public:
115         typedef bitvector_table table;
116 
117         bitvector_table_plugin(relation_manager & manager)
118             : table_plugin(symbol("bitvector"), manager) {}
119 
120         bool can_handle_signature(const table_signature & s) override;
121 
122         table_base * mk_empty(const table_signature & s) override;
123     };
124 
125     class bitvector_table : public table_base {
126         friend class bitvector_table_plugin;
127 
128         class bv_iterator;
129         bit_vector      m_bv;
130         unsigned        m_num_cols;
131         unsigned_vector m_shift;
132         unsigned_vector m_mask;
133 
134         unsigned fact2offset(const table_element* f) const;
135         void     offset2fact(unsigned offset, table_fact& f) const;
136 
137         bitvector_table(bitvector_table_plugin & plugin, const table_signature & sig);
138     public:
139         void add_fact(const table_fact & f) override;
140         void remove_fact(const table_element* fact) override;
141         bool contains_fact(const table_fact & f) const override;
142         iterator begin() const override;
143         iterator end() const override;
144     };
145 
146 
147 
148 };
149 
150 
151