Add Prover Based ShutdownManager

[baierd]

Most solvers allow either re-usable shutdown or we use shared environments that are created per prover, making them isolated enough to be shut down without stopping the context.

This PR adds a controlled way of shutting down only a single prover with the manager returned by our API IFF it is supported by the solver. These prover shutdown managers are all children of the context given shutdown manager.

[kfriedberger]

This PR might provide a solution for a quite old issue: https://github.com/sosy-lab/java-smt/issues/100 :-)

[baierd]

I cleaned up the default behavior of the prover API (isUnsat(), getModel(), getUnsatCore() etc.) so that they share the common prerequisites and no inconsistencies within the solver implementations exist.

I found 2 things i want to discuss:

1. The JavaDoc of unsatCoreOverAssumptions() states that: Returns an UNSAT core (if it exists, otherwise {@code Optional.empty()}), over the chosen assumptions. Does NOT require the {@link ProverOptions#GENERATE_UNSAT_CORE} option to work. But we have and check for the option GENERATE_UNSAT_CORE_OVER_ASSUMPTIONS. So i guess the JavaDoc should be updated?
2. the 2 public methods getSeqInterpolants0() and getTreeInterpolants0() are not named well in my opinion. I suggest better names like getSingletonSeqInterpolants)? (i am happy about better name suggestions ;D)

[baierd]

@kfriedberger @PhilippWendler i now merged #501 into this to get the Solver/InterruptedExceptions for the model and prover API. I also added them to getUnsatCore(). So now nearly every method in the prover throws both. This allows us to remove all that special handling for the exceptions (except iterator() ;D).

[PhilippWendler]

I just realized that ca14eff was even more important than I thought before.

If the intention of checkShutdownState() was "the method must not be called with shutdown already being triggered before", then this is not even possible. The following sequence can always happen:

1. Caller checks that no shutdown is triggered and decides to call a method like getUnsatCore.
2. Other thread triggers shutdown, e.g., due to timeout.
3. checkShutdownState() is called and throws.

This means that no matter what an application does, if it uses the shutdown interface as it is intended, it would randomly crash with IllegalStateException, which would be a bug.

So the only way to handle shutdown requests properly can be to throw InterruptedException, as it is done now I guess?

But note that it is unnecessary to check for shutdown immediately when entering a method. Because of the asynchronicity no method can and needs to guarantee that it always notices a shutdown. The only place where one needs to check for shutdowns is in loops that execute for potentially long time.

[baierd]

I just realized that ca14eff was even more important than I thought before.

If the intention of checkShutdownState() was "the method must not be called with shutdown already being triggered before", then this is not even possible. The following sequence can always happen:

1. Caller checks that no shutdown is triggered and decides to call a method like `getUnsatCore`.

2. Other thread triggers shutdown, e.g., due to timeout.

3. `checkShutdownState()` is called and throws.

This means that no matter what an application does, if it uses the shutdown interface as it is intended, it would randomly crash with IllegalStateException, which would be a bug.

So the only way to handle shutdown requests properly can be to throw InterruptedException, as it is done now I guess?

But note that it is unnecessary to check for shutdown immediately when entering a method. Because of the asynchronicity no method can and needs to guarantee that it always notices a shutdown. The only place where one needs to check for shutdowns is in loops that execute for potentially long time.

Oh wow! Good catch! This means that all the API changes are actually fully justified.