Add support for STP and Yices2 solvers

emina / rosette

The Rosette solver-aided host language, sample solver-aided DSLs, and demos

Other

640 stars 74 forks source link

Add support for STP and Yices2 solvers #272

Closed vcanumalla closed 10 months ago

vcanumalla commented 10 months ago

This PR adds support for STP and Yices2 (Yices-smt2) solvers. We initially used these solvers in our project Lakeroad, and they have performed well in our tool and in the the smtcomp2023.

I've created a PR request from, what I can tell, contains everything I need to add support for the solvers. I've

[x] Added appropriate files in the rosette/solver/smt directory for the corresponding solvers.
[x] Use of the solvers in all-rosette-tests.rkt
[x] Added the solvers to the github workflows for the tests (I believe I did this properly)

Please let me know any fixes, or suggestions folks have before merging!

Thanks a bunch!

vcanumalla commented 10 months ago

Marking as a draft until I fix failing tests

vcanumalla commented 10 months ago

stp fix looks like it might be larger than I thought, will close this PR until its ready

gussmith23 commented 10 months ago

See https://github.com/stp/stp/issues/475

gussmith23 commented 10 months ago

FYI: seems like there are two different issues here w/r/t STP.

There is a strange issue with STP on Mac. The Homebrew version (which is the version easiest to install) is out of date, which causes a different set of errors within Rosette when you run the tests on a Mac. Bug is logged here: https://github.com/stp/stp/issues/475
If you run on Ubuntu (as Rosette's CI does) then you get the most up-to-date STP, but that version of STP runs into other errors later in the testing process. Debugging those errors now. Update: Bug is logged here: https://github.com/stp/stp/issues/476