From 21cdee5e786902e42052b5af33c5d0cbdd270677 Mon Sep 17 00:00:00 2001 From: zapashcanon Date: Thu, 13 Dec 2018 06:01:48 +0100 Subject: [PATCH] switch to dune --- .gitignore | 20 +-- Makefile | 20 +++ Makefile.in | 224 ----------------------------- README.md | 63 +++++--- bdd.opam | 17 +++ configure.in | 145 ------------------- dune-project | 2 + bdd.ml => lib/bdd.ml | 41 +++--- bdd.mli => lib/bdd.mli | 0 bench_prop.ml => lib/bench_prop.ml | 26 +--- lib/dune | 17 +++ lexer.mll => lib/lexer.mll | 0 parser.mly => lib/parser.mly | 0 prop.ml => lib/prop.ml | 0 misc/headache_config.txt | 10 -- misc/header.txt | 11 -- bdd_sat.ml => test/bdd_sat.ml | 0 test/bench_prop_cli.ml | 26 ++++ check.ml => test/check.ml | 0 test/dune | 38 +++++ path.ml => test/path.ml | 9 +- queen.ml => test/queen.ml | 8 +- test.ml => test/test.ml | 64 ++++----- tiling.ml => test/tiling.ml | 0 24 files changed, 234 insertions(+), 507 deletions(-) create mode 100644 Makefile delete mode 100644 Makefile.in create mode 100644 bdd.opam delete mode 100644 configure.in create mode 100644 dune-project rename bdd.ml => lib/bdd.ml (93%) rename bdd.mli => lib/bdd.mli (100%) rename bench_prop.ml => lib/bench_prop.ml (76%) create mode 100644 lib/dune rename lexer.mll => lib/lexer.mll (100%) rename parser.mly => lib/parser.mly (100%) rename prop.ml => lib/prop.ml (100%) delete mode 100644 misc/headache_config.txt delete mode 100644 misc/header.txt rename bdd_sat.ml => test/bdd_sat.ml (100%) create mode 100644 test/bench_prop_cli.ml rename check.ml => test/check.ml (100%) create mode 100644 test/dune rename path.ml => test/path.ml (88%) rename queen.ml => test/queen.ml (89%) rename test.ml => test/test.ml (61%) rename tiling.ml => test/tiling.ml (100%) diff --git a/.gitignore b/.gitignore index 1b1f2f3..ac1ffb2 100644 --- a/.gitignore +++ b/.gitignore @@ -1,17 +1,3 @@ -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 +_build +*merlin +*.install diff --git a/Makefile b/Makefile new file mode 100644 index 0000000..174ea43 --- /dev/null +++ b/Makefile @@ -0,0 +1,20 @@ +build: + dune build @all + +doc: + dune build @doc + +clean: + dune clean + +test: + dune runtest --force + +install: + dune build @install + dune install + +uninstall: + dune uninstall + +.PHONY: test diff --git a/Makefile.in b/Makefile.in deleted file mode 100644 index 6dd12dd..0000000 --- a/Makefile.in +++ /dev/null @@ -1,224 +0,0 @@ -########################################################################## -# # -# 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 diff --git a/README.md b/README.md index 3101d35..c35ddad 100644 --- a/README.md +++ b/README.md @@ -1,35 +1,56 @@ # 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: +## Build -- bdd.ml: the BDD library; bdd.mli should be self-explanatory +You need `dune` on your system. If you don't have it, install `opam` then try `opam install dune`. -- check.ml: a quick check; "make check" compiles and runs it +To build everything: -- prop.mli, lexer.mll and parser.mly: propositional logic, with a parser, - used to test the Bdd library; see check.ml for examples +```sh +make +``` -- bench_prop.ml: various ways of generating valid propositional formulae; - compiled as binary bench_prop.opt +It will build these libraries: -- bdd_sat.ml: a propositional tautology checker using Bdd - compiled as binary bdd_sat.opt +- `bdd`: the main library - `lib/bdd.mli` should be self-explanatory +- `prop`: propositional logic, with a parser, used to test the main library - see `check` for example +- `bench_prop`: various ways of generating valid propositional formulae - these two binaries can be combined as follows: +Many executables: - ./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 +- `test`: tests producing graphical output - you'll need the `graphviz` and `gv` packages from your distribution +- `tiling` +- `bdd_sat`: a propositional tautology checker using `bdd` +- `queen`: 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) +- `path` +- `check`: a quick check +- `bench_prop_cli`: generate valide propositional formulae from command line -- 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 +To run any of them, let's say `check`, do: - ./queen.opt 8 - There are 92 solutions +```sh +dune exec test/check.exe +``` + +You can combine some of them, e.g.: + +```sh +dune exec test/bench_prop_cli -pigeon-p 7 | dune exec test/bdd_sat.exe +``` + +## Test + +You can run tests using: + +```sh +make test +``` + +## Install + +```sh +make install +``` diff --git a/bdd.opam b/bdd.opam new file mode 100644 index 0000000..37a8c56 --- /dev/null +++ b/bdd.opam @@ -0,0 +1,17 @@ +opam-version: "2.0" +synopsis: "Implementation of BDD" +maintainer: "Jean-Christophe.Filliatre@lri.fr" +authors: "Jean-Christophe Filliâtre" +license: "LGPL-2.1" +homepage: "https://www.lri.fr/~filliatr/software.en.html" +bug-reports: "https://github.com/backtracking/ocaml-bdd/issues" +depends: [ + "dune" {build} +] +build: [ + ["dune" "subst"] {pinned} + ["dune" "build" "@install" "-p" name "-j" jobs] + [with-doc "dune" "build" "@doc" "-p" name] + [with-test "dune" "runtest" "-p" name] +] +dev-repo: "git://github.com/backtracking/ocaml-bdd.git" diff --git a/configure.in b/configure.in deleted file mode 100644 index 5676594..0000000 --- a/configure.in +++ /dev/null @@ -1,145 +0,0 @@ -########################################################################## -# # -# 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. # -########################################################################## - -# the script generated by autoconf from this input will set the following -# variables: -# OCAMLC "ocamlc" if present in the path, or a failure -# or "ocamlc.opt" if present with same version number as ocamlc -# OCAMLOPT "ocamlopt" (or "ocamlopt.opt" if present), or "no" -# OCAMLBEST either "byte" if no native compiler was found, -# or "opt" otherwise -# OCAMLDEP "ocamldep" -# OCAMLLEX "ocamllex" (or "ocamllex.opt" if present) -# OCAMLYACC "ocamlyac" -# OCAMLLIB the path to the ocaml standard library -# OCAMLVERSION the ocaml version number -# OCAMLWEB "ocamlweb" (not mandatory) -# OCAMLWIN32 "yes"/"no" depending on Sys.os_type = "Win32" -# EXE ".exe" if OCAMLWIN32=yes, "" otherwise - -# check for one particular file of the sources -# ADAPT THE FOLLOWING LINE TO YOUR SOURCES! -AC_INIT(bdd.mli) - -# Check for Ocaml compilers - -# we first look for ocamlc in the path; if not present, we fail -AC_CHECK_PROG(OCAMLC,ocamlc,ocamlc,no) -if test "$OCAMLC" = no ; then - AC_MSG_ERROR(Cannot find ocamlc.) -fi - -# we extract Ocaml version number and library path -OCAMLVERSION=`$OCAMLC -v | sed -n -e 's|.*version *\(.*\)$|\1|p' ` -echo "ocaml version is $OCAMLVERSION" -OCAMLLIB=`$OCAMLC -v | tail -1 | cut -f 4 -d " "` -echo "ocaml library path is $OCAMLLIB" - -# then we look for ocamlopt; if not present, we issue a warning -# if the version is not the same, we also discard it -# we set OCAMLBEST to "opt" or "byte", whether ocamlopt is available or not -AC_CHECK_PROG(OCAMLOPT,ocamlopt,ocamlopt,no) -OCAMLBEST=byte -if test "$OCAMLOPT" = no ; then - AC_MSG_WARN(Cannot find ocamlopt; bytecode compilation only.) -else - AC_MSG_CHECKING(ocamlopt version) - TMPVERSION=`$OCAMLOPT -v | sed -n -e 's|.*version *\(.*\)$|\1|p' ` - if test "$TMPVERSION" != "$OCAMLVERSION" ; then - AC_MSG_RESULT(differs from ocamlc; ocamlopt discarded.) - OCAMLOPT=no - else - AC_MSG_RESULT(ok) - OCAMLBEST=opt - fi -fi - -# checking for ocamlc.opt -AC_CHECK_PROG(OCAMLCDOTOPT,ocamlc.opt,ocamlc.opt,no) -if test "$OCAMLCDOTOPT" != no ; then - AC_MSG_CHECKING(ocamlc.opt version) - TMPVERSION=`$OCAMLCDOTOPT -v | sed -n -e 's|.*version *\(.*\)$|\1|p' ` - if test "$TMPVERSION" != "$OCAMLVERSION" ; then - AC_MSG_RESULT(differs from ocamlc; ocamlc.opt discarded.) - else - AC_MSG_RESULT(ok) - OCAMLC=$OCAMLCDOTOPT - fi -fi - -# checking for ocamlopt.opt -if test "$OCAMLOPT" != no ; then - AC_CHECK_PROG(OCAMLOPTDOTOPT,ocamlopt.opt,ocamlopt.opt,no) - if test "$OCAMLOPTDOTOPT" != no ; then - AC_MSG_CHECKING(ocamlc.opt version) - TMPVER=`$OCAMLOPTDOTOPT -v | sed -n -e 's|.*version *\(.*\)$|\1|p' ` - if test "$TMPVER" != "$OCAMLVERSION" ; then - AC_MSG_RESULT(differs from ocamlc; ocamlopt.opt discarded.) - else - AC_MSG_RESULT(ok) - OCAMLOPT=$OCAMLOPTDOTOPT - fi - fi -fi - -# ocamldep, ocamllex and ocamlyacc should also be present in the path -AC_CHECK_PROG(OCAMLDEP,ocamldep,ocamldep,no) -if test "$OCAMLDEP" = no ; then - AC_MSG_ERROR(Cannot find ocamldep.) -fi - -AC_CHECK_PROG(OCAMLLEX,ocamllex,ocamllex,no) -if test "$OCAMLLEX" = no ; then - AC_MSG_ERROR(Cannot find ocamllex.) -else - AC_CHECK_PROG(OCAMLLEXDOTOPT,ocamllex.opt,ocamllex.opt,no) - if test "$OCAMLLEXDOTOPT" != no ; then - OCAMLLEX=$OCAMLLEXDOTOPT - fi -fi - -AC_CHECK_PROG(OCAMLYACC,ocamlyacc,ocamlyacc,no) -if test "$OCAMLYACC" = no ; then - AC_MSG_ERROR(Cannot find ocamlyacc.) -fi - -AC_CHECK_PROG(OCAMLWEB,ocamlweb,ocamlweb,true) - -# platform -AC_MSG_CHECKING(platform) -if echo "let _ = Sys.os_type" | ocaml | grep -q Win32; then - AC_MSG_RESULT(Win32) - OCAMLWIN32=yes - EXE=.exe -else - OCAMLWIN32=no - EXE= -fi - -# substitutions to perform -AC_SUBST(OCAMLC) -AC_SUBST(OCAMLOPT) -AC_SUBST(OCAMLDEP) -AC_SUBST(OCAMLLEX) -AC_SUBST(OCAMLYACC) -AC_SUBST(OCAMLBEST) -AC_SUBST(OCAMLVERSION) -AC_SUBST(OCAMLLIB) -AC_SUBST(OCAMLWEB) -AC_SUBST(OCAMLWIN32) -AC_SUBST(EXE) - -# Finally create the Makefile from Makefile.in -AC_OUTPUT(Makefile) -chmod a-w Makefile diff --git a/dune-project b/dune-project new file mode 100644 index 0000000..13109bb --- /dev/null +++ b/dune-project @@ -0,0 +1,2 @@ +(lang dune 1.6) +(using menhir 2.0) diff --git a/bdd.ml b/lib/bdd.ml similarity index 93% rename from bdd.ml rename to lib/bdd.ml index a732044..f7d49b5 100644 --- a/bdd.ml +++ b/lib/bdd.ml @@ -81,11 +81,13 @@ type t = bdd (* export *) let view b = b.node +(* unused let equal x y = match x, y with | Node (v1, l1, h1), Node (v2, l2, h2) -> v1 == v2 && l1 == l2 && h1 == h2 | _ -> x == y +*) (** perfect hashing is actually less efficient let pair a b = (a + b) * (a + b + 1) / 2 + a @@ -126,6 +128,8 @@ let fold f t init = in Array.fold_right (fold_bucket 0) t.table init +(* unused + let iter f t = let rec iter_bucket i b = if i >= Weak.length b then () else @@ -134,6 +138,7 @@ let iter f t = | None -> iter_bucket (i+1) b in Array.iter (iter_bucket 0) t.table +*) let count t = let rec count_bucket i b accu = @@ -193,7 +198,7 @@ let hashcons_node v l h = hnode end else begin match Weak.get_copy bucket i with - | Some {node=Node(v',l',h')} when v==v' && l==l' && h==h' -> + | Some {node=Node(v',l',h'); _} when v==v' && l==l' && h==h' -> begin match Weak.get bucket i with | Some v -> v | None -> loop (i+1) @@ -258,14 +263,15 @@ let mk_not x = let res = match x.node with | Zero -> one | One -> zero - | Node (v, l, h) -> mk v (mk_not_rec l) (mk_not_rec h) + | Node (v, l, h) -> mk v ~low:(mk_not_rec l) ~high:(mk_not_rec h) in H1.add cache x res; res in mk_not_rec x -let bool_of = function Zero -> false | One -> true | _ -> invalid_arg "bool_of" +(* unused +let bool_of = function Zero -> false | One -> true | _ -> invalid_arg "bool_of"*) let of_bool b = if b then one else zero module H2 = Hashtbl.Make( @@ -343,11 +349,11 @@ let gapply op = let v1 = var u1 in let v2 = var u2 in if v1 == v2 then - mk v1 (app (low u1, low u2)) (app (high u1, high u2)) + mk v1 ~low:(app (low u1, low u2)) ~high:(app (high u1, high u2)) else if v1 < v2 then - mk v1 (app (low u1, u2)) (app (high u1, u2)) + mk v1 ~low:(app (low u1, u2)) ~high:(app (high u1, u2)) else (* v1 > v2 *) - mk v2 (app (u1, low u2)) (app (u1, high u2)) + mk v2 ~low:(app (u1, low u2)) ~high:(app (u1, high u2)) in H2.add cache u12 res; res @@ -379,12 +385,12 @@ let constrain b1 b2 = if v1 == v2 then begin if low u2 == zero then app (high u1, high u2) else if high u2 == zero then app (low u1, low u2) - else mk (var u1) (app (low u1, low u2)) (app (high u1, high u2)) + else mk (var u1) ~low:(app (low u1, low u2)) ~high:(app (high u1, high u2)) end else if v1 < v2 then - mk v1 (app (low u1, u2)) (app (high u1, u2)) + mk v1 ~low:(app (low u1, u2)) ~high:(app (high u1, u2)) else (* v1 > v2 *) - mk v2 (app (u1, low u2)) (app (u1, high u2)) + mk v2 ~low:(app (u1, low u2)) ~high:(app (u1, high u2)) in H2.add cache u12 res; res @@ -409,10 +415,10 @@ let restriction b1 b2 = if v1 == v2 then begin if low u2 == zero then app (high u1, high u2) else if high u2 == zero then app (low u1, low u2) - else mk (var u1) (app (low u1, low u2)) (app (high u1, high u2)) + else mk (var u1) ~low:(app (low u1, low u2)) ~high:(app (high u1, high u2)) end else if v1 < v2 then - mk v1 (app (low u1, u2)) (app (high u1, u2)) + mk v1 ~low:(app (low u1, u2)) ~high:(app (high u1, u2)) else (* v1 > v2 *) app (u1, mk_or (low u2) (high u2)) in @@ -429,7 +435,7 @@ let restrict u x b = with Not_found -> let res = if var u > x then u - else if var u < x then mk (var u) (app (low u)) (app (high u)) + else if var u < x then mk (var u) ~low:(app (low u)) ~high:(app (high u)) else (* var u = x *) if b then app (high u) else (* var u = x, b = 0 *) app (low u) in @@ -489,7 +495,7 @@ let any_sat = let rec mk acc b = match b.node with | Zero -> raise Not_found | One -> acc - | Node (v, {node=Zero}, h) -> mk ((v,true)::acc) h + | Node (v, {node=Zero; _}, h) -> mk ((v,true)::acc) h | Node (v, l, _) -> mk ((v,false)::acc) l in mk [] @@ -498,8 +504,8 @@ let random_sat = let rec mk acc b = match b.node with | Zero -> raise Not_found | One -> acc - | Node (v, {node=Zero}, h) -> mk ((v,true) :: acc) h - | Node (v, l, {node=Zero}) -> mk ((v,false) :: acc) l + | Node (v, {node=Zero; _}, h) -> mk ((v,true) :: acc) h + | Node (v, l, {node=Zero; _}) -> mk ((v,false) :: acc) l | Node (v, l, _) when Random.bool () -> mk ((v,false) :: acc) l | Node (v, _, h) -> mk ((v,true) :: acc) h in @@ -555,7 +561,7 @@ let format_to_dot b fmt = end in Hashtbl.iter - (fun v s -> + (fun _ s -> fprintf fmt "{rank=same; "; S.iter (fun x -> fprintf fmt "%d " x.tag) s; fprintf fmt ";}@\n" @@ -590,6 +596,3 @@ let make ?(print_var=fun ff -> Format.fprintf ff "x%d") = let module B = Make(struct let print_var = print_var let size = size let max_var = max_var end) in (module B: BDD) - - - diff --git a/bdd.mli b/lib/bdd.mli similarity index 100% rename from bdd.mli rename to lib/bdd.mli diff --git a/bench_prop.ml b/lib/bench_prop.ml similarity index 76% rename from bench_prop.ml rename to lib/bench_prop.ml index 492a7b8..dd49f64 100644 --- a/bench_prop.ml +++ b/lib/bench_prop.ml @@ -83,34 +83,10 @@ let right n = let pigeon_p n = Pimp (left n, right n) -let pigeon_n n = assert false +let pigeon_n _ = assert false let equiv_p n = let f = ref (var n) in for i = 1 to n-1 do f := Piff (var (n-i), !f) done; for i = 1 to n do f := Piff (var (n+1-i), !f) done; !f - -(* main *) - -type bench = De_bruijn_p | De_bruijn_n | Pigeon_p | Equiv_p -let bench = ref De_bruijn_p -let n = ref 10 - -let () = - Arg.parse - ["-de-bruijn-p", Arg.Unit (fun () -> bench := De_bruijn_p), ""; - "-de-bruijn-n", Arg.Unit (fun () -> bench := De_bruijn_n), ""; - "-pigeon-p", Arg.Unit (fun () -> bench := Pigeon_p), ""; - "-equiv-p", Arg.Unit (fun () -> bench := Equiv_p), ""] - (fun x -> n := int_of_string x) - ""; - match !bench with - | De_bruijn_p -> - Format.printf "# de_bruijn_p n=%d@\n%a@." !n print (de_bruijn_p !n) - | De_bruijn_n -> - Format.printf "# de_bruijn_n n=%d@\n%a@." !n print (de_bruijn_n !n) - | Pigeon_p -> - Format.printf "# pigeon_p n=%d@\n%a@." !n print (pigeon_p !n) - | Equiv_p -> - Format.printf "# equiv_p n=%d@\n%a@." !n print (equiv_p !n) diff --git a/lib/dune b/lib/dune new file mode 100644 index 0000000..166bc05 --- /dev/null +++ b/lib/dune @@ -0,0 +1,17 @@ +(library + (name bdd) + (modules bdd) + (public_name bdd)) + +(library + (name prop) + (modules prop parser lexer bench_prop) + (libraries bdd) + ; we should wrap it or change the name of the modules as they're quite generic + (wrapped false)) + +(ocamllex + (modules lexer)) + +(menhir + (modules parser)) diff --git a/lexer.mll b/lib/lexer.mll similarity index 100% rename from lexer.mll rename to lib/lexer.mll diff --git a/parser.mly b/lib/parser.mly similarity index 100% rename from parser.mly rename to lib/parser.mly diff --git a/prop.ml b/lib/prop.ml similarity index 100% rename from prop.ml rename to lib/prop.ml diff --git a/misc/headache_config.txt b/misc/headache_config.txt deleted file mode 100644 index 6b8128c..0000000 --- a/misc/headache_config.txt +++ /dev/null @@ -1,10 +0,0 @@ -# Objective Caml source -| ".*\\.ml[il4]?" -> frame open:"(*" line:"*" close:"*)" -| ".*\\.mly" -> frame open:"/*" line:"*" close:"*/" -# C source -| ".*\\.c" -> frame open:"/*" line:"*" close:"*/" -# Misc -| "configure.in" -> frame open:"#" line:"#" close:"#" -| "Makefile.in" -> frame open:"#" line:"#" close:"#" -| "Makefile" -> frame open:"#" line:"#" close:"#" -| "README" -> frame open:"*" line:"*" close:"*" diff --git a/misc/header.txt b/misc/header.txt deleted file mode 100644 index b02cc63..0000000 --- a/misc/header.txt +++ /dev/null @@ -1,11 +0,0 @@ - -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. diff --git a/bdd_sat.ml b/test/bdd_sat.ml similarity index 100% rename from bdd_sat.ml rename to test/bdd_sat.ml diff --git a/test/bench_prop_cli.ml b/test/bench_prop_cli.ml new file mode 100644 index 0000000..ee400ec --- /dev/null +++ b/test/bench_prop_cli.ml @@ -0,0 +1,26 @@ +open Prop +open Bench_prop + +type bench = De_bruijn_p | De_bruijn_n | Pigeon_p | Equiv_p + +let bench = ref De_bruijn_p +let n = ref 10 + +let _ = + + Arg.parse [ + "-de-bruijn-p", Arg.Unit (fun () -> bench := De_bruijn_p), ""; + "-de-bruijn-n", Arg.Unit (fun () -> bench := De_bruijn_n), ""; + "-pigeon-p", Arg.Unit (fun () -> bench := Pigeon_p), ""; + "-equiv-p", Arg.Unit (fun () -> bench := Equiv_p), "" + ] (fun x -> n := int_of_string x) ""; + + match !bench with + | De_bruijn_p -> + Format.printf "# de_bruijn_p n=%d@\n%a@." !n print (de_bruijn_p !n) + | De_bruijn_n -> + Format.printf "# de_bruijn_n n=%d@\n%a@." !n print (de_bruijn_n !n) + | Pigeon_p -> + Format.printf "# pigeon_p n=%d@\n%a@." !n print (pigeon_p !n) + | Equiv_p -> + Format.printf "# equiv_p n=%d@\n%a@." !n print (equiv_p !n) diff --git a/check.ml b/test/check.ml similarity index 100% rename from check.ml rename to test/check.ml diff --git a/test/dune b/test/dune new file mode 100644 index 0000000..cbf6e1d --- /dev/null +++ b/test/dune @@ -0,0 +1,38 @@ +(executable + (name check) + (modules check) + (libraries bdd prop)) + +(alias + (name runtest) + (action (run ./check.exe))) + +(executable + (name test) + (modules test) + (libraries bdd prop)) + +(executable + (name queen) + (modules queen) + (libraries bdd)) + +(executable + (name tiling) + (modules tiling) + (libraries bdd)) + +(executable + (name path) + (modules path) + (libraries bdd)) + +(executable + (name bdd_sat) + (modules bdd_sat) + (libraries prop unix)) + +(executable + (name bench_prop_cli) + (modules bench_prop_cli) + (libraries prop)) diff --git a/path.ml b/test/path.ml similarity index 88% rename from path.ml rename to test/path.ml index 343713d..051e541 100644 --- a/path.ml +++ b/test/path.ml @@ -14,8 +14,13 @@ open Format -let w = int_of_string Sys.argv.(1) -let h = int_of_string Sys.argv.(2) +let _ = + if Array.length Sys.argv <> 3 then failwith ("usage: " ^ Sys.argv.(0) ^ " ") + +let w, h = match int_of_string Sys.argv.(1), int_of_string Sys.argv.(2) with + | exception _ -> failwith "weight and height should be numbers" + | w, h when w > 0 && h > 0 -> w, h + | _ -> failwith "weight and height should be greater than 0" let edges = ref [] diff --git a/queen.ml b/test/queen.ml similarity index 89% rename from queen.ml rename to test/queen.ml index 43164b6..f3c30c0 100644 --- a/queen.ml +++ b/test/queen.ml @@ -14,7 +14,13 @@ open Format -let n = try int_of_string Sys.argv.(1) with _ -> eprintf "queen N"; exit 1 +let _ = if Array.length Sys.argv <> 2 then failwith ("usage: " ^ Sys.argv.(0) ^ " ") + +let n = match int_of_string Sys.argv.(1) with + | exception _ -> failwith "size should be a number" + | n when n <= 0 -> failwith "size should be greater than 0" + | n -> n + include (val Bdd.make (n * n)) let fold_and i j f = diff --git a/test.ml b/test/test.ml similarity index 61% rename from test.ml rename to test/test.ml index 2ba06d2..e2ded4d 100644 --- a/test.ml +++ b/test/test.ml @@ -35,35 +35,35 @@ let display b = let test2 s = let b = of_formula s in display b -let r = test2 "(A -> B) -> (B -> A)" +let _ = test2 "(A -> B) -> (B -> A)" -let r = test "(a1<->a2)<->(a2<->a1)" -let r = test "A \\/ ~A" -let r = test "A -> ~~A" -let r = test "A -> A" -let r = test "((A -> B) -> A) -> A" -let r = test "(A -> B)-> (~B -> ~ A)" -let r = test "((A -> B) /\\ A) -> B" -let r = test "((A -> B) /\\ ~ B) -> ~ A" -let r = test "((A -> B) /\\ (B -> C)) -> (A -> C)" -let r = test "(A /\\ (B \\/ C)) -> ((A /\\ B) \\/ (A /\\ C))" -let r = test "((A /\\ B) \\/ (A /\\ C)) -> (A /\\ (B \\/ C))" -let r = test "(A \\/ (B /\\ C)) -> ((A \\/ B) /\\ (A \\/ C))" -let r = test "((A \\/ B) /\\ (A \\/ C)) -> (A \\/ (B /\\ C))" -let r = test "(~ A -> A) -> A " -let r = test "((P -> (Q /\\ R /\\ S)) /\\ ~S) -> ~P" -let r = test "(P /\\ Q) -> (Q /\\ P)" -let r = test "(A /\\ A) \\/ ~A" -let r = test "~~A <-> A" -let r = test "~(A /\\ B) <-> (~A \\/ ~B)" -let r = test "~(A \\/ B) <-> (~A /\\ ~ B)" -let r = test "(A \\/ (B /\\ C)) <-> ((A \\/ B) /\\ (A \\/ C))" -let r = test "(A /\\ (B \\/ C)) <-> ((A /\\ B) \\/ (A /\\ C))" +let _ = test "(a1<->a2)<->(a2<->a1)" +let _ = test "A \\/ ~A" +let _ = test "A -> ~~A" +let _ = test "A -> A" +let _ = test "((A -> B) -> A) -> A" +let _ = test "(A -> B)-> (~B -> ~ A)" +let _ = test "((A -> B) /\\ A) -> B" +let _ = test "((A -> B) /\\ ~ B) -> ~ A" +let _ = test "((A -> B) /\\ (B -> C)) -> (A -> C)" +let _ = test "(A /\\ (B \\/ C)) -> ((A /\\ B) \\/ (A /\\ C))" +let _ = test "((A /\\ B) \\/ (A /\\ C)) -> (A /\\ (B \\/ C))" +let _ = test "(A \\/ (B /\\ C)) -> ((A \\/ B) /\\ (A \\/ C))" +let _ = test "((A \\/ B) /\\ (A \\/ C)) -> (A \\/ (B /\\ C))" +let _ = test "(~ A -> A) -> A " +let _ = test "((P -> (Q /\\ R /\\ S)) /\\ ~S) -> ~P" +let _ = test "(P /\\ Q) -> (Q /\\ P)" +let _ = test "(A /\\ A) \\/ ~A" +let _ = test "~~A <-> A" +let _ = test "~(A /\\ B) <-> (~A \\/ ~B)" +let _ = test "~(A \\/ B) <-> (~A /\\ ~ B)" +let _ = test "(A \\/ (B /\\ C)) <-> ((A \\/ B) /\\ (A \\/ C))" +let _ = test "(A /\\ (B \\/ C)) <-> ((A /\\ B) \\/ (A /\\ C))" -let r = test "((b <-> c) -> (a/\\b/\\c)) /\\ +let _ = test "((b <-> c) -> (a/\\b/\\c)) /\\ ((c<->a)->(a/\\b/\\c)) /\\ ((a<->b)->(a/\\b/\\c)) -> (a/\\b/\\c)" -let r = test "~ ~(~p1 \\/ ~p2 \\/ ~p3 \\/ (p1 & p2 & p3))" +let _ = test "~ ~(~p1 \\/ ~p2 \\/ ~p3 \\/ (p1 & p2 & p3))" let de_bruijn_p_2 = test " (((((p1 -> p2) & (p2 -> p1)) -> (p1 & (p2 & (p3 & (p4 & p5))))) & ((((p2 -> @@ -72,13 +72,13 @@ p3)) -> (p1 & (p2 & (p3 & (p4 & p5))))) & ((((p4 -> p5) & (p5 -> p4)) -> (p1 & (p2 & (p3 & (p4 & p5))))) & (((p5 -> p1) & (p1 -> p5)) -> (p1 & (p2 & (p3 & (p4 & p5))))))))) -> (p1 & (p2 & (p3 & (p4 & p5)))))" -let r = test2 "A -> (A -> ~ A)" -let r = test2 "A /\\ ~A" -let r = test2 "(A \\/ B) /\\ ~A /\\ ~B" -let r = test2 "(A -> B) -> (~A -> ~B)" -let r = test2 "(A -> B) -> (B -> A)" -let r = test2 "B -> (B /\\ A)" -let r = test2 "(A -> A) <-> A" +let _ = test2 "A -> (A -> ~ A)" +let _ = test2 "A /\\ ~A" +let _ = test2 "(A \\/ B) /\\ ~A /\\ ~B" +let _ = test2 "(A -> B) -> (~A -> ~B)" +let _ = test2 "(A -> B) -> (B -> A)" +let _ = test2 "B -> (B /\\ A)" +let _ = test2 "(A -> A) <-> A" let () = let _, b = bdd_formula (Bench_prop.de_bruijn_n 5) in diff --git a/tiling.ml b/test/tiling.ml similarity index 100% rename from tiling.ml rename to test/tiling.ml