Enable additional SymbolicBit reductions

.github/workflows/rust.yml

@@ -16,7 +16,7 @@ jobs:
       matrix:
         toolchain:
           - "stable"
-          - "1.87" # MSRV
+          - "1.88" # MSRV
 
     steps:
     - uses: actions/checkout@v3

crates/sym/src/sym.rs

@@ -43,6 +43,50 @@ impl SymbolicBit {
     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 {
@@ -68,27 +112,21 @@ 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::Variable(x) => match rhs {
-                SymbolicBit::Not(y) if *y == SymbolicBit::Variable(x) => {
-                    return SymbolicBit::Literal(false);
-                }
-                _ => (),
-            },
+            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::Variable(x) => match self {
-                SymbolicBit::Not(y) if *y == SymbolicBit::Variable(x) => {
-                    return SymbolicBit::Literal(false);
-                }
-                _ => (),
-            },
+            SymbolicBit::Not(z) if z.is_identical(&self) => return SymbolicBit::Literal(false),
             _ => (),
         }
 

crates/sym/src/tests/bit.rs

@@ -63,14 +63,28 @@ fn disjunction_with_true() {
 }
 
 #[test]
-fn exclusive_or_with_self() {
+fn exclusive_or_with_same_variable() {
     let x = SymbolicBit::Variable(0);
     assert_eq!(x.clone() ^ x.clone(), SymbolicBit::Literal(false));
 }
 
+#[test]
+fn exclusive_or_with_complex_self() {
+    let x = complex_bit();
+    assert_eq!(x.clone() ^ x.clone(), SymbolicBit::Literal(false));
+}
+
 #[test]
 fn exclusive_or_with_zero() {
     let x = SymbolicBit::Variable(0);
     assert_eq!(x.clone() ^ SymbolicBit::Literal(false), x);
     assert_eq!(SymbolicBit::Literal(false) ^ x.clone(), x);
 }
+
+fn complex_bit() -> SymbolicBit {
+    let mut bit = SymbolicBit::Literal(true);
+    for i in 0..5 {
+        bit = SymbolicBit::Variable(i) & bit;
+    }
+    bit
+}