SMTLib 2.7 compliance: Bit-vector to/from Int conversions

[LeventErkok]

SMTLib 2.7 has standardized on conversions, which I quote below.

Good news is that most of the functionality is already in z3. If I read the code correctly:

• ubv_to_int is z3's bv2nat
• sbv_to_int doesn't seem to exist. (Note that z3's bv2int is actually an alias to bv2nat, which is rather confusing.)
• int_to_bv is z3's int2bv

Here's Clark's message:

Conversion operators
We have also standardized three new conversion operators:

ubv_to_int and sbv_to_int

convert from bitvectors to integers, where the bitvector is interpreted as unsigned or signed. respectively.

Examples:
(ubv_to_int #b1011) = 11
(sbv_to_int #b1011) = -5

And the operator

int_to_bv

is a new indexed operator, which is indexed by a positive numeral N and converts an integer to a bitvector of size N. The semantics here is that given an input x, the value x mod 2^N is computed and then the unsigned bitvector corresponding to this value (which is a positive integer) is returned. Note that this same definition also correctly converts negative integers to their signed bitvector representation, so only a single integer to bitvector operator is needed. Please refer to the theory documentation for more details.

Examples;
((_ int_to_bv 4) 11) = #b1011
((_ int_to_bv 4) -5) = #b1011

One other note: there are two functions, bv2nat and nat2bv, that appear in the theory documentation (and indeed were already there in version 2.6) . However, these functions are NOT operators in the SMT-LIB theory - they are only used to help define the semantics of certain operators. Some solvers have implemented support for operators with these or similar names. Such implementations should be viewed as solver-specific extensions and are not part of the standard. The new operators mentioned here are the ones that should be supported to be compliant with version 2.7. The rationale for the new names (as opposed to the semantic function names) is that natural numbers are not part of SMT-LIB, so those names would be misnomers. Additionally, the use of "2" as opposed to "to" is not consistent with other conversion operators in SMT-LIB (in strings and floating point, for example).