Add congruence constraints for nodes

[daniel-larraz]

Select pairs of calls (C1, C2) to the same node N, and assert SoFar(I1=I2) => O1=O2 where I1 and O1 are the inputs and the outputs of call C1, and I2 and O2 are the inputs and the outputs of call C2.

The current implementation pairs calls to node N called by the top node with calls to node N called by direct subnodes of the top node that are abstract in the current analysis.

It includes an optimization that makes the outputs of two calls unconditionally equal when the provided inputs are syntactically equal.