z3smtcvc4

define-fun vs define-funs-rec in smtlib


It seems that define-funs-rec is a strict superset of what define-fun can do according to the SMTLIB standard. If so is there a reason for not always using define-funs-rec, maybe except for syntactic simplicity?


Solution

  • Strictly speaking; no. But define-fun-rec is rather new (as opposed to good old define-fun), so if you want greater portability and have no need for a recursive definition, then you should stick to define-fun.

    It is conceivable that the define-fun-rec might also bring heavier-machinery in a solver that is not really needed unless you really have a recursive definition, such as a well-foundedness checker. This might end up costing some performance cycles; though I doubt this would be too much of a concern.