Skip to content

Commit

Permalink
Add support for STP and Yices2 (#273)
Browse files Browse the repository at this point in the history
Also add documentation for Bitwuzla and cvc5

---------

Co-authored-by: Vishal Canumalla <vishalc@cs.washington.edu>
  • Loading branch information
gussmith23 and vcanumalla authored Dec 14, 2023
1 parent 63524aa commit edf682d
Show file tree
Hide file tree
Showing 5 changed files with 331 additions and 2 deletions.
31 changes: 30 additions & 1 deletion .github/workflows/tests.yml
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand Down Expand Up @@ -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
Expand Down
154 changes: 153 additions & 1 deletion rosette/guide/scribble/datatypes/solvers+solutions.scrbl
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand All @@ -22,14 +26,22 @@
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
rosette/solver/solver
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
Expand Down Expand Up @@ -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?]),
Expand Down
69 changes: 69 additions & 0 deletions rosette/solver/smt/stp.rkt
Original file line number Diff line number Diff line change
@@ -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 "#<stp>"))]
#: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)

69 changes: 69 additions & 0 deletions rosette/solver/smt/yices.rkt
Original file line number Diff line number Diff line change
@@ -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 "#<yices>"))]
#: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)

10 changes: 10 additions & 0 deletions test/all-rosette-tests.rkt
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down Expand Up @@ -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
Expand Down

0 comments on commit edf682d

Please sign in to comment.