# Module Bdd

`module Bdd: `sig` .. `end``
Binary Decision Diagrams (BDDs)

* high-level functions
`type `('a, 'k)` node `
Multi-Terminal BDD nodes with leaves in `'a` and decision nodes labelled with `'k` (keys)
`type `('a, 'k)` mem `
memories for BDDs nodes (required to ensure unicity)
`val init : `('a -> int) -> ('a -> 'a -> bool) -> ('a, 'k) mem``
empty memory, with given hash and equality functions for leaves
`val constant : `('a, 'k) mem -> 'a -> ('a, 'k) node``
constant BDD (leaf)
`val unary : `('b, 'k) mem -> ('a -> 'b) -> ('a, 'k) node -> ('b, 'k) node``
applying a unary function to a BDD
`val binary : `('c, 'k) mem ->       ('a -> 'b -> 'c) ->       ('a, 'k) node -> ('b, 'k) node -> ('c, 'k) node``
applying a binary function to two BDDs (the standard "apply" function)
`val hide : `('a, 'k) mem ->       'k ->       (('a, 'k) node -> ('a, 'k) node -> ('a, 'k) node) ->       ('a, 'k) node -> ('a, 'k) node``
hide a given key, by using the given function to resolve choices
`val walk : `((('a, 'k) node -> unit) -> ('a, 'k) node -> unit) ->       ('a, 'k) node -> unit``
walking recursively through a BDD, ensuring that a given node is visited at most once
`val partial_apply : `('a, 'k) mem ->       ('k -> bool option) -> ('a, 'k) node -> ('a, 'k) node``
partially apply a BDD, by using the given function to resolve nodes
`type `('a, 'k)` unifier = `(('k * bool) list -> 'a -> 'a -> unit) ->       ('a, 'k) node -> ('a, 'k) node -> unit` `
BDD unifying functions
`val unify_naive : `bool -> ('a, 'k) unifier``
naive unifier where a set of pairs of nodes is stored. The Boolean argument indicates whether to trace operations or not
`val unify_dsf : `bool -> ('a, 'k) unifier``
union-find based unifier where a forest of pointers is stored. The Boolean argument indicates whether to trace operations or not

* Boolean formulas
`type key = `char` `
type of variables
`type formula = `(bool, key) node` `
symbolic Boolean formulas
`val neg : `formula -> formula``
the various connectives
`val dsj : `formula -> formula -> formula``
`val cnj : `formula -> formula -> formula``
`val xor : `formula -> formula -> formula``
`val iff : `formula -> formula -> formula``
`val bot : `formula``
the two constants
`val top : `formula``
`val var : `key -> formula``
literals: a single variable, or the negation of a variable
`val rav : `key -> formula``
`val witness : `(bool, 'k) node -> ('k * bool) list``
witness assignation for a satisfiable formula
`val times : `('a, 'k) mem ->       ('a, 'k) node ->       (bool, 'k) node -> ('a, 'k) node -> ('a, 'k) node``
`times m z f n` multiplies the BDD `n` by the formula `f`, using `z` where `f` is false
`val print_formula : `int -> formula Common.formatter``
pretty-printing a symbolic formula (the first argument specifies the current level, for parentheses)

* low-level functions
``type ('a, 'k) descr = private ``
 `|` `V of 'a` `|` `N of 'k * ('a, 'k) node * ('a, 'k) node`
internal private type for nodes
`val head : `('a, 'k) node -> ('a, 'k) descr``
explicit description of a given node
`val tag : `('a, 'k) node -> int``
identifier of a BDD node (unique w.r.t. a given memory)
`val hash : `('a, 'k) node -> int``
hash of a BDD node
`val node : `('a, 'k) mem ->       'k -> ('a, 'k) node -> ('a, 'k) node -> ('a, 'k) node``
low-level node creation function, variable ordering is not enforced
`val reset_caches : `unit -> unit``
reset all memoisation caches