Search code examples
z3z3py

multiple constraints in z3py if conditional

Let us assume we have 2 functions (funcA and funcB) that builds some constraints in Z3's current context.

I want to guard those in a Z3 if block. In z3py, you would write:

t = If(some_condition, funcA(), funcB())

This is dependent on the fact that funcA and funcB return some z3 expression. What if I want to represent them as a function call that builds a bunch of constraints rather than returning an expression, what would be a simpler way to do that?

Solution

  • I'd turn them into (pseduo-code):

    for c in funcA():
   s.add(Implies(some_condition, c))

for c in funcB():
   s.add(Implies(Not(some_condition), c))