Add support for STP and Yices2 #273
Conversation
This reverts commit becbfab.
With the most up-to-date version of STP, all this flag does is force the printing of the model after (check-sat), which causes a parser error.
|
Ready for review @sorawee |
rosette/solver/smt/yices-smt2.rkt
Outdated
| "../solver.rkt" | ||
| (prefix-in base/ "base-solver.rkt")) | ||
|
|
||
| (provide (rename-out [make-yices-smt2 yices-smt2]) yices-smt2? yices-smt2-available?) |
There was a problem hiding this comment.
Why is this called yices-smt2 rather than e.g. yices2 (or yices)?
There was a problem hiding this comment.
See here: https://github.com/SRI-CSL/yices2/blob/e27cf308cffb0ecc6cc7165c10e81ca65bc303b3/doc/NOTES#L1182
Apparently they make different binaries for each frontend (rather than changing the frontend with a flag, as other solvers do)
There was a problem hiding this comment.
I think this should be called yices, for consistency with other Rosette solvers.
|
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 |
|
Ready for another pass @sorawee
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.
I added a specific note in the STP docs about this! |
|
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
<#273 (comment)>:
> @@ -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
<#273 (comment)>, or
unsubscribe
<https://github.com/notifications/unsubscribe-auth/AAJFZAMO2YRU4RNZHFKLRNTYJJJZ7AVCNFSM6AAAAABATONJG2VHI2DSMVQWIX3LMV43YUDVNRWFEZLROVSXG5CSMV3GSZLXHMYTOOBQG43TMNBTG4>
.
You are receiving this because you authored the thread.Message ID:
***@***.***>
|
|
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. |
|
|
||
| @defproc[(bitwuzla-available?) boolean?]{ | ||
| Returns true if the Bitwuzla solver is available for use (i.e., Rosette can locate a @tt{bitwuzla} binary). | ||
| If this returns @racket[#f], @racket[(bitwuzla)] will not succeed |
There was a problem hiding this comment.
To make these hyperlinked correctly, you need to add rosette/solver/smt/bitwuzla, rosette/solver/smt/cvc5, etc. under for-label at the top of this file.
| Rosette specifically uses the @tt{yices-smt2} executable, which is the Yices2 | ||
| solver with its SMTLIB2 frontend enabled. | ||
| Note that just building (without installing) Yices2 will produce an executable | ||
| named @tt{yices_smt2}. This executable can safely be renamed or symlinked to |
There was a problem hiding this comment.
I would add a sentence before "This executable can safely be renamed" to indicate that the installation step will give the correct executable name. Then, say "Alternatively, the built (but not installed) yices_smt2 executable can safely be renamed ..."
|
I'm sorry. I missed that you also need to change 
|
|
Done. Sorry, could have checked that locally myself. Looks fine now, locally. |
|
This looks good to me, thanks! |
Coauthored by @vcanumalla.
TODO before converting from draft: