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