Z3 Interpolation API in Java not public

Apr 2, 2015 at 2:52 PM
Edited Apr 2, 2015 at 3:07 PM
Z3 team, thanks for making a Java binding for Z3. I've found it very useful in my projects.

I would like to to use interpolation functionality from Java and I'm wondering why
the methods GetInterpolant and ComputeInterpolant in InterpolationContext.java are not public. Is there is a reason for this?

Also, are there some examples that show how the interpolation api can be used form Java?

Thanks.
Coordinator
Apr 2, 2015 at 3:58 PM
Thanks for reporting this, that was simply an oversight. I've made those functions public now in the unstable branch. Note that we are currently in transition to a new repository, the latest code is available at github in the unstable branch.

There are no Java examples for interpolation yet, but if you try it with some smaller examples, we'd be happy to include it.
Apr 2, 2015 at 5:45 PM
Thanks for the quick turnaround. If I construct some good small examples I'll post back here.