Bdd (p.bdd.0.5.doc.bdd.Bdd)

Sourcetype variable = int

A variable is an integer, ranging from 1 to max_var (within a BDD module).

Sourcemodule BddVarMap : Map.S with type key = variable

Module providing general-purpose map data structures indexed by BDD variables.

Sourcetype formula =

| Ffalse
| Ftrue
| Fvar of variable
| Fand of formula * formula
| For of formula * formula
| Fimp of formula * formula
| Fiff of formula * formula
| Fnot of formula
| Fite of formula * formula * formula

Sourcemodule type BDD = sig ... end

Binary Decision Diagrams (BDDs)

Sourcemodule Make (X : sig ... end) : BDD

Binary Decision Diagrams (BDDs)

Source

val make : 
  ?print_var:(Format.formatter -> variable -> unit) ->
  ?size:int ->
  int ->
  (module BDD)

Creates a BDD module with a given maximum number of variables. Additionally, the size of the internal nodes table for each variable can be specified. Each table has a default size (7001) and is resized when necessary (i.e. when too many collisions occur). The print_var argument can be used to associate names with variables (by default it gives "x1", "x2", ...).