BitVector <-> Integer conversions

[romac]

Since both Z3 [0] and CVC4 [1] apparently support interpreted conversions between bit vectors and integers (via bv2int, int2bv and bv2nat, nat2bv respectively), perhaps we could add support for such conversions in Inox, with a fallback for other solvers via recursive conversion procedures implemented as a theory encoder?

I have a PR for ScalaZ3 with a test for such Int<->BigInt conversions at epfl-lara/ScalaZ3#73.

[0] Z3Prover/z3#1481 (comment)
[1] cvc5/cvc5#750

/cc @samarion @jad-hamza @vkuncak

[vkuncak]

Don't we have this already? @agilot @sankalpgambhir ?

[agilot]

I think we only have casts from bit vectors to other bit-vector types

In Stainless running:

def foo() = 
  val i: Int = 0
  val ibig: BigInt = BigInt(i)

gives the following error

[ Error  ] test.scala:12:22: Only literal arguments are allowed for BigInt.
             val ibig: BigInt = BigInt(i)
                                ^^^^^^^^^

[sankalpgambhir]

Partially addressed in #260