Add logic, engine and further options for Z3

[baierd]

This PR adds 3 explicit new configuration options to Z3:

• logic: sets the logic used for all provers created in a Z3 context.
• engine: sets the engine used in all provers of a Z3 context.
• furtherOptions: allows to specify more options for Z3, besides the ones that we set internally or in other options. Note: option values can habe several types that need to be adhered to. Parsing these from Strings is difficult for the types unsigned int and float as for example 2 can be both. I extracted all options with float type and check against them, as there is only 7 or so.

Also, 2 new test classes are added.

• Z3NativeApiTest: has 2 native tests, one for HORN solving with Spacer (taken from an old implementation that we did not merge), that shows logic selection and engine selection, as well as a test that checks whether we handle the types of option values correctly (even for new versions).
• SolverNativeOptionsTest: tests that we can hand options through to the solver via our config options. Some tests (logic and HORN tests) should be moved out of that folder into dedicated test-classes once we implement common solutions.

I added some extensions to our test setup to handle configuration changes gracefully.
I also noticed that it is helpful to have a assertThat... implementation that actually uses multiple assertions (e.g. for HORN solving. As a conjunction of multiple formulas is no equal to asserting them on their own for Z3! I opened !625 to discuss and develop extensions for our Truth based API.)

Part of the request in #613.

Note: option values with type unsigned int take type int in Z3s Java API. We should check whether this is a bug or wraps around in C (meaning we need to translate values above Cs signed int maximum in Java!).

[baierd]

@kfriedberger i added 2 SMT files provided by @ThomasHaas. They have their licenses included already, but reuse is not recognizing them. Do i need to add our license on top, or the license provided in the files explicitly?

[ThomasHaas]

If the license is problematic in any way, feel free to remove it. If you think this is too sketchy, I can remove the licensing for you :).

[baierd]

If the license is problematic in any way, feel free to remove it. If you think this is too sketchy, I can remove the licensing for you :).

I don't think that it is problematic. I just want to do it correctly and i am not sure what the process is. I think it is just applying ours over yours as long as yours allows it. Actually @PhilippWendler surely knows.

[baierd]

If the license is problematic in any way, feel free to remove it. If you think this is too sketchy, I can remove the licensing for you :).

I don't think that it is problematic. I just want to do it correctly and i am not sure what the process is. I think it is just applying ours over yours as long as yours allows it. Actually @PhilippWendler surely knows.

@ThomasHaas i just added your license with the required note on modification. All should be well now.

[PhilippWendler]

So, there are a bunch of things here.

I think it is just applying ours over yours as long as yours allows it.

No, there is no reason for us to complicate the situation by conjuncting another license to the given one. It is preferable to just ship the test files with their original license.

If the test files were generated by Dartagnan, this would typically not imply that the authors of Dartagnan have any copyright on them and can decide the license (just as compiler authors typically do not have copyright on the compiled binary). An exception is if the tool output contains copies of parts of the tool (for example where a compiler copies some functions from the stdlib into the binary) or if an argument can be made that the output is a work derived from the tool, but I am not sure if this applies here.

On the other hand, if the test file is the transformed version of a program, then copyright and license of the input program need to be respected (just like for a compiled binary). So if this is the case, please add copyright and license from the original program (because typically all open-source licenses require that when shipping a modified version of the program, one has to copy the license and copyright info, even if one is free to choose a different license).

If the test files are not transformed versions of programs, then the above does not apply and the copyright belongs to the persons that wrote the test files.

SPDX-FileCopyrightText should contain only copyright information, in particular the information that we are legally required to provide (in the case that the input program has copyright information and a license that requires us to keep it). The current files seem to contain only information that does not fall into this category. So please replace it (of course keep such non-legally-relevant information as regular notes in the test file). The note about modification must just be present, but not part of SPDX-FileCopyrightText.

It is always better to keep the legal information as close as possible to the file it apples to. Thus the preferred way is to add license and copyright info to the file itself, and use a .license file only where there is no other technical solution. It seems that it should be trivial to add the SPDX-* clauses to set-info, so please do so.

[ThomasHaas]

On the other hand, if the test file is the transformed version of a program, then copyright and license of the input program need to be respected (just like for a compiled binary). So if this is the case, please add copyright and license from the original program (because typically all open-source licenses require that when shipping a modified version of the program, one has to copy the license and copyright info, even if one is free to choose a different license).

manyRegReads is a program written by me specifically to show-case a problem, so it doesn't have any license/copyright. It is not publicly available.
client comes from a program committed in our repo. In that case, are you saying that the repo's MIT license must be preserved in the generated SMT?

[PhilippWendler]

manyRegReads is a program written by me

So you can choose a license freely. And you should also be listed as the copyright holder. (Or for both: your employer if you wrote it as part of a contract.)

client comes from a program committed in our repo. In that case, are you saying that the repo's MIT license must be preserved in the generated SMT?

Depends if the MIT license applies to that program. Many repos have test programs that are not under the main license but under different license, e.g., because they come from different sources. This is the reason why REUSE is such a great thing: Keeping a license attached in a machine-readable format to every single file greatly simplifies such questions.

[ThomasHaas]

Can you just add

; SPDX-FileCopyrightText: NONE
; SPDX-License-Identifier: CC-BY-4.0 AND MIT

to the smtlib files? That would add the missing MIT license (on top of CC-BY-4.0) from the source programs and remove any copyright.
If that is too sketchy for you, I can download the files from the PR and change it myself, but it doesn't feel any less sketchy to me :P.