search

SRI-CSL / yices2

The Yices SMT Solver
https://yices.csl.sri.com/
GNU General Public License v3.0
374 stars 48 forks source link

get-interpolant interface for SMT-LIB2 frontend #370

Open rainoftime opened 3 years ago

rainoftime commented 3 years ago

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 commented 3 years ago

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 #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).