Translates the given NNF formula as a witness circuit.
Translates the given NNF formula as a witness circuit.
Returns the current atom translation cache as an immutable function.
An immutable map from nnf Atoms to circuit variables.
Translate nnf formula to witness circuit, declares resulting gate as output.
Returns the current expression translation cache as an immutable function.
New free input of the witness circuit corresponding to the key atom.
Outputs of the witness circuit.
Translates NNF expressions to witness circuit for keyAtom.