40 lines
865 B
Python
40 lines
865 B
Python
from z3 import *
|
|
|
|
p0 = Bool('p0')
|
|
p1 = Bool('p1')
|
|
p2 = Bool('p2')
|
|
p3 = Bool('p3')
|
|
p4 = Bool('p4')
|
|
|
|
p0e = Bool('p0e')
|
|
p1e = Bool('p1e')
|
|
p2e = Bool('p2e')
|
|
p3e = Bool('p3e')
|
|
p4e = Bool('p4e')
|
|
|
|
p0p = Bool('p0p')
|
|
p1p = Bool('p1p')
|
|
p2p = Bool('p2p')
|
|
p3p = Bool('p3p')
|
|
p4p = Bool('p4p')
|
|
|
|
Cd_a1 = And( Or(p1,p1e), Or(p4,p4e), Not( Or(p2,p2e) ) )
|
|
Cd_a2 = And( Or(p2,p2e), Not( Or(p3,p3e) ) )
|
|
Cd_a3 = And( Or(p1,p1e), Or(p3,p3e), Not( Or(p2,p2e) ) )
|
|
Cd_a4 = And( Or(p3,p3e), Not( Or(p2,p2e) ) )
|
|
|
|
En1 = Or(Cd_a1,Cd_a2,Cd_a3,Cd_a4)
|
|
En2 = Or(Cd_a1,Cd_a3)
|
|
En3 = Cd_a2
|
|
En4 = Cd_a2
|
|
|
|
Pr1 = Or( And(En1,p1p) , And( Not(En1), Not(p1p)) )
|
|
Pr2 = Or( And(En2,p2p) , And( Not(En2), Not(p2p)) )
|
|
Pr3 = Or( And(En3,p3p) , And( Not(En3), Not(p3p)) )
|
|
Pr4 = Or( And(En4,p4p) , And( Not(En4), Not(p4p)) )
|
|
|
|
PrConjunction = And( Pr1, Pr2, Pr3, Pr4 )
|
|
|
|
print PrConjunction
|
|
|