Midconditions lose information about read-only and logic variables.

Motivating Example:

examples/template/diff.lp @ 0146584 fails to synthesise a program, because the precondition of the second fragment (i.e. the midcondition of the template) is too weak:

[jjc311@pixel35:~/ws/main]$ ./TemplateLearn.hs ../examples/template/diff.lp 
Synthesising the program fragment between conditions:
   Pre:  X > Y, X0=X, Y0=Y.
   Post: X=Y0, Y=X0.
[...]
Found the following program:
   1. z = y
   2. y = x
   3. x = z
Searching for a counterexample to falsify the postcondition...
Success: the postcondition could not be falsified.

Synthesising the program fragment between conditions:
   Pre:  X=Y0, Y=X0.
   Post: X = X0-Y0, X > 0.
[...]
Found the following program:
   1. x = y - x
Searching for a counterexample to falsify the postcondition...
Failure: counterexamples were found, but none admitting a solution the postcondition. Possible causes:
- The postcondition is unsatisfiable for some valid input.
- The precondition is satisfiable for some invalid input.
- The given int_range is too small.
   Input:    y0 = -10, y = -10, x0 = -10, x = -10
   Expected: (none)
   Output:   x = 0

Cause:

The information that x0 > y0, which is required for the x > 0 part of the postcondition to hold, is lost when we insert the midcondition stating that x and y are swapped. Informally, we would expect not to have to repeat this assertion on each midcondition, because it's obvious that it continues to hold throughout the whole program.

Possible solution:

We can explicitly propagate information from previous program states by renaming mutable variables in each midcondition (so that they're unique, and represent the variable's value at a particular point in time) and adding them to the precondition of each program fragment that is executed after that point.

An example of this done manually is the commented-out line template(2, mid("X=Y0, Y=X0, X1 > Y1, X0=X1, Y0=Y1")). in diff.lp which includes information from precondition, with the mutable variables renamed to X1 and Y1. Replacing the existing midcondition with this, the program is synthesised correctly:

Found the following program:
   1. x = y - x
Searching for a counterexample to falsify the postcondition...
Success: the postcondition could not be falsified.

The following program satisfies all conditions of the template:
   1. z = x
   2. x = y
   3. y = z
   4. x = y - x

joodicator / ic-while-synth