emina / rosette

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

seq: optimize append #280

Open sorawee opened 7 months ago

sorawee commented 7 months ago

There are two changes in this commit.

The first change builds the list from a variadic append operation from right to left, which is the natural order for list construction. This speeds up the following program:

(time
 (void
  (append* (for/list ([i 30000])
             (if b '() '(1))))))

from 5 seconds to 1 second.

The second change avoids making an assertion when doing unsafe/append on two symbolic unions. This is fine because all calls to unsafe/append is already guarded via type casting to make them symbolic unions of rosette-contract?, so there is no need to add another guard.

Thanks to @camoy for raising up the issue about the unnecessary assertions.