-
Notifications
You must be signed in to change notification settings - Fork 129
Closed
Description
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.
Metadata
Metadata
Assignees
Labels
No labels