latest improvements broke fresh when we have concurrent calls with the same names:

conj(
    fresh(lambda x: eq(x, 'hello')),
    fresh(lambda x: eq(x, 'bye')),
)

The two lambdas should create distinct variables so we should end up with two substitutions with the first x == 'hello', second x == 'bye'

As it stands, terms are given unique numeric values to avoid collisions, but this makes parsing the results a bit difficult since we have to reverse-engineer which fresh was called first.

We can use pythons inspect module to pull out the parameter names from the functions passed to fresh.

This pr still appends the counter to the names to ensure we keep each term fresh, but we could be smarter to avoid appending a counter if this is the first time we've seen a name.

I also modified fresh to allow for multiple new terms introduced at once

Example:

disj(
    fresh (lambda x: conj(
        eq(x,0), 
        eq(x,1))), 
    fresh(lambda x: eq(x,2)))({})

Expected behaviour: we should get a result of {x2: 2}

Instead, we get {x: 2}. The way fresh currently works, there would be no valid solutions coming out of the first conj so it wouldn't know about any of the xs. I think we have to keep a running list of variables the whole way through like in the original paper, but maybe a set of names instead of the counter they use. We could also be clever and use a collections.Counter to save the lookup time?