From 309c562e4f3fe964d47e18fa43dba1086d062369 Mon Sep 17 00:00:00 2001 From: Pedro Monteiro <83892026+peda-cos@users.noreply.github.com> Date: Mon, 12 Oct 2026 13:36:31 -0300 Subject: [PATCH 01/50] feat: SetSplitting to NAE-SAT clause-per-subset reduction (#1100) Fixes #1100 --- src/rules/mod.rs | 2 + src/rules/setsplitting_naesatisfiability.rs | 120 ++++++++++++++++++ .../rules/setsplitting_naesatisfiability.rs | 104 +++++++++++++++ 3 files changed, 226 insertions(+) create mode 100644 src/rules/setsplitting_naesatisfiability.rs create mode 100644 src/unit_tests/rules/setsplitting_naesatisfiability.rs diff --git a/src/rules/mod.rs b/src/rules/mod.rs index 3baa44186..d224900c7 100644 --- a/src/rules/mod.rs +++ b/src/rules/mod.rs @@ -146,6 +146,7 @@ pub(crate) mod satisfiability_maximum2satisfiability; pub(crate) mod satisfiability_naesatisfiability; pub(crate) mod satisfiability_nontautology; pub(crate) mod setsplitting_betweenness; +pub(crate) mod setsplitting_naesatisfiability; mod spinglass_casts; pub(crate) mod spinglass_maxcut; pub(crate) mod spinglass_qubo; @@ -449,6 +450,7 @@ pub(crate) fn canonical_rule_example_specs() -> Vec &NAESatisfiability { + &self.target + } + + fn extract_solution( + &self, + target_solution: &::Solution, + ) -> crate::rules::ExtractionResult<::Solution> { + crate::rules::traits::validate_target_witness( + self.target_problem(), + target_solution, + |value| value.0, + "target witness does not satisfy the target problem", + )?; + + Ok(target_solution[..self.source_universe_size].to_vec()) + } +} + +#[crate::aggregate_reduction(identity)] +impl crate::rules::AggregateReductionResult for ReductionSetSplittingToNAESAT {} + +#[reduction(transform = { + exact { + num_vars = "universe_size", + num_clauses = "num_subsets", + }, + upper_bound { + num_clause_variables = "universe_size * (universe_size + 1)", + num_literals = "2 * universe_size * num_subsets", + num_literal_pairs = "2 * universe_size * num_subsets * (2 * universe_size * num_subsets + 1)", + }, +})] +impl ReduceTo for SetSplitting { + type Result = ReductionSetSplittingToNAESAT; + + fn reduce_to(&self) -> Result { + let universe_size = self.universe_size(); + let mut clauses = Vec::with_capacity(self.num_subsets()); + + for subset in self.subsets() { + let mut distinct: Vec = Vec::new(); + for &element in subset { + if element >= universe_size { + return Err(>::target_construction( + format!( + "subset element {element} is outside universe of size {universe_size}" + ) + .into(), + )); + } + let literal = (element + 1) as i64; + if !distinct.contains(&literal) { + distinct.push(literal); + } + } + match distinct.len() { + 1 => distinct.push(distinct[0]), + 0 => { + return Err(>::target_construction( + crate::registry::ConstructionError::from( + "empty subset cannot be split".to_string(), + ), + )) + } + _ => {} + } + clauses.push(CNFClause::new(distinct)); + } + let target = NAESatisfiability::new(universe_size, clauses); + Ok(ReductionSetSplittingToNAESAT { + target, + source_universe_size: universe_size, + }) + } +} + +#[cfg(feature = "example-db")] +pub(crate) fn canonical_rule_example_specs() -> Vec { + use crate::export::SolutionPair; + + vec![crate::example_db::specs::RuleExampleSpec { + id: "setsplitting_to_naesatisfiability", + build: || { + crate::example_db::specs::rule_example_with_witness::<_, NAESatisfiability>( + SetSplitting::new(4, vec![vec![0, 1], vec![1, 2, 3], vec![0, 2, 3]]), + SolutionPair { + source_config: serde_json::json!(vec![true, false, true, false]), + target_config: serde_json::json!(vec![true, false, true, false]), + }, + ) + }, + }] +} + +#[cfg(test)] +#[path = "../unit_tests/rules/setsplitting_naesatisfiability.rs"] +mod tests; diff --git a/src/unit_tests/rules/setsplitting_naesatisfiability.rs b/src/unit_tests/rules/setsplitting_naesatisfiability.rs new file mode 100644 index 000000000..97cccc23d --- /dev/null +++ b/src/unit_tests/rules/setsplitting_naesatisfiability.rs @@ -0,0 +1,104 @@ +use crate::models::formula::NAESatisfiability; +use crate::models::set::SetSplitting; +use crate::rules::test_helpers::assert_satisfaction_round_trip_from_satisfaction_target; +use crate::rules::{ReduceTo, ReductionResult}; +use crate::solvers::BruteForce; +use crate::traits::Problem; + +fn rule_example_problem() -> SetSplitting { + SetSplitting::new(4, vec![vec![0, 1], vec![1, 2, 3], vec![0, 2, 3]]) +} + +#[test] +fn test_setsplitting_to_naesatisfiability_closed_loop() { + let source = rule_example_problem(); + let reduction = + ReduceTo::::reduce_to(&source).expect("reduction should succeed"); + + assert_satisfaction_round_trip_from_satisfaction_target( + &source, + &reduction, + "SetSplitting -> NAE-SAT", + ); +} + +#[test] +fn test_setsplitting_to_naesatisfiability_structure() { + let source = rule_example_problem(); + let reduction = + ReduceTo::::reduce_to(&source).expect("reduction should succeed"); + let target = reduction.target_problem(); + + assert_eq!(target.num_vars(), 4); + assert_eq!(target.num_clauses(), 3); + assert_eq!( + target + .clauses() + .iter() + .map(|clause| clause.literals.clone()) + .collect::>(), + vec![vec![1, 2], vec![2, 3, 4], vec![1, 3, 4]], + ); +} + +#[test] +fn test_setsplitting_to_naesatisfiability_repeated_members() { + let source = SetSplitting::new(1, vec![vec![0, 0]]); + let reduction = + ReduceTo::::reduce_to(&source).expect("reduction should succeed"); + + assert_eq!(reduction.target_problem().clauses()[0].literals, [1, 1]); + assert!(BruteForce::new() + .solve(reduction.target_problem()) + .unwrap() + .is_none()); +} + +#[test] +fn test_setsplitting_to_naesatisfiability_extract_solution() { + let source = rule_example_problem(); + let reduction = + ReduceTo::::reduce_to(&source).expect("reduction should succeed"); + + assert_eq!( + reduction + .extract_solution(&vec![true, false, true, false]) + .unwrap(), + vec![true, false, true, false] + ); +} + +#[test] +fn test_setsplitting_to_naesatisfiability_target_witness_extracts_to_satisfying_assignment() { + let source = rule_example_problem(); + let reduction = + ReduceTo::::reduce_to(&source).expect("reduction should succeed"); + let solver = BruteForce::new(); + + let target_solution = solver.solve(reduction.target_problem()).unwrap().unwrap(); + let source_solution = reduction.extract_solution(&target_solution).unwrap(); + + assert!(source.evaluate(&source_solution).unwrap()); +} + +#[cfg(feature = "example-db")] +#[test] +fn test_setsplitting_to_naesatisfiability_canonical_example_spec() { + let specs = crate::rules::setsplitting_naesatisfiability::canonical_rule_example_specs(); + assert_eq!(specs.len(), 1); + + let example = (specs[0].build)(); + assert_eq!(example.source.problem, "SetSplitting"); + assert_eq!(example.target.problem, "NAESatisfiability"); + assert_eq!(example.solutions.len(), 1); + + let pair = &example.solutions[0]; + assert_eq!( + pair.source_config, + serde_json::json!([true, false, true, false]) + ); + assert_eq!( + pair.target_config, + serde_json::json!([true, false, true, false]) + ); +} From 649e24c8dacd3a91b82fb99729a6094e6dfab7e5 Mon Sep 17 00:00:00 2001 From: Xiwei Pan <90967972+isPANN@users.noreply.github.com> Date: Sat, 17 Oct 2026 11:26:28 -0700 Subject: [PATCH 02/50] Add Overhead lens to the graph explorer: per-rule growth classes, SCC groups, reachability Co-Authored-By: Claude Sonnet 5.5 --- docs/website/graph-scene.schema.json | 19 +- docs/website/graph.html | 15 +- docs/website/src/lib/graph-structure.mts | 112 ++++++++ docs/website/src/pages/graph-scene.ts | 35 ++- docs/website/src/pages/graph.ts | 246 +++++++++++++++++- docs/website/src/styles/graph.css | 93 ++++++- package.json | 4 +- .../examples/export_edge_growth.rs | 9 + problemreductions-web/src/lib.rs | 156 ++++++----- problemreductions-web/tests/paths.rs | 19 +- scripts/build_website.py | 11 +- scripts/test_website.py | 36 ++- scripts/test_website_contracts.mjs | 3 +- scripts/test_website_structure.mjs | 67 +++++ 14 files changed, 731 insertions(+), 94 deletions(-) create mode 100644 docs/website/src/lib/graph-structure.mts create mode 100644 problemreductions-web/examples/export_edge_growth.rs create mode 100644 scripts/test_website_structure.mjs diff --git a/docs/website/graph-scene.schema.json b/docs/website/graph-scene.schema.json index 7510f608a..90cb68e8e 100644 --- a/docs/website/graph-scene.schema.json +++ b/docs/website/graph-scene.schema.json @@ -23,12 +23,27 @@ "type": "array", "items": { "type": "object", "additionalProperties": false, - "required": ["source", "target", "witness", "turing"], + "required": ["source", "target", "witness", "aggregate", "turing", "fields"], "properties": { "source": {"type": "integer", "minimum": 0, "maximum": 9007199254740991}, "target": {"type": "integer", "minimum": 0, "maximum": 9007199254740991}, "witness": {"type": "boolean"}, - "turing": {"type": "boolean"} + "aggregate": {"type": "boolean"}, + "turing": {"type": "boolean"}, + "fields": { + "type": "object", + "additionalProperties": { + "type": "object", "additionalProperties": false, + "required": ["certificate", "accuracy"], + "properties": { + "certificate": {"type": ["string", "null"], "minLength": 1}, + "accuracy": { + "type": "object", "required": ["kind"], + "properties": {"kind": {"enum": ["exact", "upper_bound", "unavailable"]}} + } + } + } + } } } }, diff --git a/docs/website/graph.html b/docs/website/graph.html index dcb029482..9561a2053 100644 --- a/docs/website/graph.html +++ b/docs/website/graph.html @@ -33,8 +33,15 @@
-
-

Reduction paths

+
+
+

Reduction graph

+
+ + +
+
+
@@ -49,6 +56,10 @@
+
+
diff --git a/docs/website/src/lib/graph-structure.mts b/docs/website/src/lib/graph-structure.mts new file mode 100644 index 000000000..89943108e --- /dev/null +++ b/docs/website/src/lib/graph-structure.mts @@ -0,0 +1,112 @@ +import { growth, compareDegrees } from './graph-growth.mts'; + +export interface GrowthField { certificate: string | null; accuracy: { kind: 'exact' | 'upper_bound' | 'unavailable' } } +export interface RuleEdge { + source: number; target: number; witness: boolean; aggregate: boolean; turing: boolean; + fields: Record; +} +export type Scope = 'witness' | 'aggregate' | 'turing'; +export type ClassId = 'constant' | 'linear' | 'quadratic' | 'cubic' | 'higher' | 'unknown'; +export interface Link { source: number; target: number } + +/* Polynomial total degree when every source parameter scales together: a visualization convention, not a runtime claim. */ +export const CLASSES: readonly { id: ClassId; label: string; name: string }[] = [ + { id: 'constant', label: '1', name: 'Constant' }, + { id: 'linear', label: 'n', name: 'Linear' }, + { id: 'quadratic', label: 'n²', name: 'Quadratic' }, + { id: 'cubic', label: 'n³', name: 'Cubic' }, + { id: 'higher', label: 'n⁴⁺', name: 'Higher degree' }, + { id: 'unknown', label: '?', name: 'Undetermined' }, +]; +const order = new Map(CLASSES.map((c, i) => [c.id, i])); + +export function growthClass(degree: bigint | null): ClassId { + if (degree === null) return 'unknown'; + return degree >= 4n ? 'higher' : (['constant', 'linear', 'quadratic', 'cubic'] as const)[Number(degree)]!; +} + +export interface EdgeGrowth { + degree: bigint | null; cls: ClassId; accuracy: 'exact' | 'upper_bound'; + fields: { name: string; degree: bigint | null; lead: string; kind: GrowthField['accuracy']['kind'] }[]; +} +const memo = new WeakMap(); +/* Overview policy: the highest field degree. One unavailable field leaves the whole edge undetermined. */ +export function edgeGrowth(edge: RuleEdge): EdgeGrowth { + const cached = memo.get(edge); + if (cached) return cached; + const fields = Object.entries(edge.fields).map(([name, f]) => ({ name, kind: f.accuracy.kind, ...growth(f) })); + let degree: bigint | null = 0n; + for (const f of fields) { + if (f.degree === null) { degree = null; break; } + if (compareDegrees(f.degree, degree) > 0) degree = f.degree; + } + const out = { degree, cls: growthClass(degree), fields, + accuracy: fields.every(f => f.kind === 'exact') ? 'exact' as const : 'upper_bound' as const }; + memo.set(edge, out); + return out; +} + +/* Indices of the rules in scope whose class is at most `limit`. `skip` lists rules excluded by other filters. */ +export function activeRules(rules: readonly RuleEdge[], { scope, limit, skip }: { scope: Scope; limit: ClassId; skip?: Set }) { + const max = order.get(limit)!; + return rules.flatMap((rule, i) => rule[scope] && !skip?.has(i) && order.get(edgeGrowth(rule).cls)! <= max ? [i] : []); +} + +/* Strongly connected components (iterative Tarjan); `comp[v]` indexes `groups`. */ +export function components(n: number, links: readonly Link[]) { + const out: number[][] = Array.from({ length: n }, () => []); + for (const l of links) out[l.source]!.push(l.target); + const index = new Array(n).fill(-1), low = new Array(n).fill(0), on = new Array(n).fill(false); + const comp = new Array(n).fill(-1), groups: number[][] = [], stack: number[] = []; + let counter = 0; + for (let root = 0; root < n; root++) { + if (index[root] !== -1) continue; + const work: [number, number][] = [[root, 0]]; + while (work.length) { + const frame = work[work.length - 1]!, v = frame[0]; + if (frame[1] === 0) { index[v] = low[v] = counter++; stack.push(v); on[v] = true; } + if (frame[1] < out[v]!.length) { + const w = out[v]![frame[1]++]!; + if (index[w] === -1) work.push([w, 0]); + else if (on[w]) low[v] = Math.min(low[v]!, index[w]!); + continue; + } + work.pop(); + if (work.length) { const p = work[work.length - 1]![0]; low[p] = Math.min(low[p]!, low[v]!); } + if (low[v] === index[v]) { + const group: number[] = []; + for (let w = -1; w !== v;) { w = stack.pop()!; on[w] = false; comp[w] = groups.length; group.push(w); } + groups.push(group); + } + } + } + return { comp, groups }; +} + +/* Concrete variants reachable from `start` along (down) or towards (up) the active links, excluding `start` itself. */ +export function reach(n: number, links: readonly Link[], start: number, direction: 'down' | 'up') { + const next: number[][] = Array.from({ length: n }, () => []); + for (const l of links) (direction === 'down' ? next[l.source]! : next[l.target]!).push(direction === 'down' ? l.target : l.source); + const seen = new Set([start]), queue = [start]; + for (let v = queue.pop(); v !== undefined; v = queue.pop()) for (const w of next[v]!) if (!seen.has(w)) { seen.add(w); queue.push(w); } + seen.delete(start); + return seen; +} + +export interface FamilyRule { source: string; target: string; rules: number[]; cls: ClassId; worst: ClassId } +/* Family-level navigation edges. Each keeps the exact variant rules behind it; `cls` is its cheapest rule, `worst` its dearest. */ +export function familyRules(nodes: readonly { name: string }[], rules: readonly RuleEdge[], active: readonly number[]) { + const out = new Map(); + for (const i of active) { + const rule = rules[i]!, s = nodes[rule.source]!.name, t = nodes[rule.target]!.name; + if (s === t) continue; + const cls = edgeGrowth(rule).cls, key = s + '→' + t, entry = out.get(key); + if (!entry) out.set(key, { source: s, target: t, rules: [i], cls, worst: cls }); + else { + entry.rules.push(i); + if (order.get(cls)! < order.get(entry.cls)!) entry.cls = cls; + if (order.get(cls)! > order.get(entry.worst)!) entry.worst = cls; + } + } + return out; +} diff --git a/docs/website/src/pages/graph-scene.ts b/docs/website/src/pages/graph-scene.ts index 636ab61a7..5f228f17d 100644 --- a/docs/website/src/pages/graph-scene.ts +++ b/docs/website/src/pages/graph-scene.ts @@ -8,7 +8,7 @@ export interface SceneNode extends Omit { labelKey: string | null; width: number; height: number; } export interface SceneEdge { - id: string; source: SceneNode; target: SceneNode; shape: SVGLineElement; + id: string; source: SceneNode; target: SceneNode; shape: SVGLineElement; hit: SVGLineElement; label?: never; } export type SceneItem = SceneNode | SceneEdge; @@ -49,7 +49,15 @@ export class GraphScene { const defs = make('defs'), marker = make('marker', {id: 'route-arrow', viewBox: '0 -5 10 10', refX: 9, refY: 0, markerWidth: 11, markerHeight: 11, orient: 'auto', markerUnits: 'userSpaceOnUse'}); marker.append(make('path', {d: 'M0,-4.5 L10,0 L0,4.5 Z', fill: 'var(--accent)'})); - defs.append(marker); this.svg.append(defs, this.world); container.append(this.svg); + defs.append(marker); + // One arrowhead per growth class so the colour follows the edge without relying on context-stroke. + for (const cls of ['constant', 'linear', 'quadratic', 'cubic', 'higher', 'unknown']) { + const head = make('marker', {id: 'arrow-' + cls, viewBox: '0 -5 10 10', refX: 9, refY: 0, markerWidth: 7, markerHeight: 7, + orient: 'auto', markerUnits: 'userSpaceOnUse'}); + head.append(make('path', {d: 'M0,-4 L10,0 L0,4 Z', fill: `var(--g-${cls})`})); + defs.append(head); + } + this.svg.append(defs, this.world); container.append(this.svg); this.nodes = nodes.map(data => { const shape = make('g', {class: 'scene-node', 'data-node': data.id, role: 'button', tabindex: -1, 'aria-haspopup': 'dialog', 'aria-label': data.label}); @@ -63,9 +71,11 @@ export class GraphScene { this.edges = edges.map(({s, t}) => { const source = this.byId.get(s), target = this.byId.get(t); if (!source?.label || !target?.label) throw new Error('A scene edge references a missing node'); - const edge = {id: s + '→' + t, source, target, - shape: make('line', {class: 'scene-edge', 'data-edge': s + '→' + t, 'aria-hidden': 'true'})}; - this.byId.set(edge.id, edge); this.world.append(edge.shape); return edge; + const id = s + '→' + t; + const edge = {id, source, target, + shape: make('line', {class: 'scene-edge', 'data-edge': id, 'aria-hidden': 'true'}), + hit: make('line', {class: 'edge-hit', 'data-hit': id, 'aria-hidden': 'true'})}; + this.byId.set(edge.id, edge); this.world.append(edge.hit, edge.shape); return edge; }); for (const node of this.nodes) this.world.append(node.shape); this.elements = [...this.nodes, ...this.edges]; @@ -81,8 +91,8 @@ export class GraphScene { if (e.button !== 0) return; this.stop(); const p = point(e); pointers.set(e.pointerId, p); - const target = e.target instanceof Element ? e.target.closest('[data-node], [data-edge]') : null; - const id = target?.getAttribute('data-node') || target?.getAttribute('data-edge'); + const target = e.target instanceof Element ? e.target.closest('[data-node], [data-edge], [data-hit]') : null; + const id = target?.getAttribute('data-node') || target?.getAttribute('data-edge') || target?.getAttribute('data-hit'); gesture = {item: id ? this.byId.get(id) : undefined, moved: pointers.size > 1, start: p}; this.svg.setPointerCapture(e.pointerId); @@ -232,8 +242,10 @@ export class GraphScene { for (const node of this.nodes) node.shape.setAttribute('transform', `translate(${node.x} ${node.y})`); for (const edge of this.edges) { const a = edge.source, b = edge.target, d = Math.hypot(b.x-a.x, b.y-a.y) || 1, r = b.size/2 + 4; - edge.shape.setAttribute('x1', String(a.x)); edge.shape.setAttribute('y1', String(a.y)); - edge.shape.setAttribute('x2', String(b.x - (b.x-a.x)*r/d)); edge.shape.setAttribute('y2', String(b.y - (b.y-a.y)*r/d)); + for (const line of [edge.shape, edge.hit]) { + line.setAttribute('x1', String(a.x)); line.setAttribute('y1', String(a.y)); + line.setAttribute('x2', String(b.x - (b.x-a.x)*r/d)); line.setAttribute('y2', String(b.y - (b.y-a.y)*r/d)); + } } } moveNode(node: SceneNode, dx: number, dy: number) { @@ -279,7 +291,7 @@ export class GraphScene { this.animation = requestAnimationFrame(step); } labelBox(node: SceneNode): Bounds { - const important = ['route', 'start', 'end', 'hover', 'focused'].some(c => this.has(node, c)); + const important = ['route', 'start', 'end', 'hover', 'focused', 'reach'].some(c => this.has(node, c)); const size = important ? 12 : 11, text = important ? node.routeLabel : node.labelText; const key = size + ':' + text; if (node.labelKey !== key) { @@ -297,8 +309,9 @@ export class GraphScene { node.width = Math.max(...lines.map(line => this.measure.measureText(line).width)); node.height = lines.length * size * 1.25; node.label.replaceChildren(...lines.map((line, i) => { + // Wrapped lines stay separated for assistive technology, which reads textContent. const span = document.createElementNS('http://www.w3.org/2000/svg', 'tspan'); - span.setAttribute('x', '0'); span.setAttribute('y', String(5+size+i*size*1.25)); span.textContent = line; return span; + span.setAttribute('x', '0'); span.setAttribute('y', String(5+size+i*size*1.25)); span.textContent = i < lines.length - 1 ? line + ' ' : line; return span; })); node.label.setAttribute('font-size', String(size)); } diff --git a/docs/website/src/pages/graph.ts b/docs/website/src/pages/graph.ts index db49746b8..e20eed8c5 100644 --- a/docs/website/src/pages/graph.ts +++ b/docs/website/src/pages/graph.ts @@ -1,7 +1,8 @@ import { graphStartup } from './graph-startup.ts'; import { renderDetails } from './details.ts'; -import { GraphScene, type SceneNode, type SceneItem } from "./graph-scene.ts"; +import { GraphScene, type SceneNode, type SceneItem, type SceneEdge } from "./graph-scene.ts"; import { growth, pathDegree, sizeBadge, compareDegrees } from "../lib/graph-growth.mts"; +import { CLASSES, edgeGrowth, activeRules, components, reach, familyRules, type ClassId, type RuleEdge, type Scope, type FamilyRule } from '../lib/graph-structure.mts'; import { validatePathReply, type PathRequest, type PathReply } from '../lib/path-worker-data.mts'; import type { Endpoint, Route, Step, WasmPathResult } from '../generated/wasm-paths.mjs'; @@ -89,7 +90,7 @@ const scheduleLabels = () => { cancelAnimationFrame(labelRaf); labelRaf = reques function placeLabels() { const r = freeRect(), boxes: Bounds[] = []; const box = (n: SceneNode) => scene.labelBox(n); - const important = (n: SceneNode) => ["route", "start", "end", "hover", "focused"].some(c => scene.has(n, c)); + const important = (n: SceneNode) => ["route", "start", "end", "hover", "focused", "reach"].some(c => scene.has(n, c)); const fits = (b: Bounds) => b.x1 > r.x + 4 && b.x2 < r.x + r.w - 4 && b.y1 > r.y + 4 && b.y2 < r.y + r.h - 4; const hit = (b: Bounds) => boxes.some(o => b.x1 < o.x2 + 6 && b.x2 > o.x1 - 6 && b.y1 < o.y2 + 4 && b.y2 > o.y1 - 4); scene.classes(scene.nodes, "named"); @@ -106,7 +107,7 @@ scene.onChange = scheduleLabels; scene.onDrag = () => { scheduleLabels(); placePop(); }; scene.onHover = (n, over) => { scene.classes([n], over ? "" : "hover", over ? "hover" : ""); - if (!state.result) { + if (!state.result && !lensOn) { if (over) { scene.classes(scene.elements.filter(e => e !== n && !families.get(n.id)!.nbrs.has(e.id)), "", "dim"); scene.classes(scene.edges.filter(e => e.source === n || e.target === n), "dim", "nbr"); @@ -116,6 +117,7 @@ scene.onHover = (n, over) => { }; /* ---------- State ---------- */ +let lensOn = false; const state: State = { source: null, target: null, limit: 20, result: null, selected: null, picked: false, showSlower: false, busy: false }; /* Variant options: one row of pills per variant key. Picking a value keeps the other keys when such a variant exists. */ @@ -245,14 +247,14 @@ for (const side of ["source", "target"] as const) { $("#swap").addEventListener("click", () => { [state.source, state.target] = [state.target, state.source]; syncEnds(); if (state.source != null && state.target != null) run(); }); /* ---------- Node popover ---------- */ -let popNode: SceneNode | null = null, popIndex: number | null = null; +let popNode: SceneNode | null = null, popAnchor: SceneItem | null = null, popIndex: number | null = null; function routeVariantOf(name: string) { const r = state.result?.paths[state.selected! - 1]; if (!r) return null; const hit = endpoints(r).find((e) => e.name === name); return hit ? indexOf.get(keyOf(hit)) : null; } function openPop(node: SceneNode, {keyboard = false} = {}) { - popNode = node; + popNode = popAnchor = node; const name = node.id; popIndex = [state.source, state.target].find((i) => i != null && D.nodes[i]!.name === name) ?? routeVariantOf(name) ?? defaults[name]!; renderPop(); @@ -270,12 +272,13 @@ function renderPop() { acts.append(a, b); pop.append(acts); const details = el("button", "pop-details", "Details"); details.type = "button"; details.onclick = () => showProblem(D.nodes[popIndex!]!); pop.append(details); + if (lensOn) pop.append(popLens(popIndex!)); pop.hidden = false; placePop(); restoreVariantGroup(pop, focusGroup); } function placePop() { - if (!popNode || $("#pop").hidden) return; - const pop = $("#pop"), p = scene.position(popNode), r = freeRect(); + if (!popAnchor || $("#pop").hidden) return; + const pop = $("#pop"), p = scene.position(popAnchor), r = freeRect(); pop.style.maxHeight = Math.max(1, r.h - 24) + "px"; const w = pop.offsetWidth, h = pop.offsetHeight; let x = p.x + 20; if (x + w > r.x + r.w - 12) x = p.x - 20 - w; @@ -284,7 +287,7 @@ function placePop() { } function closePop(restoreFocus = false) { const opener = popNode?.shape; - popNode = null; $("#pop").hidden = true; + popNode = popAnchor = null; $("#pop").hidden = true; if (restoreFocus) opener?.focus({preventScroll: true}); } scene.onNodeTap = openPop; @@ -362,6 +365,7 @@ function pulseAndFrame(name: string) { } $("#close-details").onclick = closeDetails; scene.onEdgeTap = (edge) => { + if (lensOn) { openEdgePop(edge); return; } if (!scene.has(edge, "route")) return; const step = state.result?.paths[state.selected! - 1]!.path.find((s) => s.from.name === edge.source.id && s.to.name === edge.target.id); @@ -469,6 +473,7 @@ function routeEls(n: number) { return [...ids].map(id => scene.byId.get(id)!); } function paintGraph() { + if (lensOn) return; scene.classes(scene.elements, "dim ghost route start end nbr"); scene.nodes.forEach(n => { n.routeLabel = display(n.id); }); if (state.result && state.selected) { @@ -622,6 +627,231 @@ function renderResults(status?: 'same' | 'none' | 'error' | 'cancelled') { } } + +/* ---------- Overhead lens ---------- */ +/* Analysis runs on concrete variants. A family edge only groups the exact variant rules behind it. */ +const rules = D.edges as RuleEdge[]; +interface Lens { scope: Scope; limit: ClassId; noIlp: boolean; focus: number | null; dir: 'down' | 'up'; group: number | null } +const lens: Lens = { scope: 'witness', limit: 'unknown', noIlp: false, focus: null, dir: 'down', group: null }; +const classOrder = CLASSES.map(c => c.id); +const SCOPES: readonly { id: Scope; name: string; hint: string }[] = [ + { id: 'witness', name: 'Witness', hint: 'Rules that map solutions back to the source. Paths mode searches this scope.' }, + { id: 'aggregate', name: 'Value', hint: 'Rules that also map completed values (optimum, count, decision).' }, + { id: 'turing', name: 'Turing', hint: 'Multi-query rules, such as binary search over a decision bound.' }, +]; +const vtext = (i: number) => Object.entries(D.nodes[i]!.variant).map(([k, v]) => k + ": " + v).join(" ") || "default"; +const vname = (i: number) => display(D.nodes[i]!.name) + (multi(D.nodes[i]!.name) ? " · " + vtext(i) : ""); +const skipIlp = () => new Set(lens.noIlp ? rules.flatMap((r, i) => D.nodes[r.source]!.name === "ILP" || D.nodes[r.target]!.name === "ILP" ? [i] : []) : []); +const badge = (cls: ClassId) => { + const c = CLASSES.find(x => x.id === cls)!, b = el("span", "gc g-" + cls, c.label); + b.title = c.name; return b; +}; +const nontrivial = (groups: number[][]) => groups.filter(g => g.length > 1).sort((a, b) => b.length - a.length); +function lensModel() { + const skip = skipIlp(), active = activeRules(rules, { scope: lens.scope, limit: lens.limit, skip }); + const links = active.map(i => rules[i]!), fam = familyRules(D.nodes, rules, active); + const groups = nontrivial(components(D.nodes.length, links).groups); + const scoped = activeRules(rules, { scope: lens.scope, limit: "unknown", skip }); + const counts = new Map(); + scoped.forEach(i => { const c = edgeGrowth(rules[i]!).cls; counts.set(c, (counts.get(c) ?? 0) + 1); }); + const baseline = nontrivial(components(D.nodes.length, scoped.map(i => rules[i]!)).groups).length; + return { active, links, fam, groups, scoped, counts, baseline }; +} +let model = lensModel(); +const ruleClass = (i: number) => edgeGrowth(rules[i]!).cls; +const ruleSteps = (i: number) => ({ from: { name: D.nodes[rules[i]!.source]!.name, variant: D.nodes[rules[i]!.source]!.variant }, + to: { name: D.nodes[rules[i]!.target]!.name, variant: D.nodes[rules[i]!.target]!.variant } }); + +function reachOf(focus: number) { + const variants = reach(D.nodes.length, model.links, focus, lens.dir); + const byFamily = new Map(); + variants.forEach(v => { const n = D.nodes[v]!.name; (byFamily.get(n) ?? byFamily.set(n, []).get(n)!).push(v); }); + byFamily.delete(D.nodes[focus]!.name); + return { variants, byFamily }; +} + +function paintLens() { + const edgeClasses = classOrder.map(c => "e-" + c).join(" "); + scene.classes(scene.elements, "dim ghost route start end nbr off cyc reach pick " + edgeClasses); + const linked = new Set(), cyc = new Set(); + model.fam.forEach(f => { linked.add(f.source); linked.add(f.target); }); + model.groups.forEach(g => g.forEach(v => cyc.add(D.nodes[v]!.name))); + scene.nodes.forEach(n => { n.routeLabel = display(n.id); }); + const picked = lens.group != null ? new Set(model.groups[lens.group]) : null; + const focus = lens.focus != null ? { ...reachOf(lens.focus), v: lens.focus } : null; + const inside = (v: number) => picked ? picked.has(v) : focus ? v === focus.v || focus.variants.has(v) : true; + const lit = new Set(); + scene.edges.forEach(edge => { + const f = model.fam.get(edge.id); + if (!f) { scene.classes([edge], "", "off"); return; } + scene.classes([edge], "", "e-" + f.cls); + if ((picked || focus) && !f.rules.some(i => inside(rules[i]!.source) && inside(rules[i]!.target))) scene.classes([edge], "", "dim"); + else if (picked || focus) { lit.add(edge.source.id); lit.add(edge.target.id); } + }); + scene.nodes.forEach(node => { + const members = families.get(node.id)!.variants; + if (cyc.has(node.id)) scene.classes([node], "", "cyc"); + if (picked || focus) { + if (members.some(inside) && (lit.has(node.id) || (focus && members.includes(focus.v)) || members.some(v => picked?.has(v)))) scene.classes([node], "", "reach"); + else scene.classes([node], "", "dim"); + } else if (!linked.has(node.id)) scene.classes([node], "", "dim"); + }); + scene.nodes.forEach(node => node.shape.setAttribute('aria-label', scene.describe(node) + (cyc.has(node.id) ? ', in a mutually reachable group' : ''))); + scheduleLabels(); +} +function refreshLens() { model = lensModel(); if (lens.group != null && lens.group >= model.groups.length) lens.group = null; paintLens(); renderLens(); } + +function radio(box: HTMLElement, label: string, items: { id: string; text: string; title?: string }[], current: string, pick: (id: string) => void) { + const row = el("div", "seg"); row.setAttribute("role", "radiogroup"); row.setAttribute("aria-label", label); + items.forEach(item => { + const b = el("button", "", item.text); b.type = "button"; b.setAttribute("role", "radio"); b.setAttribute("aria-checked", String(item.id === current)); + if (item.title) b.title = item.title; + b.addEventListener("click", () => pick(item.id)); row.append(b); + }); + box.append(row); return row; +} +function renderLens() { + const box = $("#lens"), hadFocus = document.activeElement?.closest("#lens") ? (document.activeElement as HTMLElement).dataset.key : null; + box.replaceChildren(); + const m = model; + if (lens.focus != null) { + const { variants, byFamily } = reachOf(lens.focus), f = lens.focus; + box.append(el("h2", "lens-title", lens.dir === "down" ? "Reachable from" : "Reaching")); + const head = el("p", "focus-head"); head.append(el("strong", "", vname(f))); + const clear = el("button", "link", "Clear"); clear.type = "button"; clear.addEventListener("click", () => { lens.focus = null; paintLens(); renderLens(); }); + box.append(head, el("p", "hint", `${variants.size} variants in ${byFamily.size + 1} families, following only rules in the active set.`), clear); + const items = el("div", "reach-list"); + [...byFamily].sort((a, b) => b[1].length - a[1].length || a[0].localeCompare(b[0])).forEach(([name, vs]) => { + const b = el("button", "reach-row"); b.type = "button"; + b.append(el("span", "", display(name)), el("small", "", multi(name) ? `${vs.length}/${families.get(name)!.variants.length} variants` : "")); + b.title = "Compare routes in Paths mode"; + b.addEventListener("click", () => { const pair = lens.dir === "down" ? [f, vs[0]!] : [vs[0]!, f]; setTab("paths"); state.source = pair[0]!; state.target = pair[1]!; syncEnds(); run(); }); + items.append(b); + }); + box.append(items); + } + const intro = el("p", "lens-intro"); + intro.append("Each arrow is coloured by the ", el("strong", "", "total degree"), " of its target sizes when every source size grows together. A growth convention, not a runtime bound."); + box.append(intro); + box.append(el("h2", "lens-title", "Rules in scope")); + radio(box, "Rule scope", SCOPES.map(x => ({ id: x.id, text: x.name, title: x.hint })), lens.scope, id => { lens.scope = id as Scope; lens.focus = null; lens.group = null; refreshLens(); }); + box.append(el("p", "hint", SCOPES.find(x => x.id === lens.scope)!.hint)); + + box.append(el("h2", "lens-title", "Growth of the reduced problem")); + const legend = el("div", "legend"); legend.setAttribute("role", "radiogroup"); legend.setAttribute("aria-label", "Show rules up to this growth class"); + const limitAt = classOrder.indexOf(lens.limit); + CLASSES.forEach((c, i) => { + const n = m.counts.get(c.id) ?? 0; + if (!n) return; + const b = el("button", "legend-row" + (i <= limitAt ? " on" : "")); b.type = "button"; b.setAttribute("role", "radio"); + b.setAttribute("aria-checked", String(c.id === lens.limit)); b.dataset.key = "limit-" + c.id; + const sw = document.createElementNS("http://www.w3.org/2000/svg", "svg"); sw.setAttribute("class", "swatch g-" + c.id); sw.setAttribute("viewBox", "0 0 34 8"); sw.setAttribute("aria-hidden", "true"); + const line = document.createElementNS("http://www.w3.org/2000/svg", "line"); for (const [k, v] of Object.entries({ x1: 1, y1: 4, x2: 33, y2: 4 })) line.setAttribute(k, String(v)); + sw.append(line); + b.append(sw, el("span", "gc-name", c.name), el("span", "gc-label", c.label), el("span", "gc-count", String(n))); + b.title = c.id === "unknown" ? "Show every rule, including those with an unavailable target parameter" : `Show rules up to ${c.name.toLowerCase()} growth`; + b.addEventListener("click", () => { lens.limit = c.id; lens.focus = null; refreshLens(); }); + legend.append(b); + }); + box.append(legend); + const hubs = el("label", "check"); const cb = el("input"); cb.type = "checkbox"; cb.checked = lens.noIlp; cb.dataset.key = "noilp"; + const ilpCount = rules.filter((r, i) => r[lens.scope] && (D.nodes[r.source]!.name === "ILP" || D.nodes[r.target]!.name === "ILP")).length; + const total = rules.filter(r => r[lens.scope]).length; + cb.addEventListener("change", () => { lens.noIlp = cb.checked; lens.focus = null; refreshLens(); }); + hubs.append(cb, el("span", "", `Hide rules touching ILP (${ilpCount} of ${total})`)); box.append(hubs); + const sum = el("p", "lens-sum"); sum.append(el("strong", "", String(m.active.length)), ` of ${total} rules · ${m.fam.size} family links`); box.append(sum); + + box.append(el("h2", "lens-title", "Mutually reachable groups")); + const note = el("p", "hint", m.baseline === m.groups.length + ? `${m.groups.length} groups of variants that reduce to each other, through these rules.` + : `${m.groups.length} groups now, ${m.baseline} with every rule in scope. Cheaper rules break the rest.`); + box.append(note); + const list = el("div", "groups"); + m.groups.forEach((g, gi) => { + const b = el("button", "group"); b.type = "button"; b.dataset.key = "group-" + gi; b.setAttribute("aria-pressed", String(lens.group === gi)); + b.append(el("span", "group-size", String(g.length))); + const names = el("span", "group-names"); g.slice().sort((a, c) => a - c).forEach(v => names.append(el("span", "", vname(v)))); b.append(names); + b.addEventListener("click", () => { lens.group = lens.group === gi ? null : gi; lens.focus = null; paintLens(); renderLens(); if (lens.group != null) frame(scene.elements.filter(e => e.label && scene.has(e, "reach")), 1.2); }); + list.append(b); + }); + if (!m.groups.length) list.append(el("p", "hint", "No variants are mutually reachable under this filter.")); + box.append(list); + + const foot = el("p", "hint foot", "Reachability is connectivity among registered reductions. It does not establish solver availability or efficiency."); + box.append(foot); + if (hadFocus) box.querySelector(`[data-key="${hadFocus}"]`)?.focus({ preventScroll: true }); +} + +/* Node popover section: reach and outgoing rules for the chosen variant. */ +function popLens(v: number) { + const wrap = el("div", "pop-lens"); + const down = reach(D.nodes.length, model.links, v, "down").size, up = reach(D.nodes.length, model.links, v, "up").size; + const row = el("div", "pop-reach"); + for (const [dir, label, n] of [["down", "Downstream", down], ["up", "Upstream", up]] as const) { + const b = el("button", "", `${label} ${n}`); b.type = "button"; b.title = `${n} variants ${dir === "down" ? "reachable from" : "that reach"} this one`; + b.setAttribute("aria-pressed", String(lens.focus === v && lens.dir === dir)); + b.addEventListener("click", () => { + lens.focus = v; lens.dir = dir; lens.group = null; closePop(); paintLens(); renderLens(); + frame(scene.nodes.filter(n => scene.has(n, "reach")), 1.2); + }); + row.append(b); + } + wrap.append(row); + const out = [...model.fam.values()].filter(f => f.source === D.nodes[v]!.name); + if (out.length) { + wrap.append(el("p", "pop-sub", "Rules out of this problem")); + out.sort((a, b) => classOrder.indexOf(a.cls) - classOrder.indexOf(b.cls)).forEach(f => { + const b = el("button", "pop-rule"); b.type = "button"; b.append(badge(f.cls), el("span", "", display(f.target))); + b.addEventListener("click", () => openEdgePop(scene.byId.get(f.source + "→" + f.target) as SceneEdge)); + wrap.append(b); + }); + } + return wrap; +} + +/* Edge inspector: every variant rule behind a family link, with exact and bounded formulas kept apart. */ +function openEdgePop(edge: SceneEdge) { + const f = model.fam.get(edge.id); + if (!f) return; + popNode = null; popAnchor = edge; + const pop = $("#pop"); pop.replaceChildren(); + const title = el("h2", "", display(f.source) + " → " + display(f.target)); title.id = "pop-title"; pop.append(title); + pop.append(el("p", "hint", `${f.rules.length} variant rule${f.rules.length === 1 ? "" : "s"} in scope`)); + [...f.rules].sort((a, b) => classOrder.indexOf(ruleClass(a)) - classOrder.indexOf(ruleClass(b))).forEach(i => { + const rule = rules[i]!, g = edgeGrowth(rule), card = el("div", "rule-card"); + const head = el("button", "rule-head"); head.type = "button"; + head.append(badge(g.cls), el("span", "rule-ends", `${vtext(rule.source)} → ${vtext(rule.target)}`)); + head.title = "Open the rule article"; head.addEventListener("click", () => showRule(ruleSteps(i) as Step)); + card.append(head); + const dl = el("dl", "growth"); + g.fields.forEach(x => { dl.append(el("dt", "", prettyField(x.name)), el("dd", "", x.kind === "unavailable" ? "unavailable" : x.lead)); }); + card.append(dl); + card.append(el("small", "acc", g.accuracy === "exact" ? "Θ: every formula is exact" : "O: at least one formula is an upper bound")); + pop.append(card); + }); + const close = el("button", "pop-details", "Close"); close.type = "button"; close.onclick = () => closePop(); pop.append(close); + pop.hidden = false; placePop(); +} + +function setTab(name: "paths" | "overhead") { + lensOn = name === "overhead"; + for (const id of ["paths", "overhead"] as const) { + const tab = $("#tab-" + id); tab.setAttribute("aria-selected", String(id === name)); tab.tabIndex = id === name ? 0 : -1; + $("#view-" + id).hidden = id !== name; + } + document.body.classList.toggle("lens", lensOn); + closePop(); + if (lensOn) { model = lensModel(); paintLens(); renderLens(); frame(scene.elements, 1); } + else { scene.classes(scene.elements, "dim ghost route start end nbr off cyc reach pick " + classOrder.map(c => "e-" + c).join(" ")); paintGraph(); } +} +for (const id of ["paths", "overhead"] as const) { + $("#tab-" + id).addEventListener("click", () => setTab(id)); + $("#tab-" + id).addEventListener("keydown", (e) => { + if (e.key !== "ArrowLeft" && e.key !== "ArrowRight") return; + const other = id === "paths" ? "overhead" : "paths"; setTab(other); $("#tab-" + other).focus(); + }); +} + /* ---------- Dock and resize ---------- */ const zoomBy = (k: number) => { const r = freeRect(); scene.stop(); scene.zoomAt(scene.zoom * k, { x: r.x + r.w / 2, y: r.y + r.h / 2 }); }; $("#zoom-in").onclick = () => zoomBy(1.3); diff --git a/docs/website/src/styles/graph.css b/docs/website/src/styles/graph.css index e61765559..e6b451b41 100644 --- a/docs/website/src/styles/graph.css +++ b/docs/website/src/styles/graph.css @@ -39,6 +39,13 @@ --sans: "DM Sans", system-ui, -apple-system, "Segoe UI", sans-serif; --mono: "DM Mono", ui-monospace, SFMono-Regular, Menlo, monospace; --header-height: 85px; + /* Growth classes: hue plus width and dash, so colour is never the only cue. */ + --g-constant: #b4bdff; + --g-linear: #7fd6c8; + --g-quadratic: #e8d56b; + --g-cubic: #f2a45f; + --g-higher: #ef6c72; + --g-unknown: #a5b3a7; } * { box-sizing: border-box; } html, body { height: 100%; } @@ -62,11 +69,11 @@ button { cursor: pointer; background: none; border: 0; padding: 0; } .node-halo { fill: var(--ink); opacity: 0; } .node-label { font-family: var(--sans); font-weight: 500; fill: var(--ink-2); stroke: var(--bg); stroke-width: 5; paint-order: stroke; stroke-linejoin: round; visibility: hidden; pointer-events: none; } -.scene-node.named .node-label, .scene-node:is(.route,.start,.end,.hover,.focused) .node-label { visibility: visible; } +.scene-node.named .node-label, .scene-node:is(.route,.start,.end,.hover,.focused,.reach) .node-label { visibility: visible; } .scene-node.dim { opacity: .16; } .scene-node.ghost { opacity: .75; } .scene-node:is(.route,.start,.end,.hover,.focused) { opacity: 1; } -.scene-node:is(.route,.start,.end,.hover,.focused) .node-label { fill: var(--ink); } +.scene-node:is(.route,.start,.end,.hover,.focused,.reach) .node-label { fill: var(--ink); } .scene-node.route .node-disc { stroke: var(--accent); } .scene-node.start .node-disc { stroke: var(--start); stroke-width: 3; } .scene-node.end .node-disc { stroke: var(--end); stroke-width: 3; } @@ -195,3 +202,85 @@ button { cursor: pointer; background: none; border: 0; padding: 0; } #details-drawer { z-index: 10; inset: 0; width: auto; border: 0; border-radius: 0; padding: env(safe-area-inset-top) env(safe-area-inset-right) env(safe-area-inset-bottom) env(safe-area-inset-left); } } @media (prefers-reduced-motion: reduce) { .size.pending { animation: none; } } + +/* Tabs and Overhead lens */ +.panel-head { display: flex; align-items: center; justify-content: space-between; gap: 12px; } +.tabs { display: flex; gap: 2px; padding: 3px; background: rgba(237,242,232,.06); border-radius: 999px; } +.tabs button { padding: 4px 12px; border-radius: 999px; font-size: 13px; font-weight: 500; color: var(--ink-2); } +.tabs button[aria-selected="true"] { background: var(--ink); color: var(--bg); } +.view { flex: 1; min-height: 0; display: flex; flex-direction: column; } +.lens { flex: 1; min-height: 0; overflow-y: auto; padding: 8px 18px 18px; overscroll-behavior: contain; scrollbar-width: thin; } +.lens-intro { margin: 4px 0 6px; color: var(--ink-2); font-size: 13px; } +.lens-intro strong { color: var(--ink); font-weight: 600; } +.lens-title { margin: 18px 0 8px; font: 600 12px var(--mono); letter-spacing: .04em; text-transform: uppercase; color: var(--ink-3); } +.hint { margin: 6px 0; font-size: 12.5px; color: var(--ink-2); } +.hint.foot { margin-top: 20px; color: var(--ink-3); } +.seg { display: flex; padding: 3px; gap: 2px; background: rgba(237,242,232,.06); border-radius: 10px; } +.seg button { flex: 1; padding: 5px 0; border-radius: 8px; font-size: 13px; color: var(--ink-2); } +.seg button[aria-checked="true"] { background: var(--raised); color: var(--ink); box-shadow: 0 0 0 1px var(--line); } +.legend { display: grid; gap: 2px; } +.legend-row { display: grid; grid-template-columns: 40px 1fr auto 34px; align-items: center; gap: 8px; padding: 6px 8px; border-radius: 9px; text-align: left; opacity: .38; transition: opacity .15s; } +.legend-row.on { opacity: 1; } +.legend-row:hover { background: var(--hover); opacity: 1; } +.legend-row[aria-checked="true"] { background: rgba(237,242,232,.07); box-shadow: inset 0 0 0 1px var(--line); } +.swatch { width: 34px; height: 8px; overflow: visible; } +.swatch line { stroke: currentColor; stroke-width: 2; fill: none; } +.gc-name { font-size: 13.5px; } +.gc-label, .gc-count { font: 12px var(--mono); color: var(--ink-2); text-align: right; } +.gc { display: inline-block; min-width: 30px; padding: 1px 6px; border-radius: 999px; border: 1px solid currentColor; font: 500 11.5px var(--mono); text-align: center; } +.g-constant { color: var(--g-constant); } .g-linear { color: var(--g-linear); } .g-quadratic { color: var(--g-quadratic); } +.g-cubic { color: var(--g-cubic); } .g-higher { color: var(--g-higher); } .g-unknown { color: var(--g-unknown); } +.swatch.g-higher line { stroke-dasharray: 6 3; stroke-width: 2.6; } +.swatch.g-cubic line { stroke-width: 2.2; } +.swatch.g-unknown line { stroke-dasharray: 2 3; } +.check { display: flex; gap: 8px; align-items: center; margin: 10px 0 4px; padding: 0 8px; font-size: 13px; color: var(--ink-2); cursor: pointer; } +.check input { accent-color: var(--accent); } +.lens-sum { margin: 8px 8px 0; font-size: 13px; color: var(--ink-2); } +.lens-sum strong { color: var(--ink); font-size: 15px; } +.groups { display: grid; gap: 4px; } +.group { display: grid; grid-template-columns: 24px 1fr; gap: 8px; align-items: start; padding: 7px 8px; border-radius: 10px; text-align: left; border: 1px solid var(--line); } +.group:hover { background: var(--hover); } +.group[aria-pressed="true"] { border-color: var(--accent); background: color-mix(in oklab, var(--accent) 8%, transparent); } +.group-size { font: 500 12px var(--mono); color: var(--accent-ink); background: var(--accent); border-radius: 999px; text-align: center; padding: 1px 0; } +.group-names { display: grid; gap: 1px; font-size: 12.5px; } +.focus-head { margin: 0; } +.reach-list { display: grid; gap: 1px; margin-top: 8px; max-height: 240px; overflow-y: auto; scrollbar-width: thin; } +.reach-row { display: flex; justify-content: space-between; gap: 8px; padding: 5px 8px; border-radius: 8px; font-size: 13px; text-align: left; } +.reach-row:hover { background: var(--hover); } +.reach-row small { color: var(--ink-3); font: 11.5px var(--mono); } + +/* Edges in the Overhead lens */ +.edge-hit { stroke: transparent; stroke-width: 10px; pointer-events: none; } +.lens .edge-hit { pointer-events: stroke; cursor: pointer; } +.lens .edge-hit:hover + .scene-edge { stroke-width: 3px; opacity: 1; } +.lens :is(.scene-edge, .edge-hit) { vector-effect: non-scaling-stroke; } +.lens .scene-edge { stroke-width: 1.2; opacity: .85; transition: opacity .2s, stroke .2s; } +.lens .scene-edge.off { opacity: 0; } +.lens .edge-hit:has(+ .scene-edge.off) { pointer-events: none; } +.lens .scene-edge.dim { opacity: .07; } +.scene-edge.e-constant { stroke: var(--g-constant); marker-end: url(#arrow-constant); } +.scene-edge.e-linear { stroke: var(--g-linear); marker-end: url(#arrow-linear); } +.scene-edge.e-quadratic { stroke: var(--g-quadratic); stroke-width: 1.5; marker-end: url(#arrow-quadratic); } +.scene-edge.e-cubic { stroke: var(--g-cubic); stroke-width: 1.8; marker-end: url(#arrow-cubic); } +.scene-edge.e-higher { stroke: var(--g-higher); stroke-width: 2.3; stroke-dasharray: 6 3; marker-end: url(#arrow-higher); } +.scene-edge.e-unknown { stroke: var(--g-unknown); stroke-dasharray: 2 3; marker-end: url(#arrow-unknown); } +.lens .scene-node.cyc .node-disc { stroke: var(--accent); stroke-dasharray: 3 2; stroke-width: 2.4; } +.lens .scene-node.reach { opacity: 1; } +.lens .scene-node.reach .node-label { fill: var(--ink); } + +/* Popover additions */ +.pop-lens { margin-top: 10px; padding-top: 10px; border-top: 1px solid var(--line); } +.pop-reach { display: grid; grid-template-columns: 1fr 1fr; gap: 6px; } +.pop-reach button { padding: 6px 0; border-radius: 9px; font-size: 12.5px; background: rgba(237,242,232,.07); } +.pop-reach button:hover, .pop-reach button[aria-pressed="true"] { background: var(--accent); color: var(--accent-ink); } +.pop-sub { margin: 10px 0 4px; font-size: 12px; color: var(--ink-3); } +.pop-rule { display: flex; width: 100%; align-items: center; gap: 8px; padding: 4px 2px; font-size: 13px; text-align: left; } +.pop-rule:hover span:last-child { text-decoration: underline; text-underline-offset: 3px; } +.pop:has(.rule-card) { width: 320px; } +.rule-card { margin: 8px 0; padding: 8px 10px; border: 1px solid var(--line); border-radius: 10px; } +.rule-head { display: flex; align-items: center; gap: 8px; width: 100%; text-align: left; } +.rule-head:hover .rule-ends { text-decoration: underline; text-underline-offset: 3px; } +.rule-ends { font: 12px var(--mono); color: var(--ink); overflow-wrap: anywhere; } +.rule-card .growth { margin: 8px 0 4px; font-size: 12px; } +.acc { color: var(--ink-3); font-size: 11.5px; } +@media (prefers-reduced-motion: reduce) { .legend-row, .lens .scene-edge { transition: none; } } diff --git a/package.json b/package.json index 277f84d5b..6eb189ad7 100644 --- a/package.json +++ b/package.json @@ -4,11 +4,11 @@ "scripts": { "build:frontend": "node scripts/build_frontend.mjs", "typecheck": "tsc --project tsconfig.json", - "lint:frontend": "eslint docs/website/src scripts/build_frontend.mjs scripts/generate_website_contracts.mjs scripts/validate_website_data.mjs scripts/test_website_contracts.mjs scripts/test_website_growth.mjs scripts/website_contracts.mjs", + "lint:frontend": "eslint docs/website/src scripts/build_frontend.mjs scripts/generate_website_contracts.mjs scripts/validate_website_data.mjs scripts/test_website_contracts.mjs scripts/test_website_growth.mjs scripts/test_website_structure.mjs scripts/website_contracts.mjs", "generate:reduction-graph-layout": "node scripts/generate_reduction_graph_layout.js", "test:reduction-graph-js": "node scripts/test_reduction_graph_js.js && node scripts/test_reduction_graph_layout_generator.js", "generate:frontend-contracts": "cargo run --locked -p problemreductions-web --features schema-export --example export_frontend_schema | node scripts/generate_website_contracts.mjs", - "test:frontend-contracts": "node --test scripts/test_website_contracts.mjs scripts/test_website_growth.mjs", + "test:frontend-contracts": "node --test scripts/test_website_contracts.mjs scripts/test_website_growth.mjs scripts/test_website_structure.mjs", "pretypecheck": "npm run generate:frontend-contracts", "pretest:frontend-contracts": "npm run generate:frontend-contracts" }, diff --git a/problemreductions-web/examples/export_edge_growth.rs b/problemreductions-web/examples/export_edge_growth.rs new file mode 100644 index 000000000..1fb1a52d9 --- /dev/null +++ b/problemreductions-web/examples/export_edge_growth.rs @@ -0,0 +1,9 @@ +//! Certify every registered reduction's target-parameter growth for the website graph. +use std::io::Read; + +fn main() -> Result<(), Box> { + let mut input = String::new(); + std::io::stdin().read_to_string(&mut input)?; + println!("{}", problemreductions_web::edge_growth(&input)?); + Ok(()) +} diff --git a/problemreductions-web/src/lib.rs b/problemreductions-web/src/lib.rs index 36eae808e..69d7aadfa 100644 --- a/problemreductions-web/src/lib.rs +++ b/problemreductions-web/src/lib.rs @@ -336,6 +336,49 @@ struct ComparisonQuery { paths: Vec, } +impl Edge { + /// The registered parameter relation of this one reduction. + fn transform(&self, label: &str) -> Result { + if let Some(error) = &self.parameter_contract_error { + return Err(error.clone()); + } + let mut fields = Vec::new(); + for parameter in &self.parameters { + if parameter.contract == Contract::Unavailable { + continue; + } + let formula = parameter + .formula + .as_ref() + .ok_or("Missing parameter formula.")?; + let relation = if parameter.contract == Contract::Exact { + ParameterRelation::Exact + } else { + ParameterRelation::UpperBound + }; + fields.push(( + parameter.field.clone(), + relation, + Expr::try_parse(formula).map_err(|error| error.to_string())?, + )); + } + let mut transform = ParameterTransform::from_fields(label.to_string(), fields) + .map_err(|error| error.to_string())?; + for parameter in &self.parameters { + if parameter.contract == Contract::Unavailable { + transform.declare_unavailable( + ¶meter.field, + parameter + .reason + .as_deref() + .ok_or("Missing reason for unavailable parameter.")?, + ); + } + } + Ok(transform) + } +} + impl Graph { fn route_indices(&self, route: &Route) -> Result, JsError> { if route.path.is_empty() || route.steps != route.path.len() { @@ -378,39 +421,12 @@ pub fn summarize_paths(input: &str) -> Result { .iter() .find(|edge| edge.source == pair[0] && edge.target == pair[1]) .ok_or_else(|| JsError::new("Path references an unregistered reduction."))?; - if let Some(error) = &edge.parameter_contract_error { - return Err(JsError::new(error)); - } - let mut fields = Vec::new(); - for parameter in &edge.parameters { - if parameter.contract == Contract::Unavailable { - continue; - } - let formula = parameter - .formula - .as_ref() - .ok_or_else(|| JsError::new("Missing parameter formula."))?; - let relation = if parameter.contract == Contract::Exact { - ParameterRelation::Exact - } else { - ParameterRelation::UpperBound - }; - fields.push((parameter.field.clone(), relation, Expr::try_parse(formula)?)); - } - let mut transform = ParameterTransform::from_fields( - format!("{} -> {}", nodes[pair[0]].name, nodes[pair[1]].name), - fields, - )?; - for parameter in &edge.parameters { - if parameter.contract == Contract::Unavailable { - transform.declare_unavailable( - ¶meter.field, - parameter.reason.as_deref().ok_or_else(|| { - JsError::new("Missing reason for unavailable parameter.") - })?, - ); - } - } + let transform = edge + .transform(&format!( + "{} -> {}", + nodes[pair[0]].name, nodes[pair[1]].name + )) + .map_err(|error| JsError::new(&error))?; composed = Some(if let Some(prefix) = composed { prefix.compose( &transform, @@ -437,34 +453,7 @@ pub fn summarize_paths(input: &str) -> Result { let profiles = profiles .iter() .map(|profile| { - let fields = profile - .fields - .iter() - .map(|(name, field)| { - let (certificate, accuracy) = match &field.certificate { - Ok((poly, relation)) => ( - Some(poly.to_expr().to_string()), - match relation { - ParameterRelation::Exact => ComparisonAccuracy::Exact, - ParameterRelation::UpperBound => ComparisonAccuracy::UpperBound, - }, - ), - Err(reason) => ( - None, - ComparisonAccuracy::Unavailable { - reason: reason.into(), - }, - ), - }; - ( - name.clone(), - ComparisonField { - certificate, - accuracy, - }, - ) - }) - .collect(); + let fields = comparison_fields(profile); ComparisonProfile { source_coordinates: profile.domain.iter().map(ToString::to_string).collect(), fields, @@ -478,6 +467,51 @@ pub fn summarize_paths(input: &str) -> Result { })?) } +fn comparison_fields(profile: &Profile) -> BTreeMap { + profile + .fields + .iter() + .map(|(name, field)| { + let (certificate, accuracy) = match &field.certificate { + Ok((poly, relation)) => ( + Some(poly.to_expr().to_string()), + match relation { + ParameterRelation::Exact => ComparisonAccuracy::Exact, + ParameterRelation::UpperBound => ComparisonAccuracy::UpperBound, + }, + ), + Err(reason) => ( + None, + ComparisonAccuracy::Unavailable { + reason: reason.into(), + }, + ), + }; + ( + name.clone(), + ComparisonField { + certificate, + accuracy, + }, + ) + }) + .collect() +} + +/// Growth of every registered reduction taken alone: one certified field map per edge, in edge order. +pub fn edge_growth(input: &str) -> Result { + let Graph { nodes, edges } = serde_json::from_str(input).map_err(|error| error.to_string())?; + let growth = edges + .iter() + .map(|edge| { + let label = format!("{} -> {}", nodes[edge.source].name, nodes[edge.target].name); + edge.transform(&label) + .map(|transform| comparison_fields(&Profile::from_transform(&transform))) + }) + .collect::, _>>()?; + serde_json::to_string(&growth).map_err(|error| error.to_string()) +} + #[cfg(test)] mod tests { use super::*; diff --git a/problemreductions-web/tests/paths.rs b/problemreductions-web/tests/paths.rs index 718a888e9..7f63203fe 100644 --- a/problemreductions-web/tests/paths.rs +++ b/problemreductions-web/tests/paths.rs @@ -1,4 +1,4 @@ -use problemreductions_web::{find_paths, summarize_paths}; +use problemreductions_web::{edge_growth, find_paths, summarize_paths}; use serde_json::{json, Value}; fn graph() -> Value { @@ -234,3 +234,20 @@ fn unreachable_and_identical_endpoints_have_no_routes() { assert_eq!(result, json!({"paths":[],"truncated":false})); } } + +#[test] +fn edge_growth_certifies_each_reduction_alone_and_keeps_its_accuracy() { + let mut graph = graph(); + graph["edges"][1]["parameters"] = json!([ + {"field":"n", "contract":"upper_bound", "formula":"n + m^2"}, + {"field":"k", "contract":"unavailable", "reason":"data dependent"} + ]); + let growth: Value = serde_json::from_str(&edge_growth(&graph.to_string()).unwrap()).unwrap(); + assert_eq!(growth.as_array().unwrap().len(), 3); + assert_eq!(growth[0]["n"]["certificate"], "n^2"); + assert_eq!(growth[0]["n"]["accuracy"]["kind"], "exact"); + assert_eq!(growth[1]["n"]["certificate"], "n + m^2"); + assert_eq!(growth[1]["n"]["accuracy"]["kind"], "upper_bound"); + assert_eq!(growth[1]["k"]["certificate"], Value::Null); + assert_eq!(growth[1]["k"]["accuracy"]["kind"], "unavailable"); +} diff --git a/scripts/build_website.py b/scripts/build_website.py index dbfa1ad63..6f73bbe1d 100644 --- a/scripts/build_website.py +++ b/scripts/build_website.py @@ -261,12 +261,17 @@ def build(output, graph_path, schemas_path, open_questions=None): } subprocess.run(['node', str(ROOT / 'scripts/validate_website_data.mjs'), 'atlas-summary'], input=json.dumps(summary), text=True, check=True) - scene = {"layout": layout, "aliases": graph["aliases"], - "edges": [{key: edge[key] for key in ("source", "target", "witness", "turing")} for edge in edges], - "nodes": [{key: node[key] for key in ("name", "category", "variant", "default")} for node in nodes]} engine = {"nodes": [{key: node[key] for key in ("name", "variant", "default", "parameter_names")} for node in nodes], "edges": [{key: edge[key] for key in ('source', 'target', 'parameters', 'parameter_contract_error', 'witness', 'turing')} for edge in edges]} + # Each registered reduction's certified target-parameter growth, from the same engine as Paths mode. + growth = json.loads(subprocess.run( + ["cargo", "run", "--locked", "-q", "-p", "problemreductions-web", "--example", "export_edge_growth"], + cwd=ROOT, input=json.dumps(engine), check=True, capture_output=True, text=True).stdout) + scene = {"layout": layout, "aliases": graph["aliases"], + "edges": [{**{key: edge[key] for key in ("source", "target", "witness", "aggregate", "turing")}, "fields": fields} + for edge, fields in zip(edges, growth, strict=True)], + "nodes": [{key: node[key] for key in ("name", "category", "variant", "default")} for node in nodes]} for name, data in (("graph-scene", scene), ("path-graph", engine)): subprocess.run(['node', str(ROOT / 'scripts/validate_website_data.mjs'), name], input=json.dumps(data), text=True, check=True) diff --git a/scripts/test_website.py b/scripts/test_website.py index 9cb771450..06cac8740 100644 --- a/scripts/test_website.py +++ b/scripts/test_website.py @@ -149,6 +149,40 @@ def test_accessibility_graph_popover(self): self.page.keyboard.press('Enter') self.assert_accessible('graph-popover') + def test_accessibility_graph_overhead(self): + self.page.goto(self.base + 'graph.html') + self.page.get_by_role('tab', name='Overhead').click() + expect(self.page.locator('#lens .legend-row').first).to_be_visible() + self.assert_accessible('graph-overhead') + + def test_graph_overhead_filter_recolours_edges_and_recomputes_groups(self): + self.page.goto(self.base + 'graph.html') + self.page.get_by_role('tab', name='Overhead').click() + groups = self.page.locator('#lens .group') + everything = groups.count() + self.assertGreater(everything, 0) + edges = self.page.locator('.scene-edge.e-linear, .scene-edge.e-quadratic, .scene-edge.e-cubic, .scene-edge.e-higher') + self.assertGreater(edges.count(), 0) + self.page.locator('[data-key="limit-linear"]').click() + self.assertLess(groups.count(), everything) + self.assertEqual(self.page.locator('#lens [role="radio"][aria-checked="true"][data-key="limit-linear"]').count(), 1) + self.assertGreater(self.page.locator('.scene-edge.off').count(), 0) + self.page.get_by_role('tab', name='Paths').click() + self.assertEqual(self.page.locator('.scene-edge.off').count(), 0) + expect(self.page.locator('#results .summary strong')).to_contain_text('best route') + + def test_graph_overhead_reach_hands_off_to_paths(self): + self.page.goto(self.base + 'graph.html') + self.page.get_by_role('tab', name='Overhead').click() + self.page.locator('.scene-node[data-node="MaximumIndependentSet"]').focus() + self.page.keyboard.press('Enter') + self.page.get_by_role('button', name='Downstream').click() + expect(self.page.locator('#lens .reach-row').first).to_be_visible() + self.page.locator('#lens .reach-row', has_text='QUBO').click() + expect(self.page.locator('#tab-paths')).to_have_attribute('aria-selected', 'true') + expect(self.page.locator('#target')).to_have_value('QUBO') + expect(self.page.locator('#results .summary strong')).to_contain_text('best route') + def test_accessibility_graph_desktop_drawer(self): self.page.goto(self.base + 'graph.html') self.page.locator('.steps button').first.click() @@ -598,7 +632,7 @@ def test_graph_brand_returns_home(self): self.visit() self.page.get_by_role('link', name='Graph', exact=True).click() expect(self.page.locator('#cy svg.graph-scene').first).to_be_visible() - self.page.get_by_role('link', name='Reduction paths', exact=True).click() + self.page.get_by_role('link', name='Reduction graph', exact=True).click() expect(self.page.locator('main .hero')).to_be_visible() def test_graph_pan_zoom_and_node_drag_preserve_route(self): diff --git a/scripts/test_website_contracts.mjs b/scripts/test_website_contracts.mjs index cb6019fb9..4affbea50 100644 --- a/scripts/test_website_contracts.mjs +++ b/scripts/test_website_contracts.mjs @@ -27,7 +27,8 @@ function scene() { { name: 'Alpha', category: 'graph', variant: { weight: 'i64' }, default: false }, { name: 'Beta', category: 'misc', variant: {}, default: true }, ], - edges: [{ source: 1, target: 2, witness: true, turing: false }, { source: 0, target: 2, witness: false, turing: true }], + edges: [{ source: 1, target: 2, witness: true, aggregate: false, turing: false, fields: { n: { certificate: 'num_vertices^2', accuracy: { kind: 'exact' } } } }, + { source: 0, target: 2, witness: false, aggregate: false, turing: true, fields: {} }], aliases: { Alpha: ['ALPHA'], Beta: [] }, layout: { Alpha: { x: -0.5, y: 2 }, Beta: { x: 3.25, y: -1 } }, }; diff --git a/scripts/test_website_structure.mjs b/scripts/test_website_structure.mjs new file mode 100644 index 000000000..23abd6c3b --- /dev/null +++ b/scripts/test_website_structure.mjs @@ -0,0 +1,67 @@ +import assert from 'node:assert/strict'; +import { test } from 'node:test'; +import { edgeGrowth, growthClass, activeRules, components, reach, familyRules, CLASSES } from '../docs/website/src/lib/graph-structure.mts'; + +const field = (certificate, kind = 'exact') => ({ certificate, accuracy: { kind } }); +const rule = (source, target, fields, caps = {}) => ({ source, target, witness: true, aggregate: false, turing: false, fields, ...caps }); + +test('an edge is classified by its highest-degree field and keeps exact vs bound', () => { + const g = edgeGrowth(rule(0, 1, { a: field('num_vertices'), b: field('2 * num_edges^2 + 1', 'upper_bound') })); + assert.equal(g.degree, 2n); + assert.equal(g.cls, 'quadratic'); + assert.equal(g.accuracy, 'upper_bound'); + assert.equal(edgeGrowth(rule(0, 1, { a: field('num_vertices * num_edges') })).accuracy, 'exact'); +}); + +test('constants, higher degrees and unavailable fields get their own classes', () => { + assert.equal(edgeGrowth(rule(0, 1, { a: field('3') })).cls, 'constant'); + assert.equal(edgeGrowth(rule(0, 1, { a: field('num_vertices^4') })).cls, 'higher'); + const partial = edgeGrowth(rule(0, 1, { a: field('num_vertices'), b: field(null, 'unavailable') })); + assert.equal(partial.cls, 'unknown'); + assert.equal(partial.degree, null); + assert.equal(growthClass(null), 'unknown'); + assert.deepEqual(CLASSES.map(c => c.id), ['constant', 'linear', 'quadratic', 'cubic', 'higher', 'unknown']); +}); + +test('scope selects edges by the capability alone and the limit keeps provable classes only', () => { + const rules = [ + rule(0, 1, { a: field('num_vertices') }, { aggregate: true }), + rule(1, 2, { a: field('num_vertices^2') }), + rule(2, 3, { a: field(null, 'unavailable') }), + rule(3, 0, { a: field('1') }, { witness: false, turing: true }), + ]; + assert.deepEqual(activeRules(rules, { scope: 'witness', limit: 'unknown' }), [0, 1, 2]); + assert.deepEqual(activeRules(rules, { scope: 'witness', limit: 'quadratic' }), [0, 1]); + assert.deepEqual(activeRules(rules, { scope: 'witness', limit: 'linear' }), [0]); + assert.deepEqual(activeRules(rules, { scope: 'aggregate', limit: 'unknown' }), [0]); + assert.deepEqual(activeRules(rules, { scope: 'turing', limit: 'unknown' }), [3]); + assert.deepEqual(activeRules(rules, { scope: 'witness', limit: 'unknown', skip: new Set([1]) }), [0, 2]); +}); + +test('components are strongly connected sets and follow the active edge set', () => { + const edges = [[0, 1], [1, 0], [1, 2], [2, 3], [3, 2]].map(([s, t]) => ({ source: s, target: t })); + const { groups } = components(5, edges); + assert.deepEqual(groups.filter(g => g.length > 1).map(g => [...g].sort()).sort(), [[0, 1], [2, 3]]); + assert.equal(groups.length, 3); + const cut = components(5, edges.filter(e => !(e.source === 1 && e.target === 0))); + assert.equal(cut.groups.filter(g => g.length > 1).length, 1); +}); + +test('reachability is directed over concrete variants', () => { + const edges = [[0, 1], [1, 2], [3, 1]].map(([s, t]) => ({ source: s, target: t })); + assert.deepEqual([...reach(4, edges, 0, 'down')].sort(), [1, 2]); + assert.deepEqual([...reach(4, edges, 2, 'up')].sort(), [0, 1, 3]); + assert.deepEqual([...reach(4, edges, 2, 'down')], []); +}); + +test('family rules keep every variant rule traceable and never join distinct variants', () => { + const nodes = [{ name: 'A' }, { name: 'A' }, { name: 'B' }, { name: 'B' }]; + const rules = [rule(0, 2, { a: field('num_vertices') }), rule(1, 3, { a: field('num_vertices^3') })]; + const fam = familyRules(nodes, rules, [0, 1]); + assert.equal(fam.size, 1); + const edge = fam.get('A→B'); + assert.deepEqual(edge.rules, [0, 1]); + assert.equal(edge.cls, 'linear'); + assert.equal(edge.worst, 'cubic'); + assert.equal(familyRules(nodes, rules, [1]).get('A→B').cls, 'cubic'); +}); From 22aa7ed55151abddd70dea0e0974a281fd48a6e9 Mon Sep 17 00:00:00 2001 From: Xiwei Pan <90967972+isPANN@users.noreply.github.com> Date: Sat, 17 Oct 2026 11:34:22 -0700 Subject: [PATCH 03/50] Redesign the Overhead panel around one headline, a distribution bar and short group chips Fade ILP edges on the map, frame the dense core, and lead with the finding that most reductions are at most quadratic. Co-Authored-By: Claude Sonnet 5.5 --- docs/website/src/pages/graph.ts | 162 +++++++++++++++++------------- docs/website/src/styles/graph.css | 75 ++++++++------ scripts/test_website.py | 2 +- 3 files changed, 133 insertions(+), 106 deletions(-) diff --git a/docs/website/src/pages/graph.ts b/docs/website/src/pages/graph.ts index e20eed8c5..210b1b4a0 100644 --- a/docs/website/src/pages/graph.ts +++ b/docs/website/src/pages/graph.ts @@ -672,7 +672,7 @@ function reachOf(focus: number) { function paintLens() { const edgeClasses = classOrder.map(c => "e-" + c).join(" "); - scene.classes(scene.elements, "dim ghost route start end nbr off cyc reach pick " + edgeClasses); + scene.classes(scene.elements, "dim ghost route start end nbr off cyc reach pick hub " + edgeClasses); const linked = new Set(), cyc = new Set(); model.fam.forEach(f => { linked.add(f.source); linked.add(f.target); }); model.groups.forEach(g => g.forEach(v => cyc.add(D.nodes[v]!.name))); @@ -685,6 +685,7 @@ function paintLens() { const f = model.fam.get(edge.id); if (!f) { scene.classes([edge], "", "off"); return; } scene.classes([edge], "", "e-" + f.cls); + if (!picked && !focus && (edge.source.id === "ILP" || edge.target.id === "ILP")) scene.classes([edge], "", "hub"); if ((picked || focus) && !f.rules.some(i => inside(rules[i]!.source) && inside(rules[i]!.target))) scene.classes([edge], "", "dim"); else if (picked || focus) { lit.add(edge.source.id); lit.add(edge.target.id); } }); @@ -699,86 +700,103 @@ function paintLens() { scene.nodes.forEach(node => node.shape.setAttribute('aria-label', scene.describe(node) + (cyc.has(node.id) ? ', in a mutually reachable group' : ''))); scheduleLabels(); } +/* Frame the dense middle of the map; a few far-flung isolated problems should not shrink everything else. */ +function frameCore() { + const linked = scene.nodes.filter(n => families.get(n.id)!.nbrs.size > 1); + const cx = linked.reduce((a, n) => a + n.x, 0) / linked.length, cy = linked.reduce((a, n) => a + n.y, 0) / linked.length; + const near = linked.map(n => [Math.hypot(n.x - cx, n.y - cy), n] as const).sort((a, b) => a[0] - b[0]); + frame(near.slice(0, Math.ceil(near.length * .85)).map(([, n]) => n), 1.6); +} function refreshLens() { model = lensModel(); if (lens.group != null && lens.group >= model.groups.length) lens.group = null; paintLens(); renderLens(); } -function radio(box: HTMLElement, label: string, items: { id: string; text: string; title?: string }[], current: string, pick: (id: string) => void) { - const row = el("div", "seg"); row.setAttribute("role", "radiogroup"); row.setAttribute("aria-label", label); - items.forEach(item => { - const b = el("button", "", item.text); b.type = "button"; b.setAttribute("role", "radio"); b.setAttribute("aria-checked", String(item.id === current)); - if (item.title) b.title = item.title; - b.addEventListener("click", () => pick(item.id)); row.append(b); - }); - box.append(row); return row; -} -function renderLens() { - const box = $("#lens"), hadFocus = document.activeElement?.closest("#lens") ? (document.activeElement as HTMLElement).dataset.key : null; - box.replaceChildren(); - const m = model; - if (lens.focus != null) { - const { variants, byFamily } = reachOf(lens.focus), f = lens.focus; - box.append(el("h2", "lens-title", lens.dir === "down" ? "Reachable from" : "Reaching")); - const head = el("p", "focus-head"); head.append(el("strong", "", vname(f))); - const clear = el("button", "link", "Clear"); clear.type = "button"; clear.addEventListener("click", () => { lens.focus = null; paintLens(); renderLens(); }); - box.append(head, el("p", "hint", `${variants.size} variants in ${byFamily.size + 1} families, following only rules in the active set.`), clear); - const items = el("div", "reach-list"); - [...byFamily].sort((a, b) => b[1].length - a[1].length || a[0].localeCompare(b[0])).forEach(([name, vs]) => { - const b = el("button", "reach-row"); b.type = "button"; - b.append(el("span", "", display(name)), el("small", "", multi(name) ? `${vs.length}/${families.get(name)!.variants.length} variants` : "")); - b.title = "Compare routes in Paths mode"; - b.addEventListener("click", () => { const pair = lens.dir === "down" ? [f, vs[0]!] : [vs[0]!, f]; setTab("paths"); state.source = pair[0]!; state.target = pair[1]!; syncEnds(); run(); }); - items.append(b); - }); - box.append(items); - } - const intro = el("p", "lens-intro"); - intro.append("Each arrow is coloured by the ", el("strong", "", "total degree"), " of its target sizes when every source size grows together. A growth convention, not a runtime bound."); - box.append(intro); - box.append(el("h2", "lens-title", "Rules in scope")); - radio(box, "Rule scope", SCOPES.map(x => ({ id: x.id, text: x.name, title: x.hint })), lens.scope, id => { lens.scope = id as Scope; lens.focus = null; lens.group = null; refreshLens(); }); - box.append(el("p", "hint", SCOPES.find(x => x.id === lens.scope)!.hint)); - - box.append(el("h2", "lens-title", "Growth of the reduced problem")); - const legend = el("div", "legend"); legend.setAttribute("role", "radiogroup"); legend.setAttribute("aria-label", "Show rules up to this growth class"); - const limitAt = classOrder.indexOf(lens.limit); +const short = (name: string) => aliasMap[name]?.[0] ?? display(name); +const pct = (n: number, d: number) => d ? Math.round(100 * n / d) : 0; + +/* The distribution bar doubles as legend and filter: each segment keeps every class up to itself. */ +function costCard(box: HTMLElement) { + const m = model, total = [...m.counts.values()].reduce((a, b) => a + b, 0), limitAt = classOrder.indexOf(lens.limit); + const mild = classOrder.slice(0, classOrder.indexOf("quadratic") + 1).reduce((a, c) => a + (m.counts.get(c) ?? 0), 0); + const into = rules.filter(r => r[lens.scope] && D.nodes[r.target]!.name === "ILP").length, scoped = rules.filter(r => r[lens.scope]).length; + const card = el("section", "lcard cost"); + const hero = el("div", "hero-n"); hero.append(el("span", "num", String(pct(mild, total))), el("span", "of", "%")); + card.append(el("h2", "eyebrow", "Overhead of a reduction"), hero, + el("p", "cap", `of ${total} reductions grow at most quadratically in the source size${into > scoped / 4 ? `. ILP alone receives ${into}.` : "."}`)); + const bar = el("div", "dist"); bar.setAttribute("role", "radiogroup"); bar.setAttribute("aria-label", "Show reductions up to this growth class"); + const legend = el("div", "dist-legend"); CLASSES.forEach((c, i) => { const n = m.counts.get(c.id) ?? 0; if (!n) return; - const b = el("button", "legend-row" + (i <= limitAt ? " on" : "")); b.type = "button"; b.setAttribute("role", "radio"); - b.setAttribute("aria-checked", String(c.id === lens.limit)); b.dataset.key = "limit-" + c.id; - const sw = document.createElementNS("http://www.w3.org/2000/svg", "svg"); sw.setAttribute("class", "swatch g-" + c.id); sw.setAttribute("viewBox", "0 0 34 8"); sw.setAttribute("aria-hidden", "true"); - const line = document.createElementNS("http://www.w3.org/2000/svg", "line"); for (const [k, v] of Object.entries({ x1: 1, y1: 4, x2: 33, y2: 4 })) line.setAttribute(k, String(v)); - sw.append(line); - b.append(sw, el("span", "gc-name", c.name), el("span", "gc-label", c.label), el("span", "gc-count", String(n))); - b.title = c.id === "unknown" ? "Show every rule, including those with an unavailable target parameter" : `Show rules up to ${c.name.toLowerCase()} growth`; - b.addEventListener("click", () => { lens.limit = c.id; lens.focus = null; refreshLens(); }); - legend.append(b); + const on = i <= limitAt, name = `${c.name}: ${n} reductions (${pct(n, total)}%)`; + const seg = el("button", "seg-bar g-" + c.id + (on ? " on" : "")); seg.type = "button"; seg.style.flexGrow = String(n); + seg.setAttribute("role", "radio"); seg.setAttribute("aria-checked", String(c.id === lens.limit)); seg.setAttribute("aria-label", name); seg.title = name; seg.dataset.key = "limit-" + c.id; + seg.addEventListener("click", () => { lens.limit = c.id; lens.focus = null; refreshLens(); }); + bar.append(seg); + const key = el("button", "dist-key g-" + c.id + (on ? " on" : ""), ""); key.type = "button"; key.tabIndex = -1; key.setAttribute("aria-hidden", "true"); + key.append(el("b", "", c.label), el("span", "", String(n))); + key.addEventListener("click", () => seg.click()); + legend.append(key); }); - box.append(legend); - const hubs = el("label", "check"); const cb = el("input"); cb.type = "checkbox"; cb.checked = lens.noIlp; cb.dataset.key = "noilp"; - const ilpCount = rules.filter((r, i) => r[lens.scope] && (D.nodes[r.source]!.name === "ILP" || D.nodes[r.target]!.name === "ILP")).length; - const total = rules.filter(r => r[lens.scope]).length; - cb.addEventListener("change", () => { lens.noIlp = cb.checked; lens.focus = null; refreshLens(); }); - hubs.append(cb, el("span", "", `Hide rules touching ILP (${ilpCount} of ${total})`)); box.append(hubs); - const sum = el("p", "lens-sum"); sum.append(el("strong", "", String(m.active.length)), ` of ${total} rules · ${m.fam.size} family links`); box.append(sum); - - box.append(el("h2", "lens-title", "Mutually reachable groups")); - const note = el("p", "hint", m.baseline === m.groups.length - ? `${m.groups.length} groups of variants that reduce to each other, through these rules.` - : `${m.groups.length} groups now, ${m.baseline} with every rule in scope. Cheaper rules break the rest.`); - box.append(note); + card.append(bar, legend); + const showing = lens.limit === "unknown" ? "Showing every reduction" : `Showing ${m.active.length} · ${CLASSES[limitAt]!.name.toLowerCase()} or cheaper`; + card.append(el("p", "showing", showing)); + const seg = el("div", "seg"); seg.setAttribute("role", "radiogroup"); seg.setAttribute("aria-label", "Rule scope"); + SCOPES.forEach(x => { + const b = el("button", "", x.name); b.type = "button"; b.setAttribute("role", "radio"); b.setAttribute("aria-checked", String(x.id === lens.scope)); b.title = x.hint; + b.addEventListener("click", () => { lens.scope = x.id; lens.focus = null; lens.group = null; refreshLens(); }); + seg.append(b); + }); + card.append(seg); + box.append(card); +} + +function groupsCard(box: HTMLElement) { + const m = model, card = el("section", "lcard"); + const head = el("div", "lcard-head"); head.append(el("h2", "eyebrow", "Mutually reducible")); + const count = el("span", "count", m.baseline === m.groups.length ? String(m.groups.length) : `${m.groups.length} of ${m.baseline}`); + count.title = "Groups of variants that reduce to each other"; head.append(count); card.append(head); + if (m.baseline !== m.groups.length) card.append(el("p", "cap", `${m.baseline - m.groups.length} fall apart once costlier rules are removed.`)); const list = el("div", "groups"); m.groups.forEach((g, gi) => { - const b = el("button", "group"); b.type = "button"; b.dataset.key = "group-" + gi; b.setAttribute("aria-pressed", String(lens.group === gi)); - b.append(el("span", "group-size", String(g.length))); - const names = el("span", "group-names"); g.slice().sort((a, c) => a - c).forEach(v => names.append(el("span", "", vname(v)))); b.append(names); - b.addEventListener("click", () => { lens.group = lens.group === gi ? null : gi; lens.focus = null; paintLens(); renderLens(); if (lens.group != null) frame(scene.elements.filter(e => e.label && scene.has(e, "reach")), 1.2); }); + const families = [...new Set(g.map(v => D.nodes[v]!.name))], open = lens.group === gi; + const b = el("button", "group"); b.type = "button"; b.dataset.key = "group-" + gi; b.setAttribute("aria-pressed", String(open)); + b.append(el("span", "group-names", families.map(short).join(" · ")), el("span", "group-size", String(g.length))); + b.title = g.map(vname).join("\n"); + b.addEventListener("click", () => { lens.group = open ? null : gi; lens.focus = null; paintLens(); renderLens(); if (!open) frame(scene.nodes.filter(n => scene.has(n, "reach")), 1.2); }); list.append(b); + if (open) { const d = el("ul", "group-detail"); g.slice().sort((a, c) => a - c).forEach(v => d.append(el("li", "", vname(v)))); list.append(d); } }); - if (!m.groups.length) list.append(el("p", "hint", "No variants are mutually reachable under this filter.")); - box.append(list); + if (!m.groups.length) list.append(el("p", "cap", "None under this filter.")); + card.append(list); box.append(card); +} + +function focusCard(box: HTMLElement) { + const f = lens.focus!, { variants, byFamily } = reachOf(f), card = el("section", "lcard focus"); + const head = el("div", "lcard-head"); head.append(el("h2", "eyebrow", lens.dir === "down" ? "Reduces to" : "Reduced from")); + const clear = el("button", "link", "Clear"); clear.type = "button"; clear.addEventListener("click", () => { lens.focus = null; paintLens(); renderLens(); }); + head.append(clear); card.append(head); + card.append(el("p", "focus-name", display(D.nodes[f]!.name)), el("p", "cap", `${multi(D.nodes[f]!.name) ? vtext(f) + " · " : ""}${variants.size} variants in ${byFamily.size} other families`)); + const items = el("div", "reach-list"); + [...byFamily].sort((a, b) => b[1].length - a[1].length || a[0].localeCompare(b[0])).forEach(([name, vs]) => { + const b = el("button", "reach-row"); b.type = "button"; b.append(el("span", "", display(name)), el("small", "", multi(name) ? `${vs.length}/${families.get(name)!.variants.length}` : "")); + b.title = "Compare routes in Paths"; + b.addEventListener("click", () => { const pair = lens.dir === "down" ? [f, vs[0]!] : [vs[0]!, f]; setTab("paths"); state.source = pair[0]!; state.target = pair[1]!; syncEnds(); run(); }); + items.append(b); + }); + card.append(items); box.append(card); +} - const foot = el("p", "hint foot", "Reachability is connectivity among registered reductions. It does not establish solver availability or efficiency."); - box.append(foot); +function renderLens() { + const box = $("#lens"), hadFocus = document.activeElement?.closest("#lens") ? (document.activeElement as HTMLElement).dataset.key : null; + box.replaceChildren(); + if (lens.focus != null) focusCard(box); + costCard(box); groupsCard(box); + const about = el("details", "about"); about.append(el("summary", "", "How to read this")); + about.append(el("p", "", "Arrows point from source to target. Colour is the total degree of the target's sizes when every source size grows together: a visualization convention, not a runtime bound. Θ marks exact formulas and O upper bounds.")); + about.append(el("p", "", "Reachability is connectivity among registered reductions; it does not establish solver availability or efficiency. ILP edges are faded on the map because it receives nearly half of all reductions.")); + const ilp = el("label", "check"), cb = el("input"); cb.type = "checkbox"; cb.checked = lens.noIlp; cb.dataset.key = "noilp"; + cb.addEventListener("change", () => { lens.noIlp = cb.checked; lens.focus = null; refreshLens(); }); + ilp.append(cb, el("span", "", "Leave ILP out of the analysis")); about.append(ilp); + box.append(about); if (hadFocus) box.querySelector(`[data-key="${hadFocus}"]`)?.focus({ preventScroll: true }); } @@ -841,8 +859,8 @@ function setTab(name: "paths" | "overhead") { } document.body.classList.toggle("lens", lensOn); closePop(); - if (lensOn) { model = lensModel(); paintLens(); renderLens(); frame(scene.elements, 1); } - else { scene.classes(scene.elements, "dim ghost route start end nbr off cyc reach pick " + classOrder.map(c => "e-" + c).join(" ")); paintGraph(); } + if (lensOn) { model = lensModel(); paintLens(); renderLens(); frameCore(); } + else { scene.classes(scene.elements, "dim ghost route start end nbr off cyc reach pick hub " + classOrder.map(c => "e-" + c).join(" ")); paintGraph(); } } for (const id of ["paths", "overhead"] as const) { $("#tab-" + id).addEventListener("click", () => setTab(id)); diff --git a/docs/website/src/styles/graph.css b/docs/website/src/styles/graph.css index e6b451b41..da15fdd05 100644 --- a/docs/website/src/styles/graph.css +++ b/docs/website/src/styles/graph.css @@ -209,45 +209,53 @@ button { cursor: pointer; background: none; border: 0; padding: 0; } .tabs button { padding: 4px 12px; border-radius: 999px; font-size: 13px; font-weight: 500; color: var(--ink-2); } .tabs button[aria-selected="true"] { background: var(--ink); color: var(--bg); } .view { flex: 1; min-height: 0; display: flex; flex-direction: column; } -.lens { flex: 1; min-height: 0; overflow-y: auto; padding: 8px 18px 18px; overscroll-behavior: contain; scrollbar-width: thin; } -.lens-intro { margin: 4px 0 6px; color: var(--ink-2); font-size: 13px; } -.lens-intro strong { color: var(--ink); font-weight: 600; } -.lens-title { margin: 18px 0 8px; font: 600 12px var(--mono); letter-spacing: .04em; text-transform: uppercase; color: var(--ink-3); } -.hint { margin: 6px 0; font-size: 12.5px; color: var(--ink-2); } -.hint.foot { margin-top: 20px; color: var(--ink-3); } +.lens { flex: 1; min-height: 0; overflow-y: auto; padding: 6px 14px 16px; display: grid; align-content: start; gap: 10px; overscroll-behavior: contain; scrollbar-width: thin; } +.lcard { padding: 16px 16px 14px; border-radius: 14px; background: rgba(237,242,232,.04); border: 1px solid var(--line); } +.lcard-head { display: flex; align-items: baseline; justify-content: space-between; gap: 8px; } +.eyebrow { margin: 0; font: 500 11px var(--mono); letter-spacing: .09em; text-transform: uppercase; color: var(--ink-3); } +.cap { margin: 4px 0 0; font-size: 13px; line-height: 1.4; color: var(--ink-2); } +.count { font: 500 12px var(--mono); color: var(--ink-2); } +.hero-n { margin-top: 8px; line-height: 1; } +.hero-n .num { font: italic 400 58px/1 var(--display); letter-spacing: -.01em; color: var(--ink); } +.showing { margin: 0 0 12px; font: 12px var(--mono); color: var(--ink-2); } +.hero-n .of { font: 400 26px var(--display); font-style: italic; color: var(--ink-3); } +.dist { display: flex; gap: 3px; height: 22px; margin: 16px 0 10px; } +.seg-bar { min-width: 8px; height: 100%; border-radius: 5px; background: currentColor; opacity: .3; transition: opacity .2s, transform .15s; } +.seg-bar.on { opacity: 1; } +.seg-bar:hover { transform: scaleY(1.18); opacity: 1; } +.seg-bar[aria-checked="true"] { box-shadow: 0 0 0 2px var(--bg), 0 0 0 3.5px currentColor; } +.seg-bar.g-higher { background: repeating-linear-gradient(135deg, currentColor 0 4px, color-mix(in oklab, currentColor 45%, var(--bg)) 4px 7px); } +.seg-bar.g-unknown { background: transparent; box-shadow: inset 0 0 0 1.5px currentColor; } +.dist-legend { display: flex; flex-wrap: wrap; gap: 4px 14px; margin-bottom: 8px; } +.dist-key { display: inline-flex; align-items: baseline; gap: 6px; font: 12px var(--mono); opacity: .4; } +.dist-key.on { opacity: 1; } +.dist-key b { font-weight: 500; } +.dist-key span { color: var(--ink-2); } +.lcard .seg { margin-top: 2px; } .seg { display: flex; padding: 3px; gap: 2px; background: rgba(237,242,232,.06); border-radius: 10px; } .seg button { flex: 1; padding: 5px 0; border-radius: 8px; font-size: 13px; color: var(--ink-2); } .seg button[aria-checked="true"] { background: var(--raised); color: var(--ink); box-shadow: 0 0 0 1px var(--line); } -.legend { display: grid; gap: 2px; } -.legend-row { display: grid; grid-template-columns: 40px 1fr auto 34px; align-items: center; gap: 8px; padding: 6px 8px; border-radius: 9px; text-align: left; opacity: .38; transition: opacity .15s; } -.legend-row.on { opacity: 1; } -.legend-row:hover { background: var(--hover); opacity: 1; } -.legend-row[aria-checked="true"] { background: rgba(237,242,232,.07); box-shadow: inset 0 0 0 1px var(--line); } -.swatch { width: 34px; height: 8px; overflow: visible; } -.swatch line { stroke: currentColor; stroke-width: 2; fill: none; } -.gc-name { font-size: 13.5px; } -.gc-label, .gc-count { font: 12px var(--mono); color: var(--ink-2); text-align: right; } -.gc { display: inline-block; min-width: 30px; padding: 1px 6px; border-radius: 999px; border: 1px solid currentColor; font: 500 11.5px var(--mono); text-align: center; } -.g-constant { color: var(--g-constant); } .g-linear { color: var(--g-linear); } .g-quadratic { color: var(--g-quadratic); } -.g-cubic { color: var(--g-cubic); } .g-higher { color: var(--g-higher); } .g-unknown { color: var(--g-unknown); } -.swatch.g-higher line { stroke-dasharray: 6 3; stroke-width: 2.6; } -.swatch.g-cubic line { stroke-width: 2.2; } -.swatch.g-unknown line { stroke-dasharray: 2 3; } -.check { display: flex; gap: 8px; align-items: center; margin: 10px 0 4px; padding: 0 8px; font-size: 13px; color: var(--ink-2); cursor: pointer; } -.check input { accent-color: var(--accent); } -.lens-sum { margin: 8px 8px 0; font-size: 13px; color: var(--ink-2); } -.lens-sum strong { color: var(--ink); font-size: 15px; } -.groups { display: grid; gap: 4px; } -.group { display: grid; grid-template-columns: 24px 1fr; gap: 8px; align-items: start; padding: 7px 8px; border-radius: 10px; text-align: left; border: 1px solid var(--line); } +.groups { display: grid; gap: 3px; margin-top: 10px; } +.group { display: flex; align-items: center; justify-content: space-between; gap: 10px; padding: 8px 10px; border-radius: 10px; text-align: left; background: rgba(237,242,232,.04); } .group:hover { background: var(--hover); } -.group[aria-pressed="true"] { border-color: var(--accent); background: color-mix(in oklab, var(--accent) 8%, transparent); } -.group-size { font: 500 12px var(--mono); color: var(--accent-ink); background: var(--accent); border-radius: 999px; text-align: center; padding: 1px 0; } -.group-names { display: grid; gap: 1px; font-size: 12.5px; } -.focus-head { margin: 0; } -.reach-list { display: grid; gap: 1px; margin-top: 8px; max-height: 240px; overflow-y: auto; scrollbar-width: thin; } +.group[aria-pressed="true"] { background: color-mix(in oklab, var(--accent) 14%, transparent); box-shadow: inset 0 0 0 1px color-mix(in oklab, var(--accent) 55%, transparent); } +.group-names { font-size: 13.5px; line-height: 1.35; } +.group-size { flex: none; font: 500 11px var(--mono); color: var(--ink-3); } +.group-detail { margin: 2px 0 6px; padding: 0 10px 0 22px; list-style: none; display: grid; gap: 2px; font: 12px/1.4 var(--mono); color: var(--ink-2); } +.focus { background: color-mix(in oklab, var(--accent) 7%, transparent); } +.focus-name { margin: 6px 0 0; font: italic 400 30px/1.1 var(--display); } +.reach-list { display: grid; gap: 1px; margin-top: 10px; max-height: 200px; overflow-y: auto; scrollbar-width: thin; } .reach-row { display: flex; justify-content: space-between; gap: 8px; padding: 5px 8px; border-radius: 8px; font-size: 13px; text-align: left; } .reach-row:hover { background: var(--hover); } .reach-row small { color: var(--ink-3); font: 11.5px var(--mono); } +.about { padding: 2px 4px; font-size: 12.5px; color: var(--ink-2); } +.about summary { cursor: pointer; padding: 6px 0; color: var(--ink-3); font: 500 11px var(--mono); letter-spacing: .09em; text-transform: uppercase; } +.about p { margin: 6px 0; line-height: 1.5; } +.check { display: flex; gap: 8px; align-items: center; margin: 10px 0 4px; font-size: 13px; color: var(--ink-2); cursor: pointer; } +.check input { accent-color: var(--accent); } +.g-constant { color: var(--g-constant); } .g-linear { color: var(--g-linear); } .g-quadratic { color: var(--g-quadratic); } +.g-cubic { color: var(--g-cubic); } .g-higher { color: var(--g-higher); } .g-unknown { color: var(--g-unknown); } +.gc { display: inline-block; min-width: 30px; padding: 1px 6px; border-radius: 999px; border: 1px solid currentColor; font: 500 11.5px var(--mono); text-align: center; } /* Edges in the Overhead lens */ .edge-hit { stroke: transparent; stroke-width: 10px; pointer-events: none; } @@ -258,6 +266,7 @@ button { cursor: pointer; background: none; border: 0; padding: 0; } .lens .scene-edge.off { opacity: 0; } .lens .edge-hit:has(+ .scene-edge.off) { pointer-events: none; } .lens .scene-edge.dim { opacity: .07; } +.lens .scene-edge.hub { opacity: .07; } .scene-edge.e-constant { stroke: var(--g-constant); marker-end: url(#arrow-constant); } .scene-edge.e-linear { stroke: var(--g-linear); marker-end: url(#arrow-linear); } .scene-edge.e-quadratic { stroke: var(--g-quadratic); stroke-width: 1.5; marker-end: url(#arrow-quadratic); } @@ -283,4 +292,4 @@ button { cursor: pointer; background: none; border: 0; padding: 0; } .rule-ends { font: 12px var(--mono); color: var(--ink); overflow-wrap: anywhere; } .rule-card .growth { margin: 8px 0 4px; font-size: 12px; } .acc { color: var(--ink-3); font-size: 11.5px; } -@media (prefers-reduced-motion: reduce) { .legend-row, .lens .scene-edge { transition: none; } } +@media (prefers-reduced-motion: reduce) { .seg-bar, .lens .scene-edge { transition: none; } } diff --git a/scripts/test_website.py b/scripts/test_website.py index 06cac8740..840390180 100644 --- a/scripts/test_website.py +++ b/scripts/test_website.py @@ -152,7 +152,7 @@ def test_accessibility_graph_popover(self): def test_accessibility_graph_overhead(self): self.page.goto(self.base + 'graph.html') self.page.get_by_role('tab', name='Overhead').click() - expect(self.page.locator('#lens .legend-row').first).to_be_visible() + expect(self.page.locator('#lens .seg-bar').first).to_be_visible() self.assert_accessible('graph-overhead') def test_graph_overhead_filter_recolours_edges_and_recomputes_groups(self): From 93aed595366f6840003c84abc8dd69127077cee8 Mon Sep 17 00:00:00 2001 From: Xiwei Pan <90967972+isPANN@users.noreply.github.com> Date: Sat, 17 Oct 2026 11:39:23 -0700 Subject: [PATCH 04/50] Strip explanatory captions and the options block from the Overhead panel Co-Authored-By: Claude Sonnet 5.5 --- docs/website/src/pages/graph.ts | 33 +++++++++------------------------ 1 file changed, 9 insertions(+), 24 deletions(-) diff --git a/docs/website/src/pages/graph.ts b/docs/website/src/pages/graph.ts index 210b1b4a0..d2d8f00d8 100644 --- a/docs/website/src/pages/graph.ts +++ b/docs/website/src/pages/graph.ts @@ -631,8 +631,8 @@ function renderResults(status?: 'same' | 'none' | 'error' | 'cancelled') { /* ---------- Overhead lens ---------- */ /* Analysis runs on concrete variants. A family edge only groups the exact variant rules behind it. */ const rules = D.edges as RuleEdge[]; -interface Lens { scope: Scope; limit: ClassId; noIlp: boolean; focus: number | null; dir: 'down' | 'up'; group: number | null } -const lens: Lens = { scope: 'witness', limit: 'unknown', noIlp: false, focus: null, dir: 'down', group: null }; +interface Lens { scope: Scope; limit: ClassId; focus: number | null; dir: 'down' | 'up'; group: number | null } +const lens: Lens = { scope: 'witness', limit: 'unknown', focus: null, dir: 'down', group: null }; const classOrder = CLASSES.map(c => c.id); const SCOPES: readonly { id: Scope; name: string; hint: string }[] = [ { id: 'witness', name: 'Witness', hint: 'Rules that map solutions back to the source. Paths mode searches this scope.' }, @@ -641,17 +641,16 @@ const SCOPES: readonly { id: Scope; name: string; hint: string }[] = [ ]; const vtext = (i: number) => Object.entries(D.nodes[i]!.variant).map(([k, v]) => k + ": " + v).join(" ") || "default"; const vname = (i: number) => display(D.nodes[i]!.name) + (multi(D.nodes[i]!.name) ? " · " + vtext(i) : ""); -const skipIlp = () => new Set(lens.noIlp ? rules.flatMap((r, i) => D.nodes[r.source]!.name === "ILP" || D.nodes[r.target]!.name === "ILP" ? [i] : []) : []); const badge = (cls: ClassId) => { const c = CLASSES.find(x => x.id === cls)!, b = el("span", "gc g-" + cls, c.label); b.title = c.name; return b; }; const nontrivial = (groups: number[][]) => groups.filter(g => g.length > 1).sort((a, b) => b.length - a.length); function lensModel() { - const skip = skipIlp(), active = activeRules(rules, { scope: lens.scope, limit: lens.limit, skip }); + const active = activeRules(rules, { scope: lens.scope, limit: lens.limit }); const links = active.map(i => rules[i]!), fam = familyRules(D.nodes, rules, active); const groups = nontrivial(components(D.nodes.length, links).groups); - const scoped = activeRules(rules, { scope: lens.scope, limit: "unknown", skip }); + const scoped = activeRules(rules, { scope: lens.scope, limit: "unknown" }); const counts = new Map(); scoped.forEach(i => { const c = edgeGrowth(rules[i]!).cls; counts.set(c, (counts.get(c) ?? 0) + 1); }); const baseline = nontrivial(components(D.nodes.length, scoped.map(i => rules[i]!)).groups).length; @@ -716,11 +715,11 @@ const pct = (n: number, d: number) => d ? Math.round(100 * n / d) : 0; function costCard(box: HTMLElement) { const m = model, total = [...m.counts.values()].reduce((a, b) => a + b, 0), limitAt = classOrder.indexOf(lens.limit); const mild = classOrder.slice(0, classOrder.indexOf("quadratic") + 1).reduce((a, c) => a + (m.counts.get(c) ?? 0), 0); - const into = rules.filter(r => r[lens.scope] && D.nodes[r.target]!.name === "ILP").length, scoped = rules.filter(r => r[lens.scope]).length; const card = el("section", "lcard cost"); const hero = el("div", "hero-n"); hero.append(el("span", "num", String(pct(mild, total))), el("span", "of", "%")); - card.append(el("h2", "eyebrow", "Overhead of a reduction"), hero, - el("p", "cap", `of ${total} reductions grow at most quadratically in the source size${into > scoped / 4 ? `. ILP alone receives ${into}.` : "."}`)); + const title = el("h2", "eyebrow", "Overhead of a reduction"); title.title = "Total degree of the target sizes when every source size grows together. A visualization convention, not a runtime bound."; + card.append(title, hero, + el("p", "cap", "of reductions are at most quadratic")); const bar = el("div", "dist"); bar.setAttribute("role", "radiogroup"); bar.setAttribute("aria-label", "Show reductions up to this growth class"); const legend = el("div", "dist-legend"); CLASSES.forEach((c, i) => { @@ -737,8 +736,6 @@ function costCard(box: HTMLElement) { legend.append(key); }); card.append(bar, legend); - const showing = lens.limit === "unknown" ? "Showing every reduction" : `Showing ${m.active.length} · ${CLASSES[limitAt]!.name.toLowerCase()} or cheaper`; - card.append(el("p", "showing", showing)); const seg = el("div", "seg"); seg.setAttribute("role", "radiogroup"); seg.setAttribute("aria-label", "Rule scope"); SCOPES.forEach(x => { const b = el("button", "", x.name); b.type = "button"; b.setAttribute("role", "radio"); b.setAttribute("aria-checked", String(x.id === lens.scope)); b.title = x.hint; @@ -754,7 +751,6 @@ function groupsCard(box: HTMLElement) { const head = el("div", "lcard-head"); head.append(el("h2", "eyebrow", "Mutually reducible")); const count = el("span", "count", m.baseline === m.groups.length ? String(m.groups.length) : `${m.groups.length} of ${m.baseline}`); count.title = "Groups of variants that reduce to each other"; head.append(count); card.append(head); - if (m.baseline !== m.groups.length) card.append(el("p", "cap", `${m.baseline - m.groups.length} fall apart once costlier rules are removed.`)); const list = el("div", "groups"); m.groups.forEach((g, gi) => { const families = [...new Set(g.map(v => D.nodes[v]!.name))], open = lens.group === gi; @@ -765,7 +761,7 @@ function groupsCard(box: HTMLElement) { list.append(b); if (open) { const d = el("ul", "group-detail"); g.slice().sort((a, c) => a - c).forEach(v => d.append(el("li", "", vname(v)))); list.append(d); } }); - if (!m.groups.length) list.append(el("p", "cap", "None under this filter.")); + if (!m.groups.length) list.append(el("p", "cap", "None")); card.append(list); box.append(card); } @@ -774,7 +770,7 @@ function focusCard(box: HTMLElement) { const head = el("div", "lcard-head"); head.append(el("h2", "eyebrow", lens.dir === "down" ? "Reduces to" : "Reduced from")); const clear = el("button", "link", "Clear"); clear.type = "button"; clear.addEventListener("click", () => { lens.focus = null; paintLens(); renderLens(); }); head.append(clear); card.append(head); - card.append(el("p", "focus-name", display(D.nodes[f]!.name)), el("p", "cap", `${multi(D.nodes[f]!.name) ? vtext(f) + " · " : ""}${variants.size} variants in ${byFamily.size} other families`)); + card.append(el("p", "focus-name", display(D.nodes[f]!.name)), el("p", "cap", `${multi(D.nodes[f]!.name) ? vtext(f) + " · " : ""}${variants.size} variants`)); const items = el("div", "reach-list"); [...byFamily].sort((a, b) => b[1].length - a[1].length || a[0].localeCompare(b[0])).forEach(([name, vs]) => { const b = el("button", "reach-row"); b.type = "button"; b.append(el("span", "", display(name)), el("small", "", multi(name) ? `${vs.length}/${families.get(name)!.variants.length}` : "")); @@ -790,13 +786,6 @@ function renderLens() { box.replaceChildren(); if (lens.focus != null) focusCard(box); costCard(box); groupsCard(box); - const about = el("details", "about"); about.append(el("summary", "", "How to read this")); - about.append(el("p", "", "Arrows point from source to target. Colour is the total degree of the target's sizes when every source size grows together: a visualization convention, not a runtime bound. Θ marks exact formulas and O upper bounds.")); - about.append(el("p", "", "Reachability is connectivity among registered reductions; it does not establish solver availability or efficiency. ILP edges are faded on the map because it receives nearly half of all reductions.")); - const ilp = el("label", "check"), cb = el("input"); cb.type = "checkbox"; cb.checked = lens.noIlp; cb.dataset.key = "noilp"; - cb.addEventListener("change", () => { lens.noIlp = cb.checked; lens.focus = null; refreshLens(); }); - ilp.append(cb, el("span", "", "Leave ILP out of the analysis")); about.append(ilp); - box.append(about); if (hadFocus) box.querySelector(`[data-key="${hadFocus}"]`)?.focus({ preventScroll: true }); } @@ -817,7 +806,6 @@ function popLens(v: number) { wrap.append(row); const out = [...model.fam.values()].filter(f => f.source === D.nodes[v]!.name); if (out.length) { - wrap.append(el("p", "pop-sub", "Rules out of this problem")); out.sort((a, b) => classOrder.indexOf(a.cls) - classOrder.indexOf(b.cls)).forEach(f => { const b = el("button", "pop-rule"); b.type = "button"; b.append(badge(f.cls), el("span", "", display(f.target))); b.addEventListener("click", () => openEdgePop(scene.byId.get(f.source + "→" + f.target) as SceneEdge)); @@ -834,7 +822,6 @@ function openEdgePop(edge: SceneEdge) { popNode = null; popAnchor = edge; const pop = $("#pop"); pop.replaceChildren(); const title = el("h2", "", display(f.source) + " → " + display(f.target)); title.id = "pop-title"; pop.append(title); - pop.append(el("p", "hint", `${f.rules.length} variant rule${f.rules.length === 1 ? "" : "s"} in scope`)); [...f.rules].sort((a, b) => classOrder.indexOf(ruleClass(a)) - classOrder.indexOf(ruleClass(b))).forEach(i => { const rule = rules[i]!, g = edgeGrowth(rule), card = el("div", "rule-card"); const head = el("button", "rule-head"); head.type = "button"; @@ -844,10 +831,8 @@ function openEdgePop(edge: SceneEdge) { const dl = el("dl", "growth"); g.fields.forEach(x => { dl.append(el("dt", "", prettyField(x.name)), el("dd", "", x.kind === "unavailable" ? "unavailable" : x.lead)); }); card.append(dl); - card.append(el("small", "acc", g.accuracy === "exact" ? "Θ: every formula is exact" : "O: at least one formula is an upper bound")); pop.append(card); }); - const close = el("button", "pop-details", "Close"); close.type = "button"; close.onclick = () => closePop(); pop.append(close); pop.hidden = false; placePop(); } From be08f4220b82f3688dc573f5d0c854b5c4fa784e Mon Sep 17 00:00:00 2001 From: Xiwei Pan <90967972+isPANN@users.noreply.github.com> Date: Sat, 17 Oct 2026 11:41:48 -0700 Subject: [PATCH 05/50] Quiet the Overhead map: faint edges, hub-only labels, neighbourhood on hover Co-Authored-By: Claude Sonnet 5.5 --- docs/website/src/pages/graph.ts | 17 +++++++++++++---- docs/website/src/styles/graph.css | 9 ++++++++- 2 files changed, 21 insertions(+), 5 deletions(-) diff --git a/docs/website/src/pages/graph.ts b/docs/website/src/pages/graph.ts index d2d8f00d8..c879c3788 100644 --- a/docs/website/src/pages/graph.ts +++ b/docs/website/src/pages/graph.ts @@ -96,9 +96,10 @@ function placeLabels() { scene.classes(scene.nodes, "named"); scene.nodes.filter(important).forEach(n => boxes.push(box(n))); const named: SceneNode[] = []; + const cap = lensOn && lens.focus == null && lens.group == null ? 12 : Infinity; scene.nodes.filter(n => !important(n) && !scene.has(n, "dim")).sort((a,b) => b.deg-a.deg).forEach(n => { const b = box(n); - if (fits(b) && !hit(b)) { boxes.push(b); named.push(n); } + if (named.length < cap && fits(b) && !hit(b)) { boxes.push(b); named.push(n); } }); scene.classes(named, "", "named"); placePop(); @@ -107,6 +108,14 @@ scene.onChange = scheduleLabels; scene.onDrag = () => { scheduleLabels(); placePop(); }; scene.onHover = (n, over) => { scene.classes([n], over ? "" : "hover", over ? "hover" : ""); + if (lensOn && lens.focus == null && lens.group == null) { + const nbrs = families.get(n.id)!.nbrs; + scene.classes(scene.edges, "lit quiet"); + if (over) { + scene.edges.forEach(e => scene.classes([e], "", e.source === n || e.target === n ? "lit" : "quiet")); + scene.nodes.forEach(o => scene.classes([o], "near", o !== n && nbrs.has(o.id) ? "near" : "")); + } else scene.classes(scene.nodes, "near"); + } if (!state.result && !lensOn) { if (over) { scene.classes(scene.elements.filter(e => e !== n && !families.get(n.id)!.nbrs.has(e.id)), "", "dim"); @@ -671,7 +680,7 @@ function reachOf(focus: number) { function paintLens() { const edgeClasses = classOrder.map(c => "e-" + c).join(" "); - scene.classes(scene.elements, "dim ghost route start end nbr off cyc reach pick hub " + edgeClasses); + scene.classes(scene.elements, "dim ghost route start end nbr off cyc reach pick hub lit quiet near " + edgeClasses); const linked = new Set(), cyc = new Set(); model.fam.forEach(f => { linked.add(f.source); linked.add(f.target); }); model.groups.forEach(g => g.forEach(v => cyc.add(D.nodes[v]!.name))); @@ -686,7 +695,7 @@ function paintLens() { scene.classes([edge], "", "e-" + f.cls); if (!picked && !focus && (edge.source.id === "ILP" || edge.target.id === "ILP")) scene.classes([edge], "", "hub"); if ((picked || focus) && !f.rules.some(i => inside(rules[i]!.source) && inside(rules[i]!.target))) scene.classes([edge], "", "dim"); - else if (picked || focus) { lit.add(edge.source.id); lit.add(edge.target.id); } + else if (picked || focus) { lit.add(edge.source.id); lit.add(edge.target.id); scene.classes([edge], "", "lit"); } }); scene.nodes.forEach(node => { const members = families.get(node.id)!.variants; @@ -845,7 +854,7 @@ function setTab(name: "paths" | "overhead") { document.body.classList.toggle("lens", lensOn); closePop(); if (lensOn) { model = lensModel(); paintLens(); renderLens(); frameCore(); } - else { scene.classes(scene.elements, "dim ghost route start end nbr off cyc reach pick hub " + classOrder.map(c => "e-" + c).join(" ")); paintGraph(); } + else { scene.classes(scene.elements, "dim ghost route start end nbr off cyc reach pick hub lit quiet near " + classOrder.map(c => "e-" + c).join(" ")); paintGraph(); } } for (const id of ["paths", "overhead"] as const) { $("#tab-" + id).addEventListener("click", () => setTab(id)); diff --git a/docs/website/src/styles/graph.css b/docs/website/src/styles/graph.css index da15fdd05..b6da1835b 100644 --- a/docs/website/src/styles/graph.css +++ b/docs/website/src/styles/graph.css @@ -262,7 +262,7 @@ button { cursor: pointer; background: none; border: 0; padding: 0; } .lens .edge-hit { pointer-events: stroke; cursor: pointer; } .lens .edge-hit:hover + .scene-edge { stroke-width: 3px; opacity: 1; } .lens :is(.scene-edge, .edge-hit) { vector-effect: non-scaling-stroke; } -.lens .scene-edge { stroke-width: 1.2; opacity: .85; transition: opacity .2s, stroke .2s; } +.lens .scene-edge { stroke-width: 1; opacity: .34; marker-end: none; transition: opacity .2s, stroke .2s; } .lens .scene-edge.off { opacity: 0; } .lens .edge-hit:has(+ .scene-edge.off) { pointer-events: none; } .lens .scene-edge.dim { opacity: .07; } @@ -293,3 +293,10 @@ button { cursor: pointer; background: none; border: 0; padding: 0; } .rule-card .growth { margin: 8px 0 4px; font-size: 12px; } .acc { color: var(--ink-3); font-size: 11.5px; } @media (prefers-reduced-motion: reduce) { .seg-bar, .lens .scene-edge { transition: none; } } + +.lens .scene-edge:not(.lit) { marker-end: none; } +.lens .scene-edge.lit { opacity: 1; stroke-width: 1.8; } +.lens .scene-edge.quiet { opacity: .1; } +.lens .scene-node.near .node-label { visibility: visible; fill: var(--ink); } +.lens .scene-edge.hub { opacity: .05; } +.lens .scene-edge.hub.lit { opacity: 1; } From 419f1e7a18cb111ab12b3d5b86d1d554a6c32637 Mon Sep 17 00:00:00 2001 From: Xiwei Pan <90967972+isPANN@users.noreply.github.com> Date: Sat, 17 Oct 2026 11:58:50 -0700 Subject: [PATCH 06/50] Rebuild the graph page as Explore and Directions Explore is a map-style search over problems and rules with place cards, a layered view by distance from SAT, and a growth legend. Directions is its own mode. Drop italics and the mutually-reducible default panel. Co-Authored-By: Claude Sonnet 5.5 --- docs/website/graph.html | 53 +-- docs/website/src/lib/graph-structure.mts | 45 +++ docs/website/src/pages/graph-scene.ts | 43 ++- docs/website/src/pages/graph.ts | 458 +++++++++++++---------- docs/website/src/styles/graph.css | 180 ++++----- scripts/test_website.py | 168 +++++---- scripts/test_website_structure.mjs | 35 ++ 7 files changed, 604 insertions(+), 378 deletions(-) diff --git a/docs/website/graph.html b/docs/website/graph.html index 9561a2053..b080434e9 100644 --- a/docs/website/graph.html +++ b/docs/website/graph.html @@ -33,35 +33,40 @@
-
-
-

Reduction graph

-
- - +
+
+

Reduction graph

+
+ +
-
-
-
-
- -
-
-
- -
-
- - -
-
-
+
-
+
+
+
+
+
+
+
+
-