Add support for STP and Yices2

[gussmith23]

Coauthored by @vcanumalla.

TODO before converting from draft:

• [x] Freeze STP at specific checkout
• [x] Make sure tests pass locally

[gussmith23]

Ready for review @sorawee

[sorawee]

Please also add documentation here. And please do that for cvc5 and Bitwuzla as well (perhaps as a separate PR). I overlooked this in #260, which was my bad.

If I understand correctly, on Mac, the brew installation of stp doesn't work, and it must be compiled from source. If that's the case, it would be good to add the version requirement somewhere. Perhaps the documentation might be a good place? I'm open to other possibilities too if you have an idea.

[gussmith23]

Ready for another pass @sorawee

Please also add documentation here. And please do that for cvc5 and Bitwuzla as well (perhaps as a separate PR). I overlooked this in #260, which was my bad.

Done. I added docs for all four solvers in this PR, hope you don't mind. LMK if you want me to move the CVC5/Bitwuzla stuff to a different PR, but it's mostly copy-paste and find-and-replace.

If I understand correctly, on Mac, the brew installation of stp doesn't work, and it must be compiled from source. If that's the case, it would be good to add the version requirement somewhere. Perhaps the documentation might be a good place? I'm open to other possibilities too if you have an idea.

I added a specific note in the STP docs about this!

[gussmith23]

will fix tomorrow!

On Wed, Dec 13, 2023, 5:36 PM Emina Torlak @.***> wrote:

@.**** commented on this pull request.

In rosette/solver/smt/yices-smt2.rkt https://github.com/emina/rosette/pull/273#discussion_r1426068303:

@@ -0,0 +1,69 @@ +#lang racket + +(require racket/runtime-path

• "server.rkt" "env.rkt"
• "../solver.rkt"
• (prefix-in base/ "base-solver.rkt"))

• +(provide (rename-out [make-yices-smt2 yices-smt2]) yices-smt2? yices-smt2-available?)

I think this should be called yices, for consistency with other Rosette solvers.

— Reply to this email directly, view it on GitHub https://github.com/emina/rosette/pull/273#discussion_r1426068303, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAJFZAMO2YRU4RNZHFKLRNTYJJJZ7AVCNFSM6AAAAABATONJG2VHI2DSMVQWIX3LMV43YUDVNRWFEZLROVSXG5CSMV3GSZLXHMYTOOBQG43TMNBTG4 . You are receiving this because you authored the thread.Message ID: @.***>

[gussmith23]

Ready for another review, tests are running now.

BTW: Yices2 tests didn't actually run before, because of the confusion about binary names. (you can see that CI ran STP tests and then finished!) Will have to explicitly check for the Yices2 tests in the logs once CI completes.

[sorawee]

I'm sorry. I missed that you also need to change declare-exporting at the top. Right now the links are red underlined because of that.

[gussmith23]

Done. Sorry, could have checked that locally myself. Looks fine now, locally.

[sorawee]

This looks good to me, thanks!