uwplse / syncro

Synthesis of Incremental Operations
2 stars 1 forks source link

Discuss over the number of temps and constants #13

Open Sumith1896 opened 7 years ago

Sumith1896 commented 7 years ago

Are we sure about the hypothesis that increasing the number of temporaries (and constants) in the grammar eases the synthesis? For example, when the tool just has to come up with num-T incremented by 1, it does the following:

(let ()
       (define tmp64844 (+ SET_SIZE num-T))
       (define tmp64845 (enum-set-contains? T? m))
       (begin (enum-set-add! T? m))
       (let ()
         (define constant76257 1)
         (define tmp76258 (+ tmp64844 constant76257))
         (let ()
           (if tmp64845 (set! num-T tmp64844) (set! num-T tmp76258))
           (set! num-T (- num-T SET_SIZE)))))
rohinmshah commented 7 years ago

Increasing the number of temporaries and constants certainly makes synthesis harder, since it is searching over a larger search space. (There are more correct solutions, but still it is harder.) The reason for doing this is that you need a sufficiently large search space that the correct program is actually in the space. For our microbenchmarks, it would probably help quite a bit to reduce the number of constants and temporaries, but if we did that then for our larger benchmarks we might not be able to synthesize anything at all, because the correct program would not be in there.