Compile Boolean formulas to raw circuit fragments

This file defines a proof-free compiler from BoolFormula trees to appendable CircuitCode.RawCircuit fragments. Given available existing wires, the compiler emits one new gate per formula node. Variables are absolute references into the existing prefix, and the last new wire carries the formula value.

Variables are copied through a duplicated AND gate. Constants use an arbitrary existing wire together with its negation, while formula negation uses the raw gate's free edge-negation flags. Binary formulas are emitted in postorder.

def Complexity.BoolFormula.rawOutputWire (available : ℕ) (formula : BoolFormula) : ℕ

Absolute wire carrying the output of a compiled formula fragment.

Equations

• Complexity.BoolFormula.rawOutputWire available formula = available + formula.size - 1

def Complexity.BoolFormula.compileRaw (available : ℕ) : BoolFormula → CircuitCode.RawCircuit

Compile a formula after available existing wires.

The result is a fragment rather than a complete circuit: it may be appended to an existing raw prefix without renumbering its absolute wire references.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.BoolFormula.compileRaw available (Complexity.BoolFormula.var i) = [Complexity.CircuitCode.RawGate.copy i]
• Complexity.BoolFormula.compileRaw available Complexity.BoolFormula.tru = [Complexity.CircuitCode.RawGate.constant 0 true]
• Complexity.BoolFormula.compileRaw available Complexity.BoolFormula.fls = [Complexity.CircuitCode.RawGate.constant 0 false]