search

OCamlPro / alt-ergo

OCamlPro public development repository for Alt-Ergo
https://alt-ergo.ocamlpro.com/
Other
130 stars 33 forks source link

Merge `Enum` theory into `ADT` theory #1094

Closed Halbaroth closed 2 months ago

Halbaroth commented 4 months ago

After refactoring both Enum and ADT theories, they shared most of their implementation.

This PR merges Enum theory into ADT ones.

This PR is rebased on #1093

Halbaroth commented 2 months ago

This PR have been tested on our internal benchmarks.

Halbaroth commented 2 months ago

What are the results of those tests? Is it +0-0?

It's +0-0 on ae-format, QF_DT and UFDT. In fact, the enum theory is slightly faster after this PR.

Halbaroth commented 2 months ago

As far as the code goes, this looks mostly OK to me. Outside of some small suggestions, my main concern is the new boolean flag in the Tadt constructor. I know you did some things to try to get rid of it — can you say a bit more about what other approaches you tried and the issues with them? I want to make sure we don't miss an easy way of not needing this flag.

I only tried one other approach, which is currently in the draft #1138. See the diff between these branches: https://github.com/Halbaroth/alt-ergo/compare/merge-enum...Halbaroth:alt-ergo:casesplit-enum-cstr

Instead of splitting on enum types only after each assert, I split on domains that contains a constructor without payload. I got 4 regressions (with OCaml 5) and 0 improvements and the enum theory is slower (14m30s before and 15m28s). These tests have been run on next and PR #1138 with only the UFDT test suite.

Halbaroth commented 2 months ago

I will test your suggestion in another PR. I think we can merge this one. I removed the extra flag as you wish.

Halbaroth commented 2 months ago

There is no regression. I forgot to rebase the PR after merging the fix for #1099. I ran again benchmarks on #1138 with the fix and there is no regression anymore.

bclement-ocp commented 2 months ago

I forgot to rebase the PR after merging the fix for https://github.com/OCamlPro/alt-ergo/issues/1099.

Does this mean that it is that fix that introduced regressions?

Halbaroth commented 2 months ago

I forgot to rebase the PR after merging the fix for #1099.

Does this mean that it is that fix that introduced regressions?

No. The fix solved regressions introduced with the Dolmen frontend in 2.5.0 and I didn't rebase this PR with it. So next solved new problems.

bclement-ocp commented 2 months ago

Ah, I got things backwards — thanks for the clarification.