Coln query/logical query program abstraction

[lstwn]

This PR adds a proper logical program (Datalog) layer in between the FLIR (which is essentially Datalog + implications) and the query IR. It is a real Datalog layer insofar that each rule must be in Horn-clause form, requiring a little translation to go from FLIR to logical program (especially true for constraints). The second translation from logical program to query IR is then handled just on top of this Datalog view without any knowledge of what a FLIR is.

• Stratified negation: Although the FLIR only knows negation indirectly through its use of implications in constraints so far, coln-query can now handle Datalog with stratified negation just fine, and uses it for the evaluation of implications. It works by putting the consequent into a helper predicate and negating it from the main predicate for the rule. Assume a constraint called rule with $\forall x, y, z. r(x, y, z) \land s(x) => t(y, z) \land u(z)$. This translates into:

  rule#consequent(y, z) :- t(y, z), u(z).
  rule(x, y, z) :- r(x, y, z), s(x), !rule#consequent(y, z).

• Constraints of shape: $\forall x, y. \implies r(x) \land s(x, y) \land t(y)$ "empty antecedent". This is now translated into:

  rule#consequent() :- r(x), s(x, y), t(y).
  rule() :- !rule#consequent()

  which is valid Datalog and only the translation layer injects the unit table (table with just one 0-tuple) as its left operand for the antijoin to work again.
• Constraints of shape: $\forall x, y. r(x, y) \land s(y) \implies x = y$ "single equality in antecedent". @olynch Unlike what we have agreed on during the coworking, please leave this as is and do not inject the antecedent into the consequent to ensure all consequent's variables are covered by some of its atoms. Coln-query does this now on demand and if you were to add this, I cannot optimize things further by adding selection(antecedent, x != y) on top of the query antecedent which computes, well, the antecedent. Whenever the consequent is just one Prop and all its variables are covered by the antecedent, the helper predicate can be omitted and "inlined", which I want to implement after my vacation.

For this to work properly, the logical program layer performs some static analysis checks:

1. Datalog's range restriction: All variables of the head must be bound in some positive atom of the body.
2. Stratified negation's negation safety: All variables of any negated atom must occur in a positive atom, too.
3. Comparison safety: All variables of any condition must occur in a positive atom, too.
4. Any atom's variable bindings are in the 0..arity range of its predicate and each referenced predicate has been declared ("no dangling predicates").
5. To support stratified negation, the predicate dependency graph is computed and along with it its quotient graph which collapses all strongly connected components (SCCs) into one super node. Stratified negation demands that each cycle within an SCC does not contain an edge stemming from a negated atom. We can also look at these graphs because I've implemented outputting them to Graphviz, which can be helpful for debugging once we have more load on the system. Rounded rectangles mark the SCCs. Green, dashed components are inputs and blue, dashed components are outputs. Black rectangles are intermediate components (or dead code 😄). An edge p -> s means that predicate p depends on s. A red edge with label ¬ indicates negation.

This is TransitiveClosure.coln:

This is GraphOfGraphs.coln:

And this is the Datalog pretty print of TransitiveClosure.coln:

.decl root.V(RowIdHash: uint, RowIdCtr: uint)

.decl root.E(RowIdHash: uint, RowIdCtr: uint, a.RowIdHash: uint, a.RowIdCtr: uint, b.RowIdHash: uint, b.RowIdCtr: uint)

.decl init.trans-closure.connected(a.RowIdHash: uint, a.RowIdCtr: uint, b.RowIdHash: uint, b.RowIdCtr: uint)
.output init.trans-closure.connected
// init.trans-closure.refl
init.trans-closure.connected(v.RowIdHash, v.RowIdCtr, v.RowIdHash, v.RowIdCtr) :-
    root.V(v.RowIdHash, v.RowIdCtr).
// init.trans-closure.snoc
init.trans-closure.connected(v0.RowIdHash, v0.RowIdCtr, v2.RowIdHash, v2.RowIdCtr) :-
    root.V(v0.RowIdHash, v0.RowIdCtr),
    root.V(v1.RowIdHash, v1.RowIdCtr),
    root.V(v2.RowIdHash, v2.RowIdCtr),
    init.trans-closure.connected(v0.RowIdHash, v0.RowIdCtr, v1.RowIdHash, v1.RowIdCtr),
    root.E(b.RowIdHash, b.RowIdCtr, v1.RowIdHash, v1.RowIdCtr, v2.RowIdHash, v2.RowIdCtr).

.decl root.E.foreignKey(a.RowIdHash: uint, a.RowIdCtr: uint, b.RowIdHash: uint, b.RowIdCtr: uint)
.output root.E.foreignKey
// root.E.foreignKey
root.E.foreignKey(a.RowIdHash, a.RowIdCtr, b.RowIdHash, b.RowIdCtr) :-
    root.E(_, _, a.RowIdHash, a.RowIdCtr, b.RowIdHash, b.RowIdCtr),
    !root.E.foreignKey#consequent(a.RowIdHash, a.RowIdCtr, b.RowIdHash, b.RowIdCtr).

.decl root.E.foreignKey#consequent(a.RowIdHash: uint, a.RowIdCtr: uint, b.RowIdHash: uint, b.RowIdCtr: uint)
// root.E.foreignKey#consequent
root.E.foreignKey#consequent(a.RowIdHash, a.RowIdCtr, b.RowIdHash, b.RowIdCtr) :-
    root.V(a.RowIdHash, a.RowIdCtr),
    root.V(b.RowIdHash, b.RowIdCtr).

@olynch: To your dismay, all friendliness is gone for good from the translation, so you won't find FriendlyVars and friends anymore on my next easter egg (bug?) which I've placed in some hard-to-find debug_assert!(side_effect) for you 😄.