This directory contains the code and data files noted in the article "Introduction to the OBDD Algorithm for the ATP Community" by J Strother Moore which appeared in the Journal of Automated Reasoning, 12 33-45, 1994. To run the benchmarks you will need, in addition to this file, a copy of Gnu Common Lisp (GCL, which used to be called "Austin Kyoto Common Lisp" or "AKCL"). To get GCL, see /pub/gcl/README. You may get this file by ftp from the machine ftp.cli.com. Login as user "anonymous" and give your own name and address as the password, e.g., ("Smith@cs.udelphi.edu"). Once in, FTP the file /pub/bdd/bdd.tar.Z . Then uncompress the file and run tar on it. There is also a 'gzip' version of the tar file in /pub/bdd/bdd.tar.gz . You will then find the following files init.lsp ; \ acl2.lisp ; | a stripped-down Acl2 kernel axioms-akcl.lisp ; / can.lisp ; the OBDD canonicalizer plus two subdirectories, cath and ex. The subdirectories contain IEEE benchmark files cath/add1.be cath/add2.be cath/add3.be cath/add4.be cath/addsub.be ex/mul03.be ex/mul04.be ex/mul05.be ex/mul06.be ex/mul07.be ex/mul08.be ex/rip02.be ex/rip04.be ex/rip06.be ex/rip08.be ex/transp.be ex/ztwaalf1.be ex/ztwaalf2.be CAUTIONARY NOTE: The OBDD work is written in an extension of an applicative subset of Common Lisp, called Acl2, under development at Computational Logic, Inc. In order to make the OBDD code available, a stripped down version of Acl2, containing just the necessary extension to Common Lisp, has been produced. This kernel was produced very quickly and without our usual care, simply to run the OBDD benchmarks. It should not be trusted in the way we intend Acl2 eventually to be trusted. To run my OBDD algorithm on the benchmark files, starting from the source files, proceed as follows. (1) Connect to the directory containing these files. (2) Fire up GCL (AKCL). Because one of the files is named init.lsp, GCL will automatically load it when started. That will cause acl2.lisp to be loaded as well. (3) (in-package "ACL2"), making ACL2 the current package. (4) (compile-acl2-toothbrush), compiling the Acl2 kernel. This will produce some compiler notes, but no warnings or errors. (5) (load-acl2-toothbrush), to load the Acl2 kernel (6) (load "can.lisp"), to make all macro definitions available. (7) (proclaim '(optimize (safety 0) (space 0) (speed 3))) to set the compiler optimization switches to produce fast code. (8) (proclaim-file "can.lisp"), proclaiming the functions in can.lisp (9) (compile-file "can.lisp"), to compile can.lisp. This will produce some compile notes but no warnings or errors. (10) (load "can"), to load the compiled code. (11) (cbfs), to run the benchmark files. In the future, you may simply execute steps (1), (2), (3), (10), and (11) to carry out the tests again. J Strother Moore