souffle  2.0.2-371-g6315b36
AddNullariesToAtomlessAggregates.cpp
Go to the documentation of this file.
1 /*
2  * Souffle - A Datalog Compiler
3  * Copyright (c) 2020, The Souffle Developers. 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 AddNullariesToAtomlessAggregates.cpp
12  *
13  ***********************************************************************/
14 
16 #include "ast/Aggregator.h"
17 #include "ast/Atom.h"
18 #include "ast/Clause.h"
19 #include "ast/Literal.h"
20 #include "ast/Program.h"
21 #include "ast/QualifiedName.h"
22 #include "ast/Relation.h"
23 #include "ast/TranslationUnit.h"
24 #include "ast/utility/Utils.h"
25 #include "ast/utility/Visitor.h"
27 #include <algorithm>
28 #include <memory>
29 #include <utility>
30 #include <vector>
31 
32 namespace souffle::ast::transform {
33 
34 bool AddNullariesToAtomlessAggregatesTransformer::transform(TranslationUnit& translationUnit) {
35  bool changed{false};
36  Program& program = translationUnit.getProgram();
37  visitDepthFirst(program, [&](const Aggregator& agg) {
38  bool seenAtom{false};
39  for (const auto& literal : agg.getBodyLiterals()) {
40  if (isA<Atom>(literal)) {
41  seenAtom = true;
42  }
43  }
44  if (seenAtom) {
45  return;
46  }
47  // We will add in the Tautology atom to the body of this aggregate now
48  changed = true;
49  // +Tautology()
50  auto nullaryAtom = mk<Atom>();
51  std::string relName = "+Tautology";
52  nullaryAtom->setQualifiedName(relName);
53 
54  if (getRelation(program, relName) == nullptr) {
55  // +Tautology().
56  auto fact = mk<Clause>();
57  fact->setHead(souffle::clone(nullaryAtom));
58  // .decl +Tautology()
59  auto tautologyRel = mk<Relation>();
60  tautologyRel->setQualifiedName(relName);
61  program.addRelation(std::move(tautologyRel));
62  program.addClause(std::move(fact));
63  }
64  VecOwn<Literal> newBody;
65  for (const auto& lit : agg.getBodyLiterals()) {
66  newBody.push_back(souffle::clone(lit));
67  }
68  newBody.push_back(souffle::clone(nullaryAtom));
69  const_cast<Aggregator&>(agg).setBody(std::move(newBody));
70  });
71  return changed;
72 }
73 } // namespace souffle::ast::transform
souffle::ast::transform::AddNullariesToAtomlessAggregatesTransformer::transform
bool transform(TranslationUnit &translationUnit) override
Definition: AddNullariesToAtomlessAggregates.cpp:38
TranslationUnit.h
AddNullariesToAtomlessAggregates.h
MiscUtil.h
Relation.h
Utils.h
souffle::clone
auto clone(const std::vector< A * > &xs)
Definition: ContainerUtil.h:172
souffle::ast::getRelation
Relation * getRelation(const Program &program, const QualifiedName &name)
Returns the relation with the given name in the program.
Definition: Utils.cpp:101
Atom.h
Literal.h
souffle::ast::transform
Definition: Program.h:45
Aggregator.h
QualifiedName.h
Program.h
Visitor.h
Clause.h
souffle::ast::visitDepthFirst
void visitDepthFirst(const Node &root, Visitor< R, Ps... > &visitor, Args &... args)
A utility function visiting all nodes within the ast rooted by the given node recursively in a depth-...
Definition: Visitor.h:273