Search code examples
pythonlistz3z3pyfirst-order-logic

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

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?

Solution

  • 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).

    Why comparison with strings is not a good idea

    There are several reasons for this, the most obvious ones being maintainability against typos, change of how z3 prints things in the future, etc. But more importantly, comparison against strings can fail in the following way:

    from z3 import *

MyBadFunction = Function('And', IntSort(), IntSort())
print(str(MyBadFunction(IntVal(1)).decl()) == 'And')

    If you run this, you'll see that it happily prints True, which is not what you wanted. If you use is_and instead, it'll correctly print False. So, never trust the name of anything, and always use internal constants that are defined for this very purpose.