1 /*++ 2 Copyright (c) 2006 Microsoft Corporation 3 4 Module Name: 5 6 dl_compiler.h 7 8 Abstract: 9 10 <abstract> 11 12 Author: 13 14 Krystof Hoder (t-khoder) 2010-09-14. 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/hashtable.h" 27 #include "util/map.h" 28 #include "util/obj_pair_hashtable.h" 29 #include "util/ref_vector.h" 30 #include "util/vector.h" 31 32 #include "muz/rel/dl_base.h" 33 #include "muz/base/dl_context.h" 34 #include "muz/rel/dl_instruction.h" 35 36 namespace datalog { 37 38 class compiler { 39 typedef instruction::reg_idx reg_idx; 40 typedef hashtable<unsigned, u_hash, u_eq> int_set; 41 typedef u_map<unsigned> int2int; 42 typedef u_map<unsigned_vector> int2ints; 43 typedef obj_map<func_decl, reg_idx> pred2idx; 44 typedef unsigned_vector var_vector; 45 typedef ptr_vector<func_decl> func_decl_vector; 46 47 enum assembling_column_kind { 48 ACK_BOUND_VAR, 49 ACK_UNBOUND_VAR, 50 ACK_CONSTANT 51 }; 52 53 /** 54 \brief instruction for assembling head relation from a joint relation built 55 from rule evaluation. 56 57 ACK_BOUND_VAR(source_column) - encodes that the column contains a variable 58 bound in the body. 59 60 ACK_UNBOUND_VAR(var_index) - encodes that the column contains a variable that 61 is unbound (by the corresponding rule body), 62 var_index is the de-Bruijn index (var->get_idx()) 63 of the variable associated with the column. 64 65 ACK_CONSTANT(constant) - encodes that the column contains the constant. 66 67 Examples: 68 69 P(x) :- Q(x,y), Q(y,z) 70 The variables in the body relation are [x, y, y, z] indexed as 0, 1, 2, 3. 71 The variable x gets the instruction ACK_BOUND_VAR(0) 72 73 P(u,x) :- Q(x,y), Q(y,z) 74 The variable u gets the instruction ACK_UNBOUND_VAR(#0) 75 76 P(1, x) :- Q(x,y), Q(y,z) 77 The instruction for column 0 is ACK_CONSTANT(1) 78 79 */ 80 struct assembling_column_info { 81 82 relation_sort domain; // domain of the column 83 assembling_column_kind kind; // "instruction" tag 84 union { 85 unsigned source_column; // for ACK_BOUND_VAR 86 unsigned var_index; // for ACK_UNBOUND_VAR 87 relation_element constant; // for ACK_CONSTANT 88 }; 89 }; 90 91 class instruction_observer : public instruction_block::instruction_observer { 92 compiler & m_parent; 93 rule * m_current; 94 public: instruction_observer(compiler & parent)95 instruction_observer(compiler & parent) : m_parent(parent), m_current(nullptr) {} 96 start_rule(rule * r)97 void start_rule(rule * r) { SASSERT(!m_current); m_current=r; } finish_rule()98 void finish_rule() { m_current = nullptr; } notify(instruction * i)99 void notify(instruction * i) override { 100 if(m_current) { 101 i->set_accounting_parent_object(m_parent.m_context, m_current); 102 } 103 } 104 }; 105 106 107 context & m_context; 108 rule_set const & m_rule_set; 109 /** 110 Invariant: the \c m_top_level_code never contains the loop that is being constructed, 111 so instruction that need to be executed before the loop can be pushed into it. 112 */ 113 instruction_block & m_top_level_code; 114 pred2idx m_pred_regs; 115 vector<relation_signature> m_reg_signatures; 116 obj_pair_map<sort, app, reg_idx> m_constant_registers; 117 obj_pair_map<sort, decl, reg_idx> m_total_registers; 118 obj_map<decl, reg_idx> m_empty_tables_registers; 119 instruction_observer m_instruction_observer; 120 expr_free_vars m_free_vars; 121 122 123 /** 124 If true, the union operation on the underlying structure only provides the information 125 whether the updated relation has changed or not. In this case we do not get anything 126 from using delta relations at position of input relations in the saturation loop, so we 127 would not do it. 128 */ all_or_nothing_deltas()129 bool all_or_nothing_deltas() const { return m_context.all_or_nothing_deltas(); } 130 131 /** 132 If true, we compile the saturation loops in a way that allows us to use widening. 133 */ compile_with_widening()134 bool compile_with_widening() const { return m_context.compile_with_widening(); } 135 136 reg_idx get_fresh_register(const relation_signature & sig); 137 reg_idx get_register(const relation_signature & sig, bool reuse, reg_idx r); 138 reg_idx get_single_column_register(const relation_sort s); 139 140 /** 141 \brief Allocate registers for predicates in \c pred and add them into the \c regs map. 142 143 \c regs must not already contain any predicate from \c preds. 144 */ 145 void get_fresh_registers(const func_decl_set & preds, pred2idx & regs); 146 147 void make_join(reg_idx t1, reg_idx t2, const variable_intersection & vars, reg_idx & result, 148 bool reuse_t1, instruction_block & acc); 149 void make_min(reg_idx source, reg_idx & target, const unsigned_vector & group_by_cols, 150 unsigned min_col, instruction_block & acc); 151 void make_join_project(reg_idx t1, reg_idx t2, const variable_intersection & vars, 152 const unsigned_vector & removed_cols, reg_idx & result, bool reuse_t1, instruction_block & acc); 153 void make_filter_interpreted_and_project(reg_idx src, app_ref & cond, 154 const unsigned_vector & removed_cols, reg_idx & result, bool reuse, instruction_block & acc); 155 void make_select_equal_and_project(reg_idx src, const relation_element val, unsigned col, 156 reg_idx & result, bool reuse, instruction_block & acc); 157 /** 158 \brief Create add an union or widen operation and put it into \c acc. 159 */ 160 void make_union(reg_idx src, reg_idx tgt, reg_idx delta, bool widening, instruction_block & acc); 161 void make_projection(reg_idx src, unsigned col_cnt, const unsigned * removed_cols, 162 reg_idx & result, bool reuse, instruction_block & acc); 163 void make_rename(reg_idx src, unsigned cycle_len, const unsigned * permutation_cycle, 164 reg_idx & result, bool reuse, instruction_block & acc); 165 void make_clone(reg_idx src, reg_idx & result, instruction_block & acc); 166 167 /** 168 \brief Into \c acc add code that will assemble columns of a relation according to description 169 in \c acis0. The source for bound variables is the table in register \c src. 170 171 If \c src is \c execution_context::void_register, it is assumed to be a full relation 172 with empty signature. 173 */ 174 void make_assembling_code(rule* compiled_rule, func_decl* head_pred, reg_idx src, const svector<assembling_column_info> & acis0, 175 reg_idx & result, bool & dealloc, instruction_block & acc); 176 177 void make_dealloc_non_void(reg_idx r, instruction_block & acc); 178 179 void make_add_constant_column(func_decl* pred, reg_idx src, const relation_sort s, const relation_element val, 180 reg_idx & result, bool & dealloc, instruction_block & acc); 181 182 void make_add_unbound_column(rule* compiled_rule, unsigned col_idx, func_decl* pred, reg_idx src, const relation_sort& s, reg_idx & result, 183 bool & dealloc, instruction_block & acc); 184 void make_full_relation(func_decl* pred, const relation_signature & sig, reg_idx & result, 185 instruction_block & acc); 186 187 void add_unbound_columns_for_negation(rule* compiled_rule, func_decl* pred, reg_idx& single_res, expr_ref_vector& single_res_expr, 188 bool & dealloc, instruction_block& acc); 189 190 void make_duplicate_column(reg_idx src, unsigned col, reg_idx & result, bool reuse, instruction_block & acc); 191 192 void ensure_predicate_loaded(func_decl * pred, instruction_block & acc); 193 194 /** 195 \brief For rule \c r with two positive uninterpreted predicates put into \c res indexes of 196 local variables in a table that results from join of the two positive predicates. 197 198 Used to get input for the "project" part of join-project. 199 */ 200 void get_local_indexes_for_projection(rule * r, unsigned_vector & res); 201 void get_local_indexes_for_projection(app * t, var_counter & globals, unsigned ofs, 202 unsigned_vector & res); 203 204 /** 205 \brief Into \c acc add instructions that will add new facts following from the rule into 206 \c head_reg, and add the facts that were not in \c head_reg before into \c delta_reg. 207 */ 208 void compile_rule_evaluation_run(rule * r, reg_idx head_reg, const reg_idx * tail_regs, 209 reg_idx delta_reg, bool use_widening, instruction_block & acc); 210 211 void compile_rule_evaluation(rule * r, const pred2idx * input_deltas, reg_idx output_delta, 212 bool use_widening, instruction_block & acc); 213 214 /** 215 \brief Generate code to evaluate rules corresponding to predicates in \c head_preds. 216 The rules are evaluated in the order their heads appear in the \c head_preds vector. 217 */ 218 void compile_preds(const func_decl_vector & head_preds, const func_decl_set & widened_preds, 219 const pred2idx * input_deltas, const pred2idx & output_deltas, instruction_block & acc); 220 221 /** 222 \brief Generate code to evaluate predicates in a stratum based on their non-recursive rules. 223 */ 224 void compile_preds_init(const func_decl_vector & head_preds, const func_decl_set & widened_preds, 225 const pred2idx * input_deltas, const pred2idx & output_deltas, instruction_block & acc); 226 227 void make_inloop_delta_transition(const pred2idx & global_head_deltas, 228 const pred2idx & global_tail_deltas, const pred2idx & local_deltas, instruction_block & acc); 229 void compile_loop(const func_decl_vector & head_preds, const func_decl_set & widened_preds, 230 const pred2idx & global_head_deltas, const pred2idx & global_tail_deltas, 231 const pred2idx & local_deltas, instruction_block & acc); 232 void compile_dependent_rules(const func_decl_set & head_preds, 233 const pred2idx * input_deltas, const pred2idx & output_deltas, 234 bool add_saturation_marks, instruction_block & acc); 235 236 void detect_chains(const func_decl_set & preds, func_decl_vector & ordered_preds, 237 func_decl_set & global_deltas); 238 /** 239 Return true if there is no dependency inside the \c rules stratum. 240 241 The head predicates in stratum must be strongly connected by dependency. 242 */ 243 bool is_nonrecursive_stratum(const func_decl_set & preds) const; 244 /** 245 input_deltas==0 --> we use the actual content of relations instead of deltas 246 */ 247 void compile_nonrecursive_stratum(const func_decl_set & preds, 248 const pred2idx * input_deltas, const pred2idx & output_deltas, 249 bool add_saturation_marks, instruction_block & acc); 250 251 void compile_strats(const rule_stratifier & stratifier, 252 const pred2idx * input_deltas, const pred2idx & output_deltas, 253 bool add_saturation_marks, instruction_block & acc); 254 255 bool all_saturated(const func_decl_set & preds) const; 256 257 void reset(); 258 compiler(context & ctx,rule_set const & rules,instruction_block & top_level_code)259 explicit compiler(context & ctx, rule_set const & rules, instruction_block & top_level_code) 260 : m_context(ctx), 261 m_rule_set(rules), 262 m_top_level_code(top_level_code), 263 m_instruction_observer(*this) {} 264 265 /** 266 \brief Compile \c rules in to pseudocode. 267 268 Instructions to load data and perform computations put into \c execution_code 269 */ 270 void do_compilation(instruction_block & execution_code, 271 instruction_block & termination_code); 272 273 public: 274 compile(context & ctx,rule_set const & rules,instruction_block & execution_code,instruction_block & termination_code)275 static void compile(context & ctx, rule_set const & rules, instruction_block & execution_code, 276 instruction_block & termination_code) { 277 compiler(ctx, rules, execution_code) 278 .do_compilation(execution_code, termination_code); 279 } 280 281 }; 282 283 284 }; 285 286 287