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

@@ -30,14 +30,14 @@
      ; core/bitvector.rkt
      bv @bv? bitvector bitvector-size bitvector? 
      @bveq @bvslt @bvsgt @bvsle @bvsge @bvult @bvugt @bvule @bvuge
-     @bvnot @bvor @bvand @bvxor @bvshl @bvlshr @bvashr @bvrol @bvror
+     @bvnot @bvor @bvand @bvxor @bvshl @bvlshr @bvashr
      @bvneg @bvadd @bvsub @bvmul @bvudiv @bvsdiv @bvurem @bvsrem @bvsmod
      @concat @extract @sign-extend @zero-extend 
      @integer->bitvector @bitvector->integer @bitvector->natural
      ; core/bvlib.rkt
      bit lsb msb bvzero? bvadd1 bvsub1
      bvsmin bvsmax bvumin bvumax
-     rotate-left rotate-right
+     rotate-left rotate-right bvrol bvror
      bool->bitvector bitvector->bool bitvector->bits
      ; core/function.rkt
      @fv? ~> function?

rosette/base/core/bitvector.rkt

@@ -11,7 +11,7 @@
  (rename-out [@bv bv]) @bv? bv? bv-value bv-type
  (rename-out [@bitvector bitvector]) bitvector-size bitvector? 
  @bveq @bvslt @bvsgt @bvsle @bvsge @bvult @bvugt @bvule @bvuge
- @bvnot @bvor @bvand @bvxor @bvshl @bvlshr @bvashr @bvrol @bvror
+ @bvnot @bvor @bvand @bvxor @bvshl @bvlshr @bvashr
  @bvneg @bvadd @bvsub @bvmul @bvudiv @bvsdiv @bvurem @bvsrem @bvsmod
  @concat @extract @sign-extend @zero-extend
  @integer->bitvector @bitvector->integer @bitvector->natural)
@@ -338,29 +338,6 @@
      (ite (bveq (bv 0 t) (bvand x (bv (bvsmin t) t))) (bv 0 t) (bv -1 t))]
     [(_ _) (expression @bvashr x y)]))
 
-(define (bvrol x y)
-  (match* (x y)
-    [((and a (bv _ (bitvector n))) (and b (bv _ _)))
-     (define n* (make-bv n n))
-     (define b* (@bvurem b n*))
-     (@bvor (@bvshl a b*) (@bvlshr a (@bvsub n* b*)))]
-    [(_ (bv 0 _)) x]
-    [((bv 0 _) _) x]
-    [((bv -1 _) _) x]
-    [(_ _) (expression @bvrol x y)]))
-
-(define (bvror x y)
-  (match* (x y)
-    [((and a (bv _ (bitvector n))) (and b (bv _ _)))
-     (define n* (make-bv n n))
-     (define b* (@bvurem b n*))
-     (@bvor (@bvlshr a b*) (@bvshl a (@bvsub n* b*)))]
-    [(_ (bv 0 _)) x]
-    [((bv 0 _) _) x]
-    [((bv -1 _) _) x]
-    [(_ _) (expression @bvror x y)]))
-
-
 (define-lifted-operator @bvnot bvnot T*->T)
 (define-lifted-operator @bvand bvand T*->T)
 (define-lifted-operator @bvor bvor T*->T)
@@ -368,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 @bvrol bvrol T*->T)
-(define-lifted-operator @bvror bvror T*->T)
 
 ;; ----------------- Simplification ruules for bitwise operators ----------------- ;;
 

rosette/base/core/bvlib.rkt

@@ -8,7 +8,7 @@
 
 (provide bit lsb msb bvzero? bvadd1 bvsub1
          bvsmin bvsmax bvumin bvumax
-         rotate-left rotate-right
+         rotate-left rotate-right bvrol bvror
          bool->bitvector bitvector->bool bitvector->bits)
 
 (define-syntax (define-lifted stx)
@@ -79,3 +79,15 @@
 (define-rotate rotate-right
    (lambda (i sz x)
      (@concat (@extract (- i 1) 0 x) (@extract (- sz 1) i x))))        
+         
+; x and y must be bitvectors (not unions) of the same length.
+; shift1 and shift2 are shift operators.
+(define-syntax-rule (bvrotate x y shift1 shift2)
+  (let* ([sz (bitvector-size (get-type y))]
+         [n (bv sz sz)]
+         [amount (@bvurem y n)])
+    (@bvor (shift1 x amount) (shift2 x (@bvsub n amount)))))
+
+(define-lifted (bvrol x y) (bvrotate x y @bvshl @bvlshr))
+(define-lifted (bvror x y) (bvrotate x y @bvlshr @bvshl))
+  

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/safe.rkt

@@ -27,11 +27,10 @@
   (current-solver (z3)))
 
 (provide
- (except-out (all-from-out "solver/solver.rkt")
+ (except-out (all-from-out "solver/solver.rkt") prop:solver-constructor solver-constructor)
-             prop:solver-constructor solver-constructor solver-custom-encode)
  (all-from-out  
   "solver/solution.rkt" 
   "base/base.rkt"
   "query/query.rkt")
  (for-syntax (all-from-out racket))
- rosette clear-state! output-smt)
+ rosette clear-state! output-smt)

rosette/solver/smt/base-solver.rkt

@@ -1,13 +1,12 @@
 #lang racket
 
-(require "server.rkt" "cmd.rkt" "enc.rkt" "env.rkt" 
+(require "server.rkt" "cmd.rkt" "env.rkt" 
          "../solution.rkt" 
          (only-in racket [remove-duplicates unique])
          (only-in "smtlib2.rkt" reset set-option check-sat get-model get-unsat-core push pop set-logic)
-         (only-in "../../base/core/term.rkt" expression expression? term term? term-type get-type)
+         (only-in "../../base/core/term.rkt" term term? term-type)
          (only-in "../../base/core/bool.rkt" @boolean?)
-         (only-in "../../base/core/bitvector.rkt" bitvector? bitvector-size bv bv?
+         (only-in "../../base/core/bitvector.rkt" bitvector? bv?)
-                  @bvshl @bvlshr @bvor @bvrol @bvror @bvsub @bvurem)
          (only-in "../../base/core/real.rkt" @integer? @real?)
          (only-in "../../base/core/reporter.rkt" current-reporter))
 
@@ -77,7 +76,7 @@
    server
    (begin
      ((current-reporter) 'encode-start)
-     (encode self env asserts mins maxs)
+     (encode env asserts mins maxs)
      ((current-reporter) 'encode-finish)
      (push)))
   (solver-clear-stacks! self)
@@ -100,7 +99,7 @@
                server
                (begin
                  ((current-reporter) 'encode-start)
-                 (encode self env asserts mins maxs)
+                 (encode env asserts mins maxs)
                  ((current-reporter) 'encode-finish)
                  (check-sat)))
               ((current-reporter) 'solve-start)
@@ -115,29 +114,6 @@
 (define (solver-options self)
   (config-options (solver-config self)))
 
-; x and y must be bitvectors (not unions) of the same length.
-; shift1 and shift2 are shift operators.
-(define-syntax-rule (bvrotate x y shift1 shift2)
-  (let* ([sz (bitvector-size (get-type y))]
-         [n (bv sz sz)]
-         [amount (@bvurem y n)])
-    (@bvor (shift1 x amount) (shift2 x (@bvsub n amount)))))
-
-; Implement basic support for non-indexed bit rotation operations which works
-; on all solvers that do not implement a specific extension for it. This
-; reduces the bit rotation to a bitwise or of left shift and right shift.
-; A solver which has a dedicated SMT-LIB extension for this operation could
-; override this method to encode directly to that extension. This results in
-; significantly improved performance with, e.g., Z3, so bit rotation SMT-LIB
-; extensions are preferred when available.
-(define (solver-custom-encode self expr env quantified)
-  (match expr
-    [(expression (== @bvrol) x y)
-     (enc self (bvrotate x y @bvshl @bvlshr) env quantified)]
-    [(expression (== @bvror) x y)
-     (enc self (bvrotate x y @bvlshr @bvshl) env quantified)]
-    [_ #f]))
-
 (define (solver-clear-stacks! self)
   (set-solver-asserts! self '())
   (set-solver-mins! self '())
@@ -185,4 +161,4 @@
                [other (error 'read-solution "expected unsat core, given ~a" other)]))
            'unsat)]
       [(== 'unknown) 'unknown]
-      [other (error 'read-solution "unrecognized solver output: ~a" other)])))
+      [other (error 'read-solution "unrecognized solver output: ~a" other)])))

rosette/solver/smt/bitwuzla.rkt

@@ -2,20 +2,19 @@
 #lang racket
 
 (require racket/runtime-path 
-         "server.rkt" "cmd.rkt" "enc.rkt" "env.rkt" 
+         "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 @bvrol @bvror)
+         (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 bin-path (build-path ".." ".." ".." "bin"))
+(define-runtime-path bitwuzla-path (build-path ".." ".." ".." "bin" "bitwuzla"))
-(define bitwuzla-path (build-path bin-path "bitwuzla"))
 (define bitwuzla-opts '("-m"))
 
 (define (bitwuzla-available?)
@@ -40,7 +39,7 @@
   #:methods gen:solver
   [
    (define (solver-features self)
-     '(qf_bv ext_rotate))
+     '(qf_bv))
    
    (define (solver-options self)
      (base/solver-options self))
@@ -70,17 +69,7 @@
      (base/solver-check self read-solution))
    
    (define (solver-debug self)
-     (base/solver-debug self))
+     (base/solver-debug self))])
-
-   (define (solver-custom-encode self expr env quantified)
-     (match expr
-       [(expression (== @bvrol) a b)
-        (list 'bvrol
-              (enc self a env quantified) (enc self b env quantified))]
-       [(expression (== @bvror) a b)
-        (list 'bvror
-              (enc self a env quantified) (enc self b env quantified))]
-       [_ (base/solver-custom-encode self expr env quantified)]))])
 
 (define (set-default-options server)
   void)

rosette/solver/smt/boolector.rkt

@@ -1,21 +1,20 @@
 #lang racket
 
 (require racket/runtime-path 
-         "server.rkt" "cmd.rkt" "enc.rkt" "env.rkt" 
+         "server.rkt" "cmd.rkt" "env.rkt" 
          "../solver.rkt" "../solution.rkt"
          (prefix-in base/ "base-solver.rkt")
          (only-in "smtlib2.rkt" get-model)
          (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 @bvrol @bvror)
+         (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-boolector boolector]) boolector? boolector-available?)
 
-(define-runtime-path bin-path (build-path ".." ".." ".." "bin"))
+(define-runtime-path boolector-path (build-path ".." ".." ".." "bin" "boolector"))
-(define boolector-path (build-path bin-path "boolector"))
 (define boolector-opts '("-m" "--output-format=smt2" "-i"))
 
 (define (boolector-available?)
@@ -70,10 +69,7 @@
      (base/solver-check self boolector-read-solution))
    
    (define (solver-debug self)
-     (base/solver-debug self))
+     (base/solver-debug self))])
-
-   (define (solver-custom-encode self expr env quantified)
-     (base/solver-custom-encode self expr env quantified))])
 
 (define (set-default-options server)
   void)

rosette/solver/smt/cmd.rkt

@@ -22,14 +22,14 @@
 ; already bound in the environment.  The environment will 
 ; be augmented, if needed, with additional declarations and 
 ; definitions.  This procedure will not emit any other commands.
-(define (encode solver env asserts mins maxs)
+(define (encode env asserts mins maxs)
   ((current-reporter) 'to-solver asserts mins maxs)
   (for ([a asserts])
-    (assert (enc solver a env)))
+    (assert (enc a env)))
   (for ([m mins])
-    (minimize (enc solver m env)))
+    (minimize (enc m env)))
   (for ([m maxs])
-    (maximize (enc solver m env))))
+    (maximize (enc m env))))
 
 ; Given an encoding environment and a list of asserts, 
 ; the encode-labeled procedure prints an SMT encoding of the given assertions 
@@ -38,9 +38,9 @@
 ; solver's unsat-core-extraction option to be set.  The environment will be augmented, 
 ; if needed, with additional declarations and definitions.
 ; This procedure will not emit any other commands.
-(define (encode-for-proof solver env asserts)
+(define (encode-for-proof env asserts)
   (for ([a asserts])
-    (define id (enc solver a env))
+    (define id (enc a env))
     (assert id (id->name id))))
 
 ; Generates an assertion label for a declared or defined SMT id by prefixing that 

rosette/solver/smt/cvc4.rkt

@@ -7,8 +7,7 @@
 
 (provide (rename-out [make-cvc4 cvc4]) cvc4? cvc4-available?)
 
-(define-runtime-path bin-path (build-path ".." ".." ".." "bin"))
+(define-runtime-path cvc4-path (build-path ".." ".." ".." "bin" "cvc4"))
-(define cvc4-path (build-path bin-path "cvc4"))
 (define cvc4-opts '("-L" "smt2" "-q" "-m" "-i" "--bv-print-consts-as-indexed-symbols" "--bv-div-zero-const"))
 
 (define (cvc4-available?)
@@ -63,10 +62,7 @@
      (base/solver-check self))
    
    (define (solver-debug self)
-     (base/solver-debug self))
+     (base/solver-debug self))])
-
-   (define (solver-custom-encode self expr env quantified)
-     (base/solver-custom-encode self expr env quantified))])
 
 (define (set-default-options server)
   void)

rosette/solver/smt/cvc5.rkt

@@ -7,8 +7,7 @@
 
 (provide (rename-out [make-cvc5 cvc5]) cvc5? cvc5-available?)
 
-(define-runtime-path bin-path (build-path ".." ".." ".." "bin"))
+(define-runtime-path cvc5-path (build-path ".." ".." ".." "bin" "cvc5"))
-(define cvc5-path (build-path bin-path "cvc5"))
 (define cvc5-opts '("-L" "smt2" "-q" "-m" "-i" "--bv-print-consts-as-indexed-symbols"))
 
 (define (cvc5-available?)
@@ -63,10 +62,7 @@
      (base/solver-check self))
    
    (define (solver-debug self)
-     (base/solver-debug self))
+     (base/solver-debug self))])
-
-   (define (solver-custom-encode self expr env quantified)
-     (base/solver-custom-encode self expr env quantified))])
 
 (define (set-default-options server)
   void)

rosette/solver/smt/dec.rkt

@@ -12,7 +12,7 @@
          (only-in "../../base/core/bitvector.rkt" 
                   bitvector? bitvector bv bv? bitvector-size 
                   @bvslt @bvsle @bvult @bvule   
-                  @bvnot @bvor @bvand @bvxor @bvshl @bvlshr @bvashr @bvrol @bvror
+                  @bvnot @bvor @bvand @bvxor @bvshl @bvlshr @bvashr
                   @bvneg @bvadd @bvmul @bvudiv @bvsdiv @bvurem @bvsrem @bvsmod
                   @concat @extract))
 
@@ -161,9 +161,6 @@
         'bvslt @bvslt 'bvsle @bvsle 'bvult @bvult 'bvule @bvule   
         'bvnot @bvnot 'bvor @bvor 'bvand @bvand 'bvxor @bvxor
         'bvshl @bvshl 'bvlshr @bvlshr 'bvashr @bvashr
-        ;; Z3/Boolector and Bitwuzla have different names for non-indexed bit rotation. Include
-        ;; support for decoding either name.
-        'ext_rotate_left @bvrol 'ext_rotate_right @bvror 'bvrol @bvrol 'bvror @bvror
         'bvneg @bvneg 'bvadd @bvadd 'bvmul @bvmul
         'bvudiv @bvudiv 'bvsdiv @bvsdiv
         'bvurem @bvurem 'bvsrem @bvsrem

rosette/solver/smt/enc.rkt

@@ -2,7 +2,6 @@
 
 (require "env.rkt" 
          (prefix-in $ "smtlib2.rkt") 
-         (only-in "../solver.rkt" solver-custom-encode)
          (only-in "../../base/core/term.rkt" expression expression? constant? term? get-type @app)
          (only-in "../../base/core/polymorphic.rkt" ite ite* =? guarded-test guarded-value)
          (only-in "../../base/core/distinct.rkt" @distinct?)
@@ -27,58 +26,54 @@
 ; an error is thrown. 
 ; The environment will be modified (if needed) to include an encoding for 
 ; the given value and all of its subexpressions (if any).
-(define (enc solver v env [quantified '()])
+(define (enc v env [quantified '()])
   (match v
-    [(? expression?) (ref-expr! solver v env quantified enc-expr)]
+    [(? expression?) (ref-expr! v env quantified enc-expr)]
     [(? constant?)   (ref-const! v env quantified)]
-    [_               (ref-expr! solver v env quantified enc-lit)]))
+    [_               (ref-expr! v env quantified enc-lit)]))
 
-(define (enc-expr solver v env quantified)  
+(define (enc-expr v env quantified)  
   (match v
     [(and (expression (== ite*) gvs ...) (app get-type t))
      (let-values ([($0 $op) (if (bitvector? t) 
                                 (values ($bv 0 (bitvector-size t)) $bvor) 
                                 (values 0 $+))])
        (apply $op (for/list ([gv gvs]) 
-                    ($ite (enc solver (guarded-test gv) env quantified) 
+                    ($ite (enc (guarded-test gv) env quantified) 
-                          (enc solver (guarded-value gv) env quantified) 
+                          (enc (guarded-value gv) env quantified) 
                           $0))))]
     [(expression (== @abs) x)
-     ($real-abs (enc solver x env quantified) (get-type v))]
+     ($real-abs (enc x env quantified) (get-type v))]
     [(expression (== @extract) i j e)
-     ($extract i j (enc solver e env quantified))]
+     ($extract i j (enc e env quantified))]
     [(expression (== @sign-extend) v t)
      ($sign_extend (- (bitvector-size t) (bitvector-size (get-type v)))
-                   (enc solver v env quantified))]
+                   (enc v env quantified))]
     [(expression (== @zero-extend) v t)
      ($zero_extend (- (bitvector-size t) (bitvector-size (get-type v)))
-                   (enc solver v env quantified))]
+                   (enc v env quantified))]
     [(expression (== @integer->bitvector) v t) 
-     ($int->bv (enc solver v env quantified) (bitvector-size t))]
+     ($int->bv (enc v env quantified) (bitvector-size t))]
     [(expression (== @bitvector->integer) v) 
-     ($bv->int (enc solver v env quantified) (bitvector-size (get-type v)))]  
+     ($bv->int (enc v env quantified) (bitvector-size (get-type v)))]  
     [(expression (== @bitvector->natural) v) 
-     ($bv->nat (enc solver v env quantified) (bitvector-size (get-type v)))]
+     ($bv->nat (enc v env quantified) (bitvector-size (get-type v)))]
     [(expression (and (or (== @forall) (== @exists)) op) vars body)
      (let ([vars+quantified (remove-duplicates (append vars quantified))])
        ((if (equal? op @forall) $forall $exists)
         (for/list ([v vars])
           (list (ref-const! v env vars+quantified) (smt-type (get-type v))))
-        (enc solver body env vars+quantified)))]
+        (enc body env vars+quantified)))]
     [(expression (== @distinct?) (? real? rs) ..1 (? term? es) ...)
      (apply $distinct (append (if (equal? @real? (get-type (car es)))
                                   (for/list ([r rs]) (enc-real r))
                                   rs)
-                              (for/list ([e es]) (enc solver e env quantified))))]
+                              (for/list ([e es]) (enc e env quantified))))]
     [(expression (app rosette->smt (? procedure? $op)) es ...) 
-     (apply $op (for/list ([e es]) (enc solver e env quantified)))]
+     (apply $op (for/list ([e es]) (enc e env quantified)))]
-    [_
+    [_ (error 'enc "cannot encode ~a to SMT" v)]))
-     (define custom-enc (solver-custom-encode solver v env quantified))
-     (if custom-enc
-         custom-enc
-         (error 'enc "cannot encode ~a to SMT" v))]))
 
-(define (enc-lit solver v env quantified)
+(define (enc-lit v env quantified)
   (match v 
     [#t $true]
     [#f $false]

rosette/solver/smt/env.rkt

@@ -67,7 +67,7 @@
 
 ; Retrieves the SMT encoding for the Rosette expression e in the environment env.
 ; If env has a binding for (cons e quantified), that binding is returned. 
-; Otherwise, ref-expr! evaluates (encoder solver e env quantified) to obtain the encoding enc.
+; Otherwise, ref-expr! evaluates (encoder e env quantified) to obtain the encoding enc.
 ; If enc is not an s-expression (a pair), it is returned. Otherwise, ref-expr! extends
 ; the SMT encoding with (define-fun id ([arg-id type] ...) enc), where arg-id's are the
 ; SMT identifiers for the values in the quantified list. The identifier id takes the form 
@@ -75,10 +75,10 @@
 ; If the quantified list is empty, env is extended with a binding from e to id, and id
 ; is returned. Otherwise, env is extended with a binding from e to (e arg-id ...) and
 ; (e arg-id ...) is returned.
-(define (ref-expr! solver e env quantified encoder)
+(define (ref-expr! e env quantified encoder)
   (let ([k (cons e quantified)])
     (or (hash-ref env k #f) 
-        (match (encoder solver e env quantified) 
+        (match (encoder e env quantified) 
           [(? pair? enc)
            (let ([id (smt-id 'e (hash-count env))])
              (cond [(null? quantified)

rosette/solver/smt/stp.rkt

@@ -7,8 +7,7 @@
 
 (provide (rename-out [make-stp stp]) stp? stp-available?)
 
-(define-runtime-path bin-path (build-path ".." ".." ".." "bin"))
+(define-runtime-path stp-path (build-path ".." ".." ".." "bin" "stp"))
-(define stp-path (build-path bin-path "stp"))
 (define stp-opts '("--SMTLIB2"))
 
 (define (stp-available?)
@@ -63,10 +62,8 @@
      (base/solver-check self))
 
    (define (solver-debug self)
-     (base/solver-debug self))
+     (base/solver-debug self))])
-
-   (define (solver-custom-encode self expr env quantified)
-     (base/solver-custom-encode self expr env quantified))])
 
 (define (set-default-options server)
   void)
+  

rosette/solver/smt/yices.rkt

@@ -7,8 +7,7 @@
 
 (provide (rename-out [make-yices yices]) yices? yices-available?)
 
-(define-runtime-path bin-path (build-path ".." ".." ".." "bin"))
+(define-runtime-path yices-path (build-path ".." ".." ".." "bin" "yices-smt2"))
-(define yices-path (build-path bin-path "yices-smt2"))
 (define yices-opts '("--incremental"))
 
 (define (yices-available?)
@@ -63,10 +62,8 @@
      (base/solver-check self))
 
    (define (solver-debug self)
-     (base/solver-debug self))
+     (base/solver-debug self))])
-
-   (define (solver-custom-encode self expr env quantified)
-     (base/solver-custom-encode self expr env quantified))])
 
 (define (set-default-options server)
   void)
+  

rosette/solver/smt/z3.rkt

@@ -1,19 +1,18 @@
 #lang racket
 
 (require racket/runtime-path racket/hash
-         "server.rkt" "cmd.rkt" "enc.rkt" "env.rkt" 
+         "server.rkt" "cmd.rkt" "env.rkt" 
          "../solver.rkt" "../solution.rkt"
          (prefix-in base/ "base-solver.rkt")
          (only-in racket [remove-duplicates unique])
          (only-in "smtlib2.rkt" reset set-option check-sat)
-         (only-in "../../base/core/term.rkt" expression expression? term term? term-type)
+         (only-in "../../base/core/term.rkt" term term? term-type)
-         (only-in "../../base/core/bitvector.rkt" bitvector? bv? @bvrol @bvror)
+         (only-in "../../base/core/bitvector.rkt" bitvector? bv?)
          (only-in "../../base/core/real.rkt" @integer? @real?))
 
 (provide (rename-out [make-z3 z3]) z3?)
 
-(define-runtime-path bin-path (build-path ".." ".." ".." "bin"))
+(define-runtime-path z3-path (build-path ".." ".." ".." "bin" "z3"))
-(define z3-path (build-path bin-path "z3"))
 (define z3-opts '("-smt2" "-in"))
 
 (define default-options
@@ -46,7 +45,7 @@
   #:methods gen:solver
   [
    (define (solver-features self)
-     '(qf_bv qf_uf qf_lia qf_nia qf_lra qf_nra quantifiers optimize unsat-cores int2bv ext_rotate))
+     '(qf_bv qf_uf qf_lia qf_nia qf_lra qf_nra quantifiers optimize unsat-cores int2bv))
    
    (define (solver-options self)
      (base/solver-options self))
@@ -77,7 +76,7 @@
      (base/solver-pop self k))
    
    (define (solver-check self)
-     (base/solver-check self z3-read-solution))
+     (base/solver-check self))
 
    (define (solver-debug self)
      (match-define (z3 server _ (app unique asserts) _ _ _ _) self)
@@ -87,19 +86,9 @@
                  (set-core-options (base/solver-server self))
                  (server-write
                   server
-                  (begin (encode-for-proof self (base/solver-env self) asserts)
+                  (begin (encode-for-proof (base/solver-env self) asserts)
                          (check-sat)))
-                 (z3-read-solution server (base/solver-env self) #:unsat-core? #t)]))
+                 (base/read-solution server (base/solver-env self) #:unsat-core? #t)]))])
-
-   (define (solver-custom-encode self expr env quantified)
-     (match expr
-       [(expression (== @bvrol) a b)
-        (list 'ext_rotate_left
-              (enc self a env quantified) (enc self b env quantified))]
-       [(expression (== @bvror) a b)
-        (list 'ext_rotate_right
-              (enc self a env quantified) (enc self b env quantified))]
-       [_ (base/solver-custom-encode self expr env quantified)]))])
 
 (define (set-core-options server)
   (server-write server
@@ -112,27 +101,3 @@
     (match t
       [(term _ (or (== @integer?) (== @real?) (? bitvector?))) t]
       [_ (error caller "expected a numeric term, given ~s" t)])))
-
-(define (z3-read-solution server env #:unsat-core? [unsat-core? #f])
-  (decode (match (base/parse-solution server #:unsat-core? unsat-core?)
-            [(? hash? sol) (prune-model sol)]
-            [soln soln])
-          env))
-
-; Given a map M from symbols to SMTLib function definitions of the form
-; (define-fun id ((param type) ...) ret body),
-; this procedure eliminate bindings for intermediate expressions,
-; which are ids that start with "e" (e.g. "e20"),
-; originally defined with define-fun (as opposed to declare-fun) in the query.
-; In particular, old versions of Z3 did this pruning automatically,
-; and Rosette had been working under this assumption.
-; Newer versions of Z3 however included extra bindings,
-; so we are pruning them away.
-(define (prune-model sol)
-  (for/hash ([(k v) (in-immutable-hash sol)]
-             #:unless (match v
-                        [`(define-fun ,(? symbol? (app symbol->string id)) ,_ ,_ ,_)
-                         #:when (string-prefix? id "e")
-                         #t]
-                        [_ #f]))
-    (values k v)))

rosette/solver/solver.rkt

@@ -7,7 +7,6 @@
          solver-minimize solver-maximize
          solver-check solver-debug 
          solver-shutdown solver-features solver-options
-         solver-custom-encode
          prop:solver-constructor solver-constructor
          )
 
@@ -54,10 +53,6 @@
 ;
 ; The solver-options procedure returns a hash table of options the solver
 ; is configured with.
-;
-; The solver-custom-encode procedure allows extending the SMT-LIB encoding and decoding
-; operations for that specific solver to allow for custom extensions implemented by that
-; solver or behavior that differs between solvers.
 (define-generics solver
   [solver-assert solver bools]
   [solver-push solver]
@@ -69,8 +64,7 @@
   [solver-debug solver]
   [solver-shutdown solver]
   [solver-features solver]
-  [solver-options solver]
+  [solver-options solver])
-  [solver-custom-encode solver expr env quantified])
 
 ; Solvers should implement the prop:solver-constructor type property
 ; to provide the procedure used to construct new solvers of the same type.

test/base/bvlib.rkt

@@ -269,27 +269,6 @@
    #:features '(qf_bv)
    (check-bvrotate bvror bvrol)))
 
-(define tests:bvrotate-enc
-  (test-suite+
-    "Tests for encoding of bvrol/bvror in rosette/base/bvlib.rkt"
-    #:features '(ext_rotate)
-    (define out (open-output-string))
-    (output-smt out)
-    (define-symbolic a b (bitvector 32))
-    (solve
-      (begin
-        (assert (bveq (bv #x0000abcd 32) (bvrol a b)))
-        (assert (bveq (bv #x00abcd00 32) (bvror a b)))))
-    (output-smt #f)
-    (check-pred
-      (λ (s)
-        (and
-          (or (string-contains? s "ext_rotate_left")
-              (string-contains? s "bvrol"))
-          (or (string-contains? s "ext_rotate_right")
-              (string-contains? s "bvror"))))
-      (get-output-string out))))
-
 (define tests:rotate-left
   (test-suite+
    "Tests for rotate-left in rosette/base/bvlib.rkt"
@@ -317,7 +296,6 @@
   (time (run-tests tests:bvsmax))
   (time (run-tests tests:bvrol))
   (time (run-tests tests:bvror)) 
-  (time (run-tests tests:bvrotate-enc)) 
   (time (run-tests tests:rotate-left))
   (time (run-tests tests:rotate-right))
   )

test/query/solve.rkt

@@ -65,9 +65,8 @@
       (check-pred
        unknown?
        (solve
-        (assert (forall (list xi)
+        (begin (assert (> (* xi xi) 3))
-                        (exists (list xr)
+               (assert (= (+ (* xr xr xr) (* xr yr)) 3.0))))))))
-                                (= yi (* (- xi xr) (- xi xr)))))))))))
      
 (define regression-tests 
   (test-suite+ "Solve regression tests."