Stratified aggregation

[guillembartrina]

This PR adds support for stratified aggregation in carac. For example, the counting of the transitive closure can now be expressed as follows:

val e = program.relation[Constant]("e")
val tc = program.relation[Constant]("tc")
val c = program.relation[Constant]("c")
val x, y, z = program.variable()

// Stratum 0
tc(x, y) :- e(x, y)
tc(x, y) :- (e(x, z), tc(z, y))

// Stratum 1
c(x, y) :- groupBy(tc(x, z), Seq(x), AggOp.COUNT(z) -> y)

// EDB
e("a", "b") :- ()
e("b", "c") :- ()
e("c", "d") :- ()
e("d", "e") :- ()
e("e", "f") :- ()
e("f", "g") :- ()

Changes

More specifically, it includes the following changes:

• The DSL is extended to support grouping atoms, of the form groupBy(ga(t1, ..., tn), [GV1, ..., GVm], AggOp.OP1(q1) -> AV1, ..., AggOp.OPk(qk) -> AVk). They are constructed using the groupBy object by specifying the grouping atom, the grouping variables and the different aggregations (operation, target and result). The grouping atoms are checked for validity
• PrecedenceGraph now also checks that the aggregate rules are properly stratified, reusing logic from stratified negation
• A new specialized index aggregator is introduced for grouping predicates
• CollectionsEDB is extended with two new operations: distinct and groupMapReduce over CollectionsRow
• The VolcanoStorageManager and DefaultStorageManager rule evaluation logic now support grouping operations
• The AST model is extended to support grouping atoms, with a new GroupingLogicAtom that has AggOpNodesubtrees. The StagedExecutionEngine now builds the extended AST.
• CopyEliminationPass is updated to properly handle grouping atoms
• A new IROp GroupingOp is introduced, and implemented by the interpreter and for three compilation targets: BytecodeCompiler, LambdaCompiler and QuoteCompiler
• IROpTreeGenerator now generates the grouping operations
• Added support to StagedSnippetExecutionEngine and StagedSnippetCompiler

Tests and examples

• Check that malformed grouping atoms are property detected
• Check that non-stratifiable aggregation is properly detected and aliases are correctly resolved
• Counting of transitive closure (tc_count test, with all execution engines)

Moreover, some additional tests illustrate stratified aggregation:

• Vertex degrees of a graph
• Max vertex degree of a graph
• Shortest edge in a graph

[aherlihy]

I see why this is needed but one day would like to be able to remove it, as well as all the asInstanceOf. We should be able to extend the Constant type to manage this eventually.

[guillembartrina]

Yes, I completely agree that this is a temporary solution. But I couldn't find another way that didn't require refactoring the entire Atom interface into a typed interface that forces declaring specific types for each 'column'. With dynamic types + domain interpretation, even if we assume that each constant has the appropriate type so we don't need to actively check it, we need to determine at runtime the specific types of the constants in order to apply the corresponding operator.

Unless you can come up with a better way to handle it, we either leave it as is or refactor the atom interface (not entirely trivial).

[aherlihy]

The one expression that is missing to have parity with the souffle docs is B(n, m) :- A(n, m), B(m, s), 2 * s = 2 * sum s : { A(n, s) } + 2... I suppose that is just regular arithmetic, or maybe I misunderstood what that example is doing. Do you know what that would look like using this syntax?

[guillembartrina]

I have implemented a relatively simple version of aggregates, more similar to what can be found in the literature than Soufflé's. For example, in this version the grouping atoms must be over a single grouping relation (many grouping relations can be emulated by creating a new relation that joins them); and, as I implemented the aggregates before playing with arithmetic expressions, no arithmetic expressions can appear in the grouping atoms (I believe they are also syntactic sugar and can be emulated with other constructs, provided we include arithmetic expressions in carac at some point).

[guillembartrina]

The closest you can get to coding the above rule is B(n, m) :- A(n, m), B(m, s), groupBy(A(n, x), Seq(n), SUM(x) -> s)