wip: feat: add support for z3 bit rotate exts

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

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

rosette/solver/smt/boolector.rkt

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

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

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

rosette/solver/smt/dec.rkt

@@ -15,7 +15,7 @@
                   @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 @sign-extend @zero-extend))
+                  @concat @extract))
 
 
 (provide decode-model)
@@ -132,10 +132,6 @@
         (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 i sol ~env) ,(inline s sol ~env))]
-       [(list (list (== '_) (== 'zero_extend) i) s)
-        `(, @zero-extend ,(inline i sol ~env) ,(inline s sol ~env))]
        [(list (== 'let) binds body)
         (substitute (inline body sol ~env)
                     (for/hash ([id:expr binds])

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

rosette/solver/smt/z3.rkt

@@ -12,7 +12,8 @@
 
 (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
@@ -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)
@@ -88,7 +89,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
@@ -101,3 +102,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)))

test/query/solve.rkt

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