diff --git a/.github/workflows/tests.yml b/.github/workflows/tests.yml index 735b631d..b6357f54 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: @@ -57,7 +59,34 @@ 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 && + wget $STP_URL -nv -O stp.tar.gz && + mkdir stp && + tar xzf stp.tar.gz -C stp --strip-components=1 && + pushd stp && + ./scripts/deps/setup-gtest.sh && + ./scripts/deps/setup-outputcheck.sh && + ./scripts/deps/setup-cms.sh && + ./scripts/deps/setup-minisat.sh && + mkdir build && + pushd build && + cmake .. && + cmake --build . && + popd && + popd && + cp stp/build/stp bin/stp && + 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 --prefix=$PWD/out/ && + make && + make install && + popd && + cp yices2/out/bin/yices-smt2 bin/yices-smt2 - name: Install Rosette run: raco pkg install --auto --name rosette - name: Compile Rosette tests diff --git a/rosette/guide/scribble/datatypes/solvers+solutions.scrbl b/rosette/guide/scribble/datatypes/solvers+solutions.scrbl index c1cee777..96d1144d 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) @@ -22,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 @@ -29,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 @@ -279,6 +291,146 @@ 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 #:no-declare] + +@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 its SMTLIB2 frontend enabled. +Note that just building (without installing) Yices2 will produce an executable +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}. + +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-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)] 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?]), diff --git a/rosette/solver/smt/stp.rkt b/rosette/solver/smt/stp.rkt new file mode 100644 index 00000000..2cb91529 --- /dev/null +++ b/rosette/solver/smt/stp.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-stp stp]) stp? stp-available?) + +(define-runtime-path stp-path (build-path ".." ".." ".." "bin" "stp")) +(define stp-opts '("--SMTLIB2")) + +(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/rosette/solver/smt/yices.rkt b/rosette/solver/smt/yices.rkt new file mode 100644 index 00000000..a852129c --- /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-smt2")) +(define yices-opts '("--incremental")) + +(define (yices-available?) + (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 + (cond + [(yices? solver) + (base/solver-config solver)] + [else + (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-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) '())) + +(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 diff --git a/test/all-rosette-tests.rkt b/test/all-rosette-tests.rkt index c0086f7b..75162700 100644 --- a/test/all-rosette-tests.rkt +++ b/test/all-rosette-tests.rkt @@ -6,6 +6,8 @@ rosette/solver/smt/boolector rosette/solver/smt/cvc5 rosette/solver/smt/bitwuzla + rosette/solver/smt/stp + rosette/solver/smt/yices "config.rkt") (error-print-width default-error-print-width) @@ -91,6 +93,14 @@ (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-available?) + (printf "===== Running Yices2 tests =====\n") + (run-tests-with-solver yices)) ) (module+ test