Add SolverException for Model and Prover due to MathSAT5/Z3 Model Problem (Including a Sneaky Throw for API not Supporting Changes)

[baierd]

MathSAT5s model iterator method may fail and throws an IllegalArgumentException. This exception is misleading, as it is a solver error when building the model. This PR catches the IllegalArgumentException and throws a sneaky SolverException instead. Catching and throwing a different exception removed the need to recompile the solver, but could be done later on. Since Z3 has similar issues, i added SolverException and InterruptedException to many API calls in the model and prover APIs.

Still, since the iterator API does not allow a checked exception, we have to throw it sneakily unfortunately.
I also added warnings in our JavaDoc for the location that may throw sneaky exceptions.

Closes: #481

[baierd]

@kfriedberger i don't know if we want to warn users about the sneaky throws, but it seems reasonable. What do you think?

[kfriedberger]

Except for the iterator interface in model class, and maybe due to backard compatibility, I do not see any strong reason to hide the exception in the signature.
Why can't we specify the exception in the methods push and addConstraint?

[baierd]

Except for the iterator interface in model class, and maybe due to backard compatibility, I do not see any strong reason to hide the exception in the signature. Why can't we specify the exception in the methods push and addConstraint?

Since last time we tried this we ended with many changes and a long discussion, i wanted to avoid this. But since we already plan a mayor release, i added all exceptions explicitly with the exception of the iterator.

[baierd]

@PhilippWendler @kfriedberger i updated the PR and the code with explicit exceptions as far as possible. Would you two be so kind and take another look?

[kfriedberger]

This is a rather big API change. This might cause some more changes in CPAchecker than done in https://gitlab.com/sosy-lab/software/cpachecker/-/merge_requests/234 (which is still open and unmerged). I am not convinced that this step is required and solves an issue: MathSAT will still crash on specific queries and CPAchecker will abort, with and without the new exception.

[PhilippWendler]

This is a rather big API change. This might cause some more changes in CPAchecker than done in gitlab.com/sosy-lab/software/cpachecker/-/merge_requests/234 (which is still open and unmerged).

There is no need to worry about CPAchecker, we can always adopt to JavaSMT API changes. It is your other users and your general API stability promise that you need to consider.

I am not convinced that this step is required and solves an issue: MathSAT will still crash on specific queries and CPAchecker will abort, with and without the new exception.

Whether something throws an unchecked exception or the checked SolverException in a particular situation makes a significant difference: The former signals something that is a bug and that the application can not continue in a meaningful manner and needs to terminate, and the bug needs to be investigated, reported, and fixed. The latter indicates that while the operation was not successful, this was something that one had to expect and there is no need to report it, plus that the application can safely continue.

And in CPAchecker, for example, we act accordingly: For the unchecked exception we terminate immediately and show a stack trace that should help for debugging. For the checked exception, depending on what exactly was done, we go on and try fallbacks (different solver options, maybe even different solver), or we simply skip the operation it if is not strictly required (we can still dump a counterexample even without the model), or we terminate the respective analysis but keep others in a portfolio running, or (if none of the above works) we gracefully terminate CPAchecker and print an error message for the user. So "CPAchecker will abort, with and without the new exception." is not correct. And I would expect (hope) that other users of JavaSMT treat exceptions similarly.

[PhilippWendler]

i updated the PR and the code with explicit exceptions as far as possible. Would you two be so kind and take another look?

I would typically not add the exception to the implementing (solver-specific) classes everywhere, but only where it is actually meaningful because the solver can produce them. For solvers where we know that a particular exception can not happen for a given operation, it might be useful to leave it out of the method signature, for example when calling the method out of solver-specific code or if for some other reason solver-specific code is called directly in the future in some use case, or simply as documentation of what can happen and what not.

Apart from this I didn't notice anything particular, though of course I didn't do a complete review.

[baierd]

Thank you both!

This is a rather big API change. This might cause some more changes in CPAchecker than done in https://gitlab.com/sosy-lab/software/cpachecker/-/merge_requests/234 (which is still open and unmerged). I am not convinced that this step is required and solves an issue: MathSAT will still crash on specific queries and CPAchecker will abort, with and without the new exception.

I know, hence i am unsure whether or not this is good.
But it seems like there are multiple paths that all lead to these API changes, so i fear that at some point we will end up with these changes anyways? And if that's the case, we can just do it all at once.

As Philipp says, we can manage in CPAchecker. And we do catch this exception in several Analyses (e.g. BMC and Predicate), it just looks weird that we catch a IllegalArgumentException when requesting a model (without arguments) ;D

I would typically not add the exception to the implementing (solver-specific) classes everywhere, but only where it is actually meaningful because the solver can produce them. For solvers where we know that a particular exception can not happen for a given operation, it might be useful to leave it out of the method signature, for example when calling the method out of solver-specific code or if for some other reason solver-specific code is called directly in the future in some use case, or simply as documentation of what can happen and what not.

The problem here is that we nearly always call evaluateImpl() or similar methods that are not solver specific, but can throw the 2 exceptions.

In general it seems like SolverException can happen for Z3 (nearly) everywhere. For MathSAT5 in model calls depending on asList(), but since we use a caching model which calls this immediately, we know that this will therefore also fail immediately.

InterruptedException can really happen everywhere, as we should not use the prover once the notifier has been triggered.

We can of course communicate this! We could also just catch the exceptions in solvers that we know/think do never throw this so that the exception is gone in the internal implementations.

[PhilippWendler]

I would typically not add the exception to the implementing (solver-specific) classes everywhere, but only where it is actually meaningful because the solver can produce them. For solvers where we know that a particular exception can not happen for a given operation, it might be useful to leave it out of the method signature, for example when calling the method out of solver-specific code or if for some other reason solver-specific code is called directly in the future in some use case, or simply as documentation of what can happen and what not.

The problem here is that we nearly always call evaluateImpl() or similar methods that are not solver specific, but can throw the 2 exceptions.

We could also just catch the exceptions in solvers that we know/think do never throw this so that the exception is gone in the internal implementations.

No, I would keep it easy. Just remove the exceptions declarations (transitively) from those places where the Java compiler does not require them (just classes, don't change the public API).

[baierd]

No, I would keep it easy. Just remove the exceptions declarations (transitively) from those places where the Java compiler does not require them (just classes, don't change the public API).

As i said, the problem is the usage of evaluateImpl(). Those calls can throw these exceptions and we use this and other generic generic methods that throw these exceptions.

I've now removed them from the solvers that do not throw them by overriding evaluateImpl() in them and catch the exceptions in exactly 1 method getModelAssignments(). Would you be so kind and take a look? Maybe there is a better way that i don't see right now.

[PhilippWendler]

No, I would keep it easy. Just remove the exceptions declarations (transitively) from those places where the Java compiler does not require them (just classes, don't change the public API).

As i said, the problem is the usage of evaluateImpl(). Those calls can throw these exceptions and we use this and other generic generic methods that throw these exceptions.

I've now removed them from the solvers that do not throw them by overriding evaluateImpl() in them and catch the exceptions in exactly 1 method getModelAssignments(). Would you be so kind and take a look? Maybe there is a better way that i don't see right now.

I would even say the additional catch clauses are not worth it. After all, it might change in the future. My comment was really just mean to say "only add the throws declarations where the compiler forces you, not everywhere for consistency (with respect to the implementing classes, not API)".