What do the arguments to the user propagator callbacks represent?

[bakkot]

I'm looking at updating the JS bindings for the user propagator, as discussed here.

I figured I'd start by re-implementing the n-queens example in pure C, without the C++ API; then I can confirm that the equivalent using the JS bindings works. But I'm having a hard time following the logic.

I see that, for example, the Z3_fixed_eh callback type take a Z3_solver_callback as its second parameter. But what is it? The comment for Z3_solver_propagate_fixed isn't helpful; it just says that it "registers a callback", but does not say what the arguments to the callback represent.

Also, what is the fresh argument to Z3_solver_propagate_init for? All the n-queens example has to say is "The function fresh is not really interesting for our purpose but we nonetheless have to implement it."

[bakkot]

Also I can't entirely tell what the id argument is for. From the n-queens example, I see here via here that it is an identifier returned by either Z3_solver_propagate_register_cb or Z3_solver_propagate_register; the user is presumably expected to store these ids when calling Z3_solver_propagate_register so they know how to interpret the id argument to the callbacks. But why is this indirection necessary? Couldn't the callbacks just be provided with the original Z3_ast passed to Z3_solver_propagate_register, instead of id representing that call?

[NikolajBjorner]

/**
   \brief register a user-properator with the solver.

   \param c - context.
   \param s - solver object.
   \param user_context - a context used to maintain state for callbacks.
   \param push_eh - a callback invoked when scopes are pushed
   \param pop_eh - a callback invoked when scopes are poped
   \param fresh_eh - a solver may spawn new solvers internally. This callback is used to produce a fresh user_context to be associated with fresh solvers. 
 */

[NikolajBjorner]

/**
   \brief register a callback on final check.
   This provides freedom to the propagator to delay actions or implement a branch-and bound solver.
   The final check is invoked when all decision variables have been assigned by the solver.

   The \c final_eh callback takes as argument the original user_context that was used
   when calling \c Z3_solver_propagate_init, and it takes a callback context with the
   opaque type \c Z3_solver_callback. 
   The callback context is passed as argument to invoke the \c Z3_solver_propagate_consequence function.
   The callback context can only be accessed (for propagation and for dynamically registering expressions) within a callback. 
   If the callback context gets used for propagation or conflicts, those propagations take effect and
   may trigger new decision variables to be set.
 */
void Z3_API Z3_solver_propagate_final(Z3_context c, Z3_solver s, Z3_final_eh final_eh);

[NikolajBjorner]

Couldn't the callbacks just be provided with the original Z3_ast passed to Z3_solver_propagate_register, instead of id representing that call?

Yes, it is roundabout and could be a usability mistake. The Ids expose some internal way to ensure an address space for registered expressions.

[NikolajBjorner]

Overall, the user propagator is "fresh". Clemens Eisenhofer is developing a full use case for Alive2 and working out kinks while validating what API functions are relevant. I have used the Python version for more than a year in a separate project. The Python bindings are not simple, though. Storing native pointers is roundabout.

[NikolajBjorner]

I am going to change the API and remove the indirection with ids.
See the propagator branch. https://github.com/z3prover/z3/tree/propagator

[bakkot]

That does seem nicer.

How does that interact with reference counting for AST nodes? Will it automatically increment the counter while it is holding on to the node? Or is it not guaranteed to be the same literal node as you registered, just structurally equal to it?

[NikolajBjorner]

It should have ownership of the ast node when you register it (so owns a reference count).

[bakkot]

Makes sense.

Also it looks like your branch doesn't update the n-queens example yet. Probably worth doing that simultaneously, both so that the example is correct for people (like me) who are using it as a reference and to confirm the changes make sense for that project.

The PDF in that directory will become slightly wrong with these changes, but not in a way which affects understanding, I think.

[NikolajBjorner]

I am asking @CEisenhofer to update the example