Extended internal Time Profiling

[joe-hauns]

Added the option -tstat_focus which displays the time trace for some subnode in the time trace tree specified as agrument. This is helpful if you want to see only the time trace of some function you are currently optimizing, and want to skip the time trace all the other functions. Also all calls in the time trace tree to this function will be merged instead of potentially having multiple disjoint subtrees with calls with this node, which also helps for getting a good understanding of the time profile of your function.

[joe-hauns]

An example:

With -tstat on we get

===== start of time trace =====
[root] (total: 85 ms, avg: 85 ms, cnt: 1)
  ├──[89%] main loop (total: 77 ms, avg: 77 ms, cnt: 1)
  │    ├──[99%] run (total: 76 ms, avg: 76 ms, cnt: 1)
  │    │    ├──[62%] activation (total: 47 ms, avg: 662 μs, cnt: 72)
  │    │    │    ├──[87%] clause generation (total: 41 ms, avg: 67 μs, cnt: 618)
  │    │    │    │    ├──[19%] superposition (total: 8385 μs, avg: 19 μs, cnt: 426)
  │    │    │    │    │    └──[71%] perform superposition (total: 5991 μs, avg: 51 μs, cnt: 117)
  │    │    │    │    │         └──[23%] term sharing (total: 1389 μs, avg: 6042 ns, cnt: 230)
  │    │    │    │    ├──[15%] polynomial evaluation (total: 6438 μs, avg: 55 μs, cnt: 115)
  │    │    │    │    │    └──[ 0%] term sharing (total: 5208 ns, avg: 2604 ns, cnt: 2)
  │    │    │    │    ├──[10%] resolution (total: 4375 μs, avg: 9002 ns, cnt: 486)
  │    │    │    │    │    └──[10%] term sharing (total: 479 μs, avg: 5267 ns, cnt: 91)
  │    │    │    │    └──[ 2%] term sharing (total: 913 μs, avg: 7190 ns, cnt: 127)
  │    │    │    ├──[ 4%] add clause (total: 2327 μs, avg: 32 μs, cnt: 72)
  │    │    │    │    ├──[64%] backward superposition index maintenance (total: 1505 μs, avg: 20 μs, cnt: 72)
  │    │    │    │    ├──[17%] binary resolution index maintenance (total: 409 μs, avg: 5687 ns, cnt: 72)
  │    │    │    │    │    └──[18%] term sharing (total: 75 μs, avg: 5381 ns, cnt: 14)
  │    │    │    │    └──[12%] forward superposition index maintenance (total: 296 μs, avg: 4116 ns, cnt: 72)
  │    │    │    ├──[ 1%] backward demodulation index maintenance (total: 822 μs, avg: 27 μs, cnt: 30)
  │    │    │    ├──[ 1%] backward superposition index maintenance (total: 675 μs, avg: 22 μs, cnt: 30)
  │    │    │    ├──[ 0%] codetree subsumption index maintanance (total: 273 μs, avg: 9131 ns, cnt: 30)
  │    │    │    ├──[ 0%] clause selection (total: 183 μs, avg: 2552 ns, cnt: 72)
  │    │    │    │    └──[87%] literal selection (total: 161 μs, avg: 2236 ns, cnt: 72)
  │    │    │    ├──[ 0%] forward demodulation index maintenance (total: 175 μs, avg: 8783 ns, cnt: 20)
  │    │    │    ├──[ 0%] binary resolution index maintenance (total: 134 μs, avg: 4486 ns, cnt: 30)
  │    │    │    ├──[ 0%] forward superposition index maintenance (total: 133 μs, avg: 4443 ns, cnt: 30)
  │    │    │    ├──[ 0%] splitting (total: 4747 ns, avg: 65 ns, cnt: 72)
  │    │    │    └──[ 0%] redundancy check (total: 3588 ns, avg: 49 ns, cnt: 72)
  │    │    ├──[21%] forward simplification (total: 16 ms, avg: 58 μs, cnt: 275)
  │    │    │    ├──[26%] forward demodulation (total: 4326 μs, avg: 21 μs, cnt: 203)
  │    │    │    │    └──[ 7%] term sharing (total: 344 μs, avg: 7021 ns, cnt: 49)
  │    │    │    ├──[ 7%] term sharing (total: 1182 μs, avg: 5824 ns, cnt: 203)
  │    │    │    ├──[ 0%] splitting component index usage (total: 68 μs, avg: 398 ns, cnt: 171)
  │    │    │    └──[ 0%] splitting component index maintenance (total: 20 μs, avg: 1476 ns, cnt: 14)
  ...

but we might want to optimize polynomial evaluation only which occurs multiple times. So we can run wiht -tstat on -tstat_focus "polynomial evaluation" to additionally get

===== start of focussed time profile =====
polynomial evaluation (total: 6373 μs, avg: 55 μs, cnt: 115)
 └──[ 0%] term sharing (total: 5334 ns, avg: 2667 ns, cnt: 2)
===== end of focussed time profile =====
===== start of flattened focussed time profile =====
polynomial evaluation (total: 6373 μs, avg:   55 μs, cnt:    115)
 └──[ 0%] term sharing (total: 5334 ns, avg: 2667 ns, cnt:      2)
===== end of flattened focussed time profile =====