Search code examples
pythonz3z3py

If clause in Z3py without the else


How do we write an If('condition', x, y) clause in Z3py if we don't have the 'else' part ?


Solution

  • All expressions in z3 produce a value; think of it like a functional programming language as opposed to an imperative one. So, you have to provide the else clause.

    This sort of thing usually comes up when modeling imperative languages in z3; something like:

    foo = expr1
    if cond:
       foo = expr2
    

    The proper way to model this is to use the so called SSA form, and "keep" the old value, i.e., the above becomes:

    foo0 = expr1
    foo1 = If(cond, expr2, foo0)
    

    Note that each assignment to the "same" variable gets a new name (foo0, foo1, etc.), and when a value doesn't change through a conditional, we just keep its old value. Most of the symbolic-simulation systems (like Klee, or other higher-level APIs) do this under the hood for you. Note that coming up with the correct assignment, while it can be automated, can be tricky, depending on the type of foo. (What if it's a list?)

    To address your programming needs, it's always best to ask specific instances where you needed this construct; otherwise the answers will necessarily be generalizations. That is, while the above is the general strategy, your particular problem might have an easier solution. But it's impossible to know without further details of exactly what you're trying to achieve.