Data structure for creating CNF formulae.

Hardcaml combinational logic API using lists of Basic_gate.ts.

Computes information about the one-hotness of a vector. In addition it can compute if no bits are set or more than 1 bit is set.

Labels represent named variables. They contain a uid (unique identifier) which is constructed when the label is created. The name is not used for comparison.

Sequential equivalence checking.