wip: feat: add support for z3 bit rotate exts

z3 > 4.8.8 will return sign_extend and zero_extend operators in the
model, which were not handled by the smt-lib2 decoder, despite being
handled in the encoder. support for these operators has been added

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 bitwuzla-path (build-path bin-path "bitwuzla"))
+(define-runtime-path bitwuzla-path (build-path ".." ".." ".." "bin" "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 boolector-path (build-path bin-path "boolector"))
+(define-runtime-path boolector-path (build-path ".." ".." ".." "bin" "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 cvc4-path (build-path bin-path "cvc4"))
+(define-runtime-path cvc4-path (build-path ".." ".." ".." "bin" "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 cvc5-path (build-path bin-path "cvc5"))
+(define-runtime-path cvc5-path (build-path ".." ".." ".." "bin" "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))
+                  @concat @extract @sign-extend @zero-extend))
 
 
 (provide decode-model)
@@ -132,6 +132,10 @@
         (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,8 +7,7 @@
 
 (provide (rename-out [make-stp stp]) stp? stp-available?)
 
-(define-runtime-path bin-path (build-path ".." ".." ".." "bin"))
-(define stp-path (build-path bin-path "stp"))
+(define-runtime-path stp-path (build-path ".." ".." ".." "bin" "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 yices-path (build-path bin-path "yices-smt2"))
+(define-runtime-path yices-path (build-path ".." ".." ".." "bin" "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 z3-path (build-path bin-path "z3"))
+(define-runtime-path z3-path (build-path ".." ".." ".." "bin" "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)
-                        (exists (list xr)
-                                (= yi (* (- xi xr) (- xi xr)))))))))))
+        (begin (assert (> (* xi xi) 3))
+               (assert (= (+ (* xr xr xr) (* xr yr)) 3.0))))))))
      
 (define regression-tests 
   (test-suite+ "Solve regression tests."