search

emina / rosette

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

avoid quadratic time processing in solver-(assert,min/maximize) #261

Closed sorawee closed 1 year ago

sorawee commented 1 year ago

The time complexity of n calls to solver-assert / solver-minimize / solver-maximize is currently O(n^2) due to list appending at the tail, which requires traversal. This PR fixes the problem. The ordering of solver-minimize and solver-maximize matters, however (it specifies the lexicographic ordering minimization), so rearranging them is slightly more complicated.

sorawee commented 1 year ago

Forgot to include this:

Before the PR:

raco test test/all-rosette-tests.rkt  44.16s user 85.68s system 48% cpu 4:29.50 total
raco test test/all-sdsl-tests.rkt  287.05s user 4.00s system 99% cpu 4:51.98 total

After the PR:

raco test test/all-rosette-tests.rkt  43.42s user 84.33s system 48% cpu 4:25.58 total
raco test test/all-sdsl-tests.rkt  282.47s user 4.16s system 99% cpu 4:47.60 total

So it doesn't look like there's a performance degrade.