search

emina / rosette

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

Disallow define-symbolic with different types #240

Closed sorawee closed 2 years ago

sorawee commented 2 years ago

Programs like:

(define (f type)
  (define-symbolic x type)
  x)

(+ 1 (f integer?))
(+ 2 (f boolean?))

should not work. The second call in particular should result in an error, rather than using the cached term (which is an integer).

This PR makes the above program invalid. The SDSL benchmarks show that the performance was not affected by the change.

The issue was originally discovered by @gussmith23.

emina commented 2 years ago

Thanks!

gussmith23 commented 2 years ago

thank you both!

On Wed, Aug 17, 2022, 4:15 PM Emina Torlak @.***> wrote:

Thanks!

— Reply to this email directly, view it on GitHub https://github.com/emina/rosette/pull/240#issuecomment-1218618688, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAJFZAP25K5YFFYOZFHUQDTVZVXAPANCNFSM56YNMAPA . You are receiving this because you were mentioned.Message ID: @.***>