Open
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
Contributor
Author
|
@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? |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
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!).