Replies: 2 comments 1 reply
-
|
This feature isn't really supported until it is used more seriously by @agurfinkel |
Beta Was this translation helpful? Give feedback.
-
|
In the mean time, you can use CHC solver to compute interpolants. Pairwise, sequence, and tree interpolants are supported. Should work for arithmetic (linear/real), arrays, bit-vectors (maybe), and ADTs (maybe). Some examples are here: https://github.com/agurfinkel/spacer-on-jupyter/blob/master/Dagstuhl2019.ipynb |
Beta Was this translation helpful? Give feedback.
-
|
Thank you! I'll take a look at this. Does the reduction to CHC support using Z3's uninterpreted functions and built-in lists? |
Beta Was this translation helpful? Give feedback.
Uh oh!
There was an error while loading. Please reload this page.
-
I noticed that the latest version seems to have re-introduced support for getting interpolants. I am confused about how to use the new (get-interpolant) command and how much of Z3's theories it can handle? In particular, I have some code relying on the older (compute-interpolants) with a sequence of arguments. But it seems like (get-interpolant) only supports two arguments? Is it also expected to be much slower than (compute-interpolants)? Some documentation or examples with it would be appreciated.
Beta Was this translation helpful? Give feedback.
All reactions