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