Add missing API for BV

z3/src/ast.rs

@@ -1346,6 +1346,34 @@ impl<'ctx> BV<'ctx> {
         Some(unsafe { Self::wrap(ctx, ast) })
     }
 
+    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)
+    }
+
     pub fn new_const<S: Into<Symbol>>(ctx: &'ctx Context, name: S, sz: u32) -> BV<'ctx> {
         let sort = Sort::bitvector(ctx, sz);
         unsafe {

z3/tests/lib.rs

@@ -2002,3 +2002,46 @@ fn test_model_iter() {
         vec![ast::Dynamic::new_const(&ctx, "a", &Sort::int(&ctx))]
     );
 }
+
+#[test]
+fn test_bitvector_from_bit_vec() {
+    let cfg = Config::new();
+    let ctx = Context::new(&cfg);
+
+    // 0b01010101
+    let bit_vec = vec![true, false, true, false, true, false, true, false];
+
+    let a = ast::BV::new_const(&ctx, "a", 8);
+    let b = ast::BV::from_bit_vec(&ctx, bit_vec).unwrap();
+
+    let solver = Solver::new(&ctx);
+    solver.assert(&a._eq(&b));
+    assert_eq!(solver.check(), SatResult::Sat);
+
+    let model = solver.get_model().unwrap();
+    let av = model.eval(&a, true).unwrap().to_string();
+    assert_eq!(av, "#x55".to_string());
+}
+
+#[test]
+fn test_bitvector_from_byte_vec() {
+    let cfg = Config::new();
+    let ctx = Context::new(&cfg);
+
+    // 0x55AA
+    // 85 = 0x55 = 01010101
+    // 170 = 0xAA = 10101010
+    // The array should be ordered like this (at least that is how it works in rust internally)
+    let byte_vec = vec![170, 85];
+
+    let a = ast::BV::new_const(&ctx, "a", 16);
+    let b = ast::BV::from_byte_vec(&ctx, byte_vec).unwrap();
+
+    let solver = Solver::new(&ctx);
+    solver.assert(&a._eq(&b));
+    assert_eq!(solver.check(), SatResult::Sat);
+
+    let model = solver.get_model().unwrap();
+    let av = model.eval(&a, true).unwrap().to_string();
+    assert_eq!(av, "#x55aa".to_string());
+}