Avoiding/Reporting capture

[LeventErkok]

This isn't really a z3/z3py issue. But rather a question of how one should design an API (like the z3py API), that stops users from doing "unsound" things. Here's an example in z3py, though I'm sure the same can be done in pretty much any high-level API, from C/C++/Java what have you. Note that I'm using RecFunction here, even though the definition isn't recursive; but that doesn't really matter:

from z3 import *

def mkAdder (i):
    foo = RecFunction('foo', IntSort(), IntSort())
    j = Int('j')
    RecAddDefinition(foo, j, i + j)
    return foo

add1 = mkAdder(1)
add2 = mkAdder(2)

s = Solver()
k = Int('k')
s.add(add1(k) == add2(k))
print(s.check())

The Python function mkAdder captures its argument i, and makes a function out of it. But it has a bug: The name it uses is foo for that function, which does not reflect this capture. So, the two calls to mkAdder actually end up creating the same function, and thus the above produces sat, contrary to what the user might've expected.

The solution in this case is easy enough. Replace:

    foo = RecFunction('foo', IntSort(), IntSort())

with

    foo = RecFunction('foo' + str(i), IntSort(), IntSort())

Hence creating a new function with each different argument. But this is brittle: The user might not be aware of this restriction, or, it might be tricky to generate a unique name if the captured arguments are not-easy-to distinguish this way with a simple call to str. Telling users "not to do that" is always an option, but the more checks the API can perform the better, especially if these API calls are done through many other layers, further complicating the debugging process.

The question/discussion I'd like to have is if there might be a Python trick to notice this capture, and at least warn the user about it, if not flat out reject such definitions. Note that capture itself isn't' a bad thing: But can we make it safer? For instance, the user should explicitly sanction: "yes I know I'm doing a capture here" by some mechanism, and otherwise gets an error message? Can we somehow mitigate this unexpected interaction between Python and the z3 level so the API is easier/safer to use by non-suspecting users?

[NikolajBjorner]

z3 only has a single definition of 'foo'. If you re-define foo one gets lost.
It could raise an exception?

[LeventErkok]

I was hoping for something that "automatically" handled this internally; but I do agree that raising an exception would be a good thing to do here.