Leaf and connective circuits for unbounded formula compilation #
Constants, literals, and unbounded connectives each use one output gate and no internal gates. Literal negation uses the circuit model's free edge flags.
def
Complexity.AC0Formula.constantCircuit
{N : ℕ}
[NeZero N]
(value : Bool)
:
Circuit Basis.unboundedAndOr N 1 0
A nullary AND or OR gate computes a Boolean constant.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Complexity.AC0Formula.literalCircuit
{N : ℕ}
[NeZero N]
(literal : Literal N)
:
Circuit Basis.unboundedAndOr N 1 0
A unary AND gate with an edge flag computes a signed literal.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Complexity.AC0Formula.connectiveCircuit
{N : ℕ}
[NeZero N]
(op : AndOrOp)
:
Circuit Basis.unboundedAndOr N 1 0
One unbounded gate combines all primary inputs by AND or OR.
Equations
- One or more equations did not get rendered due to their size.