Python-Z3: How can I access the elements of an And-CodePudding

I can represent conjunction using a list. For instance, let

x_1 = Int('x_1')
the_list = [Not(500 <= x_1), Not(x_1 <= 500), Not(x_1 <= 300)]

phi_1 = And(the_list)

(i.e. phi_1 = And([Not(500 <= x_1), Not(x_1 <= 500), Not(x_1 <= 300)]))

Then, I can perform the_list[0] and get Not(500 <= x_1).

However, imagine I have been given the conjunction without the list:

phi_2 = And(Not(500 <= x_1), Not(x_1 <= 500), Not(x_1 <= 300))

How can I access the elements of an And as if it was a list?

CodePudding user response：

Use decl and arg calls:

from z3 import *

x_1 = Int('x_1')

phi_2 = And(Not(500 <= x_1), Not(x_1 <= 500), Not(x_1 <= 300))

print(phi_2.decl())
for i in range(phi_2.num_args()):
   print(phi_2.arg(i))

This prints:

And
Not(x_1 >= 500)
Not(x_1 <= 500)
Not(x_1 <= 300)

decl returns the function that you're applying, and arg gets the respective children. Note how z3 internally rearranged your expressions; it tends to put variables on one side and constants on the other in comparisons, without changing the meaning.

Note that the above would fail if you applied it to an expression that wasn't an application. There are also predicates to recognize what sort of a node you're dealing with, but they're more suitable for advanced/internal uses.(is_app is the most obvious one, returning true if the expression is an application of a function to arguments.)

Checking if an application is AND

If you're given an expression and want to find out if it's an application of And, use the is_and function:

print(is_and(phi_2))

prints True for the above definition of phi_2. See https://z3prover.github.io/api/html/namespacez3py.html#a29dab09fc48e1eaa661cc9366194cb29 for documentation. There are recognizers for many of the constructors you might need. And if any is missing, look at the definition of is_and itself in the linked documentation to find out the robust way of adding new ones. (i.e., by comparing to the official enumeration of all operations, as given by: https://z3prover.github.io/api/html/group__capi.html#ga1fe4399e5468621e2a799a680c6667cd).