Skip to content
New issue

Have a question about this project? # for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “#”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? # to your account

get_unsat_core for Optimize #268

Open
poscat0x04 opened this issue Nov 4, 2023 · 5 comments
Open

get_unsat_core for Optimize #268

poscat0x04 opened this issue Nov 4, 2023 · 5 comments

Comments

@poscat0x04
Copy link

Since there is support for getting unsat core from the optimizer in the C API/z3-sys, it would be nice to add it to the high level API as well.

@waywardmonkeys
Copy link
Contributor

I'll look at doing this in the next day or two if no one else submits it first.

@poscat0x04
Copy link
Author

Also, the unsat core generated by z3 will only contain assertions tracked using Z3_optimize_assert_and_track, which exists in the C API but for some reason isn't available in z3-sys

@waywardmonkeys
Copy link
Contributor

I've just added the binding to z3-sys for Z3_optimize_assert_and_track. Still working to find the time to do the rest.

@poscat0x04
Copy link
Author

no pressure :)

@toolCHAINZ
Copy link
Contributor

I just happened across this issue and thought I would chime in that I added high-level wrappers to these APIs in a PR back in June: #300

# for free to join this conversation on GitHub. Already have an account? # to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

3 participants