CozySynthesizer / cozy

The collection synthesizer
https://cozy.uwplse.org
Apache License 2.0
209 stars 18 forks source link

Improve flatMap handling #106

Closed izgzhen closed 5 years ago

izgzhen commented 5 years ago

Test

$ cd examples
$ make listcomp TIMEOUT=1 
cozy -t 1 --allow-big-sets listcomp-flatmap.ds --c++ listcomp.h -p 8080 --save listcomp.synthesized
...
Number of improvements done: 8
g++ -std=c++11 -O3 -Werror 'listcomp.cpp' -o 'listcomp'
$ ./listcomp 
0 0 0
100 18 676700
200 108 5373400
300 323 18090100
400 742 42826800
500 1413 83583500
600 2415 144360200
700 3815 229156900
800 5673 341973600
900 8057 486810300
^C
$ rm listcomp.h          
$ make listcomp TIMEOUT=10
cozy -t 10 --allow-big-sets listcomp-flatmap.ds --c++ listcomp.h -p 8080 --save listcomp.synthesized
...
Number of improvements done: 20
g++ -std=c++11 -O3 -Werror 'listcomp.cpp' -o 'listcomp'
$ ./listcomp              
0 0 0
100 0 676700
200 0 5373400
300 1 18090100
400 1 42826800
500 2 83583500
600 2 144360200
700 3 229156900
800 4 341973600
900 5 486810300
....
9900 358 646964013300

In the output of ./listcomp, the columns are: "current size of bag", "milliseconds between this and previous row", "accumulated sum". For details, please see examples/listcomp.cpp. From the second row, it is clear that the optimized flatMap makes the program much faster (see TODO graph). The third row are same across two runs, which validates the correctness of synthesis.

Figure_1

izgzhen commented 5 years ago

@Calvin-L Done! Thanks for the comments