From 7e798d2f11bb091c586af8d5687bca429ba10566 Mon Sep 17 00:00:00 2001 From: mnemonikr <138624285+mnemonikr@users.noreply.github.com> Date: Thu, 11 Dec 2025 12:37:55 -0800 Subject: [PATCH] Reorganize sym.rs into bit.rs and vec.rs --- crates/sym/src/bit.rs | 138 ++++++++++++++++++++++++++++ crates/sym/src/convert.rs | 14 ++- crates/sym/src/lib.rs | 7 +- crates/sym/src/{sym.rs => vec.rs} | 148 +----------------------------- 4 files changed, 156 insertions(+), 151 deletions(-) create mode 100644 crates/sym/src/bit.rs rename crates/sym/src/{sym.rs => vec.rs} (84%) diff --git a/crates/sym/src/bit.rs b/crates/sym/src/bit.rs new file mode 100644 index 0000000..6e79b63 --- /dev/null +++ b/crates/sym/src/bit.rs @@ -0,0 +1,138 @@ +use std::rc::Rc; + +pub const FALSE: SymbolicBit = SymbolicBit::Literal(false); +pub const TRUE: SymbolicBit = SymbolicBit::Literal(true); + +/// A value that can be used to represent a variable bit, possibly with constraints on its value. +#[derive(Debug, Clone, PartialEq, Eq)] +pub enum SymbolicBit { + /// A literal `true` or `false` value. + Literal(bool), + + /// A variable value. The parameter is the identifier for this variable. Two variables with the + /// same identifier are equivalent. + Variable(usize), + + /// The negation of a symbolic bit. The `!` operator should be preferred to this, as it has the + /// opportunity to perform simplications where a direct construction does not. + Not(Rc), + + /// The conjunction of two symbolic bits. The `&` operator should be preferred to this, as it + /// has the opportunity to perform simpliciations where a direct construction does not. + And(Rc, Rc), +} + +impl SymbolicBit { + pub fn equals(self, rhs: Self) -> Self { + (self.clone() & rhs.clone()) | (!self & !rhs) + } + + pub fn select(self, lhs: Self, rhs: Self) -> Self { + (self.clone() & lhs) | (!self & rhs) + } + + pub fn is_identical(&self, rhs: &Self) -> bool { + match self { + Self::Literal(x) => { + if let Self::Literal(y) = rhs { + return *x == *y; + } + } + Self::Variable(x) => { + if let Self::Variable(y) = rhs { + return *x == *y; + } + } + Self::Not(x) => { + if let Self::Not(y) = rhs { + if Rc::ptr_eq(x, y) { + return true; + } else if let Self::Variable(x) = **x + && let Self::Variable(y) = **y + { + // Check if same variable + return x == y; + } + } + } + Self::And(x, y) => { + if let Self::And(u, v) = rhs { + if Rc::ptr_eq(x, u) && Rc::ptr_eq(y, v) || Rc::ptr_eq(x, v) && Rc::ptr_eq(y, u) + { + return true; + } else if let Self::Variable(x) = **x + && let Self::Variable(y) = **y + && let Self::Variable(u) = **u + && let Self::Variable(v) = **v + { + // Check if same variables + return x == u && y == v || x == v && y == u; + } + } + } + } + + false + } +} + +impl Default for SymbolicBit { + fn default() -> Self { + FALSE + } +} + +impl std::ops::Not for SymbolicBit { + type Output = Self; + + fn not(self) -> Self::Output { + match self { + SymbolicBit::Literal(false) => SymbolicBit::Literal(true), + SymbolicBit::Literal(true) => SymbolicBit::Literal(false), + SymbolicBit::Not(y) => Rc::unwrap_or_clone(y), + _ => SymbolicBit::Not(Rc::new(self)), + } + } +} + +impl std::ops::BitAnd for SymbolicBit { + type Output = Self; + + fn bitand(self, rhs: Self) -> Self::Output { + if self.is_identical(&rhs) { + return self; + } + + match self { + SymbolicBit::Literal(false) => return SymbolicBit::Literal(false), + SymbolicBit::Literal(true) => return rhs, + SymbolicBit::Not(z) if z.is_identical(&rhs) => return SymbolicBit::Literal(false), + _ => (), + } + + match rhs { + SymbolicBit::Literal(false) => return SymbolicBit::Literal(false), + SymbolicBit::Literal(true) => return self, + SymbolicBit::Not(z) if z.is_identical(&self) => return SymbolicBit::Literal(false), + _ => (), + } + + SymbolicBit::And(Rc::new(self), Rc::new(rhs)) + } +} + +impl std::ops::BitOr for SymbolicBit { + type Output = Self; + + fn bitor(self, rhs: Self) -> Self::Output { + !(!self & !rhs) + } +} + +impl std::ops::BitXor for SymbolicBit { + type Output = Self; + + fn bitxor(self, rhs: Self) -> Self::Output { + (self.clone() & !rhs.clone()) | (!self & rhs) + } +} diff --git a/crates/sym/src/convert.rs b/crates/sym/src/convert.rs index d456c32..e6a0b9c 100644 --- a/crates/sym/src/convert.rs +++ b/crates/sym/src/convert.rs @@ -2,8 +2,18 @@ use std::rc::Rc; use aiger_circuit::circuit::{AigerCircuit, AndOperand, AsAigerCircuit}; +use crate::bit::{FALSE, SymbolicBit}; use crate::buf::{SymbolicBitBuf, SymbolicByte}; -use crate::sym::{self, ConcretizationError, SymbolicBit, SymbolicBitVec}; +use crate::vec::SymbolicBitVec; + +#[derive(thiserror::Error, Debug)] +pub enum ConcretizationError { + #[error("non-literal bit at index {bit_index}")] + NonLiteralBit { bit_index: usize }, + + #[error("value exceeded maximum number of bytes ({max_bytes})")] + Overflow { max_bytes: usize }, +} impl From for SymbolicBit { fn from(value: bool) -> Self { @@ -210,7 +220,7 @@ impl FromIterator for SymbolicBitVec { pub fn symbolize(iter: impl IntoIterator) -> impl Iterator { iter.into_iter().flat_map(|byte| { - let mut bits = [sym::FALSE; 8]; + let mut bits = [FALSE; 8]; for (index, bit) in bits.iter_mut().enumerate() { *bit = SymbolicBit::Literal((byte & (1 << index)) > 0); diff --git a/crates/sym/src/lib.rs b/crates/sym/src/lib.rs index 0007bc9..36207d8 100644 --- a/crates/sym/src/lib.rs +++ b/crates/sym/src/lib.rs @@ -1,15 +1,18 @@ +mod bit; mod buf; mod convert; mod eval; mod pcode; -mod sym; +mod vec; +pub use crate::bit::*; pub use crate::buf::*; pub use crate::convert::ConcreteValue; +pub use crate::convert::ConcretizationError; pub use crate::convert::concretize; pub use crate::convert::concretize_into; pub use crate::eval::*; -pub use crate::sym::*; +pub use crate::vec::*; #[cfg(test)] mod tests; diff --git a/crates/sym/src/sym.rs b/crates/sym/src/vec.rs similarity index 84% rename from crates/sym/src/sym.rs rename to crates/sym/src/vec.rs index 99e442e..9404d05 100644 --- a/crates/sym/src/sym.rs +++ b/crates/sym/src/vec.rs @@ -1,155 +1,9 @@ use std::collections::VecDeque; -use std::rc::Rc; use std::sync::atomic::{AtomicUsize, Ordering}; +use crate::bit::{FALSE, SymbolicBit}; use crate::buf::SymbolicByte; -pub const FALSE: SymbolicBit = SymbolicBit::Literal(false); -pub const TRUE: SymbolicBit = SymbolicBit::Literal(true); - -/// A value that can be used to represent a variable bit, possibly with constraints on its value. -#[derive(Debug, Clone, PartialEq, Eq)] -pub enum SymbolicBit { - /// A literal `true` or `false` value. - Literal(bool), - - /// A variable value. The parameter is the identifier for this variable. Two variables with the - /// same identifier are equivalent. - Variable(usize), - - /// The negation of a symbolic bit. The `!` operator should be preferred to this, as it has the - /// opportunity to perform simplications where a direct construction does not. - Not(Rc), - - /// The conjunction of two symbolic bits. The `&` operator should be preferred to this, as it - /// has the opportunity to perform simpliciations where a direct construction does not. - And(Rc, Rc), -} - -#[derive(thiserror::Error, Debug)] -pub enum ConcretizationError { - #[error("non-literal bit at index {bit_index}")] - NonLiteralBit { bit_index: usize }, - - #[error("value exceeded maximum number of bytes ({max_bytes})")] - Overflow { max_bytes: usize }, -} - -impl SymbolicBit { - pub fn equals(self, rhs: Self) -> Self { - (self.clone() & rhs.clone()) | (!self & !rhs) - } - - pub fn select(self, lhs: Self, rhs: Self) -> Self { - (self.clone() & lhs) | (!self & rhs) - } - - pub fn is_identical(&self, rhs: &Self) -> bool { - match self { - Self::Literal(x) => { - if let Self::Literal(y) = rhs { - return *x == *y; - } - } - Self::Variable(x) => { - if let Self::Variable(y) = rhs { - return *x == *y; - } - } - Self::Not(x) => { - if let Self::Not(y) = rhs { - if Rc::ptr_eq(x, y) { - return true; - } else if let Self::Variable(x) = **x - && let Self::Variable(y) = **y - { - // Check if same variable - return x == y; - } - } - } - Self::And(x, y) => { - if let Self::And(u, v) = rhs { - if Rc::ptr_eq(x, u) && Rc::ptr_eq(y, v) || Rc::ptr_eq(x, v) && Rc::ptr_eq(y, u) - { - return true; - } else if let Self::Variable(x) = **x - && let Self::Variable(y) = **y - && let Self::Variable(u) = **u - && let Self::Variable(v) = **v - { - // Check if same variables - return x == u && y == v || x == v && y == u; - } - } - } - } - - false - } -} - -impl Default for SymbolicBit { - fn default() -> Self { - FALSE - } -} - -impl std::ops::Not for SymbolicBit { - type Output = Self; - - fn not(self) -> Self::Output { - match self { - SymbolicBit::Literal(false) => SymbolicBit::Literal(true), - SymbolicBit::Literal(true) => SymbolicBit::Literal(false), - SymbolicBit::Not(y) => Rc::unwrap_or_clone(y), - _ => SymbolicBit::Not(Rc::new(self)), - } - } -} - -impl std::ops::BitAnd for SymbolicBit { - type Output = Self; - - fn bitand(self, rhs: Self) -> Self::Output { - if self.is_identical(&rhs) { - return self; - } - - match self { - SymbolicBit::Literal(false) => return SymbolicBit::Literal(false), - SymbolicBit::Literal(true) => return rhs, - SymbolicBit::Not(z) if z.is_identical(&rhs) => return SymbolicBit::Literal(false), - _ => (), - } - - match rhs { - SymbolicBit::Literal(false) => return SymbolicBit::Literal(false), - SymbolicBit::Literal(true) => return self, - SymbolicBit::Not(z) if z.is_identical(&self) => return SymbolicBit::Literal(false), - _ => (), - } - - SymbolicBit::And(Rc::new(self), Rc::new(rhs)) - } -} - -impl std::ops::BitOr for SymbolicBit { - type Output = Self; - - fn bitor(self, rhs: Self) -> Self::Output { - !(!self & !rhs) - } -} - -impl std::ops::BitXor for SymbolicBit { - type Output = Self; - - fn bitxor(self, rhs: Self) -> Self::Output { - (self.clone() & !rhs.clone()) | (!self & rhs) - } -} - #[derive(Debug, Clone)] pub struct SymbolicBitVec { bits: VecDeque,