Conversation
…n of the test-setup
…s (missing: tactics)
… options. Also rework processing of options by adding type retrieval via the options (as int and double can otherwise not be discerned) and processing of options
…ption value type is double and removing the expensive resolving of all types
…ns info getter in Z3SolverContext to declutter the manager
…heck that we don't forget HORN for spacer
…sions for more options to set
… we want those to be proper settings in the future!) and resolve them correctly when building new Z3 solver instances
…text to fail early for known incompatibilities and make retrieval of important options easier + better option descriptions
…eficial (currently not fully working)
… incremental usage for logic tests (as otherwise Z3 is equally fast with and without using the logic)
…r with certain options (Provided by Thomas Haar here: #613 (comment) referencing: Z3Prover/z3#8940 (comment) )
… complains about the name)
… 8 (from default: 7)
…y test that they work + documentation and refactor explicit timeout thread creation into a method
|
@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? |
|
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. |
|
So, there are a bunch of things here.
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.
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 |
|
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.)
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. |
|
Can you just add 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. |
@PhilippWendler can we link 2 licenses? |
|
@ThomasHaas i can add it, but |
… source license as well
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. |
|
Done. Thanks for the quick reply! |
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. |
…CI is a little slow sometimes
daniel-raffler
left a comment
daniel-raffler
left a comment
There was a problem hiding this comment.
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?
| SPDX-FileCopyrightText: Generator: Dartagnan | ||
| SPDX-FileCopyrightText: Application: Bounded model checking for weak memory models | ||
| SPDX-FileCopyrightText: Hernán Ponce de León, Florian Furbach, Keijo Heljanko, Roland Meyer: Dartagnan: Bounded Model Checking for Weak Memory Models (Competition Contribution). TACAS (2) 2020: 378-382 | ||
| SPDX-FileCopyrightText: Thomas Haas, Roland Meyer, Hernán Ponce de León: CAAT: consistency as a theory. Proc. ACM Program. Lang. 6(OOPSLA2): 114-144 (2022) | ||
| SPDX-FileCopyrightText: License: https://creativecommons.org/licenses/by/4.0/ | ||
| SPDX-FileCopyrightText: Modified to no include incremental solving | ||
|
|
||
| SPDX-License-Identifier: CC-BY-4.0 AND MIT |
There was a problem hiding this comment.
Do we still need separate license files? They appear to wind up in out jar, which is probably not ideal:
daniel@notebook:~/workspace/java-smt$ jar tf java-smt-6.0.0-629-g3ca8c0bed-dirty.jar | grep smt2
org/sosy_lab/java_smt/test/client.smt2.license
org/sosy_lab/java_smt/test/manyRegReads.smt2.licenseMaybe there is a way to move all the license information to the header in the files themselves?
| OPT_PRIORITY_CONFIG_KEY, | ||
| OPT_ENGINE_CONFIG_KEY); | ||
|
|
||
| enum ENGINE { |
There was a problem hiding this comment.
I think we only use all-caps for enum values, but not for the type names
| import org.sosy_lab.java_smt.api.BooleanFormula; | ||
| import org.sosy_lab.java_smt.api.SolverException; | ||
|
|
||
| public class SolverNativeOptionsTest extends SolverBasedTest0.ParameterizedSolverBasedTest0 { |
There was a problem hiding this comment.
The tests here seem pretty specific to Z3. We could just use extends SolverBasedTest0 to skip the other solvers, and then move the file someplace else (like solvers/z3)
| /** | ||
| * Options string for all available options tied to the environment of the solver. The options are | ||
| * returned 1 per line, with the pattern: | ||
| * | ||
| * <p>optionName{.detailedName} (type) infoText that may include brackets (default: defaultValue) | ||
| * | ||
| * <p>e.g.: local_ctx (bool) perform local (i.e., cheap) context simplifications (default: false) | ||
| */ | ||
| String getAllZ3Options() { | ||
| return Native.simplifyGetHelp(getEnvironment()); | ||
| } | ||
|
|
There was a problem hiding this comment.
Is this still used? Or has it been replaced by Z3SolverContext.getAllZ3Options()?
| */ | ||
| private static Thread buildShutdownThreadWith( | ||
| ShutdownManager pShutdownManager, long millisTillShutdown) { | ||
| // (Do not ever use @Test(timeout = ...) on Z3! It SIGSEGVs! |
There was a problem hiding this comment.
Has this been reported yet?
4 participants
This PR adds 3 explicit new configuration options to Z3:
unsigned intandfloatas for example2can 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 inttake typeintin 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.