Pythonic way to handle chained If statement

[gmCAD]

Hello,

I find myself writing multiple Z3 If statements like this a lot in my code

from z3 import *

a, b, c, d, e, f = Bools('a b c d e f')

formula = If(a, b, If(c, d, If(e, f, False)))

Is there a better way to write this chain of If statements using the Z3 API?

Thank you in advance for any advice provided.

[NikolajBjorner]

There isn't a "Cond" function from the API, but you can define your own. Maybe using infix hacking to define some convenient syntax such as a ==> b || c ==> d || e ==> f || False, depending on what python lets you overload.

[gmCAD]

Nikola,

Thank you for the suggestion.

Also, thank you for all your hard work maintaining Z3 and answering questions so many questions from the user community.

[pschanely]

Here's a quick ready-to-copy method:

>>> from z3 import *
>>> from functools import *
>>> Cond = partial(reduce, lambda e, p: If(*p, e))
>>> a, b, c, d, e, f = Bools('a b c d e f')
>>> Cond([(e, f), (c, d), (a, b)], False)
If(a, b, If(c, d, If(e, f, False)))