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.
0 replies
-
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.
1 reply
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
-
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