Pluggable fitness functions

[blexim]

Observation: for safety invariant generation, we might be more interested in a candidate solution being inductive than we are in it ruling out a particular violation.

As such, we might want to have the fitness function be +1 for initiation, +1 for safety, +3 for inductiveness. We think this is likely to help find good invariants faster.