Throw SolverException when interpolation fails - #701
Conversation
…the solver state is SAT
OpenSMT doesn't support model generation for arrays and will only return abstract values when evaluting array variables. We therefore can't return a model when arrays were used in the constraints
…for the selected logic OpenSMT only supports interpolation for QF_UF, QF_LIA and QF_LRA and the logic needs to be explicitly set with `solver.opensmt.logic`
baierd
left a comment
baierd
left a comment
There was a problem hiding this comment.
Nice work! Only minor points to work on.
| // https://github.com/usi-verification-and-security/opensmt/issues/630 | ||
| throw new UnsupportedOperationException( | ||
| "OpenSMT does not support model generation when arrays are used"); | ||
| throw new SolverException("OpenSMT does not support model generation when arrays are used"); |
There was a problem hiding this comment.
Better: OpenSMT2 does not support model generation when using the theory of arrays
There was a problem hiding this comment.
Hmmm.. I think that message may also be a bit misleading: OpenSMT uses QF_AUFLIRA by default, and that's fine for model generation as long as no array variables are used in the constraints. The problem is really only with extracting assignments for array variables for the model. It would be possible to return a partial model where array variables are skipped, but for the sake of simplicity we currently just throw an error
There was a problem hiding this comment.
Not returning assignments for variables can be interpreted as "may be any value" and should be considered a bug. We can however add a option that allows this, and add a warning to the logger. (If you want, you can open a issue/branch/PR for this)
Thanks for the clarification though! We should definitely change the text to reflect this better. For example: "OpenSMT2 can not return satisfiable assignments for arrays. To avoid wrong interpretation, we disallow model export for queries including arrays." + potentially some info about the option should it be added.
There was a problem hiding this comment.
Thanks, I've now updated the message
| // https://github.com/usi-verification-and-security/opensmt/issues/630 | ||
| throw new UnsupportedOperationException( | ||
| "OpenSMT does not support model generation when arrays are used"); | ||
| throw new SolverException("OpenSMT does not support model generation when arrays are used"); |
There was a problem hiding this comment.
Not returning assignments for variables can be interpreted as "may be any value" and should be considered a bug. We can however add a option that allows this, and add a warning to the logger. (If you want, you can open a issue/branch/PR for this)
Thanks for the clarification though! We should definitely change the text to reflect this better. For example: "OpenSMT2 can not return satisfiable assignments for arrays. To avoid wrong interpretation, we disallow model export for queries including arrays." + potentially some info about the option should it be added.
OpenSMT doesn't support extraction of array values for the model. We abort model generation when the constraints contain formulas over arrays and print this message
2 participants
Hello,
this PR changes some runtime exceptions to
SolverExceptionsso that they can be better caught by the user. Specifically, we now throw aSolverExceptionif interpolation fails in Bitwuzla or Yices. This is in line with how interpolation failures are handled in MathSAT, which also only has partial interpolation support for some theories. In addition we throw aSolverExceptionin OpenSMT when model generation or interpolation are not available for the selected logicCloses #643