XOR with Z3 Python API - only returns a single solution

I am testing a single XOR statement using the Python API for Z3.

This is the output I get:

[B_L = True, A_L = False, C_L = False]

However, I should have 3 solutions, where two of the variables are false and the last is true. Where do I go wrong?

from z3 import *

A_L = Bool('A_L')
A_M = Bool('A_M')
A_R = Bool('A_R')

B_L = Bool('B_L')
B_M = Bool('B_M')
B_R = Bool('B_R')

C_L = Bool('C_L')
C_M = Bool('C_M')
C_R = Bool('C_R')

def OnlyA(a,b,c):
    return And(a,Not(b),Not(c))

def XOR(a,b,c):
    return Or(OnlyA(a,b,c),OnlyA(b,c,a),OnlyA(c,b,a))

s = Solver()

s.add(XOR(A_L,B_L,C_L))

if s.check() == sat:
    m = s.model()
    print(m)
else:
    print("invalid installation profile")

Solution

You are just getting the first of three solutions.
The reason is, that your code does not look for alternative ones.

As explained in this post, you are supposed to add constraints blocking the previous solutions.
Then, re-run the Solver to obtain additional solutions.

from z3 import *

A_L = Bool('A_L')
A_M = Bool('A_M')
A_R = Bool('A_R')

B_L = Bool('B_L')
B_M = Bool('B_M')
B_R = Bool('B_R')

C_L = Bool('C_L')
C_M = Bool('C_M')
C_R = Bool('C_R')

def OnlyA(a,b,c):
    return And(a,Not(b),Not(c))

def XOR(a,b,c):
    return Or(OnlyA(a,b,c),OnlyA(b,c,a),OnlyA(c,b,a))

#  https://brandonrozek.com/blog/obtaining-multiple-solutions-z3/
def get_solutions(s: z3.z3.Solver):
    result = s.check()
    # While we still get solutions
    while (result == z3.sat):
      m = s.model()
      yield m
      # Add new solution as a constraint
      block = []
      for var in m:
          block.append(var() != m[var])
      s.add(z3.Or(block))
      # Look for new solution
      result = s.check()

s = Solver()

s.add(XOR(A_L,B_L,C_L))

solutions = get_solutions(s)
upper_bound = 10
for solution, _ in zip(solutions, range(upper_bound)):
    print(solution)

There are in fact more elaborate and more efficient ways to get multiple solutions. These are described here.