get-interpolant interface for SMT-LIB2 frontend

[rainoftime]

Hi, I observed the recent paper "Interpolation and Model Checking for Nonlinear Arithmetic".
It seems that in the SMT-LIB2 frontend, Yices only exposes the get-unsat-model-interpolant interface.
Will the interpolant generation component be exposed to the frontend, e.g., via the name get-interpol or get-interpolant? (as in MathSAT and OpenSMT)

[dddejan]

There are two main issues with providing an interface for interpolation in SMTLIB

1. There is no set standard in the SMT language for interpolation commands. Also, this would require non-trivial changes to the parser.
2. Yices currently doesn't support output of terms in the SMTLIB2 language (see Model interpolants should be displayed in the SMT syntax #368)

Although it would be nice to have, it's not clear that providing the SMTLIB interface would be useful. The interpolation interface is available from the API so for now this seems good enough for current use cases (model checking).