Custom User Propagators

[niooii]

Hi, I was wondering if you planned to eventually provide a high-level API for defining custom propagators (needed for a problem I'm working on). If this wasn't planned, I can get started on drafting an implementation if you'd like. Thanks!

[toolCHAINZ]

Hello! We would like to do this eventually, but no one is working on it actively to my knowledge. If you'd like to contribute it would be very welcome!

There was a previous attempt at this by @puyral (see #344), but it has not seen any activity in some time. That PR was made back around z3.rs 0.12 and I have changed a lot of things since then (e.g. refcounting the context, enforcing that only one context is ever accessible in safe rust) which may alleviate some of the difficulties they ran into; you'll find some short discussion in that PR.

[puyral]

Yes, sorry, work sort of stalled on my end because I no longer need the user propagator and I am still sketch out by the lifetimes of fresh.

I actually have a partially working version using the new RC-like Context. I can try to finish.

[niooii]

Yes, sorry, work sort of stalled on my end because I no longer need the user propagator and I am still sketch out by the lifetimes of fresh.

I actually have a partially working version using the new RC-like Context. I can try to finish.

Actually, funnily enough I no longer need it as well, sorry for bringing it up 😅 Appreciate the timely response though!