The formulae top and bot are constant

[Halbaroth]

This PR makes clear that the environments of both CC(X) and UF(X) are constant. The previous signature of the constructors for these environments was unit -> t and not t only because they use the top and bot semantic values. As the module Combine in Shostak cannot contain constants because of limitations with recursive module in OCaml, we have put these constants in a trivial closure.

I create a new module X which is an alias of Shostak.Combine and contains the constants top and bot.

Note: I don't remove all the aliases module X = Shostak.Combine in many modules of AE. We can do it gradually and modifying all the files will be painful while rebasing our current PRs.

Note: I cannot turn the environment of Theory into a constant because this environment uses mutable states to enqueue facts. I plan to fix that in another PR (probably by writing a module for functional queues but I have to check how the current environment behaves while backtracking).

[bclement-ocp]

This is somewhat conflicting with the direction I thought were trying to take with #798. Can you explain why it is important that these environments are constants?

I would also advise against writing functional queues for the Theory module. As far as I know, the queues in Theory are used locally and are empty between steps, we would never make use of the extra functionality provided by a functional queue compared to an imperative one.

[Halbaroth]

I think the main change here is to make clear that top and bot are constant. I can change the title. The reason why I did that it's because I want to understand why the environments of these modules seem to be imperative. If there is no reason to be imperative, we should make it clear in the signature. You can modify the signature again when you will merge your PR with a new UF.

[bclement-ocp]

I have given a longer thought about this, and I really don't like the introduction of X as a toplevel module (especially when it is a common alias in the rest of the code, and even further when it is mostly empty). Can we instead add the definitions:

let top = top ()
let bot = bot ()

directly in Shostak.Combine (but not CX), with the appropriate signature change?

[bclement-ocp]

You should be able to do `module Combine : sig include Sig.X val top : r val bot : r end` shadowing the `unit -> r` versions of `top` and `bot` I think.

[Halbaroth]

You should be able to do module Combine : sig include Sig.X val top : r val bot : r end shadowing the unit -> r versions of top and bot I think.

I removed my comment because I found this solution... :D

[bclement-ocp]

Ah, I was not sure if this was a GitHub bug that it didn't appear in the UI hence why I replied by email :) All good then!