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)

• a0cd21e Ignore. The Command module seems useful, but is reverted in 9c60b6b. The other benchmark stuff is not worth committing.
• d900c96 Ignore as it is a merge commit.
• f9b80ac Ignore as it is a merge commit.
• 6be0f53 Ignore as it only adds a benchmark.
• f7cfe35 Ignore as it is a merge commit.
• 1a4cd14 Ignore
• 71507fe We can add this although it is not necessary.
• a97e9f4 This fixes --show-refinement, but this might have been already fixed.
• 08c1220 Ignore
• 3183787 This is related to a97e9f4.
• e066dc7 A small change, but we can add this.
• 08ab27c This fixes a bug in inlining, but I'm not sure if this has already been fixed.
• fbe9259 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.
• 6eaec86 Ignore
• 3f66563 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.
• a25d1dc This adds --stop_if_intractable flag. Again, I will apply this commit, but I'm not sure if we should have such an option.
• 8512be4 Ignore. This is an update to OCaml 4.12, but I've already sent a PR for OCaml 4.14.
• 9c60b6b Ignore as it only reverts the run_command function.
• 64989be This fixes a bug of inlining, but it might have been already fixed.
• 0d2e597 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.)
• 1da67fb ea5b27a and 69a096a Ignore. These commits are for PCSat (fptprove) so and I'm not planning to maintain this backend.
• f0485b7 This improves the printing of refinement types. I'm not sure what the delta is, but it might be worth porting.
• 2a7692a 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.
• 0bd44c4 Seems like this is related to the previous commit.
• ac75736 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 fix show-refinement when dual chc is used #6.
• 2b83939 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.