Added README.md to symbit crate and supporting changes

crates/sym/Cargo.toml

@@ -13,5 +13,9 @@ rust-version.workspace = true
 
 [dependencies]
 thiserror.workspace = true
-pcode-ops = { path = "../pcode-ops/" }
-aiger-circuit = "1"
+aiger-circuit = { version = "1", optional = true }
+
+[features]
+
+# Enables integration with aiger-circuit for generating AIGER formatted circuit
+aiger = ["dep:aiger-circuit"]

crates/sym/README.md

@@ -0,0 +1,57 @@
+# Overview
+
+A symbolic bitvectors[^bitvec] library for use with theorem provers and other binary analysis tools. Supported operations include:
+
+* Bitwise arithmetic (`&`, `|`, `^`, `!`)
+* Bit manipulation (`<<`, `>>`, extension, truncation)
+* Bit segmentation (split, join)
+* Integer arithmetic (`+`, `-`, `×`, `÷`)
+* Integer comparison (`<`, `>`, `=`, `≠`, `≤`, `≥`)
+
+## Example
+
+```rust
+# use symbit::{Evaluator, SymbolicBitVec};
+# fn f() -> Option<()> {
+// Create 32-bit symbolic bitvecs. Each bit is an independent variable.
+let x = SymbolicBitVec::with_size(32);
+let y = SymbolicBitVec::with_size(32);
+
+// Compute the (symbolic) product of x and y.
+let z = x.clone() * y.clone();
+
+// Create an evaluator assuming both x and y are negative.
+// This means their most-significant bits (msb) are 1 (true).
+let x_msb = x.msb()?.maybe_variable()?;
+let y_msb = y.msb()?.maybe_variable()?;
+let eval = Evaluator::new([(x_msb, true), (y_msb, true)]);
+
+// If x and y are negative then z should be positive (msb = 0)
+let e = eval.evaluate(z.msb()?);
+assert_eq!(e.response, Some(false));
+
+// Only the msb from x and y were used in this determination
+assert_eq!(e.used_variables.len(), 2);
+
+// The least significant bit (lsb) of the product is a variable.
+let e = eval.evaluate(z.lsb()?);
+assert!(e.response.is_none());
+
+// The product lsb is dependent only on the lsb of x and y.
+let x_lsb = x.lsb()?.maybe_variable()?;
+let y_lsb = x.lsb()?.maybe_variable()?;
+assert_eq!(e.unassigned_variables.len(), 2);
+assert!(e.unassigned_variables.contains(&x_lsb));
+assert!(e.unassigned_variables.contains(&y_lsb));
+# Some(())
+# }
+```
+
+
+# Features
+
+## `aiger`
+
+AIGER is a standardized format for an and-inverter gate circuit. The `aiger` feature can be used to enable integration with the [aiger-circuit](https://crates.io/crates/aiger-circuit) crate for converting constraints on outputs into an AIGER formatted circuit.
+
+[^bitvec]: A bitvector is a fixed sized number of bits that models the semantics of signed and unsigned two's complement arithmetic.

crates/sym/src/aiger.rs

@@ -0,0 +1,27 @@
+use std::rc::Rc;
+
+use aiger_circuit::circuit::{AigerCircuit, AndOperand, AsAigerCircuit};
+
+use crate::bit::SymbolicBit;
+
+impl<'a> AsAigerCircuit<'a> for SymbolicBit {
+    type Inner = Self;
+
+    fn as_aiger_circuit(&'a self) -> AigerCircuit<'a, Self::Inner> {
+        match self {
+            SymbolicBit::Literal(value) => AigerCircuit::Literal(*value),
+            SymbolicBit::Variable(id) => AigerCircuit::Variable(*id),
+            SymbolicBit::Not(x) => AigerCircuit::Not(x.as_ref()),
+            SymbolicBit::And(x, y) => AigerCircuit::And(
+                AndOperand {
+                    id: Rc::as_ptr(x) as usize,
+                    value: x.as_ref(),
+                },
+                AndOperand {
+                    id: Rc::as_ptr(y) as usize,
+                    value: y.as_ref(),
+                },
+            ),
+        }
+    }
+}

crates/sym/src/bit.rs

@@ -23,6 +23,20 @@ pub enum SymbolicBit {
 }
 
 impl SymbolicBit {
+    pub fn maybe_literal(&self) -> Option<bool> {
+        match self {
+            Self::Literal(b) => Some(*b),
+            _ => None,
+        }
+    }
+
+    pub fn maybe_variable(&self) -> Option<usize> {
+        match self {
+            Self::Variable(id) => Some(*id),
+            _ => None,
+        }
+    }
+
     pub fn equals(self, rhs: Self) -> Self {
         (self.clone() & rhs.clone()) | (!self & !rhs)
     }

crates/sym/src/convert.rs

@@ -1,7 +1,3 @@
-use std::rc::Rc;
-
-use aiger_circuit::circuit::{AigerCircuit, AndOperand, AsAigerCircuit};
-
 use crate::bit::{FALSE, SymbolicBit};
 use crate::buf::{SymbolicBitBuf, SymbolicByte};
 use crate::vec::SymbolicBitVec;
@@ -348,25 +344,3 @@ impl_little_endian!(u64);
 impl_little_endian!(u32);
 impl_little_endian!(u16);
 impl_little_endian!(u8);
-
-impl<'a> AsAigerCircuit<'a> for SymbolicBit {
-    type Inner = Self;
-
-    fn as_aiger_circuit(&'a self) -> AigerCircuit<'a, Self::Inner> {
-        match self {
-            SymbolicBit::Literal(value) => AigerCircuit::Literal(*value),
-            SymbolicBit::Variable(id) => AigerCircuit::Variable(*id),
-            SymbolicBit::Not(x) => AigerCircuit::Not(x.as_ref()),
-            SymbolicBit::And(x, y) => AigerCircuit::And(
-                AndOperand {
-                    id: Rc::as_ptr(x) as usize,
-                    value: x.as_ref(),
-                },
-                AndOperand {
-                    id: Rc::as_ptr(y) as usize,
-                    value: y.as_ref(),
-                },
-            ),
-        }
-    }
-}

crates/sym/src/eval.rs

@@ -25,8 +25,10 @@ pub struct Evaluation {
 impl Evaluator {
     /// Create a new instance using the given [VariableAssignments]. The assignments are fixed for
     /// the lifetime of this evaluator.
-    pub fn new(assignments: VariableAssignments) -> Self {
-        Self { assignments }
+    pub fn new(assignments: impl Into<VariableAssignments>) -> Self {
+        Self {
+            assignments: assignments.into(),
+        }
     }
 
     pub fn evaluate(&self, bit: &SymbolicBit) -> Evaluation {
@@ -129,6 +131,12 @@ impl VariableAssignments {
     }
 }
 
+impl<I: IntoIterator<Item = (usize, bool)>> From<I> for VariableAssignments {
+    fn from(iter: I) -> Self {
+        iter.into_iter().collect()
+    }
+}
+
 impl FromIterator<(usize, bool)> for VariableAssignments {
     fn from_iter<T: IntoIterator<Item = (usize, bool)>>(iter: T) -> Self {
         Self {

crates/sym/src/lib.rs

@@ -1,3 +1,5 @@
+#![doc=include_str!("../README.md")]
+
 mod bit;
 mod buf;
 mod convert;
@@ -13,5 +15,8 @@ pub use crate::convert::concretize_into;
 pub use crate::eval::*;
 pub use crate::vec::*;
 
+#[cfg(feature = "aiger")]
+mod aiger;
+
 #[cfg(test)]
 mod tests;

crates/sym/src/vec.rs

@@ -23,6 +23,10 @@ impl SymbolicBitVec {
         self.bits.back()
     }
 
+    pub fn lsb(&self) -> Option<&SymbolicBit> {
+        self.bits.front()
+    }
+
     pub fn is_empty(&self) -> bool {
         self.bits.is_empty()
     }

crates/sym/src/vec/ops.rs

@@ -171,7 +171,7 @@ impl std::ops::Mul for SymbolicBitVec {
 
     fn mul(self, rhs: Self) -> Self::Output {
         // The output size is the sum of the number of bits. Clippy is overly zealous here flagging
-        // the addition as erroneous.
+        // the addition as erroneous. https://github.com/rust-lang/rust-clippy/issues/16247
         #[allow(clippy::suspicious_arithmetic_impl)]
         let output_size = self.len() + rhs.len();
 

crates/sympcode/Cargo.toml

@@ -8,5 +8,5 @@ repository.workspace = true
 rust-version.workspace = true
 
 [dependencies]
-symbit = { version = "0.1", path = "../sym" }
+symbit = { version = "0.1", path = "../sym", features = ["aiger"] }
 pcode-ops = { version = "0.1", path = "../pcode-ops/" }