search

Z3Prover / z3

The Z3 Theorem Prover
Other
10.42k stars 1.47k forks source link

Recursive function syntax #5692

Closed LeventErkok closed 3 years ago

LeventErkok commented 3 years ago

I'm a little confused about why this definition is accepted by z3:

(define-fun-rec sum ((x Int)) Int
                    (ite (= x 0) 0 (+ x ((_ sum 0) (- x 1)))))

The term (_ sum 0) suggests sum is an indexed function, which isn't really true. I'd expect z3 to error-out on this input, but it accepts it happily.

For whatever it's worth, cvc4/cvc5 both reject this definition since sum is not an indexed function.

Obviously this isn't really a big deal as z3 seems to accept more than it should, but maybe it's good to reject it to be SMTLib compliant?

NikolajBjorner commented 3 years ago

I don't understand why this should be a priority to change. The parser throws away parameters to declared functions. Having it complain could trigger other support calls.

LeventErkok commented 3 years ago

Not a priority at all. Just pedantry, and wanted to make sure you're aware. Feel free to ignore.

NikolajBjorner commented 3 years ago

It looks up the symbol here:

https://github.com/Z3Prover/z3/blob/41aa7d7b60913ec17a50df8f998d2ca773070ac8/src/cmd_context/cmd_context.cpp#L1168

It has information that there are parameters, but they are ignored. Failing the "try" function if num_indices > 0 would make your example complain, but I don't see how this is a usability improvement. It will for sure reject input that isn't strictly well-formed, but then the internal representation is well formed and can be queried (from programmatic API or through solving).