Issues with define-fun for functions with arity 0

[davidcok]

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.

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.

Moreover, there are currently numerous SMT-LIB benchmarks in
quantifier-free logics that use define-fun to define functions of
arity 0.

I believe a clarification (probably by providing a special-cased
semantics for n=0 in Section 4.2.3) might be in order.

Best,
Tjark

---

SMT-LIB mailing list
[email protected]
http://www.cs.nyu.edu/mailman/listinfo/smt-lib