Skip to content

Log and report egraph size for egg.#10

Merged
0x0f0f0f merged 6 commits intonmheim:mainfrom
gkronber:report-egraph-size
Feb 28, 2025
Merged

Log and report egraph size for egg.#10
0x0f0f0f merged 6 commits intonmheim:mainfrom
gkronber:report-egraph-size

Conversation

@gkronber
Copy link
Contributor

To better understand relative performance differences between egg and Metatheory it is useful to report the egraph size.

@gkronber
Copy link
Contributor Author

@nmheim @0x0f0f0f I think this is ready. Please let me know if there are changes required.

@0x0f0f0f
Copy link
Collaborator

Would it be possible to get the ratios between sizes in the new table, or remove the ration columns? @gkronber

@gkronber
Copy link
Contributor Author

I'll try to add the ratios

@gkronber
Copy link
Contributor Author

Ratios added. Current format:

|                                 | egg-sym | egg-cust | MT@641212a | MT@ale/3.0 | egg-sym/MT@641... | egg-cust/MT@64... | MT@ale/3.0/MT@... |
|:--------------------------------|:-------:|:--------:|:----------:|:----------:|:-----------------:|:-----------------:|:-----------------:|
| egraph_addexpr                  | 1.62 ms |          | 5.38 ms    | 5.05 ms    | 0.300             |                   | 0.937             |
| basic_maths_simpl2              | 12 ms   | 5.05 ms  | 27.5 ms    | 24.7 ms    | 0.438             | 0.183             | 0.898             |
| prop_logic_freges_theorem       | 2.56 ms | 1.61 ms  | 2.42 ms    | 2.31 ms    | 1.056             | 0.664             | 0.955             |
| calc_logic_demorgan             | 64.1 μs | 36.8 μs  | 80.2 μs    | 78.8 μs    | 0.799             | 0.458             | 0.983             |
| calc_logic_freges_theorem       | 23 ms   | 11.7 ms  | 44.3 ms    | 42.3 ms    | 0.518             | 0.263             | 0.953             |
| basic_maths_simpl1              | 5.77 ms | 2.9 ms   | 4.99 ms    | 4.6 ms     | 1.158             | 0.582             | 0.922             |
| egraph_constructor              | 0.13 μs |          | 0.1 μs     | 0.1 μs     | 1.301             |                   | 1.000             |
| prop_logic_prove1               | 38 ms   | 14.6 ms  | 44.7 ms    | 39 ms      | 0.851             | 0.327             | 0.873             |
| prop_logic_demorgan             | 89.9 μs | 49.7 μs  | 98.8 μs    | 97 μs      | 0.910             | 0.503             | 0.982             |
| while_superinterpreter_while_10 |         |          | 19.7 ms    | 18.8 ms    |                   |                   | 0.954             |
| prop_logic_rewrite              |         |          | 131 μs     | 116 μs     |                   |                   | 0.891             |
| time_to_load                    |         |          | 121 ms     | 111 ms     |                   |                   | 0.920             |

[ Info: Saving table at output.md
|                                 | egg-sym          | egg-cust         | MT@641212a       | MT@ale/3.0       | egg-sym/MT@641... | egg-cust/MT@64... | MT@ale/3.0/MT@... |
|:--------------------------------|:----------------:|:----------------:|:----------------:|:----------------:|:-----------------:|:-----------------:|:-----------------:|
| egraph_addexpr                  | 6762 6762 6762   |                  | 6663 6663 6663   | 6640 6640 6640   | 1.015 1.015       |                   | 0.997 0.997       |
| basic_maths_simpl2              | 440 2235 2836    | 440 2235 2839    | 7092 14530 15001 | 7092 14530 15001 | 0.062 0.154       | 0.062 0.154       | 1.000 1.000       |
| prop_logic_freges_theorem       | 316 1197 2315    | 316 1197 2322    | 297 899 1313     | 297 899 1313     | 1.064 1.331       | 1.064 1.331       | 1.000 1.000       |
| calc_logic_demorgan             | 16 33 35         | 16 33 35         | 15 30 32         | 15 30 32         | 1.067 1.100       | 1.067 1.100       | 1.000 1.000       |
| calc_logic_freges_theorem       | 1072 4289 17394  | 1072 4289 17280  | 1527 5402 18092  | 1527 5402 18092  | 0.702 0.794       | 0.702 0.794       | 1.000 1.000       |
| basic_maths_simpl1              | 368 1910 2543    | 368 1910 2567    | 528 1815 3042    | 528 1815 3042    | 0.697 1.052       | 0.697 1.052       | 1.000 1.000       |
| egraph_constructor              |                  |                  |                  |                  |                   |                   |                   |
| prop_logic_prove1               | 5510 17371 27976 | 4668 13644 18522 | 3061 9176 15637  | 3061 9176 15637  | 1.800 1.893       | 1.525 1.487       | 1.000 1.000       |
| prop_logic_demorgan             | 16 35 42         | 16 35 42         | 15 30 33         | 15 30 33         | 1.067 1.167       | 1.067 1.167       | 1.000 1.000       |
| while_superinterpreter_while_10 |                  |                  | 39 205 499       | 39 205 499       |                   |                   | 1.000 1.000       |
| prop_logic_rewrite              |                  |                  |                  |                  |                   |                   |                   |
| time_to_load                    |                  |                  |                  |                  |                   |                   |                   |

@0x0f0f0f 0x0f0f0f merged commit 20b3179 into nmheim:main Feb 28, 2025
1 check passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants