-
Notifications
You must be signed in to change notification settings - Fork 75
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
Add support for Bitwuzla and CVC5 #260
Add support for Bitwuzla and CVC5 #260
Conversation
See gussmith23/lakeroad#329 Co-authored-by: Sorawee Porncharoenwase <sorawee.pwase@gmail.com>
I would love to move this towards getting merged @sorawee -- let me know what it needs to get there! One thing: I copied these files and only modified them slightly, so they both may have extra unneeded junk. The cvc5 file is from cvc4; the bitwuzla file is from boolector. I'm not really sure how to tell what's needed and what's not. |
Adding tests would be nice. We have GitHub Actions's workflow that downloads solvers and tests that invoke these solvers. |
@sorawee added them, though I'm sure CI will break til I get all the dependencies right. Can you run the workflow? |
That would require @emina, @jamesbornholt, or @lukenels. I do not have a permission. |
Bump @emina @jamesbornholt @lukenels -- could someone run the workflows? |
Alternatively, deputize @sorawee so he can run them :) Thanks all!!! |
The workflow now runs. It looks like you need a |
@sorawee updated -- can you run again? or whoever ran it last time? |
Ran into some weird behavior on Bitwuzla with the tests, see the above linked issue on Bitwuzla. |
CI is passing. @sorawee @jamesbornholt @emina @lukenels ready for final review. |
This looks good to me, thanks! |
Woohoo! Thank you! |
Adds support for Bitwuzla and cvc5.
I copied and pasted the files for cvc4 and boolector respectively to make the files for cvc5 and bitwuzla. They seem to be working! Thanks for making it so easy to add support. (And thanks @sorawee for the help on this!)
Note: I've only enabled QF_BV for both solvers, as this is all I need at the moment. If you want to enable new solvers, you can just add new entries to the
solver-features
list in each file. This will likely involve having to fix tests as well.