Make evaluate preserve vector immutability (emina#244)

Prior to this patch, the following returned an immutable vector: (define empty-model (solve (void))) (evaluate (vector-immutable 1) empty-model) However, the following returned a _mutable_ vector, even though `evaluate` is given an immutable vector (containing no symbolics): (define-symbolic* b boolean?) (define model (solve (assert b))) (evaluate (vector-immutable 1) model) With this patch, both examples above return an immutable vector.
jamestiotio · Oct 17, 2022 · 7e69613 · 7e69613
1 parent 4c23c80
commit 7e69613
Showing 1 changed file with 4 additions and 1 deletion.
diff --git a/rosette/query/eval.rkt b/rosette/query/eval.rkt
@@ -47,7 +47,10 @@
                [(cons x y)               
                 (cons (eval-rec x sol cache) (eval-rec y sol cache))]
                [(? vector?)              
-                (for/vector #:length (vector-length expr) ([e expr]) (eval-rec e sol cache))]
+                (let ([v (for/vector #:length (vector-length expr) ([e expr]) (eval-rec e sol cache))])
+                  (if (immutable? expr)
+                      (vector->immutable-vector v)
+                      v))]
                [(? box?)
                 ((if (immutable? expr) box-immutable box) (eval-rec (unbox expr) sol cache))]
                [(? typed?)