emina / rosette

The Rosette solver-aided host language, sample solver-aided DSLs, and demos
Other
638 stars 74 forks source link

Make evaluate preserve vector immutability #244

Closed anishathalye closed 1 year ago

anishathalye commented 1 year ago

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.

emina commented 1 year ago

Thank you!