SMT-LIB should consider disallowing shadowed variables in define-fun(-rec)

[ajreynol]

Currently, SMT-LIB gives an unintuitive definition of how define-fun with shadowed variables should be handled, where technically this should be treated as a partial definition based on the standard.

In detail, the SMT-LIB standard page 63 states:

(define-fun f ((x1 U1) ... (xn Un)) U t)

is equivalent to

(declare-fun f (U1 ... Un) U)
(assert (forall ((x1 U1) ... (xn Un)) (= (f x1 ... xn) t)))

Now consider what happens when we have shadowed variables. Take this benchmark:

(set-logic ALL)
(define-fun P ((x Int) (x Int)) Bool (= x 0))
(assert (P 0 1))
(check-sat)

cvc5 1.1.0 and z3 4.8.10 say "unsat" for this. The command

(define-fun P ((x Int) (x Int)) Bool (= x 0))

partially defines P over the domain where its arguments are equal, as

(forall ((x Int) (x Int)) (= (P x x) (= x 0)))

is equivalent to

(forall ((x Int)) (= (P x x) (= x 0)))

meaning (P 0 1) is unconstrained.

It is recommended the standard is updated to explicitly allow variable shadowing in arguments to define-fun(-rec).

See cvc5/cvc5#11507.

[Gbury]

That is very surprising, and something I had missed when reading the standard.

For what it's worth, dolmen has what is likely not the correct interpretation, and instead uses the usual intuitive shadowing semantics for such definitions, where (define-fun P ((x Int) (x Int)) Bool (= x 0)) is semantically equivalent to (define-fun P ((_x Int) (x Int)) Bool (= x 0)) (with a warning that the first parameter is unused). This may be a problem, both for solvers that use dolmen, and for the model validation track of SMT-COMP (I'll fix dolmen asap once we have a conclusion for this issue).

If we agree that the standard indeed specifies that in such cases, we end up with the partial definition as described above, then I think indeed that we should forbid the cases where two parameters share the same name (i.e. forbid any shadowing) as suggested by @ajreynol both in 2.6 and the upcoming version 3, since this behaviour is extremely un-intuitive, and likely to not be implemented correctly. (I briefly considered just changing the semantics to the intuitive shadowing one, but such a change would likely break too many things ?)

[Gbury]

The next release of Dolmen will reject any problem where a function definition parameter shadows another parameter of the same definition (even though it's technically allowed by the spec).

When (If ?) there are discussions about this (and maybe one day a decision/solution ?), i'd be happy to participate.