bv2int and bv2nat

[florianschanda]

Hi,

The bitvector theory describes bv2nat, however Z3 implements bv2int. I was surprised to find out that this actually behaves like bv2nat (i.e. never produces negative numbers). Could it be renamed so that we (SPARK) don't have to generate different VCs for CVC4 and Z3?

Or, even better, support both?

[delcypher]

bv2nat is used to describe the semantics of the bitvector functions. I don't believe there is any requirement to actually implement bv2nat as a function itself.

I was surprised to find out that this actually behaves like bv2nat (i.e. never produces negative numbers)

Why is this surprising? BitVectors aren't signed. They are only treated in a signed manner by certain operators. int is the name of the integer sort in SMT-LIB so bv2int is a very sensible name for the function.

I was going to suggest using define-fun to work around this but this won't work because the BitVector sort is polymorphic (in the width of the bitvector).

It would be nice if the SMT-LIB standard actually defined functions to convert between Int and BitVector sorts but AFAIK they are not defined right now.

I think renaming bv2int to bv2nat is a bad idea because this will break users of Z3 that rely on this function.

Making bv2nat an alias of bv2int might be a possibility but that decision lies with the Z3 maintainers.

[wintersteiger]

What @delcypher said, plus: int2bv and bv2int are Z3-specific extensions that don't feature in any of the SMT theories or logics (until very recently there were no logics or benchmarks that contained Ints and BVs, now there is AUFBVDTLIA but it doesn't have an official logic definition yet), and they are essentially treated as uninterpreted (see also here). So, sorry, CVC4's functions are extensions just like Z3's and their semantics are not the same.

[NikolajBjorner]

I guess the question is interoperation, and that bv2nat and bv2int have the same meaning, so could be alias.