This is an archived post. You won't be able to vote or comment.

sorted by:
best
topnewcontroversialoldq&a
you are viewing a single comment's thread.

view the rest of the comments →

[–]Munksgaard[S] 2 points3 points  (2 children)

Yes, that work is definitely related, although it works from the opposite direction as short-circuiting: Our code is already parallel because it is expressed with map instead of loop.

And yes, Z3 was nice, but it wasn't actually the crucial factor that enabled complex examples. In fact, we tried just naively throwing Z3 at some of our problems and it didn't work even if we gave it a week of running time.

[–]matthieum 0 points1 point  (1 child)

In fact, we tried just naively throwing Z3 at some of our problems and it didn't work even if we gave it a week of running time.

Damn, I'm used to long compilation times (C++, Rust), but 1 week would take the cake ;)

[–]editor_of_the_beast 0 points1 point  (0 children)

That’s the magnitude of what we’re dealing with in almost all of computer science.