WIP: Add bindings to the user propagator

[puyral]

This adds bindings and an API for the user propagator and the on_clause callback.

I would consider this still experimental, as I'm not fully sure of what z3 might do with my objects (e.g., weird lifetimes and thread safety).

This also closes #343

[puyral]

So apparently Ubuntu ships with a version of z3 that is too old for the user propagator...

[puyral]

So I discovered that we can get null pointer back from z3 with my implementation of fresh_eh (which will result in a crash).

TL;DR: current lifetimes don't match z3's and I don't yet have a solution to make them agree with Rust's borrow checker assumptions.

Currently, it actually returns the null pointer that z3 gives back. This was done on purpose because implementing this function causes me huge lifetimes problems.

To give an idea of the problem. The C++ implementation for fresh says:

user_propagators created using fresh() are created during search, and their lifetimes are restricted to search time. They should be garbage collected by the propagator used to invoke fresh(). The life-time of the Z3_context object can only be assumed valid during callbacks, such as fixed(), which contains expressions based on the context.

In practice, z3 gives a new Z3_context that the inner solver will use. I understand that this context may get garbage collected before we reach the end of the search. So, no z3 object should "escape" the user propagator.
To add to the problem, it's our responsibility to garbage collect the subsolver's user propagator. We don't know when we should drop it, aside from the fact that it should happen before the very end of the search. At that point, that user propagator is almost sure to hold invalid pointers/references (e.g., the Context) that might cause UB during Drop.

These problems tend to cascade effects to the rest of the user propagator API.

I'm switching this into a draft since I don't have an immediate solution.

If you are using z3 in a way that won't spawn subsolvers, then you are safe to use the current API.

[toolCHAINZ]

It may be worth revisiting this in light of #401, #404, and #417.

Now that contexts are refcounted and implicit, there shouldn't be an issue dealing with arcane lifetimes. The trick would be designing the API to ensure correctness and memory safety in the face of callbacks that use Contexts we do not control.

I haven't done a detailed read of the contribution you have here, but going from your description of the difficulty, there's a general approach that I think could work:

• Change ContextInternal to an enum, with an internal "owned" variant (what it has right now) and a "borrowed" variant (which can be unsafely created from a raw Z3_Context). The "owned" variant would behave as it does now, destroying the inner context on Drop. The "borrowed" variant would not, making it suitable for cases like this where we are given a Context that Z3 itself is managing.
• Any Rust code running in this user propagator context would have to be expressed in a Send + Sync closure. There would be a wrapper that receives the Z3-managed Context, builds a "borrowed" Context out of it, and runs the closure using that Context in Context::thread_local.

This would ensure that no Ast or Solver associated with that Context can escape, and if existing stuff outside the propagator is needed for these callbacks, they can be moved into the closure with synchronized()/recover().

[puyral]

Amazing! It sounds like this does indeed solve most of my issues!

I'll have a try at this Weekend

[puyral]

I have adapted the work to the new RC-based Context. I also added a wrapper around the UserPropagators to be able to garbage collect them.

All looks good, but my example segfaults somewhere in z3 which doesn't seem to be related to the user propagator...

[toolCHAINZ]

I suspect this is the cause of the segfaults you're getting. impl Drop for Context frees the backing Z3_Context. But this Z3_Context was given to us, so I suspect Z3 might be freeing it as well, causing a double-free?

This is what I was referring to in my earlier comment: we probably want to structure this so that there's a "borrowed" variant of context that does not drop Z3_Context and then the challenge becomes ensuring that we properly quarantine instances of that type to places where we are sure Z3 hasn't dropped the context.

[puyral]

So the current bug is more messed up than just a double free. If I bundle with a z3 with debug enabled I get an assertion error already here which gets triggered on this line.

It doesn't seem to be a pointer problem, as z3 TRACE macro can print the term. Also requesting for the term's sort return Bool...

Commenting the register_user_propagator line out "solves" the problem, which is even more puzzling to me...

I will keep debugging this, but it might take more time than I would like..