Encode obvious equalities between register-read variables

[ThomasHaas]

No description provided.

[hernanponcedeleon]

In the SVCOMP benchmarks the new code manages to solve 2 more tasks with 1 min timeout, but overall (specially for the PASS case where times should be more stable) I would say things become slower.

@ThomasHaas for which of our benchmarks you saw some speed-up?

[ThomasHaas]

The one from #941 got a lot faster.
But I think I got around 10% also on cna.c with T=4 threads und B=4 under aarch64. I have not tested this on any other benchmarks.

Generally speaking, the equalities should never make the problem harder: they are "free" on the SMT level because the solver should just merge the variables.
That being said, the equalities could randomly affect the search heuristics but on average I would expect this to not change the verification time (sometimes it is better, sometimes it is worse).

[hernanponcedeleon]

I don't think we can infer that the extra constraints help just because you get 10% improvement in cna.c. I get the same variation on different runs with the same codebase, independently of the method

// Lazy - Run 1
> CFLAGS="-DNTHREADS=4" dartagnan/target/dartagnan-dev cat/aarch64.cat --target=arm8 benchmarks/locks/cna.c --bound=4
Test: benchmarks/locks/cna.c
Result: PASS
Time: 3:06 mins

// Lazy - Run 2
> CFLAGS="-DNTHREADS=4" dartagnan/target/dartagnan-dev cat/aarch64.cat --target=arm8 benchmarks/locks/cna.c --bound=4
Test: benchmarks/locks/cna.c
Result: PASS
Time: 2:50 mins

// Eager - Run 1
> CFLAGS="-DNTHREADS=4" dartagnan/target/dartagnan-dev cat/aarch64.cat --target=arm8 benchmarks/locks/cna.c --bound=4 --method=eager
Test: benchmarks/locks/cna.c
Result: PASS
Time: 2:54 mins

// Eager - Run 2
> CFLAGS="-DNTHREADS=4" dartagnan/target/dartagnan-dev cat/aarch64.cat --target=arm8 benchmarks/locks/cna.c --bound=4 --method=eager
Test: benchmarks/locks/cna.c
Result: PASS
Time: 2:45 mins

Since the SVCOMP results above where using yices2, I tried z3 but I still get that overall, the extra equalities introduce overhead

[ThomasHaas]

I don't think we can infer that the extra constraints help just because you get 10% improvement in cna.c. I get the same variation on different runs with the same codebase, independently of the method

Sure, I ran it around 8 times or so to get a feeling for the difference. It seemed to be positive overall on that one benchmark (using lazy). But I just reran the test 5 more times but with the eager encoding and there I didn't see any improvment.

Since the SVCOMP results above where using yices2, I tried z3 but I still get that overall, the extra equalities introduce overhead

The "overhead" is 1%. I think that falls into noise. The main question is if there is even a benchmark where merging actually happens in a meaningful way. I would not be surprised if in 95+% of the SVCOMP benchmarks nothing really changes.
This is because the added equalities are only relevant when you have merging data flow (phi nodes), because for non-merging data flow we already (indirectly) enforce the equalities due to #294, which gave a significant improvement back then. I assume if one disables the optimization from #294 then this PR would show more impact.

Anyways, if you don't find any improvements anywhere, then we don't need to merge this.
I think one aspect that hampers the benefit of merging the values of different register reads is that we still encode separate idd-edges for each read. Merging those edges might be more beneficial.