2

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?

JRR
  • 6,014
  • 6
  • 39
  • 59

1 Answers1

1

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.

alias
  • 28,120
  • 2
  • 23
  • 40
  • 1
    A decent mental model for `define-fun` is "the solver will apply eager beta reduction", and `define-fun-rec` is roughly "the solver will introduce universal quantifiers + an uninterpreted functions". This is not necessarily true of the implementation, but it should get you a decent ways. – Tim Dec 26 '18 at 18:45