souffle  2.0.2-371-g6315b36
ResolveAliases.h
Go to the documentation of this file.
1 /*
2  * Souffle - A Datalog Compiler
3  * Copyright (c) 2015, Oracle and/or its affiliates. All rights reserved
4  * Licensed under the Universal Permissive License v 1.0 as shown at:
5  * - https://opensource.org/licenses/UPL
6  * - <souffle root>/licenses/SOUFFLE-UPL.txt
7  */
8 
9 /************************************************************************
10  *
11  * @file ResolveAliases.h
12  *
13  ***********************************************************************/
14 
15 #pragma once
16 
17 #include "ast/Clause.h"
18 #include "ast/TranslationUnit.h"
21 #include <memory>
22 #include <string>
23 
24 namespace souffle::ast::transform {
25 
26 /**
27  * Transformation pass to eliminate grounded aliases.
28  * e.g. resolve: a(r) , r = [x,y] => a(x,y)
29  * e.g. resolve: a(x) , !b(y) , y = x => a(x) , !b(x)
30  */
31 class ResolveAliasesTransformer : public Transformer {
32 public:
33  std::string getName() const override {
34  return "ResolveAliasesTransformer";
35  }
36 
37  /**
38  * Converts the given clause into a version without variables aliasing
39  * grounded variables.
40  *
41  * @param clause the clause to be processed
42  * @return a modified clone of the processed clause
43  */
44  static Own<Clause> resolveAliases(const Clause& clause);
45 
46  /**
47  * Removes trivial equalities of the form t = t from the given clause.
48  *
49  * @param clause the clause to be processed
50  * @return a modified clone of the given clause
51  */
52  static Own<Clause> removeTrivialEquality(const Clause& clause);
53 
54  /**
55  * Removes complex terms in atoms, replacing them with constrained variables.
56  *
57  * @param clause the clause to be processed
58  * @return a modified clone of the processed clause
59  */
60  static Own<Clause> removeComplexTermsInAtoms(const Clause& clause);
61 
62  ResolveAliasesTransformer* clone() const override {
63  return new ResolveAliasesTransformer();
64  }
65 
66 private:
67  bool transform(TranslationUnit& translationUnit) override;
68 };
69 
70 } // namespace souffle::ast::transform
souffle::ast::transform::ResolveAliasesTransformer::removeTrivialEquality
static Own< Clause > removeTrivialEquality(const Clause &clause)
Removes trivial equalities of the form t = t from the given clause.
Definition: ResolveAliases.cpp:368
TranslationUnit.h
souffle::Own
std::unique_ptr< A > Own
Definition: ContainerUtil.h:42
Transformer.h
souffle::ast::Clause
Intermediate representation of a horn clause.
Definition: Clause.h:51
ContainerUtil.h
souffle::ast::TranslationUnit
Translation unit class for the translation pipeline.
Definition: TranslationUnit.h:51
souffle::ast::transform::ResolveAliasesTransformer
Transformation pass to eliminate grounded aliases.
Definition: ResolveAliases.h:35
souffle::ast::transform
Definition: Program.h:45
souffle::ast::transform::ResolveAliasesTransformer::clone
ResolveAliasesTransformer * clone() const override
Definition: ResolveAliases.h:70
souffle::ast::transform::ResolveAliasesTransformer::getName
std::string getName() const override
Definition: ResolveAliases.h:41
souffle::ast::transform::ResolveAliasesTransformer::transform
bool transform(TranslationUnit &translationUnit) override
Definition: ResolveAliases.cpp:479
Clause.h
souffle::ast::transform::ResolveAliasesTransformer::resolveAliases
static Own< Clause > resolveAliases(const Clause &clause)
Converts the given clause into a version without variables aliasing grounded variables.
Definition: ResolveAliases.cpp:214
souffle::ast::transform::ResolveAliasesTransformer::removeComplexTermsInAtoms
static Own< Clause > removeComplexTermsInAtoms(const Clause &clause)
Removes complex terms in atoms, replacing them with constrained variables.
Definition: ResolveAliases.cpp:389