Python: specifying "decide" in user propagator

[jordicollcaballero]

Hello,

we are trying to track "decide" events in a user propagator using the Python API. We have succeeded in defining "fixed" and "final" functions. However, we get an error when defining a "decide" funcion:

self.add_fixed(lambda x, v: self._fixed(x, v))
self.add_decide(lambda x, v: self._decide(x, v))
self.add_final(lambda: self._final())

This makes an assertion faied, which we can fix if we add in __init__ in our custom propagator the code:

self.decide = None 

However, after doing this, we still get an error, apparently coming from user_prop_decide in z3.py, where variable t_ref is undefined:

def user_prop_decide(ctx, cb, t, idx, phase):
    prop = _prop_closures.get(ctx)
    old_cb = prop.cb
    prop.cb = cb
    t = _to_expr_ref(to_Ast(t_ref), prop.ctx())
    prop.decide(t, idx, phase)
    prop.cb = old_cb

Moreover, could you please specify (or point us to the documentation) what are the parameters expected in "decide"?

[NikolajBjorner]

You are the first one to try out the decide callback from Python. It isn't fully implemented as you can see.
The function takes in-out parameters which makes it a bit cumbersome to encode.
The documentation is in z3_api.h, the C header file.

[JoanEspasa]

Thanks Nikolaj for your input. I understand then that we should already be able to implement it when implementing the propagator in C, and we should wait for the finished implementation in Python?

Thanks for all the hard work!

[NikolajBjorner]

we should wait for the finished implementation in Python?
Z3 is open source. You can implement it and add a pull request.
I don't have too much spare bandwidth.

[JoanEspasa]

We independently came to the same fix that @linusheck proposed and merged here: #7451
Thanks again everyone