Performance question: Does introducing integer variables for subexpressions affect performance?

[ThomasHaas]

Say I have a single arithmetic constraint a+b = c+d.
What are the performance characteristics between using a+b = c+d vs. using a+b = x /\ x = y /\ y = c+d in an encoding, assuming that a+b, c+d, x, and y appear nowhere else in the formula?
Is it correct to say that a+b = x /\ x = y /\ y = c+d may be harder to solve because the solver introduces 3 boolean variables in the boolean skeleton that have the potential to be assigned in conflicting ways?

[NikolajBjorner]

Generally, z3 aims to reduce number of auxiliary Booleans by rewriting during pre-processing.
Sometimes, extra Booleans can actually help to find short explanations for why some branch is infeasible.
You can tell the pre-processing rewriter to not simplify nested equalities
https://microsoft.github.io/z3guide/docs/strategies/summary#tactic-solve-eqs
by setting tacic.solve_eqs.context_solve=false

[ThomasHaas]

How does this work if the equalities are asserted in some implication?
Let's say there is a formula Cond and I assert Cond => a+b=c+d vs. Cond => (a+b = x /\ x = y /\ y = c+d).
In this case, the equalities only hold under a condition. Will the solver still try to rewrite under the condition or does the propagation/simplification of equalites only work on top-level equalities?
Alternatively, Cond => (a+b = x /\ x = y /\ y = c+d) is equisatisfiable to a+b = x /\ y = c + d /\ Cond => x=y, assuming x and y are fresh variables. Is this something the solver can detect, or is it generally smarter on my side to pull as many equalites as possible to the top-level?

You can tell the pre-processing rewriter to not simplify nested equalities
https://microsoft.github.io/z3guide/docs/strategies/summary#tactic-solve-eqs
by setting tacic.solve_eqs.context_solve=false

The docs say that context_solve is already false by default.
Unfortunately, we use a third-party interface to Z3 which doesn't allow us to change options (yet).
That's why I'm trying to figure out how careful I have to be when asserting formulas, and how I can help the solver to perform as efficiently as possible (in the general case at least).

[NikolajBjorner]

you will have to set context_solve=true to eliminate variables based on nested equalities.
Otherwise, such variables aren't going to be eliminated, or equalities are unlikely to be reorganized during pre-processing.

[ThomasHaas]

Thank you very much for the answer.