[Civl] Enhance quantifier elimination

[shazqadeer]

TryElimination looks for a substitution for the lhs of single-static assignments on a path-by-path basis through an atomic action. If an assignment is of the form x := v where both x and v are variables, it is possible that x is defined but v is not. In such a case, the code change interprets the assignment as an equality and infers a definition v <-- x.

[bkragl]

This change looks logically correct to me.

Just wondering: I believe we had a heuristic like this (and also something with arrays) in the old transition relation computation that we wanted to eliminate in the rewrite. But I don't remember any details. Do you have any recollection?

Do you have a simple example that illustrates the practical needed for this change? I'm wondering if the changes to the TryElimination calls here are related.

[shazqadeer]

I have added a test this PR. If you comment out my code change, this example does not verify.

[shazqadeer]

Just wondering: I believe we had a heuristic like this (and also something with arrays) in the old transition relation computation that we wanted to eliminate in the rewrite. But I don't remember any details. Do you have any recollection?

I do remember that in the initial approach, all assignments were treated as bidirectional equalities. So the optimization I introduced would be automatically considered. Clearly, we dropped this approach in the new implementation. But I don't remember the rationale.

[shazqadeer]

I'm wondering if the changes to the TryElimination calls here are related.

I think you are referring to the changes that attempt TryElimination multiple times in an attempt to minimize the number of bound variables. The change I am proposing in this PR seems independent.

[bkragl]

I was specifically wondering about the removed TryElimination(trc.allLocVars.Select(v => varCopies[v][0]));, but I think it is indeed unrelated.

The added example is somewhat contrived, because a procedure and action with just an empty body would be equivalent. I guess I was unsure whether such assignments (where the expr is a variable) are useful in loop-free actions to express something in the most natural way. But I can imagine that it is the case if you have branching.

I'll approve the PR.