Speed up counter example generation for PBESs using the winning strategy for the original

[mlaveaux]

This is a branch implementing the two phase approach for counter example generation. There is a flag --naive-counter-example-instantiation to revert to the previous method for comparison.

• [x] Implement the approach for pbessolve.
• [x] Implement the approach for pbessolvesymbolic, including the strategy generation and checking.
• [x] Added random tests for both approaches, not yet all variants.