package hardcaml_verify

  1. Overview
  2. Docs

Module Hardcaml_verify_kernel.TseitinSource

Sourcemodule type S = sig ... end
Sourcemodule Make (B : S) : sig ... end

Conversion functions from boolean gates to Tseitin form. The first argument to each function is the newly introduced sat literal for this gate, which should be referenced by its fanouts. The return value is the corresponding CNF.

OCaml

Innovation. Community. Security.