Library
Module
Module type
Parameter
Class
Class type
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:
If the tree is a branch labeled with the variable x
, recursively evaluate
hi
if x = true
, orlo
if x = false
.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.
A 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 cfalse : t
The constant false.
val ctrue : t
The constant true.
branch mgr var hi lo
is the diagram that behaves like hi
when var = true
, and like lo
when var = false
.
O(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.string
val render :
?var_name:(Var.t -> Base.string) ->
?format:Base.string ->
?title:Base.string ->
t ->
Base.unit
id 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.