Emit errors for ignored execution plan

[adamjseitz]

This is intended to address #2351.

It seems that user-provided execution plans are silently ignored for non-recursive and subsumptive clauses. I added an explicit error message if a user provides plans that will be ignored.

Maybe this should be a warning, instead, though, as it may break currently-working programs.

[adamjseitz]

Looking at the test results, the test semantic/subsumption_multiple_rules includes a subsumption rule with a .plan directive:

C(x1) <= C(x2) :-
    D(x1, x2),
    x1 <= x2.
    .plan 0:(1,3,2)

Enabling/disabling the .plan directive does seem to have an effect on execution order - here's the transformed RAM with and without:

  DEBUG "C(x1) <= C(x2) :- \n   D(x1,x2),\n   x1 <= x2. .plan 0:(1,3,2)\nin file subsumption_multiple_rules.dl [59:1-62:20]"
   QUERY
    IF ((NOT ISEMPTY(C)) AND (NOT ISEMPTY(D)))
     FOR t0 IN C
      FOR t1 IN D ON INDEX t1.0 = t0.0 AND t0.0 <= t1.1
       IF ((NOT (t0.0 = t1.1)) AND (t1.1) IN C)
        INSERT (t0.0) INTO @delete_C
   END QUERY
  END DEBUG
  QUERY

  DEBUG "C(x1) <= C(x2) :- \n   D(x1,x2),\n   x1 <= x2. .plan 0:(1,3,2)\nin file subsumption_multiple_rules.dl [59:1-62:20]"
   QUERY
    IF ((NOT ISEMPTY(C)) AND (NOT ISEMPTY(D)))
     FOR t0 IN C
      FOR t1 IN D ON INDEX t1.0 = t0.0 AND t0.0 <= t1.1
       IF ((NOT (t0.0 = t1.1)) AND (t1.1) IN C)
        INSERT (t0.0) INTO @delete_C
   END QUERY
  END DEBUG
  QUERY

So it looks like the ExecutionPlanChecker should not be skipping subsumptive clauses. Adding an invalid plan statement reaches an assertion:

C(x1) <= C(x2) :-
    D(x1, x2),
    x1 <= x2.
    .plan 0:(1,3,2,4)

souffle: /home/aseitz/Projects/souffle/src/ast/utility/Utils.cpp:154: std::vector<souffle::ast::Atom*> souffle::ast::reorderAtoms(const std::vector<souffle::ast::Atom*>&, const std::vector<long unsigned int>&): Assertion `newOrder.size() == atoms.size()' failed.
Aborted (core dumped)

I will try to make changes so that ExecutionPlanChecker verifies .plan directives for subsumptive rules.

[codecov]

Codecov Report

Merging #2352 (19e3da8) into master (9abb420) will increase coverage by 0.01%.
The diff coverage is 68.34%.

Additional details and impacted files

@@            Coverage Diff             @@
##           master    #2352      +/-   ##
==========================================
+ Coverage   77.43%   77.45%   +0.01%     
==========================================
  Files         468      470       +2     
  Lines       29178    29332     +154     
==========================================
+ Hits        22594    22718     +124     
- Misses       6584     6614      +30     

Impacted Files	Coverage Δ
src/include/souffle/SouffleInterface.h	88.99% <ø> (ø)
src/interpreter/Engine.h	100.00% <ø> (ø)
src/parser/ParserDriver.h	100.00% <ø> (ø)
src/synthesiser/Synthesiser.h	100.00% <ø> (ø)
src/reports/ErrorReport.cpp	12.50% <12.50%> (ø)
...ouffle/datastructure/ConcurrentInsertOnlyHashMap.h	87.20% <60.00%> (+4.27%)	⬆️
src/main.cpp	69.21% <60.00%> (-0.51%)	⬇️
src/interpreter/Engine.cpp	84.58% <72.00%> (+0.51%)	⬆️
src/synthesiser/Synthesiser.cpp	84.91% <81.48%> (+0.23%)	⬆️
...rc/include/souffle/datastructure/ConcurrentCache.h	92.85% <92.85%> (ø)
... and 13 more

[b-scholz]

Thanks for fixing it!

[b-scholz]

Thanks for fixing it!