Optimize heterogeneous Apron join

[sim642]

Precise and modular static analysis by abstract interpretation for the automatic proof of program soundness and contracts inference provides a more efficient join operator for Apron abstractions with heterogeneous environments in Definition 6.12:

This version only applies the expensive strengthening operator to the constraints that are actually between the two environments.

[sim642]

Actually, at some point I came up with similar heuristics for adding back the constraints during strengthening:

analyzer/src/cdomains/apron/apronDomain.apron.ml

Lines 641 to 645 in ff0e24c

	(* Heuristically reorder constraints to pass 36/12 with singlethreaded->multithreaded mode switching. *)
	(* Put those constraints which strictly are in one argument's env first, to (hopefully) ensure they remain. *)
	let (x_cons1_some_y, x_cons1_only_x) = Array.partition (env_exists_mem_con1 y_env) x_cons1 in
	let (y_cons1_some_x, y_cons1_only_y) = Array.partition (env_exists_mem_con1 x_env) y_cons1 in
	Array.concat [x_cons1_only_x; y_cons1_only_y; x_cons1_some_y; y_cons1_some_x]

Although the linked implementation should achieve the same thing more efficiently: it does not have to try one-by-one to add x_cons1_only_x back but simply does so with one meet.