Adapting to MuHFL

[KenSakayori]

I extracted the fork of rethfl that is used inside the POPL artifact docker image and I pushed it as popl-artifact branch.

My goal is to port the changes made in this branch to the master branch. However, I'm not planning to just merge this branch for the following reasons.

1. There are some overlapping features/fixes that has been added/made independently such as the improvement of the --show-refinement.
2. Some modifications can be ignored. For example, I don't think we need to support PCSat.

(I will keep on updating this issue; the next thing I'll do is to make a list of things that needs to be ported)

[KenSakayori]

(WIP)

• https://github.com/hopv/rethfl/commit/a0cd21e34f911f0fe5c368232db11ac733e9c2f3 Ignore. The Command module seems useful, but is reverted in https://github.com/hopv/rethfl/commit/9c60b6b7fc0b6cf2d332e8e813911a6c1fe22480. The other benchmark stuff is not worth committing.
• https://github.com/hopv/rethfl/commit/d900c969bf45c28f7f52a546dbfa7e517a8bf898 Ignore as it is a merge commit.
• https://github.com/hopv/rethfl/commit/f9b80ac5249aa94f9c61f4630a8352b662f37a97 Ignore as it is a merge commit.
• https://github.com/hopv/rethfl/commit/6be0f53c1e1d0b29fcd73d2ea744ea73d9ef106e Ignore as it only adds a benchmark.
• https://github.com/hopv/rethfl/commit/f7cfe3559ed8bdfecca38e9e2a066fa78804fe5c Ignore as it is a merge commit.
• https://github.com/hopv/rethfl/commit/1a4cd1481fc41601cbbae625c631c65d4001d827 Ignore
• [ ] https://github.com/hopv/rethfl/commit/71507fe3cbf5feec46e8d8c117eb38993d187e03 We can add this although it is not necessary.
• [ ] https://github.com/hopv/rethfl/commit/a97e9f49354ecc5e372745bb1a6c1529ebc70948 This fixes --show-refinement, but this might have been already fixed.
• https://github.com/hopv/rethfl/commit/08c1220d3d6a90bf14b4fb494850171ae1bac9ce Ignore
• [ ] https://github.com/hopv/rethfl/commit/3183787a13de1a5737b68d58a705d82caded9855 This is related to https://github.com/hopv/rethfl/commit/a97e9f49354ecc5e372745bb1a6c1529ebc70948.
• [ ] https://github.com/hopv/rethfl/commit/e066dc782c7105e389cd01cf5102205916a7ca33 A small change, but we can add this.
• [ ] https://github.com/hopv/rethfl/commit/08ab27c7cca9d0df44c812467de25db173efc72b This fixes a bug in inlining, but I'm not sure if this has already been fixed.
• [ ] https://github.com/hopv/rethfl/commit/fbe925994446e0ea1aba59889e121307de53346a This commits adds an option --dont_show_refinement. I think the option itself is useless, but this commit also modifies disprove.ml, which we might need to apply.
• https://github.com/hopv/rethfl/commit/6eaec86035c2aaa695e2c5f337c9f56b7e62ec7a Ignore
• [ ] https://github.com/hopv/rethfl/commit/3f66563b3775316a962745a2142cb73cec409809 This adds an option --tractable_check_only. I will apply this change, but I think using the executable just for this check is stupid. We should use (parts of) ReTHFL as libraries in MuHFL.
• [ ] https://github.com/hopv/rethfl/commit/a25d1dcfbe0d4553b646feff07a0bd6347ad83a0 This adds --stop_if_intractable flag. Again, I will apply this commit, but I'm not sure if we should have such an option.
• https://github.com/hopv/rethfl/commit/8512be4ede7f96f263f765208d789f1cd36667f7 Ignore. This is an update to OCaml 4.12, but I've already sent a PR for OCaml 4.14.
• https://github.com/hopv/rethfl/commit/9c60b6b7fc0b6cf2d332e8e813911a6c1fe22480 Ignore as it only reverts the run_command function.
• [ ] https://github.com/hopv/rethfl/commit/64989be803c04667e4019573cbc0f99c8582c26f This fixes a bug of inlining, but it might have been already fixed.
• https://github.com/hopv/rethfl/commit/0d2e5978d850122f29dd6fd14315b003d045a77a Ignore. This commit adds --z3_path, but I don't think we need to have such an option. (We should modify MuHFL so that it doesn't use it.)
• https://github.com/hopv/rethfl/commit/1da67fb44f60bcbbd6a6e6691c69b725a08d1365 https://github.com/hopv/rethfl/commit/ea5b27aa50bdc2ec7dd3e07f68739ec44c503cf4 and https://github.com/hopv/rethfl/commit/69a096adcffe46b3cdb19286b86eb5ce68a01f98 Ignore. These commits are for PCSat (fptprove) so and I'm not planning to maintain this backend.
• [ ] https://github.com/hopv/rethfl/commit/f0485b74ad6733424a1e014a4acd9e8e2a05e663 This improves the printing of refinement types. I'm not sure what the delta is, but it might be worth porting.
• [ ] https://github.com/hopv/rethfl/commit/2a7692a6fbcca9368a53fda04eba440178e4145f The commit messages says that this allows annotations. If the meaning of "annotations" is the refinement type annotation, then maybe we should not merge this. Also note that this commit is quite big and is hard to check.
• [ ] https://github.com/hopv/rethfl/commit/0bd44c4926fd1dc0b32a156474034b3872335ddd Seems like this is related to the previous commit.
• [X] https://github.com/hopv/rethfl/commit/ac75736aca9c1b4b592615efb08da7baea5019a6 This commit fixes a bug for --show-refinement, which was caused when the dual formuala was used. I haven't figured out in which commit the bug was introduced. This commit also does some cosmetic changes. This has been partially ported by https://github.com/hopv/rethfl/pull/6.
• [ ] https://github.com/hopv/rethfl/commit/2b839394e5ecd82c0e14215324d1e5511a54ff57 This commit adds liu-solver and also an option --solve-dual-chc, which allows users to choose whether to use the dual (extended) CHC. I'm not planning to port the former, but the latter seems useful.