Problem should enforce bracket nesting in variable names

[ciaranm]

Problem::check_name should check that if any square brackets appear in a name, then they form a valid nesting.

[philrod1]

Do you have some examples?
Regex can do a single matching pair of square brackets easy enough:
static const regex allowed{R"(_*[a-zA-Z][a-zA-Z0-9_\-]*(\[[a-zA-Z0-9_\-]+\])?)"};
which will accept things like my_name[10].
To accept nested square brackets such as x[y[z[1]]], something more than regex will be needed. So my question now is, if x[y[z[1]]] is to be accepted as a valid variable name, should y[z[1]] and z[1] also be accepted? Do they also need to be inserted into the list of names? If so, we could call Problem::check_name recursively.

[ciaranm]

Names like x[y[1]] and a{b[c{d}]} should be accepted, but the inner parts don't need to be inserted into the list of names: the square brackets are just strings we use to make the proofs easier for humans to read. So, I think this is doable just with a stack of delimiter characters, where currently [] and {} are the only valid delimiter pairs.

[philrod1]

I have been looking at various README files for GCS and VeriPB and I came across this:

Variable names (at least two characters) have been restricted further. The first character must be an ASCII letter or an underscore. The remaining characters must be ASCII letters, digits, underscores (_), curly brackets ({}), square brackets ([]) and caret (^) are still allowed.

There is no mention of hyphens, which the regex allows. The regex does not allow carets, but the line from migration_guide.md says VeriPB allows them.

[ciaranm]

I am not inclined to allow caret. It might come in handy for our own internal purposes at some point.

I think hyphens are a recent ban. We might want to think about this, because users might actually want to use them. (Are they allowed in MiniZinc and / or XCSP? I don't think so?) One option would be to allow hyphens, but to write them out as ^_ to the proof files.