search

ahumenberger / Z3.jl

Julia interface to Z3
MIT License
57 stars 7 forks source link

Missing `ForAll` and `Exists` #17

Closed dpsanders closed 5 months ago

dpsanders commented 3 years ago

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

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

OK thanks, I'll try to do that!

mlhetland commented 1 year ago

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

remysucre commented 7 months ago

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 commented 5 months ago

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