Questions about the UserPropagator API

[ThomasHaas]

I have a few questions about the usage of user propagators and how their callbacks get invoked.

Q1: Suppose I have registered two literals p and q in my user propagator and suppose the solver somehow figures out that the values of p and q are equivalent.
What are the possible callbacks that the user propagator can receive? Let me give a few scenarios:
(1) The solver first invokes the equality-callback with parameters p and q. Then the solver makes the decision p=true, triggering the fixed-callback. Will a fixed-callback also get invoked for q or is this not invoked due to the previously established equality? In other words, do I have to track equalities to get a correct picture of the current partial model or is it sufficient to track assignments alone? What about disequalities?
(2) The solver first sets p=true, invoking the fixed-callback. The solver then establishes that p==q and calls the equality-callback. Again, will a fixed-callback get invoked for q?
(3) Assuming the setting of (2) and assuming that the fixed-callback for q is not called (only equality). If the user propagator wants to enforce q==false, is he allowed to propagate a conflict in the equality-callback that establishes q==p==true? The documentation suggests that conflicts should only be raised in the fixed and final callbacks.
(4) Can the solver set p=true, then q=true, and only then invoke the equality-callback? I assume the callback is only invoked if at least one of the literals was not assigned yet.

Q2: The propagate_consequence call has essentially 3 parameters: a set fixed of fixed literals (or even arbitrary expressions?), a set eqs of equalities, and a consequence cons.
What exactly is the purpose of the eqs parameter? Are these equalities that are propagated by the user propagator or are these equalities that are a reason/premise for the consequence.
Put more formally, does the propagation correspond to And(fixed) /\ And(eqs) => cons or And(fixed) => cons /\ And(eqs)?
Also, do the equalities have to be between literals or can they be between any arbitrary expressions that were registered?

Q3: Is it possible to call propagate_consequence with an empty set of fixed literals, effectively generating an arbitrary formula given by cons? For example, suppose I find a partial assignment m to be inconsistent and raise a conflict.
Due to some symmetry in the problem, I also know that a symmetric assignment m' is going to be inconsistent and that the solver is likely going to explore it in the future. Could I somehow preemptively exclude m' by propagating something like true => not(m')?
More generally speaking, is it possible to generate arbitrary clauses, possibly unrelated to the current partial assignment, from within the user propagator?

Thanks in advance. If I have any more questions, I will add them to this discussion thread.

[NikolajBjorner]

Q1: You should only consider fixed callbacks for Booleans. The implementation will not produce equality callbacks. If the implementation changes and you get equality callbacks for Booleans they are subsumed by fixed.
Q2: When you get an equality callback it supplies two terms that are equal. These two terms are arguments to "eqs". When you get a fixed callback you get a term that is fixed. These terms are arguments to "fixed". Consequence propagation should produce satisfiability preserving of the form fixed & eqs => cons. The equalities and literals are for registered terms that are currently equal or fixed based on a callback in the current scope. Once the solver pops the scope of a fixed callback it cannot be used for propagation.
Q3: You can invoke propagate_consequence with an empty set of premises. It then produces a lemma. The lemmas should be equality preserving, so you can break symmetries too. Or you can break symmetries by controlling case splits.

[NikolajBjorner]

equality callback is for registered terms. They don't have to be uninterpreted; except for Booleans.
You don't have to propagate congruence closure in the user propagator. The theory of EUF already knows that f(x) and ~f(y) implies x != y.

You should be able to propagate consequences from within the equality callback. What is the pointer to the documentation you refer to?

[ThomasHaas]

I understand that congruence is already enforced for EUF. It was a hypothetical example.

The documentation I refer to is the comment in the API:

z3/src/api/z3_api.h

Lines 7187 to 7199 in c340233

	\brief propagate a consequence based on fixed values.
	This is a callback a client may invoke during the fixed_eh callback.
	The callback adds a propagation consequence based on the fixed values of the
	\c ids.
	The solver might discard the propagation in case it is true in the current state.
	The function returns false in this case; otw. the function returns true.
	At least one propagation in the final callback has to return true in order to
	prevent the solver from finishing.
	def_API('Z3_solver_propagate_consequence', BOOL, (_in(CONTEXT), _in(SOLVER_CALLBACK), _in(UINT), _in_array(2, AST), _in(UINT), _in_array(4, AST), _in_array(4, AST), _in(AST)))
	*/
	bool Z3_API Z3_solver_propagate_consequence(Z3_context c, Z3_solver_callback cb, unsigned num_fixed, Z3_ast const* fixed, unsigned num_eqs, Z3_ast const* eq_lhs, Z3_ast const* eq_rhs, Z3_ast conseq);

The comment mentions fixed_eh explicitly but also implies that propagation in final_eh works. No other callbacks are mentioned.

Then there is the Python example for TC, which also never propagates conflicts inside the equality callback although equalities are used for the propagation call. That made me wonder if it is even possible.

[NikolajBjorner]

4f75153

[ThomasHaas]

Thanks for the quick update :)

[ThomasHaas]

One more question about tracking of functions.

It seems the only way to get a trackable function is to use Z3_solver_propagate_declare, which declares a fresh function.
Unlike most other solver_propagate_... functions, Z3_solver_propagate_declare does not take a Z3_solver object as input.
Furthermore, registering of functions is done over the context while registering of expressions is done over the user propagator (in most bindings).
I'm wondering why there is such a difference in API here?
Wouldn't it be possible to have an API that takes an existing function declaration and tracks it?

void UserPropagator.addFunc(FuncDecl decl); // Same as UserPropagator.addExpr(Expr expr)