.github/dependabot.yml

@@ -1,6 +0,0 @@
-version: 2
-updates:
-  - package-ecosystem: "github-actions"
-    directory: "/"
-    schedule:
-      interval: "daily"

.github/workflows/docker.yml

@@ -1,50 +0,0 @@
-name: Docker
-
-on:
-  push:
-    tags:
-      - '*'
-    branches:
-      - master
-  pull_request:
-
-jobs:
-  docker:
-    runs-on: ubuntu-latest
-
-    steps:
-      - name: Clone Repository
-        uses: actions/checkout@v4
-
-      - name: Configure Docker Metadata
-        id: meta
-        uses: docker/metadata-action@v5
-        with:
-          images: ghcr.io/${{ github.repository }}
-          tags: |
-            type=ref,event=branch
-            type=ref,event=pr
-            type=ref,event=tag
-            type=semver,pattern={{version}}
-            type=semver,pattern={{major}}.{{minor}}
-
-      - name: Authenticate to Package Registry
-        uses: docker/login-action@v3
-        if: ${{ github.event_name != 'pull_request' }}
-        with:
-          registry: ghcr.io
-          username: ${{ github.actor }}
-          password: ${{ secrets.GITHUB_TOKEN }}
-
-      - name: Set up Docker Buildx
-        uses: docker/setup-buildx-action@v3
-
-      - name: Build and Publish Rosette Image
-        uses: docker/build-push-action@v6
-        with:
-          context: .
-          push: ${{ github.event_name != 'pull_request' }}
-          tags: ${{ steps.meta.outputs.tags }}
-          labels: ${{ steps.meta.outputs.labels }}
-          cache-from: type=gha
-          cache-to: type=gha,mode=max

.github/workflows/tests.yml

@@ -5,16 +5,12 @@ on: [push, pull_request]
 env:
   CVC4_URL: "http://cvc4.cs.stanford.edu/downloads/builds/x86_64-linux-opt/cvc4-1.8-x86_64-linux-opt"
   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/d70085462f07c8a5a2f1225f727cda3ef505b141.tar.gz"
-  YICES2_URL: "https://github.com/SRI-CSL/yices2/archive/e27cf308cffb0ecc6cc7165c10e81ca65bc303b3.tar.gz"
 
 jobs:
   test:
     strategy:
       matrix:
-        racket-version: ['8.1', 'current']
+        racket-version: ['8.0', 'current']
         racket-variant: ['CS']
         allow-failure: [false]
     name: Racket ${{ matrix.racket-version }} (${{ matrix.racket-variant }})
@@ -23,14 +19,12 @@ jobs:
     steps:
       - uses: actions/checkout@master
       - name: Setup Racket
-        uses: Bogdanp/setup-racket@v1.14
+        uses: Bogdanp/setup-racket@v1.1
         with:
           architecture: x64
           version: ${{ matrix.racket-version }}
           variant: ${{ matrix.racket-variant }}
       - name: Install solvers
-        # Note that setting LD_LIBRARY_PATH can be removed once this bug is
-        # fixed: https://github.com/stp/stp/issues/485
         run: |
           mkdir bin &&
           wget $CVC4_URL -nv -O bin/cvc4 &&
@@ -46,50 +40,7 @@ jobs:
           make &&
           popd &&
           cp boolector/build/bin/boolector bin/ &&
-          rm -rf boolector* &&
+          rm -rf boolector*
-          wget $CVC5_URL -nv -O bin/cvc5 &&
-          chmod +x bin/cvc5 &&
-          sudo apt-get update &&
-          sudo apt-get install -y ninja-build &&
-          pip3 install meson &&
-          wget $BITWUZLA_URL -nv -O bitwuzla.tar.gz &&
-          mkdir bitwuzla &&
-          tar xzf bitwuzla.tar.gz -C bitwuzla --strip-components=1 &&
-          pushd bitwuzla &&
-          ./configure.py &&
-          pushd build &&
-          ninja &&
-          popd &&
-          popd &&
-          cp bitwuzla/build/src/main/bitwuzla bin/ &&
-          sudo apt-get install -y build-essential git cmake bison flex libboost-all-dev libtinfo-dev python3 perl &&
-          wget $STP_URL -nv -O stp.tar.gz &&
-          mkdir stp &&
-          tar xzf stp.tar.gz -C stp --strip-components=1 &&
-          pushd stp &&
-          echo "LD_LIBRARY_PATH=$PWD/deps/cadical/build:$PWD/deps/cadiback/:$LD_LIBRARY_PATH" >> $GITHUB_ENV &&
-          ./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 &&
-          ln -s 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

Dockerfile

@@ -1,97 +0,0 @@
-FROM alpine:3.15
-
-## ==========================  [ Install Racket ] =========================== ##
-
-## Define default Racket version and variant. The Racket version is of the form
-## <major>.<minor>. The variant can be "cs" (Chez Scheme), "bc" (Before Chez) or
-## "natipkg" (where external libraries are included in the Racket packages).
-##
-ARG RACKET_VERSION=8.4
-ARG RACKET_VARIANT=cs
-
-## Install Racket. We first install system dependencies: [gcompat] is needed for
-## Racket and [ncurses] is needed for the [xrepl] and [expeditor] packages,
-## providing the REPL. We then download the installer, run it with the right
-## parameters, then remove it. After that, all that remains is to set-up the
-## Racket packages and install [expeditor]. See later for a description of the
-## arguments to [raco pkg install].
-##
-RUN apk add --no-cache gcompat ncurses
-RUN wget "https://download.racket-lang.org/installers/${RACKET_VERSION}/racket-minimal-${RACKET_VERSION}-x86_64-linux-${RACKET_VARIANT}.sh"
-RUN echo 'yes\n1\n' | sh racket-minimal-${RACKET_VERSION}-x86_64-linux-${RACKET_VARIANT}.sh --create-dir --unix-style --dest /usr/
-RUN rm racket-minimal-${RACKET_VERSION}-x86_64-linux-${RACKET_VARIANT}.sh
-RUN raco setup --no-docs
-RUN raco pkg install -i --batch --auto --no-docs expeditor-lib
-
-## =================== [ Install Rosette's Dependencies ] =================== ##
-
-## Work on Rosette's installation within /usr/local. This directory will be
-## cleaned up later on so it could be anything.
-##
-WORKDIR /usr/local/rosette
-
-## Get all the info.rkt files. Trying to install Rosette based only on these
-## files would fail, but we can use them to only install dependencies.
-##
-COPY info.rkt         .
-COPY rosette/info.rkt rosette/
-
-## Install only Rosette's dependencies. We have to install the external
-## dependencies [libstdc++] and [libgcc] because Z3 needs them at runtime. As
-## for the Racket dependencies only, we achieve that in three steps:
-##
-##   1. We use [raco pkg install --no-setup] to download and register Rosette
-##      and all its dependencies without setting them up, that is without
-##      compiling them. At this point, the system is in an inconsistent state,
-##      where packages are registered but not actually present. The other flags
-##      are the following:
-##
-##        -i         install packages for all users
-##        --batch    disable interactive mode and suppress prompts
-##        --auto     download missing packages automatically
-##
-##   2. We use [raco pkg remove --no-setup] to unregister Rosette. This keeps
-##      the dependencies as registered. The system is still in an inconsistent
-##      state. See above for the flags.
-##
-##   3. We use [raco setup] to set up all the registered package. This brings
-##      the system back in a consistent state. Since Rosette's dependencies were
-##      registered but not Rosette itself, this achieves our goal. The flags are
-##      the following:
-##
-##        --fail-fast    fail on the first error encountered
-##        --no-docs      do not compile the documentations
-##
-RUN apk add --no-cache libstdc++ libgcc
-RUN raco pkg install -i --batch --auto --no-setup ../rosette
-RUN raco pkg remove  -i                --no-setup    rosette
-RUN raco setup       --fail-fast --no-docs
-
-## ========================== [ Install Rosette ] =========================== ##
-
-## Get all of Rosette; build and install it. The dependencies should all be
-## installed, so we can remove the --auto flag which will lead us to failure if
-## a dependency cannot be found. The additional flags are the following:
-##
-##   --copy    copy content to install path (instead of linking)
-##
-COPY . .
-RUN raco pkg install -i --batch --copy --no-docs ./rosette
-RUN rm -R /usr/local/rosette
-
-## ===================== [ Prepare Clean Entry Point ] ====================== ##
-
-## For further use of the image, we can start with user `rosette`, group
-## `rosette` in `/rosette` by default.
-##
-RUN addgroup rosette
-RUN adduser --system --shell /bin/false --disabled-password \
-    --home /rosette --ingroup rosette rosette
-RUN chown -R rosette:rosette /rosette
-USER rosette
-WORKDIR /rosette
-
-## Rosette files are simply Racket files using the Rosette library: the default
-## entry point of this image is therefore the Racket executable.
-##
-ENTRYPOINT ["/usr/bin/racket", "-I", "rosette"]

NOTES.md

@@ -1,9 +1,5 @@
 # Release Notes
 
-## Version 4.1
-
-This is a minor bug-fixing release.
-
 ## Version 4.0
 
 This is a major release with significant changes to the language and the runtime.  Rosette 4.0 is *not backward compatible* with Rosette 3.x. But porting Rosette 3.x code to Rosette 4.0 should be straightforward for most applications.

README.md

@@ -9,7 +9,7 @@ The Rosette Language
 
 The easiest way to install Rosette is from Racket's package manager:
 
-* Download and install Racket 8.1 or later from http://racket-lang.org
+* Download and install Racket 8.0 or later from http://racket-lang.org
 
 * Use Racket's `raco` tool to install Rosette:
 
@@ -19,7 +19,7 @@ The easiest way to install Rosette is from Racket's package manager:
 
 Alternatively, you can install Rosette from source:
 
-* Download and install Racket 8.1 or later from http://racket-lang.org
+* Download and install Racket 8.0 or later from http://racket-lang.org
 
 * Clone the rosette repository:
 

info.rkt

@@ -5,7 +5,7 @@
 (define deps '("custom-load"
                "sandbox-lib"
                "scribble-lib"
-               ("racket" #:version "8.1")
+               ("racket" #:version "8.0")
                "r6rs-lib"
                "rfc6455"
                "net-lib"

rosette/base/base.rkt

@@ -33,7 +33,6 @@
      @bvnot @bvor @bvand @bvxor @bvshl @bvlshr @bvashr
      @bvneg @bvadd @bvsub @bvmul @bvudiv @bvsdiv @bvurem @bvsrem @bvsmod
      @concat @extract @sign-extend @zero-extend 
-     @z3_ext_rotate_left @z3_ext_rotate_right
      @integer->bitvector @bitvector->integer @bitvector->natural
      ; core/bvlib.rkt
      bit lsb msb bvzero? bvadd1 bvsub1

rosette/base/core/bitvector.rkt

@@ -14,19 +14,20 @@
  @bvnot @bvor @bvand @bvxor @bvshl @bvlshr @bvashr
  @bvneg @bvadd @bvsub @bvmul @bvudiv @bvsdiv @bvurem @bvsrem @bvsmod
  @concat @extract @sign-extend @zero-extend
- @z3_ext_rotate_left @z3_ext_rotate_right
  @integer->bitvector @bitvector->integer @bitvector->natural)
 
 ;; ----------------- Bitvector Types ----------------- ;; 
 
 ; Cache of all bitvector types constructed so far, mapping sizes to types.
-(define bitvector-types (make-hasheq))
+(define bitvector-types (make-hash))
 
 ; Returns the bitvector type of the given size.
 (define (bitvector-type size)
-  (assert (and (exact-positive-integer? size) (fixnum? size))
+  (assert (exact-positive-integer? size) (argument-error 'bitvector "exact-positive-integer?" size))
-          (argument-error 'bitvector "(and/c exact-positive-integer? fixnum?)" size))
+  (or (hash-ref bitvector-types size #f)
-  (hash-ref! bitvector-types size (λ () (bitvector size))))
+      (let ([t (bitvector size)]) 
+        (hash-set! bitvector-types size t)
+        t)))
 
 ; Represents a bitvector type.
 (struct bitvector (size)
@@ -339,13 +340,6 @@
      (ite (bveq (bv 0 t) (bvand x (bv (bvsmin t) t))) (bv 0 t) (bv -1 t))]
     [(_ _) (expression @bvashr x y)]))
 
-
-(define (z3_ext_rotate_left x y)
-  (expression @z3_ext_rotate_left x y))
-
-(define (z3_ext_rotate_right x y)
-  (expression @z3_ext_rotate_right x y))
-
 (define-lifted-operator @bvnot bvnot T*->T)
 (define-lifted-operator @bvand bvand T*->T)
 (define-lifted-operator @bvor bvor T*->T)
@@ -353,8 +347,6 @@
 (define-lifted-operator @bvshl bvshl T*->T)
 (define-lifted-operator @bvlshr bvlshr T*->T)
 (define-lifted-operator @bvashr bvashr T*->T)
-(define-lifted-operator @z3_ext_rotate_left z3_ext_rotate_left T*->T)
-(define-lifted-operator @z3_ext_rotate_right z3_ext_rotate_right T*->T)
 
 ;; ----------------- Simplification ruules for bitwise operators ----------------- ;;
 
@@ -603,7 +595,7 @@
                       _))
      (if (< i size)
          (extract i j a)
-         (expression @bvop a (bitvector-type (add1 i))))]
+         (expression @bvop a (bitvector (add1 i))))]
     [(_ _ _) (expression @extract i j x)]))
         
 (define-operator @extract

rosette/base/core/polymorphic.rkt

@@ -152,7 +152,7 @@
   (match* ((car p) (cdr p))
     [(a (expression (== ite) a x _)) (cons a x)]
     [(a (expression (== ite) (expression (== @!) a) _ x)) (cons a x)]
-    [((and (expression (== @!) a) !a) (expression (== ite) a _ x)) (cons !a x)]
+    [((expression (== @!) a) (expression (== ite) a _ x)) (cons a x)]
     [(_ _) p]))
 
 

rosette/base/core/term.rkt

@@ -19,12 +19,7 @@
 ; These IDs are never reused, and they are used to impose an ordering on the children
 ; of expressions with commutative operators.
 #|-----------------------------------------------------------------------------------|#
-
+(define current-terms (make-parameter (make-hash)))
-;; Initialize with #f so that the hash table cooperates with garbage collector.
-;; See #247
-(define current-terms (make-parameter #f))
-(current-terms (make-hash))
-
 (define current-index (make-parameter 0))
 
 ; Clears the entire term cache if invoked with #f (default), or 
@@ -82,23 +77,17 @@
 ; restores (terms) to its old value. If terms-expr is not given, it defaults to
 ; (terms), so (with-terms expr) is equivalent to (with-terms (terms) expr).
 (define-syntax (with-terms stx)
-  ;; Parameterize with #f so that the hash table cooperates with garbage collector.
-  ;; See #247
   (syntax-parse stx
     [(_ expr)
-     #'(let ([orig-terms (current-terms)])
+     #'(parameterize ([current-terms (hash-copy (current-terms))])
-         (parameterize ([current-terms #f])
+         expr)]
-           (current-terms (hash-copy orig-terms))
-           expr))]
     [(_ terms-expr expr)
-     #'(let ([orig-terms (current-terms)])
+     #'(parameterize ([current-terms (hash-copy-clear (current-terms))])
-         (parameterize ([current-terms #f])
-           (current-terms (hash-copy-clear orig-terms))
          (let ([ts terms-expr]
                [cache (current-terms)])
            (for ([t ts])
              (hash-set! cache (term-val t) t))
-             expr)))]))
+           expr))]))
            
          
     
@@ -132,21 +121,14 @@
 (define (term<? s1 s2) (< (term-ord s1) (term-ord s2)))
 
 (define-syntax-rule (make-term term-constructor args type rest ...) 
-  (let ([val args]
+  (let ([val args])
-        [ty type])
+    (or (hash-ref (current-terms) val #f)
-    (define cached (hash-ref (current-terms) val #f))
+        (let* ([ord (current-index)]
-    (cond
+               [out (term-constructor val type ord rest ...)])
-      [cached
-       (unless (equal? (term-type cached) ty)
-         (error 'define-symbolic "type should remain unchanged"))
-       cached]
-      [else
-       (define ord (current-index))
-       (define out (term-constructor val ty ord rest ...))
           (current-index (add1 ord))
           ((current-reporter) 'new-term out)
           (hash-set! (current-terms) val out)
-       out])))
+          out))))
            
 (define (make-const id t) 
   (unless (and (type? t) (solvable? t))

rosette/base/core/type.rkt

@@ -43,8 +43,8 @@
   [type-cast type val [caller]]       ; (-> type? any/c symbol? any/c)
   [type-name type]                    ; (-> type? symbol?)
   [type-applicable? type]             ; (-> type? boolean?)
-  [type-eq? type u v]                 ; (-> type? any/c any/c @boolean?)
+  [type-eq? type u v]                 ; (-> type? (-> any/c any/c @boolean?)))
-  [type-equal? type u v]              ; (-> type? any/c any/c @boolean?)
+  [type-equal? type u v]              ; (-> type? (-> any/c any/c @boolean?)))
   [type-compress type force? ps]      ; (-> type? (listof (cons @boolean? any/c)) (listof (cons @boolean? any/c)))
   [type-construct type vals]          ; (-> type? (listof any/c) any/c)
   [type-deconstruct type val])        ; (-> type? any/c (listof any/c))

rosette/guide/scribble/datatypes/bitvectors.scrbl

@@ -140,7 +140,7 @@ equality (@racket[bveq]) and signed / unsigned versions of
            [(bvor  [x (bitvector n)] ...+) (bitvector n)]
            [(bvxor [x (bitvector n)] ...+) (bitvector n)])]{
                                                             
-Returns the bitwise ``and'', ``or'', ``xor'' of one or more bitvector values of the same type.
+Returns the bitwise "and", "or", "xor" of one or more bitvector values of the same type.
 
  @examples[#:eval rosette-eval
  (bvand (bv -1 4) (bv 2 4))
@@ -434,7 +434,7 @@ leads to faster solving times.
 
 @(rosette-eval '(clear-vc!))
 
-@defproc[(bitvector->bits [x (bitvector n)]) (listof (bitvector 1))]{
+@defproc[(bitvector->bits [x (bitvector n)]) (listof (bitvector n))]{
                                                                      
 Returns the bits of @racket[x] as a list, i.e., @racket[(list (bit 0 x) ... (bit (- n 1) x))].
                     

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

@@ -3,11 +3,7 @@
 @(require (for-label 
            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/yices 
-           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) 
@@ -25,11 +21,8 @@
                    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/solver/smt/boolector
                    #:use-sources 
                    (rosette/query/finitize
                     rosette/query/query
@@ -37,11 +30,8 @@
                     rosette/solver/solution
                     rosette/solver/smt/z3
                     rosette/solver/smt/cvc4
-                    rosette/solver/smt/boolector
+                    rosette/solver/smt/yices
-                    rosette/solver/smt/bitwuzla
+                    rosette/solver/smt/boolector)]
-                    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
@@ -291,146 +281,37 @@ 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]
+@subsection{Yices}
-
-@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]
+                   [#:logic logic symbol? 'ALL]
                    [#: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.
+Returns a @racket[solver?] wrapper for the @hyperlink["http://yices.csl.sri.com/"]{Yices} solver from SRI.
 
-To use this solver, download prebuilt Yices2 or build it yourself,
+To use this solver, download and install Yices (version 2.6.0 or later),
-and ensure the executable is on your @tt{PATH} or pass the path to the 
+and either add the @tt{yices-smt2} executable to your @tt{PATH}
-executable as the optional @racket[path] argument.
+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
+emitted constraints fall within the chosen logic. The default is @racket['ALL].
-set; Rosette defaults to @racket['QF_BV].
 
-The @racket[options] argument provides additional options that are sent to Yices2
+The @racket[options] argument provides additional options that are sent to Yices
 via the @tt{set-option} SMT command.
-For example, setting @racket[options] to @racket[(hash ':seed 5)]
+For example, setting @racket[options] to @racket[(hash ':random-seed 5)]
-will send the command @tt{(set-option :seed 5)} to Yices2 prior to solving.
+will send the command @tt{(set-option :random-seed 5)} to Yices 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).
+Returns true if the Yices 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?]),

rosette/guide/scribble/datatypes/vectors.scrbl

@@ -3,7 +3,6 @@
 @(require (for-label 
            rosette/base/form/define rosette/query/query 
            rosette/base/core/term  
-           rosette/solver/solution
            (only-in rosette/base/base assert define-symbolic union?
                     vc clear-vc! bitvector bitvector? bv?
                     bitvector->natural integer->bitvector

rosette/guide/scribble/essentials/essentials.scrbl

@@ -1,21 +1,19 @@
 #lang scribble/manual
 
-@(require (for-label
+@(require (for-label racket (only-in racket/sandbox with-deep-time-limit))
-           racket
+          (for-label  
-           (only-in racket/sandbox with-deep-time-limit)
            rosette/base/form/define
+           (only-in rosette/base/base assert assume vc vc-asserts vc-assumes clear-vc!)
            rosette/query/query 
-           rosette/solver/solution
+           (only-in rosette/base/base bv? bitvector
-           (only-in rosette/base/base
-                    assert assume vc vc-asserts vc-assumes clear-vc!
-                    bv? bitvector
                     bvsdiv bvadd bvsle bvsub bvand
                     bvor bvxor bvshl bvlshr bvashr
                     bvnot bvneg)
            rosette/lib/synthax))
 
 @(require racket/sandbox  racket/runtime-path  scribble/core scribble/racket
-          scribble/example scribble/html-properties scriblib/footnote)
+          scribble/example scribble/html-properties scriblib/footnote 
+          (only-in racket [unsyntax racket/unsyntax]))
 
 @(require (only-in "../refs.scrbl" ~cite rosette:onward13 rosette:pldi14)
           "../util/lifted.rkt")
@@ -142,7 +140,7 @@ Assumptions behave analogously to assertions on both concrete and symbolic value
 
 @section[#:tag "sec:queries"]{Solver-Aided Queries}
 
-The solver reasons about assumed and asserted properties only when we ask a question about them---for example, ``Does my program have an execution that violates an assertion while satisfying all the assumptions?''  We pose such @emph{solver-aided queries} with the help of constructs explained in the remainder of this chapter.
+The solver reasons about assumed and asserted properties only when we ask a question about them---for example, "Does my program have an execution that violates an assertion while satisfying all the assumptions?"  We pose such @emph{solver-aided queries} with the help of constructs explained in the remainder of this chapter.
 
 We will illustrate the queries on the following toy example. Suppose that we want to implement a
 procedure @racket[bvmid] that takes as input two non-negative 32-bit integers, @racket[lo] ≤ @racket[hi],
@@ -323,7 +321,7 @@ The synthesis query takes the form @racket[(synthesize #:forall #, @var[input] #
 
 Rosette supports one more solver-aided query, which we call angelic execution. This query is the dual of verification.  Given a program with symbolic values, it instructs the solver to find a binding for them that will cause the program to execute normally---that is, without any assumption or assertion failures. 
 
-Angelic execution can be used to solve puzzles, to run incomplete code, or to ``invert'' a program, by searching for inputs that produce a desired output.  For example, we can ask the solver to search for two distinct legal inputs, @racket[l] and @racket[h], whose midpoint is the bitwise-and of their bits:
+Angelic execution can be used to solve puzzles, to run incomplete code, or to "invert" a program, by searching for inputs that produce a desired output.  For example, we can ask the solver to search for two distinct legal inputs, @racket[l] and @racket[h], whose midpoint is the bitwise-and of their bits: 
 @examples[#:eval rosette-eval #:label #f 
 (define (bvmid-fast lo hi)
   (bvlshr (bvadd hi lo) (bv #x00000001 32)))
@@ -482,7 +480,7 @@ n2
 n3]
 In general, recursion terminates under symbolic evaluation only when the stopping condition is reached with concrete values.
 
-We can force termination by placing a concrete bound @var{k} on the number of times @racket[bvsqrt] can call itself recursively. This approach is called @deftech{finitization}, and it is the standard way to handle unbounded loops and recursion under symbolic evaluation. The following code shows how to implement a @emph{sound} finitization policy. If a @racket[verify] query returns @racket[(unsat)] under a sound policy, we know that (1) the unrolling bound @var{k} is sufficient to execute all possible inputs to  @racket[bvsqrt], and (2) all of these executions satisfy the query. If we pick a bound that is too small, the query will generate a counterexample input that needs a larger bound to compute the result. In our example, the bound of 16 is sufficient to verify the correctness of @racket[bvsqrt] on all inputs:
+We can force termination by placing a concrete bound @var{k} on the number of times @racket[bvsqrt] can call itself recursively. This approach is called @deftech{finitization}, and it is the standard way to handle unbounded loops and recursion under symbolic evaluation. The following code shows how to implement a @emph{sound} finitization policy. If a @racket[verify] query returns @racket[(unsat)] under a sound policy, we know that (1) the unrolling bound @var{k} is sufficient to execute all possible inputs to  @racket[bvsqrt], and (2) all of these executions satisfy the query. If we pick a bound that is too small, the query will generate a counterexample input that needs a larger bound to compute the result. In our example, the bound of 16 is sufficient to verify the correctness of @racket[sqrt] on all inputs: 
 @(rosette-eval '(clear-vc!))
 @(rosette-eval '(require (only-in racket make-parameter parameterize)))
 @examples[#:eval rosette-eval #:label #f #:no-prompt

rosette/guide/scribble/forms/forms.scrbl

@@ -5,7 +5,7 @@
 
 @title[#:tag "ch:syntactic-forms" #:style 'toc]{Syntactic Forms}
 
-The core of the Rosette language (@racketmodname[rosette/safe]) consists of two kinds of syntax forms: a set of basic  forms @deftech[#:key "lifted constructs"]{lifted} from Racket, and a set of forms for @seclink["ch:essentials"]{solver-aided programming}.  We use the term ``lifted'' to refer to parts of the Racket language that can be used with symbolic values and other solver-aided constructs.
+The core of the Rosette language (@racket[rosette/safe]) consists of two kinds of syntax forms: a set of basic  forms @deftech[#:key "lifted constructs"]{lifted} from Racket, and a set of forms for @seclink["ch:essentials"]{solver-aided programming}.  We use the term "lifted" to refer to parts of the Racket language that can be used with symbolic values and other solver-aided constructs.
 
 @[table-of-contents]
 @include-section["racket-forms.scrbl"]

rosette/guide/scribble/libs/libraries.scrbl

@@ -4,7 +4,7 @@
 
 @title[#:tag "ch:libraries" #:style 'toc]{Libraries}
 
-Chapters @seclink["ch:getting-started"]{1}-@seclink["ch:programmer-defined-datatypes"]{5} introduce the basic constructs and datatypes for programming in Rosette. This chapter describes the parts of the core Racket libraries (e.g., I/O procedures) that are exported by @racketmodname[rosette/safe], as well as Rosette libraries that provide additional facilities for solver-aided development.
+Chapters @seclink["ch:getting-started"]{1}-@seclink["ch:programmer-defined-datatypes"]{5} introduce the basic constructs and datatypes for programming in Rosette. This chapter describes the parts of the core Racket libraries (e.g., I/O procedures) that are exported by @racket[rosette/safe], as well as Rosette libraries that provide additional facilities for solver-aided development.
 
 @[table-of-contents]
 

rosette/guide/scribble/libs/racket-libs.scrbl

@@ -17,4 +17,5 @@ Rosette exports the following facilities from the core Racket libraries:
 
 These facilities are safe to use in Rosette programs, even in the presence of symbolic values, assertions, and solver-aided queries. They are not, however, @tech[#:key "lifted constructs"]{lifted}:  if their Racket implementation expects a concrete value of a given type, they will fail when given a symbolic value.  These constructs are safe to use in the sense that they will fail in a predictable fashion, according to their concrete Racket specification, instead of causing the enclosing Rosette program to exhibit unexpected behavior.
 
-The @racketmodname[rosette/safe] language allows programs to import arbitrary Racket code using the standard @racket[require] mechanism.  This is strongly discouraged, however, unless the use of such code obeys the restrictions outlined in the @seclink["ch:unsafe"]{Chapter 8}.  Violating these restrictions may lead to incorrect program behavior, crashes, and loss of data (for programs that perform external side-effects, such as writing to files).  In other words, arbitrary Racket code is, by default, unsafe to use.
+The @racket[rosette/safe] language allows programs to import arbitrary Racket code using the standard @racket[require] mechanism.  This is strongly discouraged, however, unless the use of such code obeys the restrictions outlined in the @seclink["ch:unsafe"]{Chapter 8}.  Violating these restrictions may lead to incorrect program behavior, crashes, and loss of data (for programs that perform external side-effects, such as writing to files).  In other words, arbitrary Racket code is, by default, unsafe to use.
+

rosette/guide/scribble/libs/rosette-libs.scrbl

@@ -367,7 +367,7 @@ sol
   generated for programs that have been saved to disk.
 
   This procedure cooperates with the constructs in the
-  @racketmodname[rosette/lib/synthax] library to turn solutions into
+  @racket[rosette/lib/synthax] library to turn solutions into
   code. It works by scanning program files for
   @racketlink[??]{constant}, @racketlink[choose]{choice}, and
   @racketlink[define-grammar]{grammar} holes, and replacing

rosette/guide/scribble/performance/performance.scrbl

@@ -55,7 +55,7 @@ integers and reals (while being correct under the
 finite-precision semantics). For example, this program
 incorrectly says that no integer greater than 15 exists,
 because the setting of @racket[current-bitwidth] causes it
-to consider only values of @racket[x] that can be
+to consider only values of @racket{x} that can be
 represented as a 5-bit bitvector.
 
 @examples[#:eval rosette-eval #:label #f
@@ -387,15 +387,15 @@ the performance of @tt{verify-xform} to degrade, from a
 couple of seconds when @tt{N} = 5 to over a minute when @tt{N}
 = 20. To identify the source of this performance issue, we
 can invoke the @tech{symbolic profiler} on the verifier,
-producing the output below (after selecting the ``Collapse
+producing the output below (after selecting the "Collapse
-solver time'' checkbox):
+solver time" checkbox):
 
 @(image profile-xform.png #:scale 0.425)
 
 The symbolic profiler identifies @tt{list-set} as the
 bottleneck in this program. The output shows that @tt{list-set}
 creates many symbolic terms, and performs many symbolic
-operations (the ``Union Size'' and ``Merge Cases'' columns).
+operations (the "Union Size" and "Merge Cases" columns).
 
 The core issue here is an @tech{algorithmic mismatch}: @tt{list-set}
 makes a recursive call guarded by a short-circuiting

rosette/guide/scribble/reflection/value-reflection.scrbl

@@ -241,8 +241,8 @@ as well as for tuning the performance of symbolic
 evaluation.
 
 
-@declare-exporting[rosette/base/core/forall
+@declare-exporting[rosette/base/core/forall rosette/lib/lift
-                   #:use-sources (rosette/base/core/forall)]
+                   #:use-sources (rosette/base/core/forall rosette/lib/lift)]
 
 @defform[(for/all ([id val-expr maybe-exhaustive]) body ...+)
          #:grammar [(maybe-exhaustive (code:line) #:exhaustive)]]{

rosette/guide/scribble/refs.scrbl

@@ -9,28 +9,21 @@
 
 @(define rosette:onward13
    (make-bib
-     #:title @hyperlink["http://dl.acm.org/citation.cfm?id=2509586"]{Growing Solver-Aided Languages with Rosette}
+     #:title @hyperlink["http://homes.cs.washington.edu/~emina/pubs/rosette.onward13.pdf"]{Growing Solver-Aided Languages with Rosette}
      #:author (authors "Emina Torlak" "Rastislav Bodik")
      #:date 2013
      #:location "New Ideas, New Paradigms, and Reflections on Programming and Software (Onward!)"))
 
 @(define rosette:pldi14
    (make-bib
-    #:title @hyperlink["http://dl.acm.org/citation.cfm?id=2594340"]{A Lightweight Symbolic Virtual Machine for Solver-Aided Host Languages}
+    #:title @hyperlink["http://homes.cs.washington.edu/~emina/pubs/rosette.pldi14.pdf"]{A Lightweight Symbolic Virtual Machine for Solver-Aided Host Languages}
     #:author (authors "Emina Torlak" "Rastislav Bodik")
     #:date 2014
     #:location "Programming Language Design and Implementation (PLDI)"))
 
 @(define sympro:oopsla18
    (make-bib
-    #:title @hyperlink["https://dl.acm.org/citation.cfm?id=3276519"]{Finding Code That Explodes Under Symbolic Evaluation}
+    #:title @hyperlink["https://unsat.cs.washington.edu/papers/bornholt-sympro.pdf"]{Finding Code That Explodes Under Symbolic Evaluation}
     #:author (authors "James Bornholt" "Emina Torlak")
     #:date 2018
     #:location "Object Oriented Programming, Systems, Languages, and Applications (OOPSLA)"))
-
-@(define rosette:popl22
-   (make-bib
-    #:title @hyperlink["https://doi.org/10.1145/3498709"]{A Formal Foundation for Symbolic Evaluation with Merging}
-    #:author (authors "Sorawee Porncharoenwase" "Luke Nelson" "Xi Wang" "Emina Torlak")
-    #:date 2022
-    #:location "Principles of Programming Languages (POPL)"))

rosette/guide/scribble/unsafe/unsafe.scrbl

@@ -4,7 +4,7 @@
 @(require (for-label rosette/base/form/define rosette/query/query rosette/solver/solution
                      (only-in rosette/base/base assert vc-true? vc) )
           racket/runtime-path racket/sandbox)
-@(require (only-in "../refs.scrbl" ~cite rosette:pldi14 rosette:popl22))
+@(require (only-in "../refs.scrbl" ~cite rosette:pldi14))
 @(require "../util/lifted.rkt")
 
 @(define-runtime-path root ".")
@@ -13,20 +13,20 @@
 @title[#:tag "ch:unsafe"]{Unsafe Operations}
 
 Throughout this guide, we have assumed that Rosette programs are 
-written in the @racketmodname[rosette/safe] dialect of the full language.
+written in the @racket[rosette/safe] dialect of the full language.  
 This dialect extends a core subset of Racket with @seclink["ch:essentials"]{solver-aided 
-functionality}.  In this chapter, we briefly discuss the @racketmodname[rosette]
+functionality}.  In this chapter, we briefly discuss the @racket[rosette] 
 dialect of the language, which exports all of Racket.  
 
-Safe use of the full @racketmodname[rosette] language requires a basic understanding
+Safe use of the full @racket[rosette] language requires a basic understanding 
-of how Rosette's Symbolic Virtual Machine (SVM) works  @~cite[rosette:pldi14 rosette:popl22].  
+of how Rosette's Symbolic Virtual Machine (SVM) works  @~cite[rosette:pldi14].  
 Briefly, the SVM hijacks the normal Racket execution for all procedures and 
-constructs that are exported by @racketmodname[rosette/safe].  Any programs that are
+constructs that are exported by @racket[rosette/safe].  Any programs that are 
-implemented exclusively in the @racketmodname[rosette/safe] language are therefore
+implemented exclusively in the @racket[rosette/safe] language are therefore 
 fully under the SVM's control.  This means that the SVM can correctly interpret 
 the application of a procedure or a macro to a symbolic value, and it 
 can correctly handle any side-effects (in particular, writes to memory) performed 
-by @racketmodname[rosette/safe] code.
+by @racket[rosette/safe] code.
 
 The following snippet demonstrates the non-standard execution that the SVM needs to 
 perform in order to assign the expected meaning to Rosette code:
@@ -53,17 +53,17 @@ y
 (define sol2 (solve (assert (not b))))
 (evaluate y sol2)]
 
-Because the SVM controls only the execution of @racketmodname[rosette/safe] code,
+Because the SVM controls only the execution of @racket[rosette/safe] code, 
-it cannot, in general, guarantee the safety or correctness of arbitrary @racketmodname[rosette] programs.
+it cannot, in general, guarantee the safety or correctness of arbitrary @racket[rosette] programs. 
-As soon as a @racketmodname[rosette] program calls an @tech[#:key "lifted construct"]{unlifted} Racket construct
+As soon as a @racket[rosette] program calls an @tech[#:key "lifted construct"]{unlifted} Racket construct  
-(that is, a procedure or a macro not implemented in or provided by the @racketmodname[rosette/safe] language),
+(that is, a procedure or a macro not implemented in or provided by the @racket[rosette/safe] language), 
 the execution escapes back to the Racket interpreter.  The SVM has no control over the side-effects 
 performed by the Racket interpreter, or the meaning that it (perhaps incorrectly) assigns to programs 
 in the presence of symbolic values.  As a result, the programmer is responsible for ensuring that 
-a @racketmodname[rosette] program continues to behave correctly after the execution returns from the Racket interpreter.
+a @racket[rosette] program continues to behave correctly after the execution returns from the Racket interpreter.
 
-As an example of incorrect behavior, consider the following @racketmodname[rosette] snippet.
+As an example of incorrect behavior, consider the following @racket[rosette] snippet.  
-The procedures @racket[make-hash], @racket[hash-ref], and @racket[hash-clear!] are not in @racketmodname[rosette/safe].
+The procedures @racket[make-hash], @racket[hash-ref], and @racket[hash-clear!] are not in @racket[rosette/safe].
 Whenever they are invoked, the execution escapes to the Racket interpreter.
 
 @(rosette-eval '(require (only-in racket make-hash hash-clear! hash-ref)))

rosette/guide/scribble/welcome/welcome.scrbl

@@ -16,13 +16,13 @@ Rosette is a @emph{solver-aided} programming system with two components:
                 compiles them to logical constraints.  The SVM enables Rosette 
                 to use the solver to automatically reason about program behaviors.}]
 
-The name ``Rosette'' refers both to the language and the whole system.
+The name "Rosette" refers both to the language and the whole system.
 
 @section[#:tag "sec:get"]{Installing Rosette}
 
 To install Rosette, you will need to
 
-@itemlist[@item{Download and install @hyperlink["http://racket-lang.org"]{Racket} (version 8.1 or later).}
+@itemlist[@item{Download and install @hyperlink["http://racket-lang.org"]{Racket} (version 8.0 or later).}
            @item{Use Racket's @tt{raco} tool to install Rosette:
                  @nested{
                          @verbatim|{> raco pkg install rosette}|}}]

rosette/info.rkt

@@ -14,7 +14,10 @@
      (experimental))))
      ;; Documentation category. On Racket 6.3+ this can be any string.
 
-(define compile-omit-files '("lib/trace/report/node_modules"))
+;; Runs the code in `private/install.rkt` before installing this collection.
+(define pre-install-collection "private/install.rkt")
+(define compile-omit-files '("private/install.rkt"
+                             "lib/trace/report/node_modules"))
 
 (define raco-commands
   '(("symprofile"

rosette/lib/destruct.rkt

@@ -48,11 +48,10 @@
 
 (define-simple-macro (destruct val [pat:clause-pattern e:expr ...+] ...)
   #:do [(for-each check-duplicate-identifier! (attribute pat.id-set))]
-  #:with match-expr (syntax/loc this-syntax (match var [pat (begin e ...)] ...))
   #:with result
   (syntax/loc this-syntax
     (for/all ([var val]);(guarded-values val)])
-      match-expr))
+      (match var [pat (begin e ...)] ...)))
   result)
 
 (define-simple-macro (destruct* (val ...) [(pat:clause-pattern ...) e:expr ...+] ...)

rosette/lib/profile/raco.rkt

@@ -40,7 +40,7 @@
                  "Only install the compile handler; do not run the profiler"
                  (run-profiler? #f)]
                 [("-m" "--module") name
-                 "Run submodule <name> (defaults to 'main')"
+                 "Run submodule <name> (defaults to 'main)"
                  (module-name (string->symbol name))]
                 [("-r" "--racket")
                  "Instrument code in any language, not just `#lang rosette`"

rosette/lib/profile/record.rkt

@@ -78,13 +78,8 @@
              ; all events from the box. if that happened then the ENTER we're trying
              ; to delete has already been published, and so we need to retain the
              ; corresponding EXIT.
-             (let loop ()
              (unless (box-cas! the-box evts (cdr evts))
-                 (if (eq? evts (unbox the-box))
+               (do-record-exit! out))]))))))
-                     ; spurious CAS failure; retry
-                     (loop)
-                     ; box has changed, so we need to retain the EXIT
-                     (do-record-exit! out))))]))))))
 
 ; Default version just uses the current-profile/current-reporter params
 (define default-record-exit

rosette/lib/synthax.rkt

@@ -296,4 +296,4 @@
 (define (print-forms sol)
   (for ([f (generate-forms sol)])
     (printf "~a:~a:~a\n" (syntax-source f) (syntax-line f) (syntax-column f))
-    (pretty-write (syntax->datum f))))
+    (pretty-print (syntax->datum f))))

rosette/lib/trace/raco.rkt

@@ -29,7 +29,7 @@
 
    ;; SymPro options
    [("-m" "--module") name
-                      "Run submodule <name> (defaults to 'main')"
+                      "Run submodule <name> (defaults to 'main)"
                       (module-name (string->symbol name))]
    [("-r" "--racket")
     "Instrument code in any language, not just `#lang rosette`"

rosette/lib/util/module.rkt

@@ -21,8 +21,6 @@
   (string-prefix? (path->string (resolve-path a))
                   (path->string (resolve-path b))))
 
-(define pkg-cache (make-hash))
-
 (define (make-rosette-load/use-compiled pkgs-to-instrument)
   (make-custom-load/use-compiled
    #:blacklist
@@ -30,6 +28,6 @@
      (cond
        [(path-prefix? path (find-collects-dir)) #f]
        [else
-        (match (path->pkg path #:cache pkg-cache)
+        (match (path->pkg path)
           [#f #t]
           [pkg-name (member pkg-name pkgs-to-instrument)])]))))

rosette/lib/util/streaming-server.rkt

@@ -14,7 +14,6 @@
   ; the procedure for handling connections
   (define (ws-connection conn _state)
     ; only one client may connect
-    (let loop ()
     (cond
       [(box-cas! connected? #f #t)  ; we won the race to connect
        ; tell the main thread we're connected
@@ -43,11 +42,9 @@
                   (unless (eq? sync-result 'finish)
                     (channel-get channel))
                   (channel-put channel 'finish)]))))]
-        [(unbox connected?)
+      [else
-         ;; it's already connected
        (channel-put channel "another client is already connected")
-         (ws-close! conn)]
+       (ws-close! conn)]))
-        [else (loop)])))
 
   ; start the server
   (define conf-channel (make-async-channel))

rosette/private/install.rkt

@@ -0,0 +1,107 @@
+#lang racket/base
+
+;; Check whether z3 is installed during package setup.
+;; If missing, builds & links a z3 binary.
+
+
+(provide pre-installer)
+
+(require racket/match
+         racket/file
+         racket/port
+         net/url
+         file/unzip)
+
+(define (print-failure path msg)
+  (printf "\n\n********** Failed to install Z3 **********\n\n")
+  (printf "You'll need to manually install a Z3 binary\n")
+  (printf "to this location: ~a\n\n" path)
+  (printf "The problem was:\n~a\n\n" msg)
+  (printf "*********\n\n\n"))
+
+(define (pre-installer collections-top-path racl-path)
+  (define bin-path (simplify-path (build-path racl-path ".." "bin")))
+  (define z3-path (build-path bin-path "z3"))
+  (with-handlers ([exn:fail? (lambda (e) (print-failure z3-path (exn-message e)))])
+    (unless (custom-z3-symlink? z3-path)
+      (define-values (z3-url z3-path-in-zip) (get-z3-url))
+      (define z3-port (get-pure-port (string->url z3-url) #:redirections 10))  
+      (make-directory* bin-path) ;; Ensure that `bin-path` exists
+      (delete-directory/files z3-path #:must-exist? #f) ;; Delete old version of Z3, if any
+      (parameterize ([current-directory bin-path])    
+        (call-with-unzip z3-port
+                         (λ (dir)
+                           (copy-directory/files (build-path dir z3-path-in-zip) z3-path)))
+        ;; Unzipping loses file permissions, so we reset the z3 binary here
+        (file-or-directory-permissions 
+          z3-path 
+          (if (equal? (system-type) 'windows) #o777 #o755))))))
+
+(define (custom-z3-symlink? z3-path)
+  (and (file-exists? z3-path)
+       (let ([p (simplify-path z3-path)])
+         (not (equal? (resolve-path p) p)))))
+
+(define (get-z3-url)
+  (define site "https://github.com/Z3Prover/z3/releases/download")
+  (define version "z3-4.8.8")
+  (define-values (os exe)
+    (match (list (system-type) (system-type 'word))
+      ['(unix 64)    (values "x64-ubuntu-16.04" "z3")]
+      [`(macosx ,_)  (values "x64-osx-10.14.6" "z3")]
+      ['(windows 64) (values "x64-win" "z3.exe")]
+      [any           (raise-user-error 'get-z3-url "Unknown system type '~a'" any)]))
+  (define name (format "~a-~a" version os))
+  (values
+   (format "~a/~a/~a.zip" site version name)
+   (format "~a/bin/~a" name exe)))
+
+
+;; A copy of net/url's get-pure-port/headers, except with the Location header
+;; for redirects made case-insensitive, fixing https://github.com/racket/racket/pull/3057
+(require net/http-client net/url-connect)
+(define (get-pure-port url #:redirections [redirections 0])
+  (let redirection-loop ([redirections redirections] [url url])
+    (define hc (http-conn-open (url-host url)
+                               #:ssl? (if (equal? "https" (url-scheme url))
+                                          (current-https-protocol)
+                                          #f)))
+    (define access-string
+      (url->string
+       ;; RFCs 1945 and 2616 say:
+       ;;   Note that the absolute path cannot be empty; if none is present in
+       ;;   the original URI, it must be given as "/" (the server root).
+       (let-values ([(abs? path)
+                     (if (null? (url-path url))
+                         (values #t (list (make-path/param "" '())))
+                         (values (url-path-absolute? url) (url-path url)))])
+         (make-url #f #f #f #f abs? path (url-query url) (url-fragment url)))))
+    (http-conn-send! hc access-string #:method #"GET" #:content-decode '())
+    (define-values (status headers response-port)
+      (http-conn-recv! hc #:method #"GET" #:close? #t #:content-decode '()))
+
+    (define new-url
+      (ormap (λ (h)
+               (match (regexp-match #rx#"^[Ll]ocation: (.*)$" h)
+                 [#f #f]
+                 [(list _ m1b)
+                  (define m1 (bytes->string/utf-8 m1b))
+                  (with-handlers ((exn:fail? (λ (x) #f)))
+                    (define next-url (string->url m1))
+                    (make-url
+                     (or (url-scheme next-url) (url-scheme url))
+                     (or (url-user next-url) (url-user url))
+                     (or (url-host next-url) (url-host url))
+                     (or (url-port next-url) (url-port url))
+                     (url-path-absolute? next-url)
+                     (url-path next-url)
+                     (url-query next-url)
+                     (url-fragment next-url)))]))
+             headers))
+    (define redirection-status-line?
+      (regexp-match #rx#"^HTTP/[0-9]+[.][0-9]+ 3[0-9][0-9]" status))
+    (cond
+      [(and redirection-status-line? new-url (not (zero? redirections)))
+       (redirection-loop (- redirections 1) new-url)]
+      [else
+       response-port])))

rosette/query/core.rkt

@@ -150,12 +150,12 @@
 ; ∃H. (∀I. assumes => asserts) ∧ (∃I. assumes).
 (define (cegis inputs assumes asserts guesser checker)
   
-  (define  φ `(,(=> (apply && assumes) (apply && asserts))))
+  (define φ   (append assumes asserts))
   
   (define ¬φ `(,@assumes ,(apply || (map ! asserts))))
   
-  (define (guess ψ)
+  (define (guess sol)
-    (solver-assert guesser ψ)
+    (solver-assert guesser (evaluate φ sol))
     (match (solver-check guesser)
       [(model m) (sat (for/hash ([(c v) m] #:unless (member c inputs)) (values c v)))]
       [other other]))
@@ -171,14 +171,14 @@
                                          v)))))]
       [other other]))
     
-  (let loop ([candidate (guess (append assumes asserts))])
+  (let loop ([candidate (begin0 (guess (sat)) (solver-clear guesser))])
     (cond 
       [(unsat? candidate) candidate]
       [else
         (let ([cex (check candidate)])
           (cond 
             [(unsat? cex) candidate]
-            [else (loop (guess (evaluate φ cex)))]))])))
+            [else (loop (guess cex))]))])))
 
 
         

rosette/query/eval.rkt

@@ -47,10 +47,7 @@
                [(cons x y)               
                 (cons (eval-rec x sol cache) (eval-rec y sol cache))]
                [(? vector?)              
-                (let ([v (for/vector #:length (vector-length expr) ([e expr]) (eval-rec e sol cache))])
+                (for/vector #:length (vector-length expr) ([e expr]) (eval-rec e sol cache))]
-                  (if (immutable? expr)
-                      (vector->immutable-vector v)
-                      v))]
                [(? box?)
                 ((if (immutable? expr) box-immutable box) (eval-rec (unbox expr) sol cache))]
                [(? typed?)              

rosette/query/form.rkt

@@ -1,7 +1,6 @@
 #lang racket
 
-(require syntax/parse/define
+(require "core.rkt" 
-         "core.rkt"
          (only-in "../base/core/reflect.rkt" symbolics)
          (only-in "../base/core/result.rkt" result-state)
          (only-in "../base/core/bool.rkt" ! vc with-vc vc-assumes vc-asserts vc-true))
@@ -71,15 +70,14 @@
 ; generate any assumptions or assertions, these are reflected in the (vc) after
 ; the optimize query returns. The assumptions and assertions generated by expr
 ; are not added to (vc) after optimize returns.
-(define-syntax-parser optimize
+(define-syntax optimize
-  [(_ {~and kw {~or* #:minimize #:maximize}} opt #:guarantee expr)
+  (syntax-rules ()
-   #'(let ([obj opt]    ; evaluate objective first to add its spec to (vc)
+    [(_ kw opt #:guarantee expr)
+     (let ([obj opt]    ; evaluate objective first to add its spec to (vc)
            [post (query-vc expr)])
        (∃-solve `(,@(pre) ,(vc-assumes post) ,(vc-asserts post)) kw obj))]
-  [(_ {~and kw1 {~or* #:minimize #:maximize}} opt1
+    [(_ kw1 opt1 kw2 opt2 #:guarantee expr)
-      {~and kw2 {~or* #:minimize #:maximize}} opt2
+     (let ([obj1 opt1]  ; evaluate objectives first to add their spec to (vc)
-      #:guarantee expr)
-   #'(let ([obj1 opt1]  ; evaluate objectives first to add their spec to (vc)
            [obj2 opt2]
            [post (query-vc expr)])  
-       (∃-solve `(,@(pre) ,(vc-assumes post) ,(vc-asserts post)) kw1 obj1 kw2 obj2))])
+       (∃-solve `(,@(pre) ,(vc-assumes post) ,(vc-asserts post)) kw1 obj1 kw2 obj2))]))

rosette/solver/smt/base-solver.rkt

@@ -12,8 +12,6 @@
 
 (provide (all-defined-out))
 
-(define (unique/reverse xs)
-  (reverse (unique xs)))
 
 (define (find-solver binary base-path [user-path #f])
   (cond
@@ -44,15 +42,14 @@
   (unless (list? bools)
     (raise-argument-error 'solver-assert "(listof boolean?)" bools))
   (define wfcheck-cache (mutable-set))
-  (set-solver-asserts!
+  (set-solver-asserts! self 
-   self
+    (append (solver-asserts self)
-   (append (for/list ([b bools] #:unless (equal? b #t))
+            (for/list ([b bools] #:unless (equal? b #t))
               (unless (or (boolean? b) (and (term? b) (equal? @boolean? (term-type b))))
                 (error 'assert "expected a boolean value, given ~s" b))
               (when wfcheck
                 (wfcheck b wfcheck-cache))
-             b)
+              b))))
-           (solver-asserts self))))
 
 (define (solver-minimize self nums)
   (unless (null? nums)
@@ -71,7 +68,7 @@
   (server-shutdown (solver-server self)))
 
 (define (solver-push self)
-  (match-define (solver server _ (app unique asserts) (app unique/reverse mins) (app unique/reverse maxs) env level) self)
+  (match-define (solver server _ (app unique asserts) (app unique mins) (app unique maxs) env level) self)
   (server-write
    server
    (begin
@@ -93,7 +90,7 @@
   (set-solver-level! self (drop level k)))
      
 (define (solver-check self [read-solution read-solution])
-  (match-define (solver server _ (app unique asserts) (app unique/reverse mins) (app unique/reverse maxs) env _) self)
+  (match-define (solver server _ (app unique asserts) (app unique mins) (app unique maxs) env _) self)
   (cond [(ormap false? asserts) (unsat)]
         [else (server-write
                server
@@ -134,9 +131,7 @@
 ; core was extracted); #f (if the solution is 
 ; 'unsat and no core was extracted); or 'unknown otherwise.
 (define (read-solution server env #:unsat-core? [unsat-core? #f])
-  (decode (parse-solution server #:unsat-core? unsat-core?) env))
+  (decode
-
-(define (parse-solution server #:unsat-core? [unsat-core? #f])
    (parameterize ([current-readtable (make-readtable #f #\# #\a #f)]) ; read BV literals as symbols
      (match (server-read server (read))
        [(== 'sat)
@@ -144,11 +139,7 @@
         (let loop ()
           (match (server-read server (read))
             [(list (== 'objectives) _ ...) (loop)]
-           ; The SMT-LIB spec says that a model should be just a list of
+            [(list (== 'model) def ...)
-           ; `define-fun`s, but many SMT solvers used to prefix that list
-           ; with `model`, so let's support both versions.
-           ; https://groups.google.com/g/smt-lib/c/5xpcIxdQ8-A/m/X4uQ7dIgAwAJ
-           [(or (list (== 'model) def ...) (list def ...))
              (for/hash ([d def] #:when (and (pair? d) (equal? (car d) 'define-fun)))
                (values (cadr d) d))]
             [other (error 'read-solution "expected model, given ~a" other)]))]
@@ -161,4 +152,5 @@
                 [other (error 'read-solution "expected unsat core, given ~a" other)]))
             'unsat)]
        [(== 'unknown) 'unknown]
-      [other (error 'read-solution "unrecognized solver output: ~a" other)])))
+       [other (error 'read-solution "unrecognized solver output: ~a" other)]))
+   env))

rosette/solver/smt/bitwuzla.rkt

@@ -1,106 +0,0 @@
-;;; Requires Bitwuzla 0.1.0 or later.
-#lang racket
-
-(require racket/runtime-path 
-         "server.rkt" "cmd.rkt" "env.rkt" 
-         "../solver.rkt" "../solution.rkt"
-         (prefix-in base/ "base-solver.rkt")
-         (only-in "../../base/core/term.rkt" term term? term-type constant? expression constant with-terms)
-         (only-in "../../base/core/bool.rkt" @boolean? @forall @exists)
-         (only-in "../../base/core/bitvector.rkt" bitvector bitvector? bv? bv bv-value @extract @sign-extend @zero-extend @bveq)
-         (only-in "../../base/core/function.rkt" function-domain function-range function? function fv)
-         (only-in "../../base/core/type.rkt" type-of)
-         (only-in "../../base/form/control.rkt" @if))
-
-(provide (rename-out [make-bitwuzla bitwuzla]) bitwuzla? bitwuzla-available?)
-
-(define-runtime-path bitwuzla-path (build-path ".." ".." ".." "bin" "bitwuzla"))
-(define bitwuzla-opts '("-m"))
-
-(define (bitwuzla-available?)
-  (not (false? (base/find-solver "bitwuzla" bitwuzla-path #f))))
-
-(define (make-bitwuzla [solver #f] #:options [options (hash)] #:logic [logic #f] #:path [path #f])
-  (define config
-    (cond
-      [(bitwuzla? solver)
-       (base/solver-config solver)]
-      [else
-       (define real-bitwuzla-path (base/find-solver "bitwuzla" bitwuzla-path path))
-       (when (and (false? real-bitwuzla-path) (not (getenv "PLT_PKG_BUILD_SERVICE")))
-         (error 'bitwuzla "bitwuzla binary is not available (expected to be at ~a); try passing the #:path argument to (bitwuzla)" (path->string (simplify-path bitwuzla-path))))
-       (base/config options real-bitwuzla-path logic)]))
-  (bitwuzla (server (base/config-path config) bitwuzla-opts (base/make-send-options config)) config '() '() '() (env) '()))
-
-(struct bitwuzla base/solver ()
-  #:property prop:solver-constructor make-bitwuzla
-  #:methods gen:custom-write
-  [(define (write-proc self port mode) (fprintf port "#<bitwuzla>"))]
-  #: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 bitwuzla-wfcheck))
-
-   (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 [read-solution base/read-solution])
-     (base/solver-check self read-solution))
-   
-   (define (solver-debug self)
-     (base/solver-debug self))])
-
-(define (set-default-options server)
-  void)
-
-
-(define (valid-type? t)
-    (or (equal? t @boolean?)
-        (bitvector? t)
-        (and (function? t)
-             (for/and ([d (in-list (function-domain t))]) (valid-type? d))
-             (valid-type? (function-range t)))))
-; Check whether a term v is well-formed for bitwuzla -- it must not mention
-; types other than bitvectors, booleans, and uninterpreted functions over those
-; types. If not, raise an exception.
-(define (bitwuzla-wfcheck v [cache (mutable-set)])
-  (unless (set-member? cache v)
-    (set-add! cache v)
-    (cond
-      [(term? v)
-       (unless (valid-type? (type-of v))
-         (error 'bitwuzla "bitwuzla does not support values of type ~v (value: ~v)" (type-of v) v))
-       (match v
-         [(expression (or (== @forall) (== @exists)) vars body)
-          (error 'bitwuzla "bitwuzla does not support quantified formulas (value: ~v)" v)]
-         [(expression (== @extract) i j e)
-          (bitwuzla-wfcheck e cache)]
-         [(expression (or (== @sign-extend) (== @zero-extend)) v t)
-          (bitwuzla-wfcheck v cache)]
-         [(expression op es ...)
-          (for ([e es]) (bitwuzla-wfcheck e cache))]
-         [_ #t])]
-      [else
-       (unless (or (boolean? v) (bv? v))
-         (error 'bitwuzla "bitwuzla does not support value (expected boolean? or bv?): ~v" v))])))

rosette/solver/smt/boolector.rkt

@@ -107,10 +107,28 @@
 
 
 ; Reads the SMT solution from the server.
-; This is the same as `base/read-solution` except that it applies some fixups
+; The solution consists of 'sat or 'unsat, followed by  
-; for quirks in how various versions of Boolector have emitted models.
+; followed by a suitably formatted s-expression.  The 
+; output of this procedure is a hashtable from constant 
+; identifiers to their SMTLib values (if the solution is 'sat);
+; a non-empty list of assertion identifiers that form an
+; unsatisfiable core (if the solution is 'unsat and a 
+; core was extracted); #f (if the solution is 
+; 'unsat and no core was extracted); or 'unknown otherwise.
 (define (boolector-read-solution server env)
-  (define raw-model (base/parse-solution server))
+  (define raw-model
+    (parameterize ([current-readtable (make-readtable #f #\# #\a #f)]) ; read BV literals as symbols
+       (match (server-read server (read))
+         [(== 'sat)
+          (server-write server (get-model))
+          (match (server-read server (read))
+            [(list (== 'model) def ...)
+             (for/hash ([d def] #:when (and (pair? d) (equal? (car d) 'define-fun)))
+               (values (cadr d) d))]
+            [other (error 'read-solution "expected model, given ~a" other)])]
+         [(== 'unsat) 'unsat]
+         [(== 'unknown) 'unknown]
+         [other (error 'read-solution "unrecognized solver output: ~a" other)])))
   ; First, we need to fix up the model's shadowing of incremental variables
   (define stripped-raw-model (if (hash? raw-model) (fixup-incremental-names raw-model) raw-model))
   ; Now decode in an environment with fake types for UFs

rosette/solver/smt/cvc5.rkt

@@ -1,68 +0,0 @@
-#lang racket
-
-(require racket/runtime-path 
-         "server.rkt" "env.rkt" 
-         "../solver.rkt"
-         (prefix-in base/ "base-solver.rkt"))
-
-(provide (rename-out [make-cvc5 cvc5]) cvc5? cvc5-available?)
-
-(define-runtime-path cvc5-path (build-path ".." ".." ".." "bin" "cvc5"))
-(define cvc5-opts '("-L" "smt2" "-q" "-m" "-i" "--bv-print-consts-as-indexed-symbols"))
-
-(define (cvc5-available?)
-  (not (false? (base/find-solver "cvc5" cvc5-path #f))))
-
-(define (make-cvc5 [solver #f] #:options [options (hash)] #:logic [logic #f] #:path [path #f])
-  (define config
-    (cond
-      [(cvc5? solver)
-       (base/solver-config solver)]
-      [else
-       (define real-cvc5-path (base/find-solver "cvc5" cvc5-path path))
-       (when (and (false? real-cvc5-path) (not (getenv "PLT_PKG_BUILD_SERVICE")))
-         (error 'cvc5 "cvc5 binary is not available (expected to be at ~a); try passing the #:path argument to (cvc5)" (path->string (simplify-path cvc5-path))))
-       (base/config options real-cvc5-path logic)]))
-  (cvc5 (server (base/config-path config) cvc5-opts (base/make-send-options config)) config '() '() '() (env) '()))
-
-(struct cvc5 base/solver ()
-  #:property prop:solver-constructor make-cvc5
-  #:methods gen:custom-write
-  [(define (write-proc self port mode) (fprintf port "#<cvc5>"))]
-  #: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)

rosette/solver/smt/dec.rkt

@@ -14,8 +14,7 @@
                   @bvslt @bvsle @bvult @bvule   
                   @bvnot @bvor @bvand @bvxor @bvshl @bvlshr @bvashr
                   @bvneg @bvadd @bvmul @bvudiv @bvsdiv @bvurem @bvsrem @bvsmod
-                  @z3_ext_rotate_left @z3_ext_rotate_right
+                  @concat @extract))
-                  @concat @extract @sign-extend @zero-extend))
 
 
 (provide decode-model)
@@ -117,6 +116,7 @@
         (hash-ref ~env id)]
        [(== true) #t]
        [(== false) #f]
+       [(? integer?) (inexact->exact expr)]
        [(? real?) expr]
        [(? symbol?)
         (cond
@@ -132,10 +132,6 @@
         (bv n (bitvector len))]
        [(list (list (== '_) (== 'extract) i j) s)
         `(, @extract ,(inline i sol ~env) ,(inline j sol ~env) ,(inline s sol ~env))]
-       [(list (list (== '_) (== 'sign_extend) i) s)
-        `(, @sign-extend ,(inline i sol ~env) ,(inline s sol ~env))]
-       [(list (list (== '_) (== 'zero_extend) i) s)
-        `(, @zero-extend ,(inline i sol ~env) ,(inline s sol ~env))]
        [(list (== 'let) binds body)
         (substitute (inline body sol ~env)
                     (for/hash ([id:expr binds])
@@ -166,7 +162,6 @@
         'bvslt @bvslt 'bvsle @bvsle 'bvult @bvult 'bvule @bvule   
         'bvnot @bvnot 'bvor @bvor 'bvand @bvand 'bvxor @bvxor
         'bvshl @bvshl 'bvlshr @bvlshr 'bvashr @bvashr
-        'ext_rotate_left @z3_ext_rotate_left 'ext_rotate_right @z3_ext_rotate_right
         'bvneg @bvneg 'bvadd @bvadd 'bvmul @bvmul
         'bvudiv @bvudiv 'bvsdiv @bvsdiv
         'bvurem @bvurem 'bvsrem @bvsrem

rosette/solver/smt/enc.rkt

@@ -16,7 +16,6 @@
                   @bvnot @bvor @bvand @bvxor @bvshl @bvlshr @bvashr
                   @bvneg @bvadd @bvmul @bvudiv @bvsdiv @bvurem @bvsrem @bvsmod
                   @concat @extract @zero-extend @sign-extend 
-                  @z3_ext_rotate_left @z3_ext_rotate_right
                   @integer->bitvector @bitvector->integer @bitvector->natural))
 
 (provide enc)
@@ -109,7 +108,6 @@
   [@bveq $=] [@bvslt $bvslt] [@bvsle $bvsle] [@bvult $bvult] [@bvule $bvule] 
   [@bvnot $bvnot] [@bvor $bvor] [@bvand $bvand] [@bvxor $bvxor] 
   [@bvshl $bvshl] [@bvlshr $bvlshr] [@bvashr $bvashr]
-  [@z3_ext_rotate_left $ext_rotate_left] [@z3_ext_rotate_right $ext_rotate_right]
   [@bvneg $bvneg] [@bvadd $bvadd] [@bvmul $bvmul] [@bvudiv $bvudiv] [@bvsdiv $bvsdiv]
   [@bvurem $bvurem] [@bvsrem $bvsrem] [@bvsmod $bvsmod] [@concat $concat])
 

rosette/solver/smt/smtlib2.rkt

@@ -68,8 +68,7 @@
   bvnot bvand bvor bvxor 
   bvule bvult bvuge bvugt bvsle bvslt bvsge bvsgt
   bvneg bvadd bvsub bvmul bvsdiv bvudiv bvurem bvsrem bvsmod
-  bvshl bvlshr bvashr concat
+  bvshl bvlshr bvashr concat) 
-  ext_rotate_left ext_rotate_right) 
 
 (define (extract i j s)
   `((_ extract ,i ,j) ,s))

rosette/solver/smt/stp.rkt

@@ -1,69 +0,0 @@
-#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)
-  

rosette/solver/smt/yices.rkt

@@ -1,9 +1,13 @@
 #lang racket
 
 (require racket/runtime-path 
-         "server.rkt" "env.rkt" 
+         "server.rkt" "env.rkt" "cmd.rkt"
          "../solver.rkt"
-         (prefix-in base/ "base-solver.rkt"))
+         (only-in "smtlib2.rkt" get-model echo)
+         (prefix-in base/ "base-solver.rkt")
+         (only-in "../../base/core/term.rkt" term? expression)
+         (only-in "../../base/core/bool.rkt" @forall @exists)
+         (only-in "../../base/core/bitvector.rkt"  @integer->bitvector))
 
 (provide (rename-out [make-yices yices]) yices? yices-available?)
 
@@ -11,17 +15,17 @@
 (define yices-opts '("--incremental"))
 
 (define (yices-available?)
-  (not (false? (base/find-solver "yices-smt2" yices-path #f))))
+  (not (false? (base/find-solver "yices" 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 (make-yices [solver #f] #:options [options (hash)] #:logic [logic 'ALL] #: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))
+       (define real-yices-path (base/find-solver "yices" 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))))
+         (error 'yices "yices 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) '()))
 
@@ -32,13 +36,13 @@
   #:methods gen:solver
   [
    (define (solver-features self)
-     '(qf_bv))
+     '(qf_bv qf_uf qf_lia qf_lra))
    
    (define (solver-options self)
      (base/solver-options self))
 
    (define (solver-assert self bools)
-     (base/solver-assert self bools))
+     (base/solver-assert self bools yices-wfcheck))
 
    (define (solver-minimize self nums)
      (base/solver-minimize self nums))
@@ -59,11 +63,85 @@
      (base/solver-pop self k))
    
    (define (solver-check self)
-     (base/solver-check self))
+     (base/solver-check self yices-read-solution))
    
    (define (solver-debug self)
      (base/solver-debug self))])
 
-(define (set-default-options server)
-  void)
 
+; Check whether a term v is well-formed for Yices -- it must not 
+; use integer->bitvector, which Yices doesn't support natively,
+; nor a quantifier.
+(define (yices-wfcheck v [cache (mutable-set)])
+  (unless (set-member? cache v)
+    (set-add! cache v)
+    (when (term? v)
+      (match v
+        [(expression (or (== @forall) (== @exists)) vars body)
+         (error 'yices "yices does not support quantified formulas (value: ~v)" v)]
+        [(expression (== @integer->bitvector) rest ...)
+         (error 'yices "yices does not support integer->bitvector (value: ~v)" v)]
+        [(expression op es ...)
+         (for ([e es]) (yices-wfcheck e cache))]
+        [_ #t]))))
+
+
+; Reads the SMT solution from the server.
+; The solution consists of 'sat or 'unsat, followed by  
+; followed by a suitably formatted s-expression.  The 
+; output of this procedure is a hashtable from constant 
+; identifiers to their SMTLib values (if the solution is 'sat);
+; a non-empty list of assertion identifiers that form an
+; unsatisfiable core (if the solution is 'unsat and a 
+; core was extracted); #f (if the solution is 
+; 'unsat and no core was extracted); or 'unknown otherwise.
+;
+; For Yices, we need to adapt to its strange way of printing models,
+; which are just a list of terms of the form (= x y), with no delimiters
+; for the start and end of a model. We print a "done" symbol to detect when
+; to stop reading terms. We also need to handle Yices' format for printing
+; uninterpreted functions:
+; (= x @fun_6)
+; (function @fun_6
+;  (type (-> int int))
+;  (= (@fun_6 0) 0)
+;  (= (@fun_6 1) 1)
+;  (default 2))
+; We convert these models into define-fun forms, with each case becoming
+; a nested ITE. The define-fun forms have fake type information, since
+; decode doesn't use it (preferring to use the type info from env).
+(define (yices-read-solution server env)
+  (define raw-model
+    (parameterize ([current-readtable (make-readtable #f #\# #\a #f)]) ; read BV literals as symbols
+       (match (server-read server (read))
+         [(== 'sat)
+          (server-write server
+            (get-model)
+            (echo "done"))
+          (let loop ([model (hash)][functions (hash)])
+            (match (server-read server (read))
+              [(list (== '=) var val)
+               (loop (hash-set model var `(define-fun ,var () X ,val)) functions)]
+              [(list (== 'function) var type cases ...)
+               (define args (for/list ([x (in-range (- (length (cadr type)) 2))]) (gensym)))
+               (define (call->guard call)
+                 (if (equal? (length args) 1)
+                     `(= ,(car args) ,(cadr call))
+                     `(and ,@(for/list ([a args][c (cdr call)]) `(= ,a ,c)))))
+               (define fun
+                 (let inner ([cases cases])
+                   (match (car cases)
+                     [(list (== 'default) val) val]
+                     [(list (== '=) call val)
+                      `(ite ,(call->guard call) ,val ,(inner (cdr cases)))])))
+               (loop model
+                     (hash-set functions var `(define-fun ,var ,(for/list ([a args]) `(,a X)) X ,fun)))]
+              ['done
+               (for/hash ([(var defn) (in-dict model)])
+                 (define val (fifth defn))
+                 (values var (hash-ref functions val defn)))]
+              [other (error 'read-solution "expected model, given ~a" other)]))]
+         [(== 'unsat) 'unsat]
+         [(== 'unknown) 'unknown]
+         [other (error 'read-solution "unrecognized solver output: ~a" other)])))
+  (decode raw-model env))

rosette/solver/smt/z3.rkt

@@ -30,9 +30,7 @@
       [else
        (define real-z3-path (base/find-solver "z3" z3-path path))
        (when (and (false? real-z3-path) (not (getenv "PLT_PKG_BUILD_SERVICE")))
-         (fprintf (current-error-port)
+         (printf "warning: could not find z3 executable at ~a\n" (path->string (simplify-path z3-path))))
-                  "warning: could not find z3 executable at ~a\n"
-                  (path->string (simplify-path z3-path))))
        (define opts (hash-union default-options options #:combine (lambda (a b) b)))
        (base/config opts real-z3-path logic)]))
   (z3 (server (base/config-path config) z3-opts (base/make-send-options config)) config '() '() '() (env) '()))
@@ -54,10 +52,10 @@
      (base/solver-assert self bools))
 
    (define (solver-minimize self nums)
-     (base/set-solver-mins! self (append (reverse (numeric-terms nums 'solver-minimize)) (base/solver-mins self))))
+     (base/set-solver-mins! self (append (base/solver-mins self) (numeric-terms nums 'solver-minimize))))
    
    (define (solver-maximize self nums)
-     (base/set-solver-maxs! self (append (reverse (numeric-terms nums 'solver-maximize)) (base/solver-maxs self))))
+     (base/set-solver-maxs! self (append (base/solver-maxs self) (numeric-terms nums 'solver-maximize))))
    
    (define (solver-clear self) 
      (base/solver-clear-stacks! self)

sdsl/fsm/lib.rkt

@@ -1,6 +1,7 @@
 #lang rosette
 
 (require 
+ rosette/lib/lift 
  (prefix-in racket/ (only-in racket string-append symbol->string regexp-match?)))
 
 (provide (all-defined-out))

test/all-rosette-tests.rkt

@@ -3,11 +3,7 @@
 (require (only-in rosette solver-features current-solver) "base/solver.rkt"
          rosette/lib/roseunit
          rosette/solver/smt/z3 rosette/solver/smt/cvc4 
-         rosette/solver/smt/boolector 
+         rosette/solver/smt/boolector rosette/solver/smt/yices
-         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)
@@ -42,7 +38,6 @@
  "base/distinct.rkt"
  "base/generics.rkt"
  "base/push-pop.rkt"
- "base/optimize-order.rkt"
  "base/reflect.rkt"
  "base/decode.rkt"
  "query/solve.rkt"
@@ -86,20 +81,8 @@
     (printf "===== Running Boolector tests =====\n")
     (run-tests-with-solver boolector))
 
-  (when (cvc5-available?)
-    (printf "===== Running cvc5 tests =====\n")
-    (run-tests-with-solver cvc5))
-
-  (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")
+    (printf "===== Running Yices tests =====\n")
     (run-tests-with-solver yices))
 )
 

test/base/bvlib.rkt

@@ -272,13 +272,13 @@
 (define tests:rotate-left
   (test-suite+
    "Tests for rotate-left in rosette/base/bvlib.rkt"
-   #:features '(qf_lia int2bv qf_bv)
+   #:features '(qf_lia qf_bv)
    (check-rotate rotate-left rotate-right bvrol)))
 
 (define tests:rotate-right
   (test-suite+
    "Tests for rotate-right in rosette/base/bvlib.rkt"
-   #:features '(qf_lia int2bv qf_bv)
+   #:features '(qf_lia qf_bv)
    (check-rotate rotate-right rotate-left bvror)))
 
 (module+ test

test/base/optimize-order.rkt

@@ -1,27 +0,0 @@
-#lang rosette
-
-;; This test is taken from https://www.philipzucker.com/z3-rise4fun/optimization.html
-
-(require rackunit rackunit/text-ui racket/generator
-         rosette/lib/roseunit)
-
-(current-bitwidth #f)
-(define-symbolic x y z integer?)
-
-(define (check-model sol m)
-  (check-pred sat? sol)
-  (check-equal? (model sol) m))
-
-(define optimization-order-tests
-  (test-suite+ "Tests for the optimization order"
-   #:features '(optimize)
-
-  (define solver (current-solver))
-  (solver-clear solver)
-  (solver-assert solver (list (< x z) (< y z) (< z 5) (not (= x y))))
-  (solver-maximize solver (list x))
-  (solver-maximize solver (list y))
-  (check-model (solver-check solver) (hash x 3 y 2 z 4))))
-
-(module+ test
-  (time (run-tests optimization-order-tests)))

test/base/term.rkt

@@ -14,10 +14,6 @@
 (define-symbolic b @boolean?)
 (define-symbolic c @boolean?)
 
-(define (f type)
-  (define-symbolic x type)
-  x)
-
 (define (check-ordered v1 v2)
   (check-true (and (or (term<? v1 v2) (term<? v2 v1)) 
                    (not (and (term<? v1 v2) (term<? v2 v1))))))
@@ -53,47 +49,7 @@
    (check-cached @/ x y)
    (check-cached @remainder x y)
    (check-cached @= x y)
-   (check-cached @< x y)
+   (check-cached @< x y)))
-
-   (f @integer?)
-   (check-exn #px"type should remain unchanged" (lambda () (f @boolean?)))))
-
-(define clear-terms!+gc-terms!-tests
-  (test-suite+
-   "Tests for clear-terms! and gc-terms!"
-
-   (with-terms '()
-     (let ()
-       (define-symbolic x y z @integer?)
-       (define a (@+ x 1))
-       (define b (@+ y 2))
-       (define c (@+ z 3))
-       (check-equal? (length (terms)) 6)
-
-       ;; this should evict z and c
-       (clear-terms! (list z))
-
-       (check-equal? (length (terms)) 4)
-
-       ;; this doesn't affect strongly-held values
-       (set! b #f)
-
-       (check-equal? (length (terms)) 4)
-
-       (gc-terms!) ; change the representation
-       (collect-garbage)
-
-       (check-equal? (length (terms)) 3)
-
-       (clear-terms! (list x))
-       (collect-garbage)
-
-       (check-equal? (length (terms)) 1)
-
-       ;; this is a dummy check to reference a, b, and c so that
-       ;; they are not garbage-collected earlier
-       (check-equal? (length (list a b c)) 3)))))
 
 (module+ test
-  (time (run-tests value-tests))
+  (time (run-tests value-tests)))
-  (time (run-tests clear-terms!+gc-terms!-tests)))