wip: feat: add support for z3 bit rotate exts

z3 > 4.8.8 will return sign_extend and zero_extend operators in the
model, which were not handled by the smt-lib2 decoder, despite being
handled in the encoder. support for these operators has been added

.github/dependabot.yml

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

.github/workflows/docker.yml

@@ -0,0 +1,50 @@
+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,12 +5,16 @@ 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.0', 'current']
+        racket-version: ['8.1', 'current']
         racket-variant: ['CS']
         allow-failure: [false]
     name: Racket ${{ matrix.racket-version }} (${{ matrix.racket-variant }})
@@ -19,12 +23,14 @@ jobs:
     steps:
       - uses: actions/checkout@master
       - name: Setup Racket
-        uses: Bogdanp/setup-racket@v1.1
+        uses: Bogdanp/setup-racket@v1.14
         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 &&
@@ -40,7 +46,50 @@ 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

@@ -0,0 +1,97 @@
+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,5 +1,9 @@
 # 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.0 or later from http://racket-lang.org
+* Download and install Racket 8.1 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.0 or later from http://racket-lang.org
+* Download and install Racket 8.1 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.0")
+               ("racket" #:version "8.1")
                "r6rs-lib"
                "rfc6455"
                "net-lib"

rosette/base/base.rkt

@@ -33,6 +33,7 @@
      @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,20 +14,19 @@
  @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-hash))
+(define bitvector-types (make-hasheq))
 
 ; Returns the bitvector type of the given size.
 (define (bitvector-type size)
-  (assert (exact-positive-integer? size) (argument-error 'bitvector "exact-positive-integer?" size))
-  (or (hash-ref bitvector-types size #f)
-      (let ([t (bitvector size)]) 
-        (hash-set! bitvector-types size t)
-        t)))
+  (assert (and (exact-positive-integer? size) (fixnum? size))
+          (argument-error 'bitvector "(and/c exact-positive-integer? fixnum?)" size))
+  (hash-ref! bitvector-types size (λ () (bitvector size))))
 
 ; Represents a bitvector type.
 (struct bitvector (size)
@@ -340,6 +339,13 @@
      (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)
@@ -347,6 +353,8 @@
 (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 ----------------- ;;
 
@@ -595,7 +603,7 @@
                       _))
      (if (< i size)
          (extract i j a)
-         (expression @bvop a (bitvector (add1 i))))]
+         (expression @bvop a (bitvector-type (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)]
-    [((expression (== @!) a) (expression (== ite) a _ x)) (cons a x)]
+    [((and (expression (== @!) a) !a) (expression (== ite) a _ x)) (cons !a x)]
     [(_ _) p]))
 
 

rosette/base/core/term.rkt

@@ -19,7 +19,12 @@
 ; 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 
@@ -77,17 +82,23 @@
 ; 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)
-     #'(parameterize ([current-terms (hash-copy (current-terms))])
-         expr)]
+     #'(let ([orig-terms (current-terms)])
+         (parameterize ([current-terms #f])
+           (current-terms (hash-copy orig-terms))
+           expr))]
     [(_ terms-expr expr)
-     #'(parameterize ([current-terms (hash-copy-clear (current-terms))])
-         (let ([ts terms-expr]
-               [cache (current-terms)])
-           (for ([t ts])
-             (hash-set! cache (term-val t) t))
-           expr))]))
+     #'(let ([orig-terms (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)))]))
            
          
     
@@ -121,14 +132,21 @@
 (define (term<? s1 s2) (< (term-ord s1) (term-ord s2)))
 
 (define-syntax-rule (make-term term-constructor args type rest ...) 
-  (let ([val args])
-    (or (hash-ref (current-terms) val #f)
-        (let* ([ord (current-index)]
-               [out (term-constructor val type ord rest ...)])
-          (current-index (add1 ord))
-          ((current-reporter) 'new-term out)
-          (hash-set! (current-terms) val out)
-          out))))
+  (let ([val args]
+        [ty type])
+    (define cached (hash-ref (current-terms) val #f))
+    (cond
+      [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])))
            
 (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-equal? 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-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 n))]{
+@defproc[(bitvector->bits [x (bitvector n)]) (listof (bitvector 1))]{
                                                                      
 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,7 +3,11 @@
 @(require (for-label 
            rosette/solver/solver rosette/solver/solution 
            rosette/solver/smt/z3 rosette/solver/smt/cvc4
-           rosette/solver/smt/boolector rosette/solver/smt/yices 
+           rosette/solver/smt/boolector 
+           rosette/solver/smt/bitwuzla
+           rosette/solver/smt/cvc5
+           rosette/solver/smt/stp
+           rosette/solver/smt/yices
            rosette/base/form/define rosette/query/query 
            rosette/base/core/term (only-in rosette/base/base bv?)
            (only-in rosette/base/base assert) 
@@ -21,8 +25,11 @@
                    rosette/solver/solution
                    rosette/solver/smt/z3
                    rosette/solver/smt/cvc4
-                   rosette/solver/smt/yices
                    rosette/solver/smt/boolector
+                   rosette/solver/smt/bitwuzla
+                   rosette/solver/smt/cvc5
+                   rosette/solver/smt/stp
+                   rosette/solver/smt/yices
                    #:use-sources 
                    (rosette/query/finitize
                     rosette/query/query
@@ -30,8 +37,11 @@
                     rosette/solver/solution
                     rosette/solver/smt/z3
                     rosette/solver/smt/cvc4
-                    rosette/solver/smt/yices
-                    rosette/solver/smt/boolector)]
+                    rosette/solver/smt/boolector
+                    rosette/solver/smt/bitwuzla
+                    rosette/solver/smt/cvc5
+                    rosette/solver/smt/stp
+                    rosette/solver/smt/yices)]
 
 A @deftech{solver} is an automatic reasoning engine, used to answer 
 @seclink["sec:queries"]{queries} about Rosette programs.  The result of
@@ -281,37 +291,146 @@ Returns true if the Boolector solver is available for use (i.e., Rosette can loc
 If this returns @racket[#f], @racket[(boolector)] will not succeed
 without its optional @racket[path] argument.}
 
+@subsection{Bitwuzla}
 
-@subsection{Yices}
+@defmodule[rosette/solver/smt/bitwuzla #:no-declare]
+
+@defproc*[([(bitwuzla [#:path path (or/c path-string? #f) #f]
+                      [#:logic logic (or/c symbol? #f) #f]
+                      [#:options options (hash/c symbol? any/c) (hash)]) solver?]
+           [(bitwuzla? [v any/c]) boolean?])]{
+                                               
+Returns a @racket[solver?] wrapper for the @hyperlink["https://bitwuzla.github.io/"]{Bitwuzla} solver.
+
+To use this solver, download prebuilt Bitwuzla or build it yourself,
+and ensure the executable is on your @tt{PATH} or pass the path to the 
+executable as the optional @racket[path] argument.
+Rosette currently tests Bitwuzla at commit 
+@tt{93a3d930f622b4cef0063215e63b7c3bd10bd663}.
+
+The optional @racket[logic] argument specifies an SMT logic for the solver to use (e.g., @racket['QF_BV]).
+Specifying a logic can improve solving performance, but Rosette makes no effort to check that
+emitted constraints fall within the chosen logic. The default is @racket[#f],
+which uses Bitwuzla's default logic.
+
+The @racket[options] argument provides additional options that are sent to Bitwuzla
+via the @tt{set-option} SMT command.
+For example, setting @racket[options] to @racket[(hash ':seed 5)]
+will send the command @tt{(set-option :seed 5)} to Bitwuzla prior to solving.
+}
+
+@defproc[(bitwuzla-available?) boolean?]{
+Returns true if the Bitwuzla solver is available for use (i.e., Rosette can locate a @tt{bitwuzla} binary).
+If this returns @racket[#f], @racket[(bitwuzla)] will not succeed
+without its optional @racket[path] argument.}
+
+@subsection{CVC5}
+
+@defmodule[rosette/solver/smt/cvc5 #:no-declare]
+
+@defproc*[([(cvc5 [#:path path (or/c path-string? #f) #f]
+                  [#:logic logic (or/c symbol? #f) #f]
+                  [#:options options (hash/c symbol? any/c) (hash)]) solver?]
+           [(cvc5? [v any/c]) boolean?])]{
+                                               
+Returns a @racket[solver?] wrapper for the @hyperlink["https://cvc5.github.io/"]{CVC5} solver.
+
+To use this solver, download prebuilt CVC5 or build it yourself,
+and ensure the executable is on your @tt{PATH} or pass the path to the 
+executable as the optional @racket[path] argument.
+Rosette currently tests CVC5 at version 1.0.7.
+
+The optional @racket[logic] argument specifies an SMT logic for the solver to use (e.g., @racket['QF_BV]).
+Specifying a logic can improve solving performance, but Rosette makes no effort to check that
+emitted constraints fall within the chosen logic. The default is @racket[#f],
+which uses CVC5's default logic.
+
+The @racket[options] argument provides additional options that are sent to CVC5
+via the @tt{set-option} SMT command.
+For example, setting @racket[options] to @racket[(hash ':seed 5)]
+will send the command @tt{(set-option :seed 5)} to CVC5 prior to solving.
+}
+
+@defproc[(cvc5-available?) boolean?]{
+Returns true if the CVC5 solver is available for use (i.e., Rosette can locate a @tt{cvc5} binary).
+If this returns @racket[#f], @racket[(cvc5)] will not succeed
+without its optional @racket[path] argument.}
+
+@subsection{STP}
+
+@defmodule[rosette/solver/smt/stp #:no-declare]
+
+@defproc*[([(stp [#:path path (or/c path-string? #f) #f]
+                 [#:logic logic (or/c symbol? #f) #f]
+                 [#:options options (hash/c symbol? any/c) (hash)]) solver?]
+           [(stp? [v any/c]) boolean?])]{
+                                               
+Returns a @racket[solver?] wrapper for the @hyperlink["https://stp.github.io/"]{STP} solver.
+
+To use this solver, download prebuilt STP or build it yourself,
+and ensure the executable is on your @tt{PATH} or pass the path to the 
+executable as the optional @racket[path] argument.
+Rosette currently tests STP at commit 
+@tt{0510509a85b6823278211891cbb274022340fa5c}.
+Note that as of December 2023, the STP version on Mac Homebrew is too old to be
+supported by Rosette.
+
+The optional @racket[logic] argument specifies an SMT logic for the solver to use (e.g., @racket['QF_BV]).
+Specifying a logic can improve solving performance, but Rosette makes no effort to check that
+emitted constraints fall within the chosen logic. The default is @racket[#f],
+which uses STP's default logic.
+
+The @racket[options] argument provides additional options that are sent to STP
+via the @tt{set-option} SMT command.
+For example, setting @racket[options] to @racket[(hash ':seed 5)]
+will send the command @tt{(set-option :seed 5)} to STP prior to solving.
+}
+
+@defproc[(stp-available?) boolean?]{
+Returns true if the STP solver is available for use (i.e., Rosette can locate a @tt{stp} binary).
+If this returns @racket[#f], @racket[(stp)] will not succeed
+without its optional @racket[path] argument.}
+
+@subsection{Yices2}
 
 @defmodule[rosette/solver/smt/yices #:no-declare]
 
 @defproc*[([(yices [#:path path (or/c path-string? #f) #f]
-                   [#:logic logic symbol? 'ALL]
+                   [#:logic logic (or/c symbol? #f) 'QF_BV]
                    [#:options options (hash/c symbol? any/c) (hash)]) solver?]
            [(yices? [v any/c]) boolean?])]{
                                                
-Returns a @racket[solver?] wrapper for the @hyperlink["http://yices.csl.sri.com/"]{Yices} solver from SRI.
+Returns a @racket[solver?] wrapper for the @hyperlink["https://yices.csl.sri.com/"]{Yices2} solver.
 
-To use this solver, download and install Yices (version 2.6.0 or later),
-and either add the @tt{yices-smt2} executable to your @tt{PATH}
-or pass the path to the executable as the optional @racket[path] argument.
+To use this solver, download prebuilt Yices2 or build it yourself,
+and ensure the executable is on your @tt{PATH} or pass the path to the 
+executable as the optional @racket[path] argument.
+Rosette specifically uses the @tt{yices-smt2} executable, which is the Yices2
+solver with its SMTLIB2 frontend enabled.
+Note that just building (without installing) Yices2 will produce an executable
+named @tt{yices_smt2}. Running the installation step produces an executable
+with the correct name. However, it is safe to skip the installation step and
+simply rename or symlink the @tt{yices_smt2} executable to @tt{yices-smt2}.
+Rosette currently tests Yices2 at commit 
+@tt{e27cf308cffb0ecc6cc7165c10e81ca65bc303b3}.
 
 The optional @racket[logic] argument specifies an SMT logic for the solver to use (e.g., @racket['QF_BV]).
 Specifying a logic can improve solving performance, but Rosette makes no effort to check that
-emitted constraints fall within the chosen logic. The default is @racket['ALL].
+emitted constraints fall within the chosen logic. Yices2 expects a logic to be
+set; Rosette defaults to @racket['QF_BV].
 
-The @racket[options] argument provides additional options that are sent to Yices
+The @racket[options] argument provides additional options that are sent to Yices2
 via the @tt{set-option} SMT command.
-For example, setting @racket[options] to @racket[(hash ':random-seed 5)]
-will send the command @tt{(set-option :random-seed 5)} to Yices prior to solving.
+For example, setting @racket[options] to @racket[(hash ':seed 5)]
+will send the command @tt{(set-option :seed 5)} to Yices2 prior to solving.
 }
 
 @defproc[(yices-available?) boolean?]{
-Returns true if the Yices solver is available for use (i.e., Rosette can locate a @tt{yices-smt2} binary).
+Returns true if the Yices2 solver is available for use (i.e., Rosette can locate a @tt{yices-smt2} binary).
 If this returns @racket[#f], @racket[(yices)] will not succeed
 without its optional @racket[path] argument.}
 
+
 @section{Solutions}
 
 A solution to a set of formulas may be satisfiable (@racket[sat?]), unsatisfiable  (@racket[unsat?]),

rosette/guide/scribble/datatypes/vectors.scrbl

@@ -3,6 +3,7 @@
 @(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,19 +1,21 @@
 #lang scribble/manual
 
-@(require (for-label racket (only-in racket/sandbox with-deep-time-limit))
-          (for-label  
+@(require (for-label
+           racket
+           (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
-           (only-in rosette/base/base bv? bitvector
+           rosette/solver/solution
+           (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 
-          (only-in racket [unsyntax racket/unsyntax]))
+@(require racket/sandbox racket/runtime-path scribble/core scribble/racket
+          scribble/example scribble/html-properties scriblib/footnote)
 
 @(require (only-in "../refs.scrbl" ~cite rosette:onward13 rosette:pldi14)
           "../util/lifted.rkt")
@@ -140,7 +142,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],
@@ -321,7 +323,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)))
@@ -480,7 +482,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[sqrt] 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[bvsqrt] 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 (@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.
+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.
 
 @[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 @racket[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 @racketmodname[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,5 +17,4 @@ 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 @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.
-
+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.

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
-  @racket[rosette/lib/synthax] library to turn solutions into
+  @racketmodname[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
-solver time" checkbox):
+producing the output below (after selecting the ``Collapse
+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 rosette/lib/lift
-                   #:use-sources (rosette/base/core/forall rosette/lib/lift)]
+@declare-exporting[rosette/base/core/forall
+                   #:use-sources (rosette/base/core/forall)]
 
 @defform[(for/all ([id val-expr maybe-exhaustive]) body ...+)
          #:grammar [(maybe-exhaustive (code:line) #:exhaustive)]]{

rosette/guide/scribble/refs.scrbl

@@ -9,21 +9,28 @@
 
 @(define rosette:onward13
    (make-bib
-     #:title @hyperlink["http://homes.cs.washington.edu/~emina/pubs/rosette.onward13.pdf"]{Growing Solver-Aided Languages with Rosette}
+     #:title @hyperlink["http://dl.acm.org/citation.cfm?id=2509586"]{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://homes.cs.washington.edu/~emina/pubs/rosette.pldi14.pdf"]{A Lightweight Symbolic Virtual Machine for Solver-Aided Host Languages}
+    #:title @hyperlink["http://dl.acm.org/citation.cfm?id=2594340"]{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://unsat.cs.washington.edu/papers/bornholt-sympro.pdf"]{Finding Code That Explodes Under Symbolic Evaluation}
+    #:title @hyperlink["https://dl.acm.org/citation.cfm?id=3276519"]{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))
+@(require (only-in "../refs.scrbl" ~cite rosette:pldi14 rosette:popl22))
 @(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 @racket[rosette/safe] dialect of the full language.  
+written in the @racketmodname[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 @racket[rosette] 
+functionality}.  In this chapter, we briefly discuss the @racketmodname[rosette]
 dialect of the language, which exports all of Racket.  
 
-Safe use of the full @racket[rosette] language requires a basic understanding 
-of how Rosette's Symbolic Virtual Machine (SVM) works  @~cite[rosette:pldi14].  
+Safe use of the full @racketmodname[rosette] language requires a basic understanding
+of how Rosette's Symbolic Virtual Machine (SVM) works  @~cite[rosette:pldi14 rosette:popl22].  
 Briefly, the SVM hijacks the normal Racket execution for all procedures and 
-constructs that are exported by @racket[rosette/safe].  Any programs that are 
-implemented exclusively in the @racket[rosette/safe] language are therefore 
+constructs that are exported by @racketmodname[rosette/safe].  Any programs that are
+implemented exclusively in the @racketmodname[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 @racket[rosette/safe] code.
+by @racketmodname[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 @racket[rosette/safe] code, 
-it cannot, in general, guarantee the safety or correctness of arbitrary @racket[rosette] programs. 
-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 @racket[rosette/safe] language), 
+Because the SVM controls only the execution of @racketmodname[rosette/safe] code,
+it cannot, in general, guarantee the safety or correctness of arbitrary @racketmodname[rosette] programs.
+As soon as a @racketmodname[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),
 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 @racket[rosette] program continues to behave correctly after the execution returns from the Racket interpreter.
+a @racketmodname[rosette] program continues to behave correctly after the execution returns from the Racket interpreter.
 
-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 @racket[rosette/safe].
+As an example of incorrect behavior, consider the following @racketmodname[rosette] snippet.
+The procedures @racket[make-hash], @racket[hash-ref], and @racket[hash-clear!] are not in @racketmodname[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.0 or later).}
+@itemlist[@item{Download and install @hyperlink["http://racket-lang.org"]{Racket} (version 8.1 or later).}
            @item{Use Racket's @tt{raco} tool to install Rosette:
                  @nested{
                          @verbatim|{> raco pkg install rosette}|}}]

rosette/info.rkt

@@ -14,10 +14,7 @@
      (experimental))))
      ;; Documentation category. On Racket 6.3+ this can be any string.
 
-;; 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 compile-omit-files '("lib/trace/report/node_modules"))
 
 (define raco-commands
   '(("symprofile"

rosette/lib/destruct.rkt

@@ -48,10 +48,11 @@
 
 (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 var [pat (begin e ...)] ...)))
+      match-expr))
   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,8 +78,13 @@
              ; 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.
-             (unless (box-cas! the-box evts (cdr evts))
-               (do-record-exit! out))]))))))
+             (let loop ()
+               (unless (box-cas! the-box evts (cdr evts))
+                 (if (eq? evts (unbox the-box))
+                     ; 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-print (syntax->datum f))))
+    (pretty-write (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,6 +21,8 @@
   (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
@@ -28,6 +30,6 @@
      (cond
        [(path-prefix? path (find-collects-dir)) #f]
        [else
-        (match (path->pkg path)
+        (match (path->pkg path #:cache pkg-cache)
           [#f #t]
           [pkg-name (member pkg-name pkgs-to-instrument)])]))))

rosette/lib/util/streaming-server.rkt

@@ -14,37 +14,40 @@
   ; the procedure for handling connections
   (define (ws-connection conn _state)
     ; only one client may connect
-    (cond
-      [(box-cas! connected? #f #t)  ; we won the race to connect
-       ; tell the main thread we're connected
-       (channel-put channel 'connected)
-       ; loop until we're done
-       (let loop ()
-         (define sync-result (sync/timeout/enable-break interval channel))
-         (define messages (get-message))
+    (let loop ()
+      (cond
+        [(box-cas! connected? #f #t)  ; we won the race to connect
+         ; tell the main thread we're connected
+         (channel-put channel 'connected)
+         ; loop until we're done
+         (let loop ()
+           (define sync-result (sync/timeout/enable-break interval channel))
+           (define messages (get-message))
 
-         ; send the messages; bail out if it fails
-         (define continue? (not (eq? sync-result 'finish)))
-         (with-handlers ([exn:fail? (lambda (e)
-                                      (eprintf "~e\n" e)
-                                      (set! continue? #f))])
-           (ws-send! conn (jsexpr->bytes messages)))
-         (if continue?
-             (loop)
-             (begin
-               (with-handlers ([exn:fail? void])  ; the connection might be dead, but we don't care
-                 (ws-send! conn (jsexpr->bytes (list (get-finish-message))))
-                 (ws-close! conn))
-               ; if we weren't told to shut down, we need to wait until we are.
-               (cond
-                 [on-shutdown (on-shutdown)]
-                 [else
-                  (unless (eq? sync-result 'finish)
-                    (channel-get channel))
-                  (channel-put channel 'finish)]))))]
-      [else
-       (channel-put channel "another client is already connected")
-       (ws-close! conn)]))
+           ; send the messages; bail out if it fails
+           (define continue? (not (eq? sync-result 'finish)))
+           (with-handlers ([exn:fail? (lambda (e)
+                                        (eprintf "~e\n" e)
+                                        (set! continue? #f))])
+             (ws-send! conn (jsexpr->bytes messages)))
+           (if continue?
+               (loop)
+               (begin
+                 (with-handlers ([exn:fail? void])  ; the connection might be dead, but we don't care
+                   (ws-send! conn (jsexpr->bytes (list (get-finish-message))))
+                   (ws-close! conn))
+                 ; if we weren't told to shut down, we need to wait until we are.
+                 (cond
+                   [on-shutdown (on-shutdown)]
+                   [else
+                    (unless (eq? sync-result 'finish)
+                      (channel-get channel))
+                    (channel-put channel 'finish)]))))]
+        [(unbox connected?)
+         ;; it's already connected
+         (channel-put channel "another client is already connected")
+         (ws-close! conn)]
+        [else (loop)])))
 
   ; start the server
   (define conf-channel (make-async-channel))

rosette/private/install.rkt

@@ -1,107 +0,0 @@
-#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 φ   (append assumes asserts))
+  (define  φ `(,(=> (apply && assumes) (apply && asserts))))
   
   (define ¬φ `(,@assumes ,(apply || (map ! asserts))))
 
-  (define (guess sol)
-    (solver-assert guesser (evaluate φ sol))
+  (define (guess ψ)
+    (solver-assert guesser ψ)
     (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 (begin0 (guess (sat)) (solver-clear guesser))])
+  (let loop ([candidate (guess (append assumes asserts))])
     (cond 
       [(unsat? candidate) candidate]
       [else
         (let ([cex (check candidate)])
           (cond 
             [(unsat? cex) candidate]
-            [else (loop (guess cex))]))])))
+            [else (loop (guess (evaluate φ cex)))]))])))
 
 
         

rosette/query/eval.rkt

@@ -47,7 +47,10 @@
                [(cons x y)               
                 (cons (eval-rec x sol cache) (eval-rec y sol cache))]
                [(? vector?)              
-                (for/vector #:length (vector-length expr) ([e expr]) (eval-rec e sol cache))]
+                (let ([v (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,6 +1,7 @@
 #lang racket
 
-(require "core.rkt" 
+(require syntax/parse/define
+         "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))
@@ -70,14 +71,15 @@
 ; 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 optimize
-  (syntax-rules ()
-    [(_ kw opt #:guarantee expr)
-     (let ([obj opt]    ; evaluate objective first to add its spec to (vc)
+(define-syntax-parser optimize
+  [(_ {~and kw {~or* #:minimize #:maximize}} 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))]
-    [(_ kw1 opt1 kw2 opt2 #:guarantee expr)
-     (let ([obj1 opt1]  ; evaluate objectives first to add their spec to (vc)
+  [(_ {~and kw1 {~or* #:minimize #:maximize}} opt1
+      {~and kw2 {~or* #:minimize #:maximize}} opt2
+      #: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,6 +12,8 @@
 
 (provide (all-defined-out))
 
+(define (unique/reverse xs)
+  (reverse (unique xs)))
 
 (define (find-solver binary base-path [user-path #f])
   (cond
@@ -42,14 +44,15 @@
   (unless (list? bools)
     (raise-argument-error 'solver-assert "(listof boolean?)" bools))
   (define wfcheck-cache (mutable-set))
-  (set-solver-asserts! self 
-    (append (solver-asserts self)
-            (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))))
+  (set-solver-asserts!
+   self
+   (append (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)
+           (solver-asserts self))))
 
 (define (solver-minimize self nums)
   (unless (null? nums)
@@ -68,7 +71,7 @@
   (server-shutdown (solver-server self)))
 
 (define (solver-push self)
-  (match-define (solver server _ (app unique asserts) (app unique mins) (app unique maxs) env level) self)
+  (match-define (solver server _ (app unique asserts) (app unique/reverse mins) (app unique/reverse maxs) env level) self)
   (server-write
    server
    (begin
@@ -90,7 +93,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 mins) (app unique maxs) env _) self)
+  (match-define (solver server _ (app unique asserts) (app unique/reverse mins) (app unique/reverse maxs) env _) self)
   (cond [(ormap false? asserts) (unsat)]
         [else (server-write
                server
@@ -131,26 +134,31 @@
 ; 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
-   (parameterize ([current-readtable (make-readtable #f #\# #\a #f)]) ; read BV literals as symbols
-     (match (server-read server (read))
-       [(== 'sat)
-        (server-write server (get-model))
-        (let loop ()
-          (match (server-read server (read))
-            [(list (== 'objectives) _ ...) (loop)]
-            [(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)
-        (if unsat-core?
-            (begin
-              (server-write server (get-unsat-core))
-              (match (server-read server (read))
-                [(list (? symbol? name) ...) name]
-                [other (error 'read-solution "expected unsat core, given ~a" other)]))
-            'unsat)]
-       [(== 'unknown) 'unknown]
-       [other (error 'read-solution "unrecognized solver output: ~a" other)]))
-   env))
+  (decode (parse-solution server #:unsat-core? unsat-core?) env))
+
+(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)
+       (server-write server (get-model))
+       (let loop ()
+         (match (server-read server (read))
+           [(list (== 'objectives) _ ...) (loop)]
+           ; The SMT-LIB spec says that a model should be just a list of
+           ; `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)]))]
+      [(== 'unsat)
+       (if unsat-core?
+           (begin
+             (server-write server (get-unsat-core))
+             (match (server-read server (read))
+               [(list (? symbol? name) ...) name]
+               [other (error 'read-solution "expected unsat core, given ~a" other)]))
+           'unsat)]
+      [(== 'unknown) 'unknown]
+      [other (error 'read-solution "unrecognized solver output: ~a" other)])))

rosette/solver/smt/bitwuzla.rkt

@@ -0,0 +1,106 @@
+;;; 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,28 +107,10 @@
 
 
 ; 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.
+; This is the same as `base/read-solution` except that it applies some fixups
+; for quirks in how various versions of Boolector have emitted models.
 (define (boolector-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))
-          (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)])))
+  (define raw-model (base/parse-solution server))
   ; 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

@@ -0,0 +1,68 @@
+#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,7 +14,8 @@
                   @bvslt @bvsle @bvult @bvule   
                   @bvnot @bvor @bvand @bvxor @bvshl @bvlshr @bvashr
                   @bvneg @bvadd @bvmul @bvudiv @bvsdiv @bvurem @bvsrem @bvsmod
-                  @concat @extract))
+                  @z3_ext_rotate_left @z3_ext_rotate_right
+                  @concat @extract @sign-extend @zero-extend))
 
 
 (provide decode-model)
@@ -116,7 +117,6 @@
         (hash-ref ~env id)]
        [(== true) #t]
        [(== false) #f]
-       [(? integer?) (inexact->exact expr)]
        [(? real?) expr]
        [(? symbol?)
         (cond
@@ -132,6 +132,10 @@
         (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])
@@ -162,6 +166,7 @@
         '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,6 +16,7 @@
                   @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)
@@ -108,6 +109,7 @@
   [@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,7 +68,8 @@
   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

@@ -0,0 +1,69 @@
+#lang racket
+
+(require racket/runtime-path 
+         "server.rkt" "env.rkt" 
+         "../solver.rkt"
+         (prefix-in base/ "base-solver.rkt"))
+
+(provide (rename-out [make-stp stp]) stp? stp-available?)
+
+(define-runtime-path stp-path (build-path ".." ".." ".." "bin" "stp"))
+(define stp-opts '("--SMTLIB2"))
+
+(define (stp-available?)
+  (not (false? (base/find-solver "stp" stp-path #f))))
+
+(define (make-stp [solver #f] #:options [options (hash)] #:logic [logic #f] #:path [path #f])
+  (define config
+    (cond
+      [(stp? solver)
+       (base/solver-config solver)]
+      [else
+       (define real-stp-path (base/find-solver "stp" stp-path path))
+       (when (and (false? real-stp-path) (not (getenv "PLT_PKG_BUILD_SERVICE")))
+         (error 'stp "stp binary is not available (expected to be at ~a); try passing the #:path argument to (stp)" (path->string (simplify-path stp-path))))
+       (base/config options real-stp-path logic)]))
+  (stp (server (base/config-path config) stp-opts (base/make-send-options config)) config '() '() '() (env) '()))
+
+(struct stp base/solver ()
+  #:property prop:solver-constructor make-stp
+  #:methods gen:custom-write
+  [(define (write-proc self port mode) (fprintf port "#<stp>"))]
+  #:methods gen:solver
+  [
+   (define (solver-features self)
+     '(qf_bv))
+
+   (define (solver-options self)
+     (base/solver-options self))
+
+   (define (solver-assert self bools)
+     (base/solver-assert self bools))
+
+   (define (solver-minimize self nums)
+     (base/solver-minimize self nums))
+
+   (define (solver-maximize self nums)
+     (base/solver-maximize self nums))
+
+   (define (solver-clear self)
+     (base/solver-clear self))
+
+   (define (solver-shutdown self)
+     (base/solver-shutdown self))
+
+   (define (solver-push self)
+     (base/solver-push self))
+
+   (define (solver-pop self [k 1])
+     (base/solver-pop self k))
+
+   (define (solver-check self)
+     (base/solver-check self))
+
+   (define (solver-debug self)
+     (base/solver-debug self))])
+
+(define (set-default-options server)
+  void)
+  

rosette/solver/smt/yices.rkt

@@ -1,13 +1,9 @@
 #lang racket
 
 (require racket/runtime-path 
-         "server.rkt" "env.rkt" "cmd.rkt"
+         "server.rkt" "env.rkt" 
          "../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))
+         (prefix-in base/ "base-solver.rkt"))
 
 (provide (rename-out [make-yices yices]) yices? yices-available?)
 
@@ -15,17 +11,17 @@
 (define yices-opts '("--incremental"))
 
 (define (yices-available?)
-  (not (false? (base/find-solver "yices" yices-path #f))))
-
-(define (make-yices [solver #f] #:options [options (hash)] #:logic [logic 'ALL] #:path [path #f])
+  (not (false? (base/find-solver "yices-smt2" yices-path #f))))
+(define default-logic 'QF_BV) ;; Yices2 needs a default logic set otherwise it will error
+(define (make-yices [solver #f] #:options [options (hash)] #:logic [logic default-logic] #:path [path #f])
   (define config
     (cond
       [(yices? solver)
        (base/solver-config solver)]
       [else
-       (define real-yices-path (base/find-solver "yices" yices-path path))
+       (define real-yices-path (base/find-solver "yices-smt2" yices-path path))
        (when (and (false? real-yices-path) (not (getenv "PLT_PKG_BUILD_SERVICE")))
-         (error 'yices "yices 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-smt2 binary is not available (expected to be at ~a); try passing the #:path argument to (yices)" (path->string (simplify-path yices-path))))
        (base/config options real-yices-path logic)]))
   (yices (server (base/config-path config) yices-opts (base/make-send-options config)) config '() '() '() (env) '()))
 
@@ -36,13 +32,13 @@
   #:methods gen:solver
   [
    (define (solver-features self)
-     '(qf_bv qf_uf qf_lia qf_lra))
+     '(qf_bv))
 
    (define (solver-options self)
      (base/solver-options self))
 
    (define (solver-assert self bools)
-     (base/solver-assert self bools yices-wfcheck))
+     (base/solver-assert self bools))
 
    (define (solver-minimize self nums)
      (base/solver-minimize self nums))
@@ -63,85 +59,11 @@
      (base/solver-pop self k))
 
    (define (solver-check self)
-     (base/solver-check self yices-read-solution))
+     (base/solver-check self))
 
    (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,7 +30,9 @@
       [else
        (define real-z3-path (base/find-solver "z3" z3-path path))
        (when (and (false? real-z3-path) (not (getenv "PLT_PKG_BUILD_SERVICE")))
-         (printf "warning: could not find z3 executable at ~a\n" (path->string (simplify-path z3-path))))
+         (fprintf (current-error-port)
+                  "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) '()))
@@ -52,10 +54,10 @@
      (base/solver-assert self bools))
 
    (define (solver-minimize self nums)
-     (base/set-solver-mins! self (append (base/solver-mins self) (numeric-terms nums 'solver-minimize))))
+     (base/set-solver-mins! self (append (reverse (numeric-terms nums 'solver-minimize)) (base/solver-mins self))))
    
    (define (solver-maximize self nums)
-     (base/set-solver-maxs! self (append (base/solver-maxs self) (numeric-terms nums 'solver-maximize))))
+     (base/set-solver-maxs! self (append (reverse (numeric-terms nums 'solver-maximize)) (base/solver-maxs self))))
    
    (define (solver-clear self) 
      (base/solver-clear-stacks! self)

sdsl/fsm/lib.rkt

@@ -1,7 +1,6 @@
 #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,7 +3,11 @@
 (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/yices
+         rosette/solver/smt/boolector 
+         rosette/solver/smt/cvc5
+         rosette/solver/smt/bitwuzla
+         rosette/solver/smt/stp
+         rosette/solver/smt/yices
          "config.rkt")
 
 (error-print-width default-error-print-width)
@@ -38,6 +42,7 @@
  "base/distinct.rkt"
  "base/generics.rkt"
  "base/push-pop.rkt"
+ "base/optimize-order.rkt"
  "base/reflect.rkt"
  "base/decode.rkt"
  "query/solve.rkt"
@@ -81,8 +86,20 @@
     (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 Yices tests =====\n")
+    (printf "===== Running Yices2 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 qf_bv)
+   #:features '(qf_lia int2bv 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 qf_bv)
+   #:features '(qf_lia int2bv qf_bv)
    (check-rotate rotate-right rotate-left bvror)))
 
 (module+ test

test/base/optimize-order.rkt

@@ -0,0 +1,27 @@
+#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,6 +14,10 @@
 (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))))))
@@ -49,7 +53,47 @@
    (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)))