Skip to content

Commit

Permalink
z3: bump version to 4.12.6
Browse files Browse the repository at this point in the history
4.12.6 is the latest version released last week.
The main motivation for the upgrade, though, is to get past 4.12.3,
as subsequent versions (4.12.4 onward) support aarch64 for Linux.
  • Loading branch information
sorawee committed Mar 6, 2024
1 parent edf682d commit 4cb6d19
Show file tree
Hide file tree
Showing 3 changed files with 44 additions and 21 deletions.
32 changes: 15 additions & 17 deletions rosette/private/install.rkt
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@
; far more obvious.
(define z3-install-failure #f)

(define z3-version "4.8.8")
(define z3-version "4.12.6")

(define (print-failure path msg)
(printf "\n\n********** Failed to install Z3 **********\n\n")
Expand Down Expand Up @@ -66,19 +66,17 @@
(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)))))
(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-glibc-2.35" "z3")]
['(linux aarch64) (values "arm64-glibc-2.35" "z3")]
['(macosx x86_64) (values "x64-osx-11.7.10" "z3")]
['(macosx aarch64) (values "arm64-osx-11.0" "z3")]
['(windows x86_64) (values "x64-win" "z3.exe")]
['(windows aarch64) (values "arm64-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)))
28 changes: 26 additions & 2 deletions rosette/solver/smt/z3.rkt
Original file line number Diff line number Diff line change
Expand Up @@ -74,7 +74,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)
Expand All @@ -86,7 +86,7 @@
server
(begin (encode-for-proof (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 (set-core-options server)
(server-write server
Expand All @@ -99,3 +99,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)))
5 changes: 3 additions & 2 deletions test/query/solve.rkt
Original file line number Diff line number Diff line change
Expand Up @@ -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."
Expand Down

0 comments on commit 4cb6d19

Please sign in to comment.