From de7016ea21c3e85dd8b3b75055e48af9b0aa1542 Mon Sep 17 00:00:00 2001
From: Sorawee Porncharoenwase <sorawee.pwase@gmail.com>
Date: Tue, 5 Mar 2024 05:27:26 -0800
Subject: [PATCH] z3: bump version to 4.12.6

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.
---
 rosette/private/install.rkt | 32 +++++++++++++++-----------------
 rosette/solver/smt/dec.rkt  |  8 +++++++-
 test/query/solve.rkt        |  5 +++--
 3 files changed, 25 insertions(+), 20 deletions(-)

diff --git a/rosette/private/install.rkt b/rosette/private/install.rkt
index 5ae12314..4709ab39 100644
--- a/rosette/private/install.rkt
+++ b/rosette/private/install.rkt
@@ -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")
@@ -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)))
diff --git a/rosette/solver/smt/dec.rkt b/rosette/solver/smt/dec.rkt
index 408d0c58..753f1232 100644
--- a/rosette/solver/smt/dec.rkt
+++ b/rosette/solver/smt/dec.rkt
@@ -14,7 +14,7 @@
                   @bvslt @bvsle @bvult @bvule   
                   @bvnot @bvor @bvand @bvxor @bvshl @bvlshr @bvashr
                   @bvneg @bvadd @bvmul @bvudiv @bvsdiv @bvurem @bvsrem @bvsmod
-                  @concat @extract))
+                  @concat @extract @sign-extend @zero-extend @integer->bitvector))
 
 
 (provide decode-model)
@@ -131,6 +131,12 @@
         (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 s sol ~env) ,(bitvector (inline i sol ~env)))]
+       [(list (list (== '_) (== 'zero_extend) i) s)
+        `(, @zero-extend ,(inline s sol ~env) ,(bitvector (inline i sol ~env)))]
+       [(list (list (== '_) (== 'int2bv) i) s)
+        `(, @integer->bitvector ,(inline s sol ~env) ,(bitvector (inline i sol ~env)))]
        [(list (== 'let) binds body)
         (substitute (inline body sol ~env)
                     (for/hash ([id:expr binds])
diff --git a/test/query/solve.rkt b/test/query/solve.rkt
index 52453739..77c995ff 100644
--- a/test/query/solve.rkt
+++ b/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."