How To Model In Z3py

I have a total of seven (A, B, C, D, E, r, c) Z3 Boolean variables, where A, B, C, D, E represent the edges from a point, represented as a black dot in the following Fig.1. The r

Solution 1:

Your description is a bit hard to follow, but you should be able to express these almost literally as follows. (I added some inline comments so you can follow the coding logic and modify as appropriate.)

from z3 import *

A, B, C, D, E, r, c = Bools('A B C D E r c')

s = Solver()

# Case 1
Case1 = Implies(A, Xor(C,D))
s.add(Case1)

# Case 2
Case2 = Implies(B, Xor(C,D))
s.add(Case2)

# Conditions for r. Your description is a bit confusing here,# as it says both `r` is true, and if one of Case1 or Case2# is true. This suggests one of Case1 or Case2 must be true,# though it's not clear to me why described it in this complex# way. Modify accordingly.
s.add(r)
s.add(Or(Case1, Case2))

# Case 3: if A and C are True then c will be true if both E and D are true
s.add(Implies(And(A, C), Implies(And(E, D), c)))

# Case 4: if A and D are True then c will be true if both E and C are true
s.add(Implies(And(A, D), Implies(And(E, C), c)))

# Case 5: if B and C are True then c will be true if both E and D are true
s.add(Implies(And(B, C), Implies(And(E, D), c)))

# Case 6: if B and D are True then c will be true if both E and C are true
s.add(Implies(And(B, D), Implies(And(E, C), c)))

vars = [A, B, C, D, E, r, c]
while s.check() == sat:
    m = s.model()
    for v invars:
      print("%s = %5s" % (v, m.evaluate(v, model_completion = True))),
    print
    s.add(Or([p != v for p, v in [(v, m.evaluate(v, model_completion = True)) for v invars]]))

When run, this prints:

A = False B = False C = False D = False E = False r =  True c = FalseA = False B = False C =  True D = False E = False r =  True c = FalseA = False B = False C =  True D =  True E = False r =  True c = FalseA = False B = False C = False D =  True E = False r =  True c =  TrueA = False B = False C =  True D = False E = False r =  True c =  TrueA = False B = False C =  True D =  True E = False r =  True c =  TrueA = False B =  True C = False D =  True E = False r =  True c =  TrueA = False B =  True C =  True D = False E = False r =  True c = FalseA = False B =  True C =  True D = False E = False r =  True c =  TrueA =  True B =  True C =  True D = False E = False r =  True c =  TrueA =  True B = False C =  True D = False E =  True r =  True c =  TrueA = False B =  True C =  True D = False E =  True r =  True c =  TrueA =  True B =  True C =  True D = False E =  True r =  True c = FalseA =  True B =  True C =  True D = False E =  True r =  True c =  TrueA = False B =  True C = False D =  True E =  True r =  True c =  TrueA = False B =  True C =  True D = False E =  True r =  True c = FalseA = False B = False C =  True D = False E =  True r =  True c = FalseA = False B = False C =  True D =  True E =  True r =  True c = FalseA = False B = False C = False D =  True E = False r =  True c = FalseA = False B = False C = False D =  True E =  True r =  True c = FalseA = False B = False C = False D = False E =  True r =  True c = FalseA = False B = False C = False D = False E =  True r =  True c =  TrueA = False B = False C = False D = False E = False r =  True c =  TrueA = False B = False C = False D =  True E =  True r =  True c =  TrueA =  True B = False C = False D =  True E =  True r =  True c =  TrueA =  True B = False C = False D =  True E =  True r =  True c = FalseA =  True B =  True C = False D =  True E = False r =  True c = FalseA =  True B =  True C = False D =  True E =  True r =  True c = FalseA = False B =  True C = False D =  True E = False r =  True c = FalseA =  True B =  True C = False D =  True E = False r =  True c =  TrueA =  True B = False C = False D =  True E = False r =  True c =  TrueA =  True B = False C =  True D = False E = False r =  True c =  TrueA =  True B = False C =  True D = False E = False r =  True c = FalseA =  True B = False C = False D =  True E = False r =  True c = FalseA = False B =  True C = False D =  True E =  True r =  True c = FalseA = False B = False C =  True D =  True E =  True r =  True c =  TrueA = False B = False C =  True D = False E =  True r =  True c =  TrueA =  True B =  True C =  True D = False E = False r =  True c = FalseA =  True B = False C =  True D = False E =  True r =  True c = FalseA =  True B =  True C = False D =  True E =  True r =  True c =  True

This prints all possible models. You can of course constrain it further.