Returns the current expression translation cache as an immutable function.
Generates a witness circuit from the nnf formula for each atom of the nnf.
Witness translators map.
Returns the current expression translation cache as an immutable function.
Witness circuit translation function.