package frenetic

  1. Overview
  2. Docs
package frenetic
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

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

module V : HashCmp
module L : Lattice
module R : Result

Signature

Sourcetype 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.

include Core.Comparator.S with type t := t
type comparator_witness
val comparator : (t, comparator_witness) Core_kernel__Comparator.comparator
Sourcetype v = V.t * L.t

The type of a variable in the decision diagram.

Sourcetype r = R.t

The type of the result of a decision diagram

Sourcetype d = private
  1. | Leaf of r
  2. | Branch of {
    1. test : v;
    2. tru : t;
    3. fls : t;
    4. all_fls : t;
    }
Sourcemodule Tbl : Core.Hashtbl.S with type key = t
Sourcemodule BinTbl : Core.Hashtbl.S with type key = t * t
Sourceval get : d -> t
Sourceval unget : t -> d
Sourceval get_uid : t -> int
Sourceval drop : t

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

Sourceval id : t

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

Sourceval const : r -> t

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

Sourceval 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.

Sourceval cond : v -> t -> t -> t

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

Sourceval 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!

Sourceval 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.

Sourceval 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.

Sourceval 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

Sourceval 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)

Sourceval 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.

Sourceval 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.

Sourceval 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.

Sourceval 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.

Sourceval compare : t -> t -> int
Sourceval to_string : t -> string

to_string t returns a string representation of the diagram.

Sourceval clear_cache : preserve:Core.Int.Set.t -> unit

clear_cache () clears the internal cache of diagrams.

Sourceval compressed_size : t -> int

compressed_size t returns the number of nodes in the diagram, duplicates not counted

Sourceval uncompressed_size : t -> int

uncompressed_size t returns the number of nodes in the diagram, duplicates counted

Sourceval 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.

Sourceval refs : t -> Core.Int.Set.t

refs t returns set of subdiagrams in this diagram.

Sourceval serialize : t -> string
Sourceval deserialize : string -> t
Sourceval render : ?format:string -> ?title:string -> t -> unit

Compiles the provided Fdd `t` using `graphviz`, and opens the resulting file.

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct