How to encode the anagram relation?

[lquesada1975]

Dear all,
I am new to z3. I wonder what is the recommended way of encoding the anagram relation (between a string variable and a string value) . Please have a look at my naive attempt below and let me know whether I can do better.
Thank you very much in advance!
Cheers,
Luis

[lquesada1975]

from z3 import *

# Post constraint that S is an anagram of Sval (S is a Z3 String variable, Sval is a Python string)
def anagram(S, Sval):
    n = len(Sval)
    S_chars = [String(f"{S}_char_{i}") for i in range(n)]
    constraints = []
    # Each S_chars[i] is a string of length 1
    for ch in S_chars:
        constraints.append(Length(ch) == 1)
    # Constrain S to be the concatenation of S_chars
    constraints.append(S == Concat(*S_chars))
    constraints.append(Length(S) == n)
    # Ensure the multiset of characters matches Sval
    from collections import Counter
    freq = Counter(Sval)
    allowed = list(freq.keys())
    for ch in S_chars:
        constraints.append(Or([ch == StringVal(c) for c in allowed]))
    for c, f in freq.items():
        constraints.append(Sum([If(S_chars[i] == StringVal(c), 1, 0) for i in range(n)]) == f)
    return constraints

# z3_anagram_of now uses anagram(S, Sval)
def z3_anagram_of(S_name, Sval):
    S = String(S_name)
    solver = Solver()
    constraints = anagram(S, Sval)
    for c in constraints:
        solver.add(c)
    return solver, S

# Example usage:
Sval = "1x2x3x4x5"
solver, S = z3_anagram_of("S", Sval)

if solver.check() == sat:
    model = solver.model()
    print("Anagram of", Sval, ":", model.eval(S))
else:
    print("No solution")