From f4f9fd94afbda6eaca91bd61059cdfdcc55c9ddb Mon Sep 17 00:00:00 2001 From: mnemonikr <138624285+mnemonikr@users.noreply.github.com> Date: Thu, 11 Dec 2025 22:44:37 -0800 Subject: [PATCH 1/3] Additional small fixes in sym --- crates/sym/src/buf.rs | 24 ++++++++++-------------- crates/sym/src/vec.rs | 2 +- 2 files changed, 11 insertions(+), 15 deletions(-) diff --git a/crates/sym/src/buf.rs b/crates/sym/src/buf.rs index 7d3e022..67e7420 100644 --- a/crates/sym/src/buf.rs +++ b/crates/sym/src/buf.rs @@ -84,17 +84,15 @@ impl std::ops::IndexMut for SymbolicBitBuf { impl From> for Vec { fn from(mut value: SymbolicBitBuf) -> Self { const { - assert!(N % 8 == 0); + assert!(N.is_multiple_of(8)); } - let num_bytes = N / 8; - let mut result = Vec::with_capacity(num_bytes); - for n in 0..num_bytes { - let mut bits = [crate::FALSE; 8]; - for i in 0..8 { - std::mem::swap(&mut bits[i], &mut value.bits[8 * n + i]); - } - result.push(SymbolicByte::from(bits)); + let mut result = Vec::with_capacity(N / 8); + let (buf_bytes, _) = value.bits.as_chunks_mut::<8>(); + for buf_byte in buf_bytes { + let mut byte = [crate::FALSE; 8]; + std::mem::swap(&mut byte, buf_byte); + result.push(SymbolicByte::from(byte)); } result @@ -109,8 +107,7 @@ impl TryFrom> for SymbolicBitBuf { let initializer = |uninit_bits: &mut [MaybeUninit]| { value .into_iter() - .map(|byte| byte.into_inner().into_iter()) - .flatten() + .flat_map(|byte| byte.into_inner().into_iter()) .enumerate() .for_each(|(i, bit)| { uninit_bits[i].write(bit); @@ -136,8 +133,7 @@ impl TryFrom> for SymbolicBitBuf { let initializer = |uninit_bits: &mut [MaybeUninit]| { value .into_iter() - .map(|byte| byte.inner().iter()) - .flatten() + .flat_map(|byte| byte.inner().iter()) .cloned() .enumerate() .for_each(|(i, bit)| { @@ -221,7 +217,7 @@ impl SymbolicBitBuf { let initializer = |uninit_bits: &mut [MaybeUninit]| { self.bits .into_iter() - .chain(rhs.bits.into_iter()) + .chain(rhs.bits) .enumerate() .for_each(|(i, bit)| { uninit_bits[i].write(bit); diff --git a/crates/sym/src/vec.rs b/crates/sym/src/vec.rs index a30a823..175f7a0 100644 --- a/crates/sym/src/vec.rs +++ b/crates/sym/src/vec.rs @@ -28,7 +28,7 @@ impl SymbolicBitVec { } pub fn num_bytes(&self) -> usize { - self.bits.len().next_multiple_of(8) / 8 + self.bits.len().div_ceil(8) } pub fn len(&self) -> usize { From e04f6c9728549ed60ba7bca29c9002b7d7818a09 Mon Sep 17 00:00:00 2001 From: mnemonikr <138624285+mnemonikr@users.noreply.github.com> Date: Thu, 11 Dec 2025 22:49:07 -0800 Subject: [PATCH 2/3] Use FALSE constant in SymbolicBitBuf --- crates/sym/src/buf.rs | 16 +++++++--------- 1 file changed, 7 insertions(+), 9 deletions(-) diff --git a/crates/sym/src/buf.rs b/crates/sym/src/buf.rs index 67e7420..61bc074 100644 --- a/crates/sym/src/buf.rs +++ b/crates/sym/src/buf.rs @@ -2,7 +2,7 @@ use std::mem::MaybeUninit; use std::ops::Deref; -use crate::SymbolicBit; +use crate::bit::{FALSE, SymbolicBit}; /// An array of symbolic bits. #[derive(PartialEq, Eq, Debug, Clone)] @@ -62,9 +62,7 @@ impl From> for [SymbolicBit; N] { impl Default for SymbolicBitBuf { fn default() -> Self { - const DEFAULT: SymbolicBit = SymbolicBit::Literal(false); - let bits = [DEFAULT; N]; - Self { bits } + Self { bits: [FALSE; N] } } } @@ -90,7 +88,7 @@ impl From> for Vec { let mut result = Vec::with_capacity(N / 8); let (buf_bytes, _) = value.bits.as_chunks_mut::<8>(); for buf_byte in buf_bytes { - let mut byte = [crate::FALSE; 8]; + let mut byte = [FALSE; 8]; std::mem::swap(&mut byte, buf_byte); result.push(SymbolicByte::from(byte)); } @@ -332,7 +330,7 @@ impl std::ops::ShlAssign for SymbolicBitBuf { fn shl_assign(&mut self, rhs: Self) { for (i, shift_bit) in rhs.bits.into_iter().enumerate() { let mut shifted_value = self.clone(); - shifted_value.shift(1 << i, SymbolicBit::Literal(false), ShiftDirection::Left); + shifted_value.shift(1 << i, FALSE, ShiftDirection::Left); self.mux(shifted_value, !shift_bit); } } @@ -349,7 +347,7 @@ impl std::ops::Shl for SymbolicBitBuf { impl std::ops::ShlAssign for SymbolicBitBuf { fn shl_assign(&mut self, rhs: usize) { - self.shift(rhs, SymbolicBit::Literal(false), ShiftDirection::Left); + self.shift(rhs, FALSE, ShiftDirection::Left); } } @@ -367,7 +365,7 @@ impl std::ops::ShrAssign for SymbolicBitBuf { fn shr_assign(&mut self, rhs: Self) { for (i, shift_bit) in rhs.bits.into_iter().enumerate() { let mut shifted_value = self.clone(); - shifted_value.shift(1 << i, SymbolicBit::Literal(false), ShiftDirection::Right); + shifted_value.shift(1 << i, FALSE, ShiftDirection::Right); self.mux(shifted_value, !shift_bit); } } @@ -384,7 +382,7 @@ impl std::ops::Shr for SymbolicBitBuf { impl std::ops::ShrAssign for SymbolicBitBuf { fn shr_assign(&mut self, rhs: usize) { - self.shift(rhs, SymbolicBit::Literal(false), ShiftDirection::Right); + self.shift(rhs, FALSE, ShiftDirection::Right); } } From 81633fffa943be3a2e2eb01915df6e95a3878bb1 Mon Sep 17 00:00:00 2001 From: mnemonikr <138624285+mnemonikr@users.noreply.github.com> Date: Thu, 11 Dec 2025 22:53:37 -0800 Subject: [PATCH 3/3] if let chain was stabalized yessss --- crates/sym/src/eval.rs | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/crates/sym/src/eval.rs b/crates/sym/src/eval.rs index 579672d..f70f47d 100644 --- a/crates/sym/src/eval.rs +++ b/crates/sym/src/eval.rs @@ -113,10 +113,10 @@ impl VariableAssignments { pub fn from_bitvecs(variables: &SymbolicBitVec, literals: &SymbolicBitVec) -> Self { let iter = std::iter::zip(variables.iter(), literals.iter()).filter_map(|(variable, literal)| { - if let SymbolicBit::Variable(variable) = variable { - if let SymbolicBit::Literal(literal) = literal { - return Some((*variable, *literal)); - } + if let SymbolicBit::Variable(variable) = variable + && let SymbolicBit::Literal(literal) = literal + { + return Some((*variable, *literal)); } None