**************************************************************************
* *
* Copyright (C) Jean-Christophe Filliatre *
* *
* This software is free software; you can redistribute it and/or *
* modify it under the terms of the GNU Library General Public *
* License version 2, 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. *
* *
**************************************************************************
This is a quick implementation of a BDD library for Ocaml.
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