Genetic seeding

[blexim]

Observation: when synthesising safety invariants, ranking functions etc. we can often take a good guess at which subexpressions are likely to appear in the final result, e.g. for the program:

while (*) {
x++;
y--;
}

assert(x > y);

the expressions:
x+1
y-1
x>y
x+1 > y-1

are likely to appear in the final invariant. We can take advantage of this fact by seeding the first generation of the genetic synthesiser with any old subexpressions we can think of.

We can think of this as picking a good starting point in the space of all programs, which doesn't reduce the search space, but does make us more likely (heuristically) to find a solution quickly.

Conjecture: this cannot make the search worse than just random initialisation.