Update Yices bindings and add some missing features#8
Open
daniel-raffler wants to merge 8 commits intoSRI-CSL:masterfrom
Open
Update Yices bindings and add some missing features#8daniel-raffler wants to merge 8 commits intoSRI-CSL:masterfrom
daniel-raffler wants to merge 8 commits intoSRI-CSL:masterfrom
Conversation
We're not adding the entire ff API, but just the new constructors. This was necessary as the new constructors changed the values of existing constructors Adding the rest of the API will have to be done in a separate commit See SRI-CSL/yices2#605
Yices may return zero mappings for a function if it is constant (f.ex `f(x)=0`)
Yices will rewrite terms that were built with regular (binary) addition or multiplication as sums and products. So we need these methods to access the terms, even when we're not creating sums/products ourselves
Set the system property 'yices.skipAutoloader' to 'true' if the binary has already been preloaded
With failifexecutionfails the build only fails if the `make` command can't be found. We should use failonerror instead, and abort if `make` has returned an error
|
Hi, |
Author
|
Thanks for looking into this! |
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
2 participants
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.
Hello everyone,
I'm working on the JavaSMT project, which is a library wrapper that provide a unified interface for SMT solvers in Java. We've recently moved the Yices backend from our own JNI bindings to your project. This PR contains some changes that were necessary to get all of our features to work:
nullto be used as defaultParametersModel.expandFunctionless strict to allow for functions that only have a default valueWe'd like to merge as much of this upstream as possible. Could you have a look at it to see which parts may be useful to you? If you only need some of the changes, the commits should be self-contained, so you can simply pick and choose the parts you need
Cheers,
Daniel