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

Question

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.

alias · Accepted Answer · 2023-01-11T21:47:53.040

1

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

edited Jan 11 '23 at 21:47

answered Dec 21 '22 at 16:48

alias

28,120
2
23
40

1

NB: `s.add(A1 == x+y > 1)` and `s.add(A2 == x <= 0)` might not work well unless an extra parenthesis is added, i.e., `s.add(A2 == (x <= 0))` – foobar Jan 11 '23 at 10:40
Thank you for the idea about attaching expressions with Boolean variables. However, is there a way to get `{A1, A2, P1}` (which are Boolean variables) from `s`. Or I manually make a separate set of them and use them in later code, i.e., `my_vars = {A1, A2, P1}` and then later something like: `for var in my_vars: m.evaluate(And(f, Not(var)))` – foobar Jan 11 '23 at 10:46
1

Make a separate set. There’s no way to get those variables unless you start doing some Python meta programming; which has nothing to do with z3. – alias Jan 11 '23 at 14:24
1

You're right about the parentheses. Indeed they need to be present to avoid any operator-precedence/parsing snafus. I've updated the answer. Good catch! – alias Jan 11 '23 at 21:50

score 0 · Answer 2 · answered Dec 21 '22 at 17:02

You could recursively traverse your expression tree to collect the intermediate expressions above leaf level:

def show_expression(e, margin=""):
    nc = len(e.children())
    print(f"{margin}decl {e.decl()} has {nc} children: {e}")
    dMax = 0
    for ic in range(nc):
        d = show_expression(e.children()[ic], margin + "  ")
        dMax = d if d > dMax else dMax
    dMax += 1
    if dMax > 1:
        #  higher order
        print(f"{margin}dMax = {dMax}")
    return dMax

Result for your example:

decl And has 2 children: And(Implies(P1, x + y > 1), Implies(Not(P1), x <= 0))
  decl Implies has 2 children: Implies(P1, x + y > 1)
    decl P1 has 0 children: P1
    decl > has 2 children: x + y > 1
      decl + has 2 children: x + y
        decl x has 0 children: x
        decl y has 0 children: y
      dMax = 2
      decl Int has 0 children: 1
    dMax = 3
  dMax = 4
  decl Implies has 2 children: Implies(Not(P1), x <= 0)
    decl Not has 1 children: Not(P1)
      decl P1 has 0 children: P1
    dMax = 2
    decl <= has 2 children: x <= 0
      decl x has 0 children: x
      decl Int has 0 children: 0
    dMax = 2
  dMax = 3
dMax = 5

If the depth below an intermediate expression is above 1, you could store it for your later evaluation or experiments.

What does this have to do with `A1`/`A2` etc? The point is to be able to refer to `A1` as a variable, these are lost when translated through the z3py API. I don't see how your solution gives access to them as the original-poster seemingly wants to do. The point isn't about recovering expressions (which will be very expensive in general anyhow), but rather referring to expressions as they appeared in the original Python program. — alias, Dec 21 '22 at 17:08

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

2 Answers2