Allow to skip System.loadLibrary() calls from Java Native class #4667
Conversation
This file contains 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
vlsergey
changed the title
NikolajBjorner
added a commit
that referenced
this pull request
Sep 8, 2020
* fixing issue #4651 * regression fix * fix #4662 Signed-off-by: Nikolaj Bjorner <[email protected]> * na Signed-off-by: Nikolaj Bjorner <[email protected]> * reenabled lift_ites_throttled with an additional filter, without the filter finding the model in report #4651 goes from .02s to 20s, also updated pretty printing of regexes to be more accurate * removing temp testing variable * Allow to skip System.loadLibrary() calls from Java Native class (#4667) * using intended utility methods for sort detection * adding ack/model Signed-off-by: Nikolaj Bjorner <[email protected]> * add smt params dependency Signed-off-by: Nikolaj Bjorner <[email protected]> * missing file Signed-off-by: Nikolaj Bjorner <[email protected]> * deps Signed-off-by: Nikolaj Bjorner <[email protected]> * order Signed-off-by: Nikolaj Bjorner <[email protected]> * persist fields Signed-off-by: Nikolaj Bjorner <[email protected]> * dbg build Signed-off-by: Nikolaj Bjorner <[email protected]> * reset caches Signed-off-by: Nikolaj Bjorner <[email protected]> * sr Signed-off-by: Nikolaj Bjorner <[email protected]> * fix cmake build Signed-off-by: Nikolaj Bjorner <[email protected]> * shuffle dependencies Signed-off-by: Nikolaj Bjorner <[email protected]> * warnings /errors Signed-off-by: Nikolaj Bjorner <[email protected]> * update include Signed-off-by: Nikolaj Bjorner <[email protected]> * missing cmakelists Signed-off-by: Nikolaj Bjorner <[email protected]> * update cmake Signed-off-by: Nikolaj Bjorner <[email protected]> * add depend Signed-off-by: Nikolaj Bjorner <[email protected]> * add depend Signed-off-by: Nikolaj Bjorner <[email protected]> * virtual method Signed-off-by: Nikolaj Bjorner <[email protected]> * path Signed-off-by: Nikolaj Bjorner <[email protected]> * move parameters from ast/rewriter to params Signed-off-by: Nikolaj Bjorner <[email protected]> * move fpa Signed-off-by: Nikolaj Bjorner <[email protected]> * fix warnings Signed-off-by: Nikolaj Bjorner <[email protected]> * remove pragma Signed-off-by: Nikolaj Bjorner <[email protected]> * dbg Signed-off-by: Nikolaj Bjorner <[email protected]> * updated sat_smt Signed-off-by: Nikolaj Bjorner <[email protected]> * na Signed-off-by: Nikolaj Bjorner <[email protected]> * fix #4651 Signed-off-by: Nikolaj Bjorner <[email protected]> * encoding options #4665 Signed-off-by: Nikolaj Bjorner <[email protected]> * expose name inclusion as optional Signed-off-by: Nikolaj Bjorner <[email protected]> * fix misc issues around #4661 introduced when adding lazy push/pop to selected theories Signed-off-by: Nikolaj Bjorner <[email protected]> * remove lazy push from theory_lra Signed-off-by: Nikolaj Bjorner <[email protected]> * na Signed-off-by: Nikolaj Bjorner <[email protected]> * fix dotnet build Signed-off-by: Nikolaj Bjorner <[email protected]> * na Signed-off-by: Nikolaj Bjorner <[email protected]> * release nodes Signed-off-by: Nikolaj Bjorner <[email protected]> * free memory in egraph Signed-off-by: Nikolaj Bjorner <[email protected]> * avoid duplicate class names frame in sat_scc and sat_smt Signed-off-by: Nikolaj Bjorner <[email protected]> * adding euf Signed-off-by: Nikolaj Bjorner <[email protected]> * elaborate on smt/drat format outline, expose euf mode as config Signed-off-by: Nikolaj Bjorner <[email protected]> * mk-var during copy Signed-off-by: Nikolaj Bjorner <[email protected]> * move theory_var_list into id_var_list and utilities from smt-enode into it, prepare for theory variables in egraph Signed-off-by: Nikolaj Bjorner <[email protected]> * with bounded Signed-off-by: Nikolaj Bjorner <[email protected]> * na Signed-off-by: Nikolaj Bjorner <[email protected]> * Remove duplicate binary condition. Fixes #4668. * butterfly effect on fp? Signed-off-by: Nikolaj Bjorner <[email protected]> * prepare for theory plugins Signed-off-by: Nikolaj Bjorner <[email protected]> * file Signed-off-by: Nikolaj Bjorner <[email protected]> * build fix * remove SMTFD Signed-off-by: Nikolaj Bjorner <[email protected]> * na Signed-off-by: Nikolaj Bjorner <[email protected]> * na * na Signed-off-by: Nikolaj Bjorner <[email protected]> * na Signed-off-by: Nikolaj Bjorner <[email protected]> * na Signed-off-by: Nikolaj Bjorner <[email protected]> * na Signed-off-by: Nikolaj Bjorner <[email protected]> * na Signed-off-by: Nikolaj Bjorner <[email protected]> * na Signed-off-by: Nikolaj Bjorner <[email protected]> * na Signed-off-by: Nikolaj Bjorner <[email protected]> * SMTFD is back (#4676) * fixing issue #4651 * regression fix * reenabled lift_ites_throttled with an additional filter, without the filter finding the model in report #4651 goes from .02s to 20s, also updated pretty printing of regexes to be more accurate * removing temp testing variable * using intended utility methods for sort detection * misc edits related to nonground regexes * bug fix of state id off by 1 calculation error and improved pretty printing with regex tooltip generated in dgml state graph * removed unused method declaration * improved id to regex value map info in generated dgml * reorgd callback function for state pretty printer * updated some comments Co-authored-by: Nikolaj Bjorner <[email protected]> Co-authored-by: Sergey Vladimirov <[email protected]> Co-authored-by: Christoph M. Wintersteiger <[email protected]> Co-authored-by: Arie Gurfinkel <[email protected]>
|
@NikolajBjorner and @vlsergey |
|
not sure what is the best place for documenting this |
NikolajBjorner
pushed a commit
that referenced
this pull request
Aug 13, 2021
…e library in Java bindings (#5477) * limit range of environment variable for loading the native library in Java to "true". This change specifies the range of values that are allowed to set the environment variable "z3.skipLibraryLoad". Only the value "true" (in upper-, lower-, and mixed-case is accepted as valid value. Other values, such as "false", "0", "1", "foo", an empty or a missing value are evaluated to "false" and cause the default loading of the native library. * adding documentation about environment variable for (not) loading the native library in Java. This is a follow-up commit for #4667 to provide a publicly visible documentation.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
It's not hard for client code to write a couple of lines for System.loadLibrary()
But it is very very hard for client code to embed Z3 code into JAR file where libraries are need to be loaded from JAR file (as resource). The problem here that System.loadLibrary() works only if libraries are placed in java.library.path and does not allow to load it from temporary folder/file.