merged contributions by Timothy Bourke

functor, first-class module (no more set_max_var)
new functions restrict, constrain, and restriction
new function print_to_dot

.gitignore

@@ -0,0 +1,17 @@
+Makefile
+config.status
+parser.output
+autom4te.cache/
+config.log
+.depend
+configure
+lexer.ml
+parser.mli
+parser.ml
+*.cm*
+*.annot
+*.o
+*.opt
+version.ml
+test.dot
+test.pdf

CHANGES

@@ -0,0 +1,23 @@
+November 13, 2018 (VERSION 0.4)
+-------------------------------
+ o no more set_max_var -> a functor Make and a function 'make' instead
+ o new function restrict
+ o new functions constrain and restriction
+ o extend print_to_dot and display with optional print_var argument
+All this contributed by Timothy Bourke (tbrk@github)
+
+February 2, 2010 (version 0.3)
+------------------------------
+ o new function random_sat
+ o new example in tiling.ml (tiling the 8x8 chessboard with 2x1 dominoes *)
+ o init removed and subsumed by set_max_var
+ o improved efficiency (one node table for each variable)
+
+July 16, 2009 (version 0.2)
+---------------------------
+ o fixed bug in count_sat (unused variables below the top variable where not
+   taken into account)
+
+June 7, 2008 (version 0.1)
+--------------------------
+ o LGPL license, with special exception for linking (see LICENSE)

Makefile.in

@@ -0,0 +1,224 @@
+##########################################################################
+#                                                                        #
+#  Copyright (C) Jean-Christophe Filliatre                               #
+#                                                                        #
+#  This software is free software; you can redistribute it and/or        #
+#  modify it under the terms of the GNU Lesser General Public            #
+#  License version 2.1, with the special exception on linking            #
+#  described in file LICENSE.                                            #
+#                                                                        #
+#  This software is distributed in the hope that it will be useful,      #
+#  but WITHOUT ANY WARRANTY; without even the implied warranty of        #
+#  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  #
+##########################################################################
+
+# where to install the binaries
+prefix=@prefix@
+exec_prefix=@exec_prefix@
+BINDIR=@bindir@
+
+# where to install the man page
+MANDIR=@mandir@
+
+# other variables set by ./configure
+OCAMLC   = @OCAMLC@
+OCAMLOPT = @OCAMLOPT@
+OCAMLDEP = @OCAMLDEP@
+OCAMLLEX = @OCAMLLEX@
+OCAMLYACC= @OCAMLYACC@
+OCAMLLIB = @OCAMLLIB@
+OCAMLBEST= @OCAMLBEST@
+OCAMLVERSION = @OCAMLVERSION@
+OCAMLWEB = @OCAMLWEB@
+OCAMLWIN32 = @OCAMLWIN32@
+EXE = @EXE@
+
+INCLUDES =
+BFLAGS = -g $(INCLUDES)
+OFLAGS = $(INCLUDES)
+
+# main target
+#############
+
+NAME = bdd
+
+all: bdd_sat.opt bench_prop.opt
+
+.PHONY: check
+check: check.opt
+	./check.opt
+
+check.opt: bdd.cmx prop.cmx parser.cmx lexer.cmx check.cmx
+	$(OCAMLOPT) $(OFLAGS) -o $@ $^
+
+test.opt: bdd.cmx prop.cmx parser.cmx lexer.cmx bench_prop.cmx test.cmx
+	$(OCAMLOPT) $(OFLAGS) -o $@ $^
+
+bdd_sat.opt: bdd.cmx prop.cmx parser.cmx lexer.cmx bdd_sat.cmx
+	$(OCAMLOPT) $(OFLAGS) -o $@ unix.cmxa $^
+
+bench_prop.opt: bdd.cmx prop.cmx bench_prop.cmx
+	$(OCAMLOPT) $(OFLAGS) -o $@ $^
+
+queen.opt: bdd.cmx queen.cmx
+	$(OCAMLOPT) $(OFLAGS) -o $@ $^
+
+tiling.opt: bdd.cmx tiling.cmx
+	$(OCAMLOPT) $(OFLAGS) -o $@ $^
+
+path.opt: bdd.cmx path.cmx
+	$(OCAMLOPT) $(OFLAGS) -o $@ $^
+
+# bytecode and native-code compilation
+######################################
+
+CMO = bdd.cmo lexer.cmo parser.cmo
+CMX = $(CMO:.cmo=.cmx)
+
+GENERATED = version.ml lexer.ml parser.ml
+
+byte: $(CMO)
+opt: $(CMX)
+
+VERSION=0.4
+
+version.ml: Makefile
+	echo "let version = \""$(VERSION)"\"" > version.ml
+	echo "let date = \""`date`"\"" >> version.ml
+
+# installation
+##############
+
+install-indep:
+	mkdir -p $(BINDIR)
+	mkdir -p $(MANDIR)/man1
+	cp -f $(NAME).1 $(MANDIR)/man1
+
+install: install-indep
+	cp -f $(NAME).$(OCAMLBEST) $(BINDIR)/$(NAME)$(EXE)
+
+install-byte: install-indep
+	cp -f $(NAME).byte $(BINDIR)/$(NAME)$(EXE)
+
+install-opt: install-indep
+	cp -f $(NAME).opt $(BINDIR)/$(NAME)$(EXE)
+
+# headers
+#########
+
+.PHONY: headers
+headers:
+	headache -c misc/headache_config.txt -h misc/header.txt \
+		Makefile.in configure.in *.ml *.mli *.mll *.mly
+
+# documentation
+###############
+
+DOCFILES=manual.ps manual.html
+
+doc: $(DOCFILES)
+
+# export
+########
+
+EXPORTDIR=$(NAME)-$(VERSION)
+TAR=$(EXPORTDIR).tar
+TGZ=$(TAR).gz
+
+FTP = $$HOME/WWW/ftp/ocaml/bdd
+
+FILES = *.ml* Makefile.in configure configure.in   \
+	.depend README LICENSE CHANGES
+
+.PHONY: export
+
+export: export/$(TGZ)
+	cp README LICENSE CHANGES export/$(TGZ) $(FTP)
+	caml2html -d $(FTP) bdd.mli bdd.ml
+
+export/$(TGZ):
+	mkdir -p export/$(EXPORTDIR)
+	cp $(FILES) export/$(EXPORTDIR)
+	cd export ; tar cf $(TAR) $(EXPORTDIR) ; gzip -f --best $(TAR)
+
+
+# generic rules
+###############
+
+.SUFFIXES: .mli .ml .cmi .cmo .cmx .mll .mly .tex .dvi .ps .html
+
+.mli.cmi:
+	$(OCAMLC) -c $(BFLAGS) $<
+
+.ml.cmo:
+	$(OCAMLC) -c $(BFLAGS) $<
+
+.ml.o:
+	$(OCAMLOPT) -c $(OFLAGS) $<
+
+.ml.cmx:
+	$(OCAMLOPT) -c $(OFLAGS) $<
+
+.mll.ml:
+	$(OCAMLLEX) $<
+
+.mly.ml:
+	$(OCAMLYACC) -v $<
+
+.mly.mli:
+	$(OCAMLYACC) -v $<
+
+.tex.dvi:
+	latex $< && latex $<
+
+.dvi.ps:
+	dvips $< -o $@
+
+.tex.html:
+	hevea $<
+
+# Emacs tags
+############
+
+tags:
+	find . -name "*.ml*" | sort -r | xargs \
+	etags "--regex=/let[ \t]+\([^ \t]+\)/\1/" \
+	      "--regex=/let[ \t]+rec[ \t]+\([^ \t]+\)/\1/" \
+	      "--regex=/and[ \t]+\([^ \t]+\)/\1/" \
+	      "--regex=/type[ \t]+\([^ \t]+\)/\1/" \
+              "--regex=/exception[ \t]+\([^ \t]+\)/\1/" \
+	      "--regex=/val[ \t]+\([^ \t]+\)/\1/" \
+	      "--regex=/module[ \t]+\([^ \t]+\)/\1/"
+
+# Makefile is rebuilt whenever Makefile.in or configure.in is modified
+######################################################################
+
+Makefile: Makefile.in config.status
+	./config.status
+
+config.status: configure
+	./config.status --recheck
+
+configure: configure.in
+	autoconf
+
+# clean
+#######
+
+clean::
+	rm -f *.cm[iox] *.o *~
+	rm -f $(GENERATED) parser.output
+	rm -f $(NAME).byte $(NAME).opt
+	rm -f *.aux *.log $(NAME).tex $(NAME).dvi $(NAME).ps
+
+dist-clean distclean:: clean
+	rm -f Makefile config.cache config.log config.status
+
+# depend
+########
+
+.depend depend:: $(GENERATED)
+	rm -f .depend
+	$(OCAMLDEP) $(INCLUDES) *.ml *.mli > .depend
+
+include .depend

README.md

@@ -1,2 +1,35 @@
 # ocaml-bdd
 A simple BDD library for OCaml
+
+This is a simple implementation of a BDD library for OCaml,
+mostly for teaching and quick experiment purposes.
+
+Files are:
+
+- bdd.ml: the BDD library; bdd.mli should be self-explanatory
+
+- check.ml: a quick check; "make check" compiles and runs it
+
+- prop.mli, lexer.mll and parser.mly: propositional logic, with a parser,
+  used to test the Bdd library; see check.ml for examples
+
+- bench_prop.ml: various ways of generating valid propositional formulae;
+  compiled as binary bench_prop.opt
+
+- bdd_sat.ml: a propositional tautology checker using Bdd
+  compiled as binary bdd_sat.opt
+
+  these two binaries can be combined as follows:
+
+	./bench_prop.opt -pigeon-p 7 | ./bdd_sat.opt
+	1: valid user time: 0.60
+	table length: 100003 / nb. entries: 2 / sum of bucket length: 20679
+	smallest bucket: 0 / median bucket: 0 / biggest bucket: 3
+
+- queen.ml: computes the number of solutions to the n-queens problem, using
+  a propositional formula (this is not an efficient way to solve this problem,
+  simply another way to test the Bdd library); compile with "make queen.opt"
+  and run as
+
+	./queen.opt 8
+	There are 92 solutions