Skip to content
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

Better Bitwuzla solver support #71

Merged
merged 72 commits into from
Feb 17, 2023
Merged

Better Bitwuzla solver support #71

merged 72 commits into from
Feb 17, 2023

Conversation

Saloed
Copy link
Collaborator

@Saloed Saloed commented Feb 14, 2023

JNI bindings

  • Replace JNA with JNI bindings (based on @DKARAGODIN implementation)
  • Proper native exceptions handling
  • Solver timeout implementation without callbacks from Native to Java

Bitwuzla solver

  • Support uninterpreted sorts (Bv32 is used as replacement)
  • Fix quantifiers internalization/convertion
  • Fix tracking of currenlty declared constants
  • Support fpToIEEEBv expression using assertion-with-axiom mechanism

Other

  • Better evaluation of array select expressions
  • Fixes in test infrastructure

@Saloed Saloed force-pushed the simplifying-context branch from 20dbd32 to 07063df Compare February 14, 2023 10:15
@Saloed Saloed force-pushed the bitwuzla-jni-bindings branch from 70db44e to 6721e97 Compare February 14, 2023 10:29
@Saloed Saloed force-pushed the bitwuzla-jni-bindings branch from 6721e97 to b2ddf91 Compare February 17, 2023 16:17
@Saloed Saloed requested a review from CaelmBleidd February 17, 2023 16:52
@Saloed Saloed force-pushed the bitwuzla-jni-bindings branch from 32f6220 to 4e021a3 Compare February 17, 2023 17:02
Base automatically changed from simplifying-context to main February 17, 2023 17:22
@Saloed Saloed force-pushed the bitwuzla-jni-bindings branch from 4e021a3 to e8c95dc Compare February 17, 2023 18:08
@Saloed Saloed merged commit a188ab9 into main Feb 17, 2023
@Saloed Saloed deleted the bitwuzla-jni-bindings branch February 17, 2023 18:17
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants