Circuit dependency graphs -- definitions

The dependency graph of a circuit has one vertex for every primary input, internal gate, and output gate. Each gate-input occurrence contributes an edge from the referenced wire to the gate that reads it. Repeated occurrences of the same wire at the same gate collapse in the graph's edge set, while Circuit.totalFanIn continues to count them with multiplicity.

def Complexity.Circuit.totalFanIn {B : Basis} {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit B N M G) : ℕ

Total number of gate-input occurrences, including output gates.

Equations

• c.totalFanIn = ∑ i : Fin G, (c.gates i).fanIn + ∑ j : Fin M, (c.outputs j).fanIn

@[reducible, inline]

abbrev Complexity.Circuit.DependencyOccurrence {B : Basis} {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit B N M G) : Type

One internal- or output-gate input occurrence in a circuit.

Equations

• c.DependencyOccurrence = ((i : Fin G) × Fin (c.gates i).fanIn ⊕ (j : Fin M) × Fin (c.outputs j).fanIn)

def Complexity.Circuit.dependencyEdge {B : Basis} {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit B N M G) : c.DependencyOccurrence → Fin (N + G + M) × Fin (N + G + M)

The directed dependency edge represented by one gate-input occurrence.

Equations

• c.dependencyEdge (Sum.inl ⟨i, input⟩) = (⟨↑((c.gates i).inputs input), ⋯⟩, ⟨N + ↑i, ⋯⟩)
• c.dependencyEdge (Sum.inr ⟨j, input⟩) = (⟨↑((c.outputs j).inputs input), ⋯⟩, ⟨N + G + ↑j, ⋯⟩)

def Complexity.Circuit.dependencyEdges {B : Basis} {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit B N M G) : Finset (Fin (N + G + M) × Fin (N + G + M))

The finite set of dependency edges. Parallel occurrences collapse here.

Equations

• c.dependencyEdges = Finset.image c.dependencyEdge Finset.univ

def Complexity.Circuit.dependencyGraph {B : Basis} {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit B N M G) : Digraph (Fin (N + G + M))

The directed graph whose edges are the circuit's wire dependencies.

Equations

• c.dependencyGraph = { Adj := fun (source target : Fin (N + G + M)) => (source, target) ∈ c.dependencyEdges }

@[implicit_reducible]

instance Complexity.Circuit.instDecidableRelFinHAddNatAdjDependencyGraph {B : Basis} {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit B N M G) : DecidableRel c.dependencyGraph.Adj

Equations

• c.instDecidableRelFinHAddNatAdjDependencyGraph source target = id inferInstance