Computing a value from the data itself

In the formula evaluator from Part 2, we had two extensionals:

input predicate node_var(id: integer, idx: integer).
input predicate num_vars(n: integer).

Using max, we can derive the second from the first:

highest_index(max(I)) :- node_var(_, I).
num_vars(N)           :- highest_index(M), N = M + 1.

This works as follows:

1. highest_index takes the largest index I over every node_var row.
2. Indices start at 0, so there are M + 1 variables.