[do not merge] profiling for lia in bsearch.v

[samuelgruetter]

No description provided.

[samuelgruetter]

This is to test the effects on lia of @thery's cond_hyps_factor:

Ltac cond_hyps_factor :=
    repeat match goal with
	   | [ H : ?x -> _, H' : ?x -> _ |- _ ] =>
		pose proof (fun u : x => conj (H u) (H' u)); clear H H' end.

Reporting the results for Coq 8.9.0 on my machine, but the CI builds of this PR provide results for Coq 8.9.1 and Coq master (note though, that on CI, .lia.cache is not deleted before processing bsearch.v, so the results might be inaccurate).

I varied two boolean options, resulting in 4 scenarios:

• The lia preprocessing can do Z.div_to_equations or Z.div_mod_to_equations. The former creates fewer hypotheses and is sufficient for the file being tested (because we manually take care of the mod aspects), but it would be more convenient to always call the latter, without having to manually take care of the mod aspects.
• We can call or not call cond_hyps_factor before lia.

Z.div_to_equations and no cond_hyps_factor:

total time      63.569s
% in lia        76.7%
secs in lia     48.75s
secs in rest    14.81s

Z.div_to_equations and cond_hyps_factor:

total time      55.638s
% in lia        73.2%
secs in lia     40.72s
secs in rest    14.91s

which means a 16% improvement on the time spent in lia.

Z.div_mod_to_equations and no cond_hyps_factor:

stack overflow

Z.div_mod_to_equations and cond_hyps_factor:

total time:    165.812s
% in lia        91.2%
secs in lia    151.22s

which means an improvement from infeasible (stack overflow) to feasible.