souffle  2.0.2-371-g6315b36
ast_transformers_test.cpp
Go to the documentation of this file.
1 /*
2  * Souffle - A Datalog Compiler
3  * Copyright (c) 2013, 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 ast_transformers_test.cpp
12  *
13  * Tests souffle's AST transformers.
14  *
15  ***********************************************************************/
16 
17 #include "tests/test.h"
18 
19 #include "ast/Clause.h"
20 #include "ast/Node.h"
21 #include "ast/Program.h"
22 #include "ast/QualifiedName.h"
23 #include "ast/Relation.h"
24 #include "ast/TranslationUnit.h"
25 #include "ast/analysis/ClauseNormalisation.h"
26 #include "ast/transform/MagicSet.h"
27 #include "ast/transform/MinimiseProgram.h"
28 #include "ast/transform/RemoveRedundantRelations.h"
29 #include "ast/transform/RemoveRelationCopies.h"
30 #include "ast/transform/ResolveAliases.h"
31 #include "ast/utility/Utils.h"
32 #include "parser/ParserDriver.h"
33 #include "reports/DebugReport.h"
34 #include "reports/ErrorReport.h"
35 #include "souffle/utility/ContainerUtil.h"
36 #include "souffle/utility/StringUtil.h"
37 #include <map>
38 #include <memory>
39 #include <set>
40 #include <string>
41 #include <vector>
42 
43 namespace souffle::ast::transform::test {
44 using namespace analysis;
45 
46 TEST(Transformers, GroundTermPropagation) {
47  ErrorReport errorReport;
48  DebugReport debugReport;
49  // load some test program
50  Own<TranslationUnit> tu = ParserDriver::parseTranslationUnit(
51  R"(
52  .type D <: symbol
53  .decl p(a:D,b:D)
54 
55  p(a,b) :- p(x,y), r = [x,y], s = r, s = [w,v], [w,v] = [a,b].
56  )",
57  errorReport, debugReport);
58 
59  Program& program = tu->getProgram();
60 
61  // check types in clauses
62  Clause* a = getClauses(program, "p")[0];
63 
64  EXPECT_EQ("p(a,b) :- \n p(x,y),\n r = [x,y],\n s = r,\n s = [w,v],\n [w,v] = [a,b].",
65  toString(*a));
66 
67  Own<Clause> res = ResolveAliasesTransformer::resolveAliases(*a);
68  Own<Clause> cleaned = ResolveAliasesTransformer::removeTrivialEquality(*res);
69 
70  EXPECT_EQ(
71  "p(x,y) :- \n p(x,y),\n [x,y] = [x,y],\n [x,y] = [x,y],\n [x,y] = [x,y],\n [x,y] = "
72  "[x,y].",
73  toString(*res));
74  EXPECT_EQ("p(x,y) :- \n p(x,y).", toString(*cleaned));
75 }
76 
77 TEST(Transformers, GroundTermPropagation2) {
78  ErrorReport errorReport;
79  DebugReport debugReport;
80  // load some test program
81  Own<TranslationUnit> tu = ParserDriver::parseTranslationUnit(
82  R"(
83  .type D <: symbol
84  .decl p(a:D,b:D)
85 
86  p(a,b) :- p(x,y), x = y, x = a, y = b.
87  )",
88  errorReport, debugReport);
89 
90  Program& program = tu->getProgram();
91 
92  // check types in clauses
93  Clause* a = getClauses(program, "p")[0];
94 
95  EXPECT_EQ("p(a,b) :- \n p(x,y),\n x = y,\n x = a,\n y = b.", toString(*a));
96 
97  Own<Clause> res = ResolveAliasesTransformer::resolveAliases(*a);
98  Own<Clause> cleaned = ResolveAliasesTransformer::removeTrivialEquality(*res);
99 
100  EXPECT_EQ("p(b,b) :- \n p(b,b),\n b = b,\n b = b,\n b = b.", toString(*res));
101  EXPECT_EQ("p(b,b) :- \n p(b,b).", toString(*cleaned));
102 }
103 
104 TEST(Transformers, ResolveGroundedAliases) {
105  // load some test program
106  ErrorReport errorReport;
107  DebugReport debugReport;
108  Own<TranslationUnit> tu = ParserDriver::parseTranslationUnit(
109  R"(
110  .type D <: symbol
111  .decl p(a:D,b:D)
112 
113  p(a,b) :- p(x,y), r = [x,y], s = r, s = [w,v], [w,v] = [a,b].
114  )",
115  errorReport, debugReport);
116 
117  Program& program = tu->getProgram();
118 
119  EXPECT_EQ("p(a,b) :- \n p(x,y),\n r = [x,y],\n s = r,\n s = [w,v],\n [w,v] = [a,b].",
120  toString(*getClauses(program, "p")[0]));
121 
122  mk<ResolveAliasesTransformer>()->apply(*tu);
123 
124  EXPECT_EQ("p(x,y) :- \n p(x,y).", toString(*getClauses(program, "p")[0]));
125 }
126 
127 TEST(Transformers, ResolveAliasesWithTermsInAtoms) {
128  // load some test program
129  ErrorReport errorReport;
130  DebugReport debugReport;
131  Own<TranslationUnit> tu = ParserDriver::parseTranslationUnit(
132  R"(
133  .type D <: symbol
134  .decl p(a:D,b:D)
135 
136  p(x,c) :- p(x,b), p(b,c), c = b+1, x=c+2.
137  )",
138  errorReport, debugReport);
139 
140  Program& program = tu->getProgram();
141 
142  EXPECT_EQ("p(x,c) :- \n p(x,b),\n p(b,c),\n c = (b+1),\n x = (c+2).",
143  toString(*getClauses(program, "p")[0]));
144 
145  mk<ResolveAliasesTransformer>()->apply(*tu);
146 
147  EXPECT_EQ("p(x,c) :- \n p(x,b),\n p(b,c),\n c = (b+1),\n x = (c+2).",
148  toString(*getClauses(program, "p")[0]));
149 }
150 
151 /**
152  * Test that copies of relations are removed by RemoveRelationCopiesTransformer
153  *
154  * A(1, 2).
155  * B(x, y) :- A(x, y).
156  * C(x, y) :- B(x, y).
157  * D(x, y) :- C(x, y).
158  *
159  * -> D(x, y) :- A(x, y).
160  *
161  * B and C can be removed
162  *
163  */
164 
165 TEST(Transformers, RemoveRelationCopies) {
166  ErrorReport errorReport;
167  DebugReport debugReport;
168  // load some test program
169  Own<TranslationUnit> tu = ParserDriver::parseTranslationUnit(
170  R"(
171  .type D = number
172  .decl a(a:D,b:D)
173  .decl b(a:D,b:D)
174  .decl c(a:D,b:D)
175  .decl d(a:D,b:D)
176 
177  a(1,2).
178  b(x,y) :- a(x,y).
179  c(x,y) :- b(x,y).
180 
181  d(x,y) :- b(x,y), c(y,x).
182 
183  )",
184  errorReport, debugReport);
185 
186  Program& program = tu->getProgram();
187 
188  EXPECT_EQ(4, program.getRelations().size());
189 
190  RemoveRelationCopiesTransformer::removeRelationCopies(*tu);
191 
192  EXPECT_EQ(2, program.getRelations().size());
193 }
194 
195 /**
196  * Test that copies of relations are removed by RemoveRelationCopiesTransformer
197  *
198  * A(1, 2).
199  * B(x, y) :- A(x, y).
200  * C(x, y) :- B(x, y).
201  * D(x, y) :- C(x, y).
202  * .output C
203  *
204  * -> C(x, y) :- A(x, y).
205  * -> D(x, y) :- C(x, y).
206  *
207  * B can be removed, but not C as C is output
208  *
209  */
210 TEST(Transformers, RemoveRelationCopiesOutput) {
211  ErrorReport errorReport;
212  DebugReport debugReport;
213  // load some test program
214  Own<TranslationUnit> tu = ParserDriver::parseTranslationUnit(
215  R"(
216  .type D = number
217  .decl a(a:D,b:D)
218  .decl b(a:D,b:D)
219  .decl c(a:D,b:D)
220  .output c
221  .decl d(a:D,b:D)
222 
223  a(1,2).
224  b(x,y) :- a(x,y).
225  c(x,y) :- b(x,y).
226 
227  d(x,y) :- b(x,y), c(y,x).
228 
229  )",
230  errorReport, debugReport);
231 
232  Program& program = tu->getProgram();
233 
234  EXPECT_EQ(4, program.getRelations().size());
235 
236  RemoveRelationCopiesTransformer::removeRelationCopies(*tu);
237 
238  EXPECT_EQ(3, program.getRelations().size());
239 }
240 
241 /**
242  * Test the equivalence (or lack of equivalence) of clauses using the MinimiseProgramTransfomer.
243  */
244 TEST(Transformers, CheckClausalEquivalence) {
245  ErrorReport errorReport;
246  DebugReport debugReport;
247 
248  Own<TranslationUnit> tu = ParserDriver::parseTranslationUnit(
249  R"(
250  .decl A(x:number, y:number)
251  .decl B(x:number)
252  .decl C(x:number)
253 
254  A(0,0).
255  A(0,0).
256  A(0,1).
257 
258  B(1).
259 
260  C(z) :- A(z,y), A(z,x), x != 3, x < y, !B(x), y > 3, B(y).
261  C(r) :- A(r,y), A(r,x), x != 3, x < y, !B(y), y > 3, B(y), B(x), x < y.
262  C(x) :- A(x,a), a != 3, !B(a), A(x,b), b > 3, B(c), a < b, c = b.
263  )",
264  errorReport, debugReport);
265 
266  const auto& program = tu->getProgram();
267 
268  // Resolve aliases to remove trivial equalities
269  mk<ResolveAliasesTransformer>()->apply(*tu);
270  auto aClauses = getClauses(program, "A");
271  auto bClauses = getClauses(program, "B");
272  auto cClauses = getClauses(program, "C");
273 
274  EXPECT_EQ(3, aClauses.size());
275  EXPECT_EQ("A(0,0).", toString(*aClauses[0]));
276  EXPECT_EQ("A(0,0).", toString(*aClauses[1]));
277  EXPECT_EQ("A(0,1).", toString(*aClauses[2]));
278 
279  EXPECT_EQ(1, bClauses.size());
280  EXPECT_EQ("B(1).", toString(*bClauses[0]));
281 
282  EXPECT_EQ(3, cClauses.size());
283  EXPECT_EQ("C(z) :- \n A(z,y),\n A(z,x),\n x != 3,\n x < y,\n !B(x),\n y > 3,\n B(y).",
284  toString(*cClauses[0]));
285  EXPECT_EQ(
286  "C(r) :- \n A(r,y),\n A(r,x),\n x != 3,\n x < y,\n !B(y),\n y > 3,\n B(y),\n "
287  "B(x).",
288  toString(*cClauses[1]));
289  EXPECT_EQ("C(x) :- \n A(x,a),\n a != 3,\n !B(a),\n A(x,b),\n b > 3,\n B(b),\n a < b.",
290  toString(*cClauses[2]));
291 
292  // Check equivalence of these clauses
293  // -- A
294  const auto normA0 = NormalisedClause(aClauses[0]);
295  const auto normA1 = NormalisedClause(aClauses[1]);
296  const auto normA2 = NormalisedClause(aClauses[2]);
297  EXPECT_TRUE(MinimiseProgramTransformer::areBijectivelyEquivalent(normA0, normA1));
298  EXPECT_TRUE(MinimiseProgramTransformer::areBijectivelyEquivalent(normA1, normA0));
299  EXPECT_FALSE(MinimiseProgramTransformer::areBijectivelyEquivalent(normA1, normA2));
300  EXPECT_FALSE(MinimiseProgramTransformer::areBijectivelyEquivalent(normA0, normA2));
301 
302  // -- C
303  const auto normC0 = NormalisedClause(cClauses[0]);
304  const auto normC1 = NormalisedClause(cClauses[1]);
305  const auto normC2 = NormalisedClause(cClauses[2]);
306  EXPECT_TRUE(MinimiseProgramTransformer::areBijectivelyEquivalent(normC0, normC2));
307  EXPECT_FALSE(MinimiseProgramTransformer::areBijectivelyEquivalent(normC0, normC1));
308  EXPECT_FALSE(MinimiseProgramTransformer::areBijectivelyEquivalent(normC2, normC1));
309 
310  // Make sure equivalent (and only equivalent) clauses are removed by the minimiser
311  mk<MinimiseProgramTransformer>()->apply(*tu);
312  auto aMinClauses = getClauses(program, "A");
313  auto bMinClauses = getClauses(program, "B");
314  auto cMinClauses = getClauses(program, "C");
315 
316  EXPECT_EQ(2, aMinClauses.size());
317  EXPECT_EQ("A(0,0).", toString(*aMinClauses[0]));
318  EXPECT_EQ("A(0,1).", toString(*aMinClauses[1]));
319 
320  EXPECT_EQ(1, bMinClauses.size());
321  EXPECT_EQ("B(1).", toString(*bMinClauses[0]));
322 
323  EXPECT_EQ(2, cMinClauses.size());
324  EXPECT_EQ("C(z) :- \n A(z,y),\n A(z,x),\n x != 3,\n x < y,\n !B(x),\n y > 3,\n B(y).",
325  toString(*cMinClauses[0]));
326  EXPECT_EQ(
327  "C(r) :- \n A(r,y),\n A(r,x),\n x != 3,\n x < y,\n !B(y),\n y > 3,\n B(y),\n "
328  "B(x).",
329  toString(*cMinClauses[1]));
330 }
331 
332 /**
333  * Test the equivalence (or lack of equivalence) of aggregators using the MinimiseProgramTransfomer.
334  */
335 TEST(Transformers, CheckAggregatorEquivalence) {
336  ErrorReport errorReport;
337  DebugReport debugReport;
338 
339  Own<TranslationUnit> tu = ParserDriver::parseTranslationUnit(
340  R"(
341  .decl A,B,C,D(X:number) input
342  // first and second are equivalent
343  D(X) :-
344  B(X),
345  X < max Y : { C(Y), B(Y), Y < 2 },
346  A(Z),
347  Z = sum A : { C(A), B(A), A > count : { A(M), C(M) } }.
348 
349  D(V) :-
350  B(V),
351  A(W),
352  W = sum test1 : { C(test1), B(test1), test1 > count : { C(X), A(X) } },
353  V < max test2 : { C(test2), B(test2), test2 < 2 }.
354 
355  // third not equivalent
356  D(V) :-
357  B(V),
358  A(W),
359  W = min test1 : { C(test1), B(test1), test1 > count : { C(X), A(X) } },
360  V < max test2 : { C(test2), B(test2), test2 < 2 }.
361 
362  .output D()
363  )",
364  errorReport, debugReport);
365 
366  const auto& program = tu->getProgram();
367  mk<MinimiseProgramTransformer>()->apply(*tu);
368 
369  // A, B, C, D should still be the relations
370  EXPECT_EQ(4, program.getRelations().size());
371  EXPECT_NE(nullptr, getRelation(program, "A"));
372  EXPECT_NE(nullptr, getRelation(program, "B"));
373  EXPECT_NE(nullptr, getRelation(program, "C"));
374  EXPECT_NE(nullptr, getRelation(program, "D"));
375 
376  // D should now only have the two clauses non-equivalent clauses
377  const auto& dClauses = getClauses(program, "D");
378  EXPECT_EQ(2, dClauses.size());
379  EXPECT_EQ(
380  "D(X) :- \n B(X),\n X < max Y : { C(Y),B(Y),Y < 2 },\n A(Z),\n Z = sum A : { C(A),B(A),A "
381  "> count : { A(M),C(M) } }.",
382  toString(*dClauses[0]));
383  EXPECT_EQ(
384  "D(V) :- \n B(V),\n A(W),\n W = min test1 : { C(test1),B(test1),test1 > count : { "
385  "C(X),A(X) } },\n V < max test2 : { C(test2),B(test2),test2 < 2 }.",
386  toString(*dClauses[1]));
387 }
388 
389 /**
390  * Test the removal of redundancies within clauses using the MinimiseProgramTransformer.
391  *
392  * In particular, the removal of:
393  * - intraclausal literals equivalent to another literal in the body
394  * e.g. a(x) :- b(x), b(x), c(x). --> a(x) :- b(x), c(x).
395  * - clauses that are only trivially satisfiable
396  * e.g. a(x) :- a(x), x != 0. is only true if a(x) is already true
397  */
398 TEST(Transformers, RemoveClauseRedundancies) {
399  ErrorReport errorReport;
400  DebugReport debugReport;
401 
402  Own<TranslationUnit> tu = ParserDriver::parseTranslationUnit(
403  R"(
404  .decl a,b,c(X:number)
405  a(0).
406  b(1).
407  c(X) :- b(X).
408 
409  a(X) :- b(X), c(X).
410  a(X) :- a(X).
411  a(X) :- a(X), X != 1.
412 
413  q(X) :- a(X).
414 
415  .decl q(X:number)
416  .output q()
417  )",
418  errorReport, debugReport);
419 
420  const auto& program = tu->getProgram();
421 
422  // Invoking the `RemoveRelationCopiesTransformer` to create some extra redundancy
423  // In particular: The relation `c` will be replaced with `b` throughout, creating
424  // the clause b(x) :- b(x).
425  mk<RemoveRelationCopiesTransformer>()->apply(*tu);
426  EXPECT_EQ(nullptr, getRelation(program, "c"));
427  auto bIntermediateClauses = getClauses(program, "b");
428  EXPECT_EQ(2, bIntermediateClauses.size());
429  EXPECT_EQ("b(1).", toString(*bIntermediateClauses[0]));
430  EXPECT_EQ("b(X) :- \n b(X).", toString(*bIntermediateClauses[1]));
431 
432  // Attempt to minimise the program
433  mk<MinimiseProgramTransformer>()->apply(*tu);
434  EXPECT_EQ(3, program.getRelations().size());
435 
436  auto aClauses = getClauses(program, "a");
437  EXPECT_EQ(2, aClauses.size());
438  EXPECT_EQ("a(0).", toString(*aClauses[0]));
439  EXPECT_EQ("a(X) :- \n b(X).", toString(*aClauses[1]));
440 
441  auto bClauses = getClauses(program, "b");
442  EXPECT_EQ(1, bClauses.size());
443  EXPECT_EQ("b(1).", toString(*bClauses[0]));
444 
445  auto qClauses = getClauses(program, "q");
446  EXPECT_EQ(1, qClauses.size());
447  EXPECT_EQ("q(X) :- \n a(X).", toString(*qClauses[0]));
448 }
449 
450 /**
451  * Test the magic-set transformation on an example that covers all subtransformers, namely:
452  * (1) NormaliseDatabaseTransformer
453  * (2) LabelDatabaseTransformer
454  * (3) AdornDatabaseTransformer
455  * (4) MagicSetTransformer
456  */
457 TEST(Transformers, MagicSetComprehensive) {
458  ErrorReport e;
459  DebugReport d;
460 
461  Own<TranslationUnit> tu = ParserDriver::parseTranslationUnit(
462  R"(
463  // Stratum 0 - Base Relations
464  .decl BaseOne(X:number) magic
465  .decl BaseTwo(X:number) magic
466  .input BaseOne, BaseTwo
467 
468  // Stratum 1 [depends on: 0]
469  .decl A(X:number) magic
470  .decl B(X:number) magic
471  A(X) :- BaseOne(X).
472  A(X) :- BaseOne(X), B(X).
473  B(X) :- BaseTwo(X), A(X).
474 
475  // Stratum 2 [depends on: 0,1]
476  .decl C(X:number) magic
477  C(X) :- BaseTwo(X), A(X), B(X), X != 1.
478 
479  // Stratum 3 [depends on: 0,1]
480  .decl R(X:number) magic
481  R(X) :- BaseTwo(X), A(X), B(X), X != 0.
482 
483  // Stratum 4 [depends on: 0,1,2,3]
484  .decl D(X:number) magic
485  D(X) :- BaseOne(X), A(X), !C(X), !R(X).
486 
487  // Stratum 4 - Query [depends on: 0,1,4]
488  .decl Query(X:number) magic
489  .output Query
490  Query(X) :- BaseOne(X), D(X), A(X).
491  )",
492  e, d);
493 
494  auto& program = tu->getProgram();
495 
496  // Test helpers
497  auto mappifyRelations = [&](const Program& program) {
498  std::map<std::string, std::multiset<std::string>> result;
499  for (const auto* rel : program.getRelations()) {
500  std::multiset<std::string> clauseStrings;
501  auto relName = rel->getQualifiedName();
502  for (const auto* clause : getClauses(program, rel->getQualifiedName())) {
503  clauseStrings.insert(toString(*clause));
504  }
505  result[toString(relName)] = clauseStrings;
506  }
507  return result;
508  };
509  auto checkRelMapEq = [&](const std::map<std::string, std::multiset<std::string>> left,
510  const std::map<std::string, std::multiset<std::string>> right) {
511  EXPECT_EQ(left.size(), right.size());
512  for (const auto& [name, clauses] : left) {
513  EXPECT_TRUE(contains(right, name));
514  EXPECT_EQ(clauses, right.at(name));
515  }
516  };
517 
518  /* Stage 1: Database normalisation */
519  // Constants should now be extracted from the inequality constraints
520  mk<MagicSetTransformer::NormaliseDatabaseTransformer>()->apply(*tu);
521  const auto relations1 = program.getRelations();
522  EXPECT_EQ(8, program.getRelations().size());
523  EXPECT_EQ(7, program.getClauses().size());
524 
525  auto expectedNormalisation = std::map<std::string, std::multiset<std::string>>({
526  {"BaseOne", {}},
527  {"BaseTwo", {}},
528  {"A", {"A(X) :- \n BaseOne(X).", "A(X) :- \n BaseOne(X),\n B(X)."}},
529  {"B", {"B(X) :- \n BaseTwo(X),\n A(X)."}},
530  {"C", {"C(X) :- \n BaseTwo(X),\n A(X),\n B(X),\n X != @abdul0,\n @abdul0 = 1."}},
531  {"R", {"R(X) :- \n BaseTwo(X),\n A(X),\n B(X),\n X != @abdul0,\n @abdul0 = 0."}},
532  {"D", {"D(X) :- \n BaseOne(X),\n A(X),\n !C(X),\n !R(X)."}},
533  {"Query", {"Query(X) :- \n BaseOne(X),\n D(X),\n A(X)."}},
534  });
535  checkRelMapEq(expectedNormalisation, mappifyRelations(program));
536 
537  /* Stage 2: Database negative and positive labelling, keeping only the relevant ones */
538  /* Stage 2.1: Negative labelling */
539  mk<MagicSetTransformer::LabelDatabaseTransformer::NegativeLabellingTransformer>()->apply(*tu);
540  EXPECT_EQ(14, program.getRelations().size());
541  EXPECT_EQ(14, program.getClauses().size());
542 
543  auto expectedNegLabelling = std::map<std::string, std::multiset<std::string>>({
544  // Original strata - neglabels should appear on all negated appearances of relations
545  {"BaseOne", {}},
546  {"BaseTwo", {}},
547  {"A", {"A(X) :- \n BaseOne(X).", "A(X) :- \n BaseOne(X),\n B(X)."}},
548  {"B", {"B(X) :- \n BaseTwo(X),\n A(X)."}},
549  {"C", {"C(X) :- \n BaseTwo(X),\n A(X),\n B(X),\n X != @abdul0,\n @abdul0 = 1."}},
550  {"R", {"R(X) :- \n BaseTwo(X),\n A(X),\n B(X),\n X != @abdul0,\n @abdul0 = 0."}},
551  {"D", {"D(X) :- \n BaseOne(X),\n A(X),\n !@neglabel.C(X),\n !@neglabel.R(X)."}},
552  {"Query", {"Query(X) :- \n BaseOne(X),\n D(X),\n A(X)."}},
553 
554  // Neglaelled strata - relations should be copied and neglabelled one stratum at a time
555  {"@neglabel.A", {"@neglabel.A(X) :- \n BaseOne(X).",
556  "@neglabel.A(X) :- \n BaseOne(X),\n @neglabel.B(X)."}},
557  {"@neglabel.B", {"@neglabel.B(X) :- \n BaseTwo(X),\n @neglabel.A(X)."}},
558  {"@neglabel.C", {"@neglabel.C(X) :- \n BaseTwo(X),\n A(X),\n B(X),\n X != @abdul0,\n "
559  "@abdul0 = 1."}},
560  {"@neglabel.R", {"@neglabel.R(X) :- \n BaseTwo(X),\n A(X),\n B(X),\n X != @abdul0,\n "
561  "@abdul0 = 0."}},
562  {"@neglabel.D", {"@neglabel.D(X) :- \n BaseOne(X),\n A(X),\n !@neglabel.C(X),\n "
563  "!@neglabel.R(X)."}},
564  {"@neglabel.Query", {"@neglabel.Query(X) :- \n BaseOne(X),\n D(X),\n A(X)."}},
565  });
566  checkRelMapEq(expectedNegLabelling, mappifyRelations(program));
567 
568  /* Stage 2.2: Positive labelling */
569  mk<MagicSetTransformer::LabelDatabaseTransformer::PositiveLabellingTransformer>()->apply(*tu);
570  EXPECT_EQ(33, program.getRelations().size());
571  EXPECT_EQ(27, program.getClauses().size());
572 
573  auto expectedPosLabelling = std::map<std::string, std::multiset<std::string>>({
574  // Original strata should remain the same
575  {"BaseOne", {}},
576  {"BaseTwo", {}},
577  {"A", {"A(X) :- \n BaseOne(X).", "A(X) :- \n BaseOne(X),\n B(X)."}},
578  {"B", {"B(X) :- \n BaseTwo(X),\n A(X)."}},
579  {"C", {"C(X) :- \n BaseTwo(X),\n A(X),\n B(X),\n X != @abdul0,\n @abdul0 = 1."}},
580  {"R", {"R(X) :- \n BaseTwo(X),\n A(X),\n B(X),\n X != @abdul0,\n @abdul0 = 0."}},
581  {"D", {"D(X) :- \n BaseOne(X),\n A(X),\n !@neglabel.C(X),\n !@neglabel.R(X)."}},
582  {"Query", {"Query(X) :- \n BaseOne(X),\n D(X),\n A(X)."}},
583 
584  // Poslabelled + neglabelled strata - poslabel all positive derived literals
585  {"@neglabel.A", {"@neglabel.A(X) :- \n BaseOne(X).",
586  "@neglabel.A(X) :- \n BaseOne(X),\n @neglabel.B(X)."}},
587  {"@neglabel.B", {"@neglabel.B(X) :- \n BaseTwo(X),\n @neglabel.A(X)."}},
588  {"@neglabel.C", {"@neglabel.C(X) :- \n BaseTwo(X),\n @poscopy_1.A(X),\n @poscopy_1.B(X),\n "
589  " X != @abdul0,\n "
590  "@abdul0 = 1."}},
591  {"@neglabel.R", {"@neglabel.R(X) :- \n BaseTwo(X),\n @poscopy_2.A(X),\n @poscopy_2.B(X),\n "
592  " X != @abdul0,\n "
593  "@abdul0 = 0."}},
594  {"@neglabel.D",
595  {"@neglabel.D(X) :- \n BaseOne(X),\n @poscopy_3.A(X),\n !@neglabel.C(X),\n "
596  "!@neglabel.R(X)."}},
597  {"@neglabel.Query",
598  {"@neglabel.Query(X) :- \n BaseOne(X),\n @poscopy_1.D(X),\n @poscopy_4.A(X)."}},
599 
600  // Copies of input stratum
601  {"@poscopy_1.BaseOne", {}},
602  {"@poscopy_1.BaseTwo", {}},
603  {"@poscopy_2.BaseOne", {}},
604  {"@poscopy_2.BaseTwo", {}},
605  {"@poscopy_3.BaseOne", {}},
606  {"@poscopy_3.BaseTwo", {}},
607  {"@poscopy_4.BaseOne", {}},
608  {"@poscopy_4.BaseTwo", {}},
609  {"@poscopy_5.BaseOne", {}},
610  {"@poscopy_5.BaseTwo", {}},
611 
612  // Copies of {A,B} stratum
613  {"@poscopy_1.A", {"@poscopy_1.A(X) :- \n BaseOne(X).",
614  "@poscopy_1.A(X) :- \n BaseOne(X),\n @poscopy_1.B(X)."}},
615  {"@poscopy_1.B", {"@poscopy_1.B(X) :- \n BaseTwo(X),\n @poscopy_1.A(X)."}},
616  {"@poscopy_2.A", {"@poscopy_2.A(X) :- \n BaseOne(X).",
617  "@poscopy_2.A(X) :- \n BaseOne(X),\n @poscopy_2.B(X)."}},
618  {"@poscopy_2.B", {"@poscopy_2.B(X) :- \n BaseTwo(X),\n @poscopy_2.A(X)."}},
619  {"@poscopy_3.A", {"@poscopy_3.A(X) :- \n BaseOne(X).",
620  "@poscopy_3.A(X) :- \n BaseOne(X),\n @poscopy_3.B(X)."}},
621  {"@poscopy_3.B", {"@poscopy_3.B(X) :- \n BaseTwo(X),\n @poscopy_3.A(X)."}},
622  {"@poscopy_4.A", {"@poscopy_4.A(X) :- \n BaseOne(X).",
623  "@poscopy_4.A(X) :- \n BaseOne(X),\n @poscopy_4.B(X)."}},
624  {"@poscopy_4.B", {"@poscopy_4.B(X) :- \n BaseTwo(X),\n @poscopy_4.A(X)."}},
625 
626  // Copies of {D} stratum
627  {"@poscopy_1.D", {"@poscopy_1.D(X) :- \n BaseOne(X),\n @poscopy_4.A(X),\n "
628  "!@neglabel.C(X),\n !@neglabel.R(X)."}},
629  });
630  checkRelMapEq(expectedPosLabelling, mappifyRelations(program));
631 
632  /* Stage 2.3: Remove unnecessary labelled relations */
633  mk<RemoveRedundantRelationsTransformer>()->apply(*tu);
634  EXPECT_EQ(12, program.getRelations().size());
635  EXPECT_EQ(13, program.getClauses().size());
636 
637  auto expectedFullLabelling = std::map<std::string, std::multiset<std::string>>({
638  // Original strata
639  {"BaseOne", {}},
640  {"BaseTwo", {}},
641  {"A", {"A(X) :- \n BaseOne(X).", "A(X) :- \n BaseOne(X),\n B(X)."}},
642  {"B", {"B(X) :- \n BaseTwo(X),\n A(X)."}},
643  {"D", {"D(X) :- \n BaseOne(X),\n A(X),\n !@neglabel.C(X),\n !@neglabel.R(X)."}},
644  {"Query", {"Query(X) :- \n BaseOne(X),\n D(X),\n A(X)."}},
645 
646  // Neglabelled strata
647  {"@neglabel.C", {"@neglabel.C(X) :- \n BaseTwo(X),\n @poscopy_1.A(X),\n @poscopy_1.B(X),\n "
648  " X != @abdul0,\n "
649  "@abdul0 = 1."}},
650  {"@neglabel.R", {"@neglabel.R(X) :- \n BaseTwo(X),\n @poscopy_2.A(X),\n @poscopy_2.B(X),\n "
651  " X != @abdul0,\n "
652  "@abdul0 = 0."}},
653 
654  // Poslabelled strata
655  {"@poscopy_1.A", {"@poscopy_1.A(X) :- \n BaseOne(X).",
656  "@poscopy_1.A(X) :- \n BaseOne(X),\n @poscopy_1.B(X)."}},
657  {"@poscopy_1.B", {"@poscopy_1.B(X) :- \n BaseTwo(X),\n @poscopy_1.A(X)."}},
658  {"@poscopy_2.A", {"@poscopy_2.A(X) :- \n BaseOne(X).",
659  "@poscopy_2.A(X) :- \n BaseOne(X),\n @poscopy_2.B(X)."}},
660  {"@poscopy_2.B", {"@poscopy_2.B(X) :- \n BaseTwo(X),\n @poscopy_2.A(X)."}},
661  });
662  checkRelMapEq(expectedFullLabelling, mappifyRelations(program));
663 
664  /* Stage 3: Database adornment */
665  /* Stage 3.1: Adornment algorithm */
666  mk<MagicSetTransformer::AdornDatabaseTransformer>()->apply(*tu);
667  EXPECT_EQ(19, program.getRelations().size());
668  EXPECT_EQ(23, program.getClauses().size());
669 
670  auto expectedAdornment = std::map<std::string, std::multiset<std::string>>({
671  {"BaseOne", {}},
672  {"BaseTwo", {}},
673  {"A", {"A(X) :- \n BaseOne(X).", "A(X) :- \n BaseOne(X),\n B(X)."}},
674  {"B", {"B(X) :- \n BaseTwo(X),\n A(X)."}},
675  {"D", {"D(X) :- \n BaseOne(X),\n A(X),\n !@neglabel.C(X),\n !@neglabel.R(X)."}},
676 
677  {"@neglabel.C", {"@neglabel.C(X) :- \n BaseTwo(X),\n @poscopy_1.A.{b}(X),\n "
678  "@poscopy_1.B.{b}(X),\n X != @abdul0,\n @abdul0 = 1."}},
679  {"@neglabel.R", {"@neglabel.R(X) :- \n BaseTwo(X),\n @poscopy_2.A.{b}(X),\n "
680  "@poscopy_2.B.{b}(X),\n X != @abdul0,\n @abdul0 = 0."}},
681  {"@poscopy_1.A", {"@poscopy_1.A(X) :- \n BaseOne(X).",
682  "@poscopy_1.A(X) :- \n BaseOne(X),\n @poscopy_1.B(X)."}},
683  {"@poscopy_1.B", {"@poscopy_1.B(X) :- \n BaseTwo(X),\n @poscopy_1.A(X)."}},
684  {"@poscopy_2.A", {"@poscopy_2.A(X) :- \n BaseOne(X).",
685  "@poscopy_2.A(X) :- \n BaseOne(X),\n @poscopy_2.B(X)."}},
686  {"@poscopy_2.B", {"@poscopy_2.B(X) :- \n BaseTwo(X),\n @poscopy_2.A(X)."}},
687 
688  {"Query", {"Query(X) :- \n BaseOne(X),\n D.{b}(X),\n A.{b}(X)."}},
689  {"A.{b}", {"A.{b}(X) :- \n BaseOne(X).", "A.{b}(X) :- \n BaseOne(X),\n B.{b}(X)."}},
690  {"B.{b}", {"B.{b}(X) :- \n BaseTwo(X),\n A.{b}(X)."}},
691  {"D.{b}",
692  {"D.{b}(X) :- \n BaseOne(X),\n A.{b}(X),\n !@neglabel.C(X),\n !@neglabel.R(X)."}},
693  {"@poscopy_1.A.{b}", {"@poscopy_1.A.{b}(X) :- \n BaseOne(X).",
694  "@poscopy_1.A.{b}(X) :- \n BaseOne(X),\n @poscopy_1.B.{b}(X)."}},
695  {"@poscopy_1.B.{b}", {"@poscopy_1.B.{b}(X) :- \n BaseTwo(X),\n @poscopy_1.A.{b}(X)."}},
696  {"@poscopy_2.A.{b}", {"@poscopy_2.A.{b}(X) :- \n BaseOne(X).",
697  "@poscopy_2.A.{b}(X) :- \n BaseOne(X),\n @poscopy_2.B.{b}(X)."}},
698  {"@poscopy_2.B.{b}", {"@poscopy_2.B.{b}(X) :- \n BaseTwo(X),\n @poscopy_2.A.{b}(X)."}},
699 
700  });
701  checkRelMapEq(expectedAdornment, mappifyRelations(program));
702 
703  /* Stage 2.3: Remove no longer necessary relations */
704  mk<RemoveRedundantRelationsTransformer>()->apply(*tu);
705  EXPECT_EQ(12, program.getRelations().size());
706  EXPECT_EQ(13, program.getClauses().size());
707 
708  auto expectedFinalAdornment = std::map<std::string, std::multiset<std::string>>({
709  {"BaseOne", {}},
710  {"BaseTwo", {}},
711  {"@neglabel.C", {"@neglabel.C(X) :- \n BaseTwo(X),\n @poscopy_1.A.{b}(X),\n "
712  "@poscopy_1.B.{b}(X),\n X != @abdul0,\n @abdul0 = 1."}},
713  {"@neglabel.R", {"@neglabel.R(X) :- \n BaseTwo(X),\n @poscopy_2.A.{b}(X),\n "
714  "@poscopy_2.B.{b}(X),\n X != @abdul0,\n @abdul0 = 0."}},
715  {"Query", {"Query(X) :- \n BaseOne(X),\n D.{b}(X),\n A.{b}(X)."}},
716  {"A.{b}", {"A.{b}(X) :- \n BaseOne(X).", "A.{b}(X) :- \n BaseOne(X),\n B.{b}(X)."}},
717  {"B.{b}", {"B.{b}(X) :- \n BaseTwo(X),\n A.{b}(X)."}},
718  {"D.{b}",
719  {"D.{b}(X) :- \n BaseOne(X),\n A.{b}(X),\n !@neglabel.C(X),\n !@neglabel.R(X)."}},
720  {"@poscopy_1.A.{b}", {"@poscopy_1.A.{b}(X) :- \n BaseOne(X).",
721  "@poscopy_1.A.{b}(X) :- \n BaseOne(X),\n @poscopy_1.B.{b}(X)."}},
722  {"@poscopy_1.B.{b}", {"@poscopy_1.B.{b}(X) :- \n BaseTwo(X),\n @poscopy_1.A.{b}(X)."}},
723  {"@poscopy_2.A.{b}", {"@poscopy_2.A.{b}(X) :- \n BaseOne(X).",
724  "@poscopy_2.A.{b}(X) :- \n BaseOne(X),\n @poscopy_2.B.{b}(X)."}},
725  {"@poscopy_2.B.{b}", {"@poscopy_2.B.{b}(X) :- \n BaseTwo(X),\n @poscopy_2.A.{b}(X)."}},
726 
727  });
728  checkRelMapEq(expectedFinalAdornment, mappifyRelations(program));
729 
730  /* Stage 4: MST core transformation */
731  mk<MagicSetTransformer::MagicSetCoreTransformer>()->apply(*tu);
732  EXPECT_EQ(19, program.getRelations().size());
733  EXPECT_EQ(26, program.getClauses().size());
734 
735  auto finalProgram = std::map<std::string, std::multiset<std::string>>({
736  {"BaseOne", {}},
737  {"BaseTwo", {}},
738 
739  {"@neglabel.C", {"@neglabel.C(X) :- \n BaseTwo(X),\n @poscopy_1.A.{b}(X),\n "
740  "@poscopy_1.B.{b}(X),\n X != @abdul0,\n @abdul0 = 1."}},
741  {"@neglabel.R", {"@neglabel.R(X) :- \n BaseTwo(X),\n @poscopy_2.A.{b}(X),\n "
742  "@poscopy_2.B.{b}(X),\n X != @abdul0,\n @abdul0 = 0."}},
743 
744  {"A.{b}", {"A.{b}(X) :- \n @magic.A.{b}(X),\n BaseOne(X),\n B.{b}(X).",
745  "A.{b}(X) :- \n @magic.A.{b}(X),\n BaseOne(X)."}},
746  {"B.{b}", {"B.{b}(X) :- \n @magic.B.{b}(X),\n BaseTwo(X),\n A.{b}(X)."}},
747  {"D.{b}", {"D.{b}(X) :- \n @magic.D.{b}(X),\n BaseOne(X),\n A.{b}(X),\n "
748  "!@neglabel.C(X),\n !@neglabel.R(X)."}},
749 
750  {"@poscopy_1.A.{b}", {"@poscopy_1.A.{b}(X) :- \n @magic.@poscopy_1.A.{b}(X),\n BaseOne(X).",
751  "@poscopy_1.A.{b}(X) :- \n @magic.@poscopy_1.A.{b}(X),\n "
752  "BaseOne(X),\n @poscopy_1.B.{b}(X)."}},
753  {"@poscopy_1.B.{b}", {"@poscopy_1.B.{b}(X) :- \n @magic.@poscopy_1.B.{b}(X),\n BaseTwo(X),\n "
754  " @poscopy_1.A.{b}(X)."}},
755  {"@poscopy_2.A.{b}", {"@poscopy_2.A.{b}(X) :- \n @magic.@poscopy_2.A.{b}(X),\n BaseOne(X).",
756  "@poscopy_2.A.{b}(X) :- \n @magic.@poscopy_2.A.{b}(X),\n "
757  "BaseOne(X),\n @poscopy_2.B.{b}(X)."}},
758  {"@poscopy_2.B.{b}", {"@poscopy_2.B.{b}(X) :- \n @magic.@poscopy_2.B.{b}(X),\n BaseTwo(X),\n "
759  " @poscopy_2.A.{b}(X)."}},
760 
761  {"Query", {"Query(X) :- \n BaseOne(X),\n D.{b}(X),\n A.{b}(X)."}},
762 
763  // Magic rules
764  {"@magic.A.{b}", {"@magic.A.{b}(X) :- \n @magic.B.{b}(X),\n BaseTwo(X).",
765  "@magic.A.{b}(X) :- \n BaseOne(X),\n D.{b}(X).",
766  "@magic.A.{b}(X) :- \n @magic.D.{b}(X),\n BaseOne(X)."}},
767  {"@magic.B.{b}", {"@magic.B.{b}(X) :- \n @magic.A.{b}(X),\n BaseOne(X)."}},
768  {"@magic.D.{b}", {"@magic.D.{b}(X) :- \n BaseOne(X)."}},
769  {"@magic.@poscopy_1.A.{b}", {"@magic.@poscopy_1.A.{b}(X) :- \n BaseTwo(X),\n @abdul0 = 1.",
770  "@magic.@poscopy_1.A.{b}(X) :- \n "
771  "@magic.@poscopy_1.B.{b}(X),\n BaseTwo(X)."}},
772  {"@magic.@poscopy_2.A.{b}", {"@magic.@poscopy_2.A.{b}(X) :- \n BaseTwo(X),\n @abdul0 = 0.",
773  "@magic.@poscopy_2.A.{b}(X) :- \n "
774  "@magic.@poscopy_2.B.{b}(X),\n BaseTwo(X)."}},
775  {"@magic.@poscopy_1.B.{b}",
776  {"@magic.@poscopy_1.B.{b}(X) :- \n BaseTwo(X),\n @poscopy_1.A.{b}(X),\n @abdul0 = "
777  "1.",
778  "@magic.@poscopy_1.B.{b}(X) :- \n @magic.@poscopy_1.A.{b}(X),\n "
779  "BaseOne(X)."}},
780  {"@magic.@poscopy_2.B.{b}",
781  {"@magic.@poscopy_2.B.{b}(X) :- \n BaseTwo(X),\n @poscopy_2.A.{b}(X),\n @abdul0 = "
782  "0.",
783  "@magic.@poscopy_2.B.{b}(X) :- \n @magic.@poscopy_2.A.{b}(X),\n "
784  "BaseOne(X)."}},
785  });
786  checkRelMapEq(finalProgram, mappifyRelations(program));
787 }
788 } // namespace souffle::ast::transform::test
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
souffle::ParserDriver::parseTranslationUnit
static Own< ast::TranslationUnit > parseTranslationUnit(const std::string &filename, FILE *in, ErrorReport &errorReport, DebugReport &debugReport)
Definition: ParserDriver.cpp:84
EXPECT_TRUE
#define EXPECT_TRUE(a)
Definition: test.h:189
TranslationUnit.h
DebugReport.h
souffle::ast::analysis::NormalisedClause
Definition: ClauseNormalisation.h:46
RemoveRedundantRelations.h
souffle::contains
bool contains(const C &container, const typename C::value_type &element)
A utility to check generically whether a given element is contained in a given container.
Definition: ContainerUtil.h:75
EXPECT_EQ
#define EXPECT_EQ(a, b)
Definition: test.h:191
e
l j a showGridBackground &&c b raw series this eventEmitter e
Definition: htmlJsChartistMin.h:15
souffle::Own
std::unique_ptr< A > Own
Definition: ContainerUtil.h:42
souffle::ast::Clause
Intermediate representation of a horn clause.
Definition: Clause.h:51
souffle::ast::Program::getClauses
std::vector< Clause * > getClauses() const
Return clauses.
Definition: Program.h:65
Relation.h
Utils.h
souffle::toString
const std::string & toString(const std::string &str)
A generic function converting strings into strings (trivial case).
Definition: StringUtil.h:234
souffle::ast::Program
The program class consists of relations, clauses and types.
Definition: Program.h:52
ClauseNormalisation.h
ContainerUtil.h
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
souffle::DebugReport
Class representing a HTML report, consisting of a list of sections.
Definition: DebugReport.h:87
clauses
std::vector< Own< Clause > > clauses
Definition: ComponentInstantiation.cpp:67
StringUtil.h
souffle::ast::Program::getRelations
std::vector< Relation * > getRelations() const
Return relations.
Definition: Program.h:60
test.h
souffle::ast::getClauses
std::vector< Clause * > getClauses(const Program &program, const QualifiedName &relationName)
Returns a vector of clauses in the program describing the relation with the given name.
Definition: Utils.cpp:77
Node.h
EXPECT_NE
#define EXPECT_NE(a, b)
Definition: test.h:195
QualifiedName.h
souffle::ast::transform::MinimiseProgramTransformer::areBijectivelyEquivalent
static bool areBijectivelyEquivalent(const analysis::NormalisedClause &left, const analysis::NormalisedClause &right)
Definition: MinimiseProgram.cpp:190
Program.h
MinimiseProgram.h
souffle::ast::transform::test::TEST
TEST(Transformers, GroundTermPropagation)
Definition: ast_transformers_test.cpp:52
souffle::ast::transform::RemoveRelationCopiesTransformer::removeRelationCopies
static bool removeRelationCopies(TranslationUnit &translationUnit)
Replaces copies of relations by their origin in the given program.
Definition: RemoveRelationCopies.cpp:42
Clause.h
d
else d
Definition: htmlJsChartistMin.h:15
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
ParserDriver.h
RemoveRelationCopies.h
rel
void rel(size_t limit, bool showLimit=true)
Definition: Tui.h:1086
souffle::ast::Program::apply
void apply(const NodeMapper &map) override
Apply the mapper to all child nodes.
Definition: Program.h:139
souffle::ErrorReport
Definition: ErrorReport.h:152
souffle::ast::transform::test
Definition: ast_transformers_test.cpp:43
ErrorReport.h
MagicSet.h
EXPECT_FALSE
#define EXPECT_FALSE(a)
Definition: test.h:190
ResolveAliases.h
Generated by   doxygen 1.8.17