package wax-lib

  1. Overview
  2. Docs
package wax-lib
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

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.