Understanding user_propagator_base’s propagate method

[wbthomason]

I hope this isn't too stupid of a question, but: what is the meaning of the conseq parameter given to user_propagator_base's propagate method, in the C++ API? In the implementation of the conflict method, it seems to be a constant Boolean false value, but I'm not sure I understand how this is used by the solver, or what other expressions given as consequences via propagate might do.

I believe I understand how to use conflict - it can be used to provide to the solver a list of expression IDs the value of which a given variable setting (from a call to fixed or final) causes to be invalid. I'm less clear on how propagate can be used to provide a richer set of constraints for user theories. Any help/resources/etc. in understanding this would be much appreciated. Thanks!

[NikolajBjorner]

I haven't tried the user propagator with too many different scenarios. The idea with conseq argument is that you can propagate an arbitrary formula. So if you want to instantiate a quantifier yourself you could track the quantifier (forall x phi(x)), which is a Boolean, and whenever it is assigned to true have the option to generate an instance phi(t). You set conseq to phi(t) and use the identifier from the quantified formula as a premise for the propagation.
In practice there are going to be some limitations for what works with propagation. Formulas with existential quantifiers don't work with the current setup. It can be fixed, but I am not sure how important it is to change the code without having set up more thorough testing.
Another scenario that could turn out to be problematic is if you create an arithmetical formula x + y >= z + u + 1, since the current main solver assumes some normal form conversion of inequalities. This is also fixable, but I would rather take it if it becomes an issue.
The current code creates a literal from conseq so is potentially a place where it can be tuned (if it receives an equality consequence it could just propagate the equality without creating a fresh literal into the search space). The literals are temporary, though: their life-time depends on whether they participate in conflicts.

[wbthomason]

Thank you! I think the case I'm interested in is actually much simpler: I have some implications a -> b & c & !d, and I was wondering if I could, upon a being fixed, propagate the implication. From your answer, it sounds like this is feasible by e.g. giving the IDs of b, c, and d as the value of the fixed parameter to propagate, and the expression b & c & !d as the value of conseq?

[NikolajBjorner]

The better approach is to propagate b, d, !d separately.
So:

1. register a so it has an identifier. Let's call it id_a.
2. start search
3. when receiving the assignment to id_a and value true:
4. create expressions for b, c, d (and !d). For efficiency cache them for reuse.
5. add propagations id_a implies c, id_a implies b, id_a implies !d using the propagate callback with assumption [id_a] and the three consequences.

it is also legal to create b & d & !d as a single expression. It will just cause the solver to create more clauses internally.

[wbthomason]

Ah, I see, thanks!

[NikolajBjorner]

Note (for others reading this thread) also that there is a new sample

https://github.com/Z3Prover/z3/tree/master/examples/userPropagator

It offers an introductory illustration of the feature.

[wbthomason]

(For what it's worth, that example - which I found in its PR - is what got me playing around with user theory propagation, since I was surprised by the speedup gained by the example implementation using implicit constraints).

EDIT: Although I now see I missed the existence of https://github.com/Z3Prover/z3/blob/master/examples/userPropagator/example.pdf in the PR, which is helpful.