Consider using int instead of uint in the managed Z3 API

Jul 14, 2014 at 1:24 PM
The current version (4.3) of the Z3 managed API uses unsigned ints everywhere. Examples: The arguments to MkExtract and BitVecExpr.SortSize.

These arguments are meant to be >= 0 which makes the data type choice understandable. On the other hand this causes lots of unsigned/signed issues in C#. For example:
var sortSize = 32;
context.MkBV(0, sortSize); //error! sortSize is int. must be uint
Calculations with mixed int and uint are very awkward and require tons of casts.

Please consider taking a breaking change in the next major version and changing all managed APIs to use signed integers (and validate them to be >= 0).

(I have written a ton of Z3 code in the last month involving bitvectors. This issue bites me every day in a few places.)
Coordinator
Jul 14, 2014 at 2:02 PM
Thanks for the suggestion! I'm not fully convinced this would really help. It would be quite a breaking change to do that, and it would also make the .NET API diverge from the other APIs too. Is this only a problem when using `var' do declare variables and the implicit signed type it assumes? Furthermore, it would make it impossible to pass anything >= 2^31 to those functions, which would be a limitation that doesn't exist in the other APIs.
Jul 14, 2014 at 2:24 PM
The var example was just an example. Every time you want to use an int that comes from somewhere else in the program you have to insert a cast. Most .NET APIs use signed ints. I'll add another example to make this point:
BitVecExpr someExpr = ...;
int bitvectorSize = Utils.GetBitvectorSizeRequiredForBitcount((int)someExpr.SortSize);
BitVecExpr countExpr = context.MkBVConst("count", (uint)bitvectorSize);
Here, Utils.GetBitcountRequiredForCounting is a math helper that basically computes ceil(log2(x)). It deals in ints because it supports signed input.

Casting surprisingly often comes up when using arithmetical operators. For example:

int a;
uint b;
var x = a << b; //does not compile. 2nd operand must be convertible int

The C# language and BCL are just made for ints.

Your objections are valid of course. It's a trade-off to be made. Just wanted to make you are aware of this.