search

fritzo / pomagma

An inference engine for extensional untyped λ-calculus
Other
17 stars 2 forks source link

Slowest survey programs #25

Closed fritzo closed 7 years ago

fritzo commented 9 years ago

From python -m pomagma explore skja:

2015:05:06:09:04
...
20094   1592.11     INFO    starting 16 survey threads
20094   26152.3     INFO    finished 16 survey threads
20094   26152.3     INFO    merge tasks: 4 executed / 4 scheduled
20094   26152.3     INFO    enforce tasks: 14317968 executed / 14317972 scheduled
20094   26152.3     INFO    sample tasks: 526 executed / 0 scheduled
20094   26152.3     INFO    cleanup tasks: 119521 executed / 0 scheduled
20094   26152.3     INFO    Profile of VirtualMachine programs:
20094   26152.3     INFO     Line       Calls Percent   Total sec Per call sec
20094   26152.3     INFO    ----- ----------- ------- ----------- ------------
20094   26152.3     INFO      906        2717   19.21    58181.18     21.41
20094   26152.3     INFO      914        2717   16.66    50454.45     18.57
20094   26152.3     INFO     4837    14178607   14.47    43805.89      0.00
20094   26152.3     INFO     1146        2717   11.52    34871.00     12.83
20094   26152.3     INFO      860        2964    7.49    22676.76      7.65
20094   26152.3     INFO      922        2717    5.51    16678.19      6.14
20094   26152.3     INFO     1211        2717    3.76    11381.47      4.19
...

Where the most expensive programs are

# line 906, plan 22: 22 bytes
FOR_BLOCK
FOR_ALL a
IF_BLOCK a
FOR_BINARY_FUNCTION_LHS COMP a b c
FOR_BINARY_FUNCTION_LHS APP b d e
INFER_BINARY_BINARY APP c d APP a e

# line 914, plan 23: 22 bytes
FOR_BLOCK
FOR_ALL a
IF_BLOCK a
FOR_BINARY_FUNCTION_LHS COMP a b c
FOR_BINARY_FUNCTION_LHS COMP b d e
INFER_BINARY_BINARY COMP a e COMP c d

# line 4837, plan 64: 3271 bytes
GIVEN_BINARY_RELATION NLESS a b
SEQUENCE 16
LETS_BINARY_RELATION_RHS LESS c b
LETS_BINARY_RELATION_LHS NLESS a d
FOR_POS_NEG e c d
INFER_BINARY_RELATION NLESS a e
SEQUENCE 16
LETS_BINARY_RELATION_LHS LESS a c
LETS_BINARY_RELATION_RHS NLESS d b
FOR_POS_NEG e c d
INFER_BINARY_RELATION NLESS e b
SEQUENCE 35
IF_NULLARY_FUNCTION Y b
FOR_NULLARY_FUNCTION I c
FOR_NULLARY_FUNCTION S d
FOR_BINARY_FUNCTION_LHS_RHS APP d c e
FOR_BINARY_FUNCTION_LHS_RHS APP e a f
SEQUENCE 8
IF_BINARY_RELATION LESS a f
INFER_BINARY_RELATION NLESS f a
IF_BINARY_RELATION LESS f a
INFER_BINARY_RELATION NLESS a f
PADDING
SEQUENCE 35
IF_NULLARY_FUNCTION Y a
FOR_NULLARY_FUNCTION I c
FOR_NULLARY_FUNCTION S d
FOR_BINARY_FUNCTION_LHS_RHS APP d c e
FOR_BINARY_FUNCTION_LHS_RHS APP e b f
SEQUENCE 8
IF_BINARY_RELATION LESS b f
INFER_BINARY_RELATION NLESS f b
IF_BINARY_RELATION LESS f b
INFER_BINARY_RELATION NLESS b f
PADDING
SEQUENCE 99
IF_NULLARY_FUNCTION TOP a
SEQUENCE 16
FOR_NULLARY_FUNCTION BOT c
FOR_NULLARY_FUNCTION DIV d
FOR_BINARY_FUNCTION_LHS_VAL APP d e b
INFER_BINARY_FUNCTION APP d e c
SEQUENCE 37
FOR_NULLARY_FUNCTION J c
IF_BINARY_RELATION NLESS b c
SEQUENCE 16
FOR_NULLARY_FUNCTION BOT d
FOR_NULLARY_FUNCTION BOOOL e
FOR_BINARY_FUNCTION_LHS_VAL APP e f b
INFER_BINARY_FUNCTION APP e f d
FOR_NULLARY_FUNCTION K d
FOR_NULLARY_FUNCTION BOOOL e
FOR_BINARY_FUNCTION_LHS_VAL APP e f b
INFER_BINARY_FUNCTION APP e f d
PADDING
SEQUENCE 46
FOR_NULLARY_FUNCTION I c
SEQUENCE 20
IF_BINARY_RELATION NLESS b c
FOR_NULLARY_FUNCTION BOT d
FOR_NULLARY_FUNCTION SEMI e
FOR_BINARY_FUNCTION_LHS_VAL APP e f b
INFER_BINARY_FUNCTION APP e f d
SEQUENCE 13
FOR_NULLARY_FUNCTION UNIT d
FOR_BINARY_FUNCTION_LHS_VAL APP d e b
INFER_BINARY_FUNCTION APP d e c
FOR_NULLARY_FUNCTION BOT d
IF_BINARY_RELATION NLESS b d
FOR_NULLARY_FUNCTION SEMI e
FOR_BINARY_FUNCTION_LHS_VAL APP e f b
INFER_BINARY_FUNCTION APP e f c
FOR_NULLARY_FUNCTION F c
SEQUENCE 20
FOR_NULLARY_FUNCTION J d
IF_BINARY_RELATION NLESS b d
FOR_NULLARY_FUNCTION BOOOL e
FOR_BINARY_FUNCTION_LHS_VAL APP e f b
INFER_BINARY_FUNCTION APP e f c
SEQUENCE 20
FOR_NULLARY_FUNCTION K d
IF_BINARY_RELATION NLESS b d
FOR_NULLARY_FUNCTION BOOL e
FOR_BINARY_FUNCTION_LHS_VAL APP e f b
INFER_BINARY_FUNCTION APP e f c
IF_BINARY_RELATION NLESS b c
SEQUENCE 23
FOR_NULLARY_FUNCTION J d
FOR_NULLARY_FUNCTION K e
IF_BINARY_RELATION NLESS b e
FOR_NULLARY_FUNCTION BOOOL f
FOR_BINARY_FUNCTION_LHS_VAL APP f g b
INFER_BINARY_FUNCTION APP f g d
FOR_NULLARY_FUNCTION K d
SEQUENCE 13
FOR_NULLARY_FUNCTION BOOL e
FOR_BINARY_FUNCTION_LHS_VAL APP e f b
INFER_BINARY_FUNCTION APP e f d
IF_BINARY_RELATION NLESS b d
FOR_NULLARY_FUNCTION BOT e
FOR_NULLARY_FUNCTION BOOL f
FOR_BINARY_FUNCTION_LHS_VAL APP f g b
INFER_BINARY_FUNCTION APP f g e
PADDING
PADDING
PADDING
PADDING
PADDING
PADDING
PADDING
SEQUENCE 99
IF_NULLARY_FUNCTION K b
FOR_NULLARY_FUNCTION F c
SEQUENCE 20
FOR_NULLARY_FUNCTION J d
IF_BINARY_RELATION NLESS d a
FOR_NULLARY_FUNCTION BOOOL e
FOR_BINARY_FUNCTION_LHS_VAL APP e f a
INFER_BINARY_FUNCTION APP e f c
SEQUENCE 20
FOR_NULLARY_FUNCTION TOP d
IF_BINARY_RELATION NLESS d a
FOR_NULLARY_FUNCTION BOOL e
FOR_BINARY_FUNCTION_LHS_VAL APP e f a
INFER_BINARY_FUNCTION APP e f c
SEQUENCE 59
IF_BINARY_RELATION NLESS c a
SEQUENCE 31
FOR_NULLARY_FUNCTION BOT d
SEQUENCE 13
FOR_NULLARY_FUNCTION BOOL e
FOR_BINARY_FUNCTION_LHS_VAL APP e f a
INFER_BINARY_FUNCTION APP e f d
FOR_NULLARY_FUNCTION BOOOL e
FOR_BINARY_FUNCTION_LHS_VAL APP e f a
INFER_BINARY_FUNCTION APP e f d
SEQUENCE 16
FOR_NULLARY_FUNCTION J d
FOR_NULLARY_FUNCTION BOOOL e
FOR_BINARY_FUNCTION_LHS_VAL APP e f a
INFER_BINARY_FUNCTION APP e f d
FOR_NULLARY_FUNCTION TOP d
SEQUENCE 13
FOR_NULLARY_FUNCTION BOOL e
FOR_BINARY_FUNCTION_LHS_VAL APP e f a
INFER_BINARY_FUNCTION APP e f d
FOR_NULLARY_FUNCTION BOOOL e
FOR_BINARY_FUNCTION_LHS_VAL APP e f a
INFER_BINARY_FUNCTION APP e f d
IF_BINARY_RELATION NLESS a c
SEQUENCE 16
FOR_NULLARY_FUNCTION TOP d
FOR_NULLARY_FUNCTION BOOL e
FOR_BINARY_FUNCTION_LHS_VAL APP e f a
INFER_BINARY_FUNCTION APP e f d
SEQUENCE 23
FOR_NULLARY_FUNCTION BOT d
FOR_NULLARY_FUNCTION TOP e
IF_BINARY_RELATION NLESS e a
FOR_NULLARY_FUNCTION BOOL f
FOR_BINARY_FUNCTION_LHS_VAL APP f g a
INFER_BINARY_FUNCTION APP f g d
FOR_NULLARY_FUNCTION J d
SEQUENCE 20
FOR_NULLARY_FUNCTION TOP e
IF_BINARY_RELATION NLESS e a
FOR_NULLARY_FUNCTION BOOOL f
FOR_BINARY_FUNCTION_LHS_VAL APP f g a
INFER_BINARY_FUNCTION APP f g d
IF_BINARY_RELATION NLESS d a
SEQUENCE 16
FOR_NULLARY_FUNCTION BOT e
FOR_NULLARY_FUNCTION BOOOL f
FOR_BINARY_FUNCTION_LHS_VAL APP f g a
INFER_BINARY_FUNCTION APP f g e
FOR_NULLARY_FUNCTION TOP e
FOR_NULLARY_FUNCTION BOOOL f
FOR_BINARY_FUNCTION_LHS_VAL APP f g a
INFER_BINARY_FUNCTION APP f g e
SEQUENCE 110
IF_NULLARY_FUNCTION K a
SEQUENCE 37
FOR_NULLARY_FUNCTION J c
IF_BINARY_RELATION NLESS b c
SEQUENCE 16
FOR_NULLARY_FUNCTION BOT d
FOR_NULLARY_FUNCTION BOOOL e
FOR_BINARY_FUNCTION_LHS_VAL APP e f b
INFER_BINARY_FUNCTION APP e f d
FOR_NULLARY_FUNCTION TOP d
FOR_NULLARY_FUNCTION BOOOL e
FOR_BINARY_FUNCTION_LHS_VAL APP e f b
INFER_BINARY_FUNCTION APP e f d
PADDING
FOR_NULLARY_FUNCTION F c
SEQUENCE 34
FOR_NULLARY_FUNCTION BOT d
IF_BINARY_RELATION NLESS b d
SEQUENCE 13
FOR_NULLARY_FUNCTION BOOL e
FOR_BINARY_FUNCTION_LHS_VAL APP e f b
INFER_BINARY_FUNCTION APP e f c
FOR_NULLARY_FUNCTION BOOOL e
FOR_BINARY_FUNCTION_LHS_VAL APP e f b
INFER_BINARY_FUNCTION APP e f c
PADDING
SEQUENCE 20
FOR_NULLARY_FUNCTION J d
IF_BINARY_RELATION NLESS b d
FOR_NULLARY_FUNCTION BOOOL e
FOR_BINARY_FUNCTION_LHS_VAL APP e f b
INFER_BINARY_FUNCTION APP e f c
SEQUENCE 59
IF_BINARY_RELATION NLESS b c
SEQUENCE 31
FOR_NULLARY_FUNCTION BOT d
SEQUENCE 13
FOR_NULLARY_FUNCTION BOOL e
FOR_BINARY_FUNCTION_LHS_VAL APP e f b
INFER_BINARY_FUNCTION APP e f d
FOR_NULLARY_FUNCTION BOOOL e
FOR_BINARY_FUNCTION_LHS_VAL APP e f b
INFER_BINARY_FUNCTION APP e f d
SEQUENCE 16
FOR_NULLARY_FUNCTION J d
FOR_NULLARY_FUNCTION BOOOL e
FOR_BINARY_FUNCTION_LHS_VAL APP e f b
INFER_BINARY_FUNCTION APP e f d
FOR_NULLARY_FUNCTION TOP d
SEQUENCE 13
FOR_NULLARY_FUNCTION BOOL e
FOR_BINARY_FUNCTION_LHS_VAL APP e f b
INFER_BINARY_FUNCTION APP e f d
FOR_NULLARY_FUNCTION BOOOL e
FOR_BINARY_FUNCTION_LHS_VAL APP e f b
INFER_BINARY_FUNCTION APP e f d
IF_BINARY_RELATION NLESS c b
SEQUENCE 48
FOR_NULLARY_FUNCTION J d
SEQUENCE 20
FOR_NULLARY_FUNCTION BOT e
IF_BINARY_RELATION NLESS b e
FOR_NULLARY_FUNCTION BOOOL f
FOR_BINARY_FUNCTION_LHS_VAL APP f g b
INFER_BINARY_FUNCTION APP f g d
IF_BINARY_RELATION NLESS b d
SEQUENCE 16
FOR_NULLARY_FUNCTION BOT e
FOR_NULLARY_FUNCTION BOOOL f
FOR_BINARY_FUNCTION_LHS_VAL APP f g b
INFER_BINARY_FUNCTION APP f g e
FOR_NULLARY_FUNCTION TOP e
FOR_NULLARY_FUNCTION BOOOL f
FOR_BINARY_FUNCTION_LHS_VAL APP f g b
INFER_BINARY_FUNCTION APP f g e
PADDING
FOR_NULLARY_FUNCTION BOT d
SEQUENCE 13
FOR_NULLARY_FUNCTION BOOL e
FOR_BINARY_FUNCTION_LHS_VAL APP e f b
INFER_BINARY_FUNCTION APP e f d
SEQUENCE 13
FOR_NULLARY_FUNCTION BOOOL e
FOR_BINARY_FUNCTION_LHS_VAL APP e f b
INFER_BINARY_FUNCTION APP e f d
IF_BINARY_RELATION NLESS b d
FOR_NULLARY_FUNCTION TOP e
SEQUENCE 13
FOR_NULLARY_FUNCTION BOOL f
FOR_BINARY_FUNCTION_LHS_VAL APP f g b
INFER_BINARY_FUNCTION APP f g e
FOR_NULLARY_FUNCTION BOOOL f
FOR_BINARY_FUNCTION_LHS_VAL APP f g b
INFER_BINARY_FUNCTION APP f g e
SEQUENCE 100
IF_NULLARY_FUNCTION J b
SEQUENCE 16
FOR_NULLARY_FUNCTION TOP c
FOR_NULLARY_FUNCTION BOOOL d
FOR_BINARY_FUNCTION_LHS_VAL APP d e a
INFER_BINARY_FUNCTION APP d e c
SEQUENCE 23
FOR_NULLARY_FUNCTION BOT c
FOR_NULLARY_FUNCTION TOP d
IF_BINARY_RELATION NLESS d a
FOR_NULLARY_FUNCTION BOOOL e
FOR_BINARY_FUNCTION_LHS_VAL APP e f a
INFER_BINARY_FUNCTION APP e f c
SEQUENCE 48
FOR_NULLARY_FUNCTION K c
SEQUENCE 20
FOR_NULLARY_FUNCTION TOP d
IF_BINARY_RELATION NLESS d a
FOR_NULLARY_FUNCTION BOOOL e
FOR_BINARY_FUNCTION_LHS_VAL APP e f a
INFER_BINARY_FUNCTION APP e f c
IF_BINARY_RELATION NLESS c a
SEQUENCE 16
FOR_NULLARY_FUNCTION BOT d
FOR_NULLARY_FUNCTION BOOOL e
FOR_BINARY_FUNCTION_LHS_VAL APP e f a
INFER_BINARY_FUNCTION APP e f d
FOR_NULLARY_FUNCTION TOP d
FOR_NULLARY_FUNCTION BOOOL e
FOR_BINARY_FUNCTION_LHS_VAL APP e f a
INFER_BINARY_FUNCTION APP e f d
PADDING
FOR_NULLARY_FUNCTION F c
SEQUENCE 20
FOR_NULLARY_FUNCTION K d
IF_BINARY_RELATION NLESS d a
FOR_NULLARY_FUNCTION BOOOL e
FOR_BINARY_FUNCTION_LHS_VAL APP e f a
INFER_BINARY_FUNCTION APP e f c
SEQUENCE 20
FOR_NULLARY_FUNCTION TOP d
IF_BINARY_RELATION NLESS d a
FOR_NULLARY_FUNCTION BOOOL e
FOR_BINARY_FUNCTION_LHS_VAL APP e f a
INFER_BINARY_FUNCTION APP e f c
IF_BINARY_RELATION NLESS c a
SEQUENCE 16
FOR_NULLARY_FUNCTION TOP d
FOR_NULLARY_FUNCTION BOOOL e
FOR_BINARY_FUNCTION_LHS_VAL APP e f a
INFER_BINARY_FUNCTION APP e f d
SEQUENCE 16
FOR_NULLARY_FUNCTION BOT d
FOR_NULLARY_FUNCTION BOOOL e
FOR_BINARY_FUNCTION_LHS_VAL APP e f a
INFER_BINARY_FUNCTION APP e f d
FOR_NULLARY_FUNCTION K d
SEQUENCE 13
FOR_NULLARY_FUNCTION BOOOL e
FOR_BINARY_FUNCTION_LHS_VAL APP e f a
INFER_BINARY_FUNCTION APP e f d
IF_BINARY_RELATION NLESS d a
SEQUENCE 16
FOR_NULLARY_FUNCTION BOT e
FOR_NULLARY_FUNCTION BOOOL f
FOR_BINARY_FUNCTION_LHS_VAL APP f g a
INFER_BINARY_FUNCTION APP f g e
FOR_NULLARY_FUNCTION TOP e
FOR_NULLARY_FUNCTION BOOOL f
FOR_BINARY_FUNCTION_LHS_VAL APP f g a
INFER_BINARY_FUNCTION APP f g e
PADDING
SEQUENCE 60
IF_NULLARY_FUNCTION J a
FOR_NULLARY_FUNCTION F c
SEQUENCE 20
FOR_NULLARY_FUNCTION K d
IF_BINARY_RELATION NLESS b d
FOR_NULLARY_FUNCTION BOOOL e
FOR_BINARY_FUNCTION_LHS_VAL APP e f b
INFER_BINARY_FUNCTION APP e f c
IF_BINARY_RELATION NLESS b c
FOR_NULLARY_FUNCTION K d
SEQUENCE 13
FOR_NULLARY_FUNCTION BOOOL e
FOR_BINARY_FUNCTION_LHS_VAL APP e f b
INFER_BINARY_FUNCTION APP e f d
IF_BINARY_RELATION NLESS b d
SEQUENCE 16
FOR_NULLARY_FUNCTION BOT e
FOR_NULLARY_FUNCTION BOOOL f
FOR_BINARY_FUNCTION_LHS_VAL APP f g b
INFER_BINARY_FUNCTION APP f g e
FOR_NULLARY_FUNCTION TOP e
FOR_NULLARY_FUNCTION BOOOL f
FOR_BINARY_FUNCTION_LHS_VAL APP f g b
INFER_BINARY_FUNCTION APP f g e
SEQUENCE 46
IF_NULLARY_FUNCTION I b
SEQUENCE 23
FOR_NULLARY_FUNCTION BOT c
FOR_NULLARY_FUNCTION TOP d
IF_BINARY_RELATION NLESS d a
FOR_NULLARY_FUNCTION SEMI e
FOR_BINARY_FUNCTION_LHS_VAL APP e f a
INFER_BINARY_FUNCTION APP e f c
FOR_NULLARY_FUNCTION TOP c
SEQUENCE 13
FOR_NULLARY_FUNCTION SEMI d
FOR_BINARY_FUNCTION_LHS_VAL APP d e a
INFER_BINARY_FUNCTION APP d e c
FOR_NULLARY_FUNCTION UNIT d
FOR_BINARY_FUNCTION_LHS_VAL APP d e a
INFER_BINARY_FUNCTION APP d e c
PADDING
SEQUENCE 46
IF_NULLARY_FUNCTION I a
SEQUENCE 16
FOR_NULLARY_FUNCTION TOP c
FOR_NULLARY_FUNCTION UNIT d
FOR_BINARY_FUNCTION_LHS_VAL APP d e b
INFER_BINARY_FUNCTION APP d e c
FOR_NULLARY_FUNCTION BOT c
SEQUENCE 13
FOR_NULLARY_FUNCTION SEMI d
FOR_BINARY_FUNCTION_LHS_VAL APP d e b
INFER_BINARY_FUNCTION APP d e c
IF_BINARY_RELATION NLESS b c
FOR_NULLARY_FUNCTION TOP d
FOR_NULLARY_FUNCTION SEMI e
FOR_BINARY_FUNCTION_LHS_VAL APP e f b
INFER_BINARY_FUNCTION APP e f d
PADDING
SEQUENCE 101
IF_NULLARY_FUNCTION F b
SEQUENCE 68
FOR_NULLARY_FUNCTION J c
SEQUENCE 39
FOR_NULLARY_FUNCTION K d
SEQUENCE 17
IF_BINARY_RELATION NLESS d a
FOR_NULLARY_FUNCTION BOOOL e
FOR_BINARY_FUNCTION_LHS_VAL APP e f a
INFER_BINARY_FUNCTION APP e f c
IF_BINARY_RELATION NLESS a d
FOR_NULLARY_FUNCTION TOP e
IF_BINARY_RELATION NLESS e a
FOR_NULLARY_FUNCTION BOOOL f
FOR_BINARY_FUNCTION_LHS_VAL APP f g a
INFER_BINARY_FUNCTION APP f g c
IF_BINARY_RELATION NLESS c a
FOR_NULLARY_FUNCTION K d
SEQUENCE 13
FOR_NULLARY_FUNCTION BOOOL e
FOR_BINARY_FUNCTION_LHS_VAL APP e f a
INFER_BINARY_FUNCTION APP e f d
IF_BINARY_RELATION NLESS a d
SEQUENCE 16
FOR_NULLARY_FUNCTION BOT e
FOR_NULLARY_FUNCTION BOOOL f
FOR_BINARY_FUNCTION_LHS_VAL APP f g a
INFER_BINARY_FUNCTION APP f g e
FOR_NULLARY_FUNCTION TOP e
FOR_NULLARY_FUNCTION BOOOL f
FOR_BINARY_FUNCTION_LHS_VAL APP f g a
INFER_BINARY_FUNCTION APP f g e
PADDING
FOR_NULLARY_FUNCTION K c
SEQUENCE 20
FOR_NULLARY_FUNCTION TOP d
IF_BINARY_RELATION NLESS d a
FOR_NULLARY_FUNCTION BOOL e
FOR_BINARY_FUNCTION_LHS_VAL APP e f a
INFER_BINARY_FUNCTION APP e f c
SEQUENCE 39
IF_BINARY_RELATION NLESS a c
SEQUENCE 16
FOR_NULLARY_FUNCTION TOP d
FOR_NULLARY_FUNCTION BOOL e
FOR_BINARY_FUNCTION_LHS_VAL APP e f a
INFER_BINARY_FUNCTION APP e f d
FOR_NULLARY_FUNCTION BOT d
FOR_NULLARY_FUNCTION TOP e
IF_BINARY_RELATION NLESS e a
FOR_NULLARY_FUNCTION BOOL f
FOR_BINARY_FUNCTION_LHS_VAL APP f g a
INFER_BINARY_FUNCTION APP f g d
PADDING
IF_BINARY_RELATION NLESS c a
SEQUENCE 31
FOR_NULLARY_FUNCTION BOT d
SEQUENCE 13
FOR_NULLARY_FUNCTION BOOL e
FOR_BINARY_FUNCTION_LHS_VAL APP e f a
INFER_BINARY_FUNCTION APP e f d
FOR_NULLARY_FUNCTION BOOOL e
FOR_BINARY_FUNCTION_LHS_VAL APP e f a
INFER_BINARY_FUNCTION APP e f d
FOR_NULLARY_FUNCTION TOP d
SEQUENCE 13
FOR_NULLARY_FUNCTION BOOL e
FOR_BINARY_FUNCTION_LHS_VAL APP e f a
INFER_BINARY_FUNCTION APP e f d
FOR_NULLARY_FUNCTION BOOOL e
FOR_BINARY_FUNCTION_LHS_VAL APP e f a
INFER_BINARY_FUNCTION APP e f d
PADDING
PADDING
PADDING
PADDING
PADDING
PADDING
SEQUENCE 110
IF_NULLARY_FUNCTION F a
SEQUENCE 77
FOR_NULLARY_FUNCTION J c
SEQUENCE 39
FOR_NULLARY_FUNCTION K d
SEQUENCE 17
IF_BINARY_RELATION NLESS b d
FOR_NULLARY_FUNCTION BOOOL e
FOR_BINARY_FUNCTION_LHS_VAL APP e f b
INFER_BINARY_FUNCTION APP e f c
IF_BINARY_RELATION NLESS d b
FOR_NULLARY_FUNCTION BOT e
IF_BINARY_RELATION NLESS b e
FOR_NULLARY_FUNCTION BOOOL f
FOR_BINARY_FUNCTION_LHS_VAL APP f g b
INFER_BINARY_FUNCTION APP f g c
IF_BINARY_RELATION NLESS b c
SEQUENCE 16
FOR_NULLARY_FUNCTION TOP d
FOR_NULLARY_FUNCTION BOOOL e
FOR_BINARY_FUNCTION_LHS_VAL APP e f b
INFER_BINARY_FUNCTION APP e f d
SEQUENCE 16
FOR_NULLARY_FUNCTION BOT d
FOR_NULLARY_FUNCTION BOOOL e
FOR_BINARY_FUNCTION_LHS_VAL APP e f b
INFER_BINARY_FUNCTION APP e f d
FOR_NULLARY_FUNCTION K d
SEQUENCE 13
FOR_NULLARY_FUNCTION BOOOL e
FOR_BINARY_FUNCTION_LHS_VAL APP e f b
INFER_BINARY_FUNCTION APP e f d
IF_BINARY_RELATION NLESS d b
SEQUENCE 16
FOR_NULLARY_FUNCTION BOT e
FOR_NULLARY_FUNCTION BOOOL f
FOR_BINARY_FUNCTION_LHS_VAL APP f g b
INFER_BINARY_FUNCTION APP f g e
FOR_NULLARY_FUNCTION TOP e
FOR_NULLARY_FUNCTION BOOOL f
FOR_BINARY_FUNCTION_LHS_VAL APP f g b
INFER_BINARY_FUNCTION APP f g e
PADDING
FOR_NULLARY_FUNCTION K c
SEQUENCE 34
FOR_NULLARY_FUNCTION BOT d
IF_BINARY_RELATION NLESS b d
SEQUENCE 13
FOR_NULLARY_FUNCTION BOOL e
FOR_BINARY_FUNCTION_LHS_VAL APP e f b
INFER_BINARY_FUNCTION APP e f c
FOR_NULLARY_FUNCTION BOOOL e
FOR_BINARY_FUNCTION_LHS_VAL APP e f b
INFER_BINARY_FUNCTION APP e f c
PADDING
SEQUENCE 50
IF_BINARY_RELATION NLESS b c
SEQUENCE 31
FOR_NULLARY_FUNCTION BOT d
SEQUENCE 13
FOR_NULLARY_FUNCTION BOOL e
FOR_BINARY_FUNCTION_LHS_VAL APP e f b
INFER_BINARY_FUNCTION APP e f d
FOR_NULLARY_FUNCTION BOOOL e
FOR_BINARY_FUNCTION_LHS_VAL APP e f b
INFER_BINARY_FUNCTION APP e f d
FOR_NULLARY_FUNCTION TOP d
SEQUENCE 13
FOR_NULLARY_FUNCTION BOOL e
FOR_BINARY_FUNCTION_LHS_VAL APP e f b
INFER_BINARY_FUNCTION APP e f d
FOR_NULLARY_FUNCTION BOOOL e
FOR_BINARY_FUNCTION_LHS_VAL APP e f b
INFER_BINARY_FUNCTION APP e f d
IF_BINARY_RELATION NLESS c b
FOR_NULLARY_FUNCTION BOT d
SEQUENCE 13
FOR_NULLARY_FUNCTION BOOL e
FOR_BINARY_FUNCTION_LHS_VAL APP e f b
INFER_BINARY_FUNCTION APP e f d
SEQUENCE 13
FOR_NULLARY_FUNCTION BOOOL e
FOR_BINARY_FUNCTION_LHS_VAL APP e f b
INFER_BINARY_FUNCTION APP e f d
IF_BINARY_RELATION NLESS b d
FOR_NULLARY_FUNCTION TOP e
SEQUENCE 13
FOR_NULLARY_FUNCTION BOOL f
FOR_BINARY_FUNCTION_LHS_VAL APP f g b
INFER_BINARY_FUNCTION APP f g e
FOR_NULLARY_FUNCTION BOOOL f
FOR_BINARY_FUNCTION_LHS_VAL APP f g b
INFER_BINARY_FUNCTION APP f g e
SEQUENCE 92
IF_NULLARY_FUNCTION BOT b
SEQUENCE 16
FOR_NULLARY_FUNCTION DIV c
FOR_NULLARY_FUNCTION TOP d
FOR_BINARY_FUNCTION_LHS_VAL APP c e a
INFER_BINARY_FUNCTION APP c e d
SEQUENCE 39
FOR_NULLARY_FUNCTION I c
SEQUENCE 20
FOR_NULLARY_FUNCTION TOP d
IF_BINARY_RELATION NLESS d a
FOR_NULLARY_FUNCTION SEMI e
FOR_BINARY_FUNCTION_LHS_VAL APP e f a
INFER_BINARY_FUNCTION APP e f c
IF_BINARY_RELATION NLESS c a
FOR_NULLARY_FUNCTION TOP d
FOR_NULLARY_FUNCTION SEMI e
FOR_BINARY_FUNCTION_LHS_VAL APP e f a
INFER_BINARY_FUNCTION APP e f d
PADDING
FOR_NULLARY_FUNCTION F c
SEQUENCE 34
FOR_NULLARY_FUNCTION K d
IF_BINARY_RELATION NLESS d a
SEQUENCE 13
FOR_NULLARY_FUNCTION BOOL e
FOR_BINARY_FUNCTION_LHS_VAL APP e f a
INFER_BINARY_FUNCTION APP e f c
FOR_NULLARY_FUNCTION BOOOL e
FOR_BINARY_FUNCTION_LHS_VAL APP e f a
INFER_BINARY_FUNCTION APP e f c
PADDING
IF_BINARY_RELATION NLESS c a
SEQUENCE 23
FOR_NULLARY_FUNCTION J d
FOR_NULLARY_FUNCTION K e
IF_BINARY_RELATION NLESS e a
FOR_NULLARY_FUNCTION BOOOL f
FOR_BINARY_FUNCTION_LHS_VAL APP f g a
INFER_BINARY_FUNCTION APP f g d
FOR_NULLARY_FUNCTION K d
SEQUENCE 13
FOR_NULLARY_FUNCTION BOOL e
FOR_BINARY_FUNCTION_LHS_VAL APP e f a
INFER_BINARY_FUNCTION APP e f d
SEQUENCE 13
FOR_NULLARY_FUNCTION BOOOL e
FOR_BINARY_FUNCTION_LHS_VAL APP e f a
INFER_BINARY_FUNCTION APP e f d
IF_BINARY_RELATION NLESS d a
FOR_NULLARY_FUNCTION TOP e
SEQUENCE 13
FOR_NULLARY_FUNCTION BOOL f
FOR_BINARY_FUNCTION_LHS_VAL APP f g a
INFER_BINARY_FUNCTION APP f g e
FOR_NULLARY_FUNCTION BOOOL f
FOR_BINARY_FUNCTION_LHS_VAL APP f g a
INFER_BINARY_FUNCTION APP f g e
PADDING
SEQUENCE 33
IF_NULLARY_FUNCTION A b
FOR_NULLARY_FUNCTION I c
FOR_NULLARY_FUNCTION CI d
FOR_BINARY_FUNCTION_LHS APP d e f
FOR_BINARY_FUNCTION_LHS_VAL COMP f g a
FOR_BINARY_FUNCTION_LHS_VAL APP d h g
FOR_BINARY_FUNCTION_LHS_RHS COMP e h i
INFER_BINARY_RELATION NLESS i c
PADDING
SEQUENCE 33
FOR_SYMMETRIC_FUNCTION_VAL JOIN c d a
SEQUENCE 8
IF_BINARY_RELATION LESS d b
INFER_BINARY_RELATION NLESS c b
SEQUENCE 8
IF_BINARY_RELATION LESS c b
INFER_BINARY_RELATION NLESS d b
FOR_SYMMETRIC_FUNCTION_LHS_VAL JOIN c e b
INFER_BINARY_RELATION NLESS d e
SEQUENCE 9
FOR_SYMMETRIC_FUNCTION_LHS_VAL JOIN b c a
INFER_BINARY_RELATION NLESS c b
SEQUENCE 9
FOR_SYMMETRIC_FUNCTION_LHS_VAL JOIN a c b
INFER_BINARY_RELATION NLESS c a
SEQUENCE 17
FOR_NULLARY_FUNCTION Y c
FOR_BINARY_FUNCTION_LHS_VAL APP c d a
FOR_BINARY_FUNCTION_LHS_RHS APP d b e
INFER_BINARY_RELATION NLESS e b
SEQUENCE 25
FOR_BINARY_FUNCTION_VAL APP c d a
SEQUENCE 9
FOR_BINARY_FUNCTION_LHS_VAL APP c e b
INFER_BINARY_RELATION NLESS d e
FOR_BINARY_FUNCTION_RHS_VAL APP e d b
INFER_BINARY_RELATION NLESS c e
SEQUENCE 25
FOR_BINARY_FUNCTION_VAL COMP c d a
SEQUENCE 9
FOR_BINARY_FUNCTION_LHS_VAL COMP c e b
INFER_BINARY_RELATION NLESS d e
FOR_BINARY_FUNCTION_RHS_VAL COMP e d b
INFER_BINARY_RELATION NLESS c e
SEQUENCE 38
FOR_NULLARY_FUNCTION V c
SEQUENCE 19
FOR_BINARY_FUNCTION_RHS_VAL APP d a b
FOR_BINARY_FUNCTION_LHS_VAL APP c e d
FOR_BINARY_FUNCTION_LHS_RHS APP e a f
INFER_BINARY_RELATION NLESS f a
FOR_BINARY_FUNCTION_RHS_VAL APP d b a
FOR_BINARY_FUNCTION_LHS_VAL APP c e d
FOR_BINARY_FUNCTION_LHS_RHS APP e b f
INFER_BINARY_RELATION NLESS f b
PADDING
SEQUENCE 47
FOR_NULLARY_FUNCTION BOT c
FOR_NULLARY_FUNCTION DIV d
FOR_NULLARY_FUNCTION TOP e
FOR_BINARY_FUNCTION_RHS_VAL COMP f d a
FOR_BINARY_FUNCTION_LHS_RHS APP f c g
FOR_BINARY_FUNCTION_LHS_RHS APP f e h
FOR_BINARY_FUNCTION_RHS_VAL COMP i d b
FOR_BINARY_FUNCTION_LHS_RHS APP i c j
SEQUENCE 13
FOR_BINARY_FUNCTION_LHS_RHS APP i e k
IF_BINARY_RELATION LESS h k
INFER_BINARY_RELATION NLESS g j
IF_BINARY_RELATION LESS g j
FOR_BINARY_FUNCTION_LHS_RHS APP i e k
INFER_BINARY_RELATION NLESS h k
SEQUENCE 54
FOR_NULLARY_FUNCTION U c
SEQUENCE 14
IF_BINARY_FUNCTION APP c b a
FOR_BINARY_FUNCTION_LHS_RHS COMP b b d
INFER_BINARY_RELATION NLESS d b
SEQUENCE 14
IF_BINARY_FUNCTION APP c a b
FOR_BINARY_FUNCTION_LHS_RHS COMP a a d
INFER_BINARY_RELATION NLESS d a
SEQUENCE 19
FOR_BINARY_FUNCTION_VAL APP d e a
FOR_BINARY_FUNCTION_LHS_RHS APP c d f
IF_BINARY_FUNCTION APP f e b
INFER_BINARY_RELATION NLESS a e
FOR_BINARY_FUNCTION_VAL APP d e b
FOR_BINARY_FUNCTION_LHS_RHS APP c d f
IF_BINARY_FUNCTION APP f e a
INFER_BINARY_RELATION NLESS b e
PADDING
SEQUENCE 106
FOR_NULLARY_FUNCTION I c
SEQUENCE 34
IF_BINARY_RELATION LESS c b
FOR_NULLARY_FUNCTION V d
IF_BINARY_FUNCTION APP d b a
FOR_BINARY_FUNCTION_LHS_RHS COMP b b e
SEQUENCE 8
IF_BINARY_RELATION LESS b e
INFER_BINARY_RELATION NLESS e b
IF_BINARY_RELATION LESS e b
INFER_BINARY_RELATION NLESS b e
PADDING
SEQUENCE 37
IF_BINARY_RELATION LESS c a
FOR_NULLARY_FUNCTION V d
IF_BINARY_FUNCTION APP d a b
FOR_BINARY_FUNCTION_LHS_RHS COMP a a e
SEQUENCE 4
INFER_BINARY_RELATION NLESS e a
SEQUENCE 8
IF_BINARY_RELATION LESS a e
INFER_BINARY_RELATION NLESS e a
IF_BINARY_RELATION LESS e a
INFER_BINARY_RELATION NLESS a e
PADDING
SEQUENCE 41
FOR_NULLARY_FUNCTION V d
SEQUENCE 17
IF_BINARY_FUNCTION APP d b a
FOR_BINARY_FUNCTION_LHS_RHS COMP b b e
IF_EQUAL e b
INFER_BINARY_RELATION NLESS c b
IF_BINARY_FUNCTION APP d a b
FOR_BINARY_FUNCTION_LHS_RHS COMP a a e
SEQUENCE 7
IF_EQUAL e a
INFER_BINARY_RELATION NLESS c a
IF_BINARY_RELATION LESS e a
INFER_BINARY_RELATION NLESS c a
PADDING
SEQUENCE 46
FOR_NULLARY_FUNCTION TOP d
FOR_NULLARY_FUNCTION UNIT e
FOR_BINARY_FUNCTION_RHS_VAL COMP f e a
FOR_BINARY_FUNCTION_LHS_RHS APP f c g
FOR_BINARY_FUNCTION_LHS_RHS APP f d h
FOR_BINARY_FUNCTION_RHS_VAL COMP i e b
FOR_BINARY_FUNCTION_LHS_RHS APP i c j
SEQUENCE 13
FOR_BINARY_FUNCTION_LHS_RHS APP i d k
IF_BINARY_RELATION LESS h k
INFER_BINARY_RELATION NLESS g j
IF_BINARY_RELATION LESS g j
FOR_BINARY_FUNCTION_LHS_RHS APP i d k
INFER_BINARY_RELATION NLESS h k
PADDING
FOR_NULLARY_FUNCTION BOT d
FOR_NULLARY_FUNCTION TOP e
FOR_NULLARY_FUNCTION SEMI f
FOR_BINARY_FUNCTION_RHS_VAL COMP g f a
FOR_BINARY_FUNCTION_LHS_RHS APP g c h
FOR_BINARY_FUNCTION_LHS_RHS APP g d i
FOR_BINARY_FUNCTION_LHS_RHS APP g e j
FOR_BINARY_FUNCTION_RHS_VAL COMP k f b
FOR_BINARY_FUNCTION_LHS_RHS APP k c l
SEQUENCE 22
FOR_BINARY_FUNCTION_LHS_RHS APP k d m
IF_BINARY_RELATION LESS i m
FOR_BINARY_FUNCTION_LHS_RHS APP k e n
IF_BINARY_RELATION LESS j n
INFER_BINARY_RELATION NLESS h l
IF_BINARY_RELATION LESS h l
FOR_BINARY_FUNCTION_LHS_RHS APP k d m
SEQUENCE 13
FOR_BINARY_FUNCTION_LHS_RHS APP k e n
IF_BINARY_RELATION LESS j n
INFER_BINARY_RELATION NLESS i m
IF_BINARY_RELATION LESS i m
FOR_BINARY_FUNCTION_LHS_RHS APP k e n
INFER_BINARY_RELATION NLESS j n
PADDING
PADDING
PADDING
PADDING
PADDING
FOR_NULLARY_FUNCTION F c
SEQUENCE 78
FOR_NULLARY_FUNCTION K d
FOR_NULLARY_FUNCTION BOT e
FOR_NULLARY_FUNCTION TOP f
FOR_NULLARY_FUNCTION BOOL g
FOR_BINARY_FUNCTION_RHS_VAL COMP h g a
FOR_BINARY_FUNCTION_LHS_RHS APP h c i
FOR_BINARY_FUNCTION_LHS_RHS APP h d j
FOR_BINARY_FUNCTION_LHS_RHS APP h e k
FOR_BINARY_FUNCTION_LHS_RHS APP h f l
FOR_BINARY_FUNCTION_RHS_VAL COMP m g b
FOR_BINARY_FUNCTION_LHS_RHS APP m c n
SEQUENCE 31
FOR_BINARY_FUNCTION_LHS_RHS APP m d o
IF_BINARY_RELATION LESS j o
FOR_BINARY_FUNCTION_LHS_RHS APP m e p
IF_BINARY_RELATION LESS k p
FOR_BINARY_FUNCTION_LHS_RHS APP m f q
IF_BINARY_RELATION LESS l q
INFER_BINARY_RELATION NLESS i n
IF_BINARY_RELATION LESS i n
FOR_BINARY_FUNCTION_LHS_RHS APP m d o
SEQUENCE 22
FOR_BINARY_FUNCTION_LHS_RHS APP m e p
IF_BINARY_RELATION LESS k p
FOR_BINARY_FUNCTION_LHS_RHS APP m f q
IF_BINARY_RELATION LESS l q
INFER_BINARY_RELATION NLESS j o
IF_BINARY_RELATION LESS j o
FOR_BINARY_FUNCTION_LHS_RHS APP m e p
SEQUENCE 13
FOR_BINARY_FUNCTION_LHS_RHS APP m f q
IF_BINARY_RELATION LESS l q
INFER_BINARY_RELATION NLESS k p
IF_BINARY_RELATION LESS k p
FOR_BINARY_FUNCTION_LHS_RHS APP m f q
INFER_BINARY_RELATION NLESS l q
PADDING
PADDING
FOR_NULLARY_FUNCTION J d
FOR_NULLARY_FUNCTION K e
FOR_NULLARY_FUNCTION BOT f
FOR_NULLARY_FUNCTION TOP g
FOR_NULLARY_FUNCTION BOOOL h
FOR_BINARY_FUNCTION_RHS_VAL COMP i h a
FOR_BINARY_FUNCTION_LHS_RHS APP i c j
FOR_BINARY_FUNCTION_LHS_RHS APP i d k
FOR_BINARY_FUNCTION_LHS_RHS APP i e l
FOR_BINARY_FUNCTION_LHS_RHS APP i f m
FOR_BINARY_FUNCTION_LHS_RHS APP i g n
FOR_BINARY_FUNCTION_RHS_VAL COMP o h b
FOR_BINARY_FUNCTION_LHS_RHS APP o c p
SEQUENCE 36
FOR_BINARY_FUNCTION_LHS_RHS APP o d q
IF_BINARY_RELATION LESS k q
FOR_BINARY_FUNCTION_LHS_RHS APP o e r
IF_BINARY_RELATION LESS l r
FOR_BINARY_FUNCTION_LHS_RHS APP o f s
IF_BINARY_RELATION LESS m s
FOR_BINARY_FUNCTION_LHS_RHS APP o g t
IF_BINARY_RELATION LESS n t
INFER_BINARY_RELATION NLESS j p
IF_BINARY_RELATION LESS j p
FOR_BINARY_FUNCTION_LHS_RHS APP o d q
SEQUENCE 31
FOR_BINARY_FUNCTION_LHS_RHS APP o e r
IF_BINARY_RELATION LESS l r
FOR_BINARY_FUNCTION_LHS_RHS APP o f s
IF_BINARY_RELATION LESS m s
FOR_BINARY_FUNCTION_LHS_RHS APP o g t
IF_BINARY_RELATION LESS n t
INFER_BINARY_RELATION NLESS k q
IF_BINARY_RELATION LESS k q
FOR_BINARY_FUNCTION_LHS_RHS APP o e r
SEQUENCE 22
FOR_BINARY_FUNCTION_LHS_RHS APP o f s
IF_BINARY_RELATION LESS m s
FOR_BINARY_FUNCTION_LHS_RHS APP o g t
IF_BINARY_RELATION LESS n t
INFER_BINARY_RELATION NLESS l r
IF_BINARY_RELATION LESS l r
FOR_BINARY_FUNCTION_LHS_RHS APP o f s
SEQUENCE 13
FOR_BINARY_FUNCTION_LHS_RHS APP o g t
IF_BINARY_RELATION LESS n t
INFER_BINARY_RELATION NLESS m s
IF_BINARY_RELATION LESS m s
FOR_BINARY_FUNCTION_LHS_RHS APP o g t
INFER_BINARY_RELATION NLESS n t

# line 1146, plan 46: 28 bytes
FOR_BLOCK
FOR_NULLARY_FUNCTION C a
FOR_BINARY_FUNCTION_LHS APP a b c
IF_BLOCK b
FOR_BINARY_FUNCTION_LHS APP c d e
FOR_BINARY_FUNCTION_LHS APP b f g
INFER_BINARY_BINARY APP e f APP g d

# line 860, plan 18: 35 bytes
FOR_BLOCK
FOR_ALL a
IF_BLOCK a
FOR_BINARY_FUNCTION_LHS APP a b c
LETS_BINARY_FUNCTION_LHS APP a d
LETS_BINARY_RELATION_LHS NLESS b e
FOR_POS_NEG f d e
LET_BINARY_FUNCTION APP a f d
IF_BINARY_RELATION NLESS c d
INFER_BINARY_RELATION NLESS b f

# line 922, plan 24: 35 bytes
FOR_BLOCK
FOR_ALL a
IF_BLOCK a
FOR_BINARY_FUNCTION_LHS COMP a b c
LETS_BINARY_FUNCTION_LHS COMP a d
LETS_BINARY_RELATION_LHS NLESS b e
FOR_POS_NEG f d e
LET_BINARY_FUNCTION COMP a f d
IF_BINARY_RELATION NLESS c d
INFER_BINARY_RELATION NLESS b f

# line 1211, plan 54: 50 bytes
FOR_BLOCK
FOR_NULLARY_FUNCTION P a
FOR_BINARY_FUNCTION_LHS APP a b c
IF_BLOCK b
LETS_BINARY_FUNCTION_LHS APP a d
LETS_BINARY_FUNCTION_LHS APP c e
FOR_POS_POS f d e
LET_BINARY_FUNCTION APP a f d
LET_BINARY_FUNCTION APP c f e
FOR_BINARY_FUNCTION_LHS_RHS APP a e g
FOR_BINARY_FUNCTION_LHS APP d h i
INFER_BINARY_BINARY APP c i APP g h
fritzo commented 9 years ago

After implementing an inference deadline, cleanup exits early and NLESS tasks now take up most of the time:

2015:06:28:03:32
...
20367   326.516     INFO    starting 16 deadlined threads
20367   326.516     INFO    Setting deadline of 18000 sec
20367   18002.6     INFO    Deadline reached
20367   18612.6     INFO    finished 16 deadlined threads
20367   18612.6     INFO    merge tasks: 6 executed / 6 scheduled
20367   18612.6     INFO    enforce tasks: 18101402 executed / 18100186 scheduled
20367   18612.6     INFO    sample tasks: 523 executed / 0 scheduled
20367   18612.6     INFO    cleanup tasks: 18798 executed / 0 scheduled
20367   18612.6     INFO    Profile of VirtualMachine programs:
20367   18612.6     INFO     Line       Calls Percent   Total sec Per call sec
20367   18612.6     INFO    ----- ----------- ------- ----------- ------------
20367   18612.6     INFO     4837    17980658   59.07   126658.86      0.01
20367   18612.6     INFO      906         528   10.25    21988.15     41.64
20367   18612.6     INFO      914         528    7.77    16666.36     31.57
20367   18612.6     INFO     1146         282    6.81    14600.46     51.77
20367   18612.6     INFO      860         528    3.25     6977.70     13.22
20367   18612.6     INFO      922         528    2.00     4295.02      8.13
...
fritzo commented 7 years ago

Information moved into /doc/benchmarks.md.