/
MinimiseProgram.h
86 lines (67 loc) · 2.71 KB
/
MinimiseProgram.h
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
/*
* Souffle - A Datalog Compiler
* Copyright (c) 2018, The Souffle Developers. All rights reserved
* Licensed under the Universal Permissive License v 1.0 as shown at:
* - https://opensource.org/licenses/UPL
* - <souffle root>/licenses/SOUFFLE-UPL.txt
*/
/************************************************************************
*
* @file MinimiseProgram.h
*
* Transformation pass to remove equivalent rules.
*
***********************************************************************/
#pragma once
#include "ast/transform/Transformer.h"
#include <string>
#include <vector>
namespace souffle {
class AstClause;
class AstTranslationUnit;
/**
* Transformation pass to remove equivalent rules.
*/
class MinimiseProgramTransformer : public AstTransformer {
public:
std::string getName() const override {
return "MinimiseProgramTransformer";
}
// Check whether two clauses are bijectively equivalent.
static bool areBijectivelyEquivalent(const AstClause* left, const AstClause* right);
MinimiseProgramTransformer* clone() const override {
return new MinimiseProgramTransformer();
}
private:
class NormalisedClauseRepr;
bool transform(AstTranslationUnit& translationUnit) override;
/** -- Bijective Equivalence Helper Methods -- */
// Check whether two normalised clause representations are equivalent.
static bool areBijectivelyEquivalent(const NormalisedClauseRepr& left, const NormalisedClauseRepr& right);
// Check whether a valid variable mapping exists for the given permutation.
static bool isValidPermutation(const NormalisedClauseRepr& left, const NormalisedClauseRepr& right,
const std::vector<unsigned int>& permutation);
/** -- Sub-Transformations -- */
/**
* Reduces locally-redundant clauses.
* A clause is locally-redundant if there is another clause within the same relation
* that computes the same set of tuples.
*/
static bool reduceLocallyEquivalentClauses(AstTranslationUnit& translationUnit);
/**
* Remove clauses that are only satisfied if they are already satisfied.
*/
static bool removeRedundantClauses(AstTranslationUnit& translationUnit);
/**
* Remove redundant literals within a clause.
*/
static bool reduceClauseBodies(AstTranslationUnit& translationUnit);
/**
* Removes redundant singleton relations.
* Singleton relations are relations with a single clause. A singleton relation is redundant
* if there exists another singleton relation that computes the same set of tuples.
* @return true iff the program was changed
*/
static bool reduceSingletonRelations(AstTranslationUnit& translationUnit);
};
} // end of namespace souffle