Expose the bv2nat and int2bv primitives

[bclement-ocp]

This patch exposes the bv2nat and int2bv primitives as symbols available to the user. Even though these symbols are not part of the official smtlib theories, they are useful for mixed bitvector/integer specifications that are likely to occur in the context of program verification, and they are also supported by other solvers such as Z3 and CVC5.

[Halbaroth]

Is the cache really useful?

[bclement-ocp]

I believe it is necessary to ensure that Dolmen knows that multiple uses of the primitive are actually the same primitive. I am not 100% sure we need it in this case though, @Gbury would know.

[Gbury]

So, for terms, the cache is useful and better, but not absolutely necessary. Basically, the cache ensures that we correctly identify two instances of what is the same symbol: without the cache, you would generate two different symbols for the same semantic one (e.g. two instance of bv2nat on bitvectors of size 3), and then end up in a situation where two terms that should be equal are not equal, that should not be too big of a problem (contrary to the same situation for types), especially since you then translate those terms to alt-ergo's terms. That being said, unless it becomes a problem, it's better to use a cache.

[bclement-ocp]

I think that fits with my understanding, thanks for the clarification. I think it's better to have the cache since Dolmen has it everywhere so we don't break the fact that identical constructors are physically equal, even if we don't currently depend on that.

(I've aso opened Gbury/dolmen#176 to suggest exposing with_cache so that we don't have to reimplement it)