CODEWITHSUNDEEP
z3z3py
Pushpa
Pushpa

Reputation: 458

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.

Upvotes: 1

Views: 326

Answers (1)

Nikolaj Bjorner
Nikolaj Bjorner

Reputation: 8359

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)

Upvotes: 2

Related Questions