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

Update Bitwuzla code for new API #347

Merged
merged 49 commits into from
Jun 18, 2024

Conversation

samanthaarcher0
Copy link
Contributor

@samanthaarcher0 samanthaarcher0 commented May 16, 2024

Add support for the new C++ API of Bitwuzla

@samanthaarcher0 samanthaarcher0 marked this pull request as draft May 16, 2024 22:07
@CyanoKobalamyne CyanoKobalamyne self-requested a review May 16, 2024 22:08
@CyanoKobalamyne CyanoKobalamyne self-assigned this May 16, 2024
@CyanoKobalamyne CyanoKobalamyne changed the title Bitwuzla update for SMT Switch Update Bitwuzla code for new API May 21, 2024
@CyanoKobalamyne CyanoKobalamyne marked this pull request as ready for review June 14, 2024 01:42
@CyanoKobalamyne
Copy link
Collaborator

@yoni206 I think this is good to go now, please take a look when you have the chance.

Copy link
Collaborator

@yoni206 yoni206 left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks for all of this. It looks fine, though I am wondering if this would be a good opportunity to add a corresponding test directory to here https://github.com/stanford-centaur/smt-switch/tree/main/tests (I think bitwuzla is the only solver that doesn't have one, right?)

@CyanoKobalamyne
Copy link
Collaborator

I can do that, but this PR is already big enough, so maybe let's merge that separately.

@CyanoKobalamyne
Copy link
Collaborator

Actually, what are the solver-specific tests testing that the top-level ones aren't? They mostly just seem a lot older.

@yoni206 yoni206 merged commit 2da835b into stanford-centaur:main Jun 18, 2024
12 checks passed
@yoni206
Copy link
Collaborator

yoni206 commented Jun 18, 2024

You are right, it is not really related to this PR. Merged.
Also, I actually don't see a real difference between these two types of tests.
For example, the tests inside the solver directories also just create a solver with the factory, nothing more internal than that.
So perhaps we can at some point port these tests into the unit tests. But that's also not related to this PR and is not urgent.

Thanks for updating bitwuzla!

@CyanoKobalamyne
Copy link
Collaborator

Yay, of course, thanks for reviewing! And thank you to @samanthaarcher0! :)

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.

None yet

3 participants