1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
dl_mk_interp_tail_simplifier.h
Abstract:
Rule transformer which simplifies interpreted tails
Author:
Krystof Hoder (t-khoder) 2011-10-01.
Revision History:
--*/
#pragma once
#include "muz/base/dl_context.h"
#include "muz/base/dl_rule_transformer.h"
#include "ast/substitution/unifier.h"
#include "ast/substitution/substitution.h"
#include "ast/arith_decl_plugin.h"
namespace datalog {
class mk_interp_tail_simplifier : public rule_transformer::plugin {
class rule_substitution
{
ast_manager& m;
context& m_context;
substitution m_subst;
unifier m_unif;
app_ref m_head;
app_ref_vector m_tail;
bool_vector m_neg;
rule * m_rule;
void apply(app * a, app_ref& res);
public:
rule_substitution(context & ctx)
: m(ctx.get_manager()), m_context(ctx), m_subst(m), m_unif(m), m_head(m), m_tail(m), m_rule(nullptr) {}
/**
Reset substitution and get it ready for working with rule r.
As long as this object is used without a reset, the rule r must exist.
*/
void reset(rule * r);
/** Reset substitution and unify tail tgt_idx of the target rule and the head of the src rule */
bool unify(expr * e1, expr * e2);
void get_result(rule_ref & res);
void display(std::ostream& stm) {
m_subst.display(stm);
}
};
class normalizer_cfg;
class normalizer_rw;
ast_manager & m;
context & m_context;
th_rewriter & m_simp;
arith_util a;
rule_substitution m_rule_subst;
ptr_vector<expr> m_todo;
obj_hashtable<expr> m_leqs;
app_ref_vector m_tail;
expr_ref_vector m_itail_members;
expr_ref_vector m_conj;
bool_vector m_tail_neg;
normalizer_cfg* m_cfg;
normalizer_rw* m_rw;
void simplify_expr(app * a, expr_ref& res);
/** return true if some propagation was done */
bool propagate_variable_equivalences(rule * r, rule_ref& res);
/** Return true if something was modified */
bool transform_rules(const rule_set & orig, rule_set & tgt);
public:
mk_interp_tail_simplifier(context & ctx, unsigned priority=40000);
~mk_interp_tail_simplifier() override;
/**If rule should be retained, assign transformed version to res and return true;
if rule can be deleted, return false.
This method is kind of useful, so it's public to allow other rules to use it,
e.g. on their intermediate results.
*/
bool transform_rule(rule * r, rule_ref& res);
rule_set * operator()(rule_set const & source) override;
};
};