bitvector overflow and conversion (to/from integers) operators

[Clark Barrett]

We'd like to call your attention to some new operators that are now standard in the theory of FixedSizeBitvectors as of version 2.7.  These are based on and informed by discussions with the community (including on this email list) over the past few years.

1. Overflow Predicates

First, we have added "overflow" predicates, whose semantics is that they are true if the corresponding bitvector arithmetic operation would overflow.  The new operators are:

bvnego, bvuaddo, bvsaddo, bvumulo, bvsmulo

Please refer to the theory documentation for their precise definitions.

2. 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).

Best,

The SMT-LIB initiative maintaniers

(Clark Barrett, Pascal Fontaine, Cesare Tinelli)