1 /*++ 2 Copyright (c) 2006 Microsoft Corporation 3 4 Module Name: 5 6 dl_mk_unbound_compressor.h 7 8 Abstract: 9 10 <abstract> 11 12 Author: 13 14 Krystof Hoder (t-khoder) 2010-10-4. 15 16 Revision History: 17 18 --*/ 19 #pragma once 20 21 #include<utility> 22 23 #include "util/map.h" 24 #include "util/obj_pair_hashtable.h" 25 26 #include "muz/base/dl_context.h" 27 #include "muz/base/dl_rule_set.h" 28 #include "muz/base/dl_rule_transformer.h" 29 30 namespace datalog { 31 32 /** 33 \brief Functor for introducing auxiliary predicates to avoid unbound variables in 34 rule heads. 35 36 A rule 37 P(x,_) :- T(x). 38 is replaced by 39 P1(x) :- T(x). 40 and for each occurrence of P in a tail of a rule, a new rule is added with P1 in 41 its place. 42 */ 43 class mk_unbound_compressor : public rule_transformer::plugin { 44 /** predicate and index of compressed argument */ 45 typedef std::pair<func_decl*,unsigned> c_info; 46 typedef pair_hash<ptr_hash<func_decl>,unsigned_hash> c_info_hash; 47 /** predicates that are results of compression */ 48 typedef map<c_info, func_decl*, c_info_hash, default_eq<c_info> > c_map; 49 typedef hashtable<c_info, c_info_hash, default_eq<c_info> > in_progress_table; 50 typedef svector<c_info> todo_stack; 51 52 context & m_context; 53 ast_manager & m; 54 rule_manager & rm; 55 rule_ref_vector m_rules; 56 bool m_modified; 57 todo_stack m_todo; 58 in_progress_table m_in_progress; 59 c_map m_map; 60 61 /** 62 Relations that contain facts 63 */ 64 func_decl_set m_non_empty_rels; 65 66 ast_counter m_head_occurrence_ctr; 67 68 ast_ref_vector m_pinned; 69 70 71 bool is_unbound_argument(rule * r, unsigned head_index); 72 bool has_unbound_head_var(rule * r); 73 74 void detect_tasks(rule_set const& source, unsigned rule_index); 75 void add_task(func_decl * pred, unsigned arg_index); 76 lbool try_compress(rule_set const& source, unsigned rule_index); 77 void add_decompression_rules(rule_set const& source, unsigned rule_index); 78 rule_ref mk_decompression_rule(rule * r, unsigned tail_index, unsigned arg_index); 79 void add_decompression_rule(rule_set const& source, rule * r, unsigned tail_index, unsigned arg_index); 80 void replace_by_decompression_rule(rule_set const& source, unsigned rule_index, unsigned tail_index, unsigned arg_index); 81 82 void add_in_progress_indices(unsigned_vector& arg_indices, app* p); 83 bool decompress_rule(rule_set const& source, rule* r, unsigned_vector const& cmpressed_tail_pred_arg_indexes, unsigned rule_index, unsigned tail_index); 84 void reset(); 85 public: 86 mk_unbound_compressor(context & ctx); 87 88 rule_set * operator()(rule_set const & source) override; 89 }; 90 91 }; 92 93 94