Bump actions/checkout from 4 to 6

Bumps [actions/checkout](https://github.com/actions/checkout) from 4 to 6.
- [Release notes](https://github.com/actions/checkout/releases)
- [Changelog](https://github.com/actions/checkout/blob/main/CHANGELOG.md)
- [Commits](https://github.com/actions/checkout/compare/v4...v6)

---
updated-dependencies:
- dependency-name: actions/checkout
  dependency-version: '6'
  dependency-type: direct:production
  update-type: version-update:semver-major
...

Signed-off-by: dependabot[bot] <support@github.com>

.github/workflows/docker.yml

@@ -14,7 +14,7 @@ jobs:
 
     steps:
       - name: Clone Repository
-        uses: actions/checkout@v4
+        uses: actions/checkout@v6
 
       - name: Configure Docker Metadata
         id: meta

rosette/base/base.rkt

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

rosette/base/core/bitvector.rkt

@@ -14,7 +14,6 @@
  @bvnot @bvor @bvand @bvxor @bvshl @bvlshr @bvashr
  @bvneg @bvadd @bvsub @bvmul @bvudiv @bvsdiv @bvurem @bvsrem @bvsmod
  @concat @extract @sign-extend @zero-extend
- @z3_ext_rotate_left @z3_ext_rotate_right
  @integer->bitvector @bitvector->integer @bitvector->natural)
 
 ;; ----------------- Bitvector Types ----------------- ;; 
@@ -339,13 +338,6 @@
      (ite (bveq (bv 0 t) (bvand x (bv (bvsmin t) t))) (bv 0 t) (bv -1 t))]
     [(_ _) (expression @bvashr x y)]))
 
-
-(define (z3_ext_rotate_left x y)
-  (expression @z3_ext_rotate_left x y))
-
-(define (z3_ext_rotate_right x y)
-  (expression @z3_ext_rotate_right x y))
-
 (define-lifted-operator @bvnot bvnot T*->T)
 (define-lifted-operator @bvand bvand T*->T)
 (define-lifted-operator @bvor bvor T*->T)
@@ -353,8 +345,6 @@
 (define-lifted-operator @bvshl bvshl T*->T)
 (define-lifted-operator @bvlshr bvlshr T*->T)
 (define-lifted-operator @bvashr bvashr T*->T)
-(define-lifted-operator @z3_ext_rotate_left z3_ext_rotate_left T*->T)
-(define-lifted-operator @z3_ext_rotate_right z3_ext_rotate_right T*->T)
 
 ;; ----------------- Simplification ruules for bitwise operators ----------------- ;;
 

rosette/info.rkt

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

rosette/private/install.rkt

@@ -0,0 +1,84 @@
+#lang racket/base
+
+;; Check whether z3 is installed during package setup.
+;; If missing, builds & links a z3 binary.
+
+
+(provide pre-installer post-installer)
+
+(require racket/match
+         racket/file
+         racket/port
+         net/url
+         file/unzip)
+
+; We need to run the Z3 installer as a pre-install step, because building the
+; documentation relies on Z3 being available. But pre-install is so early in
+; the build that its output gets pushed off screen by the later steps. So we
+; use this little hack to repeat the failure message as a post-install step,
+; which happens at the very end of the install and so makes the error message
+; far more obvious.
+(define z3-install-failure #f)
+
+(define z3-version "4.8.8")
+
+(define (print-failure path msg)
+  (printf "\n\n********** Failed to install Z3 **********\n\n")
+  (printf "Rosette installed successfully, but wasn't able to install the Z3 SMT solver.\n\n")
+  (printf "You'll need to manually install a Z3 binary at this location:\n")
+  (printf "    ~a\n" path)
+  (printf "or anywhere that is on your PATH. Alternatively, in your programs, you can\n")
+  (printf "construct a solver object manually:\n")
+  (printf "    (current-solver (z3 #:path \"/path/to/z3\"))\n\n")
+  (printf "Note that Rosette ships with a specific release of Z3 (v~a). Installing a\n" z3-version)
+  (printf "different version of Z3 may change the performance of Rosette programs.\n\n")
+  (printf "The problem was:\n    ~a\n\n" msg)
+  (printf "**********\n\n\n"))
+
+(define (post-installer collections-top-path)
+  (match z3-install-failure
+    [(cons z3-path msg) (print-failure z3-path msg)]
+    [_ (void)]))
+
+(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)
+                               (set! z3-install-failure (cons z3-path (exn-message 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)
+  ; TODO: Z3 packages a macOS aarch64 binary as of 4.8.16, so remove this special case when we update
+  ; to a newer Z3 version.
+  (if (and (equal? (system-type 'os*) 'macosx) (equal? (system-type 'arch) 'aarch64))
+      (values "https://github.com/emina/rosette/releases/download/4.1/z3-4.8.8-aarch64-osx-13.3.1.zip" "z3")
+      (let ()
+        (define site "https://github.com/Z3Prover/z3/releases/download")
+        (define-values (os exe)
+          (match (list (system-type 'os*) (system-type 'arch))
+            ['(linux x86_64)   (values "x64-ubuntu-16.04" "z3")]
+            [`(macosx ,_)      (values "x64-osx-10.14.6" "z3")]
+            ['(windows x86_64) (values "x64-win" "z3.exe")]
+            [any               (raise-user-error 'get-z3-url "No Z3 binary available for system type '~a" any)]))
+        (define name (format "z3-~a-~a" z3-version os))
+        (values
+         (format "~a/z3-~a/~a.zip" site z3-version name)
+         (format "~a/bin/~a" name exe)))))

rosette/solver/smt/dec.rkt

@@ -14,8 +14,7 @@
                   @bvslt @bvsle @bvult @bvule   
                   @bvnot @bvor @bvand @bvxor @bvshl @bvlshr @bvashr
                   @bvneg @bvadd @bvmul @bvudiv @bvsdiv @bvurem @bvsrem @bvsmod
-                  @z3_ext_rotate_left @z3_ext_rotate_right
+                  @concat @extract))
-                  @concat @extract @sign-extend @zero-extend))
 
 
 (provide decode-model)
@@ -132,10 +131,6 @@
         (bv n (bitvector len))]
        [(list (list (== '_) (== 'extract) i j) s)
         `(, @extract ,(inline i sol ~env) ,(inline j sol ~env) ,(inline s sol ~env))]
-       [(list (list (== '_) (== 'sign_extend) i) s)
-        `(, @sign-extend ,(inline i sol ~env) ,(inline s sol ~env))]
-       [(list (list (== '_) (== 'zero_extend) i) s)
-        `(, @zero-extend ,(inline i sol ~env) ,(inline s sol ~env))]
        [(list (== 'let) binds body)
         (substitute (inline body sol ~env)
                     (for/hash ([id:expr binds])
@@ -166,7 +161,6 @@
         'bvslt @bvslt 'bvsle @bvsle 'bvult @bvult 'bvule @bvule   
         'bvnot @bvnot 'bvor @bvor 'bvand @bvand 'bvxor @bvxor
         'bvshl @bvshl 'bvlshr @bvlshr 'bvashr @bvashr
-        'ext_rotate_left @z3_ext_rotate_left 'ext_rotate_right @z3_ext_rotate_right
         'bvneg @bvneg 'bvadd @bvadd 'bvmul @bvmul
         'bvudiv @bvudiv 'bvsdiv @bvsdiv
         'bvurem @bvurem 'bvsrem @bvsrem

rosette/solver/smt/enc.rkt

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

rosette/solver/smt/smtlib2.rkt

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