In an answer to this question, Leo suggested to use quantifiers to define functions. Suppose I only need to apply the function only 1 time, does using quantifier affects the performance of Z3?
How it compares to the case where I declare a function without parameters and without the quantifiers (since I only use the function only 1 time)?
You can try to use the option smt.macro_finder=true to convert quantified equalities into macros. It is off by default, so it is better to define macros for the functions that you only apply once. It also means that Z3 ends up using the general quantifier based solver. In some cases functions defined by macros, using the "define-fun" commands, are handy for formulas that are purely bit-vector or purely linear arithmetic. In these cases, Z3 uses more efficient settings. For example, Z3 uses "relevancy" propagation to avoid superfluous quantifier instantiation. relevancy propagation comes with its own overhead, which is tolerable with quantified formulas, but not a good idea for quantifier-free formulas.
