User Propagator: Register fixed only when value is True

[lukerooney7]

I am implementing a User Propagator and am following Boolean values which I only want to implement logic in fixed when this value is set to True. Since there are so many checks currently it is expensive to call it when it is false and to implement the boolean check at the start of the function.

is_true and is_false take ~40% of the total time of the solving.

Is there a way to register fixed

Thank you :)

[ThomasHaas]

Is your user propagator implemented in C++? If so, I don't think letting Z3 internally check the value vs. your function checking the value is any different. You would only save a function call which should not be a big deal.
If you use other languages, e.g. Python or Java, I can see that there is more overhead.

Since there are so many checks currently it is expensive to call it when it is false and to implement the boolean check at the start of the function.

I don't understand this part. The amount of checks in your function is irrelevant if you immediately return on false values, no?

[NikolajBjorner]

I added a short cut in python API for speeding up is_true/is_false.
Though, you can also create a constant

true_val = BoolVal(True)
false_val = BoolVal(False)

Then compare value == true_val, which uses fewer Python object creations.