[SMT-LIB] Issues with define-fun for Functions of Arity 0

[Cesare Tinelli]

Tjark,

On 21 Apr 2016, at 8:48, Tjark Weber wrote:

> According to Section 4.2.3 of the SMT-LIB Standard (version 2.5),
>
>   (define-fun f ((x1 σ1) ··· (xn σn)) σ t)
>
> with n ≥ 0 is semantically equivalent to
>
>   (declare-fun f (σ1 ··· σn) σ)
>   (assert (forall ((x1 σ1) ··· (xn σn)) (= (f x1 ··· xn) t))
>
> Here, n=0 is explicitly permitted.
>
Yes, the implicit understanding there was that the asserted formula 
reduces to (= f t) when n = 0.

> However, the grammar for terms in Section 3.6 requires that a "forall"
> binder is followed by *one or more* (cf. Section 1.1.3) sorted
> variables.
>
The forall assertion is not to be understood as a literal translation of 
define-fun but more as an explanation of its meaning.

> Moreover, there are currently numerous SMT-LIB benchmarks in
> *quantifier-free* logics that use define-fun to define functions of
> arity 0.
>
That is not an oversight. Intentionally,

  (define-fun f ((x1 σ1) ··· (xn σn)) σ t)

is not an abbreviation of

  (declare-fun f (σ1 ··· σn) σ)
  (assert (forall ((x1 σ1) ··· (xn σn)) (= (f x1 ··· xn) t))

although it has the same meaning as the two commands above when n > 0.

The rationale is that, since define-fun is essentially a macro 
definition command, supporting it does not need quantifier reasoning 
capabilities. Applications of functions introduced by it can be 
eliminated by macro expansion.

> I believe a clarification (probably by providing a special-cased
> semantics for n=0 in Section 4.2.3) might be in order.
>
That is a good idea nonetheless. Will do.

Thanks,


Cesare




> Best,
> Tjark
>
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib