News for hackers. Stuff that matters.

A comment on Learning to Superoptimize Programs. Parent comment

Re:Learning to Superoptimize Programs by bloaf on Sunday November 20, 2016 @12:13PM (#12999846)
But it seems to me that the fact that they have a theorem prover at all means they do know ahead of time what semantic preserving transformations are available.
[ Parent | on HN ]
Re:Learning to Superoptimize Programs by dom0 on Sunday November 20, 2016 @12:24PM (#12999910)
No. They have a verificator that can show that two (sub-)programs (more accurately; that an applied transformation preserves semantics) are semantically identical. This is a bit like a P-verificator for the solution to a NP-hard problem using a certificate. It can only help you prove that the solution is right, not find new solutions.
[ Parent | on HN ]