From b49f4a908adf7bad66e41f09abe6c4ebfe002e5e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= <laeufer@cs.berkeley.edu>
Date: Thu, 16 May 2024 13:51:50 -0400
Subject: [PATCH] add bitvec conversions

---
 .github/workflows/test.yml |  1 +
 Cargo.toml                 |  4 +-
 src/io/bitvec.rs           | 95 ++++++++++++++++++++++++++++++++++++++
 src/io/mod.rs              |  3 ++
 4 files changed, 102 insertions(+), 1 deletion(-)
 create mode 100644 src/io/bitvec.rs

diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
index 194466a..6d87883 100644
--- a/.github/workflows/test.yml
+++ b/.github/workflows/test.yml
@@ -20,6 +20,7 @@ jobs:
         features:
           - default
           - bigint
+          - bitvec1
 
     steps:
     - name: Update Rust to ${{ matrix.toolchain }}
diff --git a/Cargo.toml b/Cargo.toml
index 9a77c20..914b430 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -13,6 +13,7 @@ readme = "Readme.md"
 rust-version = "1.73.0"
 
 [dependencies]
+bitvec = { version = "1.0", optional = true, features = ["std", "alloc"] }
 num-bigint = { version = "0.4.5", optional = true}
 smallvec = "1.13.2"
 thiserror = "1.0.60"
@@ -22,4 +23,5 @@ proptest = "1.4.0"
 
 [features]
 default = []
-bigint = ["dep:num-bigint"]
\ No newline at end of file
+bigint = ["dep:num-bigint"]
+bitvec1 = ["dep:bitvec"]
diff --git a/src/io/bitvec.rs b/src/io/bitvec.rs
new file mode 100644
index 0000000..95b46ac
--- /dev/null
+++ b/src/io/bitvec.rs
@@ -0,0 +1,95 @@
+// Copyright 2024 The Regents of the University of California
+// released under BSD 3-Clause License
+// author: Kevin Laeufer <laeufer@berkeley.edu>
+
+use crate::io::strings::{from_bit_str, to_bit_str};
+use crate::{WidthInt, Word};
+use bitvec::macros::internal::funty::Fundamental;
+use bitvec::prelude::*;
+
+pub(crate) fn to_bitvec(values: &[Word], width: WidthInt) -> BitVec {
+    if width == 0 {
+        return bitvec![];
+    }
+
+    let mut out = BitVec::with_capacity(width as usize);
+    for (word_ii, word) in values.iter().enumerate() {
+        let msb_word = word_ii == values.len() - 1;
+        let uneven_bits = width % Word::BITS != 0;
+        let bits = if msb_word && uneven_bits {
+            width % Word::BITS
+        } else {
+            Word::BITS
+        };
+        for bit in 0..bits {
+            let value = (*word >> bit) & 1;
+            out.push(value == 1);
+        }
+    }
+    debug_assert_eq!(out.len(), width as usize);
+    out
+}
+
+pub(crate) fn from_bitvec<T, O>(bits: &BitVec<T, O>, out: &mut [Word]) -> WidthInt
+where
+    T: BitStore,
+    O: BitOrder,
+{
+    if bits.is_empty() {
+        return 0;
+    }
+    let width = bits.len() as WidthInt;
+    let words = width.div_ceil(Word::BITS);
+    let mut word = 0 as Word;
+    let mut out_ii = (words - 1) as usize;
+
+    for (ii, cc) in bits.iter().rev().enumerate() {
+        let ii_rev = width as usize - ii - 1;
+        if ii > 0 && ((ii_rev + 1) % Word::BITS as usize) == 0 {
+            out[out_ii] = word;
+            out_ii -= 1;
+            word = 0;
+        }
+        let value: Word = cc.as_u8().into();
+        word = (word << 1) | value;
+    }
+    debug_assert_eq!(out_ii, 0);
+    out[0] = word;
+
+    width
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+    use proptest::proptest;
+
+    fn str_to_bitvec(s: &str) -> BitVec {
+        let mut out = BitVec::with_capacity(s.len());
+        for cc in s.chars().rev() {
+            match cc {
+                '0' => out.push(false),
+                '1' => out.push(true),
+                _ => unreachable!(),
+            }
+        }
+        out
+    }
+
+    fn do_test_from_to_bitvec(s: &str) {
+        let vec_in = str_to_bitvec(s);
+        let words = vec_in.len().div_ceil(Word::BITS as usize);
+        let mut out = vec![0; words];
+        let width = from_bitvec(&vec_in, &mut out);
+        assert_eq!(width as usize, vec_in.len());
+        let vec_out = to_bitvec(&out, width);
+        assert_eq!(vec_in, vec_out);
+    }
+
+    proptest! {
+        #[test]
+        fn test_from_to_bitvec(s in "[01]*") {
+            do_test_from_to_bitvec(&s);
+        }
+    }
+}
diff --git a/src/io/mod.rs b/src/io/mod.rs
index 865b4c8..d37c157 100644
--- a/src/io/mod.rs
+++ b/src/io/mod.rs
@@ -6,3 +6,6 @@
 #[cfg(feature = "bigint")]
 pub(crate) mod bigint;
 pub(crate) mod strings;
+
+#[cfg(feature = "bitvec1")]
+pub(crate) mod bitvec;