Decision Diagrams (DDs).
This module serves as the base for the BDD and IDD modules. It provides hash-consed decision trees, but does not enforce any structural invariants on these trees beyond guranteeing that structural equality coincides with physical equality.
A decision diagram (DD) is a finite binary tree whose leaves are labeled with the constants true or false, and whose branches are labeled with boolean variables. Each branch has two subtrees hi and lo for the cases that the variable is true or false, respectively.
Given an assignment of booleans to the variables, one can evaluate such a tree in the following way:
The module enforces a key invariant : If u : t and v : t were constructed using the same manager, then id u = id v if and only if u and v are structurally equal (ignoring IDs). In other words, all DDs built using the same manager are hash consed .
type t = private | True | False | Branch of {var : Var.t ;the variable on which to branch
hi : t ;subdiagram for case var = true
lo : t ;subdiagramm for case var = false
id : Base.int;unique identifier for this diagram
}
The type of a decision diagram (DD).
type managerA DD manager mgr : manager encapsulates all state required for DD construction. In particular, it is required by the branch function to allocate unique identifiers for each DD.
val manager : Base.unit -> manager Initialize a fresh manager
val cfalse : t The constant false.
val ctrue : t The constant true.
val branch : manager -> Var.t -> t -> t -> t branch mgr var hi lo is the diagram that behaves like hi when var = true, and like lo when var = false.
val equal : t -> t -> Base.boolO(1) structural equality.
PRECONDITION : The result of equal u v is only defined when u and v were built using the same manager. Otherwise, the result is arbitrary.
val to_string : ?var_name:(Var.t -> Base.string) -> t -> Base.stringval render : ?var_name:(Var.t -> Base.string) -> ?format:Base.string -> ?title:Base.string -> t -> Base.unitval id : t -> Base.intid u is an integer that is guranteed to be unique to the the diagram u. In particular, the following invariant holds whenever u and v were constructed using the same manager: id u = id v iff the trees u and v are structurally equal (ignoring IDs). Thus, one can use the IDs to test for equality in O(1). IDs are also useful for memoizing functions on DDs.
val index : t -> Base.intThe index of a diagram is the index of its top-most variable, or -1 if the diagram is a leaf.