Issues with define-fun for functions with arity 0 #7
Description
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