package frenetic
Install
Dune Dependency
Authors
Maintainers
Sources
md5=baf754df13a759c32f2c86a1b6f328da
sha512=80140900e7009ccab14b25e244fe7edab87d858676f8a4b3799b4fea16825013cf68363fe5faec71dd54ba825bb4ea2f812c2c666390948ab217ffa75d9cbd29
doc/frenetic.netkat/Frenetic_netkat/Vlr/Make/index.html
Module Vlr.MakeSource
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
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.
include Core.Comparator.S with type t := t
val comparator : (t, comparator_witness) Core_kernel__Comparator.comparatordrop returns the leaf for a drop operation, which is always present as a leaf node
id returns the leaf for the identity operation, which is always present as a leaf node
const r creates a constant diagram out of r. It's essentially a leaf node with a constant.
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.
cond v t f creates a diagram with pattern v, true-branch t and false-branch f.
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.
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) ->
tdp_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.
clear_cache () clears the internal cache of diagrams.
compressed_size t returns the number of nodes in the diagram, duplicates not counted
uncompressed_size t returns the number of nodes in the diagram, duplicates counted
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.