Module Theo.VoidSource

An empty theory.

Used when no theory reasoning is required. BDDs created with Theo.Make(Void) behave like standard BDDs, supporting only boolean variables.

Sourcetype _ t

The type of theory atoms. The type parameter is a phantom type used to distinguish different kinds of atoms (e.g., boolean vs integer) if needed, or ignored if the theory is uniform.

Sourceval equal : _ t -> _ t -> bool

Equality check for atoms. Must be consistent with compare and hash.

Sourceval compare : _ t -> _ t -> int

Total ordering function. Used for set/map operations and canonical ordering in BDDs.

Sourceval hash : _ t -> int

Hash function for atoms. Must be compatible with equal.

Sourceval to_string : _ t -> string

String representation for debugging.