Reorganize sym.rs into bit.rs and vec.rs

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<Self>),
+
+    /// 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<Self>, Rc<Self>),
+}
+
+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)
+    }
+}

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<bool> for SymbolicBit {
     fn from(value: bool) -> Self {
@@ -210,7 +220,7 @@ impl FromIterator<u8> for SymbolicBitVec {
 
 pub fn symbolize(iter: impl IntoIterator<Item = u8>) -> impl Iterator<Item = SymbolicBit> {
     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);

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;

crates/sym/src/sym.rs → 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<Self>),
-
-    /// 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<Self>, Rc<Self>),
-}
-
-#[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<SymbolicBit>,