runtimeverification / mx-semantics

7 stars 3 forks source link

Decision tree optimization #2 #265

Closed bbyalcinkaya closed 4 months ago

bbyalcinkaya commented 4 months ago

This PR aims to optimize the decision tree by adding <instrs> to the rules that operate on the <commands> cell.

Target Before
(compilation time / dt dir size)
After
llvm-mandos 2m27s / 474 MB 1m8s / 195 MB
llvm-kasmer 5m15s / 566 MB 1m32s / 231 MB
Baltoli commented 4 months ago

This cuts the compilation time down to 4:31 for the entire semantics on my machine, which as I said on Slack, wouldn't previously finish if left overnight!