search

emina / rosette

The Rosette solver-aided host language, sample solver-aided DSLs, and demos
Other
638 stars 74 forks source link

Add support for Bitwuzla and CVC5 #260

Closed gussmith23 closed 1 year ago

gussmith23 commented 1 year ago

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.

gussmith23 commented 1 year ago

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.

sorawee commented 1 year ago

Adding tests would be nice. We have GitHub Actions's workflow that downloads solvers and tests that invoke these solvers.

gussmith23 commented 1 year ago

@sorawee added them, though I'm sure CI will break til I get all the dependencies right. Can you run the workflow?

sorawee commented 1 year ago

That would require @emina, @jamesbornholt, or @lukenels. I do not have a permission.

gussmith23 commented 1 year ago

Bump @emina @jamesbornholt @lukenels -- could someone run the workflows?

gussmith23 commented 1 year ago

Alternatively, deputize @sorawee so he can run them :)

Thanks all!!!

sorawee commented 1 year ago

The workflow now runs. It looks like you need a sudo for apt-get install.

gussmith23 commented 1 year ago

@sorawee updated -- can you run again? or whoever ran it last time?

gussmith23 commented 1 year ago

Ran into some weird behavior on Bitwuzla with the tests, see the above linked issue on Bitwuzla.

gussmith23 commented 1 year ago

CI is passing. @sorawee @jamesbornholt @emina @lukenels ready for final review.

sorawee commented 1 year ago

This looks good to me, thanks!

gussmith23 commented 1 year ago

Woohoo! Thank you!