[z3][solver] solver errors elaboration scheme
The following scheme is implemented now: when the solver verdict is "sat" and the solver output contains errors, an exception is thrown (see isSat method at ru.ispras.fortress.expression.ExprUtils class).
This scheme is incomplete, because we cannot detect critical errors when the solver verdict is "unsat", for example.
So the following scheme should be implemented:
While parsing Z3 solver output, only those errors should be taken into account, that come before the solver verdict (sat, unsat, unknown).
Those errors are critical and the library should throw an appropriate exception.
Errors that come after the solver verdict (such errors appears every time we call "get-model" when the verdict is "unsat"), can be treated as warnings/non-critical or ignored (as you wish). There is no need to throw an exception on them.
Updated by Andrei Tatarnikov about 6 years ago
- Status changed from New to Resolved
- % Done changed from 0 to 100
Done r723 and r724. Now it works in the following way:
- Method Z3TextSolver.solve returns SolverResult.Status.ERROR if an error is detected before status information (sat, unsat, unknown) was read from the solver output.
- Method ExprUtils.isSAT throws an exception if the solver result status is not SAT (in the case, true is returned) or UNSAT (in the case, false is returned).