Aggregate Semantic Check Missing

[souffle-lang]

Aggregate Semantic Check Missing

[b-scholz]

The compiled version of Souffle works; however, the interpreter seg-faults in visitStore() in the RamExecutor.cpp.

[b-scholz]

I have further investigated the issue. The problem with that example is the following line

scc(A, C) :- C = min D : {mutually_reaching(A,B), id(B, D)}.

The issue is that here we assume that we not just compute the minimum value of the set

mutually_reaching(A,B), id(B, D)

but also request the witness environment for the minimum value. In this case, the witness environment would constitute of values for variables A, B, and D at the time when the
minimum was observed. The witness issue could be semantically justified for min/max. However, for counting, it would make no sense.

scc(A, C) :- C = count : {mutually_reaching(A,B), id(B, D)}.

There is no single value of A that could produce a sensible value for the relation scc.

[b-scholz]

I forgot to say because we don't have a semantic check that stops witnesses (and we don't store them at the moment), the above program produces either invalid results for variable A or crashes converting the invalid value of A to a symbol.

The easiest solution for the problem would be to check for witnesses and report warnings. Note that a witness is basically an unground variable in the outer scope of the aggregation. We would need a semantic check that prohibits unground variables in the outer scope that become grounded in the aggregation scope.

Alternatively, we permit witnesses for min/max and extend the interpreter and compiler for storing the witness environment. The runtime for aggregation may increase if a witness environment is stored. However, for this solution, we need still need the semantic check for the count-aggregation. For a count-aggregation, witnesses do not make sense and must not be permitted.

I would suggest to enforce the witness check first, i.e., no witnesses are permitted and later add the extension if required by some users.

As of pull request #387, there is now a test in tests/evaluation/count_sccs2/count_sccs2.dl for this issue. When this issue is solved, uncomment the line in evaluation.at marked with # TODO (see issue #128) POSITIVE_TEST([count_sccs2],[evaluation]) and update the relevant output files in the test directory.