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

@@ -14,8 +14,7 @@
 
 (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?)

rosette/solver/smt/boolector.rkt

@@ -14,8 +14,7 @@
 
 (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?)

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?)

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?)

rosette/solver/smt/dec.rkt

@@ -14,7 +14,6 @@
                   @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))
 
 
@@ -162,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))

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?)
@@ -67,3 +66,4 @@
 
 (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?)
@@ -67,3 +66,4 @@
 
 (define (set-default-options server)
   void)
+  

rosette/solver/smt/z3.rkt

@@ -12,8 +12,7 @@
 
 (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
@@ -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)
@@ -89,7 +88,7 @@
                   server
                   (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 (set-core-options server)
   (server-write server
@@ -102,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)))

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."