Optimize encodings of coherence and acyclicity (mostly IDL)

[ThomasHaas]

This PR adds a little trick to make the ordering constraints of some must-edges unconditional, i.e., it changes the encoding from exec(x) /\ exec(y) => clk(x) < clk(y) to clk(x) < clk(y) if possible.
The argument for when this can be done is quite subtle.

Most benefit is expected on eager encodings, especially for SC where I saw improvements in the range of 10-30%.
I think it might be worth having an SVCOMP run with this branch.

The optimization might also be applicable to the SAT encodings for acyclicty. I have not thought about this yet though.

EDIT: I have added the same optimization to the SAT encoding for acyclicity. I also saw some improvement, but not as big as in the IDL case.

[ThomasHaas]

See cna.c in #1016 for a benchmark where the optimizations of this PR are quite effectful.
IIRC, this is particularly the case for verifying program_spec of the #define FAIL version, where solving time went from 16 minutes down to 4-5 (using Z3/IDL encoding).

[hernanponcedeleon]

I did some evaluation and the results are really non-conclusive.

On SV-COMP benchmarks, the overall times (considering only safe benchmarks) show some regression when using IDL but some speed-up when using the default option (is there any functional change in the code for the base version or is this just noise?).

Configuration	Status (All)	CPU (s)	Wall (s)	Correct
dev-base	164	744	733	158
PR1015-base	164	647	634	159
dev-idl2sat	164	419	406	163
PR1015-idl2sat	164	439	425	163

Using our usual benchmarks, results change from model to model.

SC

AArch64

RC11

Considering there are cases where the optimization works well, we might want to get the code merged. However, we should have this guarded by a configuration option and I would not even enable it by default.

[ThomasHaas]

What do you mean by base version? The changes affect the encoding of acyclicity axioms (both IDL and SAT) and the IDL encoding for co (not the SAT encoding). So the only totally unaffected configuration should be idl2sat + lazy.

I think we should also get rid of all the benchmarks below 1 sec (or even below 10 sec) when evaluating changes. For many of them, the best solution is to not do analysis at all and just solve directly because processing/analyses are the biggest bottleneck.

The numbers of RC11 look interesting. I'm wondering how often the optimization even applies there.
I think I should add logger output with #strengthened acyclicity constraints (maybe this is around 0 and so there is basically only analysis overhead).
We might also want to wait until JavaSMT adds support for Z3 configs: sosy-lab/java-smt#626
This could affect the the benefit of this optimization, at least for Z3.

[hernanponcedeleon]

What do you mean by base version?
Base means --idl2sat=false

[ThomasHaas]

Then the SVCOMP evaluation shows improvements in the 10% range, no?
The optimizations were meant for the IDL-based encoding (as the PR title says).

[hernanponcedeleon]

The optimizations were meant for the IDL-based encoding (as the PR title says).

But the EDIT says you also optimized the SAT-based version, and in that case the evaluation suggests a regression for SVCOMP benchmarks

[ThomasHaas]

The optimizations is likely more effective for IDL. The SVCOMP regressions for idl2sat are mostly due to overhead in the encoding stage: there are many benchmarks where the analysis + encoding time is higher than the actual solving time, hence, adding even more analyses is almost always going to be bad.
Basically, to improve SVCOMP times, we need a totally different approach that does less up-front work and more quickly invokes the SMT solver.