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