Python API not very pythonic

[Celelibi]

Hello,

I just compiled and installed boolector. It's very nice, but the python API is very surprising on some aspects. The most important one is, I think, the __getitem__ method that reverse the order of the slice bounds.

In python the list slices are always written with the lower bound first.

>>> a = [1, 2, 3, 4]
>>> a[1:3]
[2, 3]

Other than that there's a few things that might not feel very natural to python users. Like the naming convention that doesn't follow the PEP8: It's more usual in python to spell method names all lower case with underscores. Bit vectors and arrays are also hardly iterable.

But I guess some of those would require incompatible API change and would be better suited for a pure python wrapper library.

[aytey]

I would guess that the slice arguments are to match what's in SMT-LIB with respect to taking an extract of bit-vector ... that is, in SMT-LIB, you say (_ extract <high> <low>) <bv> (http://smtlib.cs.uiowa.edu/theories-FixedSizeBitVectors.shtml), so Boolector's API has just matched that way of writing it.

[mpreiner]

As @andrewvaughanj said, the slice limits are reversed since it's based on the SMT-LIB semantics of the extract operator. I'm also not very happy with the method names, but I guess we have to stick with it if we don't want to break the Python API.

What would you expect from iterable bit-vectors and arrays?

[aytey]

Aside: as a user, I could tolerate a breaking change, if it made people "happier".

For our usage, Boolector's API is completely abstracted anyway, so one change in Boolector == one change in our API.

[Celelibi]

No doubt that it was made to match to C arguments, which itself match the SMT-LIB definition. But it doesn't have to be that way. The python slice notation is only loosely related to the C API and SMT-LIB. I mean it's understandable that the Slice method has the upper bound first. But the slice notation is not like a direct binding where one might read the documentation for the C API or the SMT-LIB specification and expect the python slice notation to follow it closely. Actually, since there's already a Slice method, what's the point of supporting the slice notation if it's not meant to follow the python conventions?

I know fixing this would break the python API. That's why I'm suggesting that this might go into a higher level wrapper library. (Which I would love to see include more high level stuff like C types or unbounded integers. But that's beside the scope of this issue I guess.)

The goal of iterating bit vectors or arrays is to build a model that does something slightly different to every bit of a bit vector or to every element of an array. I mean, it's not like you can't do:

for i in range(bv.width):
    something(bv[i])

But rather that you can't do:

for bit in bv:
    something(bit)

which is the usual idiom. Not to mention the functions and constructions that work on iterables, like zip, enumerate, map, reduce, comprension lists, the list constructor or the whole itertools module.

But I guess this can be fixed very easily by raising an IndexError exception (or a subclass thereof) when the index is out of bound instead of a generic BoolectorException. Adding a __len__ method is also pretty cheap and might help integrate more nicely with the rest of python.

[aniemetz]

@Celelibi thanks for the feedback!

I'm against changing the order for the slice operator. It's already confusing enough as it is and I'd rather have it be consistent with the SMT-LIB standard (and our C API is). I'd not break the API while we're still at 3.x, but for 4.x we can make major changes in the Python API and will consider your suggestions.

[mpreiner]

The slice is just for convenience since it's shorter to write. Instead of btor.Slice(x, 0, 0) you can just write x[0:0]. Same with arithmetic operations btor.Add(x,y) -> x + y.

[mpreiner]

Boolector is not actively maintained and developed anymore. It was succeeded by Bitwuzla and the repository is now archived.