setting BitVec

Stream: Is there code for X?

[Wrenna Robson]

I was expecting to find setLsb and setMsb as we have getLsb and getMsb in BitVec. Do these have a different name?

[Henrik Böving]

x ||| (1#w <<< n) is the name I would say

[Wrenna Robson]

That certainly is what I'd define it as, but I was somewhat expecting there to be a name for it beyond that!

[Henrik Böving]

BitVec currently implements SMT-LIB, SMT-LIB doesn't do this

[Wrenna Robson]

Right.

[Henrik Böving]

If you want to add it feel free but keep in mind that you would have to define a couple dozen theorems to capture its behavior.

[Wrenna Robson]

Oh of course :)

[Wrenna Robson]

Actually I have some more complicated functions that I've defined due to an off-library project (which I hope to get into the library at some point) and I was hoping to mimic the API

[Wrenna Robson]

I assume a similar reason is why BitVec.msb exists but BitVec.lsb does not.

[Ralf Stephan]

@Wrenna Robson is your code somewhere? I'm suddenly in need of this too.

[Wrenna Robson]

Unfortunately I don't think I did do it fully.

[Wrenna Robson]

It would be useful I think!