Synthesise advice constraints in eqsat lowering.

[xlauko]

Implement synthesis of advice constraints from advice nodes and its arguments.

This allows to specify simpler patterns that creates new advices. We can just specify that advice a is equal to x in the context C1 and y in the context C2 as a = advice[x:C1, y:C2].

Lowering then creates required advice constraints for each context (they won't. be present in the egraph).