Interactions between Guidance and the tokenization

[vivien000]

Hi! I have a technical question to better understand how Guidance works. Let's imagine that we are interested in generating a string satisfying a certain constraint. Let S be the set of strings satisfying this constraint.

Are the token sequences potentially generated by Guidance exactly:

1. those that can be decoded as a string of S (ie. the preimage of S through the tokenizer's decoding function);
2. those are the image of a string of S through the tokenization
   (ie. the image of S through the tokenizer's encoding function) ?

For example, if a regex is "^[a-z]{10}$", can Guidance return:

1. any token sequence whose total number of letters is 10;
2. only those that actually correspond to the tokenization of an a-z string of length 10?

I understand the answer is 1) but I would appreciate if this can be confirmed.