support non-indexed bit rotate where possible

rosette (for convenience) provides functionality to download and install
a z3 binary during raco installation. unfortunately this package is
currently very out of date, so this commit removes all install-time
functionality, causing rosette to fall back to searching for the z3
binary in the system PATH

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
+     @bvnot @bvor @bvand @bvxor @bvshl @bvlshr @bvashr @bvrol @bvror
      @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 bvrol bvror
+     rotate-left rotate-right
      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
+ @bvnot @bvor @bvand @bvxor @bvshl @bvlshr @bvashr @bvrol @bvror
  @bvneg @bvadd @bvsub @bvmul @bvudiv @bvsdiv @bvurem @bvsrem @bvsmod
  @concat @extract @sign-extend @zero-extend
  @integer->bitvector @bitvector->integer @bitvector->natural)
@@ -338,6 +338,29 @@
      (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)
@@ -345,6 +368,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 @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 bvrol bvror
+         rotate-left rotate-right
          bool->bitvector bitvector->bool bitvector->bits)
 
 (define-syntax (define-lifted stx)
@@ -79,15 +79,3 @@
 (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,11 +14,7 @@
      (experimental))))
      ;; Documentation category. On Racket 6.3+ this can be any string.
 
-;; 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 compile-omit-files '("lib/trace/report/node_modules"))
 
 (define raco-commands
   '(("symprofile"

rosette/private/install.rkt

@@ -1,84 +0,0 @@
-#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,10 +27,11 @@
   (current-solver (z3)))
 
 (provide
- (except-out (all-from-out "solver/solver.rkt") prop:solver-constructor solver-constructor)
+ (except-out (all-from-out "solver/solver.rkt")
+             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,12 +1,13 @@
 #lang racket
 
-(require "server.rkt" "cmd.rkt" "env.rkt" 
+(require "server.rkt" "cmd.rkt" "enc.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" term term? term-type)
+         (only-in "../../base/core/term.rkt" expression expression? term term? term-type get-type)
          (only-in "../../base/core/bool.rkt" @boolean?)
-         (only-in "../../base/core/bitvector.rkt" bitvector? bv?)
+         (only-in "../../base/core/bitvector.rkt" bitvector? bitvector-size bv bv?
+                  @bvshl @bvlshr @bvor @bvrol @bvror @bvsub @bvurem)
          (only-in "../../base/core/real.rkt" @integer? @real?)
          (only-in "../../base/core/reporter.rkt" current-reporter))
 
@@ -76,7 +77,7 @@
    server
    (begin
      ((current-reporter) 'encode-start)
-     (encode env asserts mins maxs)
+     (encode self env asserts mins maxs)
      ((current-reporter) 'encode-finish)
      (push)))
   (solver-clear-stacks! self)
@@ -99,7 +100,7 @@
                server
                (begin
                  ((current-reporter) 'encode-start)
-                 (encode env asserts mins maxs)
+                 (encode self env asserts mins maxs)
                  ((current-reporter) 'encode-finish)
                  (check-sat)))
               ((current-reporter) 'solve-start)
@@ -114,6 +115,29 @@
 (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 '())
@@ -161,4 +185,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,19 +2,20 @@
 #lang racket
 
 (require racket/runtime-path 
-         "server.rkt" "cmd.rkt" "env.rkt" 
+         "server.rkt" "cmd.rkt" "enc.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/bitvector.rkt" bitvector bitvector? bv? bv bv-value @extract @sign-extend @zero-extend @bveq @bvrol @bvror)
          (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-runtime-path bin-path (build-path ".." ".." ".." "bin"))
+(define bitwuzla-path (build-path bin-path "bitwuzla"))
 (define bitwuzla-opts '("-m"))
 
 (define (bitwuzla-available?)
@@ -39,7 +40,7 @@
   #:methods gen:solver
   [
    (define (solver-features self)
-     '(qf_bv))
+     '(qf_bv ext_rotate))
    
    (define (solver-options self)
      (base/solver-options self))
@@ -69,7 +70,17 @@
      (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,20 +1,21 @@
 #lang racket
 
 (require racket/runtime-path 
-         "server.rkt" "cmd.rkt" "env.rkt" 
+         "server.rkt" "cmd.rkt" "enc.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)
+         (only-in "../../base/core/bitvector.rkt" bitvector bitvector? bv? bv bv-value @extract @sign-extend @zero-extend @bveq @bvrol @bvror)
          (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 boolector-path (build-path ".." ".." ".." "bin" "boolector"))
+(define-runtime-path bin-path (build-path ".." ".." ".." "bin"))
+(define boolector-path (build-path bin-path "boolector"))
 (define boolector-opts '("-m" "--output-format=smt2" "-i"))
 
 (define (boolector-available?)
@@ -69,7 +70,10 @@
      (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 env asserts mins maxs)
+(define (encode solver env asserts mins maxs)
   ((current-reporter) 'to-solver asserts mins maxs)
   (for ([a asserts])
-    (assert (enc a env)))
+    (assert (enc solver a env)))
   (for ([m mins])
-    (minimize (enc m env)))
+    (minimize (enc solver m env)))
   (for ([m maxs])
-    (maximize (enc m env))))
+    (maximize (enc solver 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 env asserts)
+(define (encode-for-proof solver env asserts)
   (for ([a asserts])
-    (define id (enc a env))
+    (define id (enc solver 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,7 +7,8 @@
 
 (provide (rename-out [make-cvc4 cvc4]) cvc4? cvc4-available?)
 
-(define-runtime-path cvc4-path (build-path ".." ".." ".." "bin" "cvc4"))
+(define-runtime-path bin-path (build-path ".." ".." ".." "bin"))
+(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?)
@@ -62,7 +63,10 @@
      (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,7 +7,8 @@
 
 (provide (rename-out [make-cvc5 cvc5]) cvc5? cvc5-available?)
 
-(define-runtime-path cvc5-path (build-path ".." ".." ".." "bin" "cvc5"))
+(define-runtime-path bin-path (build-path ".." ".." ".." "bin"))
+(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?)
@@ -62,7 +63,10 @@
      (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
+                  @bvnot @bvor @bvand @bvxor @bvshl @bvlshr @bvashr @bvrol @bvror
                   @bvneg @bvadd @bvmul @bvudiv @bvsdiv @bvurem @bvsrem @bvsmod
                   @concat @extract))
 
@@ -161,6 +161,9 @@
         '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,6 +2,7 @@
 
 (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?)
@@ -26,54 +27,58 @@
 ; 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 v env [quantified '()])
+(define (enc solver v env [quantified '()])
   (match v
-    [(? expression?) (ref-expr! v env quantified enc-expr)]
+    [(? expression?) (ref-expr! solver v env quantified enc-expr)]
     [(? constant?)   (ref-const! v env quantified)]
-    [_               (ref-expr! v env quantified enc-lit)]))
+    [_               (ref-expr! solver v env quantified enc-lit)]))
 
-(define (enc-expr v env quantified)  
+(define (enc-expr solver 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 (guarded-test gv) env quantified) 
-                          (enc (guarded-value gv) env quantified) 
+                    ($ite (enc solver (guarded-test gv) env quantified) 
+                          (enc solver (guarded-value gv) env quantified) 
                           $0))))]
     [(expression (== @abs) x)
-     ($real-abs (enc x env quantified) (get-type v))]
+     ($real-abs (enc solver x env quantified) (get-type v))]
     [(expression (== @extract) i j e)
-     ($extract i j (enc e env quantified))]
+     ($extract i j (enc solver e env quantified))]
     [(expression (== @sign-extend) v t)
      ($sign_extend (- (bitvector-size t) (bitvector-size (get-type v)))
-                   (enc v env quantified))]
+                   (enc solver v env quantified))]
     [(expression (== @zero-extend) v t)
      ($zero_extend (- (bitvector-size t) (bitvector-size (get-type v)))
-                   (enc v env quantified))]
+                   (enc solver v env quantified))]
     [(expression (== @integer->bitvector) v t) 
-     ($int->bv (enc v env quantified) (bitvector-size t))]
+     ($int->bv (enc solver v env quantified) (bitvector-size t))]
     [(expression (== @bitvector->integer) v) 
-     ($bv->int (enc v env quantified) (bitvector-size (get-type v)))]  
+     ($bv->int (enc solver v env quantified) (bitvector-size (get-type v)))]  
     [(expression (== @bitvector->natural) v) 
-     ($bv->nat (enc v env quantified) (bitvector-size (get-type v)))]
+     ($bv->nat (enc solver 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 body env vars+quantified)))]
+        (enc solver 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 e env quantified))))]
+                              (for/list ([e es]) (enc solver e env quantified))))]
     [(expression (app rosette->smt (? procedure? $op)) es ...) 
-     (apply $op (for/list ([e es]) (enc e env quantified)))]
-    [_ (error 'enc "cannot encode ~a to SMT" v)]))
+     (apply $op (for/list ([e es]) (enc solver e env quantified)))]
+    [_
+     (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 v env quantified)
+(define (enc-lit solver 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 e env quantified) to obtain the encoding enc.
+; Otherwise, ref-expr! evaluates (encoder solver 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! e env quantified encoder)
+(define (ref-expr! solver e env quantified encoder)
   (let ([k (cons e quantified)])
     (or (hash-ref env k #f) 
-        (match (encoder e env quantified) 
+        (match (encoder solver e env quantified) 
           [(? pair? enc)
            (let ([id (smt-id 'e (hash-count env))])
              (cond [(null? quantified)

rosette/solver/smt/stp.rkt

@@ -7,7 +7,8 @@
 
 (provide (rename-out [make-stp stp]) stp? stp-available?)
 
-(define-runtime-path stp-path (build-path ".." ".." ".." "bin" "stp"))
+(define-runtime-path bin-path (build-path ".." ".." ".." "bin"))
+(define stp-path (build-path bin-path "stp"))
 (define stp-opts '("--SMTLIB2"))
 
 (define (stp-available?)
@@ -62,8 +63,10 @@
      (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,7 +7,8 @@
 
 (provide (rename-out [make-yices yices]) yices? yices-available?)
 
-(define-runtime-path yices-path (build-path ".." ".." ".." "bin" "yices-smt2"))
+(define-runtime-path bin-path (build-path ".." ".." ".." "bin"))
+(define yices-path (build-path bin-path "yices-smt2"))
 (define yices-opts '("--incremental"))
 
 (define (yices-available?)
@@ -62,8 +63,10 @@
      (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,18 +1,19 @@
 #lang racket
 
 (require racket/runtime-path racket/hash
-         "server.rkt" "cmd.rkt" "env.rkt" 
+         "server.rkt" "cmd.rkt" "enc.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" term term? term-type)
-         (only-in "../../base/core/bitvector.rkt" bitvector? bv?)
+         (only-in "../../base/core/term.rkt" expression expression? term term? term-type)
+         (only-in "../../base/core/bitvector.rkt" bitvector? bv? @bvrol @bvror)
          (only-in "../../base/core/real.rkt" @integer? @real?))
 
 (provide (rename-out [make-z3 z3]) z3?)
 
-(define-runtime-path z3-path (build-path ".." ".." ".." "bin" "z3"))
+(define-runtime-path bin-path (build-path ".." ".." ".." "bin"))
+(define z3-path (build-path bin-path "z3"))
 (define z3-opts '("-smt2" "-in"))
 
 (define default-options
@@ -45,7 +46,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))
+     '(qf_bv qf_uf qf_lia qf_nia qf_lra qf_nra quantifiers optimize unsat-cores int2bv ext_rotate))
    
    (define (solver-options self)
      (base/solver-options self))
@@ -76,7 +77,7 @@
      (base/solver-pop self k))
    
    (define (solver-check self)
-     (base/solver-check self))
+     (base/solver-check self z3-read-solution))
 
    (define (solver-debug self)
      (match-define (z3 server _ (app unique asserts) _ _ _ _) self)
@@ -86,9 +87,19 @@
                  (set-core-options (base/solver-server self))
                  (server-write
                   server
-                  (begin (encode-for-proof (base/solver-env self) asserts)
+                  (begin (encode-for-proof self (base/solver-env self) asserts)
                          (check-sat)))
-                 (base/read-solution server (base/solver-env self) #:unsat-core? #t)]))])
+                 (z3-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
@@ -101,3 +112,27 @@
     (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,6 +7,7 @@
          solver-minimize solver-maximize
          solver-check solver-debug 
          solver-shutdown solver-features solver-options
+         solver-custom-encode
          prop:solver-constructor solver-constructor
          )
 
@@ -53,6 +54,10 @@
 ;
 ; 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]
@@ -64,7 +69,8 @@
   [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,6 +269,27 @@
    #: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"
@@ -296,6 +317,7 @@
   (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,8 +65,9 @@
       (check-pred
        unknown?
        (solve
-        (begin (assert (> (* xi xi) 3))
-               (assert (= (+ (* xr xr xr) (* xr yr)) 3.0))))))))
+        (assert (forall (list xi)
+                        (exists (list xr)
+                                (= yi (* (- xi xr) (- xi xr)))))))))))
      
 (define regression-tests 
   (test-suite+ "Solve regression tests."