Fix expected verdicts of XCSP (swapped), improve recreation

[lembergerth]

The expected verdicts of XCSP seem to have been swapped.

Benchmark tasks created from satisfiable constraint-solving problems can reach the call to reach_error, so their verdict should be 'false', and vice versa.

In the process of fixing this, I realized that the creation-script for these tasks was not adjusted to the new task-definition format and that recreation was difficult because the xcsp3_cpp_parser required to transform XCSP-tasks into C programs had to be downloaded and built manually.

I've adjusted the creation script and included the xcsp3_cpp_parser binary in the directory. I hope I set the corresponding licenses correctly; it would be nice if the reviewer could also double-check these.

@matthiaskettl, the original author of these tasks, wrote:

Yes, based on your explanation I think I confused the verdicts.

I used https://arxiv.org/pdf/2001.07914 (page 5, first paragraph under "A. Experimental Setup") as resource.

The linked paper states:

We tested three classes of extensional constraint problems: AIM-100 and AIM-200 (each consists of 16 satisfiable and 8 unsatisfiable problems), and Dubois (30 unsatisfiable problems). For intensional CSP problems, we used the All-Interval (19 satisfiable problems), Costas- Array (8 satisfiable problems), and Haystacks (14 problems) problem classes

It does not state whether 'Haystacks' is satisfiable or unsatisifiable, so we assumed that they are satisfiable. According to this explanation, the verdicts should be ok now.

[lembergerth]

How about letting the script also generate REUSE-style license headers while you are already improving it?

I've added calls to the corresponding reuse commands to the Makefile. I guess it is unlikely, but if other tasks are added to this directory, people have to be careful about stating the correct copyright.

Is this good enough?

[PhilippWendler]

Thanks! I would say, yes, this is fine.

Adding headers to task-definition files is ok, but in #1099 we decided that we do not require them, so you could also leave them out if you want (and have a smaller diff).

I noticed in the origin LICENSE file there is attribution to Dirk Beyer, though I do not know what exactly it applies to. Because the license requires us to keep attribution, the easiest way would be to add it to basically all files in the directory except the task-definition files?

[lembergerth]

Adding headers to task-definition files is ok, but in #1099 we decided that we do not require them, so you could also leave them out if you want (and have a smaller diff).

Ok, I removed them. I didn't bother reading through the whole PR, but relied on the documentation in CONTRIBUTING.md and your input.

I noticed in the origin LICENSE file there is attribution to Dirk Beyer, though I do not know what exactly it applies to.

The tasks are pretty new, so this is easy to track back.

• The original tasks are copyrighted by Gilles Audemard and licensed under MIT.
• xcsp3_cpp_parser is copyrighted by Olivier Roussel and the XCSP3 team.
• The script that creates the final SV benchmark tasks uses xcsp3_cpp_parser and performs multiple file modifications. It was created by @matthiaskettl and is thus under copyright of Dirk Beyer.
• Because the final benchmark files were created by @matthiaskettl/created from his script, they are copyright of Dirk Beyer.

So there is no software involved with copyright by Dirk Beyer, but only the script present here and the final tasks. Is this knowledge enough to just give the copyright to the SV-benchmarks community (and Gilles Audemard)? Actually, do we have to include Olivier Roussel in the copyright of the benchmark tasks?

Edit in italics

[PhilippWendler]

I see, thanks for taking the effort to investigate!

Here my interpretation:

Gilles Audemard is definitely one copyright holder of the final C files if these were generated from his tasks (similar example for reference: the author of source code also has copyright on the resulting binary after compilation).

The creator of the script for generating tasks from another source might or might not have a copyright on the products. Typically, if you create a tool (like a paint program) you do not have copyright on the works created with it, but if for example your script is creating larger parts of the final sources from itself (e.g., by hard-coded inserting snippets), then one could probably claim partial copyright.

The action of executing a script on a certain set of input files does not grant any copyright.

The authors of the parser won't get any copyright on anything (though if the parser would have been GPL, the script that uses it would have to satisfy the respective restrictions).

If we put this together, it seems the script should have copyright statements for Dirk Beyer (and I would say the SV-Benchmarks Community because it uses definitions etc. defined by it) and the final sources should have copyright by Gilles Audemard and maybe Dirk Beyer and the SV-Benchmarks Community.

[lembergerth]

Makes total sense - thanks for taking the time to think of examples, this really helps to understand the issue. I've added Dirk Beyer's copyright to the corresponding files; the other copyrights were already present.

[dbeyer]

@lembergerth CI complains, unfortunately.

[lembergerth]

Thanks for the pointer - let's see whether it's fixed now.

[lembergerth]

@PhilippWendler or @dbeyer , CI is passing. Could you approve and merge the PR please?

[lembergerth]

@matthiaskettl Since you are the original contributor of these tasks, would you mind to also review my changes?