Refute side condition by transitivity of equality

[ttuegel]

Follow-up to #2089.

This is another unsatisfiable side condition which is not detected by Z3 or the backend itself:

    #Ceil ( #lookup ( 'QuesUnds'3 , int , 'QuesUnds'4:Int , int ) )
  #And
    {
      #lookup ( 'QuesUnds'3 , int , 'QuesUnds'4:Int , int )
    #Equals
      None
    }
  #And
    {
      #lookup ( 'QuesUnds'3 , int , 'QuesUnds'4:Int , int )
    #Equals
      Some I3:Int
    }

This side condition is unsatisfiable because None and Some are distinct constructors. #lookup isn't translated for the SMT solver because it is a partial function. However, it is known to be defined, so we could take advantage of that fact. (How?)

We could also use the first equality as a substitution to simplify the second equality. This would also solve #2032. We would need some heuristic for doing this; maybe: given \equals(function, constructor-at-top), substitute the right-hand side for the left-hand side everywhere.

[ttuegel]

@sskeirik Please replicate the kore-exec run that produced this condition, with the option --bug-report issue-2095, and attach the result to this issue.

[sskeirik]

Here is the issue tarball: https://drive.google.com/file/d/1rrLns6ARLqUC_KtJQY1xV1BmS10vC--P/view?usp=sharing

[virgil-serbanuta]

"However, it is known to be defined, so we could take advantage of that fact. (How?)"
We could translate a == b by first replacing it with (ceil(a) and ceil(b) and a==b) or (not ceil(a) and not ceil(b)), then simplifying the new expression. Then, in the resulting expression, we can translate a==b without caring about definedness.

The equality simplification thing is also a nice option.

[ttuegel]

Bug report: issue-2095.tar.gz

[ttuegel]

We could also use the first equality as a substitution to simplify the second equality. This would also solve #2032. We would need some heuristic for doing this; maybe: given \equals(function, constructor-at-top), substitute the right-hand side for the left-hand side everywhere.

I'm thinking of taking this approach because I realized it is a simple extensions of what I am doing in #2107.