Merge pull request #23 from cucapra/crate-publish

Crate publish

Author: Modertool999

.github/workflows/diff-test.yml

@@ -26,7 +26,7 @@ jobs:
         run: uv tool install turnt
 
       - name: Build Rust implementation
-        run: cargo build
+        run: cargo build --features cli --bin raig
 
       - name: Install C AIGER
         run: |

.github/workflows/snapshot-test.yml

@@ -38,7 +38,7 @@ jobs:
         run: cargo test --all
 
       - name: Build debug binary
-        run: cargo build
+        run: cargo build --features cli --bin raig
 
       - name: Run AIGER snapshot tests
         run: turnt -e raw -e opt tests/inputs/*.aag

Cargo.lock

@@ -1,8 +1,30 @@
 [package]
-name = "aig"
+name = "raig"
 version = "0.1.0"
+authors = ["Modi Goldstein-Rosenfeld <mbg237@cornell.edu>", "Adrian Sampson <asampson@cs.cornell.edu>", "Kevin Laeufer <laeufer@cornell.edu>"]
 edition = "2024"
+rust-version = "1.85"
+description = "A library for boolean logic verification using And-Inverter Graphs (AIGs)"
+documentation = "https://docs.rs/raig"
+repository = "https://github.com/cucapra/aig"
+license = "MIT"
+keywords = ["aig", "aiger", "logic", "verification", "boolean"]
+categories = ["data-structures", "development-tools::testing", "parsing", "simulation"]
+include = [
+    "/Cargo.toml",
+    "/LICENSE",
+    "/README.md",
+    "/src/**",
+]
 
-[dependencies]
-clap = { version = "4.6.1", features = ["derive"] }
+[features]
+default = []
+cli = ["dep:clap"]
+
+[[bin]]
+name = "raig"
+path = "src/main.rs"
+required-features = ["cli"]
 
+[dependencies]
+clap = { version = "4.6.1", features = ["derive"], optional = true }

Cargo.toml

@@ -0,0 +1,21 @@
+MIT License
+
+Copyright (c) 2026 Modi Goldstein-Rosenfeld, Adrian Sampson, and Kevin Laeufer
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all
+copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+SOFTWARE.

LICENSE

@@ -1,222 +1,30 @@
-# AIG in Rust (last updated: 6/22/26)
+# raig
 
-And-Inverter Graphs (AIGs) implemented in Rust for formal verification and circuit synthesis.
+`raig` (pronounced “rage”) is a dependency-free library for working with
+<a href="https://en.wikipedia.org/wiki/And-inverter_graph" target="_blank" rel="noopener noreferrer">And-Inverter Graphs (AIGs)</a>
+in Rust, developed at
+<a href="https://capra.cs.cornell.edu/" target="_blank" rel="noopener noreferrer">Cornell's Capra Lab</a>.
 
-## Overview
+An AIG represents Boolean logic with AND gates and inverted edges. This compact
+form is useful for logic verification, synthesis, and testing tools.
 
-An And-Inverter Graph (AIG) is a data structure used to represent Boolean logic circuits. Since any Boolean circuit can be represented using only `AND` and `NOT`, an AIG represents nodes as `AND` gates and edges as either regular or inverted connections
+The library has no default dependencies. The optional `cli` feature enables the
+`raig` command-line tool and its `clap` dependency.
 
+## Installation
 
-## Internal Representation
+Add the library to a Rust project:
 
-The graph stores AIG nodes in a `Vec<AigNode>`:
-
-```rust
-pub struct AigGraph {
-    nodes: Vec<AigNode>,
-}
-```
-
-AND nodes store two child `NodeId: u32`s:
-
-```rust
-AigNode {
-    left: NodeId,
-    right: NodeId,
-}
-```
-
-Each child `NodeId` can refer to a constant, an input, an AND node, or an inverted version of any of those. This means NOT gates are not stored as separate nodes. Instead, inversion is represented directly on the `NodeId`.
-
-```rust
-pub struct AigNode {
-    left: NodeId,
-    right: NodeId,
-}
-``` 
-
-The least significant bit of a `NodeId` is used as the inversion bit:
-
-```text
-even NodeId = regular signal
-odd NodeId  = inverted signal
-```
-
-So inverting a `NodeId` just toggles the last bit.
-
-```text
-a = NodeId(2);
-!a = NodeId(3);
-b = NodeId(4);
-!b = NodeId(5);
-```
-
-Constants are represented directly as special reserved `NodeId` values:
-
-```rust
-impl NodeId {
-    pub const FALSE: NodeId = NodeId(0);
-    pub const TRUE: NodeId = NodeId(1);
-}
-```
-
-This works because `NodeId(1)` is just `NodeId(0)` with the inversion bit set:
-
-```text
-NodeId(0) = false
-NodeId(1) = !false = true
-```
-
-Constants are not stored as nodes in the graph vector. Real graph nodes start at `NodeId(2)` since `NodeId(0)` and `NodeId(1)` are reserved for the constants `true` and `false`:
-
-```text
-graph[0] -> NodeId(2)
-graph[1] -> NodeId(4)
-graph[2] -> NodeId(6)
-```
-
-Their inverted versions are represented by setting the least significant bit:
-
-```text
-NodeId(2) = graph[0]
-NodeId(3) = !graph[0]
-
-NodeId(4) = graph[1]
-NodeId(5) = !graph[1]
-
-NodeId(6) = graph[2]
-NodeId(7) = !graph[2]
-```
-
-Inputs are stored as `NodeId`s and are represented by setting both child fields to a special marker value:
-
-```rust
-const INPUT_NODE_MARKER: NodeId = NodeId(NODE_ID_MASK);
-```
-
-`NODE_ID_MASK` is all `1`s except for the least significant inversion bit:
-
-```text
-NODE_ID_MASK = 11111111111111111111111111111110
-```
-
-So the input marker is:
-
-```text
-INPUT_NODE_MARKER = NodeId(11111111111111111111111111111110)
-```
-
-For example, an input node is stored like this:
-
-```rust
-AigNode {
-    left: INPUT_NODE_MARKER,
-    right: INPUT_NODE_MARKER,
-}
-```
-
-While multiple inputs contain the same internal marker data, but they are still different inputs because they have different `NodeId`s:
-
-```text
-graph[0] = input node -> NodeId(2)
-graph[1] = input node -> NodeId(4)
-graph[2] = input node -> NodeId(6)
-```
-
-Latches are also stored as graph nodes. They are recognized by setting the left child to the same marker and storing the latch input, or next-state signal, in the right child:
-
-```rust
-AigNode {
-    left: INPUT_NODE_MARKER,
-    right: next_state,
-}
-```
-
-This lets latch state variables have stable `NodeId`s like inputs and AND nodes, while the right side points to the signal that drives the latch on the next step.
-
-
-
-
-
-## AIGER Input Support
-
-The parser supports both ASCII `.aag` files and binary `.aig` files.
-
-ASCII AIGER files begin with a header of the form:
-
-```text
-aag M I L O A
-```
-
-Binary AIGER files use the same counts with an `aig` header:
-
-```text
-aig M I L O A
-```
-
-where:
-
-```text
-M = maximum variable index
-I = number of inputs
-L = number of latches
-O = number of outputs
-A = number of AND gates
+```sh
+cargo add raig
 ```
 
-The header must satisfy:
+Install the command-line tool:
 
-```text
-M >= I + L + A
+```sh
+cargo install raig --features cli
 ```
 
-Latch lines are supported in the ASCII parser:
-
-```text
-<latch literal> <next-state literal> [reset]
-```
-
-The optional reset field is currently accepted only when it is `0`, because reset values are not represented in `AigNode`.
-
-In binary AIGER, input literals and latch current-state literals are implicit. The parser reads one next-state literal per latch, one output literal per output, then decodes each AND gate from its binary delta encoding. Binary files must satisfy:
-
-```text
-M = I + L + A
-```
-
-The parser is split by responsibility:
-
-```text
-src/aiger_parser.rs         = header parsing, format validation, dispatch
-src/aiger_ascii_parser.rs   = ASCII body parsing
-src/aiger_binary_parser.rs  = binary body parsing
-```
-
-## Parsing an AIGER File
-
-To parse an AIGER file, use:
-
-```rust
-run_parser_with_options(file_name: &str, pre_optimize: bool) -> io::Result<()>
-```
-
-Example:
-
-```rust
-run_parser_with_options("example.aag", true)?;
-run_parser_with_options("example.aig", true)?;
-```
-
-The `pre_optimize` option controls whether the parser performs simple on-the-fly optimizations while building the graph.
-
-If `pre_optimize` is `true`, the parser simplifies expressions before inserting new AND nodes. For example:
-
-```text
-x & false = false
-x & true  = x
-x & x     = x
-x & !x    = false
-...
-```
+## License
 
-If `pre_optimize` is `false`, the parser builds the graph directly from the AIGER file without applying these simplifications.
+Licensed under the MIT license.