diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..1b1f2f3 --- /dev/null +++ b/.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 diff --git a/CHANGES b/CHANGES new file mode 100644 index 0000000..cd38954 --- /dev/null +++ b/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) diff --git a/LICENSE b/LICENSE new file mode 100644 index 0000000..550c7cb --- /dev/null +++ b/LICENSE @@ -0,0 +1,526 @@ +The library Creal is distributed under the terms of the GNU Lesser +General Public License version 2.1 (included below). + +As a special exception to the GNU Lesser General Public License, you +may link, statically or dynamically, a "work that uses the Library" +with a publicly distributed version of the Library to produce an +executable file containing portions of the Library, and distribute +that executable file under terms of your choice, without any of the +additional requirements listed in clause 6 of the GNU Lesser General +Public License. By "a publicly distributed version of the Library", we +mean either the unmodified Library as distributed, or a +modified version of the Library that is distributed under the +conditions defined in clause 2 of the GNU Lesser General Public +License. This exception does not however invalidate any other reasons +why the executable file might be covered by the GNU Lesser General +Public License. + +====================================================================== + + GNU LESSER GENERAL PUBLIC LICENSE + Version 2.1, February 1999 + + Copyright (C) 1991, 1999 Free Software Foundation, Inc. + 51 Franklin St, Fifth Floor, Boston, MA 02110-1301 USA + Everyone is permitted to copy and distribute verbatim copies + of this license document, but changing it is not allowed. + +[This is the first released version of the Lesser GPL. It also counts + as the successor of the GNU Library Public License, version 2, hence + the version number 2.1.] + + Preamble + + The licenses for most software are designed to take away your +freedom to share and change it. By contrast, the GNU General Public +Licenses are intended to guarantee your freedom to share and change +free software--to make sure the software is free for all its users. + + This license, the Lesser General Public License, applies to some +specially designated software packages--typically libraries--of the +Free Software Foundation and other authors who decide to use it. You +can use it too, but we suggest you first think carefully about whether +this license or the ordinary General Public License is the better +strategy to use in any particular case, based on the explanations +below. + + When we speak of free software, we are referring to freedom of use, +not price. Our General Public Licenses are designed to make sure that +you have the freedom to distribute copies of free software (and charge +for this service if you wish); that you receive source code or can get +it if you want it; that you can change the software and use pieces of +it in new free programs; and that you are informed that you can do +these things. + + To protect your rights, we need to make restrictions that forbid +distributors to deny you these rights or to ask you to surrender these +rights. These restrictions translate to certain responsibilities for +you if you distribute copies of the library or if you modify it. + + For example, if you distribute copies of the library, whether gratis +or for a fee, you must give the recipients all the rights that we gave +you. You must make sure that they, too, receive or can get the source +code. If you link other code with the library, you must provide +complete object files to the recipients, so that they can relink them +with the library after making changes to the library and recompiling +it. And you must show them these terms so they know their rights. + + We protect your rights with a two-step method: (1) we copyright the +library, and (2) we offer you this license, which gives you legal +permission to copy, distribute and/or modify the library. + + To protect each distributor, we want to make it very clear that +there is no warranty for the free library. Also, if the library is +modified by someone else and passed on, the recipients should know +that what they have is not the original version, so that the original +author's reputation will not be affected by problems that might be +introduced by others. + + Finally, software patents pose a constant threat to the existence of +any free program. We wish to make sure that a company cannot +effectively restrict the users of a free program by obtaining a +restrictive license from a patent holder. Therefore, we insist that +any patent license obtained for a version of the library must be +consistent with the full freedom of use specified in this license. + + Most GNU software, including some libraries, is covered by the +ordinary GNU General Public License. This license, the GNU Lesser +General Public License, applies to certain designated libraries, and +is quite different from the ordinary General Public License. We use +this license for certain libraries in order to permit linking those +libraries into non-free programs. + + When a program is linked with a library, whether statically or using +a shared library, the combination of the two is legally speaking a +combined work, a derivative of the original library. The ordinary +General Public License therefore permits such linking only if the +entire combination fits its criteria of freedom. The Lesser General +Public License permits more lax criteria for linking other code with +the library. + + We call this license the "Lesser" General Public License because it +does Less to protect the user's freedom than the ordinary General +Public License. It also provides other free software developers Less +of an advantage over competing non-free programs. These disadvantages +are the reason we use the ordinary General Public License for many +libraries. However, the Lesser license provides advantages in certain +special circumstances. + + For example, on rare occasions, there may be a special need to +encourage the widest possible use of a certain library, so that it +becomes a de-facto standard. To achieve this, non-free programs must +be allowed to use the library. A more frequent case is that a free +library does the same job as widely used non-free libraries. In this +case, there is little to gain by limiting the free library to free +software only, so we use the Lesser General Public License. + + In other cases, permission to use a particular library in non-free +programs enables a greater number of people to use a large body of +free software. For example, permission to use the GNU C Library in +non-free programs enables many more people to use the whole GNU +operating system, as well as its variant, the GNU/Linux operating +system. + + Although the Lesser General Public License is Less protective of the +users' freedom, it does ensure that the user of a program that is +linked with the Library has the freedom and the wherewithal to run +that program using a modified version of the Library. + + The precise terms and conditions for copying, distribution and +modification follow. Pay close attention to the difference between a +"work based on the library" and a "work that uses the library". The +former contains code derived from the library, whereas the latter must +be combined with the library in order to run. + + GNU LESSER GENERAL PUBLIC LICENSE + TERMS AND CONDITIONS FOR COPYING, DISTRIBUTION AND MODIFICATION + + 0. This License Agreement applies to any software library or other +program which contains a notice placed by the copyright holder or +other authorized party saying it may be distributed under the terms of +this Lesser General Public License (also called "this License"). +Each licensee is addressed as "you". + + A "library" means a collection of software functions and/or data +prepared so as to be conveniently linked with application programs +(which use some of those functions and data) to form executables. + + The "Library", below, refers to any such software library or work +which has been distributed under these terms. A "work based on the +Library" means either the Library or any derivative work under +copyright law: that is to say, a work containing the Library or a +portion of it, either verbatim or with modifications and/or translated +straightforwardly into another language. (Hereinafter, translation is +included without limitation in the term "modification".) + + "Source code" for a work means the preferred form of the work for +making modifications to it. For a library, complete source code means +all the source code for all modules it contains, plus any associated +interface definition files, plus the scripts used to control +compilation and installation of the library. + + Activities other than copying, distribution and modification are not +covered by this License; they are outside its scope. The act of +running a program using the Library is not restricted, and output from +such a program is covered only if its contents constitute a work based +on the Library (independent of the use of the Library in a tool for +writing it). Whether that is true depends on what the Library does +and what the program that uses the Library does. + + 1. You may copy and distribute verbatim copies of the Library's +complete source code as you receive it, in any medium, provided that +you conspicuously and appropriately publish on each copy an +appropriate copyright notice and disclaimer of warranty; keep intact +all the notices that refer to this License and to the absence of any +warranty; and distribute a copy of this License along with the +Library. + + You may charge a fee for the physical act of transferring a copy, +and you may at your option offer warranty protection in exchange for a +fee. + + 2. You may modify your copy or copies of the Library or any portion +of it, thus forming a work based on the Library, and copy and +distribute such modifications or work under the terms of Section 1 +above, provided that you also meet all of these conditions: + + a) The modified work must itself be a software library. + + b) You must cause the files modified to carry prominent notices + stating that you changed the files and the date of any change. + + c) You must cause the whole of the work to be licensed at no + charge to all third parties under the terms of this License. + + d) If a facility in the modified Library refers to a function or a + table of data to be supplied by an application program that uses + the facility, other than as an argument passed when the facility + is invoked, then you must make a good faith effort to ensure that, + in the event an application does not supply such function or + table, the facility still operates, and performs whatever part of + its purpose remains meaningful. + + (For example, a function in a library to compute square roots has + a purpose that is entirely well-defined independent of the + application. Therefore, Subsection 2d requires that any + application-supplied function or table used by this function must + be optional: if the application does not supply it, the square + root function must still compute square roots.) + +These requirements apply to the modified work as a whole. If +identifiable sections of that work are not derived from the Library, +and can be reasonably considered independent and separate works in +themselves, then this License, and its terms, do not apply to those +sections when you distribute them as separate works. But when you +distribute the same sections as part of a whole which is a work based +on the Library, the distribution of the whole must be on the terms of +this License, whose permissions for other licensees extend to the +entire whole, and thus to each and every part regardless of who wrote +it. + +Thus, it is not the intent of this section to claim rights or contest +your rights to work written entirely by you; rather, the intent is to +exercise the right to control the distribution of derivative or +collective works based on the Library. + +In addition, mere aggregation of another work not based on the Library +with the Library (or with a work based on the Library) on a volume of +a storage or distribution medium does not bring the other work under +the scope of this License. + + 3. You may opt to apply the terms of the ordinary GNU General Public +License instead of this License to a given copy of the Library. To do +this, you must alter all the notices that refer to this License, so +that they refer to the ordinary GNU General Public License, version 2, +instead of to this License. (If a newer version than version 2 of the +ordinary GNU General Public License has appeared, then you can specify +that version instead if you wish.) Do not make any other change in +these notices. + + Once this change is made in a given copy, it is irreversible for +that copy, so the ordinary GNU General Public License applies to all +subsequent copies and derivative works made from that copy. + + This option is useful when you wish to copy part of the code of +the Library into a program that is not a library. + + 4. You may copy and distribute the Library (or a portion or +derivative of it, under Section 2) in object code or executable form +under the terms of Sections 1 and 2 above provided that you accompany +it with the complete corresponding machine-readable source code, which +must be distributed under the terms of Sections 1 and 2 above on a +medium customarily used for software interchange. + + If distribution of object code is made by offering access to copy +from a designated place, then offering equivalent access to copy the +source code from the same place satisfies the requirement to +distribute the source code, even though third parties are not +compelled to copy the source along with the object code. + + 5. A program that contains no derivative of any portion of the +Library, but is designed to work with the Library by being compiled or +linked with it, is called a "work that uses the Library". Such a +work, in isolation, is not a derivative work of the Library, and +therefore falls outside the scope of this License. + + However, linking a "work that uses the Library" with the Library +creates an executable that is a derivative of the Library (because it +contains portions of the Library), rather than a "work that uses the +library". The executable is therefore covered by this License. +Section 6 states terms for distribution of such executables. + + When a "work that uses the Library" uses material from a header file +that is part of the Library, the object code for the work may be a +derivative work of the Library even though the source code is not. +Whether this is true is especially significant if the work can be +linked without the Library, or if the work is itself a library. The +threshold for this to be true is not precisely defined by law. + + If such an object file uses only numerical parameters, data +structure layouts and accessors, and small macros and small inline +functions (ten lines or less in length), then the use of the object +file is unrestricted, regardless of whether it is legally a derivative +work. (Executables containing this object code plus portions of the +Library will still fall under Section 6.) + + Otherwise, if the work is a derivative of the Library, you may +distribute the object code for the work under the terms of Section 6. +Any executables containing that work also fall under Section 6, +whether or not they are linked directly with the Library itself. + + 6. As an exception to the Sections above, you may also combine or +link a "work that uses the Library" with the Library to produce a +work containing portions of the Library, and distribute that work +under terms of your choice, provided that the terms permit +modification of the work for the customer's own use and reverse +engineering for debugging such modifications. + + You must give prominent notice with each copy of the work that the +Library is used in it and that the Library and its use are covered by +this License. You must supply a copy of this License. If the work +during execution displays copyright notices, you must include the +copyright notice for the Library among them, as well as a reference +directing the user to the copy of this License. Also, you must do one +of these things: + + a) Accompany the work with the complete corresponding + machine-readable source code for the Library including whatever + changes were used in the work (which must be distributed under + Sections 1 and 2 above); and, if the work is an executable linked + with the Library, with the complete machine-readable "work that + uses the Library", as object code and/or source code, so that the + user can modify the Library and then relink to produce a modified + executable containing the modified Library. (It is understood + that the user who changes the contents of definitions files in the + Library will not necessarily be able to recompile the application + to use the modified definitions.) + + b) Use a suitable shared library mechanism for linking with the + Library. A suitable mechanism is one that (1) uses at run time a + copy of the library already present on the user's computer system, + rather than copying library functions into the executable, and (2) + will operate properly with a modified version of the library, if + the user installs one, as long as the modified version is + interface-compatible with the version that the work was made with. + + c) Accompany the work with a written offer, valid for at least + three years, to give the same user the materials specified in + Subsection 6a, above, for a charge no more than the cost of + performing this distribution. + + d) If distribution of the work is made by offering access to copy + from a designated place, offer equivalent access to copy the above + specified materials from the same place. + + e) Verify that the user has already received a copy of these + materials or that you have already sent this user a copy. + + For an executable, the required form of the "work that uses the +Library" must include any data and utility programs needed for +reproducing the executable from it. However, as a special exception, +the materials to be distributed need not include anything that is +normally distributed (in either source or binary form) with the major +components (compiler, kernel, and so on) of the operating system on +which the executable runs, unless that component itself accompanies +the executable. + + It may happen that this requirement contradicts the license +restrictions of other proprietary libraries that do not normally +accompany the operating system. Such a contradiction means you cannot +use both them and the Library together in an executable that you +distribute. + + 7. You may place library facilities that are a work based on the +Library side-by-side in a single library together with other library +facilities not covered by this License, and distribute such a combined +library, provided that the separate distribution of the work based on +the Library and of the other library facilities is otherwise +permitted, and provided that you do these two things: + + a) Accompany the combined library with a copy of the same work + based on the Library, uncombined with any other library + facilities. This must be distributed under the terms of the + Sections above. + + b) Give prominent notice with the combined library of the fact + that part of it is a work based on the Library, and explaining + where to find the accompanying uncombined form of the same work. + + 8. You may not copy, modify, sublicense, link with, or distribute +the Library except as expressly provided under this License. Any +attempt otherwise to copy, modify, sublicense, link with, or +distribute the Library is void, and will automatically terminate your +rights under this License. However, parties who have received copies, +or rights, from you under this License will not have their licenses +terminated so long as such parties remain in full compliance. + + 9. You are not required to accept this License, since you have not +signed it. However, nothing else grants you permission to modify or +distribute the Library or its derivative works. These actions are +prohibited by law if you do not accept this License. Therefore, by +modifying or distributing the Library (or any work based on the +Library), you indicate your acceptance of this License to do so, and +all its terms and conditions for copying, distributing or modifying +the Library or works based on it. + + 10. Each time you redistribute the Library (or any work based on the +Library), the recipient automatically receives a license from the +original licensor to copy, distribute, link with or modify the Library +subject to these terms and conditions. You may not impose any further +restrictions on the recipients' exercise of the rights granted herein. +You are not responsible for enforcing compliance by third parties with +this License. + + 11. If, as a consequence of a court judgment or allegation of patent +infringement or for any other reason (not limited to patent issues), +conditions are imposed on you (whether by court order, agreement or +otherwise) that contradict the conditions of this License, they do not +excuse you from the conditions of this License. If you cannot +distribute so as to satisfy simultaneously your obligations under this +License and any other pertinent obligations, then as a consequence you +may not distribute the Library at all. For example, if a patent +license would not permit royalty-free redistribution of the Library by +all those who receive copies directly or indirectly through you, then +the only way you could satisfy both it and this License would be to +refrain entirely from distribution of the Library. + +If any portion of this section is held invalid or unenforceable under +any particular circumstance, the balance of the section is intended to +apply, and the section as a whole is intended to apply in other +circumstances. + +It is not the purpose of this section to induce you to infringe any +patents or other property right claims or to contest validity of any +such claims; this section has the sole purpose of protecting the +integrity of the free software distribution system which is +implemented by public license practices. Many people have made +generous contributions to the wide range of software distributed +through that system in reliance on consistent application of that +system; it is up to the author/donor to decide if he or she is willing +to distribute software through any other system and a licensee cannot +impose that choice. + +This section is intended to make thoroughly clear what is believed to +be a consequence of the rest of this License. + + 12. If the distribution and/or use of the Library is restricted in +certain countries either by patents or by copyrighted interfaces, the +original copyright holder who places the Library under this License +may add an explicit geographical distribution limitation excluding those +countries, so that distribution is permitted only in or among +countries not thus excluded. In such case, this License incorporates +the limitation as if written in the body of this License. + + 13. The Free Software Foundation may publish revised and/or new +versions of the Lesser General Public License from time to time. +Such new versions will be similar in spirit to the present version, +but may differ in detail to address new problems or concerns. + +Each version is given a distinguishing version number. If the Library +specifies a version number of this License which applies to it and +"any later version", you have the option of following the terms and +conditions either of that version or of any later version published by +the Free Software Foundation. If the Library does not specify a +license version number, you may choose any version ever published by +the Free Software Foundation. + + 14. If you wish to incorporate parts of the Library into other free +programs whose distribution conditions are incompatible with these, +write to the author to ask for permission. For software which is +copyrighted by the Free Software Foundation, write to the Free +Software Foundation; we sometimes make exceptions for this. Our +decision will be guided by the two goals of preserving the free status +of all derivatives of our free software and of promoting the sharing +and reuse of software generally. + + NO WARRANTY + + 15. BECAUSE THE LIBRARY IS LICENSED FREE OF CHARGE, THERE IS NO +WARRANTY FOR THE LIBRARY, TO THE EXTENT PERMITTED BY APPLICABLE LAW. +EXCEPT WHEN OTHERWISE STATED IN WRITING THE COPYRIGHT HOLDERS AND/OR +OTHER PARTIES PROVIDE THE LIBRARY "AS IS" WITHOUT WARRANTY OF ANY +KIND, EITHER EXPRESSED OR IMPLIED, INCLUDING, BUT NOT LIMITED TO, THE +IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR +PURPOSE. THE ENTIRE RISK AS TO THE QUALITY AND PERFORMANCE OF THE +LIBRARY IS WITH YOU. SHOULD THE LIBRARY PROVE DEFECTIVE, YOU ASSUME +THE COST OF ALL NECESSARY SERVICING, REPAIR OR CORRECTION. + + 16. IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGREED TO IN +WRITING WILL ANY COPYRIGHT HOLDER, OR ANY OTHER PARTY WHO MAY MODIFY +AND/OR REDISTRIBUTE THE LIBRARY AS PERMITTED ABOVE, BE LIABLE TO YOU +FOR DAMAGES, INCLUDING ANY GENERAL, SPECIAL, INCIDENTAL OR +CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OR INABILITY TO USE THE +LIBRARY (INCLUDING BUT NOT LIMITED TO LOSS OF DATA OR DATA BEING +RENDERED INACCURATE OR LOSSES SUSTAINED BY YOU OR THIRD PARTIES OR A +FAILURE OF THE LIBRARY TO OPERATE WITH ANY OTHER SOFTWARE), EVEN IF +SUCH HOLDER OR OTHER PARTY HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH +DAMAGES. + + END OF TERMS AND CONDITIONS + + How to Apply These Terms to Your New Libraries + + If you develop a new library, and you want it to be of the greatest +possible use to the public, we recommend making it free software that +everyone can redistribute and change. You can do so by permitting +redistribution under these terms (or, alternatively, under the terms +of the ordinary General Public License). + + To apply these terms, attach the following notices to the library. +It is safest to attach them to the start of each source file to most +effectively convey the exclusion of warranty; and each file should +have at least the "copyright" line and a pointer to where the full +notice is found. + + + + Copyright (C) + + This library is free software; you can redistribute it and/or + modify it under the terms of the GNU Lesser General Public + License as published by the Free Software Foundation; either + version 2.1 of the License, or (at your option) any later version. + + This library 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. See the GNU + Lesser General Public License for more details. + + You should have received a copy of the GNU Lesser General Public + License along with this library; if not, write to the Free Software + Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA 02110-1301 USA + +Also add information on how to contact you by electronic and paper mail. + +You should also get your employer (if you work as a programmer) or +your school, if any, to sign a "copyright disclaimer" for the library, +if necessary. Here is a sample; alter the names: + + Yoyodyne, Inc., hereby disclaims all copyright interest in the + library `Frob' (a library for tweaking knobs) written by James + Random Hacker. + + , 1 April 1990 + Ty Coon, President of Vice + +That's all there is to it! diff --git a/Makefile.in b/Makefile.in new file mode 100644 index 0000000..6dd12dd --- /dev/null +++ b/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 diff --git a/README.md b/README.md index f3da3d7..3101d35 100644 --- a/README.md +++ b/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 diff --git a/bdd.ml b/bdd.ml new file mode 100644 index 0000000..a732044 --- /dev/null +++ b/bdd.ml @@ -0,0 +1,595 @@ +(**************************************************************************) +(* *) +(* 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. *) +(**************************************************************************) + +(* Binary Decision Diagrams *) + +type variable = int (* 1..max_var *) + +type formula = + | Ffalse + | Ftrue + | Fvar of variable + | Fand of formula * formula + | For of formula * formula + | Fimp of formula * formula + | Fiff of formula * formula + | Fnot of formula + +module type BDD = sig + val get_max_var : unit -> int + type t + type view = Zero | One | Node of variable * t * t + val view : t -> view + val var : t -> variable + val low : t -> t + val high : t -> t + val zero : t + val one : t + val make : variable -> low:t -> high:t -> t + val mk_var : variable -> t + val mk_not : t -> t + val mk_and : t -> t -> t + val mk_or : t -> t -> t + val mk_imp : t -> t -> t + val apply : (bool -> bool -> bool) -> t -> t -> t + val constrain : t -> t -> t + val restriction : t -> t -> t + val restrict : t -> variable -> bool -> t + val build : formula -> t + val is_sat : t -> bool + val tautology : t -> bool + val count_sat : t -> Int64.t + val any_sat : t -> (variable * bool) list + val random_sat : t -> (variable * bool) list + val all_sat : t -> (variable * bool) list list + val print_var : Format.formatter -> variable -> unit + val to_dot : t -> string + val print_to_dot : t -> file:string -> unit + val display : t -> unit + val stats : unit -> (int * int * int * int * int * int) array +end + +let debug = false + +(* Make a fresh module *) +module Make(X: sig + val print_var: Format.formatter -> int -> unit + val size: int + val max_var: int +end) = struct + open X + +let print_var = print_var + +let get_max_var () = max_var + +type bdd = { tag: int; node : view } +and view = Zero | One | Node of variable * bdd (*low*) * bdd (*high*) + +type t = bdd (* export *) + +let view b = b.node + +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 +let triple a b c = pair c (pair a b) +let hash_node v l h = abs (triple l.tag h.tag v) +**) +let hash_node l h = abs (19 * l.tag + h.tag) + +let hash = function + | Zero -> 0 + | One -> 1 + | Node (_, l, h) -> hash_node l h + +let gentag = let r = ref (-1) in fun () -> incr r; !r + +type table = { + mutable table : bdd Weak.t array; + mutable totsize : int; (* sum of the bucket sizes *) + mutable limit : int; (* max ratio totsize/table length *) +} + +let create sz = + let sz = if sz < 7 then 7 else sz in + let sz = if sz > Sys.max_array_length then Sys.max_array_length else sz in + let emptybucket = Weak.create 0 in + { table = Array.make sz emptybucket; + totsize = 0; + limit = 3; } + +let vt = Array.init max_var (fun _ -> create size) + +let fold f t init = + let rec fold_bucket i b accu = + if i >= Weak.length b then accu else + match Weak.get b i with + | Some v -> fold_bucket (i+1) b (f v accu) + | None -> fold_bucket (i+1) b accu + in + Array.fold_right (fold_bucket 0) t.table init + +let iter f t = + let rec iter_bucket i b = + if i >= Weak.length b then () else + match Weak.get b i with + | Some v -> f v; iter_bucket (i+1) b + | None -> iter_bucket (i+1) b + in + Array.iter (iter_bucket 0) t.table + +let count t = + let rec count_bucket i b accu = + if i >= Weak.length b then accu else + count_bucket (i+1) b (accu + (if Weak.check b i then 1 else 0)) + in + Array.fold_right (count_bucket 0) t.table 0 + +let next_sz n = min (3*n/2 + 3) (Sys.max_array_length - 1) + +let rec resize t = + if debug then Format.eprintf "resizing...@."; + let oldlen = Array.length t.table in + let newlen = next_sz oldlen in + if newlen > oldlen then begin + let newt = create newlen in + newt.limit <- t.limit + 100; (* prevent resizing of newt *) + fold (fun d () -> add newt d) t (); + t.table <- newt.table; + t.limit <- t.limit + 2; + end + +and add t d = + add_index t d ((hash d.node) mod (Array.length t.table)) + +and add_index t d index = + let bucket = t.table.(index) in + let sz = Weak.length bucket in + let rec loop i = + if i >= sz then begin + let newsz = min (sz + 3) (Sys.max_array_length - 1) in + if newsz <= sz then + failwith "Hashcons.Make: hash bucket cannot grow more"; + let newbucket = Weak.create newsz in + Weak.blit bucket 0 newbucket 0 sz; + Weak.set newbucket i (Some d); + t.table.(index) <- newbucket; + t.totsize <- t.totsize + (newsz - sz); + if t.totsize > t.limit * Array.length t.table then resize t; + end else begin + if Weak.check bucket i + then loop (i+1) + else Weak.set bucket i (Some d) + end + in + loop 0 + +let hashcons_node v l h = + let t = vt.(v - 1) in + let index = (hash_node l h) mod (Array.length t.table) in + let bucket = t.table.(index) in + let sz = Weak.length bucket in + let rec loop i = + if i >= sz then begin + let hnode = { tag = gentag (); node = Node (v, l, h) } in + add_index t hnode index; + hnode + end else begin + match Weak.get_copy bucket i with + | 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) + end + | _ -> loop (i+1) + end + in + loop 0 + +let stat t = + let len = Array.length t.table in + let lens = Array.map Weak.length t.table in + Array.sort compare lens; + let totlen = Array.fold_left ( + ) 0 lens in + (len, count t, totlen, lens.(0), lens.(len/2), lens.(len-1)) + +let stats () = Array.map stat vt + +(* zero and one allocated once and for all *) +let zero = { tag = gentag (); node = Zero } +let one = { tag = gentag (); node = One } + +let var b = match b.node with + | Zero | One -> max_var + 1 + | Node (v, _, _) -> v + +let low b = match b.node with + | Zero | One -> invalid_arg "Bdd.low" + | Node (_, l, _) -> l + +let high b = match b.node with + | Zero | One -> invalid_arg "Bdd.low" + | Node (_, _, h) -> h + +let mk v ~low ~high = + if low == high then low else hashcons_node v low high + +let make v ~low ~high = + if v < 1 || v > max_var then invalid_arg "Bdd.make"; + mk v ~low ~high + +let mk_var v = + if v < 1 || v > max_var then invalid_arg "Bdd.mk_var"; + mk v ~low:zero ~high:one + +module Bdd = struct + type t = bdd + let equal = (==) + let hash b = b.tag + let compare b1 b2 = Pervasives.compare b1.tag b2.tag +end +module H1 = Hashtbl.Make(Bdd) + +let cache_default_size = 7001 + +let mk_not x = + let cache = H1.create cache_default_size in + let rec mk_not_rec x = + try + H1.find cache x + with Not_found -> + let res = match x.node with + | Zero -> one + | One -> zero + | Node (v, l, h) -> mk v (mk_not_rec l) (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" +let of_bool b = if b then one else zero + +module H2 = Hashtbl.Make( + struct + type t = bdd * bdd + let equal (u1,v1) (u2,v2) = u1==u2 && v1==v2 + let hash (u,v) = + (*abs (19 * u.tag + v.tag)*) + let s = u.tag + v.tag in abs (s * (s+1) / 2 + u.tag) + end) + +type operator = + | Op_and | Op_or | Op_imp + | Op_any of (bool -> bool -> bool) + +let apply_op op b1 b2 = match op with + | Op_and -> b1 && b2 + | Op_or -> b1 || b2 + | Op_imp -> (not b1) || b2 + | Op_any f -> f b1 b2 + +let gapply op = + let op_z_z = of_bool (apply_op op false false) in + let op_z_o = of_bool (apply_op op false true) in + let op_o_z = of_bool (apply_op op true false) in + let op_o_o = of_bool (apply_op op true true) in + fun b1 b2 -> + let cache = H2.create cache_default_size in + let rec app ((u1,u2) as u12) = + match op with + | Op_and -> + if u1 == u2 then + u1 + else if u1 == zero || u2 == zero then + zero + else if u1 == one then + u2 + else if u2 == one then + u1 + else + app_gen u12 + | Op_or -> + if u1 == u2 then + u1 + else if u1 == one || u2 == one then + one + else if u1 == zero then + u2 + else if u2 == zero then + u1 + else + app_gen u12 + | Op_imp -> + if u1 == zero then + one + else if u1 == one then + u2 + else if u2 == one then + one + else + app_gen u12 + | Op_any _ -> + app_gen u12 + and app_gen ((u1,u2) as u12) = + match u1.node, u2.node with + | Zero, Zero -> op_z_z + | Zero, One -> op_z_o + | One, Zero -> op_o_z + | One, One -> op_o_o + | _ -> + try + H2.find cache u12 + with Not_found -> + let res = + 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)) + else if v1 < v2 then + mk v1 (app (low u1, u2)) (app (high u1, u2)) + else (* v1 > v2 *) + mk v2 (app (u1, low u2)) (app (u1, high u2)) + in + H2.add cache u12 res; + res + in + app (b1, b2) + +let mk_and = gapply Op_and +let mk_or = gapply Op_or +let mk_imp = gapply Op_imp +let mk_iff = gapply (Op_any (fun b1 b2 -> b1 == b2)) + +let apply f = gapply (Op_any f) + +let constrain b1 b2 = + let cache = H2.create cache_default_size in + let rec app ((u1,u2) as u12) = + match u1.node, u2.node with + | _, Zero -> failwith "constrain 0 is undefined" + | _, One -> u1 + | Zero, _ -> u1 + | One, _ -> u1 + | _ -> + try + H2.find cache u12 + with Not_found -> + let res = + let v1 = var u1 in + let v2 = var u2 in + 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)) + end + else if v1 < v2 then + mk v1 (app (low u1, u2)) (app (high u1, u2)) + else (* v1 > v2 *) + mk v2 (app (u1, low u2)) (app (u1, high u2)) + in + H2.add cache u12 res; + res + in + app (b1, b2) + +let restriction b1 b2 = + let cache = H2.create cache_default_size in + let rec app ((u1,u2) as u12) = + match u1.node, u2.node with + | _, Zero -> failwith "constrain 0 is undefined" + | _, One -> u1 + | Zero, _ -> u1 + | One, _ -> u1 + | _ -> + try + H2.find cache u12 + with Not_found -> + let res = + let v1 = var u1 in + let v2 = var u2 in + 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)) + end + else if v1 < v2 then + mk v1 (app (low u1, u2)) (app (high u1, u2)) + else (* v1 > v2 *) + app (u1, mk_or (low u2) (high u2)) + in + H2.add cache u12 res; + res + in + app (b1, b2) + +let restrict u x b = + let cache = H1.create cache_default_size in + let rec app u = + try + H1.find cache u + 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 (* var u = x *) if b then app (high u) + else (* var u = x, b = 0 *) app (low u) + in + H1.add cache u res; + res + in + app u + +(* formula -> bdd *) + +let rec build = function + | Ffalse -> zero + | Ftrue -> one + | Fvar v -> mk_var v + | Fand (f1, f2) -> mk_and (build f1) (build f2) + | For (f1, f2) -> mk_or (build f1) (build f2) + | Fimp (f1, f2) -> mk_imp (build f1) (build f2) + | Fiff (f1, f2) -> mk_iff (build f1) (build f2) + | Fnot f -> mk_not (build f) + +(* satisfiability *) + +let is_sat b = b.node != Zero + +let tautology b = b.node == One + +let rec int64_two_to = function + | 0 -> + Int64.one + | n -> + let r = int64_two_to (n/2) in + let r2 = Int64.mul r r in + if n mod 2 == 0 then r2 else Int64.mul (Int64.of_int 2) r2 + +let count_sat b = + let cache = H1.create cache_default_size in + let rec count b = + try + H1.find cache b + with Not_found -> + let n = match b.node with + | Zero -> Int64.zero + | One -> Int64.one + | Node (v, l, h) -> + let dvl = var l - v - 1 in + let dvh = var h - v - 1 in + Int64.add + (Int64.mul (int64_two_to dvl) (count l)) + (Int64.mul (int64_two_to dvh) (count h)) + in + H1.add cache b n; + n + in + Int64.mul (int64_two_to (var b - 1)) (count b) + +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, l, _) -> mk ((v,false)::acc) l + in + mk [] + +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, l, _) when Random.bool () -> mk ((v,false) :: acc) l + | Node (v, _, h) -> mk ((v,true) :: acc) h + in + mk [] + +(* TODO: a CPS version of all_sat *) +let all_sat = + let cache = H1.create cache_default_size in + let rec mk b = + try + H1.find cache b + with Not_found -> + let res = match b.node with + | Zero -> [] + | One -> [[]] + | Node (v, l, h) -> + (List.map (fun a -> (v,false)::a) (mk l)) + @ (List.map (fun a -> (v,true)::a) (mk h)) + in + H1.add cache b res; + res + in + mk + +(* DOT pretty-printing *) + +module S = Set.Make(Bdd) + +open Format + +let format_to_dot b fmt = + fprintf fmt "digraph bdd {@\n"; + let ranks = Hashtbl.create 17 in (* var -> set of nodes *) + let add_rank v b = + try Hashtbl.replace ranks v (S.add b (Hashtbl.find ranks v)) + with Not_found -> Hashtbl.add ranks v (S.singleton b) + in + let visited = H1.create cache_default_size in + let rec visit b = + if not (H1.mem visited b) then begin + H1.add visited b (); + match b.node with + | Zero -> + fprintf fmt "%d [shape=box label=\"0\"];" b.tag + | One -> + fprintf fmt "%d [shape=box label=\"1\"];" b.tag + | Node (v, l, h) -> + add_rank v b; + fprintf fmt "%d [label=\"%a\"];" b.tag print_var v; + fprintf fmt "%d -> %d;@\n" b.tag h.tag; + fprintf fmt "%d -> %d [style=\"dashed\"];@\n" b.tag l.tag; + visit h; visit l + end + in + Hashtbl.iter + (fun v s -> + fprintf fmt "{rank=same; "; + S.iter (fun x -> fprintf fmt "%d " x.tag) s; + fprintf fmt ";}@\n" + ) + ranks; + visit b; + fprintf fmt "}@." + +let to_dot b = + Buffer.truncate Format.stdbuf 0; + format_to_dot b Format.str_formatter; + Buffer.contents Format.stdbuf + +let print_to_dot b ~file = + let c = open_out file in + let fmt = formatter_of_out_channel c in + format_to_dot b fmt; + close_out c + +let display b = + let file = Filename.temp_file "bdd" ".dot" in + print_to_dot b ~file; + let cmd = sprintf "dot -Tps %s | gv -" file in + begin try ignore (Sys.command cmd) with _ -> () end; + try Sys.remove file with _ -> () + +end (* module Session *) + +let make ?(print_var=fun ff -> Format.fprintf ff "x%d") + ?(size=7001) + max_var + = 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/bdd.mli new file mode 100644 index 0000000..e4f3d68 --- /dev/null +++ b/bdd.mli @@ -0,0 +1,155 @@ +(**************************************************************************) +(* *) +(* 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. *) +(**************************************************************************) + +(** Propositional formulas *) + +type variable = int + (** A variable is an integer, ranging from 1 to [max_var] (within + a BDD module). *) + +type formula = + | Ffalse + | Ftrue + | Fvar of variable + | Fand of formula * formula + | For of formula * formula + | Fimp of formula * formula + | Fiff of formula * formula + | Fnot of formula + +module type BDD = sig + (** Binary Decision Diagrams (BDDs) *) + + (** Number of variables *) + + val get_max_var : unit -> int + (** Returns the number of variables [max_var]. + Default value is 0, which means that bdds cannot be created + until the module is initialized using [set_max_var]. *) + + (** The abstract type of BDD nodes *) + + type t + + (** View *) + + type view = Zero | One | Node of variable * t (*low*) * t (*high*) + + val view : t -> view + (** Displays a bdd as a tree. *) + + (** Accessors *) + + val var : t -> variable + (** The root variable of a bdd. + Convention: [Zero] and [One] have variable [max_var+1] *) + + val low : t -> t + val high : t -> t + (** The low and high parts of a bdd, respectively. + [low] and [high] raise [Invalid_argument] on [Zero] and [One]. *) + + (** Constructors *) + + val zero : t + val one : t + + val make : variable -> low:t -> high:t -> t + (** Builds a bdd node. + Raises [Invalid_argument] is the variable is out of [1..max_var]. *) + + val mk_var : variable -> t + (** Builds the bdd reduced to a single variable. *) + + val mk_not : t -> t + val mk_and : t -> t -> t + val mk_or : t -> t -> t + val mk_imp : t -> t -> t + (** Builds bdds for negation, conjunction, disjunction and implication. *) + + (** Generic binary operator constructor *) + + val apply : (bool -> bool -> bool) -> t -> t -> t + + val constrain : t -> t -> t + + val restriction : t -> t -> t + + val restrict : t -> variable -> bool -> t + + val build : formula -> t + (** Builds a bdd from a propositional formula [f]. + Raises [Invalid_argument] if [f] contains a variable out of + [1..max_var]. *) + + (** Satisfiability *) + + val is_sat : t -> bool + (** Checks if a bdd is satisfiable i.e. different from [zero] *) + + val tautology : t -> bool + (** Checks if a bdd is a tautology i.e. equal to [one] *) + + val count_sat : t -> Int64.t + (** Counts the number of different ways to satisfy a bdd. *) + + val any_sat : t -> (variable * bool) list + (** Returns one truth assignment which satisfies a bdd, if any. + The result is chosen deterministically. + Raises [Not_found] if the bdd is [zero] *) + + val random_sat : t -> (variable * bool) list + (** Returns one truth assignment which satisfies a bdd, if any. + The result is chosen randomly. + Raises [Not_found] if the bdd is [zero] *) + + val all_sat : t -> (variable * bool) list list + (** Returns all truth assignments which satisfy a bdd [b]. *) + + (** Pretty printer *) + + val print_var : Format.formatter -> variable -> unit + + val to_dot : t -> string + + val print_to_dot : t -> file:string -> unit + + val display : t -> unit + (** displays the given bdd using a shell command "dot -Tps | gv -" *) + + (** Stats *) + + val stats : unit -> (int * int * int * int * int * int) array + (** Return statistics on the internal nodes tables (one for each variable). + The numbers are, in order: + table length, number of entries, sum of bucket lengths, + smallest bucket length, median bucket length, biggest bucket length. *) +end + +module Make(X: sig + val print_var: Format.formatter -> int -> unit + val size: int + val max_var: int +end) : BDD + +val make : ?print_var:(Format.formatter -> variable -> unit) + -> ?size:int + -> int + -> (module BDD) + (** Creates a BDD module with a given maximum number of variables. + Additionally, the size of the internal nodes table for each variable + can be specified. Each table has a default size (7001) and is + resized when necessary (i.e. when too many collisions occur). + The [print_var] argument can be used to associate names with variables + (by default it gives "x1", "x2", ...). *) diff --git a/bdd_sat.ml b/bdd_sat.ml new file mode 100644 index 0000000..e20603c --- /dev/null +++ b/bdd_sat.ml @@ -0,0 +1,60 @@ +(**************************************************************************) +(* *) +(* 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. *) +(**************************************************************************) + +open Format +open Prop +open Bdd + +module Time = struct + + open Unix + + let utime f x = + let u = (times()).tms_utime in + let y = f x in + let ut = (times()).tms_utime -. u in + (y,ut) + + let print_utime f x = + let (y,ut) = utime f x in + printf "user time: %2.2f@." ut; + y + +end + +let print_stats (module B : BDD) = + Array.iter + (fun (l,n,s,b1,b2,b3) -> + printf "table length: %d / nb. entries: %d / sum of bucket length: %d@." + l n s; + printf "smallest bucket: %d / median bucket: %d / biggest bucket: %d@." + b1 b2 b3) + (B.stats ()) + +let nb = ref 0 + +let sat_unsat f = + incr nb; + let nbvar, f = bdd_formula f in + let module B = (val make nbvar) in + let b = B.build f in + printf "%d: %s " !nb (if B.tautology b then "valid" else "invalid"); + print_stats (module B) + +let check = Time.print_utime sat_unsat + +let () = + let lb = Lexing.from_channel stdin in + let fl = Parser.file Lexer.token lb in + List.iter check fl diff --git a/bench_prop.ml b/bench_prop.ml new file mode 100644 index 0000000..492a7b8 --- /dev/null +++ b/bench_prop.ml @@ -0,0 +1,116 @@ +(**************************************************************************) +(* *) +(* 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. *) +(**************************************************************************) + +open Prop + +let pand p1 p2 = match p1, p2 with + | Ptrue, p2 -> p2 + | p1, Ptrue -> p1 + | _ -> Pand (p1, p2) + +let pands i j f = + let rec mk k = if k > j then Ptrue else pand (f k) (mk (k+1)) in + mk i + +let piff p1 p2 = match p1, p2 with + | Ptrue, p2 -> p2 + | p1, Ptrue -> p1 + | _ -> Piff (p1, p2) + +let piffs i j f = + let rec mk k = if k > j then Ptrue else piff (f k) (mk (k+1)) in + mk i + +let por p1 p2 = match p1, p2 with + | Pfalse, p2 -> p2 + | p1, Pfalse -> p1 + | _ -> Por (p1, p2) + +let pors i j f = + let rec mk k = if k > j then Pfalse else por (f k) (mk (k+1)) in + mk i + +(* de bruijn *) + +let var i = Pvar ("p" ^ string_of_int i) + +let iff p1 p2 = Pand (Pimp (p1, p2), Pimp (p2, p1)) + +(** +de_bruijn_p(n) == LHS(2*n+1) -> RHS(2*n+1) +de_bruijn_n(n) == LHS(2*n) -> (p0 v RHS(2*n) v ~p0) + +RHS(m) = &&_{i=1..m} p(i) +LHS(m) = &&_{i=1..m} ((p(i)<->p(i+1)) -> c(n)) +where addition is computed modulo m. +***) + +let lhs m = + pands 1 m (fun i -> Pnot (iff (var i) (var (if i=m then 1 else i+1)))) + +let de_bruijn_p n = Pnot (lhs (2*n+1)) +let de_bruijn_n n = Pnot (lhs (2*n)) + +(* pigeons + +ph_p(n) =def left(n) -> right(n) + +left(n) =def &&_{p=1..n+1} (vv_{j=1,..n} occ(i,j) ) +right(n) =def vv_{h=1..n, p1=1..{n+1}, p2={p1+1}..{n+1}} s(i1,i2,j) +s(p1,p2,h) =def occ(p1,h) & occ(p2,h) + +*) + +let occ i j = Pvar ("occ_" ^ string_of_int i ^ "_" ^ string_of_int j) + +let left n = pands 1 (n+1) (fun i -> pors 1 n (fun j -> occ i j)) +let right n = + pors 1 n (fun h -> + pors 1 (n+1) (fun p1 -> + pors (p1+1) (n+1) (fun p2 -> Pand (occ p1 h, + occ p2 h)))) + +let pigeon_p n = Pimp (left n, right n) + +let pigeon_n 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/check.ml b/check.ml new file mode 100644 index 0000000..e280c98 --- /dev/null +++ b/check.ml @@ -0,0 +1,88 @@ +(**************************************************************************) +(* *) +(* 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. *) +(**************************************************************************) + +open Bdd +open Prop + +module B = (val make 42) +let of_formula s = + let nv, f = bdd_formula (Lexer.formula_of_string s) in + assert (nv <= 42); + B.build f + +let valid s = + assert (B.tautology (of_formula s)) +let invalid s = + assert (not (B.tautology (of_formula s))) + +let () = valid " +((b <-> c) -> (a&b&c)) & +((c<->a)->(a&b&c)) & ((a<->b)->(a&b&c)) -> (a&b&c)" + +let () = valid "~ ~(~p1 \\/ ~p2 \\/ ~p3 \\/ (p1 & p2 & p3))" + +let () = valid "(a1<->a2)<->(a2<->a1)" + +let () = valid " A \\/ ~A" +let () = valid " A -> ~~A" +let () = valid " A -> A" +let () = valid " ((A -> B) -> A) -> A" +let () = valid " (A -> B)-> (~B -> ~ A)" +let () = valid " ((A -> B) & A) -> B" +let () = valid " ((A -> B) & ~ B) -> ~ A" +let () = valid " ((A -> B) & (B -> C)) -> (A -> C)" +let () = valid " (A & (B \\/ C)) -> ((A & B) \\/ (A & C))" +let () = valid " ((A & B) \\/ (A & C)) -> (A & (B \\/ C))" +let () = valid " (A \\/ (B & C)) -> ((A \\/ B) & (A \\/ C))" +let () = valid " ((A \\/ B) & (A \\/ C)) -> (A \\/ (B & C))" +let () = valid " (~ A -> A) -> A " +let () = valid " ((P -> (Q & R & S)) & ~S) -> ~P" +let () = valid " (P & Q) -> (Q & P)" +let () = valid " (A & A) \\/ ~A" +let () = valid " ~~A <-> A" +let () = valid " ~(A & B) <-> (~A \\/ ~B)" +let () = valid " ~(A \\/ B) <-> (~A & ~ B)" +let () = valid " (A \\/ (B & C)) <-> ((A \\/ B) & (A \\/ C))" +let () = valid " (A & (B \\/ C)) <-> ((A & B) \\/ (A & C))" + + +let () = invalid " A -> (A -> ~ A)" +let () = invalid " A & ~A" +let () = invalid " (A \\/ B) & ~A & ~B" +let () = invalid " (A -> B) -> (~A -> ~B)" +let () = invalid " (A -> B) -> (B -> A)" +let () = invalid " B -> (B & A)" +let () = invalid " (A -> A) <-> A" + +open Format + +let print_count_sat s = + let n = B.count_sat (of_formula s) in + printf "count_sat(%s) = %Ld@." s n + +let check_count_sat s n = + let nv, f = bdd_formula (Lexer.formula_of_string s) in + let module B = (val make nv) in + assert (B.count_sat (B.build f) = n) + +let () = check_count_sat "A" 1L +let () = check_count_sat "A \\/ B" 3L +let () = check_count_sat "A /\\ B" 1L +let () = check_count_sat "A /\\ (B \\/ C)" 3L + +let () = check_count_sat "A \\/ ~A" 2L +let () = check_count_sat "(A \\/ ~A) /\\ (B \\/ ~B)" 4L + +let () = print_endline "all tests successfully completed" + diff --git a/configure.in b/configure.in new file mode 100644 index 0000000..5676594 --- /dev/null +++ b/configure.in @@ -0,0 +1,145 @@ +########################################################################## +# # +# 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/lexer.mll b/lexer.mll new file mode 100644 index 0000000..c22646f --- /dev/null +++ b/lexer.mll @@ -0,0 +1,68 @@ +(**************************************************************************) +(* *) +(* 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. *) +(**************************************************************************) + +{ + open Lexing + open Parser + + exception Lexical_error of string + + let newline lexbuf = + let pos = lexbuf.lex_curr_p in + lexbuf.lex_curr_p <- + { pos with pos_lnum = pos.pos_lnum + 1; pos_bol = pos.pos_cnum; + pos_cnum=0 } + +} + +let space = [' ' '\t' '\r']+ +let ident = ['a'-'z' 'A'-'Z'] ['a'-'z' 'A'-'Z' '0'-'9' ':' '_']* +let number = ['0' - '9']+ + +rule token = parse + | '\n' + { newline lexbuf; token lexbuf } + | space + { token lexbuf } + | '#' [^'\n']* ('\n' | eof) + { newline lexbuf; token lexbuf } + | '(' + { LPAR } + | ')' + { RPAR } + | '~' + { NOT } + | "->" + { IMP } + | "<->" + { EQUIV } + | "/\\" | '&' + { AND } + | "\\/" | 'v' + { OR } + | ident + { IDENT (lexeme lexbuf) } + | _ + { raise (Lexical_error ("illegal character: " ^ lexeme lexbuf)) } + | eof + { EOF } + +{ + let formula_of_string s = + let lb = Lexing.from_string s in + match Parser.file token lb with + | f :: _ -> f + | _ -> assert false +} + diff --git a/misc/headache_config.txt b/misc/headache_config.txt new file mode 100644 index 0000000..6b8128c --- /dev/null +++ b/misc/headache_config.txt @@ -0,0 +1,10 @@ +# 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 new file mode 100644 index 0000000..b02cc63 --- /dev/null +++ b/misc/header.txt @@ -0,0 +1,11 @@ + +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/parser.mly b/parser.mly new file mode 100644 index 0000000..3824774 --- /dev/null +++ b/parser.mly @@ -0,0 +1,51 @@ +/**************************************************************************/ +/* */ +/* 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. */ +/**************************************************************************/ + +%{ + open Prop +%} + +%token IDENT +%token AND OR +%token IMP EQUIV +%token NOT +%token LPAR RPAR +%token EOF + +%right IMP EQUIV +%left AND OR +%right NOT + +%start file +%type file + +%% + +file: +| formulas EOF { List.rev $1} +; + +formulas: +| { [] } +| formulas formula { $2 :: $1 } + +formula: +| IDENT { Pvar $1 } +| formula IMP formula { Pimp($1,$3) } +| formula EQUIV formula { Piff($1,$3) } +| formula AND formula { Pand($1,$3) } +| formula OR formula { Por($1,$3) } +| NOT formula { Pnot($2) } +| LPAR formula RPAR { $2 } +; diff --git a/path.ml b/path.ml new file mode 100644 index 0000000..343713d --- /dev/null +++ b/path.ml @@ -0,0 +1,99 @@ +(**************************************************************************) +(* *) +(* 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. *) +(**************************************************************************) + +open Format + +let w = int_of_string Sys.argv.(1) +let h = int_of_string Sys.argv.(2) + +let edges = ref [] + +let add_edge v1 v2 = edges := (v1, v2) :: !edges + +let () = + for i = 0 to w do for j = 0 to h do + if i < w then add_edge (i,j) (i+1,j); (* right *) + if j < h then add_edge (i,j) (i,j+1); (* down *) + done done + +let edges = Array.of_list !edges + +let n_edges = Array.length edges +let () = printf "%d edges@." n_edges + +include (val Bdd.make n_edges) + +let adj = Hashtbl.create 17 + +let () = + for i = 0 to n_edges - 1 do + let e = i+1 in + let v1,v2 = edges.(i) in + Hashtbl.add adj v1 e; + Hashtbl.add adj v2 e + done + +let rec iter_pairs f = function + | [] | [_] -> + () + | x :: l -> + List.iter (f x) l; + iter_pairs f l + +let exactly_two_neighbors v = + let adj_v = Hashtbl.find_all adj v in + let b = ref zero in + iter_pairs + (fun e1 e2 -> (* e1 <> e2 *) + (* we have edges e1 and e2 *) + let b1 = ref (mk_and (mk_var e1) (mk_var e2)) in + (* and no other edge for v *) + List.iter + (fun e -> + if e <> e1 && e <> e2 then + b1 := mk_and !b1 (mk_not (mk_var e))) + adj_v; + b := mk_or !b !b1) + adj_v; + !b + +let () = + printf "creating the bdd...@."; + let bdd = ref one in + for i = 0 to w do for j = 0 to h do + printf "%d,%d @?" i j; + let v = i,j in + bdd := mk_and !bdd (exactly_two_neighbors v) + done done; + (* display !bdd; *) + printf "counting...@."; + printf "%Ld paths@." (count_sat !bdd); +(* List.iter *) +(* (fun ta -> *) +(* List.iter *) +(* (fun (e,b) -> *) +(* if b then *) +(* let (i1,j1),(i2,j2) = edges.(e-1) in *) +(* printf "%d,%d -- %d,%d " i1 j1 i2 j2) *) +(* ta; *) +(* printf "---@." *) +(* ) *) +(* (all_sat !bdd); *) + () + +(* +Local Variables: +compile-command: "make path.opt" +End: +*) diff --git a/prop.ml b/prop.ml new file mode 100644 index 0000000..18e979c --- /dev/null +++ b/prop.ml @@ -0,0 +1,62 @@ +(**************************************************************************) +(* *) +(* 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. *) +(**************************************************************************) + +(** Propositional formulas with named variables + (contrary to [Bdd.formula] where variables are integers). *) + +type t = + | Pvar of string + | Pnot of t + | Pand of t * t + | Por of t * t + | Pimp of t * t + | Piff of t * t + | Ptrue + | Pfalse + +open Format + +let print fmt p = + let rec pr fmt = function + | Pvar s -> fprintf fmt "%s" s + | Pnot f -> fprintf fmt "(~%a)" pr f + | Pand (f1, f2) -> fprintf fmt "(%a &@ %a)" pr f1 pr f2 + | Por (f1, f2) -> fprintf fmt "(%a v@ %a)" pr f1 pr f2 + | Pimp (f1, f2) -> fprintf fmt "(%a ->@ %a)" pr f1 pr f2 + | Piff (f1, f2) -> fprintf fmt "(%a <->@ %a)" pr f1 pr f2 + | Ptrue -> fprintf fmt "true" + | Pfalse -> fprintf fmt "false" + in + fprintf fmt "@[%a@]" pr p + +open Bdd + +let bdd_formula f = + let nbvar = ref 0 in + let vars = Hashtbl.create 17 in + let rec trans = function + | Pvar s -> + Fvar + (try Hashtbl.find vars s + with Not_found -> incr nbvar; Hashtbl.add vars s !nbvar; !nbvar) + | Pnot f -> Fnot (trans f) + | Pand (f1, f2) -> Fand (trans f1, trans f2) + | Por (f1, f2) -> For (trans f1, trans f2) + | Pimp (f1, f2) -> Fimp (trans f1, trans f2) + | Piff (f1, f2) -> Fiff (trans f1, trans f2) + | Ptrue -> Ftrue + | Pfalse -> Ffalse + in + let f = trans f in + !nbvar, f diff --git a/queen.ml b/queen.ml new file mode 100644 index 0000000..43164b6 --- /dev/null +++ b/queen.ml @@ -0,0 +1,72 @@ +(**************************************************************************) +(* *) +(* 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. *) +(**************************************************************************) + +open Format + +let n = try int_of_string Sys.argv.(1) with _ -> eprintf "queen N"; exit 1 +include (val Bdd.make (n * n)) + +let fold_and i j f = + let rec mk k = if k > j then one else mk_and (f k) (mk (k+1)) in + mk i + +let fold_or i j f = + let rec mk k = if k > j then zero else mk_or (f k) (mk (k+1)) in + mk i + +let fold_for i j f = + let rec fold k acc = if k > j then acc else fold (k+1) (f k acc) in + fold i + +(* 0..n-1 x 0..n-1 -> 1..n x n *) +let vars = + Array.init n (fun i -> Array.init n (fun j -> mk_var (1 + n * i + j))) +let var i j = vars.(i).(j) + +let constraints i j = + let b1 = + fold_and 0 (n-1) + (fun l -> if l = j then one else mk_not (var i l)) + in + let b2 = + fold_and 0 (n-1) + (fun k -> if k = i then one else mk_not (var k j)) + in + let b3 = + fold_and 0 (n-1) + (fun k -> + let ll = j+k-i in + if ll >= 0 && ll < n && k <> i then mk_not (var k ll) else one) + in + let b4 = + fold_and 0 (n-1) + (fun k -> + let ll = j+i-k in + if ll >= 0 && ll < n && k <> i then mk_not (var k ll) else one) + in + mk_and b1 (mk_and b2 (mk_and b3 b4)) + +let bdd = + fold_and 0 (n-1) (fun i -> fold_or 0 (n-1) (fun j -> var i j)) + +let bdd = + fold_for 0 (n-1) + (fun i acc -> + fold_for 0 (n-1) + (fun j acc -> + mk_and acc (mk_imp (var i j) (constraints i j))) + acc) + bdd + +let () = printf "There are %Ld solutions@." (count_sat bdd) diff --git a/test.ml b/test.ml new file mode 100644 index 0000000..2ba06d2 --- /dev/null +++ b/test.ml @@ -0,0 +1,85 @@ +(**************************************************************************) +(* *) +(* 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. *) +(**************************************************************************) + +open Bdd +open Prop + +let p s = + let lb = Lexing.from_string s in + match Parser.file Lexer.token lb with + | f :: _ -> f + | _ -> assert false + +module B = (val make 42) + +let of_formula s = + let nv, f = bdd_formula (p s) in assert (nv <= 42); B.build f +let test s = B.display (of_formula s) +let count s = B.count_sat (of_formula s) + +let display b = + B.print_to_dot b ~file:"test.dot"; + ignore (Sys.command "dot -Tpdf test.dot > test.pdf"); + ignore (Sys.command "evince test.pdf") + +let test2 s = let b = of_formula s in display b + +let r = 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 r = 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 de_bruijn_p_2 = test " +(((((p1 -> p2) & (p2 -> p1)) -> (p1 & (p2 & (p3 & (p4 & p5))))) & ((((p2 -> +p3) & (p3 -> p2)) -> (p1 & (p2 & (p3 & (p4 & p5))))) & ((((p3 -> p4) & (p4 -> +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 () = + let _, b = bdd_formula (Bench_prop.de_bruijn_n 5) in + B.display (B.build b) diff --git a/tiling.ml b/tiling.ml new file mode 100644 index 0000000..37a8191 --- /dev/null +++ b/tiling.ml @@ -0,0 +1,87 @@ +(**************************************************************************) +(* *) +(* 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. *) +(**************************************************************************) + +(* Tiling the 8x8 chessboard with 2x1 dominoes + (cf TAOCP vol 4, Section 7.1.4, page 49) *) + +(* there are 2x7x8 = 112 variables *) +let n = 112 +include (val Bdd.make n) +let var i = mk_var (1+i) + +(* m[i,j] tells whether domino i occupies cell j *) +let m = Array.make_matrix n 64 false + +let () = + let v = ref 0 in + for l = 0 to 7 do for c = 0 to 7 do + (* cell (l,c) of the chessboard is j = 8*l + c *) + let j = 8 * l + c in + (* horizontal domino *) + if c < 7 then begin + m.(!v).(j) <- true; m.(!v).(j+1) <- true; + incr v; + end; + (* vertical domino *) + if l < 7 then begin + m.(!v).(j) <- true; m.(!v).(j+8) <- true; + incr v; + end; + done done + +(* col j is the list of all i such that m[i,j]=true *) +let col j = + let rec make acc i = + if i = n then acc else make (if m.(i).(j) then i::acc else acc) (i+1) + in + make [] 0 + +let bdd = + let rec make bdd j = + if j = 64 then + bdd + else + let cell_j = + let cj = col j in + List.fold_left + (fun f i -> + mk_or f + (List.fold_left + (fun f i' -> + if i' <> i then mk_and f (mk_not (var i')) else f) + (var i) + cj)) + zero cj + in + make (mk_and bdd cell_j) (j+1) + in + make one 0 + +open Format + +let () = + printf "%Ld solutions@." (count_sat bdd) + +(* 12988816 solutions *) + +let () = + let s = random_sat bdd in + List.iter + (fun (v,b) -> + let i = v-1 in + if b then begin + Array.iteri (fun j mij -> if mij then printf "%d " j) m.(i); + printf "@." + end) + s