A plan for optimizing PLE #500
Comments
|
Hi @facundominguez -- these are excellent observations, thanks! I suspect some of them will get addressed with the |
|
@ranjitjhala Is there a PR for that, or has it been merged already? |
|
Hello! I've been quietly working on this during the last weeks. I accumulated some achievements but I have been finding tests again and again which challenged my understanding of the interactions of PLE with LH. At the moment, I have only one test failing: my own Here's a list of the more interesting things that I have implemented
I did other little experiments that I leave to discuss when I start the prs. Here's the work-in-progress. As usual, I'm keeping the commits small, and will try to get them merged in smaller chunks. The few benchmarks I ran don't show huge speed ups, but I think the code in PLE is simpler and the quality of the produced dumps is improved. The produced equalities are fewer and smaller to the point that I believe they approach what a human would have written for the task. Anyway, I'm going to revisit the benchmarks when I get all of the tests passing. I'm going to be taking some vacation time soon, so likely merging and discussing all this is going to extend well into May. |
I spent some time last week looking at dumps of formulas from PLE, and it is looking like we could go far by reducing the amount of equations that are produced and then their size.
There are some categories of equations in the output, discussed below. I have the impression that addressing these, and some redundant computations, the PLE version based on
fastEvalcould be sped up to less than half the time it takes today. I have some prototype implementation to build this intuition, but it still fails on some tests.I still would need to understand PLE with autorewrites to know how this story works there, but I wanted to share these thoughts in case they inspire others working on LF.
1. Equations that reduce datatype selectors
Equations like
or
The SMT solver knows about datatypes, so one could hope that spelling this equalities is redundant.
#499 gets rid of the equalities involving selectors. I haven't explored how to eliminate the constructor tests.
2. Reduction of if-then-else
The following equality states that the top level if-then-else can be reduced since its condition is known to be False.
But if the SMT solver knows that the condition of the if-then-else is False, it already knows that this equation holds! There is no point either in asserting it explicitly.
3. Unfoldings of recursive functions
The following equation unfolds a call to a reflected function called
checkBindings. Every invocation of the function duplicates pretty much the whole body.I'm thinking that it should be possible to serialize the body of the function without recursion once for all of PLE, and rewrite the above equality as
which leaves to the SMT solver the trouble of unfolding
checkBindingsNonRecursivewhich should have been previously defined as4. Nested unfoldings
Equalities of the form
are unnecessarily verbose since they duplicate the context in which
gis invoked. Unlessxis bound by a lambda in the context (which appears to be a rare situation), the same information can be conveyed withg x = body_of_gThe text was updated successfully, but these errors were encountered: