Get bitvector model as a vector of bool

[mikhailramalho]

I'm using the vc_bvConstExprFromStr methods to create some large bitvectors (width > 64), but is there a way to get its value from the model also as an array of bools or a string of 0's/1's? I only found the getBVInt, getBVUnsigned and getBVUnsignedLongLong functions.

[aytey]

Joining the dots: Z3Prover/z3#4568 (comment)

Are you using the C or Python API? Do you want an STP vc_boolType or a language-level Boolean type (e.g., bool in C99/Python)?

[aytey]

So I was just taking a look at this for you, and I noticed this:

• getBVInt calls GetUnsignedConst

• getBVUnsigned calls GetUnsignedConst

The code for GetUnsignedConst seems to be limited to unsigned numbers that fit in a machine unsigned int (the message says 32, but I think it would be supported for a 64-bit value if you're on a 64-bit host).

When you say you're "creat[ing] some large bitvectors (width > 64)", have you created BVs that are larger than your machine-size unsigned int and successfully retrieved them over the API?

Anyway back to your original issue: behind the scenes getBVUnsignedLongLong calls BitVector_to_Bin, which looks like it is close to what you need.

Edit

Actually, I need to change my response here. As far as I'm aware, there are no functions in the C API that directly return a heap-based object that is expected to be managed by the caller. Anything that returns a char* (e.g., get_git_version_sha) is returning a pointer that we do not expect the to free.

That being said, there are a few vc_print... methods that take a char** as an argument, and we update that as an output parameter. Would this work for you? You would need to pass in an address to an (unallocated) pointer, we could make this (double pointer) point to a string in memory that had your 0s/1s, and then you'd need to free it.

These print methods are exposed by the Python API, but I am really not sure how these are supposed to work. If you need this in the Python API, I might need to think a bit more ...

[aytey]

Should be done; take a look at: #358

To be clear: this PR needs to be agreed by one of: @msoos @TrevorHansen @rgov -- it is possible that they might not want this API call.

[mikhailramalho]

So I was just taking a look at this for you, and I noticed this:

• getBVInt calls GetUnsignedConst
• getBVUnsigned calls GetUnsignedConst

The code for GetUnsignedConst seems to be limited to unsigned numbers that fit in a machine unsigned int (the message says 32, but I think it would be supported for a 64-bit value if you're on a 64-bit host).

When you say you're "creat[ing] some large bitvectors (width > 64)", have you created BVs that are larger than your machine-size unsigned int and successfully retrieved them over the API?

Anyway back to your original issue: behind the scenes getBVUnsignedLongLong calls BitVector_to_Bin, which looks like it is close to what you need.

Edit

Actually, I need to change my response here. As far as I'm aware, there are no functions in the C API that directly return a heap-based object that is expected to be managed by the caller. Anything that returns a char* (e.g., get_git_version_sha) is returning a pointer that we do not expect the to free.

That being said, there are a few vc_print... methods that take a char** as an argument, and we update that as an output parameter. Would this work for you? You would need to pass in an address to an (unallocated) pointer, we could make this (double pointer) point to a string in memory that had your 0s/1s, and then you'd need to free it.

These print methods are exposed by the Python API, but I am really not sure how these are supposed to work. If you need this in the Python API, I might need to think a bit more ...

Returning the char pointer is fine by me, and it seems consistent with other functions like vc_printQueryStateToBuffer and vc_printCounterExampleToBuffer.

[aytey]

Okay; cool. So that's what's in the PR.

An example of usage is here: https://github.com/andrewvaughanj/stp/blob/return_bit_string/tests/api/C/bit_string.cpp#L40