package hardcaml_verify

  1. Overview
  2. Docs

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.

In actual hardware using popcount might be better as it can be formulated as a tree with log depth. This implementation has depth O(width vector) but is small and simple.

It's primary purpose is as an efficient check for proving SAT properties.

module Make (Comb : Hardcaml.Comb.S) : sig ... end