Bdd (Calculemus)

Bdd Module

Namespace: Calculemus
Assembly: Calculemus.dll

Binary decision diagrams (BDDs) using complement edges.

In practice one would use hash tables, but we use abstract finite partial functions here. They might also look nicer imperatively.

Types

Type	Description
bdd	The type of Binary Decision Diagram.
bddnode	The type of binary decision diagram (bdd) node.

Functions and values

Function or value	Description
`bdd_and (arg1, arg2) (m1, m2)` Full Usage: `bdd_and (arg1, arg2) (m1, m2)` Parameters: arg0 : `bdd` arg1 : `func<(int * int), int>` m1 : `int` m2 : `int` Returns: `(bdd * func<(int * int), int>) * int`	Perform an AND operation on BDDs, maintaining canonicity. arg0 : `bdd` arg1 : `func<(int * int), int>` m1 : `int` m2 : `int` Returns: `(bdd * func<(int * int), int>) * int`
`bdd_iff (arg1, arg2) (m1, m2)` Full Usage: `bdd_iff (arg1, arg2) (m1, m2)` Parameters: arg0 : `bdd` arg1 : `func<(int * int), int>` m1 : `int` m2 : `int` Returns: `(bdd * func<(int * int), int>) * int`	Perform an IFF operation on BDDs, maintaining canonicity. arg0 : `bdd` arg1 : `func<(int * int), int>` m1 : `int` m2 : `int` Returns: `(bdd * func<(int * int), int>) * int`
`bdd_imp (arg1, arg2) (m1, m2)` Full Usage: `bdd_imp (arg1, arg2) (m1, m2)` Parameters: arg0 : `bdd` arg1 : `func<(int * int), int>` m1 : `int` m2 : `int` Returns: `(bdd * func<(int * int), int>) * int`	Perform an IMP operation on BDDs, maintaining canonicity. arg0 : `bdd` arg1 : `func<(int * int), int>` m1 : `int` m2 : `int` Returns: `(bdd * func<(int * int), int>) * int`
`bdd_or (arg1, arg2) (m1, m2)` Full Usage: `bdd_or (arg1, arg2) (m1, m2)` Parameters: arg0 : `bdd` arg1 : `func<(int * int), int>` m1 : `int` m2 : `int` Returns: `(bdd * func<(int * int), int>) * int`	Perform an OR operation on BDDs, maintaining canonicity. arg0 : `bdd` arg1 : `func<(int * int), int>` m1 : `int` m2 : `int` Returns: `(bdd * func<(int * int), int>) * int`
`bddtaut fm` Full Usage: `bddtaut fm` Parameters: fm : `formula<prop>` Returns: `bool`	Tautology checking using BDDs. fm : `formula<prop>` Returns: `bool`
`dest_iffdef fm` Full Usage: `dest_iffdef fm` Parameters: fm : `formula<'a>` Returns: `'a * formula<'a>`	fm : `formula<'a>` Returns: `'a * formula<'a>`
`dest_nimp fm` Full Usage: `dest_nimp fm` Parameters: fm : `formula<'a>` Returns: `formula<'a> * formula<'a>`	fm : `formula<'a>` Returns: `formula<'a> * formula<'a>`
`ebddtaut fm` Full Usage: `ebddtaut fm` Parameters: fm : `formula<prop>` Returns: `bool`	Tautology checking using BDDs with an improved setup fm : `formula<prop>` Returns: `bool`
`expand_node arg1 n` Full Usage: `expand_node arg1 n` Parameters: arg0 : `bdd` n : `int` Returns: `bddnode`	Returns the bddnode corresponding to the index `n` of the bdd If a negative index is used the complement of the node is returned. arg0 : `bdd` n : `int` Returns: `bddnode`
`lookup_unique bdd (arg2, arg3, arg4)` Full Usage: `lookup_unique bdd (arg2, arg3, arg4)` Parameters: bdd : `bdd` arg1 : `prop` arg2 : `int` arg3 : `int` Returns: `bdd * int`	Lookup or insertion if not there in unique table. bdd : `bdd` arg1 : `prop` arg2 : `int` arg3 : `int` Returns: `bdd * int`
`mk_bdd ord` Full Usage: `mk_bdd ord` Parameters: ord : `prop -> prop -> bool` Returns: `bdd`	Create a new BDD with a given ordering. ord : `prop -> prop -> bool` Returns: `bdd`
`mk_node bdd (s, l, r)` Full Usage: `mk_node bdd (s, l, r)` Parameters: bdd : `bdd` s : `prop` l : `int` r : `int` Returns: `bdd * int`	Produce a BDD node (old or new). bdd : `bdd` s : `prop` l : `int` r : `int` Returns: `bdd * int`
`mkbdd (arg1, arg2) fm` Full Usage: `mkbdd (arg1, arg2) fm` Parameters: arg0 : `bdd` arg1 : `func<(int * int), int>` fm : `formula<prop>` Returns: `(bdd * func<(int * int), int>) * int`	Formula to BDD conversion. arg0 : `bdd` arg1 : `func<(int * int), int>` fm : `formula<prop>` Returns: `(bdd * func<(int * int), int>) * int`
`mkbdde sfn (arg2, arg3) fm` Full Usage: `mkbdde sfn (arg2, arg3) fm` Parameters: sfn : `func<prop, int>` arg1 : `bdd` arg2 : `func<(int * int), int>` fm : `formula<prop>` Returns: `(bdd * func<(int * int), int>) * int`	Formula to BDD conversion with improved setup sfn : `func<prop, int>` arg1 : `bdd` arg2 : `func<(int * int), int>` fm : `formula<prop>` Returns: `(bdd * func<(int * int), int>) * int`
`mkbdds sfn (arg2, arg3) defs fm` Full Usage: `mkbdds sfn (arg2, arg3) defs fm` Parameters: sfn : `func<prop, int>` arg1 : `bdd` arg2 : `func<(int * int), int>` defs : `(prop * formula<prop>) list` fm : `formula<prop>` Returns: `(bdd * func<(int * int), int>) * int`	sfn : `func<prop, int>` arg1 : `bdd` arg2 : `func<(int * int), int>` defs : `(prop * formula<prop>) list` fm : `formula<prop>` Returns: `(bdd * func<(int * int), int>) * int`
`order arg1 p1 p2` Full Usage: `order arg1 p1 p2` Parameters: arg0 : `bdd` p1 : `prop` p2 : `prop` Returns: `bool`	Extract the ordering field of a BDD. arg0 : `bdd` p1 : `prop` p2 : `prop` Returns: `bool`
`print_bdd arg1` Full Usage: `print_bdd arg1` Parameters: arg0 : `bdd`	arg0 : `bdd`
`restore_iffdef (x, e) fm` Full Usage: `restore_iffdef (x, e) fm` Parameters: x : `'a` e : `formula<'a>` fm : `formula<'a>` Returns: `formula<'a>`	x : `'a` e : `formula<'a>` fm : `formula<'a>` Returns: `formula<'a>`
`sort_defs acc defs fm` Full Usage: `sort_defs acc defs fm` Parameters: acc : `('a * formula<'a>) list` defs : `('a * formula<'a>) list` fm : `formula<'a>` Returns: `('a * formula<'a>) list * formula<'a>`	acc : `('a * formula<'a>) list` defs : `('a * formula<'a>) list` fm : `formula<'a>` Returns: `('a * formula<'a>) list * formula<'a>`
`suitable_iffdef defs (x, q)` Full Usage: `suitable_iffdef defs (x, q)` Parameters: defs : `('a * 'b) list` x : `'c` q : `formula<'a>` Returns: `bool`	defs : `('a * 'b) list` x : `'c` q : `formula<'a>` Returns: `bool`
`thread s g (f1, x1) (f2, x2)` Full Usage: `thread s g (f1, x1) (f2, x2)` Parameters: s : `'a` g : `'b -> 'c * 'd -> 'e` f1 : `'a -> 'f -> 'g * 'c` x1 : `'f` f2 : `'g -> 'h -> 'b * 'd` x2 : `'h` Returns: `'e`	Threading state through. s : `'a` g : `'b -> 'c * 'd -> 'e` f1 : `'a -> 'f -> 'g * 'c` x1 : `'f` f2 : `'g -> 'h -> 'b * 'd` x2 : `'h` Returns: `'e`