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