Skip to content

solvers: avoid specifying solver paths in define-runtime-path #278

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
sorawee wants to merge 1 commit into
base: master
Choose a base branch
from
Open

solvers: avoid specifying solver paths in define-runtime-path #278

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 2 additions & 1 deletion rosette/solver/smt/bitwuzla.rkt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,8 @@

(provide (rename-out [make-bitwuzla bitwuzla]) bitwuzla? bitwuzla-available?)

(define-runtime-path bitwuzla-path (build-path ".." ".." ".." "bin" "bitwuzla"))
(define-runtime-path bin-path (build-path ".." ".." ".." "bin"))
(define bitwuzla-path (build-path bin-path "bitwuzla"))
(define bitwuzla-opts '("-m"))

(define (bitwuzla-available?)
Expand Down
3 changes: 2 additions & 1 deletion rosette/solver/smt/boolector.rkt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,8 @@

(provide (rename-out [make-boolector boolector]) boolector? boolector-available?)

(define-runtime-path boolector-path (build-path ".." ".." ".." "bin" "boolector"))
(define-runtime-path bin-path (build-path ".." ".." ".." "bin"))
(define boolector-path (build-path bin-path "boolector"))
(define boolector-opts '("-m" "--output-format=smt2" "-i"))

(define (boolector-available?)
Expand Down
3 changes: 2 additions & 1 deletion rosette/solver/smt/cvc4.rkt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,8 @@

(provide (rename-out [make-cvc4 cvc4]) cvc4? cvc4-available?)

(define-runtime-path cvc4-path (build-path ".." ".." ".." "bin" "cvc4"))
(define-runtime-path bin-path (build-path ".." ".." ".." "bin"))
(define cvc4-path (build-path bin-path "cvc4"))
(define cvc4-opts '("-L" "smt2" "-q" "-m" "-i" "--bv-print-consts-as-indexed-symbols" "--bv-div-zero-const"))

(define (cvc4-available?)
Expand Down
3 changes: 2 additions & 1 deletion rosette/solver/smt/cvc5.rkt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,8 @@

(provide (rename-out [make-cvc5 cvc5]) cvc5? cvc5-available?)

(define-runtime-path cvc5-path (build-path ".." ".." ".." "bin" "cvc5"))
(define-runtime-path bin-path (build-path ".." ".." ".." "bin"))
(define cvc5-path (build-path bin-path "cvc5"))
(define cvc5-opts '("-L" "smt2" "-q" "-m" "-i" "--bv-print-consts-as-indexed-symbols"))

(define (cvc5-available?)
Expand Down
4 changes: 2 additions & 2 deletions rosette/solver/smt/stp.rkt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,8 @@

(provide (rename-out [make-stp stp]) stp? stp-available?)

(define-runtime-path stp-path (build-path ".." ".." ".." "bin" "stp"))
(define-runtime-path bin-path (build-path ".." ".." ".." "bin"))
(define stp-path (build-path bin-path "stp"))
(define stp-opts '("--SMTLIB2"))

(define (stp-available?)
Expand Down Expand Up @@ -66,4 +67,3 @@

(define (set-default-options server)
void)

4 changes: 2 additions & 2 deletions rosette/solver/smt/yices.rkt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,8 @@

(provide (rename-out [make-yices yices]) yices? yices-available?)

(define-runtime-path yices-path (build-path ".." ".." ".." "bin" "yices-smt2"))
(define-runtime-path bin-path (build-path ".." ".." ".." "bin"))
(define yices-path (build-path bin-path "yices-smt2"))
(define yices-opts '("--incremental"))

(define (yices-available?)
Expand Down Expand Up @@ -66,4 +67,3 @@

(define (set-default-options server)
void)

3 changes: 2 additions & 1 deletion rosette/solver/smt/z3.rkt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,8 @@

(provide (rename-out [make-z3 z3]) z3?)

(define-runtime-path z3-path (build-path ".." ".." ".." "bin" "z3"))
(define-runtime-path bin-path (build-path ".." ".." ".." "bin"))
(define z3-path (build-path bin-path "z3"))
(define z3-opts '("-smt2" "-in"))

(define default-options
Expand Down