z3 - Assert the # of elements with value x == # of elements with value y?

Question

I have some string constants in z3, e.g.

boxes = [String(x) for x in range(10)]

# Valid values are x or y
for box in boxes:
    s.add(Or([box == val for val in 'xy']))

How would I add the constraint that the number of strings that equal "x" == the number of strings that equal "y"?

Answer 1

Try:

from z3 import *

s = Solver()

boxes = [String("s" + str(x)) for x in range(10)]

# Make sure each box is either x or y
for box in boxes:
    s.add(Or(box == StringVal("x"), box == StringVal("y")))

# Count x's and y's
xcount = 0
ycount = 0
for box in boxes:
    xcount += If(box == StringVal("x"), 1, 0)
    ycount += If(box == StringVal("y"), 1, 0)

# Assert the number of x's equal y's
s.add(xcount == ycount)

# Get a model:
if s.check() == sat:
    print (s.model())
else:
    print("No solution")

This prints:

[s9 = "x",
 s3 = "x",
 s6 = "y",
 s2 = "y",
 s5 = "y",
 s7 = "y",
 s4 = "x",
 s1 = "x",
 s0 = "x",
 s8 = "y"]