Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
38 changes: 16 additions & 22 deletions crates/sym/src/buf.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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)]
Expand Down Expand Up @@ -62,9 +62,7 @@ impl<const N: usize> From<SymbolicBitBuf<N>> for [SymbolicBit; N] {

impl<const N: usize> Default for SymbolicBitBuf<N> {
fn default() -> Self {
const DEFAULT: SymbolicBit = SymbolicBit::Literal(false);
let bits = [DEFAULT; N];
Self { bits }
Self { bits: [FALSE; N] }
}
}

Expand All @@ -84,17 +82,15 @@ impl<const N: usize> std::ops::IndexMut<usize> for SymbolicBitBuf<N> {
impl<const N: usize> From<SymbolicBitBuf<N>> for Vec<SymbolicByte> {
fn from(mut value: SymbolicBitBuf<N>) -> 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 = [FALSE; 8];
std::mem::swap(&mut byte, buf_byte);
result.push(SymbolicByte::from(byte));
}

result
Expand All @@ -109,8 +105,7 @@ impl<const N: usize> TryFrom<Vec<SymbolicByte>> for SymbolicBitBuf<N> {
let initializer = |uninit_bits: &mut [MaybeUninit<SymbolicBit>]| {
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);
Expand All @@ -136,8 +131,7 @@ impl<const N: usize> TryFrom<Vec<&SymbolicByte>> for SymbolicBitBuf<N> {
let initializer = |uninit_bits: &mut [MaybeUninit<SymbolicBit>]| {
value
.into_iter()
.map(|byte| byte.inner().iter())
.flatten()
.flat_map(|byte| byte.inner().iter())
.cloned()
.enumerate()
.for_each(|(i, bit)| {
Expand Down Expand Up @@ -221,7 +215,7 @@ impl<const N: usize> SymbolicBitBuf<N> {
let initializer = |uninit_bits: &mut [MaybeUninit<SymbolicBit>]| {
self.bits
.into_iter()
.chain(rhs.bits.into_iter())
.chain(rhs.bits)
.enumerate()
.for_each(|(i, bit)| {
uninit_bits[i].write(bit);
Expand Down Expand Up @@ -336,7 +330,7 @@ impl<const N: usize> std::ops::ShlAssign for SymbolicBitBuf<N> {
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);
}
}
Expand All @@ -353,7 +347,7 @@ impl<const N: usize> std::ops::Shl for SymbolicBitBuf<N> {

impl<const N: usize> std::ops::ShlAssign<usize> for SymbolicBitBuf<N> {
fn shl_assign(&mut self, rhs: usize) {
self.shift(rhs, SymbolicBit::Literal(false), ShiftDirection::Left);
self.shift(rhs, FALSE, ShiftDirection::Left);
}
}

Expand All @@ -371,7 +365,7 @@ impl<const N: usize> std::ops::ShrAssign for SymbolicBitBuf<N> {
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);
}
}
Expand All @@ -388,7 +382,7 @@ impl<const N: usize> std::ops::Shr for SymbolicBitBuf<N> {

impl<const N: usize> std::ops::ShrAssign<usize> for SymbolicBitBuf<N> {
fn shr_assign(&mut self, rhs: usize) {
self.shift(rhs, SymbolicBit::Literal(false), ShiftDirection::Right);
self.shift(rhs, FALSE, ShiftDirection::Right);
}
}

Expand Down
8 changes: 4 additions & 4 deletions crates/sym/src/eval.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion crates/sym/src/vec.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand Down