search

prove-rs / z3.rs

Rust bindings for the Z3 solver.
337 stars 105 forks source link

`get_unsat_core` for `Optimize` #268

Open poscat0x04 opened 10 months ago

poscat0x04 commented 10 months ago

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

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

poscat0x04 commented 10 months ago

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

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

no pressure :)