Skip to content

Commit edf682d

Browse files
gussmith23vcanumalla
gussmith23
and
vcanumalla
authored
Add support for STP and Yices2 (#273)
Also add documentation for Bitwuzla and cvc5 --------- Co-authored-by: Vishal Canumalla <[email protected]>
1 parent 63524aa commit edf682d

File tree

5 files changed

+331
-2
lines changed

5 files changed

+331
-2
lines changed

‎.github/workflows/tests.yml

+30-1
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,8 @@ env:
77
BOOLECTOR_URL: "https://github.com/Boolector/boolector/archive/3.2.1.tar.gz"
88
CVC5_URL: "https://github.com/cvc5/cvc5/releases/download/cvc5-1.0.7/cvc5-Linux"
99
BITWUZLA_URL: "https://github.com/bitwuzla/bitwuzla/archive/93a3d930f622b4cef0063215e63b7c3bd10bd663.tar.gz"
10+
STP_URL: "https://github.com/stp/stp/archive/0510509a85b6823278211891cbb274022340fa5c.tar.gz"
11+
YICES2_URL: "https://github.com/SRI-CSL/yices2/archive/e27cf308cffb0ecc6cc7165c10e81ca65bc303b3.tar.gz"
1012

1113
jobs:
1214
test:
@@ -57,7 +59,34 @@ jobs:
5759
ninja &&
5860
popd &&
5961
popd &&
60-
cp bitwuzla/build/src/main/bitwuzla bin/
62+
cp bitwuzla/build/src/main/bitwuzla bin/ &&
63+
sudo apt-get install -y git cmake bison flex libboost-all-dev python2 perl &&
64+
wget $STP_URL -nv -O stp.tar.gz &&
65+
mkdir stp &&
66+
tar xzf stp.tar.gz -C stp --strip-components=1 &&
67+
pushd stp &&
68+
./scripts/deps/setup-gtest.sh &&
69+
./scripts/deps/setup-outputcheck.sh &&
70+
./scripts/deps/setup-cms.sh &&
71+
./scripts/deps/setup-minisat.sh &&
72+
mkdir build &&
73+
pushd build &&
74+
cmake .. &&
75+
cmake --build . &&
76+
popd &&
77+
popd &&
78+
cp stp/build/stp bin/stp &&
79+
sudo apt-get install -y gperf &&
80+
wget $YICES2_URL -nv -O yices2.tar.gz &&
81+
mkdir yices2 &&
82+
tar xvf yices2.tar.gz -C yices2 --strip-components=1 &&
83+
pushd yices2 &&
84+
autoconf &&
85+
./configure --prefix=$PWD/out/ &&
86+
make &&
87+
make install &&
88+
popd &&
89+
cp yices2/out/bin/yices-smt2 bin/yices-smt2
6190
- name: Install Rosette
6291
run: raco pkg install --auto --name rosette
6392
- name: Compile Rosette tests

‎rosette/guide/scribble/datatypes/solvers+solutions.scrbl

+153-1
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,10 @@
44
rosette/solver/solver rosette/solver/solution
55
rosette/solver/smt/z3 rosette/solver/smt/cvc4
66
rosette/solver/smt/boolector
7+
rosette/solver/smt/bitwuzla
8+
rosette/solver/smt/cvc5
9+
rosette/solver/smt/stp
10+
rosette/solver/smt/yices
711
rosette/base/form/define rosette/query/query
812
rosette/base/core/term (only-in rosette/base/base bv?)
913
(only-in rosette/base/base assert)
@@ -22,14 +26,22 @@
2226
rosette/solver/smt/z3
2327
rosette/solver/smt/cvc4
2428
rosette/solver/smt/boolector
29+
rosette/solver/smt/bitwuzla
30+
rosette/solver/smt/cvc5
31+
rosette/solver/smt/stp
32+
rosette/solver/smt/yices
2533
#:use-sources
2634
(rosette/query/finitize
2735
rosette/query/query
2836
rosette/solver/solver
2937
rosette/solver/solution
3038
rosette/solver/smt/z3
3139
rosette/solver/smt/cvc4
32-
rosette/solver/smt/boolector)]
40+
rosette/solver/smt/boolector
41+
rosette/solver/smt/bitwuzla
42+
rosette/solver/smt/cvc5
43+
rosette/solver/smt/stp
44+
rosette/solver/smt/yices)]
3345

3446
A @deftech{solver} is an automatic reasoning engine, used to answer
3547
@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
279291
If this returns @racket[#f], @racket[(boolector)] will not succeed
280292
without its optional @racket[path] argument.}
281293

294+
@subsection{Bitwuzla}
295+
296+
@defmodule[rosette/solver/smt/bitwuzla #:no-declare]
297+
298+
@defproc*[([(bitwuzla [#:path path (or/c path-string? #f) #f]
299+
[#:logic logic (or/c symbol? #f) #f]
300+
[#:options options (hash/c symbol? any/c) (hash)]) solver?]
301+
[(bitwuzla? [v any/c]) boolean?])]{
302+
303+
Returns a @racket[solver?] wrapper for the @hyperlink["https://bitwuzla.github.io/"]{Bitwuzla} solver.
304+
305+
To use this solver, download prebuilt Bitwuzla or build it yourself,
306+
and ensure the executable is on your @tt{PATH} or pass the path to the
307+
executable as the optional @racket[path] argument.
308+
Rosette currently tests Bitwuzla at commit
309+
@tt{93a3d930f622b4cef0063215e63b7c3bd10bd663}.
310+
311+
The optional @racket[logic] argument specifies an SMT logic for the solver to use (e.g., @racket['QF_BV]).
312+
Specifying a logic can improve solving performance, but Rosette makes no effort to check that
313+
emitted constraints fall within the chosen logic. The default is @racket[#f],
314+
which uses Bitwuzla's default logic.
315+
316+
The @racket[options] argument provides additional options that are sent to Bitwuzla
317+
via the @tt{set-option} SMT command.
318+
For example, setting @racket[options] to @racket[(hash ':seed 5)]
319+
will send the command @tt{(set-option :seed 5)} to Bitwuzla prior to solving.
320+
}
321+
322+
@defproc[(bitwuzla-available?) boolean?]{
323+
Returns true if the Bitwuzla solver is available for use (i.e., Rosette can locate a @tt{bitwuzla} binary).
324+
If this returns @racket[#f], @racket[(bitwuzla)] will not succeed
325+
without its optional @racket[path] argument.}
326+
327+
@subsection{CVC5}
328+
329+
@defmodule[rosette/solver/smt/cvc5 #:no-declare]
330+
331+
@defproc*[([(cvc5 [#:path path (or/c path-string? #f) #f]
332+
[#:logic logic (or/c symbol? #f) #f]
333+
[#:options options (hash/c symbol? any/c) (hash)]) solver?]
334+
[(cvc5? [v any/c]) boolean?])]{
335+
336+
Returns a @racket[solver?] wrapper for the @hyperlink["https://cvc5.github.io/"]{CVC5} solver.
337+
338+
To use this solver, download prebuilt CVC5 or build it yourself,
339+
and ensure the executable is on your @tt{PATH} or pass the path to the
340+
executable as the optional @racket[path] argument.
341+
Rosette currently tests CVC5 at version 1.0.7.
342+
343+
The optional @racket[logic] argument specifies an SMT logic for the solver to use (e.g., @racket['QF_BV]).
344+
Specifying a logic can improve solving performance, but Rosette makes no effort to check that
345+
emitted constraints fall within the chosen logic. The default is @racket[#f],
346+
which uses CVC5's default logic.
347+
348+
The @racket[options] argument provides additional options that are sent to CVC5
349+
via the @tt{set-option} SMT command.
350+
For example, setting @racket[options] to @racket[(hash ':seed 5)]
351+
will send the command @tt{(set-option :seed 5)} to CVC5 prior to solving.
352+
}
353+
354+
@defproc[(cvc5-available?) boolean?]{
355+
Returns true if the CVC5 solver is available for use (i.e., Rosette can locate a @tt{cvc5} binary).
356+
If this returns @racket[#f], @racket[(cvc5)] will not succeed
357+
without its optional @racket[path] argument.}
358+
359+
@subsection{STP}
360+
361+
@defmodule[rosette/solver/smt/stp #:no-declare]
362+
363+
@defproc*[([(stp [#:path path (or/c path-string? #f) #f]
364+
[#:logic logic (or/c symbol? #f) #f]
365+
[#:options options (hash/c symbol? any/c) (hash)]) solver?]
366+
[(stp? [v any/c]) boolean?])]{
367+
368+
Returns a @racket[solver?] wrapper for the @hyperlink["https://stp.github.io/"]{STP} solver.
369+
370+
To use this solver, download prebuilt STP or build it yourself,
371+
and ensure the executable is on your @tt{PATH} or pass the path to the
372+
executable as the optional @racket[path] argument.
373+
Rosette currently tests STP at commit
374+
@tt{0510509a85b6823278211891cbb274022340fa5c}.
375+
Note that as of December 2023, the STP version on Mac Homebrew is too old to be
376+
supported by Rosette.
377+
378+
The optional @racket[logic] argument specifies an SMT logic for the solver to use (e.g., @racket['QF_BV]).
379+
Specifying a logic can improve solving performance, but Rosette makes no effort to check that
380+
emitted constraints fall within the chosen logic. The default is @racket[#f],
381+
which uses STP's default logic.
382+
383+
The @racket[options] argument provides additional options that are sent to STP
384+
via the @tt{set-option} SMT command.
385+
For example, setting @racket[options] to @racket[(hash ':seed 5)]
386+
will send the command @tt{(set-option :seed 5)} to STP prior to solving.
387+
}
388+
389+
@defproc[(stp-available?) boolean?]{
390+
Returns true if the STP solver is available for use (i.e., Rosette can locate a @tt{stp} binary).
391+
If this returns @racket[#f], @racket[(stp)] will not succeed
392+
without its optional @racket[path] argument.}
393+
394+
@subsection{Yices2}
395+
396+
@defmodule[rosette/solver/smt/yices #:no-declare]
397+
398+
@defproc*[([(yices [#:path path (or/c path-string? #f) #f]
399+
[#:logic logic (or/c symbol? #f) 'QF_BV]
400+
[#:options options (hash/c symbol? any/c) (hash)]) solver?]
401+
[(yices? [v any/c]) boolean?])]{
402+
403+
Returns a @racket[solver?] wrapper for the @hyperlink["https://yices.csl.sri.com/"]{Yices2} solver.
404+
405+
To use this solver, download prebuilt Yices2 or build it yourself,
406+
and ensure the executable is on your @tt{PATH} or pass the path to the
407+
executable as the optional @racket[path] argument.
408+
Rosette specifically uses the @tt{yices-smt2} executable, which is the Yices2
409+
solver with its SMTLIB2 frontend enabled.
410+
Note that just building (without installing) Yices2 will produce an executable
411+
named @tt{yices_smt2}. Running the installation step produces an executable
412+
with the correct name. However, it is safe to skip the installation step and
413+
simply rename or symlink the @tt{yices_smt2} executable to @tt{yices-smt2}.
414+
Rosette currently tests Yices2 at commit
415+
@tt{e27cf308cffb0ecc6cc7165c10e81ca65bc303b3}.
416+
417+
The optional @racket[logic] argument specifies an SMT logic for the solver to use (e.g., @racket['QF_BV]).
418+
Specifying a logic can improve solving performance, but Rosette makes no effort to check that
419+
emitted constraints fall within the chosen logic. Yices2 expects a logic to be
420+
set; Rosette defaults to @racket['QF_BV].
421+
422+
The @racket[options] argument provides additional options that are sent to Yices2
423+
via the @tt{set-option} SMT command.
424+
For example, setting @racket[options] to @racket[(hash ':seed 5)]
425+
will send the command @tt{(set-option :seed 5)} to Yices2 prior to solving.
426+
}
427+
428+
@defproc[(yices-available?) boolean?]{
429+
Returns true if the Yices2 solver is available for use (i.e., Rosette can locate a @tt{yices-smt2} binary).
430+
If this returns @racket[#f], @racket[(yices)] will not succeed
431+
without its optional @racket[path] argument.}
432+
433+
282434
@section{Solutions}
283435

284436
A solution to a set of formulas may be satisfiable (@racket[sat?]), unsatisfiable (@racket[unsat?]),

‎rosette/solver/smt/stp.rkt

+69
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,69 @@
1+
#lang racket
2+
3+
(require racket/runtime-path
4+
"server.rkt" "env.rkt"
5+
"../solver.rkt"
6+
(prefix-in base/ "base-solver.rkt"))
7+
8+
(provide (rename-out [make-stp stp]) stp? stp-available?)
9+
10+
(define-runtime-path stp-path (build-path ".." ".." ".." "bin" "stp"))
11+
(define stp-opts '("--SMTLIB2"))
12+
13+
(define (stp-available?)
14+
(not (false? (base/find-solver "stp" stp-path #f))))
15+
16+
(define (make-stp [solver #f] #:options [options (hash)] #:logic [logic #f] #:path [path #f])
17+
(define config
18+
(cond
19+
[(stp? solver)
20+
(base/solver-config solver)]
21+
[else
22+
(define real-stp-path (base/find-solver "stp" stp-path path))
23+
(when (and (false? real-stp-path) (not (getenv "PLT_PKG_BUILD_SERVICE")))
24+
(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))))
25+
(base/config options real-stp-path logic)]))
26+
(stp (server (base/config-path config) stp-opts (base/make-send-options config)) config '() '() '() (env) '()))
27+
28+
(struct stp base/solver ()
29+
#:property prop:solver-constructor make-stp
30+
#:methods gen:custom-write
31+
[(define (write-proc self port mode) (fprintf port "#<stp>"))]
32+
#:methods gen:solver
33+
[
34+
(define (solver-features self)
35+
'(qf_bv))
36+
37+
(define (solver-options self)
38+
(base/solver-options self))
39+
40+
(define (solver-assert self bools)
41+
(base/solver-assert self bools))
42+
43+
(define (solver-minimize self nums)
44+
(base/solver-minimize self nums))
45+
46+
(define (solver-maximize self nums)
47+
(base/solver-maximize self nums))
48+
49+
(define (solver-clear self)
50+
(base/solver-clear self))
51+
52+
(define (solver-shutdown self)
53+
(base/solver-shutdown self))
54+
55+
(define (solver-push self)
56+
(base/solver-push self))
57+
58+
(define (solver-pop self [k 1])
59+
(base/solver-pop self k))
60+
61+
(define (solver-check self)
62+
(base/solver-check self))
63+
64+
(define (solver-debug self)
65+
(base/solver-debug self))])
66+
67+
(define (set-default-options server)
68+
void)
69+

‎rosette/solver/smt/yices.rkt

+69
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,69 @@
1+
#lang racket
2+
3+
(require racket/runtime-path
4+
"server.rkt" "env.rkt"
5+
"../solver.rkt"
6+
(prefix-in base/ "base-solver.rkt"))
7+
8+
(provide (rename-out [make-yices yices]) yices? yices-available?)
9+
10+
(define-runtime-path yices-path (build-path ".." ".." ".." "bin" "yices-smt2"))
11+
(define yices-opts '("--incremental"))
12+
13+
(define (yices-available?)
14+
(not (false? (base/find-solver "yices-smt2" yices-path #f))))
15+
(define default-logic 'QF_BV) ;; Yices2 needs a default logic set otherwise it will error
16+
(define (make-yices [solver #f] #:options [options (hash)] #:logic [logic default-logic] #:path [path #f])
17+
(define config
18+
(cond
19+
[(yices? solver)
20+
(base/solver-config solver)]
21+
[else
22+
(define real-yices-path (base/find-solver "yices-smt2" yices-path path))
23+
(when (and (false? real-yices-path) (not (getenv "PLT_PKG_BUILD_SERVICE")))
24+
(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))))
25+
(base/config options real-yices-path logic)]))
26+
(yices (server (base/config-path config) yices-opts (base/make-send-options config)) config '() '() '() (env) '()))
27+
28+
(struct yices base/solver ()
29+
#:property prop:solver-constructor make-yices
30+
#:methods gen:custom-write
31+
[(define (write-proc self port mode) (fprintf port "#<yices>"))]
32+
#:methods gen:solver
33+
[
34+
(define (solver-features self)
35+
'(qf_bv))
36+
37+
(define (solver-options self)
38+
(base/solver-options self))
39+
40+
(define (solver-assert self bools)
41+
(base/solver-assert self bools))
42+
43+
(define (solver-minimize self nums)
44+
(base/solver-minimize self nums))
45+
46+
(define (solver-maximize self nums)
47+
(base/solver-maximize self nums))
48+
49+
(define (solver-clear self)
50+
(base/solver-clear self))
51+
52+
(define (solver-shutdown self)
53+
(base/solver-shutdown self))
54+
55+
(define (solver-push self)
56+
(base/solver-push self))
57+
58+
(define (solver-pop self [k 1])
59+
(base/solver-pop self k))
60+
61+
(define (solver-check self)
62+
(base/solver-check self))
63+
64+
(define (solver-debug self)
65+
(base/solver-debug self))])
66+
67+
(define (set-default-options server)
68+
void)
69+

‎test/all-rosette-tests.rkt

+10
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,8 @@
66
rosette/solver/smt/boolector
77
rosette/solver/smt/cvc5
88
rosette/solver/smt/bitwuzla
9+
rosette/solver/smt/stp
10+
rosette/solver/smt/yices
911
"config.rkt")
1012

1113
(error-print-width default-error-print-width)
@@ -91,6 +93,14 @@
9193
(when (bitwuzla-available?)
9294
(printf "===== Running bitwuzla tests =====\n")
9395
(run-tests-with-solver bitwuzla))
96+
97+
(when (stp-available?)
98+
(printf "===== Running stp tests =====\n")
99+
(run-tests-with-solver stp))
100+
101+
(when (yices-available?)
102+
(printf "===== Running Yices2 tests =====\n")
103+
(run-tests-with-solver yices))
94104
)
95105

96106
(module+ test

0 commit comments

Comments
 (0)