Make (frenetic.netkat.Frenetic

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.

Parameters

Signature

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.

type v = V.t * L.t

The type of a variable in the decision diagram.

type r = R.t

The type of the result of a decision diagram

type d = private

| Leaf of r

| Branch of {

test : v;

tru : t;

fls : t;

all_fls : t;

}

module Tbl : Core.Hashtbl.S with type Tbl.key = t

module BinTbl : Core.Hashtbl.S with type BinTbl.key = t * t

val get : d ‑> t

val unget : t ‑> d

val get_uid : t ‑> int

val drop : t

drop returns the leaf for a drop operation, which is always present as a leaf node

val id : t

id returns the leaf for the identity operation, which is always present as a leaf node

val const : r ‑> t

const r creates a constant diagram out of r. It's essentially a leaf node with a constant.

val atom : v ‑> r ‑> r ‑> t

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.

val cond : v ‑> t ‑> t ‑> t

cond v t f creates a diagram with pattern v, true-branch t and false-branch f.

val unchecked_cond : v ‑> t ‑> t ‑> t

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!

val restrict : v list ‑> t ‑> t

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.

val sum : t ‑> t ‑> t

sum a b returns the disjunction of the two diagrams. The sum operation on the r type is used to combine leaf nodes.

val prod : t ‑> t ‑> t

prod a b returns the conjunction of the two diagrams. The prod operation on the r type is used to combine leaf nodes.

val map : f:(r ‑> t) ‑> g:(v ‑> t ‑> t ‑> t) ‑> t ‑> t

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

val map_r : f:(r ‑> r) ‑> t ‑> t

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)

val fold : f:(r ‑> 'a) ‑> g:(v ‑> 'a ‑> 'a ‑> 'a) ‑> t ‑> 'a

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.

val equal : t ‑> t ‑> bool

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.

val sum : t ‑> t ‑> t

sum a b returns the disjunction of the two diagrams. The sum operation on the r type is used to combine leaf nodes.

val prod : t ‑> t ‑> t

prod a b returns the conjunction of the two diagrams. The prod operation on the r type is used to combine leaf nodes.

val compare : t ‑> t ‑> int

val to_string : t ‑> string

to_string t returns a string representation of the diagram.

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 refs : t ‑> Core.Int.Set.t

refs t returns set of subdiagrams in this diagram.