search

stanford-centaur / smt-switch

A generic C++ API for SMT solving. It provides abstract classes which can be implemented by different SMT solvers.
Other
103 stars 40 forks source link

Update Bitwuzla code for new API #347

Closed samanthaarcher0 closed 3 months ago

samanthaarcher0 commented 4 months ago

Add support for the new C++ API of Bitwuzla

CyanoKobalamyne commented 3 months ago

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

CyanoKobalamyne commented 3 months ago

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

CyanoKobalamyne commented 3 months ago

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

yoni206 commented 3 months ago

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 commented 3 months ago

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