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!).

I plan on adding a common logic selection that is uniform in all solvers once we have this and #636 merged.

[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.

[baierd]

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.

@PhilippWendler can we link 2 licenses?

[baierd]

@ThomasHaas i can add it, but (set-info :license "https://creativecommons.org/licenses/by/4.0/") remains in the SMTLIB2 files. Should i also update that?

[ThomasHaas]

@ThomasHaas i can add it, but (set-info :license "https://creativecommons.org/licenses/by/4.0/") remains in the SMTLIB2 files. Should i also update that?

I think that is not necessary. You can maybe just remove that line because it was the SMTComp-specific way of providing licenses.

I also think the extra .license files become obsolete with the SPDX headers directly embedded in the SMTLIB2 files.

[baierd]

Done. Thanks for the quick reply!

[PhilippWendler]

@PhilippWendler can we link 2 licenses?

If a conjunction of licences apply to a file, then we have no other choice than to specify that conjunction. We cannot just change the license.

[daniel-raffler]

There are a few open TODOs left in the code. However, maybe these are easier to address once we have more general support for solver options or setting the logic?

[ThomasHaas]

Bump :)

FYI, besides standard options, Z3 also supports tactics and simplifiers. The simplifiers are quite interesting because they enable in-processing of incremental queries.
For example, smt.solve-eqs=true does not seem to work on incremental queries, but adding (set-simplifier solve-eqs) directly to the smtlib2 file does work.

If you feel particularly bored, maybe adding a special option z3.simplifiers=<listOfSimplifiers> that creates simplifiers using Z3_mk_simplifier(...), concatenates them via Z3_simplifier_and_then(...), and then attaches them to the solver via Z3_solver_add_simplifier(...) could be interesting (if they are exposed via Z3's Java API at all?).

There seems to be some ongoing AI-powered effort on Z3's side to convert existing tactics to simplifiers to allow their use in incremental solving. I experimented a little bit with simplifiers and found only mild success so far (or at least measurable impact) using (set-simplifier (then simplify solve-eqs propagate-values)). That being said, I only tested it on 2-3 examples.

[baierd]

There are a few open TODOs left in the code. However, maybe these are easier to address once we have more general support for solver options or setting the logic?

Exactly, i wanted to note them down to get this merged and then move on to add the logics for the other solves before adding a common API.

[baierd]

Bump :)

FYI, besides standard options, Z3 also supports tactics and simplifiers. The simplifiers are quite interesting because they enable in-processing of incremental queries. For example, smt.solve-eqs=true does not seem to work on incremental queries, but adding (set-simplifier solve-eqs) directly to the smtlib2 file does work.

There seems to be some ongoing AI-powered effort on Z3's side to convert existing tactics to simplifiers to allow their use in incremental solving. I experimented a little bit with simplifiers and found only mild success so far (or at least measurable impact) using (set-simplifier (then simplify solve-eqs propagate-values)). That being said, I only tested it on 2-3 examples.

Thank you for the information! We will definitely add simplifiers at some point. But since they actually seem to be more useful now and in the future, we can also speed this up.

If you feel particularly bored, maybe adding a special option z3.simplifiers=<listOfSimplifiers> that creates simplifiers using Z3_mk_simplifier(...), concatenates them via Z3_simplifier_and_then(...), and then attaches them to the solver via Z3_solver_add_simplifier(...) could be interesting (if they are exposed via Z3's Java API at all?).

That is definitely how we will add them! I would argue that we finish this PR first, then look into simplifiers.

[ThomasHaas]

If you feel particularly bored, maybe adding a special option z3.simplifiers=<listOfSimplifiers> that creates simplifiers using Z3_mk_simplifier(...), concatenates them via Z3_simplifier_and_then(...), and then attaches them to the solver via Z3_solver_add_simplifier(...) could be interesting (if they are exposed via Z3's Java API at all?).

That is definitely how we will add them! I would argue that we finish this PR first, then look into simplifiers.

I agree with doing it in a separate PR. I only really care about the arithmetic solver option to enable IDL-specific reasoning :).

[daniel-raffler]

LGTM!

[PhilippWendler]

I would recommend to not add an API that changes an existing test setup retroactively to the API. This can easily cause problems for example when users accidentally use the solver before re-initializing it. And SolverBasedTest0 is supposed to be used by client code and the new methods are available to all code using it, so it is effectively public and removing the methods later on would be a breaking change.

Why not simply use the existing methods that SolverBasedTest0 already provides? Just override createTestConfigBuilder() and set the options in the returned instance.

[baierd]

I would recommend to not add an API that changes an existing test setup retroactively to the API. This can easily cause problems for example when users accidentally use the solver before re-initializing it. And SolverBasedTest0 is supposed to be used by client code and the new methods are available to all code using it, so it is effectively public and removing the methods later on would be a breaking change.

Why not simply use the existing methods that SolverBasedTest0 already provides? Just override createTestConfigBuilder() and set the options in the returned instance.

I see. Thanks for the hint! I'll take another look and update the code!