z3.rs icon indicating copy to clipboard operation
z3.rs copied to clipboard

Published 20 hours ago • verified publisher icon prove-rs

Strongly typed bitvector-lengths

Open djrenren opened this issue 3 years ago • 1 comments

Now that const generics are stable, we could have a pub struct BV<'ctx, const N: usize>. This would prevent any mix ups when you have multiple sizes of bitvector floating around. I don't have time to put together a PR for this atm, but it would be really neat and I think not too difficult.

djrenren avatar Sep 28 '21 05:09 djrenren

If anyone decides to implement this please make sure that the ability to have bitvectors with sizes not known at compile time is not lost. I think this means that two versions of BV may be needed? I'm not entirely sure as I am not very familiar with Rust const generics.

GreenBeard avatar Nov 06 '21 05:11 GreenBeard