pythonz3smtz3pysat

z3 python change logic gate children


My algorithm needs to modify the children() of the existing logic gate. Suppose i have the following code

a = Bool('a')
b = Bool('b')
c = Bool('c')
or_gate = Or(a, b)

I want to modify or_gate to be Or(a, c).

I have tried the following:

or_gate.children()[1] = c
print(or_gate)

The above code doesn't work, or_gate is still Or(a, b). So how do i change the children of a logic gate in z3?
Edit: i can't create new Or() that contains the children i want due to nested gate. For example consider the following

a = Bool('a')
b = Bool('b')
c = Bool('c')
d = Bool('d')
e = Bool('e')
or_gate_one = Or(a, b)
or_gate_two = Or(or_gate_one, c)
or_gate_three = Or(or_gate_two, d)

If we create new object instead of directly modifying the children of or_gate_one, then or_gate_two and or_gate_three should also be modified, which is horrible for large scale. I need to modify the children of or_gate_one directly.


Solution

  • Use the substitute method:

    from z3 import *
    
    a = Bool('a')
    b = Bool('b')
    c = Bool('c')
    
    or_gate = Or(a, b)
    print(or_gate)
    
    or_gate_c = substitute(or_gate, *[(a, c)])
    print(or_gate_c)
    

    This prints:

    Or(a, b)
    Or(c, b)
    

    I wouldn't worry about efficiency, unless you observe it to be a problem down the road: (1) z3 will "share" the internal AST when you use substitute as much as it can, and (2) in most z3 programming, run-time is dominated by solving the constraints, not building them.

    If you find that building the constraints is very costly, then you should switch to the lower-level APIs (i.e., C/C++), instead of using Python so you can avoid the extra-level of interpretation in between. But again, only do this if you have run-time evidence that building is the bottleneck, not the solving. (Because in the common case of the latter, switching to C/C++ isn't going to save you much anyhow.)