From 01cf9f3c30c0bff98d01422a09d5a4e0d64b09f7 Mon Sep 17 00:00:00 2001 From: Vishal Canumalla Date: Tue, 28 Nov 2023 21:02:50 -0800 Subject: [PATCH 01/30] stp support --- rosette/solver/smt/stp.rkt | 68 ++++++++++++++++++++++++++++++++++++++ test/all-rosette-tests.rkt | 34 ++++++++++--------- 2 files changed, 87 insertions(+), 15 deletions(-) create mode 100644 rosette/solver/smt/stp.rkt diff --git a/rosette/solver/smt/stp.rkt b/rosette/solver/smt/stp.rkt new file mode 100644 index 00000000..f98ac5ad --- /dev/null +++ b/rosette/solver/smt/stp.rkt @@ -0,0 +1,68 @@ +#lang racket + +(require racket/runtime-path + "server.rkt" "env.rkt" + "../solver.rkt" + (prefix-in base/ "base-solver.rkt")) + +(provide (rename-out [make-stp stp]) stp? stp-available?) + +(define-runtime-path stp-path (build-path ".." ".." ".." "bin" "stp")) +(define stp-opts '()) + +(define (stp-available?) + (not (false? (base/find-solver "stp" stp-path #f)))) + +(define (make-stp [solver #f] #:options [options (hash)] #:logic [logic #f] #:path [path #f]) + (define config + (cond + [(stp? solver) + (base/solver-config solver)] + [else + (define real-stp-path (base/find-solver "stp" stp-path path)) + (when (and (false? real-stp-path) (not (getenv "PLT_PKG_BUILD_SERVICE"))) + (error 'stp "stp binary is not available (expected to be at ~a); try passing the #:path argument to (stp)" (path->string (simplify-path stp-path)))) + (base/config options real-stp-path logic)])) + (stp (server (base/config-path config) stp-opts (base/make-send-options config)) config '() '() '() (env) '())) + +(struct stp base/solver () + #:property prop:solver-constructor make-stp + #:methods gen:custom-write + [(define (write-proc self port mode) (fprintf port "#"))] + #:methods gen:solver + [ + (define (solver-features self) + '(qf_bv)) + + (define (solver-options self) + (base/solver-options self)) + + (define (solver-assert self bools) + (base/solver-assert self bools)) + + (define (solver-minimize self nums) + (base/solver-minimize self nums)) + + (define (solver-maximize self nums) + (base/solver-maximize self nums)) + + (define (solver-clear self) + (base/solver-clear self)) + + (define (solver-shutdown self) + (base/solver-shutdown self)) + + (define (solver-push self) + (base/solver-push self)) + + (define (solver-pop self [k 1]) + (base/solver-pop self k)) + + (define (solver-check self) + (base/solver-check self)) + + (define (solver-debug self) + (base/solver-debug self))]) + +(define (set-default-options server) + void) \ No newline at end of file diff --git a/test/all-rosette-tests.rkt b/test/all-rosette-tests.rkt index c0086f7b..73fe1397 100644 --- a/test/all-rosette-tests.rkt +++ b/test/all-rosette-tests.rkt @@ -6,6 +6,7 @@ rosette/solver/smt/boolector rosette/solver/smt/cvc5 rosette/solver/smt/bitwuzla + rosette/solver/smt/stp "config.rkt") (error-print-width default-error-print-width) @@ -76,21 +77,24 @@ (define (slow-tests) - (when (cvc4-available?) - (printf "===== Running CVC4 tests =====\n") - (run-tests-with-solver cvc4)) - - (when (boolector-available?) - (printf "===== Running Boolector tests =====\n") - (run-tests-with-solver boolector)) - - (when (cvc5-available?) - (printf "===== Running cvc5 tests =====\n") - (run-tests-with-solver cvc5)) - - (when (bitwuzla-available?) - (printf "===== Running bitwuzla tests =====\n") - (run-tests-with-solver bitwuzla)) + ; (when (cvc4-available?) + ; (printf "===== Running CVC4 tests =====\n") + ; (run-tests-with-solver cvc4)) + + ; (when (boolector-available?) + ; (printf "===== Running Boolector tests =====\n") + ; (run-tests-with-solver boolector)) + + ; (when (cvc5-available?) + ; (printf "===== Running cvc5 tests =====\n") + ; (run-tests-with-solver cvc5)) + + ; (when (bitwuzla-available?) + ; (printf "===== Running bitwuzla tests =====\n") + ; (run-tests-with-solver bitwuzla)) + (when (stp-available?) + (printf "===== Running stp tests =====\n") + (run-tests-with-solver stp)) ) (module+ test From cd7c0740b87332b8985ad4337ea337025e7dbd67 Mon Sep 17 00:00:00 2001 From: Vishal Canumalla Date: Thu, 30 Nov 2023 15:28:30 -0800 Subject: [PATCH 02/30] added yices2 --- test/all-rosette-tests.rkt | 29 ++++++++++++++++------------- test/base/bitvector.rkt | 7 +++++-- 2 files changed, 21 insertions(+), 15 deletions(-) diff --git a/test/all-rosette-tests.rkt b/test/all-rosette-tests.rkt index 73fe1397..14cad2b2 100644 --- a/test/all-rosette-tests.rkt +++ b/test/all-rosette-tests.rkt @@ -7,8 +7,8 @@ rosette/solver/smt/cvc5 rosette/solver/smt/bitwuzla rosette/solver/smt/stp + rosette/solver/smt/yices-smt2 "config.rkt") - (error-print-width default-error-print-width) @@ -77,24 +77,27 @@ (define (slow-tests) - ; (when (cvc4-available?) - ; (printf "===== Running CVC4 tests =====\n") - ; (run-tests-with-solver cvc4)) + (when (cvc4-available?) + (printf "===== Running CVC4 tests =====\n") + (run-tests-with-solver cvc4)) - ; (when (boolector-available?) - ; (printf "===== Running Boolector tests =====\n") - ; (run-tests-with-solver boolector)) + (when (boolector-available?) + (printf "===== Running Boolector tests =====\n") + (run-tests-with-solver boolector)) - ; (when (cvc5-available?) - ; (printf "===== Running cvc5 tests =====\n") - ; (run-tests-with-solver cvc5)) + (when (cvc5-available?) + (printf "===== Running cvc5 tests =====\n") + (run-tests-with-solver cvc5)) - ; (when (bitwuzla-available?) - ; (printf "===== Running bitwuzla tests =====\n") - ; (run-tests-with-solver bitwuzla)) + (when (bitwuzla-available?) + (printf "===== Running bitwuzla tests =====\n") + (run-tests-with-solver bitwuzla)) (when (stp-available?) (printf "===== Running stp tests =====\n") (run-tests-with-solver stp)) + (when (yices-smt2-available?) + (printf "===== Running yices-smt2 tests =====\n") + (run-tests-with-solver yices-smt2)) ) (module+ test diff --git a/test/base/bitvector.rkt b/test/base/bitvector.rkt index d8430091..f3d3d03e 100644 --- a/test/base/bitvector.rkt +++ b/test/base/bitvector.rkt @@ -1,12 +1,15 @@ #lang racket (require rackunit rackunit/text-ui racket/generator (rename-in rackunit [check-exn rackunit/check-exn]) - rosette/solver/solution + rosette/solver/solution + ; (only-in rosette solver-features current-solver) "solver.rkt" + ; rosette/solver/smt/yices-smt2 rosette/lib/roseunit rosette/solver/smt/boolector racket/fixnum rosette/base/core/term rosette/base/core/bool rosette/base/core/result + ; rosette/solver/smt/server (except-in rosette/base/core/bitvector bv) (only-in rosette/base/core/bitvector [bv @bv]) rosette/base/core/polymorphic rosette/base/core/merge @@ -26,7 +29,7 @@ (define maxval+1 (expt 2 (sub1 (bitvector-size BV)))) (define maxval (sub1 maxval+1)) (define (bv v [t BV]) (@bv v t)) - +; (output-smt "output-debug/") (define-syntax-rule (check-exn e ...) (begin (rackunit/check-exn e ...) From 5994ae286a584e3035be92e95dd14e0e1e81704d Mon Sep 17 00:00:00 2001 From: Vishal Canumalla Date: Tue, 5 Dec 2023 18:03:37 -0800 Subject: [PATCH 03/30] yices2 addition --- rosette/solver/smt/yices-smt2.rkt | 68 +++++++++++++++++++++++++++++++ test/base/bitvector.rkt | 4 -- 2 files changed, 68 insertions(+), 4 deletions(-) create mode 100644 rosette/solver/smt/yices-smt2.rkt diff --git a/rosette/solver/smt/yices-smt2.rkt b/rosette/solver/smt/yices-smt2.rkt new file mode 100644 index 00000000..484f5f0b --- /dev/null +++ b/rosette/solver/smt/yices-smt2.rkt @@ -0,0 +1,68 @@ +#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?) + +(define-runtime-path yices-smt2-path (build-path ".." ".." ".." "bin" "yices-smt2")) +(define yices-smt2-opts '("--incremental")) + +(define (yices-smt2-available?) + (not (false? (base/find-solver "yices-smt2" yices-smt2-path #f)))) +(define default-logic 'QF_BV) ;; YICES_2 needs a default logic set otherwise it will error +(define (make-yices-smt2 [solver #f] #:options [options (hash)] #:logic [logic default-logic] #:path [path #f]) + (define config + (cond + [(yices-smt2? solver) + (base/solver-config solver)] + [else + (define real-yices-smt2-path (base/find-solver "yices-smt2" yices-smt2-path path)) + (when (and (false? real-yices-smt2-path) (not (getenv "PLT_PKG_BUILD_SERVICE"))) + (error 'yices-smt2 "yices-smt2 binary is not available (expected to be at ~a); try passing the #:path argument to (yices-smt2)" (path->string (simplify-path yices-smt2-path)))) + (base/config options real-yices-smt2-path logic)])) + (yices-smt2 (server (base/config-path config) yices-smt2-opts (base/make-send-options config)) config '() '() '() (env) '())) + +(struct yices-smt2 base/solver () + #:property prop:solver-constructor make-yices-smt2 + #:methods gen:custom-write + [(define (write-proc self port mode) (fprintf port "#"))] + #:methods gen:solver + [ + (define (solver-features self) + '(qf_bv)) + + (define (solver-options self) + (base/solver-options self)) + + (define (solver-assert self bools) + (base/solver-assert self bools)) + + (define (solver-minimize self nums) + (base/solver-minimize self nums)) + + (define (solver-maximize self nums) + (base/solver-maximize self nums)) + + (define (solver-clear self) + (base/solver-clear self)) + + (define (solver-shutdown self) + (base/solver-shutdown self)) + + (define (solver-push self) + (base/solver-push self)) + + (define (solver-pop self [k 1]) + (base/solver-pop self k)) + + (define (solver-check self) + (base/solver-check self)) + + (define (solver-debug self) + (base/solver-debug self))]) + +(define (set-default-options server) + void) \ No newline at end of file diff --git a/test/base/bitvector.rkt b/test/base/bitvector.rkt index f3d3d03e..4a46d525 100644 --- a/test/base/bitvector.rkt +++ b/test/base/bitvector.rkt @@ -2,14 +2,11 @@ (require rackunit rackunit/text-ui racket/generator (rename-in rackunit [check-exn rackunit/check-exn]) rosette/solver/solution - ; (only-in rosette solver-features current-solver) "solver.rkt" - ; rosette/solver/smt/yices-smt2 rosette/lib/roseunit rosette/solver/smt/boolector racket/fixnum rosette/base/core/term rosette/base/core/bool rosette/base/core/result - ; rosette/solver/smt/server (except-in rosette/base/core/bitvector bv) (only-in rosette/base/core/bitvector [bv @bv]) rosette/base/core/polymorphic rosette/base/core/merge @@ -29,7 +26,6 @@ (define maxval+1 (expt 2 (sub1 (bitvector-size BV)))) (define maxval (sub1 maxval+1)) (define (bv v [t BV]) (@bv v t)) -; (output-smt "output-debug/") (define-syntax-rule (check-exn e ...) (begin (rackunit/check-exn e ...) From 82a345850e5e1c70b6d77abb9d4cc6939734aa3e Mon Sep 17 00:00:00 2001 From: Vishal Canumalla Date: Wed, 6 Dec 2023 18:27:47 -0800 Subject: [PATCH 04/30] workflow --- .github/workflows/tests.yml | 21 ++++++++++++++++++++- 1 file changed, 20 insertions(+), 1 deletion(-) diff --git a/.github/workflows/tests.yml b/.github/workflows/tests.yml index 735b631d..54d0ddb5 100644 --- a/.github/workflows/tests.yml +++ b/.github/workflows/tests.yml @@ -29,6 +29,7 @@ jobs: - name: Install solvers run: | mkdir bin && + wget $CVC4_URL -nv -O bin/cvc4 && chmod +x bin/cvc4 && wget $BOOLECTOR_URL -nv -O boolector.tar.gz && @@ -57,7 +58,25 @@ jobs: ninja && popd && popd && - cp bitwuzla/build/src/main/bitwuzla bin/ + cp bitwuzla/build/src/main/bitwuzla bin/ && + + sudo apt-get install -y git cmake bison flex libboost-all-dev python2 perl && + git clone https://github.com/stp/stp && + pushd stp && + git submodule init && git submodule update && + ./scripts/deps/setup-gtest.sh && + ./scripts/deps/setup-outputcheck.sh && + ./scripts/deps/setup-cms.sh && + ./scripts/deps/setup-minisat.sh && + mkdir build && + cd build && + cmake .. && + cmake --build . && + cp stp bin/ && + add-apt-repository -y ppa:sri-csl/formal-methods && + apt-get update && + apt-get install -y yices2 + - name: Install Rosette run: raco pkg install --auto --name rosette - name: Compile Rosette tests From ad210a6a2582bcadad8705e52a0daa914e34ef80 Mon Sep 17 00:00:00 2001 From: Vishal Canumalla Date: Wed, 6 Dec 2023 18:28:53 -0800 Subject: [PATCH 05/30] add some sudos --- .github/workflows/tests.yml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/.github/workflows/tests.yml b/.github/workflows/tests.yml index 54d0ddb5..73da38f8 100644 --- a/.github/workflows/tests.yml +++ b/.github/workflows/tests.yml @@ -73,9 +73,9 @@ jobs: cmake .. && cmake --build . && cp stp bin/ && - add-apt-repository -y ppa:sri-csl/formal-methods && - apt-get update && - apt-get install -y yices2 + sudo add-apt-repository -y ppa:sri-csl/formal-methods && + sudo apt-get update && + sudo apt-get install -y yices2 - name: Install Rosette run: raco pkg install --auto --name rosette From 3e69e044bc09453e60f1520ce6445755cc8c9923 Mon Sep 17 00:00:00 2001 From: Vishal Canumalla Date: Wed, 6 Dec 2023 18:32:59 -0800 Subject: [PATCH 06/30] delete some random whitespace --- .github/workflows/tests.yml | 3 --- 1 file changed, 3 deletions(-) diff --git a/.github/workflows/tests.yml b/.github/workflows/tests.yml index 73da38f8..bd89e86f 100644 --- a/.github/workflows/tests.yml +++ b/.github/workflows/tests.yml @@ -29,7 +29,6 @@ jobs: - name: Install solvers run: | mkdir bin && - wget $CVC4_URL -nv -O bin/cvc4 && chmod +x bin/cvc4 && wget $BOOLECTOR_URL -nv -O boolector.tar.gz && @@ -59,7 +58,6 @@ jobs: popd && popd && cp bitwuzla/build/src/main/bitwuzla bin/ && - sudo apt-get install -y git cmake bison flex libboost-all-dev python2 perl && git clone https://github.com/stp/stp && pushd stp && @@ -76,7 +74,6 @@ jobs: sudo add-apt-repository -y ppa:sri-csl/formal-methods && sudo apt-get update && sudo apt-get install -y yices2 - - name: Install Rosette run: raco pkg install --auto --name rosette - name: Compile Rosette tests From 7aeac356185e55ac3f13c345fd6f6ca0ab8cf218 Mon Sep 17 00:00:00 2001 From: Vishal Canumalla Date: Wed, 6 Dec 2023 18:36:27 -0800 Subject: [PATCH 07/30] end files in newline --- rosette/solver/smt/stp.rkt | 3 ++- rosette/solver/smt/yices-smt2.rkt | 3 ++- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/rosette/solver/smt/stp.rkt b/rosette/solver/smt/stp.rkt index f98ac5ad..3377561e 100644 --- a/rosette/solver/smt/stp.rkt +++ b/rosette/solver/smt/stp.rkt @@ -65,4 +65,5 @@ (base/solver-debug self))]) (define (set-default-options server) - void) \ No newline at end of file + void) + \ No newline at end of file diff --git a/rosette/solver/smt/yices-smt2.rkt b/rosette/solver/smt/yices-smt2.rkt index 484f5f0b..d5be70c0 100644 --- a/rosette/solver/smt/yices-smt2.rkt +++ b/rosette/solver/smt/yices-smt2.rkt @@ -65,4 +65,5 @@ (base/solver-debug self))]) (define (set-default-options server) - void) \ No newline at end of file + void) + \ No newline at end of file From 507a9a74b600053b236e0d0b36e16ee8eeadc8b5 Mon Sep 17 00:00:00 2001 From: Vishal Canumalla Date: Wed, 6 Dec 2023 18:45:01 -0800 Subject: [PATCH 08/30] fix added whitespace --- test/base/bitvector.rkt | 1 + 1 file changed, 1 insertion(+) diff --git a/test/base/bitvector.rkt b/test/base/bitvector.rkt index 4a46d525..07331c61 100644 --- a/test/base/bitvector.rkt +++ b/test/base/bitvector.rkt @@ -26,6 +26,7 @@ (define maxval+1 (expt 2 (sub1 (bitvector-size BV)))) (define maxval (sub1 maxval+1)) (define (bv v [t BV]) (@bv v t)) + (define-syntax-rule (check-exn e ...) (begin (rackunit/check-exn e ...) From 1c531f351d2e02fae79aab07b64a18f9dc9e61f2 Mon Sep 17 00:00:00 2001 From: Vishal Canumalla Date: Wed, 6 Dec 2023 19:23:04 -0800 Subject: [PATCH 09/30] fix workflows test --- .github/workflows/tests.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/tests.yml b/.github/workflows/tests.yml index bd89e86f..37e28397 100644 --- a/.github/workflows/tests.yml +++ b/.github/workflows/tests.yml @@ -70,7 +70,7 @@ jobs: cd build && cmake .. && cmake --build . && - cp stp bin/ && + cp stp bin/stp && sudo add-apt-repository -y ppa:sri-csl/formal-methods && sudo apt-get update && sudo apt-get install -y yices2 From 47450f07648c2183d097c7074c37cf7b4d1dc0b5 Mon Sep 17 00:00:00 2001 From: Vishal Canumalla Date: Wed, 6 Dec 2023 19:30:11 -0800 Subject: [PATCH 10/30] fix path --- .github/workflows/tests.yml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/.github/workflows/tests.yml b/.github/workflows/tests.yml index 37e28397..0c411152 100644 --- a/.github/workflows/tests.yml +++ b/.github/workflows/tests.yml @@ -70,6 +70,8 @@ jobs: cd build && cmake .. && cmake --build . && + popd && + popd && cp stp bin/stp && sudo add-apt-repository -y ppa:sri-csl/formal-methods && sudo apt-get update && From eab000174aa8df904fe388cf2fb0674f61d0cd10 Mon Sep 17 00:00:00 2001 From: Vishal Canumalla Date: Wed, 6 Dec 2023 19:30:31 -0800 Subject: [PATCH 11/30] bin should be in right folder now --- .github/workflows/tests.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/tests.yml b/.github/workflows/tests.yml index 0c411152..5656ea27 100644 --- a/.github/workflows/tests.yml +++ b/.github/workflows/tests.yml @@ -67,12 +67,12 @@ jobs: ./scripts/deps/setup-cms.sh && ./scripts/deps/setup-minisat.sh && mkdir build && - cd build && + pushd build && cmake .. && cmake --build . && popd && popd && - cp stp bin/stp && + cp stp/build/stp bin/stp && sudo add-apt-repository -y ppa:sri-csl/formal-methods && sudo apt-get update && sudo apt-get install -y yices2 From 53fd00a5c5387d06052e1707406b75fcff4932be Mon Sep 17 00:00:00 2001 From: Vishal Canumalla Date: Thu, 7 Dec 2023 11:59:15 -0800 Subject: [PATCH 12/30] debugging for stp failure --- test/all-rosette-tests.rkt | 29 +++++++++++++++-------------- 1 file changed, 15 insertions(+), 14 deletions(-) diff --git a/test/all-rosette-tests.rkt b/test/all-rosette-tests.rkt index 14cad2b2..5ae1aefb 100644 --- a/test/all-rosette-tests.rkt +++ b/test/all-rosette-tests.rkt @@ -77,21 +77,21 @@ (define (slow-tests) - (when (cvc4-available?) - (printf "===== Running CVC4 tests =====\n") - (run-tests-with-solver cvc4)) + ; (when (cvc4-available?) + ; (printf "===== Running CVC4 tests =====\n") + ; (run-tests-with-solver cvc4)) - (when (boolector-available?) - (printf "===== Running Boolector tests =====\n") - (run-tests-with-solver boolector)) + ; (when (boolector-available?) + ; (printf "===== Running Boolector tests =====\n") + ; (run-tests-with-solver boolector)) - (when (cvc5-available?) - (printf "===== Running cvc5 tests =====\n") - (run-tests-with-solver cvc5)) + ; (when (cvc5-available?) + ; (printf "===== Running cvc5 tests =====\n") + ; (run-tests-with-solver cvc5)) - (when (bitwuzla-available?) - (printf "===== Running bitwuzla tests =====\n") - (run-tests-with-solver bitwuzla)) + ; (when (bitwuzla-available?) + ; (printf "===== Running bitwuzla tests =====\n") + ; (run-tests-with-solver bitwuzla)) (when (stp-available?) (printf "===== Running stp tests =====\n") (run-tests-with-solver stp)) @@ -101,5 +101,6 @@ ) (module+ test - (fast-tests) - (slow-tests)) + ; (fast-tests) + (slow-tests) + ) From 3f01d861b97bec7e018a95191497f70efaebf0ef Mon Sep 17 00:00:00 2001 From: Vishal Canumalla Date: Thu, 7 Dec 2023 14:02:13 -0800 Subject: [PATCH 13/30] some debugging info and output --- rosette/solver/smt/stp.rkt | 2 +- test/all-rosette-tests.rkt | 70 +++++++++++++++++++------------------- test/base/push-pop.rkt | 2 +- 3 files changed, 37 insertions(+), 37 deletions(-) diff --git a/rosette/solver/smt/stp.rkt b/rosette/solver/smt/stp.rkt index 3377561e..59c54e1e 100644 --- a/rosette/solver/smt/stp.rkt +++ b/rosette/solver/smt/stp.rkt @@ -8,7 +8,7 @@ (provide (rename-out [make-stp stp]) stp? stp-available?) (define-runtime-path stp-path (build-path ".." ".." ".." "bin" "stp")) -(define stp-opts '()) +(define stp-opts '("--SMTLIB2" "-p")) (define (stp-available?) (not (false? (base/find-solver "stp" stp-path #f)))) diff --git a/test/all-rosette-tests.rkt b/test/all-rosette-tests.rkt index 5ae1aefb..c95d3257 100644 --- a/test/all-rosette-tests.rkt +++ b/test/all-rosette-tests.rkt @@ -20,39 +20,39 @@ (require-all-tests - "base/type.rkt" - "base/term.rkt" - "base/bool.rkt" - "base/merge.rkt" - "base/store.rkt" - "base/vc.rkt" - "base/eval-guarded.rkt" - "base/list.rkt" - "base/vector.rkt" - "base/bvseq.rkt" - "base/forall.rkt" - "base/bitvector.rkt" - "base/bvlib.rkt" - "base/equality.rkt" - "base/uninterpreted.rkt" - "base/real.rkt" - "base/quantified.rkt" - "base/finitize.rkt" - "base/distinct.rkt" - "base/generics.rkt" +; "base/type.rkt" +; "base/term.rkt" +; "base/bool.rkt" +; "base/merge.rkt" +; "base/store.rkt" +; "base/vc.rkt" +; "base/eval-guarded.rkt" +; "base/list.rkt" +; "base/vector.rkt" +; "base/bvseq.rkt" +; "base/forall.rkt" +; "base/bitvector.rkt" +; "base/bvlib.rkt" +; "base/equality.rkt" +; "base/uninterpreted.rkt" +; "base/real.rkt" +; "base/quantified.rkt" +; "base/finitize.rkt" +; "base/distinct.rkt" +; "base/generics.rkt" "base/push-pop.rkt" - "base/optimize-order.rkt" - "base/reflect.rkt" - "base/decode.rkt" - "query/solve.rkt" - "query/verify.rkt" - "query/synthesize.rkt" - "query/solve+.rkt" - "query/synthax.rkt" - "query/grammar.rkt" - "query/optimize.rkt" - "lib/destruct.rkt" - "profile/test.rkt" +; "base/optimize-order.rkt" +; "base/reflect.rkt" +; "base/decode.rkt" +; "query/solve.rkt" +; "query/verify.rkt" +; "query/synthesize.rkt" +; "query/solve+.rkt" +; "query/synthax.rkt" +; "query/grammar.rkt" +; "query/optimize.rkt" +; "lib/destruct.rkt" +; "profile/test.rkt" "trace/test.rkt") @@ -95,9 +95,9 @@ (when (stp-available?) (printf "===== Running stp tests =====\n") (run-tests-with-solver stp)) - (when (yices-smt2-available?) - (printf "===== Running yices-smt2 tests =====\n") - (run-tests-with-solver yices-smt2)) + ; (when (yices-smt2-available?) + ; (printf "===== Running yices-smt2 tests =====\n") + ; (run-tests-with-solver yices-smt2)) ) (module+ test diff --git a/test/base/push-pop.rkt b/test/base/push-pop.rkt index 30d201e9..3d33e4df 100644 --- a/test/base/push-pop.rkt +++ b/test/base/push-pop.rkt @@ -14,7 +14,7 @@ (define push-pop-tests (test-suite+ "Tests for the push / pop interface." #:features '(qf_bv) - + (output-smt "push-pop-tests.smt2") (define solver (current-solver)) (check-exn exn:fail? (thunk (solver-pop solver))) From 3a7fc3c6eba1a167befa996ad27d7e4ee8387713 Mon Sep 17 00:00:00 2001 From: Vishal Canumalla Date: Thu, 7 Dec 2023 16:59:49 -0800 Subject: [PATCH 14/30] is yices2 working --- test/all-rosette-tests.rkt | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/test/all-rosette-tests.rkt b/test/all-rosette-tests.rkt index c95d3257..1d7fa86e 100644 --- a/test/all-rosette-tests.rkt +++ b/test/all-rosette-tests.rkt @@ -31,7 +31,7 @@ ; "base/vector.rkt" ; "base/bvseq.rkt" ; "base/forall.rkt" -; "base/bitvector.rkt" + "base/bitvector.rkt" ; "base/bvlib.rkt" ; "base/equality.rkt" ; "base/uninterpreted.rkt" @@ -40,7 +40,7 @@ ; "base/finitize.rkt" ; "base/distinct.rkt" ; "base/generics.rkt" - "base/push-pop.rkt" +; "base/push-pop.rkt" ; "base/optimize-order.rkt" ; "base/reflect.rkt" ; "base/decode.rkt" @@ -95,9 +95,9 @@ (when (stp-available?) (printf "===== Running stp tests =====\n") (run-tests-with-solver stp)) - ; (when (yices-smt2-available?) - ; (printf "===== Running yices-smt2 tests =====\n") - ; (run-tests-with-solver yices-smt2)) + (when (yices-smt2-available?) + (printf "===== Running yices-smt2 tests =====\n") + (run-tests-with-solver yices-smt2)) ) (module+ test From becbfab2b7b4f889f5980b25d9545dddb99a7263 Mon Sep 17 00:00:00 2001 From: Gus Smith Date: Tue, 12 Dec 2023 10:38:37 -0800 Subject: [PATCH 15/30] Skip `ASSERT` lines during `check-sat` for STP --- rosette/solver/smt/stp.rkt | 21 +++++++++++++++++++-- 1 file changed, 19 insertions(+), 2 deletions(-) diff --git a/rosette/solver/smt/stp.rkt b/rosette/solver/smt/stp.rkt index 59c54e1e..be90e65e 100644 --- a/rosette/solver/smt/stp.rkt +++ b/rosette/solver/smt/stp.rkt @@ -58,8 +58,25 @@ (define (solver-pop self [k 1]) (base/solver-pop self k)) - (define (solver-check self) - (base/solver-check self)) + +(define (solver-check self) + (define (read-solution server env #:unsat-core? [unsat-core? #f]) + ;;; Ignore the ASSERT lines, if present. + (server-read server + ; Peek at the first five characters, which should always be present. They'll either be "unsat" or + ; "ASSER", the latter of which is the first five characters of "ASSERT". + (let loop () + (if (and (not (equal? (peek-string 3 0) "sat")) + (not (equal? (peek-string 5 0) "unsat"))) + (begin + (when (not (string-prefix? (read-line) "ASSERT")) + (error "Expected extra line to start with ASSERT")) + (loop)) + (void)))) + (base/read-solution server env #:unsat-core? unsat-core?)) + + (base/solver-check self read-solution) + ) (define (solver-debug self) (base/solver-debug self))]) From 5d5cfae067e036a270b6b8608eb91d513c923ad7 Mon Sep 17 00:00:00 2001 From: Gus Smith Date: Tue, 12 Dec 2023 11:00:59 -0800 Subject: [PATCH 16/30] Revert "Skip `ASSERT` lines during `check-sat` for STP" This reverts commit becbfab2b7b4f889f5980b25d9545dddb99a7263. --- rosette/solver/smt/stp.rkt | 21 ++------------------- 1 file changed, 2 insertions(+), 19 deletions(-) diff --git a/rosette/solver/smt/stp.rkt b/rosette/solver/smt/stp.rkt index be90e65e..59c54e1e 100644 --- a/rosette/solver/smt/stp.rkt +++ b/rosette/solver/smt/stp.rkt @@ -58,25 +58,8 @@ (define (solver-pop self [k 1]) (base/solver-pop self k)) - -(define (solver-check self) - (define (read-solution server env #:unsat-core? [unsat-core? #f]) - ;;; Ignore the ASSERT lines, if present. - (server-read server - ; Peek at the first five characters, which should always be present. They'll either be "unsat" or - ; "ASSER", the latter of which is the first five characters of "ASSERT". - (let loop () - (if (and (not (equal? (peek-string 3 0) "sat")) - (not (equal? (peek-string 5 0) "unsat"))) - (begin - (when (not (string-prefix? (read-line) "ASSERT")) - (error "Expected extra line to start with ASSERT")) - (loop)) - (void)))) - (base/read-solution server env #:unsat-core? unsat-core?)) - - (base/solver-check self read-solution) - ) + (define (solver-check self) + (base/solver-check self)) (define (solver-debug self) (base/solver-debug self))]) From f1ad2907e55125120fe1e76a9a4b1ff309043cc6 Mon Sep 17 00:00:00 2001 From: Gus Smith Date: Tue, 12 Dec 2023 12:49:58 -0800 Subject: [PATCH 17/30] don't need the -p flag 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. --- rosette/solver/smt/stp.rkt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/rosette/solver/smt/stp.rkt b/rosette/solver/smt/stp.rkt index 59c54e1e..2cb91529 100644 --- a/rosette/solver/smt/stp.rkt +++ b/rosette/solver/smt/stp.rkt @@ -8,7 +8,7 @@ (provide (rename-out [make-stp stp]) stp? stp-available?) (define-runtime-path stp-path (build-path ".." ".." ".." "bin" "stp")) -(define stp-opts '("--SMTLIB2" "-p")) +(define stp-opts '("--SMTLIB2")) (define (stp-available?) (not (false? (base/find-solver "stp" stp-path #f)))) From c405c6fc0b1f24c3381df264f279cffbbeb08768 Mon Sep 17 00:00:00 2001 From: Gus Smith Date: Wed, 13 Dec 2023 08:24:07 -0800 Subject: [PATCH 18/30] Undo unnecessary changes --- test/all-rosette-tests.rkt | 96 +++++++++++++++++++------------------- test/base/bitvector.rkt | 2 +- test/base/push-pop.rkt | 2 +- 3 files changed, 51 insertions(+), 49 deletions(-) diff --git a/test/all-rosette-tests.rkt b/test/all-rosette-tests.rkt index 1d7fa86e..33078b84 100644 --- a/test/all-rosette-tests.rkt +++ b/test/all-rosette-tests.rkt @@ -9,6 +9,7 @@ rosette/solver/smt/stp rosette/solver/smt/yices-smt2 "config.rkt") + (error-print-width default-error-print-width) @@ -20,39 +21,39 @@ (require-all-tests -; "base/type.rkt" -; "base/term.rkt" -; "base/bool.rkt" -; "base/merge.rkt" -; "base/store.rkt" -; "base/vc.rkt" -; "base/eval-guarded.rkt" -; "base/list.rkt" -; "base/vector.rkt" -; "base/bvseq.rkt" -; "base/forall.rkt" + "base/type.rkt" + "base/term.rkt" + "base/bool.rkt" + "base/merge.rkt" + "base/store.rkt" + "base/vc.rkt" + "base/eval-guarded.rkt" + "base/list.rkt" + "base/vector.rkt" + "base/bvseq.rkt" + "base/forall.rkt" "base/bitvector.rkt" -; "base/bvlib.rkt" -; "base/equality.rkt" -; "base/uninterpreted.rkt" -; "base/real.rkt" -; "base/quantified.rkt" -; "base/finitize.rkt" -; "base/distinct.rkt" -; "base/generics.rkt" -; "base/push-pop.rkt" -; "base/optimize-order.rkt" -; "base/reflect.rkt" -; "base/decode.rkt" -; "query/solve.rkt" -; "query/verify.rkt" -; "query/synthesize.rkt" -; "query/solve+.rkt" -; "query/synthax.rkt" -; "query/grammar.rkt" -; "query/optimize.rkt" -; "lib/destruct.rkt" -; "profile/test.rkt" + "base/bvlib.rkt" + "base/equality.rkt" + "base/uninterpreted.rkt" + "base/real.rkt" + "base/quantified.rkt" + "base/finitize.rkt" + "base/distinct.rkt" + "base/generics.rkt" + "base/push-pop.rkt" + "base/optimize-order.rkt" + "base/reflect.rkt" + "base/decode.rkt" + "query/solve.rkt" + "query/verify.rkt" + "query/synthesize.rkt" + "query/solve+.rkt" + "query/synthax.rkt" + "query/grammar.rkt" + "query/optimize.rkt" + "lib/destruct.rkt" + "profile/test.rkt" "trace/test.rkt") @@ -77,30 +78,31 @@ (define (slow-tests) - ; (when (cvc4-available?) - ; (printf "===== Running CVC4 tests =====\n") - ; (run-tests-with-solver cvc4)) + (when (cvc4-available?) + (printf "===== Running CVC4 tests =====\n") + (run-tests-with-solver cvc4)) + + (when (boolector-available?) + (printf "===== Running Boolector tests =====\n") + (run-tests-with-solver boolector)) - ; (when (boolector-available?) - ; (printf "===== Running Boolector tests =====\n") - ; (run-tests-with-solver boolector)) + (when (cvc5-available?) + (printf "===== Running cvc5 tests =====\n") + (run-tests-with-solver cvc5)) - ; (when (cvc5-available?) - ; (printf "===== Running cvc5 tests =====\n") - ; (run-tests-with-solver cvc5)) + (when (bitwuzla-available?) + (printf "===== Running bitwuzla tests =====\n") + (run-tests-with-solver bitwuzla)) - ; (when (bitwuzla-available?) - ; (printf "===== Running bitwuzla tests =====\n") - ; (run-tests-with-solver bitwuzla)) (when (stp-available?) (printf "===== Running stp tests =====\n") (run-tests-with-solver stp)) + (when (yices-smt2-available?) (printf "===== Running yices-smt2 tests =====\n") (run-tests-with-solver yices-smt2)) ) (module+ test - ; (fast-tests) - (slow-tests) - ) + (fast-tests) + (slow-tests)) diff --git a/test/base/bitvector.rkt b/test/base/bitvector.rkt index 07331c61..d8430091 100644 --- a/test/base/bitvector.rkt +++ b/test/base/bitvector.rkt @@ -1,7 +1,7 @@ #lang racket (require rackunit rackunit/text-ui racket/generator (rename-in rackunit [check-exn rackunit/check-exn]) - rosette/solver/solution + rosette/solver/solution rosette/lib/roseunit rosette/solver/smt/boolector racket/fixnum rosette/base/core/term diff --git a/test/base/push-pop.rkt b/test/base/push-pop.rkt index 3d33e4df..30d201e9 100644 --- a/test/base/push-pop.rkt +++ b/test/base/push-pop.rkt @@ -14,7 +14,7 @@ (define push-pop-tests (test-suite+ "Tests for the push / pop interface." #:features '(qf_bv) - (output-smt "push-pop-tests.smt2") + (define solver (current-solver)) (check-exn exn:fail? (thunk (solver-pop solver))) From a486654d380c3fde0ac88d1f3259dc8a61a1c793 Mon Sep 17 00:00:00 2001 From: Gus Smith Date: Wed, 13 Dec 2023 08:47:54 -0800 Subject: [PATCH 19/30] Convert new tests.yml code to match existing style --- .github/workflows/tests.yml | 20 +++++++++++++++----- 1 file changed, 15 insertions(+), 5 deletions(-) diff --git a/.github/workflows/tests.yml b/.github/workflows/tests.yml index 5656ea27..463d7453 100644 --- a/.github/workflows/tests.yml +++ b/.github/workflows/tests.yml @@ -7,6 +7,8 @@ env: BOOLECTOR_URL: "https://github.com/Boolector/boolector/archive/3.2.1.tar.gz" CVC5_URL: "https://github.com/cvc5/cvc5/releases/download/cvc5-1.0.7/cvc5-Linux" BITWUZLA_URL: "https://github.com/bitwuzla/bitwuzla/archive/93a3d930f622b4cef0063215e63b7c3bd10bd663.tar.gz" + STP_URL: "https://github.com/stp/stp/archive/0510509a85b6823278211891cbb274022340fa5c.tar.gz" + YICES2_URL: "https://github.com/SRI-CSL/yices2/archive/e27cf308cffb0ecc6cc7165c10e81ca65bc303b3.tar.gz" jobs: test: @@ -59,9 +61,10 @@ jobs: popd && cp bitwuzla/build/src/main/bitwuzla bin/ && sudo apt-get install -y git cmake bison flex libboost-all-dev python2 perl && - git clone https://github.com/stp/stp && + wget $STP_URL -nv -O stp.tar.gz && + mkdir stp && + tar xzf stp.tar.gz -C stp --strip-components=1 && pushd stp && - git submodule init && git submodule update && ./scripts/deps/setup-gtest.sh && ./scripts/deps/setup-outputcheck.sh && ./scripts/deps/setup-cms.sh && @@ -73,9 +76,16 @@ jobs: popd && popd && cp stp/build/stp bin/stp && - sudo add-apt-repository -y ppa:sri-csl/formal-methods && - sudo apt-get update && - sudo apt-get install -y yices2 + sudo apt-get install -y gperf && + wget $YICES2_URL -nv -O yices2.tar.gz && + mkdir yices2 && + tar xvf yices2.tar.gz -C yices2 --strip-components=1 && + pushd yices2 && + autoconf && + ./configure && + make && + popd && + cp yices2/build/x86_64-pc-linux-gnu-release/bin/yices_smt2 bin/yices_smt2 - name: Install Rosette run: raco pkg install --auto --name rosette - name: Compile Rosette tests From 1f8e33a13b401f3fa9e4bf22256cd7b4e2e535ee Mon Sep 17 00:00:00 2001 From: Gus Smith Date: Wed, 13 Dec 2023 11:33:46 -0800 Subject: [PATCH 20/30] Add documentation --- .../datatypes/solvers+solutions.scrbl | 136 ++++++++++++++++++ 1 file changed, 136 insertions(+) diff --git a/rosette/guide/scribble/datatypes/solvers+solutions.scrbl b/rosette/guide/scribble/datatypes/solvers+solutions.scrbl index c1cee777..3e679c91 100644 --- a/rosette/guide/scribble/datatypes/solvers+solutions.scrbl +++ b/rosette/guide/scribble/datatypes/solvers+solutions.scrbl @@ -279,6 +279,142 @@ Returns true if the Boolector solver is available for use (i.e., Rosette can loc If this returns @racket[#f], @racket[(boolector)] will not succeed without its optional @racket[path] argument.} +@subsection{Bitwuzla} + +@defmodule[rosette/solver/smt/bitwuzla #:no-declare] + +@defproc*[([(bitwuzla [#:path path (or/c path-string? #f) #f] + [#:logic logic (or/c symbol? #f) #f] + [#:options options (hash/c symbol? any/c) (hash)]) solver?] + [(bitwuzla? [v any/c]) boolean?])]{ + +Returns a @racket[solver?] wrapper for the @hyperlink["https://bitwuzla.github.io/"]{Bitwuzla} solver. + +To use this solver, download prebuilt Bitwuzla or build it yourself, +and ensure the executable is on your @tt{PATH} or pass the path to the +executable as the optional @racket[path] argument. +Rosette currently tests Bitwuzla at commit +@tt{93a3d930f622b4cef0063215e63b7c3bd10bd663}. + +The optional @racket[logic] argument specifies an SMT logic for the solver to use (e.g., @racket['QF_BV]). +Specifying a logic can improve solving performance, but Rosette makes no effort to check that +emitted constraints fall within the chosen logic. The default is @racket[#f], +which uses Bitwuzla's default logic. + +The @racket[options] argument provides additional options that are sent to Bitwuzla +via the @tt{set-option} SMT command. +For example, setting @racket[options] to @racket[(hash ':seed 5)] +will send the command @tt{(set-option :seed 5)} to Bitwuzla prior to solving. +} + +@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 +without its optional @racket[path] argument.} + +@subsection{CVC5} + +@defmodule[rosette/solver/smt/cvc5 #:no-declare] + +@defproc*[([(cvc5 [#:path path (or/c path-string? #f) #f] + [#:logic logic (or/c symbol? #f) #f] + [#:options options (hash/c symbol? any/c) (hash)]) solver?] + [(cvc5? [v any/c]) boolean?])]{ + +Returns a @racket[solver?] wrapper for the @hyperlink["https://cvc5.github.io/"]{CVC5} solver. + +To use this solver, download prebuilt CVC5 or build it yourself, +and ensure the executable is on your @tt{PATH} or pass the path to the +executable as the optional @racket[path] argument. +Rosette currently tests CVC5 at version 1.0.7. + +The optional @racket[logic] argument specifies an SMT logic for the solver to use (e.g., @racket['QF_BV]). +Specifying a logic can improve solving performance, but Rosette makes no effort to check that +emitted constraints fall within the chosen logic. The default is @racket[#f], +which uses CVC5's default logic. + +The @racket[options] argument provides additional options that are sent to CVC5 +via the @tt{set-option} SMT command. +For example, setting @racket[options] to @racket[(hash ':seed 5)] +will send the command @tt{(set-option :seed 5)} to CVC5 prior to solving. +} + +@defproc[(cvc5-available?) boolean?]{ +Returns true if the CVC5 solver is available for use (i.e., Rosette can locate a @tt{cvc5} binary). +If this returns @racket[#f], @racket[(cvc5)] will not succeed +without its optional @racket[path] argument.} + +@subsection{STP} + +@defmodule[rosette/solver/smt/stp #:no-declare] + +@defproc*[([(stp [#:path path (or/c path-string? #f) #f] + [#:logic logic (or/c symbol? #f) #f] + [#:options options (hash/c symbol? any/c) (hash)]) solver?] + [(stp? [v any/c]) boolean?])]{ + +Returns a @racket[solver?] wrapper for the @hyperlink["https://stp.github.io/"]{STP} solver. + +To use this solver, download prebuilt STP or build it yourself, +and ensure the executable is on your @tt{PATH} or pass the path to the +executable as the optional @racket[path] argument. +Rosette currently tests STP at commit +@tt{0510509a85b6823278211891cbb274022340fa5c}. +Note that as of December 2023, the STP version on Mac Homebrew is too old to be +supported by Rosette. + +The optional @racket[logic] argument specifies an SMT logic for the solver to use (e.g., @racket['QF_BV]). +Specifying a logic can improve solving performance, but Rosette makes no effort to check that +emitted constraints fall within the chosen logic. The default is @racket[#f], +which uses STP's default logic. + +The @racket[options] argument provides additional options that are sent to STP +via the @tt{set-option} SMT command. +For example, setting @racket[options] to @racket[(hash ':seed 5)] +will send the command @tt{(set-option :seed 5)} to STP prior to solving. +} + +@defproc[(stp-available?) boolean?]{ +Returns true if the STP solver is available for use (i.e., Rosette can locate a @tt{stp} binary). +If this returns @racket[#f], @racket[(stp)] will not succeed +without its optional @racket[path] argument.} + +@subsection{Yices2} + +@defmodule[rosette/solver/smt/yices-smt2 #:no-declare] + +@defproc*[([(yices-smt2 [#:path path (or/c path-string? #f) #f] + [#:logic logic (or/c symbol? #f) 'QF_BV] + [#:options options (hash/c symbol? any/c) (hash)]) solver?] + [(yices-smt2? [v any/c]) boolean?])]{ + +Returns a @racket[solver?] wrapper for the @hyperlink["https://yices.csl.sri.com/"]{Yices2} solver. + +To use this solver, download prebuilt Yices2 or build it yourself, +and ensure the executable is on your @tt{PATH} or pass the path to the +executable as the optional @racket[path] argument. +Rosette specifically uses the @tt{yices_smt2} executable, which is the Yices2 +solver with SMTLIB2 as its frontend. +Rosette currently tests Yices2 at commit +@tt{e27cf308cffb0ecc6cc7165c10e81ca65bc303b3}. + +The optional @racket[logic] argument specifies an SMT logic for the solver to use (e.g., @racket['QF_BV]). +Specifying a logic can improve solving performance, but Rosette makes no effort to check that +emitted constraints fall within the chosen logic. Yices2 expects a logic to be +set; Rosette defaults to @racket['QF_BV]. + +The @racket[options] argument provides additional options that are sent to Yices2 +via the @tt{set-option} SMT command. +For example, setting @racket[options] to @racket[(hash ':seed 5)] +will send the command @tt{(set-option :seed 5)} to Yices2 prior to solving. +} + +@defproc[(yices-smt2-available?) boolean?]{ +Returns true if the Yices2 solver is available for use (i.e., Rosette can locate a @tt{yices_smt2} binary). +If this returns @racket[#f], @racket[(yices-smt2)] will not succeed +without its optional @racket[path] argument.} + + @section{Solutions} A solution to a set of formulas may be satisfiable (@racket[sat?]), unsatisfiable (@racket[unsat?]), From 4d364f28127863ed43e847899f5587d6d3117a95 Mon Sep 17 00:00:00 2001 From: Gus Smith Date: Thu, 14 Dec 2023 10:35:38 -0800 Subject: [PATCH 21/30] Rename to Yices and attempt to use `yices` binary --- .../datatypes/solvers+solutions.scrbl | 19 +++-- rosette/solver/smt/yices-smt2.rkt | 69 ------------------- rosette/solver/smt/yices.rkt | 69 +++++++++++++++++++ 3 files changed, 78 insertions(+), 79 deletions(-) delete mode 100644 rosette/solver/smt/yices-smt2.rkt create mode 100644 rosette/solver/smt/yices.rkt diff --git a/rosette/guide/scribble/datatypes/solvers+solutions.scrbl b/rosette/guide/scribble/datatypes/solvers+solutions.scrbl index 3e679c91..121175d1 100644 --- a/rosette/guide/scribble/datatypes/solvers+solutions.scrbl +++ b/rosette/guide/scribble/datatypes/solvers+solutions.scrbl @@ -381,20 +381,19 @@ without its optional @racket[path] argument.} @subsection{Yices2} -@defmodule[rosette/solver/smt/yices-smt2 #:no-declare] +@defmodule[rosette/solver/smt/yices #:no-declare] -@defproc*[([(yices-smt2 [#:path path (or/c path-string? #f) #f] - [#:logic logic (or/c symbol? #f) 'QF_BV] - [#:options options (hash/c symbol? any/c) (hash)]) solver?] - [(yices-smt2? [v any/c]) boolean?])]{ +@defproc*[([(yices [#:path path (or/c path-string? #f) #f] + [#:logic logic (or/c symbol? #f) 'QF_BV] + [#:options options (hash/c symbol? any/c) (hash)]) solver?] + [(yices? [v any/c]) boolean?])]{ Returns a @racket[solver?] wrapper for the @hyperlink["https://yices.csl.sri.com/"]{Yices2} solver. To use this solver, download prebuilt Yices2 or build it yourself, and ensure the executable is on your @tt{PATH} or pass the path to the executable as the optional @racket[path] argument. -Rosette specifically uses the @tt{yices_smt2} executable, which is the Yices2 -solver with SMTLIB2 as its frontend. +Rosette specifically uses the @tt{yices} executable. Rosette currently tests Yices2 at commit @tt{e27cf308cffb0ecc6cc7165c10e81ca65bc303b3}. @@ -409,9 +408,9 @@ For example, setting @racket[options] to @racket[(hash ':seed 5)] will send the command @tt{(set-option :seed 5)} to Yices2 prior to solving. } -@defproc[(yices-smt2-available?) boolean?]{ -Returns true if the Yices2 solver is available for use (i.e., Rosette can locate a @tt{yices_smt2} binary). -If this returns @racket[#f], @racket[(yices-smt2)] will not succeed +@defproc[(yices-available?) boolean?]{ +Returns true if the Yices2 solver is available for use (i.e., Rosette can locate a @tt{yices} binary). +If this returns @racket[#f], @racket[(yices)] will not succeed without its optional @racket[path] argument.} diff --git a/rosette/solver/smt/yices-smt2.rkt b/rosette/solver/smt/yices-smt2.rkt deleted file mode 100644 index d5be70c0..00000000 --- a/rosette/solver/smt/yices-smt2.rkt +++ /dev/null @@ -1,69 +0,0 @@ -#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?) - -(define-runtime-path yices-smt2-path (build-path ".." ".." ".." "bin" "yices-smt2")) -(define yices-smt2-opts '("--incremental")) - -(define (yices-smt2-available?) - (not (false? (base/find-solver "yices-smt2" yices-smt2-path #f)))) -(define default-logic 'QF_BV) ;; YICES_2 needs a default logic set otherwise it will error -(define (make-yices-smt2 [solver #f] #:options [options (hash)] #:logic [logic default-logic] #:path [path #f]) - (define config - (cond - [(yices-smt2? solver) - (base/solver-config solver)] - [else - (define real-yices-smt2-path (base/find-solver "yices-smt2" yices-smt2-path path)) - (when (and (false? real-yices-smt2-path) (not (getenv "PLT_PKG_BUILD_SERVICE"))) - (error 'yices-smt2 "yices-smt2 binary is not available (expected to be at ~a); try passing the #:path argument to (yices-smt2)" (path->string (simplify-path yices-smt2-path)))) - (base/config options real-yices-smt2-path logic)])) - (yices-smt2 (server (base/config-path config) yices-smt2-opts (base/make-send-options config)) config '() '() '() (env) '())) - -(struct yices-smt2 base/solver () - #:property prop:solver-constructor make-yices-smt2 - #:methods gen:custom-write - [(define (write-proc self port mode) (fprintf port "#"))] - #:methods gen:solver - [ - (define (solver-features self) - '(qf_bv)) - - (define (solver-options self) - (base/solver-options self)) - - (define (solver-assert self bools) - (base/solver-assert self bools)) - - (define (solver-minimize self nums) - (base/solver-minimize self nums)) - - (define (solver-maximize self nums) - (base/solver-maximize self nums)) - - (define (solver-clear self) - (base/solver-clear self)) - - (define (solver-shutdown self) - (base/solver-shutdown self)) - - (define (solver-push self) - (base/solver-push self)) - - (define (solver-pop self [k 1]) - (base/solver-pop self k)) - - (define (solver-check self) - (base/solver-check self)) - - (define (solver-debug self) - (base/solver-debug self))]) - -(define (set-default-options server) - void) - \ No newline at end of file diff --git a/rosette/solver/smt/yices.rkt b/rosette/solver/smt/yices.rkt new file mode 100644 index 00000000..dce431cf --- /dev/null +++ b/rosette/solver/smt/yices.rkt @@ -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 yices]) yices? yices-available?) + +(define-runtime-path yices-path (build-path ".." ".." ".." "bin" "yices")) +(define yices-opts '("--incremental")) + +(define (yices-available?) + (not (false? (base/find-solver "yices" yices-path #f)))) +(define default-logic 'QF_BV) ;; Yices2 needs a default logic set otherwise it will error +(define (make-yices [solver #f] #:options [options (hash)] #:logic [logic default-logic] #:path [path #f]) + (define config + (cond + [(yices? solver) + (base/solver-config solver)] + [else + (define real-yices-path (base/find-solver "yices" yices-path path)) + (when (and (false? real-yices-path) (not (getenv "PLT_PKG_BUILD_SERVICE"))) + (error 'yices "yices binary is not available (expected to be at ~a); try passing the #:path argument to (yices)" (path->string (simplify-path yices-path)))) + (base/config options real-yices-path logic)])) + (yices (server (base/config-path config) yices-opts (base/make-send-options config)) config '() '() '() (env) '())) + +(struct yices base/solver () + #:property prop:solver-constructor make-yices + #:methods gen:custom-write + [(define (write-proc self port mode) (fprintf port "#"))] + #:methods gen:solver + [ + (define (solver-features self) + '(qf_bv)) + + (define (solver-options self) + (base/solver-options self)) + + (define (solver-assert self bools) + (base/solver-assert self bools)) + + (define (solver-minimize self nums) + (base/solver-minimize self nums)) + + (define (solver-maximize self nums) + (base/solver-maximize self nums)) + + (define (solver-clear self) + (base/solver-clear self)) + + (define (solver-shutdown self) + (base/solver-shutdown self)) + + (define (solver-push self) + (base/solver-push self)) + + (define (solver-pop self [k 1]) + (base/solver-pop self k)) + + (define (solver-check self) + (base/solver-check self)) + + (define (solver-debug self) + (base/solver-debug self))]) + +(define (set-default-options server) + void) + \ No newline at end of file From 4b6327667433aafb5f542b5b6a313cd804e26f75 Mon Sep 17 00:00:00 2001 From: Gus Smith Date: Thu, 14 Dec 2023 10:51:33 -0800 Subject: [PATCH 22/30] Switch back to yices-smt2 binary --- rosette/solver/smt/yices.rkt | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/rosette/solver/smt/yices.rkt b/rosette/solver/smt/yices.rkt index dce431cf..a852129c 100644 --- a/rosette/solver/smt/yices.rkt +++ b/rosette/solver/smt/yices.rkt @@ -7,11 +7,11 @@ (provide (rename-out [make-yices yices]) yices? yices-available?) -(define-runtime-path yices-path (build-path ".." ".." ".." "bin" "yices")) +(define-runtime-path yices-path (build-path ".." ".." ".." "bin" "yices-smt2")) (define yices-opts '("--incremental")) (define (yices-available?) - (not (false? (base/find-solver "yices" yices-path #f)))) + (not (false? (base/find-solver "yices-smt2" yices-path #f)))) (define default-logic 'QF_BV) ;; Yices2 needs a default logic set otherwise it will error (define (make-yices [solver #f] #:options [options (hash)] #:logic [logic default-logic] #:path [path #f]) (define config @@ -19,9 +19,9 @@ [(yices? solver) (base/solver-config solver)] [else - (define real-yices-path (base/find-solver "yices" yices-path path)) + (define real-yices-path (base/find-solver "yices-smt2" yices-path path)) (when (and (false? real-yices-path) (not (getenv "PLT_PKG_BUILD_SERVICE"))) - (error 'yices "yices binary is not available (expected to be at ~a); try passing the #:path argument to (yices)" (path->string (simplify-path yices-path)))) + (error 'yices "yices-smt2 binary is not available (expected to be at ~a); try passing the #:path argument to (yices)" (path->string (simplify-path yices-path)))) (base/config options real-yices-path logic)])) (yices (server (base/config-path config) yices-opts (base/make-send-options config)) config '() '() '() (env) '())) From f8dfb4b5f889bba35e9c9b22df39035cb7b79ff7 Mon Sep 17 00:00:00 2001 From: Gus Smith Date: Thu, 14 Dec 2023 10:51:49 -0800 Subject: [PATCH 23/30] Update documentation --- rosette/guide/scribble/datatypes/solvers+solutions.scrbl | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/rosette/guide/scribble/datatypes/solvers+solutions.scrbl b/rosette/guide/scribble/datatypes/solvers+solutions.scrbl index 121175d1..e137e169 100644 --- a/rosette/guide/scribble/datatypes/solvers+solutions.scrbl +++ b/rosette/guide/scribble/datatypes/solvers+solutions.scrbl @@ -393,7 +393,11 @@ Returns a @racket[solver?] wrapper for the @hyperlink["https://yices.csl.sri.com To use this solver, download prebuilt Yices2 or build it yourself, and ensure the executable is on your @tt{PATH} or pass the path to the executable as the optional @racket[path] argument. -Rosette specifically uses the @tt{yices} executable. +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 +@tt{yices-smt2}. Rosette currently tests Yices2 at commit @tt{e27cf308cffb0ecc6cc7165c10e81ca65bc303b3}. From 5c92eec5f0573f2e5b4bfa1cbac9e3c31f004c12 Mon Sep 17 00:00:00 2001 From: Gus Smith Date: Thu, 14 Dec 2023 10:52:03 -0800 Subject: [PATCH 24/30] More updates --- test/all-rosette-tests.rkt | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/test/all-rosette-tests.rkt b/test/all-rosette-tests.rkt index 33078b84..75162700 100644 --- a/test/all-rosette-tests.rkt +++ b/test/all-rosette-tests.rkt @@ -7,7 +7,7 @@ rosette/solver/smt/cvc5 rosette/solver/smt/bitwuzla rosette/solver/smt/stp - rosette/solver/smt/yices-smt2 + rosette/solver/smt/yices "config.rkt") (error-print-width default-error-print-width) @@ -98,9 +98,9 @@ (printf "===== Running stp tests =====\n") (run-tests-with-solver stp)) - (when (yices-smt2-available?) - (printf "===== Running yices-smt2 tests =====\n") - (run-tests-with-solver yices-smt2)) + (when (yices-available?) + (printf "===== Running Yices2 tests =====\n") + (run-tests-with-solver yices)) ) (module+ test From 974d8e4646793c21028c99d98b485e4647023186 Mon Sep 17 00:00:00 2001 From: Gus Smith Date: Thu, 14 Dec 2023 10:54:05 -0800 Subject: [PATCH 25/30] Run `install` so that binary gets renamed --- .github/workflows/tests.yml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/.github/workflows/tests.yml b/.github/workflows/tests.yml index 463d7453..49553c36 100644 --- a/.github/workflows/tests.yml +++ b/.github/workflows/tests.yml @@ -82,10 +82,10 @@ jobs: tar xvf yices2.tar.gz -C yices2 --strip-components=1 && pushd yices2 && autoconf && - ./configure && - make && + ./configure --prefix=$PWD/out/ && + make install && popd && - cp yices2/build/x86_64-pc-linux-gnu-release/bin/yices_smt2 bin/yices_smt2 + cp yices2/out/bin/yices-smt2 bin/yices-smt2 - name: Install Rosette run: raco pkg install --auto --name rosette - name: Compile Rosette tests From 5b2fcefde826e9afa102ef29a7629656eac90210 Mon Sep 17 00:00:00 2001 From: Gus Smith Date: Thu, 14 Dec 2023 11:08:22 -0800 Subject: [PATCH 26/30] Forgot to before --- .github/workflows/tests.yml | 1 + 1 file changed, 1 insertion(+) diff --git a/.github/workflows/tests.yml b/.github/workflows/tests.yml index 49553c36..b6357f54 100644 --- a/.github/workflows/tests.yml +++ b/.github/workflows/tests.yml @@ -83,6 +83,7 @@ jobs: pushd yices2 && autoconf && ./configure --prefix=$PWD/out/ && + make && make install && popd && cp yices2/out/bin/yices-smt2 bin/yices-smt2 From e00ac84dfbd39c5383d3bfeb97253ee6404dea26 Mon Sep 17 00:00:00 2001 From: Gus Smith Date: Thu, 14 Dec 2023 11:14:27 -0800 Subject: [PATCH 27/30] yices->yices-smt2 in docs --- rosette/guide/scribble/datatypes/solvers+solutions.scrbl | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/rosette/guide/scribble/datatypes/solvers+solutions.scrbl b/rosette/guide/scribble/datatypes/solvers+solutions.scrbl index e137e169..ff39c154 100644 --- a/rosette/guide/scribble/datatypes/solvers+solutions.scrbl +++ b/rosette/guide/scribble/datatypes/solvers+solutions.scrbl @@ -413,7 +413,7 @@ will send the command @tt{(set-option :seed 5)} to Yices2 prior to solving. } @defproc[(yices-available?) boolean?]{ -Returns true if the Yices2 solver is available for use (i.e., Rosette can locate a @tt{yices} binary). +Returns true if the Yices2 solver is available for use (i.e., Rosette can locate a @tt{yices-smt2} binary). If this returns @racket[#f], @racket[(yices)] will not succeed without its optional @racket[path] argument.} From c4eaceac055345bd5398cf6de963fb2f4ca47c8a Mon Sep 17 00:00:00 2001 From: Gus Smith Date: Thu, 14 Dec 2023 12:06:06 -0800 Subject: [PATCH 28/30] Add imports --- rosette/guide/scribble/datatypes/solvers+solutions.scrbl | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/rosette/guide/scribble/datatypes/solvers+solutions.scrbl b/rosette/guide/scribble/datatypes/solvers+solutions.scrbl index ff39c154..0ba15299 100644 --- a/rosette/guide/scribble/datatypes/solvers+solutions.scrbl +++ b/rosette/guide/scribble/datatypes/solvers+solutions.scrbl @@ -4,6 +4,10 @@ rosette/solver/solver rosette/solver/solution rosette/solver/smt/z3 rosette/solver/smt/cvc4 rosette/solver/smt/boolector + rosette/solver/smt/bitwuzla + rosette/solver/smt/cvc5 + rosette/solver/smt/stp + rosette/solver/smt/yices rosette/base/form/define rosette/query/query rosette/base/core/term (only-in rosette/base/base bv?) (only-in rosette/base/base assert) From 44f4c3cf49a141530134f2bb6d13100e69f74c0d Mon Sep 17 00:00:00 2001 From: Gus Smith Date: Thu, 14 Dec 2023 12:14:48 -0800 Subject: [PATCH 29/30] More detail in the documentation --- rosette/guide/scribble/datatypes/solvers+solutions.scrbl | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/rosette/guide/scribble/datatypes/solvers+solutions.scrbl b/rosette/guide/scribble/datatypes/solvers+solutions.scrbl index 0ba15299..a1cca0ff 100644 --- a/rosette/guide/scribble/datatypes/solvers+solutions.scrbl +++ b/rosette/guide/scribble/datatypes/solvers+solutions.scrbl @@ -400,8 +400,9 @@ executable as the optional @racket[path] argument. 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 -@tt{yices-smt2}. +named @tt{yices_smt2}. Running the installation step produces an executable +with the correct name. However, it is safe to skip the installation step and +simply rename or symlink the @tt{yices_smt2} executable to @tt{yices-smt2}. Rosette currently tests Yices2 at commit @tt{e27cf308cffb0ecc6cc7165c10e81ca65bc303b3}. From 5d150475b333f78d3e21b1d72185958bb5cff34a Mon Sep 17 00:00:00 2001 From: Gus Smith Date: Thu, 14 Dec 2023 12:38:24 -0800 Subject: [PATCH 30/30] fix docs --- .../guide/scribble/datatypes/solvers+solutions.scrbl | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/rosette/guide/scribble/datatypes/solvers+solutions.scrbl b/rosette/guide/scribble/datatypes/solvers+solutions.scrbl index a1cca0ff..96d1144d 100644 --- a/rosette/guide/scribble/datatypes/solvers+solutions.scrbl +++ b/rosette/guide/scribble/datatypes/solvers+solutions.scrbl @@ -26,6 +26,10 @@ rosette/solver/smt/z3 rosette/solver/smt/cvc4 rosette/solver/smt/boolector + rosette/solver/smt/bitwuzla + rosette/solver/smt/cvc5 + rosette/solver/smt/stp + rosette/solver/smt/yices #:use-sources (rosette/query/finitize rosette/query/query @@ -33,7 +37,11 @@ rosette/solver/solution rosette/solver/smt/z3 rosette/solver/smt/cvc4 - rosette/solver/smt/boolector)] + rosette/solver/smt/boolector + rosette/solver/smt/bitwuzla + rosette/solver/smt/cvc5 + rosette/solver/smt/stp + rosette/solver/smt/yices)] A @deftech{solver} is an automatic reasoning engine, used to answer @seclink["sec:queries"]{queries} about Rosette programs. The result of