Here is the code for a minimal BDD manager written in Ocaml: tinybdd.ml.
Build and use instructions
ocamlc tinybdd.ml ocaml tinybdd.cmo # open Tinybdd;;
The commands above compile the code, and launch a shell that first executes tinybdd.ml, then asks for further input. You can play more with it. Here is an example of an interactive session:
> ocamlc -g tinybdd.ml
> ocaml tinybdd.cmo
Objective Caml version 3.10.0
# open Tinybdd;;
# let a = m#bdd_literal 2;;
val a : int = 2
# let b = m#bdd_literal 5;;
val b : int = 3
# let c = m#bdd_and a b;;
val c : int = 4
# m#print_bdd c;;
(x_2 = 0:
(false))
(x_2 = 1:
(x_5 = 0:
(false))
(x_5 = 1:
(true))
)
- : unit = ()
# m#print_bdd_table ;;
0) Var: 0 F: 0 T: 0
1) Var: 0 F: 0 T: 0
2) Var: 2 F: 0 T: 1
3) Var: 5 F: 0 T: 1
4) Var: 2 F: 0 T: 3
- : unit = ()
#
The Assignment
You need to write the following class methods:
bdd_not : int -> int, so that bdd_not b computes the negation (complementation) of the bdd b.
bdd_replace : int -> int -> int -> int, so that bdd_replace b x y replaces all occurrences of variable x with variable y in b, i.e., it computes b[y/x].
bdd_equant : int -> int -> int, so that bdd_equant b x existentially quantifies x in b, that is, computes b[false/x] or b[true/x]. Note: do not use this method; try to compute bdd_equant b x in a single pass!
Email me a single .ml file that contains the above definitions, along with some simple testing code for the required functions (see the source file for an example).
The catches
I am not 100% sure that my code is correct; you will have to fix it as part of the assignment. Ocaml has a very nice compiler available, called ocamldebug; if you run into trouble, use it.
ocamlc -g tinybdd.ml ocamldebug a.out
Note that in this way, you cannot use the interactive Ocaml shell.