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
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
dl_mk_similarity_compressor.h
Abstract:
<abstract>
Author:
Krystof Hoder (t-khoder) 2010-10-22.
Revision History:
--*/
#pragma once
#include<utility>
#include "util/map.h"
#include "util/obj_pair_hashtable.h"
#include "muz/base/dl_context.h"
#include "muz/base/dl_rule_set.h"
#include "muz/base/dl_rule_transformer.h"
namespace datalog {
/**
\brief Functor for merging groups of similar rules.
A rule sequence
P("1",x):-Q(x).
...
P("N",x):-Q(x).
will be replaced by
P(y,x):-Q(x), Aux(y).
and a set of facts
Aux("1").
...
Aux("N").
Similar transformation is performed when the varying constant appears in the positive tail.
*/
class mk_similarity_compressor : public rule_transformer::plugin {
context & m_context;
ast_manager & m_manager;
/** number of similar rules necessary for a group to be introduced */
unsigned m_threshold_count;
rule_vector m_rules;
rule_ref_vector m_result_rules;
bool m_modified;
ast_ref_vector m_pinned;
void merge_class(rule_vector::iterator first, rule_vector::iterator after_last);
void process_class(rule_set const& source, rule_vector::iterator first, rule_vector::iterator after_last);
void reset();
public:
mk_similarity_compressor(context & ctx);
rule_set * operator()(rule_set const & source) override;
};
}