diff --git a/AGENTS.md b/AGENTS.md index 5c6ae541..68b0828d 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -19,6 +19,7 @@ - Exact SAT-based local placer, survey, and construct/compact pipeline: `docs/exact_local_placer.md` - Full-adder tiles that chain into n-bit ripple-carry adders (`CarryTiling`): `docs/carry_tiles.md` - Critical paths in redstone ticks: static timing, delay bounds, and timing-first construction and compaction: `docs/timing_driven_placement.md` +- Equivalent NOR netlists from an e-graph (egg) with exact SAT extraction: `docs/egraph_netlists.md` - Solver modeling DSL (rsdsl v2, crate `crates/rsdsl`): design and parity measurements `docs/solver_dsl_design.md`; grammar and language spec `docs/solver_dsl_grammar.md`; the exact placer's model is `src/transform/place_and_route/local_placer/exact/exact_placer.rsdsl` (grounded by `exact/dsl.rs`) When asked to create or preserve project documentation, add an appropriate file under `docs/` and link it from this file when it is useful for future agents. diff --git a/Cargo.lock b/Cargo.lock index 533acd1b..5e783232 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -8,6 +8,17 @@ version = "1.0.2" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "f26201604c87b1e01bd3d98f8d5d9a8fcbb815e8cedb41ffccbeb4bf593a35fe" +[[package]] +name = "ahash" +version = "0.7.8" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "891477e0c6a8957309ee5c45a6368af3ae14bb510732d2684ffa19af310920f9" +dependencies = [ + "getrandom", + "once_cell", + "version_check", +] + [[package]] name = "ansi_term" version = "0.12.1" @@ -221,6 +232,24 @@ dependencies = [ "syn 2.0.87", ] +[[package]] +name = "egg" +version = "0.9.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "96beaf9d35dbc4686bc86a4ecb851fd6a406f0bf32d9f646b1225a5c5cf5b5d7" +dependencies = [ + "env_logger", + "fxhash", + "hashbrown 0.12.3", + "indexmap 1.9.3", + "instant", + "log", + "smallvec", + "symbol_table", + "symbolic_expressions", + "thiserror 1.0.69", +] + [[package]] name = "either" version = "1.8.1" @@ -233,6 +262,15 @@ version = "1.0.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "34aa73646ffb006b8f5147f3dc182bd4bcb190227ce861fc4a4844bf8e3cb2c0" +[[package]] +name = "env_logger" +version = "0.9.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a12e6657c4c97ebab115a42dcee77225f7f482cdd841cf7088c657a42e9e00e7" +dependencies = [ + "log", +] + [[package]] name = "equivalent" version = "1.0.1" @@ -294,6 +332,15 @@ dependencies = [ "miniz_oxide", ] +[[package]] +name = "fxhash" +version = "0.2.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c31b6d751ae2c7f11320402d34e41349dd1016f8d5d45e48c4312bc8625af50c" +dependencies = [ + "byteorder", +] + [[package]] name = "getrandom" version = "0.2.15" @@ -312,6 +359,9 @@ name = "hashbrown" version = "0.12.3" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "8a9ee70c43aaf417c914396645a0fa852624801b24ebb7ae78fe8272889ac888" +dependencies = [ + "ahash", +] [[package]] name = "hashbrown" @@ -397,6 +447,15 @@ dependencies = [ "web-time", ] +[[package]] +name = "instant" +version = "0.1.13" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e0242819d153cba4b4b05a5a8f2a7e9bbf97b6055b2a002b395c96b5ff3c0222" +dependencies = [ + "cfg-if", +] + [[package]] name = "itertools" version = "0.11.0" @@ -732,6 +791,7 @@ dependencies = [ "cadical", "derive_more", "disjoint-set", + "egg", "eyre", "fastanvil", "fastnbt", @@ -908,6 +968,22 @@ dependencies = [ "syn 2.0.87", ] +[[package]] +name = "symbol_table" +version = "0.2.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "32bf088d1d7df2b2b6711b06da3471bc86677383c57b27251e18c56df8deac14" +dependencies = [ + "ahash", + "hashbrown 0.12.3", +] + +[[package]] +name = "symbolic_expressions" +version = "5.0.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7c68d531d83ec6c531150584c42a4290911964d5f0d79132b193b67252a23b71" + [[package]] name = "syn" version = "1.0.109" @@ -939,13 +1015,33 @@ dependencies = [ "unicode-width 0.1.10", ] +[[package]] +name = "thiserror" +version = "1.0.69" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b6aaf5339b578ea85b50e080feb250a3e8ae8cfcdff9a461c9ec2904bc923f52" +dependencies = [ + "thiserror-impl 1.0.69", +] + [[package]] name = "thiserror" version = "2.0.18" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "4288b5bcbc7920c07a1149a35cf9590a2aa808e0bc1eafaade0b80947865fbc4" dependencies = [ - "thiserror-impl", + "thiserror-impl 2.0.18", +] + +[[package]] +name = "thiserror-impl" +version = "1.0.69" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "4fee6c4efc90059e10f81e6d42c60a18f76588c3d74cb83a0b242a2b6c7504c1" +dependencies = [ + "proc-macro2", + "quote", + "syn 2.0.87", ] [[package]] @@ -1298,7 +1394,7 @@ dependencies = [ "flate2", "indexmap 2.0.0", "memchr", - "thiserror", + "thiserror 2.0.18", "zopfli", ] diff --git a/Cargo.toml b/Cargo.toml index 447389f8..dd791783 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -35,6 +35,7 @@ tracing-subscriber = "0.3.17" flate2 = "1.0.26" serde = "1.0.183" zip = { version = "2.2", default-features = false, features = ["deflate"] } +egg = "0.9" [target.'cfg(not(target_arch = "wasm32"))'.dependencies] mimalloc = "0.1.43" diff --git a/docs/egraph_netlists.md b/docs/egraph_netlists.md new file mode 100644 index 00000000..b9d3263d --- /dev/null +++ b/docs/egraph_netlists.md @@ -0,0 +1,166 @@ +# Equivalent NOR netlists from an e-graph (2026-10-05) + +The exact placer builds the NOR netlist it is given. Construction places one +gate per step, and the signal vocabulary is the netlist's net functions and +their complements. A hand-written netlist such as the full adder's `nor9` +therefore fixes how many torches there are and how deep the logic runs. +`exact/egraph.rs` searches the equivalent netlists with an e-graph (the `egg` +crate) and extracts the ones worth placing. + +## Saturation + +The language has `~`, `|`, `&`, `^`, and inputs. Only `~` (a torch: one gate, +one redstone tick) and `|` (dust and blocks: free) are built; `&` and `^` +state functions and give the rewrites something to pass through. + +The rules are: + +- commutativity and associativity; +- double negation, idempotence, and absorption; +- De Morgan in both directions; +- AND over OR and OR over AND, both ways; +- XOR as a sum of products and as a product of sums; +- XNOR as XOR with one input negated. + +The analysis gives every e-class its truth table (up to 6 inputs). `modify` +unions any two classes with the same table as soon as the second appears. +Two forms of one function thus always meet, whichever rules produced them, +and the classes are the functions the rules have reached. + +The full adder (`s = a^b^cin`, `cout = ab|a·cin|b·cin`) reaches 230 of the +256 three-input functions: 6,187 nodes, 12 iterations, 73 ms. + +## Extraction + +**Greedy extraction** (`Exploration::extract`) gives each class the node +whose own and inputs' gates (shared ones counted once) and depth weigh +least, until no class changes. It decides class by class, so it misses +NORs that pay off only when several gates share them. On the full adder +every weighting gave the same 13-gate netlist, against `nor9`'s 9. + +**Exact extraction** (`Exploration::extract_exact`) solves the choice with +SAT, from a second rsdsl model, `exact/egraph_extract.rsdsl`: + +- the outputs are needed and are torches (an OR output would become a NOR + and a NOT in the netlist); +- a needed class picks one node, and the classes that node reads are needed + too; +- `Depth` adds a tick per NOT and none per OR, which also rules out loops; + `max_depth` bounds the outputs; +- the objective is the number of picked NOTs, plus `or_cost` per picked + OR (every input of a NOR is a signal to route to its block); +- `binary` allows only NORs of two signals. + +The same CaDiCaL binding as the placer lowers the bound until the minimum +is proven. On the full adder each depth bound took 0.1-0.4 s: + +| Depth bound | Fewest gates (proven) | Depths cout / s | Most nets live at once | +| --- | --- | --- | --- | +| 2 | none | | | +| 3 | 9 | 2 / 3 | 7 | +| 4 and up | 8 | 3 / 4 | 6 | +| `nor9` (by hand) | 9 | 5 / 6 | 4 | + +The 8-gate full adder: + +``` +g3 = NOR(a, b) +g4 = NOR(a, cin, g3) +g5 = NOR(b, cin, g3) +g6 = NOR(a, g3, g4, g5) +g7 = NOR(b, g3, g4, g5) +g8 = NOR(cin, g4, g5) +s = NOR(g6, g7, g8) +cout = NOR(g3, g4, g5) +``` + +With `or_cost` 1 or more, the cheapest netlist has 9 gates and depths 4/5, +one tick faster than `nor9`. Its widest NOR reads 3 signals, and as with +`nor9` at most 4 nets are alive at once: + +``` +g3 = NOR(a, b) +g4 = NOR(a) +g5 = NOR(b) +g6 = NOR(g4, g5) +g7 = NOR(cin, g3, g6) +g8 = NOR(g3, g6, g7) +g9 = NOR(cin, g7) +s = NOR(g8, g9) +cout = NOR(g3, g7) +``` + +With `binary` (two-input NORs only), the minimum is 9 gates at depth 5/6: +`nor9` itself, proven optimal for this e-graph. Depth 5/5 needs 12 gates, +and nothing reaches depth 4. Every gain the e-graph finds over `nor9` uses +wider NORs. + +The minimum holds within this e-graph. A netlist the rules never reach can +still be smaller. + +## Placement + +The circuit harness places the extracted netlists: + +- `CIRCUIT=egraph-full-adder` uses the fewest gates overall; +- `EGRAPH_DEPTH=` uses the fewest gates within depth `n`; +- `EGRAPH_OR_COST=` charges each OR node `w`; +- `EGRAPH_BINARY=1` allows only two-input NORs. + +Full adder, 5 workers, 600 s of compaction, no timing: + +| Netlist | Seed | Construction | Compacted | +| --- | --- | --- | --- | +| `nor9`, fan-in 2 | 1 | 64 s | 2x12x9, 146 blocks, cout 13, s 18 | +| `nor9` | 2 | 96 s | 2x11x10, 148 blocks, cout 11, s 17 | +| `or_cost` 1, 9 gates, fan-in 3 | 1 | 995 s, 3 restarts | 2x15x7, 121 blocks, cout 12, s 19 | +| `or_cost` 1 | 2 | 937 s, 4 restarts | 2x11x9, 88 blocks, cout 7, s 11 | +| 8 gates, fan-in 4 | 1 | no layout in 3 restarts | | +| depth 3, 9 gates, fan-in 4 | 1 | no layout in 5 restarts | | + +- Construction is where wide NORs cost. + - Steps with a 3- or 4-input NOR ran out of their 60 s again and again: + `g4 = NOR(a, cin, g3)`, `cout = NOR(g4, g5, g7)`, and the `or_cost` 1 + netlist's `g7 = NOR(cin, g3, g6)`. + - Every input of such a NOR has to reach one block within a window two + cells wide. + - `nor9`'s two-input NORs construct on the first try in 1-1.5 minutes. +- Once built, the `or_cost` 1 netlist gave the smallest and fastest cell + of these runs (seed 2: 88 blocks, 11 ticks). +- Compaction varies too much from run to run (the 600 s runs did not + converge) to rank the netlists on two seeds. + +Two placement steps had failed as infeasible within 0.1 s, the first time +a new input was placed. Construction offered the new input the cell of a +switch kept from an earlier step, and the fixed switch was read as the new +input's. That is fixed: new inputs skip placed switches, and a fixed +switch belongs to the input whose only site it is. With +`EXACT_DIAGNOSE_INFEASIBLE`, an infeasible step is re-solved with one +requirement dropped at a time, which is how it was found. + +## Next + +- Let construction build a wide NOR in parts, its OR terms first, so + narrow windows can place the netlists with fewer gates. +- Constrain extraction for carry tiles: the carry needs monotone signals + (`carry_tiles.md`). + +## Running + +```sh +cargo test --release --lib egraph_netlists_compute_the_full_adder +cargo test --release --lib explore_egraph_netlists -- --ignored --nocapture +CIRCUIT=egraph-full-adder CIRCUIT_COMPACT_SECONDS=600 \ + cargo test --release --lib diagnose_construct_circuit -- --ignored --nocapture +``` + +`explore_egraph_netlists` takes these knobs: + +- saturation: `EGRAPH_ITERATIONS`, `EGRAPH_NODES`, `EGRAPH_SECONDS`; +- the sweep: `EGRAPH_MAX_DEPTH`, `EGRAPH_OR_COSTS` (comma-separated), + `EGRAPH_BINARY=1`; +- `EGRAPH_EXTRACT_SECONDS`; +- `EGRAPH_GREEDY=1` also prints greedy extractions. + +The circuit harness takes `EGRAPH_DEPTH`, `EGRAPH_OR_COST`, and +`EGRAPH_BINARY`. diff --git a/src/transform/place_and_route/local_placer/exact/egraph.rs b/src/transform/place_and_route/local_placer/exact/egraph.rs new file mode 100644 index 00000000..dfa0d9ca --- /dev/null +++ b/src/transform/place_and_route/local_placer/exact/egraph.rs @@ -0,0 +1,718 @@ +//! Equivalent NOR netlists from an e-graph (egg). +//! +//! A hand-written netlist (`nor9`, say) fixes which gates the placer builds. +//! Equality saturation explores other expressions of the same functions: De +//! Morgan, double negation, commutativity and associativity, distribution and +//! factoring, absorption, and XOR expansions. Every e-class carries its truth +//! table, and classes with the same table are merged as soon as they appear, +//! so two forms of one function always meet, whichever rules produced them. +//! +//! Extraction then picks NOR netlists in the placer's terms. A NOT is a torch +//! (one gate and one redstone tick), an OR is free (dust and blocks), and a +//! shared subterm is built once. `Weights` trade gates against depth, so a few +//! weightings give a small set of distinct netlists to place. + +use std::collections::{BTreeMap, BTreeSet, HashMap}; +use std::sync::atomic::AtomicBool; +use std::sync::OnceLock; +use std::time::{Duration, Instant}; + +use egg::{ + define_language, rewrite as rw, Analysis, DidMerge, EGraph, Id, RecExpr, Rewrite, Runner, + StopReason, Symbol, +}; +use eyre::{bail, ensure, eyre}; +use rsdsl::{GroundOptions, IValue, Instance, Model}; + +use super::cnf::Cnf; +use super::netlist::{Net, NetDriver, NetId, NorNetlist}; +use super::solver::{SatSolver, SolveResult, StopSignal}; + +const EXTRACT_SOURCE: &str = include_str!("egraph_extract.rsdsl"); + +fn extract_model() -> &'static Model { + static MODEL: OnceLock = OnceLock::new(); + MODEL.get_or_init(|| { + Model::parse("egraph_extract.rsdsl", EXTRACT_SOURCE) + .unwrap_or_else(|error| panic!("{error}")) + }) +} + +/// What `Exploration::extract_exact` minimizes, and within what. +#[derive(Debug, Clone, Copy)] +pub struct ExtractOptions { + /// Gates on the slowest path to an output, at most. + pub max_depth: Option, + /// Weight of each OR node (one more input on a NOR) against a gate's 1. + pub or_cost: usize, + /// Only NORs of at most two signals. + pub binary: bool, + pub time_limit: Duration, +} + +impl Default for ExtractOptions { + fn default() -> Self { + Self { + max_depth: None, + or_cost: 0, + binary: false, + time_limit: Duration::from_secs(60), + } + } +} + +/// A netlist picked by `Exploration::extract_exact`. +#[derive(Debug, Clone)] +pub struct Extraction { + pub netlist: NorNetlist, + /// The minimized cost: gates, plus `or_cost` per OR node. + pub cost: usize, + /// No netlist in the e-graph within the depth costs less. + pub proven: bool, +} + +define_language! { + /// Boolean expressions over named inputs. Only `~` and `|` are built: a + /// NOT is a torch, an OR is dust and blocks. `&` and `^` state functions + /// and give the rewrites something to go through. + pub enum Bool { + "~" = Not(Id), + "|" = Or([Id; 2]), + "&" = And([Id; 2]), + "^" = Xor([Id; 2]), + Var(Symbol), + } +} + +/// The truth table of every e-class: bit `k` is the value in input case `k`, +/// where bit `i` of `k` is input `i`. Classes with the same table are merged. +#[derive(Debug, Clone, Default)] +pub struct TruthTable { + inputs: Vec, + full: u64, + by_table: HashMap, +} + +impl TruthTable { + fn new(inputs: &[&str]) -> eyre::Result { + ensure!(inputs.len() <= 6, "truth tables hold at most 6 inputs"); + let cases = 1u32 << inputs.len(); + Ok(Self { + inputs: inputs.iter().map(|&name| Symbol::from(name)).collect(), + full: if cases == 64 { + u64::MAX + } else { + (1u64 << cases) - 1 + }, + by_table: HashMap::new(), + }) + } + + fn input(&self, symbol: Symbol) -> u64 { + let index = self + .inputs + .iter() + .position(|&input| input == symbol) + .unwrap_or_else(|| panic!("unknown input {symbol}")); + (0..self.full.count_ones()) + .filter(|case| case & (1 << index) != 0) + .fold(0, |table, case| table | (1 << case)) + } +} + +impl Analysis for TruthTable { + type Data = u64; + + fn make(egraph: &EGraph, enode: &Bool) -> u64 { + let table = |id: &Id| egraph[*id].data; + let analysis = &egraph.analysis; + match enode { + Bool::Not(a) => !table(a) & analysis.full, + Bool::Or([a, b]) => table(a) | table(b), + Bool::And([a, b]) => table(a) & table(b), + Bool::Xor([a, b]) => table(a) ^ table(b), + Bool::Var(symbol) => analysis.input(*symbol), + } + } + + fn merge(&mut self, a: &mut u64, b: u64) -> DidMerge { + assert_eq!(*a, b, "merged e-classes compute different functions"); + DidMerge(false, false) + } + + fn modify(egraph: &mut EGraph, id: Id) { + let table = egraph[id].data; + match egraph.analysis.by_table.get(&table) { + Some(&other) => { + egraph.union(other, id); + } + None => { + egraph.analysis.by_table.insert(table, id); + } + } + } +} + +fn rules() -> Vec> { + let mut rules = vec![ + rw!("or-comm"; "(| ?a ?b)" => "(| ?b ?a)"), + rw!("and-comm"; "(& ?a ?b)" => "(& ?b ?a)"), + rw!("xor-comm"; "(^ ?a ?b)" => "(^ ?b ?a)"), + rw!("or-assoc"; "(| ?a (| ?b ?c))" => "(| (| ?a ?b) ?c)"), + rw!("and-assoc"; "(& ?a (& ?b ?c))" => "(& (& ?a ?b) ?c)"), + rw!("xor-assoc"; "(^ ?a (^ ?b ?c))" => "(^ (^ ?a ?b) ?c)"), + rw!("not-not"; "(~ (~ ?a))" => "?a"), + rw!("or-absorb"; "(| ?a (& ?a ?b))" => "?a"), + rw!("and-absorb"; "(& ?a (| ?a ?b))" => "?a"), + rw!("or-idem"; "(| ?a ?a)" => "?a"), + rw!("and-idem"; "(& ?a ?a)" => "?a"), + ]; + rules.extend(rw!("and-de-morgan"; "(& ?a ?b)" <=> "(~ (| (~ ?a) (~ ?b)))")); + rules.extend(rw!("or-de-morgan"; "(~ (| ?a ?b))" <=> "(& (~ ?a) (~ ?b))")); + rules.extend(rw!("and-over-or"; "(& ?a (| ?b ?c))" <=> "(| (& ?a ?b) (& ?a ?c))")); + rules.extend(rw!("or-over-and"; "(| ?a (& ?b ?c))" <=> "(& (| ?a ?b) (| ?a ?c))")); + rules.extend(rw!("xor-sop"; "(^ ?a ?b)" <=> "(| (& ?a (~ ?b)) (& (~ ?a) ?b))")); + rules.extend(rw!("xor-pos"; "(^ ?a ?b)" <=> "(& (| ?a ?b) (~ (& ?a ?b)))")); + rules.extend(rw!("xnor"; "(~ (^ ?a ?b))" <=> "(^ (~ ?a) ?b)")); + rules +} + +/// Limits of one saturation run. +#[derive(Debug, Clone, Copy)] +pub struct Limits { + pub iterations: usize, + pub nodes: usize, + pub time: std::time::Duration, +} + +impl Default for Limits { + fn default() -> Self { + Self { + iterations: 12, + nodes: 50_000, + time: std::time::Duration::from_secs(20), + } + } +} + +/// A saturated e-graph and its output classes. +pub struct Exploration { + egraph: EGraph, + inputs: Vec, + outputs: Vec<(String, Id)>, + pub iterations: usize, + pub stop_reason: Option, +} + +/// How to weigh an extracted netlist: torches and ticks on its slowest path. +#[derive(Debug, Clone, Copy)] +pub struct Weights { + pub gates: f64, + pub depth: f64, +} + +#[derive(Debug, Clone)] +struct Choice { + node: Bool, + gates: BTreeSet, + depth: usize, +} + +impl Exploration { + /// Saturates `outputs` (infix expressions over `inputs` with `~ & ^ |`) + /// within `limits`. + pub fn new(inputs: &[&str], outputs: &[(&str, &str)], limits: Limits) -> eyre::Result { + let mut egraph = EGraph::new(TruthTable::new(inputs)?); + let mut roots = Vec::new(); + for &(name, expression) in outputs { + let expression = parse(expression)?; + roots.push((name.to_owned(), egraph.add_expr(&expression))); + } + let runner = Runner::default() + .with_egraph(egraph) + .with_iter_limit(limits.iterations) + .with_node_limit(limits.nodes) + .with_time_limit(limits.time) + .run(&rules()); + let iterations = runner.iterations.len(); + let stop_reason = runner.stop_reason.clone(); + let egraph = runner.egraph; + let outputs = roots + .into_iter() + .map(|(name, id)| (name, egraph.find(id))) + .collect(); + Ok(Self { + egraph, + inputs: inputs.iter().map(|&name| name.to_owned()).collect(), + outputs, + iterations, + stop_reason, + }) + } + + pub fn classes(&self) -> usize { + self.egraph.number_of_classes() + } + + pub fn nodes(&self) -> usize { + self.egraph.total_number_of_nodes() + } + + /// The netlist with the least weighted cost, greedily: each class takes + /// the NOT, OR, or input node whose own and inputs' gates (shared ones + /// counted once) and depth weigh least, until no class changes. + pub fn extract(&self, weights: Weights) -> eyre::Result { + let egraph = &self.egraph; + let score = |choice: &Choice| { + weights.gates * choice.gates.len() as f64 + weights.depth * choice.depth as f64 + }; + let mut best = HashMap::::new(); + for _ in 0..256 { + let mut changed = false; + for class in egraph.classes() { + for node in &class.nodes { + let Some(candidate) = self.candidate(class.id, node, &best) else { + continue; + }; + let better = match best.get(&class.id) { + None => true, + Some(current) => { + let (new, old) = (score(&candidate), score(current)); + new < old - 1e-9 + || ((new - old).abs() <= 1e-9 + && (candidate.gates.len(), candidate.depth) + < (current.gates.len(), current.depth)) + } + }; + if better { + best.insert(class.id, candidate); + changed = true; + } + } + } + if !changed { + break; + } + } + self.netlist(&best) + } + + /// The netlist with the fewest NOT gates (plus `or_cost` per OR node) + /// whose outputs are at most `max_depth` gates deep, picked exactly by + /// SAT over the e-graph (`egraph_extract.rsdsl`): one node per needed + /// class, shared classes built once. Lowers the bound until it is proven + /// or `time_limit` runs out; `None` when no netlist of the e-graph fits. + pub fn extract_exact(&self, options: &ExtractOptions) -> eyre::Result> { + let ExtractOptions { + max_depth, + or_cost, + binary, + time_limit, + } = *options; + let egraph = &self.egraph; + let classes = egraph.classes().map(|class| class.id).collect::>(); + let index = classes + .iter() + .enumerate() + .map(|(index, &id)| (id, index)) + .collect::>(); + let mut nodes = Vec::<(Id, Bool)>::new(); + let mut rows = Vec::new(); + for class in egraph.classes() { + let own = class.id; + for node in &class.nodes { + let children = match node { + Bool::Var(_) => Vec::new(), + Bool::Not(a) => vec![egraph.find(*a)], + Bool::Or([a, b]) => vec![egraph.find(*a), egraph.find(*b)], + Bool::And(_) | Bool::Xor(_) => continue, + }; + if children.contains(&own) { + continue; + } + let n = nodes.len(); + nodes.push((own, node.clone())); + rows.push(("node_class", vec![n.into(), index[&own].into()])); + match node { + Bool::Not(_) => rows.push(("gate", vec![n.into()])), + Bool::Or(_) => rows.push(("or_node", vec![n.into()])), + _ => {} + } + for child in children.into_iter().collect::>() { + rows.push(( + "edge", + vec![n.into(), index[&own].into(), index[&child].into()], + )); + } + } + } + let levels = max_depth.unwrap_or(24); + let mut instance = Instance::new("egraph"); + instance + .domain("Class", (0..classes.len()).map(IValue::from)) + .domain("Node", (0..nodes.len()).map(IValue::from)) + .domain("Tick", (0..=levels).map(IValue::from)) + .param("levels", levels) + .param("or_cost", or_cost) + .param("binary", binary); + if let Some(depth) = max_depth { + instance.param("max_depth", depth); + } + for fact in ["node_class", "edge", "gate", "or_node", "root"] { + instance.fact(fact); + } + for (fact, row) in rows { + instance.row(fact, row); + } + for (_, root) in &self.outputs { + instance.row("root", vec![index[&egraph.find(*root)].into()]); + } + let options = GroundOptions { + guards: false, + provenance: false, + positive_or_aux: false, + no_fold: false, + }; + let mut program = extract_model() + .ground(&instance, options) + .map_err(|error| eyre!("grounding egraph_extract failed:\n{error}"))?; + let objective = program + .objective() + .ok_or_else(|| eyre!("egraph_extract has no objective"))?; + let at_least = program.objective_counter(objective.total_weight()); + let picks = (0..nodes.len()) + .map(|n| program.var_lit("Pick", &[n.into()])) + .collect::>>() + .ok_or_else(|| eyre!("egraph_extract has no Pick for every node"))?; + let cnf = Cnf::from_literals( + program.num_vars(), + program.literals().to_vec(), + program.clause_count(), + ); + let mut solver = SatSolver::new(1); + solver.add_cnf(&cnf); + let stop = AtomicBool::new(false); + let signal = StopSignal { + stop: &stop, + deadline: Some(Instant::now() + time_limit), + restart: None, + }; + let mut best = None::<(i64, HashMap)>; + let mut proven = false; + loop { + let assumptions = match &best { + None => Vec::new(), + Some((cost, _)) => { + let bound = cost - 1 - objective.offset; + if bound < 0 { + proven = true; + break; + } + vec![-at_least[bound as usize]] + } + }; + match solver.solve(&assumptions, &signal) { + SolveResult::Sat => { + let cost = objective.cost(|lit| solver.value(lit)); + let chosen = nodes + .iter() + .zip(&picks) + .filter(|(_, &lit)| solver.value(lit)) + .map(|((class, node), _)| { + let choice = Choice { + node: node.clone(), + gates: BTreeSet::new(), + depth: 0, + }; + (*class, choice) + }) + .collect(); + best = Some((cost, chosen)); + } + SolveResult::Unsat => { + proven = best.is_some(); + break; + } + SolveResult::Interrupted => break, + } + } + let Some((cost, chosen)) = best else { + return Ok(None); + }; + Ok(Some(Extraction { + netlist: self.netlist(&chosen)?, + cost: cost as usize, + proven, + })) + } + + fn candidate(&self, class: Id, node: &Bool, best: &HashMap) -> Option { + let child = |id: &Id| best.get(&self.egraph.find(*id)); + match node { + Bool::Var(_) => Some(Choice { + node: node.clone(), + gates: BTreeSet::new(), + depth: 0, + }), + Bool::Or([a, b]) => { + let (a, b) = (child(a)?, child(b)?); + Some(Choice { + node: node.clone(), + gates: a.gates.union(&b.gates).copied().collect(), + depth: a.depth.max(b.depth), + }) + } + Bool::Not(a) => { + let a = child(a)?; + // A NOT of its own class (through rewrites) builds nothing. + if a.gates.contains(&class) { + return None; + } + let mut gates = a.gates.clone(); + gates.insert(class); + Some(Choice { + node: node.clone(), + gates, + depth: a.depth + 1, + }) + } + Bool::And(_) | Bool::Xor(_) => None, + } + } + + fn netlist(&self, best: &HashMap) -> eyre::Result { + let egraph = &self.egraph; + let mut nets = self + .inputs + .iter() + .enumerate() + .map(|(index, name)| Net { + name: name.clone(), + node_id: index, + driver: NetDriver::Input(name.clone()), + gate_inputs: Vec::new(), + }) + .collect::>(); + let mut net_of_class = HashMap::::new(); + + // The nets whose OR a class is (one net unless it chose an OR). + fn sources( + exploration: &Exploration, + best: &HashMap, + nets: &mut Vec, + net_of_class: &mut HashMap, + class: Id, + depth: usize, + ) -> eyre::Result> { + ensure!(depth < 256, "extraction recursed too deep"); + let class = exploration.egraph.find(class); + let choice = best + .get(&class) + .ok_or_else(|| eyre!("class {class} has no buildable form"))?; + match &choice.node { + Bool::Or([a, b]) => { + let mut set = sources(exploration, best, nets, net_of_class, *a, depth + 1)?; + set.extend(sources( + exploration, + best, + nets, + net_of_class, + *b, + depth + 1, + )?); + Ok(set) + } + _ => Ok(BTreeSet::from([net( + exploration, + best, + nets, + net_of_class, + class, + depth + 1, + )?])), + } + } + + fn net( + exploration: &Exploration, + best: &HashMap, + nets: &mut Vec, + net_of_class: &mut HashMap, + class: Id, + depth: usize, + ) -> eyre::Result { + if let Some(&net) = net_of_class.get(&class) { + return Ok(net); + } + let net = match &best[&class].node { + Bool::Var(symbol) => nets + .iter() + .position(|net| net.driver == NetDriver::Input(symbol.to_string())) + .ok_or_else(|| eyre!("unknown input {symbol}"))?, + Bool::Not(a) => { + let inputs = sources(exploration, best, nets, net_of_class, *a, depth + 1)?; + nets.push(Net { + name: format!("g{}", nets.len()), + node_id: nets.len(), + driver: NetDriver::Gate, + gate_inputs: inputs.into_iter().collect(), + }); + nets.len() - 1 + } + other => bail!("class {class} chose {other} as a net"), + }; + net_of_class.insert(class, net); + Ok(net) + } + + let mut outputs = Vec::new(); + for (name, root) in &self.outputs { + let root = egraph.find(*root); + let choice = best + .get(&root) + .ok_or_else(|| eyre!("output `{name}` has no buildable form"))?; + let output = match choice.node { + Bool::Var(_) => bail!("output `{name}` is an input"), + Bool::Not(_) => net(self, best, &mut nets, &mut net_of_class, root, 0)?, + // An OR output needs a driver: a NOT over the NOR of its terms. + _ => { + let inputs = sources(self, best, &mut nets, &mut net_of_class, root, 0)?; + nets.push(Net { + name: format!("{name}_n"), + node_id: nets.len(), + driver: NetDriver::Gate, + gate_inputs: inputs.into_iter().collect(), + }); + nets.push(Net { + name: format!("g{}", nets.len()), + node_id: nets.len(), + driver: NetDriver::Gate, + gate_inputs: vec![nets.len() - 1], + }); + nets.len() - 1 + } + }; + outputs.push((name.clone(), output)); + } + for (name, output) in &outputs { + if nets[*output].driver == NetDriver::Gate { + nets[*output].name = name.clone(); + } + } + outputs.sort(); + let netlist = NorNetlist { nets, outputs }; + netlist.check_acyclic()?; + Ok(netlist) + } +} + +/// Gates on the slowest path to each output (OR free, NOT one). +pub fn netlist_depths(netlist: &NorNetlist) -> BTreeMap { + let mut depth = vec![0usize; netlist.nets.len()]; + for net in netlist.topological_order() { + if netlist.nets[net].driver == NetDriver::Gate { + depth[net] = 1 + netlist.nets[net] + .gate_inputs + .iter() + .map(|&input| depth[input]) + .max() + .unwrap_or(0); + } + } + netlist + .outputs + .iter() + .map(|(name, net)| (name.clone(), depth[*net])) + .collect() +} + +/// The gates as functions of the inputs: two netlists with the same gate +/// functions and gate inputs build the same circuit. +pub fn signature(netlist: &NorNetlist) -> BTreeSet<(Vec, Vec>)> { + let values = netlist.net_values(); + netlist + .gates() + .map(|gate| { + let mut inputs = netlist.nets[gate] + .gate_inputs + .iter() + .map(|&input| values[input].clone()) + .collect::>(); + inputs.sort(); + (values[gate].clone(), inputs) + }) + .collect() +} + +/// Parses `~ & ^ |` (tightest first) over names and parentheses. +fn parse(text: &str) -> eyre::Result> { + struct Parser<'a> { + chars: std::iter::Peekable>, + expression: RecExpr, + } + impl Parser<'_> { + fn skip(&mut self) { + while self.chars.peek().is_some_and(|c| c.is_whitespace()) { + self.chars.next(); + } + } + fn binary(&mut self, level: usize) -> eyre::Result { + const OPERATORS: [char; 3] = ['|', '^', '&']; + if level == OPERATORS.len() { + return self.unary(); + } + let mut left = self.binary(level + 1)?; + loop { + self.skip(); + if self.chars.peek() != Some(&OPERATORS[level]) { + return Ok(left); + } + self.chars.next(); + let right = self.binary(level + 1)?; + let node = match OPERATORS[level] { + '|' => Bool::Or([left, right]), + '^' => Bool::Xor([left, right]), + _ => Bool::And([left, right]), + }; + left = self.expression.add(node); + } + } + fn unary(&mut self) -> eyre::Result { + self.skip(); + match self.chars.peek() { + Some('~') => { + self.chars.next(); + let inner = self.unary()?; + Ok(self.expression.add(Bool::Not(inner))) + } + Some('(') => { + self.chars.next(); + let inner = self.binary(0)?; + self.skip(); + ensure!(self.chars.next() == Some(')'), "missing `)`"); + Ok(inner) + } + Some(c) if c.is_alphanumeric() || *c == '_' => { + let mut name = String::new(); + while let Some(&c) = self.chars.peek() { + if !(c.is_alphanumeric() || c == '_') { + break; + } + name.push(c); + self.chars.next(); + } + Ok(self.expression.add(Bool::Var(Symbol::from(name)))) + } + other => bail!("unexpected {other:?}"), + } + } + } + let mut parser = Parser { + chars: text.chars().peekable(), + expression: RecExpr::default(), + }; + parser.binary(0)?; + parser.skip(); + ensure!(parser.chars.next().is_none(), "trailing text in `{text}`"); + Ok(parser.expression) +} diff --git a/src/transform/place_and_route/local_placer/exact/egraph_extract.rsdsl b/src/transform/place_and_route/local_placer/exact/egraph_extract.rsdsl new file mode 100644 index 00000000..9e1fc448 --- /dev/null +++ b/src/transform/place_and_route/local_placer/exact/egraph_extract.rsdsl @@ -0,0 +1,86 @@ +rsdsl 2; +model egraph_extract; + +// Exact extraction of a NOR netlist from a saturated Boolean e-graph +// (egraph.rs). Every e-class is a function of the inputs; its nodes are the +// ways to build it from other classes: an input, a NOT of one class (a +// torch), or an OR of two (dust and blocks, free). Picking one node in every +// class the outputs need gives a netlist; shared classes are built once. + +domain Class: int; +domain Node: int; +domain Tick: int; // 0..=levels + +fact node_class(Node, Class); // every buildable node and its class +fact edge(Node, Class, Class); // a node, its class, and a child class +fact gate(Node); // a NOT: one torch, one tick +fact or_node(Node); // an OR: one more input on a NOR +fact root(Class); // an output + +param levels: int = 16; +param max_depth: int? = none; +param gate_cost: int = 1; +param depth_cost: int = 0; +// Wide NORs are hard to build in a narrow box: every input is a signal that +// has to reach the torch's block, so `or_cost` charges each OR node. +param or_cost: int = 0; +// Every NOR reads at most two signals: an OR node may only join classes that +// are not themselves built as ORs. +param binary: bool = false; + +var Pick[n: Node]; +var Need[c: Class]; + +// Ticks from the inputs: a NOT adds one, an OR none. Children come strictly +// before a NOT, so picks cannot loop through torches; an OR loop would join +// classes with the same function, which the e-graph already merged (self +// loops are left out of `edge`). +@encoding(order) +int Depth[c: Class] in 0..=levels; + +// An output is a torch: the netlist names a gate for it (an OR output would +// become a NOR and a NOT there, two torches the count would miss). +rule "출력은 만들어야 하고, 토치임" { + forall c: Class where root(c) { + require Need[c]; + require any(Pick[n] for (n, k) in node_class where k == c and gate(n)); + } +} + +rule "만들 클래스는 노드 하나를 고름" { + forall c: Class { + require Need[c] -> any(Pick[n] for (n, k) in node_class where k == c); + require at_most_one(Pick[n] for (n, k) in node_class where k == c); + } +} + +rule "고른 노드의 자식도 만들고, 더 먼저 도착함" { + forall (n, k, c) in edge { + require Pick[n] -> Need[c]; + if gate(n) { + require Pick[n] -> Depth[c] < Depth[k]; + } else { + require Pick[n] -> Depth[c] <= Depth[k]; + } + } +} + +rule "2입력 NOR만" { + if binary { + forall (n, k, c) in edge where or_node(n) { + require Pick[n] -> not any(Pick[m] for (m, j) in node_class where j == c and or_node(m)); + } + } +} + +rule "출력 깊이 상한" { + if has(max_depth) { + forall c: Class where root(c) { + require Depth[c] <= max_depth; + } + } +} + +minimize gate_cost * count(Pick[n] for n: Node where gate(n)) + + or_cost * count(Pick[n] for n: Node where or_node(n)) + + depth_cost * count(Depth[c] >= t for c: Class, t: Tick where root(c) and t >= 1); diff --git a/src/transform/place_and_route/local_placer/exact/mod.rs b/src/transform/place_and_route/local_placer/exact/mod.rs index 0e4d4092..0507088f 100644 --- a/src/transform/place_and_route/local_placer/exact/mod.rs +++ b/src/transform/place_and_route/local_placer/exact/mod.rs @@ -21,6 +21,7 @@ mod compact; mod construct; mod dimacs; mod dsl; +mod egraph; mod encode; mod layout; mod netlist; @@ -40,6 +41,7 @@ use std::time::{Duration, Instant}; pub use compact::{AttemptTime, CompactionConfig, CompactionReport}; pub use construct::{ConstructionConfig, ConstructionReport, GateOrder}; pub use dimacs::DimacsComments; +pub use egraph::{netlist_depths, signature, Exploration, ExtractOptions, Extraction, Limits, Weights}; pub use encode::CellKind; pub use layout::{ExactLayout, InputPolicy, OutputPolicy}; pub use netlist::{Net, NetDriver, NetId, NorNetlist}; @@ -394,6 +396,14 @@ impl ExactLocalPlacer { }) } + /// A placer for a netlist built elsewhere (an e-graph extraction, say). + pub fn from_netlist(netlist: NorNetlist) -> Self { + Self { + netlist, + name: "exact-local-cell".to_owned(), + } + } + pub fn with_name(mut self, name: impl Into) -> Self { self.name = name.into(); self diff --git a/src/transform/place_and_route/local_placer/exact/netlist.rs b/src/transform/place_and_route/local_placer/exact/netlist.rs index 84d2aacc..50772beb 100644 --- a/src/transform/place_and_route/local_placer/exact/netlist.rs +++ b/src/transform/place_and_route/local_placer/exact/netlist.rs @@ -151,7 +151,7 @@ impl NorNetlist { Ok(netlist) } - fn check_acyclic(&self) -> eyre::Result<()> { + pub(super) fn check_acyclic(&self) -> eyre::Result<()> { let mut state = vec![0u8; self.nets.len()]; fn visit(netlist: &NorNetlist, net: NetId, state: &mut [u8]) -> eyre::Result<()> { match state[net] { diff --git a/src/transform/place_and_route/local_placer/exact/tests.rs b/src/transform/place_and_route/local_placer/exact/tests.rs index 6ab12c06..d820552d 100644 --- a/src/transform/place_and_route/local_placer/exact/tests.rs +++ b/src/transform/place_and_route/local_placer/exact/tests.rs @@ -2030,7 +2030,7 @@ fn print_attempt_times(prefix: &str, report: &CompactionReport) { } /// Construction plus compaction for small circuits: -/// `CIRCUIT=mux2|half-adder|adder2|adder2-nor|mux4|full-adder CIRCUIT_WIDTH=2 +/// `CIRCUIT=mux2|half-adder|adder2|adder2-nor|mux4|full-adder|egraph-full-adder CIRCUIT_WIDTH=2 /// CIRCUIT_HEIGHT=10 CIRCUIT_STEP_SECONDS=60 CIRCUIT_COMPACT_SECONDS=300 /// CIRCUIT_SEED=1 CIRCUIT_WORKERS=8 CIRCUIT_WRITE=`; `CIRCUIT_NETLIST_ONLY=1` stops /// after printing the NOR netlist and its live-net counts; @@ -2047,8 +2047,31 @@ fn diagnose_construct_circuit() -> eyre::Result<()> { .with_test_writer() .try_init(); let circuit = std::env::var("CIRCUIT").unwrap_or_else(|_| "mux2".to_owned()); - let graph = circuit_graph(&circuit)?; - let placer = ExactLocalPlacer::new(&graph)?.with_name(format!("exact-{circuit}")); + // `egraph-full-adder`: the cheapest netlist the e-graph holds + // (`Exploration::extract_exact`) within `EGRAPH_DEPTH` (any), with + // `EGRAPH_OR_COST` (0) per OR node, and only 2-input NORs with + // `EGRAPH_BINARY=1`. + let placer = match circuit.as_str() { + "egraph-full-adder" => { + let (inputs, outputs) = full_adder_functions(); + let exploration = Exploration::new(&inputs, &outputs, Limits::default())?; + let options = ExtractOptions { + max_depth: std::env::var("EGRAPH_DEPTH") + .ok() + .map(|depth| depth.parse::()) + .transpose()?, + or_cost: env_usize("EGRAPH_OR_COST", 0), + binary: std::env::var("EGRAPH_BINARY").as_deref() == Ok("1"), + ..Default::default() + }; + let extraction = exploration + .extract_exact(&options)? + .ok_or_else(|| eyre::eyre!("no netlist for {options:?}"))?; + ExactLocalPlacer::from_netlist(extraction.netlist) + } + _ => ExactLocalPlacer::new(&circuit_graph(&circuit)?)?, + } + .with_name(format!("exact-{circuit}")); let netlist = placer.netlist(); if circuit.starts_with("adder2") { // Both adder netlists must add: {c1, s1, s0} = a1a0 + b1b0. @@ -3519,3 +3542,155 @@ fn report_rcell_timing() -> eyre::Result<()> { } Ok(()) } + +/// The full adder as functions for the e-graph: `(inputs, outputs)`. +fn full_adder_functions() -> (Vec<&'static str>, Vec<(&'static str, &'static str)>) { + ( + vec!["a", "b", "cin"], + vec![("s", "a^b^cin"), ("cout", "(a&b)|(a&cin)|(b&cin)")], + ) +} + +/// Output functions of a netlist by name, as truth-table rows. +fn output_functions(netlist: &NorNetlist) -> BTreeMap> { + let values = netlist.net_values(); + netlist + .outputs + .iter() + .map(|(name, net)| (name.clone(), values[*net].clone())) + .collect() +} + +/// Netlists extracted from the saturated full adder compute the full adder. +/// Exact extraction needs fewer gates than the hand-written `nor9` (8, proven +/// for this e-graph, against 9) and, at the same 9 gates, half its depth; +/// greedy extraction misses the shared NORs and needs more. +#[test] +fn egraph_netlists_compute_the_full_adder() -> eyre::Result<()> { + let (inputs, outputs) = full_adder_functions(); + let exploration = Exploration::new(&inputs, &outputs, Limits::default())?; + let nor9 = NorNetlist::from_logic_graph(&full_adder_graph("nor9"))?; + let expected = output_functions(&nor9); + let greedy = exploration.extract(Weights { + gates: 1.0, + depth: 0.0, + })?; + assert_eq!(output_functions(&greedy), expected); + let fewest = exploration + .extract_exact(&ExtractOptions::default())? + .expect("a netlist"); + assert_eq!(output_functions(&fewest.netlist), expected); + assert!(fewest.proven); + assert_eq!(fewest.netlist.gates().count(), fewest.cost); + assert!(fewest.cost < nor9.gates().count()); + let within = |depth| ExtractOptions { + max_depth: Some(depth), + ..Default::default() + }; + let shallow = exploration + .extract_exact(&within(3))? + .expect("a netlist within 3 gates"); + assert_eq!(output_functions(&shallow.netlist), expected); + assert!(netlist_depths(&shallow.netlist) + .values() + .all(|&depth| depth <= 3)); + assert!(exploration.extract_exact(&within(2))?.is_none()); + Ok(()) +} + +/// Saturates `EGRAPH_CIRCUIT` (`full-adder`) and prints the e-graph's size +/// and, per weighting, the extracted netlist's gates, depths, and live nets +/// beside `nor9`'s: +/// `cargo test --release --lib explore_egraph_netlists -- --ignored --nocapture`. +#[test] +#[ignore = "experiment; run explicitly with --nocapture"] +fn explore_egraph_netlists() -> eyre::Result<()> { + let (inputs, outputs) = full_adder_functions(); + let limits = Limits { + iterations: env_usize("EGRAPH_ITERATIONS", 12), + nodes: env_usize("EGRAPH_NODES", 50_000), + time: Duration::from_secs(env_usize("EGRAPH_SECONDS", 20) as u64), + }; + let started = std::time::Instant::now(); + let exploration = Exploration::new(&inputs, &outputs, limits)?; + println!( + "EGRAPH classes={} nodes={} iterations={} stop={:?} in {:?}", + exploration.classes(), + exploration.nodes(), + exploration.iterations, + exploration.stop_reason, + started.elapsed() + ); + let describe = |label: &str, netlist: &NorNetlist| { + let gates = construct::gate_order(netlist, GateOrder::SmallestConeFirst); + let live = live_after_each_step(netlist, &gates, &BTreeSet::new()); + let fan_in = netlist + .gates() + .map(|gate| netlist.nets[gate].gate_inputs.len()) + .max() + .unwrap_or(0); + println!( + "EGRAPH {label}: gates={} depths={:?} max_fan_in={fan_in} live_max={} live={live:?}", + netlist.gates().count(), + netlist_depths(netlist), + live.iter().max().unwrap_or(&0) + ); + for gate in netlist.gates() { + let inputs = netlist.nets[gate] + .gate_inputs + .iter() + .map(|&input| netlist.nets[input].name.as_str()) + .collect::>(); + println!("EGRAPH {} = NOR{inputs:?}", netlist.nets[gate].name); + } + }; + describe( + "nor9", + &NorNetlist::from_logic_graph(&full_adder_graph("nor9"))?, + ); + if std::env::var("EGRAPH_GREEDY").is_ok() { + for (gates, depth) in [(1.0, 0.0), (1.0, 1.0), (0.01, 1.0)] { + let netlist = exploration.extract(Weights { gates, depth })?; + describe(&format!("greedy gates*{gates}+depth*{depth}"), &netlist); + } + } + // Exact: the cheapest netlist within each depth, shallowest first, for + // each OR cost (`EGRAPH_OR_COSTS`, `0`). + let seconds = Duration::from_secs(env_usize("EGRAPH_EXTRACT_SECONDS", 60) as u64); + let or_costs = std::env::var("EGRAPH_OR_COSTS") + .unwrap_or_else(|_| "0".to_owned()) + .split(',') + .map(str::parse::) + .collect::, _>>()?; + for or_cost in or_costs { + for depth in (2..=env_usize("EGRAPH_MAX_DEPTH", 8)) + .map(Some) + .chain([None]) + { + let started = std::time::Instant::now(); + let options = ExtractOptions { + max_depth: depth, + or_cost, + binary: std::env::var("EGRAPH_BINARY").as_deref() == Ok("1"), + time_limit: seconds, + }; + match exploration.extract_exact(&options)? { + Some(extraction) => describe( + &format!( + "exact or_cost={or_cost} depth<={} cost={} proven={} in {:.1?}", + depth.map_or("any".to_owned(), |depth| depth.to_string()), + extraction.cost, + extraction.proven, + started.elapsed() + ), + &extraction.netlist, + ), + None => println!( + "EGRAPH exact or_cost={or_cost} depth<={depth:?}: none in {:.1?}", + started.elapsed() + ), + } + } + } + Ok(()) +}