Get list of the available high-level variables in Z3 formula

I wonder if we can get a list of the higher-order free variables in the Z3 formula as they were declared while making the formula.

For example, in the following code:

P1 = Bool('P1')
x, y = Ints('x y')
A1 = (x + y > 1)
A2 = (x <= 0)

f = And(Implies(P1, A1), Implies(Not(P1), A2))

Is there a way, to get {P1, A1, A2} from f? Using this answer, I can get {x, y, P1} which are not the higher order. Because in my later parts of the code, I want to get models for And(f, Not(A1)) etc.

Solution

The term "high-level variable" isn't common terminology. In any case, A1, A2 etc. are Python variables, and z3 has no knowledge of them. So, there's no way of accessing them as "variables" later on. One way to think of them is that they entirely live on the Python side of things, and they never make it to z3 in any way.

The usual way to handle this sort of a problem is to give names to which ever expression you need to refer to later on. Like this:

from z3 import *

s = Solver()

P1 = Bool('P1')
x, y = Ints('x y')

A1, A2, f = Bools('A1 A2 f')

# instead of equality at Python level
# declare these expressions equal in Z3
s.add(A1 == (x+y > 1))
s.add(A2 == (x <= 0))
s.add(f, And(Implies(P1, A1), Implies(Not(P1), A2)))

if s.check() == sat:
    m = s.model()
    print("And(f, Not(A1)): ", m.evaluate(And(f, Not(A1))))

This prints:

And(f, Not(A1)):  False