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

On commands like `raco distribute`, paths under `define-runtime-path`
will be copied over for distribution, which mandates their existence.
Therefore, we should only use `define-runtime-path` with paths
that we know for sure that they exist.

rosette/solver/smt/bitwuzla.rkt

@@ -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?)

rosette/solver/smt/boolector.rkt

@@ -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?)

rosette/solver/smt/cvc4.rkt

@@ -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?)

rosette/solver/smt/cvc5.rkt

@@ -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?)

rosette/solver/smt/stp.rkt

@@ -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?)
@@ -66,4 +67,3 @@
 
 (define (set-default-options server)
   void)
-

rosette/solver/smt/yices.rkt

@@ -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?)
@@ -66,4 +67,3 @@
 
 (define (set-default-options server)
   void)
-

rosette/solver/smt/z3.rkt

@@ -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