Variable-Lattice-Result
This module implements a variant of a binary decision diagrams. Rather than representing boolean-valued functions over boolean variables, this data structure represents functions that take on values in a semi-ring, and whose variables are assigned values from a lattice, i.e., that are partially ordered.
type t
= private int
A decision diagram index. All diagrams and subdiagrams within it are given an
index. You can convert this to a tree with unget
, and from a tree with get
.
val get_uid : t ‑> int
atom v t f
creates a diagram that checks the variable assignment
v
holds and returns the result t
if it does hold, and the result f
otherwise.
Unsafe!! unchecked_cond v t f
behaves like cond v t f
, but always puts the pattern v
in the root node, without ensuring the FDD-ordering invariant is enforced. Only use this if you know what you are doing!
restrict vs t
returns a diagram derived from t
and that agrees with
t
when every variable assignment v
in vs
is true. This will eliminate
the variables in vs
from the diagram, if present.
This function assumes that a variable will only appear once in the list of variable assignments. If the list assigns multiple values to a variable, then the behavior is unspecified.
sum a b
returns the disjunction of the two diagrams. The sum
operation on the r
type is used to combine leaf nodes.
prod a b
returns the conjunction of the two diagrams. The prod
operation on the r
type is used to combine leaf nodes.
map f h t
traverses t in post order and first maps the leaves using
f, and then the internal nodes using h, producing a modified diagram.
val dp_map : f:(r ‑> t) ‑> g:(v ‑> t ‑> t ‑> t) ‑> t ‑> find_or_add:(t ‑> default:(unit ‑> t) ‑> t) ‑> t
dp_map f h cache t
is equal to map f h t
, but uses cache
for memoization
map_r f t
returns a diagram with the same structure but whose leaf
nodes have been modified according the function f
.
This function can be used as a general form of negation. For example, if
the r
type were bool
, one could implement negation in the following
way:
let neg = map_r (fun r -> not r)
fold f g t
traverses the diagram, replacing leaf nodes with
applications of f
to the values that they hold, and branches on
variables with applications of g
.
equal a b
returns whether or not the two diagrams are structurally
equal.
If two diagrams are structurally equal, then they represent the
same combinatorial object. However, if two diagrams are not equal, they
still may represent the same combinatorial object. Whether or not this is
the case depends on they behavior of the type v
.
sum a b
returns the disjunction of the two diagrams. The sum
operation on the r
type is used to combine leaf nodes.
prod a b
returns the conjunction of the two diagrams. The prod
operation on the r
type is used to combine leaf nodes.
val clear_cache : preserve:Core.Int.Set.t ‑> unit
clear_cache ()
clears the internal cache of diagrams.
val compressed_size : t ‑> int
compressed_size t
returns the number of nodes in the diagram, duplicates not counted
val uncompressed_size : t ‑> int
uncompressed_size t
returns the number of nodes in the diagram, duplicates counted
val to_dot : t ‑> string
to_dot t
returns a string representation of the diagram using the DOT
graph description language. The result of this function can be rendered
using Graphviz or any other program that supports the DOT language.
val serialize : t ‑> string
val deserialize : string ‑> t
val render : ?format:string ‑> ?title:string ‑> t ‑> unit
Compiles the provided Fdd `t` using `graphviz`, and opens the resulting file.