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
/*++
Copyright (c) 2013 Microsoft Corporation
Module Name:
mk_separate_negated_tails.h
Abstract:
Rule transformer which creates new rules for predicates
in negated tails that use free variables not used
elsewhere. These free variables incur an overhead
on the instructions compiled using dl_compiler.
Consider the following transformations:
P(x) :- Exists y, z, u . Q(x,y), !R(y,z), !T(z,u).
=>
P(x) :- Exists y, z . Q(x,y), !R(y,z), Exists u . ! T(z,u).
=>
P(x) :- Exists y, z . Q(x,y), !R(y,z), TN(z).
TN(z) :- !T(z,u).
Author:
Nikolaj Bjorner (nbjorner) 2013-09-09
Revision History:
--*/
#pragma once
#include "muz/base/dl_rule_transformer.h"
#include "muz/base/dl_context.h"
namespace datalog {
class mk_separate_negated_tails : public rule_transformer::plugin {
ast_manager & m;
rule_manager& rm;
context & m_ctx;
ptr_vector<expr> m_vars;
expr_free_vars m_fv;
bool has_private_vars(rule const& r, unsigned j);
void get_private_vars(rule const& r, unsigned j);
void abstract_predicate(app* p, app_ref& q, rule_set& rules);
void create_rule(rule const&r, rule_set& rules);
public:
mk_separate_negated_tails(context& ctx, unsigned priority = 21000);
rule_set * operator()(rule_set const & source) override;
};
}