CODEWITHSUNDEEP
z3smtcvc4
JRR
JRR

Reputation: 6152

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?

Upvotes: 2

Views: 407

Answers (1)

alias
alias

Reputation: 30438

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.

Upvotes: 1

Related Questions