Task #5465

[z3][solver] solver errors elaboration scheme

Added by Sergey Smolov almost 6 years ago. Updated over 5 years ago.

Andrei Tatarnikov
Target version:
Start date:
Due date:
% Done:


Estimated time:
Detected in build:
Published in build:


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 Sergey Smolov almost 6 years ago

  • Subject changed from [z3][solver] to [z3][solver] solver errors elaboration scheme

Updated by Andrei Tatarnikov almost 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:

  1. Method Z3TextSolver.solve returns SolverResult.Status.ERROR if an error is detected before status information (sat, unsat, unknown) was read from the solver output.
  2. 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).

Updated by Sergey Smolov almost 6 years ago

  • Status changed from Resolved to Verified

Updated by Andrei Tatarnikov over 5 years ago

  • Status changed from Verified to Closed
  • Published in build set to 141226

Also available in: Atom PDF