1 /*++
2 Copyright (c) 2006 Microsoft Corporation
3 
4 Module Name:
5 
6     dl_rule_set.h
7 
8 Abstract:
9 
10     <abstract>
11 
12 Author:
13 
14     Leonardo de Moura (leonardo) 2010-05-17.
15 
16 Revision History:
17 
18 --*/
19 #pragma once
20 
21 #include "util/obj_hashtable.h"
22 #include "muz/base/dl_rule.h"
23 
24 namespace datalog {
25 
26     class rule_set;
27 
28     class rule_dependencies {
29     public:
30         typedef obj_hashtable<func_decl> item_set;
31         typedef obj_map<func_decl, item_set * > deps_type;
32 
33         typedef deps_type::iterator iterator;
34     private:
35         /**
36            Map (dependent -> set of master objects)
37 
38            Each master object is also present as a key of the map, even if its master set
39            is empty.
40         */
41         deps_type        m_data;
42         context &        m_context;
43         ptr_vector<expr> m_todo;
44         expr_sparse_mark m_visited;
45 
46 
47         //we need to take care with removing to avoid memory leaks
48         void remove_m_data_entry(func_decl * key);
49 
50         //sometimes we need to return reference to an empty set,
51         //so we return reference to this one.
52         item_set m_empty_item_set;
53 
54         item_set & ensure_key(func_decl * pred);
55         void insert(func_decl * depending, func_decl * master);
56         void populate(rule const* r);
57     public:
58         rule_dependencies(context& ctx);
59         rule_dependencies(const rule_dependencies & o, bool reversed = false);
60         ~rule_dependencies();
61         void reset();
62 
63         void populate(const rule_set & rules);
64         void populate(unsigned n, rule * const * rules);
65         void restrict_dependencies(const item_set & allowed);
66         void remove(func_decl * itm);
67         void remove(const item_set & to_remove);
68 
empty()69         bool empty() const { return m_data.empty(); }
70         const item_set & get_deps(func_decl * f) const;
71         /**
72            \brief Number of predicates \c f depends on.
73          */
in_degree(func_decl * f)74         unsigned in_degree(func_decl * f) const { return get_deps(f).size(); }
75         /**
76            \brief Number of predicates that depend on \c f.
77          */
78         unsigned out_degree(func_decl * f) const;
79 
80         /**
81            \brief If the rependency graph is acyclic, put all elements into \c res
82              ordered so that elements can depend only on elements that are before them.
83              If the graph is not acyclic, return false.
84          */
85         bool sort_deps(ptr_vector<func_decl> & res);
86 
begin()87         iterator begin() const { return m_data.begin(); }
end()88         iterator end() const { return m_data.end(); }
89 
90         void display( std::ostream & out ) const;
91     };
92 
93     class rule_stratifier {
94     public:
95         typedef func_decl T;
96         typedef obj_hashtable<T> item_set;
97         typedef ptr_vector<item_set> comp_vector;
98         typedef obj_map<T, item_set *> deps_type;
99     private:
100 
101         const rule_dependencies & m_deps;
102         comp_vector m_strats;
103 
104         obj_map<T, unsigned> m_preorder_nums;
105         ptr_vector<T> m_stack_S;
106         ptr_vector<T> m_stack_P;
107 
108         obj_map<T, unsigned> m_component_nums;
109         comp_vector m_components;
110         obj_map<T, unsigned> m_pred_strat_nums;
111 
112         unsigned m_next_preorder;
113         unsigned m_first_preorder;
114 
115         /**
116             Finds strongly connected components using the Gabow's algorithm.
117         */
118         void traverse(T* el);
119 
120         /**
121             Calls \c traverse to identify strognly connected components and then
122             orders them using topological sorting.
123         */
124         void process();
125 
126     public:
127 
128         /**
129             \remark The \c stratifier object keeps a reference to the \c deps object, so
130             it must exist for the whole lifetime of the \c stratifier object.
131         */
rule_stratifier(const rule_dependencies & deps)132         rule_stratifier(const rule_dependencies & deps)
133             : m_deps(deps), m_next_preorder(0)
134         {
135             process();
136         }
137 
138         ~rule_stratifier();
139 
140         /**
141             Return vector of components ordered so that the only dependencies are from
142             later components to earlier.
143         */
get_strats()144         const comp_vector & get_strats() const { return m_strats; }
145 
146         unsigned get_predicate_strat(func_decl * pred) const;
147 
148         void display( std::ostream & out ) const;
149     };
150 
151     /**
152        \brief Datalog "Program" (aka rule set).
153     */
154     class rule_set {
155         friend class rule_dependencies;
156     public:
157         typedef ptr_vector<func_decl_set> pred_set_vector;
158         typedef obj_map<func_decl, rule_vector*> decl2rules;
159     private:
160         typedef obj_map<func_decl, func_decl_set*> decl2deps;
161 
162         context &                    m_context;
163         rule_manager &               m_rule_manager;
164         rule_ref_vector              m_rules;        //!< all rules
165         decl2rules                   m_head2rules;   //!< mapping from head symbol to rules.
166         rule_dependencies            m_deps;         //!< dependencies
167         scoped_ptr<rule_stratifier>  m_stratifier;   //!< contains stratifier object iff the rule_set is closed
168         func_decl_set                m_output_preds; //!< output predicates
169         obj_map<func_decl,func_decl*> m_orig2pred;
170         obj_map<func_decl,func_decl*> m_pred2orig;
171         func_decl_ref_vector          m_refs;
172 
173 
174         //sometimes we need to return reference to an empty rule_vector,
175         //so we return reference to this one.
176         rule_vector                  m_empty_rule_vector;
177 
178         void compute_deps();
179         void compute_tc_deps();
180         bool stratified_negation();
181     public:
182         rule_set(context & ctx);
183         rule_set(const rule_set & rs);
184         ~rule_set();
185 
186         ast_manager & get_manager() const;
get_rule_manager()187         rule_manager & get_rule_manager() const { return const_cast<rule_manager&>(m_rule_manager); }
get_context()188         context&  get_context() const { return m_context; }
189 
190 
191         void inherit_predicates(rule_set const& other);
192         void inherit_predicate(rule_set const& other, func_decl* orig, func_decl* pred);
193         func_decl* get_orig(func_decl* pred) const;
194         func_decl* get_pred(func_decl* orig) const;
195 
196         /**
197            \brief Add rule \c r to the rule set.
198         */
199         void add_rule(rule * r);
200 
201         /**
202            \brief Remove rule \c r from the rule set.
203         */
204         void del_rule(rule * r);
205         /**
206            \brief Replace a rule \c r with the rule \c other
207         */
208         void replace_rule(rule * r, rule * other);
209 
210         /**
211            \brief Add all rules from a different rule_set.
212         */
213         void add_rules(const rule_set& src);
214         void replace_rules(const rule_set& other);
215 
216         /**
217            \brief This method should be invoked after all rules are added to the rule set.
218            It will check if the negation is indeed stratified.
219            Return true if succeeded.
220 
221            \remark If new rules are added, the rule_set will be "reopen".
222         */
223         bool close();
224         void ensure_closed();
225         /**
226            \brief Undo the effect of the \c close() operation.
227          */
228         void reopen();
is_closed()229         bool is_closed() const { return m_stratifier != 0; }
230 
get_num_rules()231         unsigned get_num_rules() const { return m_rules.size(); }
empty()232         bool empty() const { return m_rules.empty(); }
233 
get_rule(unsigned i)234         rule * get_rule(unsigned i) const { return m_rules[i]; }
last()235         rule * last() const { return m_rules[m_rules.size()-1]; }
get_rules()236         rule_ref_vector const& get_rules() const { return m_rules; }
237 
238         const rule_vector & get_predicate_rules(func_decl * pred) const;
contains(func_decl * pred)239         bool contains(func_decl* pred) const { return m_head2rules.contains(pred); }
240 
get_stratifier()241         const rule_stratifier & get_stratifier() const {
242             SASSERT(m_stratifier);
243             return *m_stratifier;
244         }
245         const pred_set_vector & get_strats() const;
246         unsigned get_predicate_strat(func_decl * pred) const;
get_dependencies()247         const rule_dependencies & get_dependencies() const { SASSERT(is_closed()); return m_deps; }
248 
249         // split predicats into founded and non-founded.
250         void split_founded_rules(func_decl_set& founded, func_decl_set& non_founded);
251 
252         void reset();
253 
set_output_predicate(func_decl * pred)254         void set_output_predicate(func_decl * pred) { m_refs.push_back(pred); m_output_preds.insert(pred); }
is_output_predicate(func_decl * pred)255         bool is_output_predicate(func_decl * pred) const { return m_output_preds.contains(pred); }
inherit_output_predicate(rule_set const & src,func_decl * pred)256         void inherit_output_predicate(rule_set const& src, func_decl* pred) { if (src.is_output_predicate(pred) && !is_output_predicate(pred)) set_output_predicate(pred); }
get_output_predicates()257         const func_decl_set & get_output_predicates() const { return m_output_preds; }
get_output_predicate()258         func_decl* get_output_predicate() const { SASSERT(m_output_preds.size() == 1); return *m_output_preds.begin(); }
259 
260         bool is_finite_domain() const;
261 
262         void display(std::ostream & out) const;
263 
264         /**
265            \brief Output rule dependencies.
266 
267            The rule set must be closed before calling this function.
268          */
269         void display_deps(std::ostream & out) const;
270 
271         typedef rule * const * iterator;
begin()272         iterator begin() const { return m_rules.data(); }
end()273         iterator end() const { return m_rules.data()+m_rules.size(); }
274 
begin_grouped_rules()275         decl2rules::iterator begin_grouped_rules() const { return m_head2rules.begin(); }
end_grouped_rules()276         decl2rules::iterator end_grouped_rules() const { return m_head2rules.end(); }
277 
278     };
279 
280     inline std::ostream& operator<<(std::ostream& out, rule_set const& r) { r.display(out); return out; }
281 
282 
283 
284 };
285 
286