Closed gregr closed 8 years ago
30s -> 3s under Chez. About 33s -> 5s through the Barliman UI. I guess there's a bit more overhead there.
Thanks!
Can you tell if the faster system can now synthesize more of 'append'?
On Fri, Aug 12, 2016 at 12:53 PM, Greg Rosenblatt notifications@github.com wrote:
30s -> 3s under Chez. About 33s -> 5s through the Barliman UI. I guess there's a bit more overhead there.
— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/webyrd/Barliman/pull/11#issuecomment-239530445, or mute the thread https://github.com/notifications/unsubscribe-auth/ABHThF1fGpLHGsAQeTuRm37zdKY-IJirks5qfME0gaJpZM4JjW-B .
It can now synthesize a bit more than before. This query now succeeds, guessing the argument to null?:
(define append
(lambda (l s)
(if (null? ,A) ,B ,C)))
While guessing the full if condition, it finds a creative cheat that gets around the gensyms:
(define append
(lambda (l s)
(if ,A ,B ,C)))
Best guess:
(define append
(lambda (l s)
(if _.0
(match s
((quasiquote ())
s)
((quasiquote ((unquote _.1)))
(cons (car l) s))
(_.2
(cons (car l) (cons (car (cdr l)) _.2)))
. _.3)
_.4)))
Side conditions:
(num _.0)
(sym _.1 _.2)
Scaling it back to only guess the null? test leads to a different cheat:
(define append
(lambda (l s)
(if (,A ,D) ,B ,C)))
Best guess:
(define append
(lambda (l s)
(if (null? s)
s
(cons (car l)
(match s
((quasiquote ((unquote _.0)))
s)
(_.1
(cons (car (cdr l)) _.1))
. _.2)))))
Side conditions:
(sym _.0 _.1)
These are all performed with the following test cases:
(append '() '()) ==> '()
(append `(,g1) `(,g2)) ==> `(,g1 ,g2)
(append `(,g1 ,g2) `(,g3 ,g4 ,g5)) ==> `(,g1 ,g2 ,g3 ,g4 ,g5)
The new success takes about 19s under Chez.
The new success being a cheat?
I've been experimenting with using properties to help prevent over-specialization. In particular, the property that when l and s are proper lists, the output must be a proper list whose length is equal to the sum of the lengths of l and s.
I've been able to implement the property, but it is awkward to express, and alas doesn't help prune the search.
On Fri, Aug 12, 2016 at 1:29 PM, Greg Rosenblatt notifications@github.com wrote:
The new success takes about 19s under Chez.
— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/webyrd/Barliman/pull/11#issuecomment-239539058, or mute the thread https://github.com/notifications/unsubscribe-auth/ABHThEz3yGnp4qGo5IoMXTMxUtuNIkg2ks5qfMmjgaJpZM4JjW-B .
No, thankfully the new success is a real one that guesses the argument to null?
.
The rest of the queries result in cheats. I realize I should have used different gensyms for each test case, which should better avoid cheating, but I still can't get a result after several minutes of waiting.
No, thankfully the new success is a real one that guesses the argument to null?.
I was able to do that one before, actually, although I had to pick exactly the right arguments. However, I've never been able to guess the 'null?' part, at least without using types.
On Fri, Aug 12, 2016 at 2:39 PM, Greg Rosenblatt notifications@github.com wrote:
No, thankfully the new success is a real one that guesses the argument to null?.
The rest of the queries result in cheats. I realize I should have used different gensyms for each test case, which should better avoid cheating, but I still can't get a result after several minutes of waiting.
— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/webyrd/Barliman/pull/11#issuecomment-239554206, or mute the thread https://github.com/notifications/unsubscribe-auth/ABHThIS5ESeFGZWCldNEBmpunpLX-uh5ks5qfNoZgaJpZM4JjW-B .
I'll have to try the new version with my property hack.
On Fri, Aug 12, 2016 at 2:43 PM, William Byrd webyrd@gmail.com wrote:
No, thankfully the new success is a real one that guesses the argument to null?.
I was able to do that one before, actually, although I had to pick exactly the right arguments. However, I've never been able to guess the 'null?' part, at least without using types.
On Fri, Aug 12, 2016 at 2:39 PM, Greg Rosenblatt <notifications@github.com
wrote:
No, thankfully the new success is a real one that guesses the argument to null?.
The rest of the queries result in cheats. I realize I should have used different gensyms for each test case, which should better avoid cheating, but I still can't get a result after several minutes of waiting.
— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/webyrd/Barliman/pull/11#issuecomment-239554206, or mute the thread https://github.com/notifications/unsubscribe-auth/ABHThIS5ESeFGZWCldNEBmpunpLX-uh5ks5qfNoZgaJpZM4JjW-B .
This improves the performance of some hard benchmarks by about 10x when running directly under Chez.