Computing a value from the data itself

Remember Part 2’s formula evaluator? It needed an extra input, num_vars, supplied by hand in Part 1’s SAT solver:

extensional num_vars(n: integer).   # we had to provide this

A max over the variable leaves derives it from the formula itself:

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

highest_var(max(I)) stands alone, so it summarises the whole relation: the largest idx over every var leaf. The formula now provides its own variable count, so the num_vars extensional is gone.