-
Notifications
You must be signed in to change notification settings - Fork 1.5k
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
SMTFD is back #4676
Merged
Merged
SMTFD is back #4676
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
NikolajBjorner
added a commit
that referenced
this pull request
Sep 8, 2020
* fixing issue #4651 * regression fix * fix #4662 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * na Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * 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 <nbjorner@microsoft.com> * add smt params dependency Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * missing file Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * deps Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * order Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * persist fields Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * dbg build Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * reset caches Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * sr Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix cmake build Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * shuffle dependencies Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * warnings /errors Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * update include Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * missing cmakelists Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * update cmake Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * add depend Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * add depend Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * virtual method Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * path Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * move parameters from ast/rewriter to params Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * move fpa Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix warnings Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * remove pragma Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * dbg Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * updated sat_smt Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * na Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix #4651 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * encoding options #4665 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * expose name inclusion as optional Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix misc issues around #4661 introduced when adding lazy push/pop to selected theories Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * remove lazy push from theory_lra Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * na Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix dotnet build Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * na Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * release nodes Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * free memory in egraph Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * avoid duplicate class names frame in sat_scc and sat_smt Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * adding euf Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * elaborate on smt/drat format outline, expose euf mode as config Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * mk-var during copy Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * 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 <nbjorner@microsoft.com> * with bounded Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * na Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * Remove duplicate binary condition. Fixes #4668. * butterfly effect on fp? Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * prepare for theory plugins Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * file Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * build fix * remove SMTFD Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * na Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * na * na Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * na Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * na Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * na Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * na Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * na Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * na Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * 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 <nbjorner@microsoft.com> Co-authored-by: Sergey Vladimirov <vlsergey@gmail.com> Co-authored-by: Christoph M. Wintersteiger <cwinter@microsoft.com> Co-authored-by: Arie Gurfinkel <arie.gurfinkel@gmail.com>
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.
Request to put SMTFD back until a better solver becomes available