Search code examples
z3z3py

How to check in Z3py whether the expression contains a conditional (=>)

i'm using Z3py to traverse a Boolean formula. How to check whether the formula contains a conditional. I have checked the z3.py source code and it contains is_and(), is_or(), is_not(),.. but nothing related to is_implies(). Any idea ? Thanks.

Solution

  • You can use the function "is_app_of" to determine the built-in function of an expression. Thus, 

    def is_and(a):
    return is_app_of(a, Z3_OP_AND)

    as already implemented in the z3.py file, and similarly

    def is_implies(a):
    return is_app_of(a, Z3_OP_IMPLIES)