Add InterruptedExceptions to Model Generation #407
Conversation
…ecific exception when model generation is interrupted and throw a InterruptedExceptions
|
Note that adding a checked exception to a public method is an API-breaking change. For the |
|
I would prefer a solution as in #408 where the InterruptException is handled as RuntimeException. This keeps the signatures cleaner and is compatible with Java-defined interfaces like Iterator. |
|
I completely agree that this solution is ugly and breaking. However, i am unsure if we want to throw them as unchecked exceptions for the reasons Philipp pointed out. I am also unsure if users would expect the interrupt flag of the thread to be set even if we document it, as we have to return something in the methods. And if we return a empty model users might just never notice. |
|
Yes, setting the interrupted flag is really only good if the code can continue as it would without the interrupt. Dummy data should never be returned in place of real data. |
| satisfiableModel = Native.modelEval(z3context, model, formula, false, resultPtr); | ||
| } catch (Z3Exception e) { | ||
| throw new InterruptedException("Z3 model evaluation was interrupted."); | ||
| } |
There was a problem hiding this comment.
This code is wrong. Z3Exceptions can have other causes as well. Please use proper handling from Z3FormulaCreator.handleZ3Exception(e).
| return Native.optimizeGetModel(z3context, z3optSolver); | ||
| } catch (Z3Exception e) { | ||
| throw new InterruptedException("Z3 model generation interrupted."); | ||
| } |
There was a problem hiding this comment.
This code is wrong. Z3Exceptions can have other causes as well. Please use proper handling from Z3FormulaCreator.handleZ3Exception(e).
| try { | ||
| return Native.solverGetModel(z3context, z3solver); | ||
| } catch (Z3Exception e) { | ||
| throw new InterruptedException("Z3 model generation interrupted."); |
There was a problem hiding this comment.
This code is wrong. Z3Exceptions can have other causes as well. Please use proper handling from Z3FormulaCreator.handleZ3Exception(e).
| try { | ||
| return asList().iterator(); | ||
| } catch (InterruptedException pE) { | ||
| throw new RuntimeException(pE); |
There was a problem hiding this comment.
It would be nice to hide the runtime eexception here and just forward the InterruptedException, e.g., without changing the stacktrace and interrupt the exception trace.
| @@ -206,7 +208,8 @@ private Collection<ValueAssignment> getConstantArrayAssignment( | |||
| * @return a list of assignments {@code a[1]=0; a[2]=0; a[5]=0}. | |||
| */ | |||
| private Collection<ValueAssignment> getArrayAssignments( | |||
| long arraySymbol, long arrayFormula, long value, List<Object> upperIndices) { | |||
| long arraySymbol, long arrayFormula, long value, List<Object> upperIndices) | |||
| throws InterruptedException { | |||
| long evalDecl = Native.getAsArrayFuncDecl(z3context, value); | |||
| Native.incRef(z3context, evalDecl); | |||
| long interp = Native.modelGetFuncInterp(z3context, model, evalDecl); | |||
There was a problem hiding this comment.
Based on the annotations from https://github.com/Z3Prover/z3/blob/master/src/api/java/Model.java , it seems that methods like "modelGetFuncInterp" can also throw a Z3Exception. We might want to check more places for InterruptedException.
Adds
InterruptedExceptions to model generation and catch Z3s solver specific exception when model generation is interrupted and throw aInterruptedExceptioninstead.This adds the exception in quite a lot of places as we have the evaluation connected the model generation.
Also, we can't add the exception to the
Iteratorclass and i threw aRunTimeExceptioninstead. We probably want to throw a more precise exception here.Also, we should check if this is possible in other solvers as well.