z3 - 断言值为 x 的元素数量 == 值为 y 的元素数量？

Question

我在 z3 中有一些字符串常量，例如

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']))

如何添加等于“x”的字符串数 == 等于“y”的字符串数的约束？