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/workflows/docker.yml

@@ -14,11 +14,11 @@ jobs:
 
     steps:
       - name: Clone Repository
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Configure Docker Metadata
         id: meta
-        uses: docker/metadata-action@v3
+        uses: docker/metadata-action@v5
         with:
           images: ghcr.io/${{ github.repository }}
           tags: |
@@ -29,7 +29,7 @@ jobs:
             type=semver,pattern={{major}}.{{minor}}
 
       - name: Authenticate to Package Registry
-        uses: docker/login-action@v1
+        uses: docker/login-action@v3
         if: ${{ github.event_name != 'pull_request' }}
         with:
           registry: ghcr.io
@@ -37,10 +37,10 @@ jobs:
           password: ${{ secrets.GITHUB_TOKEN }}
 
       - name: Set up Docker Buildx
-        uses: docker/setup-buildx-action@v1
+        uses: docker/setup-buildx-action@v3
 
       - name: Build and Publish Rosette Image
-        uses: docker/build-push-action@v2
+        uses: docker/build-push-action@v6
         with:
           context: .
           push: ${{ github.event_name != 'pull_request' }}

.github/workflows/tests.yml

@@ -5,6 +5,10 @@ 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:
@@ -19,12 +23,14 @@ jobs:
     steps:
       - uses: actions/checkout@master
       - name: Setup Racket
-        uses: Bogdanp/setup-racket@v1.7
+        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

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,6 +14,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)
 
 ;; ----------------- Bitvector Types ----------------- ;; 
@@ -338,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)
@@ -345,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 ----------------- ;;
 

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

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

@@ -4,6 +4,10 @@
            rosette/solver/solver rosette/solver/solution 
            rosette/solver/smt/z3 rosette/solver/smt/cvc4
            rosette/solver/smt/boolector 
+           rosette/solver/smt/bitwuzla
+           rosette/solver/smt/cvc5
+           rosette/solver/smt/stp
+           rosette/solver/smt/yices
            rosette/base/form/define rosette/query/query 
            rosette/base/core/term (only-in rosette/base/base bv?)
            (only-in rosette/base/base assert) 
@@ -22,6 +26,10 @@
                    rosette/solver/smt/z3
                    rosette/solver/smt/cvc4
                    rosette/solver/smt/boolector
+                   rosette/solver/smt/bitwuzla
+                   rosette/solver/smt/cvc5
+                   rosette/solver/smt/stp
+                   rosette/solver/smt/yices
                    #:use-sources 
                    (rosette/query/finitize
                     rosette/query/query
@@ -29,7 +37,11 @@
                     rosette/solver/solution
                     rosette/solver/smt/z3
                     rosette/solver/smt/cvc4
-                    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
@@ -279,6 +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}
+
+@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 (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["https://yices.csl.sri.com/"]{Yices2} solver.
+
+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. Yices2 expects a logic to be
+set; Rosette defaults to @racket['QF_BV].
+
+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 ':seed 5)]
+will send the command @tt{(set-option :seed 5)} to Yices2 prior to solving.
+}
+
+@defproc[(yices-available?) boolean?]{
+Returns true if the Yices2 solver is available for use (i.e., Rosette can locate a @tt{yices-smt2} binary).
+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/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)"))
+    #: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 ".")
@@ -19,7 +19,7 @@ functionality}.  In this chapter, we briefly discuss the @racketmodname[rosette]
 dialect of the language, which exports all of Racket.  
 
 Safe use of the full @racketmodname[rosette] language requires a basic understanding
-of how Rosette's Symbolic Virtual Machine (SVM) works  @~cite[rosette:pldi14].  
+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 @racketmodname[rosette/safe].  Any programs that are
 implemented exclusively in the @racketmodname[rosette/safe] language are therefore

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/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/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/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/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
@@ -122,35 +125,40 @@
 
 
 ; 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 
+; 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 
+; unsatisfiable core (if the solution is 'unsat and a
+; core was extracted); #f (if the solution is
 ; 'unsat and no core was extracted); or 'unknown otherwise.
 (define (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,27 +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) ... (and def (list (== 'define-fun) _ ...)) ...)
-             (for/hash ([d def]) (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

@@ -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-yices yices]) yices? yices-available?)
+
+(define-runtime-path yices-path (build-path ".." ".." ".." "bin" "yices-smt2"))
+(define yices-opts '("--incremental"))
+
+(define (yices-available?)
+  (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-smt2" yices-path path))
+       (when (and (false? real-yices-path) (not (getenv "PLT_PKG_BUILD_SERVICE")))
+         (error 'yices "yices-smt2 binary is not available (expected to be at ~a); try passing the #:path argument to (yices)" (path->string (simplify-path yices-path))))
+       (base/config options real-yices-path logic)]))
+  (yices (server (base/config-path config) yices-opts (base/make-send-options config)) config '() '() '() (env) '()))
+
+(struct yices base/solver ()
+  #:property prop:solver-constructor make-yices
+  #:methods gen:custom-write
+  [(define (write-proc self port mode) (fprintf port "#<yices>"))]
+  #: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/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)

test/all-rosette-tests.rkt

@@ -4,6 +4,10 @@
          rosette/lib/roseunit
          rosette/solver/smt/z3 rosette/solver/smt/cvc4 
          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"
@@ -80,6 +85,22 @@
   (when (boolector-available?)
     (printf "===== Running Boolector tests =====\n")
     (run-tests-with-solver boolector))
+
+  (when (cvc5-available?)
+    (printf "===== Running cvc5 tests =====\n")
+    (run-tests-with-solver cvc5))
+
+  (when (bitwuzla-available?)
+    (printf "===== Running bitwuzla tests =====\n")
+    (run-tests-with-solver bitwuzla))
+
+  (when (stp-available?)
+    (printf "===== Running stp tests =====\n")
+    (run-tests-with-solver stp))
+
+  (when (yices-available?)
+    (printf "===== Running Yices2 tests =====\n")
+    (run-tests-with-solver yices))
 )
 
 (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)))