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
108
109
110
111
112
113
114
115
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
dl_rule_transformer.h
Abstract:
<abstract>
Author:
Krystof Hoder (t-khoder) 2010-09-20.
Revision History:
--*/
#pragma once
#include "util/map.h"
#include "util/vector.h"
#include "muz/base/dl_rule.h"
#include "muz/base/dl_rule_set.h"
namespace datalog {
class context;
class rule_transformer {
public:
class plugin;
private:
friend class plugin;
typedef svector<plugin*> plugin_vector;
struct plugin_comparator;
context & m_context;
rule_manager & m_rule_manager;
bool m_dirty;
svector<plugin*> m_plugins;
void ensure_ordered();
public:
rule_transformer(context & ctx);
~rule_transformer();
/**
\brief Reset all registered transformers.
*/
void reset();
void cancel();
/**
\brief Add a plugin for rule transformation.
The rule_transformer object takes ownership of the plugin object.
*/
void register_plugin(plugin * p);
/**
\brief Transform the rule set using the registered transformation plugins. If the rule
set has changed, return true; otherwise return false.
*/
bool operator()(rule_set & rules);
};
class rule_transformer::plugin {
friend class rule_transformer;
unsigned m_priority;
bool m_can_destratify_negation;
rule_transformer * m_transformer;
void attach(rule_transformer & transformer) { m_transformer = &transformer; }
protected:
/**
\brief Create a plugin object for rule_transformer.
The priority argument determines in what order will rules be applied to the rules
(higher priority plugins will be applied first).
*/
plugin(unsigned priority, bool can_destratify_negation = false) : m_priority(priority),
m_can_destratify_negation(can_destratify_negation), m_transformer(nullptr) {}
public:
virtual ~plugin() = default;
unsigned get_priority() { return m_priority; }
bool can_destratify_negation() const { return m_can_destratify_negation; }
virtual void cancel() {}
/**
\brief Return \c rule_set object with containing transformed rules or 0 if no
transformation was done.
The caller takes ownership of the returned \c rule_set object.
*/
virtual rule_set * operator()(rule_set const & source) = 0;
/**
Removes duplicate tails.
*/
static void remove_duplicate_tails(app_ref_vector& tail, bool_vector& tail_neg);
};
};