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

Add support for STP and Yices2 solvers #272

Closed
wants to merge 13 commits into from

Conversation

vcanumalla
Copy link
Contributor

@vcanumalla vcanumalla commented Dec 7, 2023

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

  • Added appropriate files in the rosette/solver/smt directory for the corresponding solvers.
  • Use of the solvers in all-rosette-tests.rkt
  • 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
Copy link
Contributor Author

Marking as a draft until I fix failing tests

@vcanumalla vcanumalla marked this pull request as draft December 7, 2023 06:05
@vcanumalla
Copy link
Contributor Author

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

@vcanumalla vcanumalla closed this Dec 7, 2023
@gussmith23
Copy link
Contributor

See stp/stp#475

@gussmith23
Copy link
Contributor

gussmith23 commented Dec 12, 2023

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

  1. 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: Get models in SMTLIB2 format without printing ASSERTs (Mac specific issue?) stp/stp#475
  2. 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: Bug with push and pop stp/stp#476

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

2 participants