Missing `ForAll` and `Exists`

[dpsanders]

I need to use quantified statements that include ForAll and Exists, but these seem to be missing currently, as far as I can see?

[ahumenberger]

These need to be added to https://github.com/Z3Prover/z3/blob/master/src/api/julia/z3jl.cpp, which lists types, methods, etc. from the Z3 C++ API which should be exposed in Julia. Apparently formal and exists are still missing there. So what needs to be done is to look at the Z3 C++ API, and add the missing entries to https://github.com/Z3Prover/z3/blob/master/src/api/julia/z3jl.cpp.

Unfortunately, my time is too limited right now to do it myself. PRs are very welcome, and I'll try to help as much as possible! Sorry for not responding earlier!

[dpsanders]

OK thanks, I'll try to do that!

[mlhetland]

Any progress on this? Would be great functionality to have in place :-)

[remysucre]

I exposed exists from the Z3 side and it will be available in the next Z3 release. You can also compile Z3 yourself to use it now, following the instructions here.

[remysucre]

Now you can use exists(ExprVector(ctx, [x, y, z]), e).