Make the organization of the issue tests uniform

[hra687261]

Some where following the shape issue_number.(ae|smt2|expected), /dolmen/(...)
While other were following the shape issue_number/(testfile|issue_number).(ae|smt2|expected), issue_number/dolmen/(...)
No there are only two sub-folder under issues: dolmen and model

[bclement-ocp]

I agree that having a uniform layout would be good, but I am not sure this is what we want to settle on. What is your reasoning for preferring this layout? Here are some thoughts I have:

• Having a uniform way of separating issues is good. Now the issues related to dolmen are separated from the issues related to models and from the issues that don't deal with any of them. It reduces cognitive load if we want to revisit a specific issue.
• Sometimes we want multiple files for the same issue (often that is a .ae and a .smt2 file, which require two distinct names), and having a one-to-one mapping from issues to files discourages that.
• On the other hand, it is slightly more convenient to work with tests/issues/404.ae than tests/issues/404/testfile.ae, but actually not that much

Actually, now that I think about it explicitly, i kind of like the actual system:

• For simple cases, use XXX.ae or `XXX.smt2, it is enough.
• For complex cases where multiple files are needed, make a XXX directory to store the multiple files you need

Only the case of dolmen/models files remain, and maybe this is where we messed up by tying the features in gentest to directories rather than files, which bloats the trees. But we could allow XXX_models.ae and XXX_dolmen.ae instead, and keep a flatter hierarchy.

(Not that I feel very strongly either way, but if we want to actually enforce something here rather than let it happen organically, we should probably spend some time thinking about what we want to enforce)

[hra687261]

often that is a .ae and a .smt2 file, which require two distinct names

Not necessarily, could be the same name if the expected output is the same, aka when there is only one goal in the file.

Actually, now that I think about it explicitly, i kind of like the actual system:

That's not the current system. (eg 340, 460, 479).

I don't have strong opinions on the subject either, what I care about is uniformity, a middle ground would be:

• Simple test cases under tests/issues
• Simple dolmen, model test cases under tests/issues/dolmen, tests/issues/model
• complex test cases (More than 1 file) under tests/issues/issue_number

Although we don't have any AFAIK, files that need to be both under model and dolmen (is that even supported?). They can either be under tests/issues/dolmen/model or be considered as complex test cases and be under tests/issues/issue_number/dolmen/model.

Another thing that can be done is consider all special cases dolmen, model, both or more than one file, as complex tests cases that need to be in their own folder, that's a lot more folders, but again, I only care about uniformity, so I let you decide.

[bclement-ocp]

often that is a .ae and a .smt2 file, which require two distinct names

Not necessarily, could be the same name if the expected output is the same, aka when there is only one goal in the file.

Does that actually work? I think I had issues running gentest when I tried to do this, but I may be misremembering.

That's not the current system. (eg 340, 460, 479).

Fair :)

Another thing that can be done is consider all special cases dolmen, model, both or more than one file, as complex tests cases that need to be in their own folder, that's a lot more folders, but again, I only care about uniformity, so I let you decide.

I think this seems the more intuitive to me. To avoid too many folders, we can allow tests/issues/XXX/models.{ae,smt2} and tests/issues/XXX/dolmen.{ae,smt2}.

[hra687261]

Does that actually work?

No, turns out it doesn't.

[bclement-ocp]

I am not fully convinced by the naming scheme XXX/XXX.dolmen.smt2 and XXX/XXX.smt2 rather than XXX/dolmen.smt2, but it's not that important and it satisfies the uniform requirement.