Index of /users/boyer/ftp/bdd

Icon  Name                    Last modified      Size  Description
[DIR] Parent Directory                             -   
[   ] bdd.tar                 23-Jun-1997 10:06  920K  
[   ] bdd.tar.Z               02-Apr-2000 15:03  273K  
[   ] bdd.tar.gz              02-Apr-2000 15:03  181K  

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