Missing API for BitVectors

[the-ssd]

Z3 can make bitvectors from arrays of bools. Something like this should work (I haven't tested it yet),

I am not sure about endianness, and how it will work

pub fn from_bit_vec(ctx: &'ctx Context, bit_vec: Vec<bool>) -> Option<BV<'ctx>> {
    let ast = unsafe {
        let size = bit_vec.len() as u32;
        let bits = bit_vec.as_ptr();

        let numeral_ptr = Z3_mk_bv_numeral(ctx.z3_ctx, size, bits);
        if numeral_ptr.is_null() {
            return None;
        }

        numeral_ptr
    };
    Some(unsafe { Self::wrap(ctx, ast) })
}

pub fn from_byte_vec(ctx: &'ctx Context, byte_vec: Vec<u8>) -> Option<BV<'ctx>> {
    let mut bit_vec = Vec::with_capacity(byte_vec.len() * 8);
    for item in byte_vec {
        for offset in 0..8 {
            let mask = 1 << offset;
            let bit = item & mask != 0;
            bit_vec.push(bit);
        }
    }

    Self::from_bit_vec(ctx, bit_vec)
}

I will make a PR when I test it.

[toolCHAINZ]

The from_bit_vec API has been added in #398 and #399.

As I mentioned in #333, there's not yet a version of the second API you provided, but I think I would want such an API to be explicit about the endianness (much like how u64 explicitly has from_le_bytes and from_be_bytes)