diff --git a/HasCacBDD.cabal b/HasCacBDD.cabal new file mode 100644 --- /dev/null +++ b/HasCacBDD.cabal @@ -0,0 +1,75 @@ +name: HasCacBDD +version: 0.1.0.0 +synopsis: Haskell bindings for CacBDD +homepage: https://github.com/m4lvin/HasCacBDD +license: GPL-2 +license-file: LICENSE +author: Malvin Gattinger +maintainer: malvin@w4eg.de +category: Data +build-type: Custom +cabal-version: >=1.23 + +description: Haskell bindings for CacBDD, a Binary Decision Diagram (BDD) package with dynamic cache management. + Original C++ code from and a C wrapper are included. + +extra-source-files: + README.md + stack.yaml + c/BDDNodeC.cpp + c/BDDNodeC.h + c/Makefile + cpp/*.cpp + cpp/*.h + cpp/Makefile + cpp/OriginalMakefile + cpp/README + +source-repository head + type: git + location: git://github.com/m4lvin/HasCacBDD.git + +custom-setup + setup-depends: base >= 4.8 && < 5, + Cabal, + directory + +library + exposed-modules: Data.HasCacBDD, + Data.HasCacBDD.Visuals + build-depends: base >=4.8 && < 5, + process >= 1.1, + QuickCheck + default-language: Haskell2010 + hs-source-dirs: hs + extra-libraries: stdc++, CacBDD + cc-options: -fPIC -shared + ghc-options: -pgml g++ -Wall -fPIC -fno-full-laziness + +test-suite example + default-language: Haskell2010 + type: exitcode-stdio-1.0 + main-is: Example.hs + hs-source-dirs: tests + build-depends: base >=4.8, + HasCacBDD + ghc-options: -pgml g++ -Wall -fPIC -fno-full-laziness + +test-suite basics + default-language: Haskell2010 + type: exitcode-stdio-1.0 + main-is: Basics.hs + hs-source-dirs: tests + build-depends: base >=4.8, + HasCacBDD + ghc-options: -Wall + +test-suite tautologies + default-language: Haskell2010 + type: exitcode-stdio-1.0 + main-is: Tautologies.hs + hs-source-dirs: tests + build-depends: base >=4.8, + HasCacBDD, + QuickCheck > 2.4 + ghc-options: -Wall -fhpc -fforce-recomp diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,340 @@ + GNU GENERAL PUBLIC LICENSE + Version 2, June 1991 + + Copyright (C) 1989, 1991 Free Software Foundation, Inc., + 51 Franklin Street, 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. + + Preamble + + The licenses for most software are designed to take away your +freedom to share and change it. By contrast, the GNU General Public +License is intended to guarantee your freedom to share and change free +software--to make sure the software is free for all its users. This +General Public License applies to most of the Free Software +Foundation's software and to any other program whose authors commit to +using it. (Some other Free Software Foundation software is covered by +the GNU Lesser General Public License instead.) You can apply it to +your programs, too. + + When we speak of free software, we are referring to freedom, 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 or use pieces of it +in new free programs; and that you know you can do these things. + + To protect your rights, we need to make restrictions that forbid +anyone to deny you these rights or to ask you to surrender the rights. +These restrictions translate to certain responsibilities for you if you +distribute copies of the software, or if you modify it. + + For example, if you distribute copies of such a program, whether +gratis or for a fee, you must give the recipients all the rights that +you have. You must make sure that they, too, receive or can get the +source code. And you must show them these terms so they know their +rights. + + We protect your rights with two steps: (1) copyright the software, and +(2) offer you this license which gives you legal permission to copy, +distribute and/or modify the software. + + Also, for each author's protection and ours, we want to make certain +that everyone understands that there is no warranty for this free +software. If the software is modified by someone else and passed on, we +want its recipients to know that what they have is not the original, so +that any problems introduced by others will not reflect on the original +authors' reputations. + + Finally, any free program is threatened constantly by software +patents. We wish to avoid the danger that redistributors of a free +program will individually obtain patent licenses, in effect making the +program proprietary. To prevent this, we have made it clear that any +patent must be licensed for everyone's free use or not licensed at all. + + The precise terms and conditions for copying, distribution and +modification follow. + + GNU GENERAL PUBLIC LICENSE + TERMS AND CONDITIONS FOR COPYING, DISTRIBUTION AND MODIFICATION + + 0. This License applies to any program or other work which contains +a notice placed by the copyright holder saying it may be distributed +under the terms of this General Public License. The "Program", below, +refers to any such program or work, and a "work based on the Program" +means either the Program or any derivative work under copyright law: +that is to say, a work containing the Program or a portion of it, +either verbatim or with modifications and/or translated into another +language. (Hereinafter, translation is included without limitation in +the term "modification".) Each licensee is addressed as "you". + +Activities other than copying, distribution and modification are not +covered by this License; they are outside its scope. The act of +running the Program is not restricted, and the output from the Program +is covered only if its contents constitute a work based on the +Program (independent of having been made by running the Program). +Whether that is true depends on what the Program does. + + 1. You may copy and distribute verbatim copies of the Program's +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 give any other recipients of the Program a copy of this License +along with the Program. + +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 Program or any portion +of it, thus forming a work based on the Program, 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) You must cause the modified files to carry prominent notices + stating that you changed the files and the date of any change. + + b) You must cause any work that you distribute or publish, that in + whole or in part contains or is derived from the Program or any + part thereof, to be licensed as a whole at no charge to all third + parties under the terms of this License. + + c) If the modified program normally reads commands interactively + when run, you must cause it, when started running for such + interactive use in the most ordinary way, to print or display an + announcement including an appropriate copyright notice and a + notice that there is no warranty (or else, saying that you provide + a warranty) and that users may redistribute the program under + these conditions, and telling the user how to view a copy of this + License. (Exception: if the Program itself is interactive but + does not normally print such an announcement, your work based on + the Program is not required to print an announcement.) + +These requirements apply to the modified work as a whole. If +identifiable sections of that work are not derived from the Program, +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 Program, 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 Program. + +In addition, mere aggregation of another work not based on the Program +with the Program (or with a work based on the Program) on a volume of +a storage or distribution medium does not bring the other work under +the scope of this License. + + 3. You may copy and distribute the Program (or a work based on it, +under Section 2) in object code or executable form under the terms of +Sections 1 and 2 above provided that you also do one of the following: + + a) 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; or, + + b) Accompany it with a written offer, valid for at least three + years, to give any third party, for a charge no more than your + cost of physically performing source distribution, a complete + machine-readable copy of the corresponding source code, to be + distributed under the terms of Sections 1 and 2 above on a medium + customarily used for software interchange; or, + + c) Accompany it with the information you received as to the offer + to distribute corresponding source code. (This alternative is + allowed only for noncommercial distribution and only if you + received the program in object code or executable form with such + an offer, in accord with Subsection b above.) + +The source code for a work means the preferred form of the work for +making modifications to it. For an executable work, 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 executable. However, as a +special exception, the source code 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. + +If distribution of executable or 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 counts as +distribution of the source code, even though third parties are not +compelled to copy the source along with the object code. + + 4. You may not copy, modify, sublicense, or distribute the Program +except as expressly provided under this License. Any attempt +otherwise to copy, modify, sublicense or distribute the Program 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. + + 5. 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 Program or its derivative works. These actions are +prohibited by law if you do not accept this License. Therefore, by +modifying or distributing the Program (or any work based on the +Program), you indicate your acceptance of this License to do so, and +all its terms and conditions for copying, distributing or modifying +the Program or works based on it. + + 6. Each time you redistribute the Program (or any work based on the +Program), the recipient automatically receives a license from the +original licensor to copy, distribute or modify the Program 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 to +this License. + + 7. 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 Program at all. For example, if a patent +license would not permit royalty-free redistribution of the Program 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 Program. + +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. + + 8. If the distribution and/or use of the Program is restricted in +certain countries either by patents or by copyrighted interfaces, the +original copyright holder who places the Program 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. + + 9. The Free Software Foundation may publish revised and/or new versions +of the 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 Program +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 Program does not specify a version number of +this License, you may choose any version ever published by the Free Software +Foundation. + + 10. If you wish to incorporate parts of the Program into other free +programs whose distribution conditions are different, 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 + + 11. BECAUSE THE PROGRAM IS LICENSED FREE OF CHARGE, THERE IS NO WARRANTY +FOR THE PROGRAM, TO THE EXTENT PERMITTED BY APPLICABLE LAW. EXCEPT WHEN +OTHERWISE STATED IN WRITING THE COPYRIGHT HOLDERS AND/OR OTHER PARTIES +PROVIDE THE PROGRAM "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 PROGRAM IS WITH YOU. SHOULD THE +PROGRAM PROVE DEFECTIVE, YOU ASSUME THE COST OF ALL NECESSARY SERVICING, +REPAIR OR CORRECTION. + + 12. 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 PROGRAM 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 PROGRAM (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 PROGRAM TO OPERATE WITH ANY OTHER +PROGRAMS), 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 Programs + + If you develop a new program, and you want it to be of the greatest +possible use to the public, the best way to achieve this is to make it +free software which everyone can redistribute and change under these terms. + + To do so, attach the following notices to the program. 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. + + {description} + Copyright (C) {year} {fullname} + + This program is free software; you can redistribute it and/or modify + it under the terms of the GNU General Public License as published by + the Free Software Foundation; either version 2 of the License, or + (at your option) any later version. + + This program 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 General Public License for more details. + + You should have received a copy of the GNU General Public License along + with this program; if not, write to the Free Software Foundation, Inc., + 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA. + +Also add information on how to contact you by electronic and paper mail. + +If the program is interactive, make it output a short notice like this +when it starts in an interactive mode: + + Gnomovision version 69, Copyright (C) year name of author + Gnomovision comes with ABSOLUTELY NO WARRANTY; for details type `show w'. + This is free software, and you are welcome to redistribute it + under certain conditions; type `show c' for details. + +The hypothetical commands `show w' and `show c' should show the appropriate +parts of the General Public License. Of course, the commands you use may +be called something other than `show w' and `show c'; they could even be +mouse-clicks or menu items--whatever suits your program. + +You should also get your employer (if you work as a programmer) or your +school, if any, to sign a "copyright disclaimer" for the program, if +necessary. Here is a sample; alter the names: + + Yoyodyne, Inc., hereby disclaims all copyright interest in the program + `Gnomovision' (which makes passes at compilers) written by James Hacker. + + {signature of Ty Coon}, 1 April 1989 + Ty Coon, President of Vice + +This General Public License does not permit incorporating your program into +proprietary programs. If your program is a subroutine library, you may +consider it more useful to permit linking proprietary applications with the +library. If this is what you want to do, use the GNU Lesser General +Public License instead of this License. + diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -0,0 +1,8 @@ +HasCacBDD +========= + +[![Build Status](https://travis-ci.org/m4lvin/HasCacBDD.svg?branch=master)](https://travis-ci.org/m4lvin/HasCacBDD) + +Haskell bindings for CacBDD, a Binary Decision Diagram (BDD) package with dynamic cache management. + +Original C++ code from and a C wrapper are included. diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,58 @@ +module Main where + +import Data.Maybe +import Distribution.PackageDescription hiding (Flag) +import Distribution.Simple +import Distribution.Simple.LocalBuildInfo +import Distribution.Simple.Setup +import Distribution.Simple.Utils +import System.Directory + +main :: IO () +main = defaultMainWithHooks simpleUserHooks + { + preConf = makeExtLib + , confHook = \a f -> confHook simpleUserHooks a f >>= updateExtraLibDirs + , postCopy = copyExtLib + , postClean = cleanExtLib + } + +makeExtLib :: Args -> ConfigFlags -> IO HookedBuildInfo +makeExtLib _ flags = do + let verbosity = fromFlag $ configVerbosity flags + rawSystemExit verbosity "env" ["make", "--directory=cpp"] + rawSystemExit verbosity "env" ["make", "--directory=c"] + return emptyHookedBuildInfo + +updateExtraLibDirs :: LocalBuildInfo -> IO LocalBuildInfo +updateExtraLibDirs localBuildInfo = do + let myPackageDescription = localPkgDescr localBuildInfo + lib = fromJust $ library myPackageDescription + libBuild = libBuildInfo lib + dir <- getCurrentDirectory + print (dir ++ "/c") + return localBuildInfo { + localPkgDescr = myPackageDescription { + library = Just $ lib { + libBuildInfo = libBuild { + extraLibDirs = (dir ++ "/c") : + extraLibDirs libBuild + } + } + } + } + +copyExtLib :: Args -> CopyFlags -> PackageDescription -> LocalBuildInfo -> IO () +copyExtLib _ flags pkg_descr lbi = do + let libPref = libdir . absoluteInstallDirs pkg_descr lbi + . fromFlag . copyDest + $ flags + let verbosity = fromFlag $ copyVerbosity flags + rawSystemExit verbosity "cp" ["c/libCacBDD.a", libPref] + +cleanExtLib :: Args -> CleanFlags -> PackageDescription -> () -> IO () +cleanExtLib _ flags _ _ = + let verbosity = fromFlag $ cleanVerbosity flags + in do + rawSystemExit verbosity "env" ["make", "--directory=c", "clean"] + rawSystemExit verbosity "env" ["make", "--directory=cpp", "clean"] diff --git a/c/BDDNodeC.cpp b/c/BDDNodeC.cpp new file mode 100644 --- /dev/null +++ b/c/BDDNodeC.cpp @@ -0,0 +1,60 @@ +#include "BDDNodeC.h" + +#include "BDDNode.h" +#include + +BDD* BDD_new() { return new BDD(); } + +int BDD_Variable(BDD* this_ptr) { return this_ptr->Variable(); } + +BDD BDD_Then(const BDD* this_ptr) { return this_ptr->Then(); } + +BDD BDD_Else(const BDD* this_ptr) { return this_ptr->Else(); } + +BDD BDD_Exist(BDD* this_ptr, const BDD* cube) { return this_ptr->Exist(*cube); } + +BDD BDD_Universal(BDD* this_ptr, const BDD* cube) { return this_ptr->Universal(*cube); } + +BDD BDD_Restrict(const BDD* this_ptr, const BDD* other) { return this_ptr->Restrict(*other); } + +BDD BDD_Compose(const BDD* this_ptr, int v, const BDD* other) { return this_ptr->Compose(v, *other); } + +BDD BDD_Permute(const BDD* this_ptr, const vector* permu) { return this_ptr->Permute(*permu); } + +BDD BDD_AndExist(BDD* this_ptr, const BDD* other, const BDD* cube) { return this_ptr->AndExist(*other, *cube); } + +bool BDD_IsComp(BDD* this_ptr) { bool b = this_ptr->IsComp(); return b; } + +const XManager* BDD_manager(const BDD* this_ptr) { return this_ptr->manager(); } + +XBDDManager* XBDDManager_new(int varCount) { return new XBDDManager(varCount); } + +BDD XBDDManager_BddOne(XBDDManager* this_ptr) { return (BDD) this_ptr->BddOne(); } + +BDD XBDDManager_BddZero(XBDDManager* this_ptr) { return (BDD) this_ptr->BddZero(); } + +BDD XBDDManager_BddVar(XBDDManager* this_ptr, int varIndex) { BDD bar = this_ptr->BddVar(varIndex); return bar; } + +BDD XBDDManager_Ite(XBDDManager* this_ptr, const BDD* f, const BDD* g, const BDD* h) { return (BDD) this_ptr->Ite(*f, *g, *h); } + +const XManager* XBDDManager_manager(const XBDDManager* this_ptr) { return this_ptr->manager(); } + +BDD BDD_Operator_Not(const BDD* this_ptr) { BDD bar = (! *this_ptr); return bar; } + +bool BDD_Operator_Equal(const BDD* this_ptr, const BDD* other) { bool b = (*this_ptr == *other); return b; } + +BDD BDD_Operator_Or(const BDD* this_ptr, const BDD* other) { BDD bar = (*this_ptr + *other); return bar; } + +BDD BDD_Operator_And(const BDD* this_ptr, const BDD* other) { return(BDD) (*this_ptr * *other); } + +BDD BDD_Operator_Xor(const BDD* this_ptr, const BDD* other) { return(BDD) (*this_ptr ^ *other); } + +BDD BDD_Operator_LessEqual(const BDD* this_ptr, const BDD* other) { return(BDD) (*this_ptr <= *other); } + +BDD BDD_Operator_Nor(const BDD* this_ptr, const BDD* other) { return (BDD) (*this_ptr % *other); } + +BDD BDD_Operator_Nand(const BDD* this_ptr, const BDD* other) { return(BDD) (*this_ptr | *other); } + +BDD BDD_Operator_XNor(const BDD* this_ptr, const BDD* other) { return(BDD) (*this_ptr & *other); } + +void XBDDManager_ShowInfo(XBDDManager* this_ptr, double vtime) { return this_ptr->ShowInfo(); } diff --git a/c/BDDNodeC.h b/c/BDDNodeC.h new file mode 100644 --- /dev/null +++ b/c/BDDNodeC.h @@ -0,0 +1,39 @@ +#include + +extern "C" { + +BDD* BDD_new(); +const XManager* BDD_checkSameManager(const BDD* this_ptr, const BDD* other); +int BDD_Variable(BDD* this_ptr); +BDD BDD_Then(const BDD* this_ptr); +BDD BDD_Else(const BDD* this_ptr); +BDD BDD_Exist(BDD* this_ptr, const BDD* cube); +BDD BDD_Universal(BDD* this_ptr, const BDD* cube); +BDD BDD_Restrict(const BDD* this_ptr, const BDD* other); +BDD BDD_Compose(const BDD* this_ptr, int v, const BDD* other); +BDD BDD_Permute(const BDD* this_ptr, const vector* permu); +BDD BDD_AndExist(BDD* this_ptr, const BDD* other, const BDD* cube); +bool BDD_IsComp(BDD* this_ptr); +const XManager* BDD_manager(const BDD* this_ptr); + +// In C we can not overload operators, so we use functions instead. +BDD BDD_Operator_Not (const BDD* this_ptr); // ! +bool BDD_Operator_Equal (const BDD* this_ptr, const BDD* other); // == +BDD BDD_Operator_Or (const BDD* this_ptr, const BDD* other); // + +BDD BDD_Operator_And (const BDD* this_ptr, const BDD* other); // * +BDD BDD_Operator_Xor (const BDD* this_ptr, const BDD* other); // ^ +BDD BDD_Operator_LessEqual (const BDD* this_ptr, const BDD* other); // <= +BDD BDD_Operator_Nor (const BDD* this_ptr, const BDD* other); // % +BDD BDD_Operator_Nand (const BDD* this_ptr, const BDD* other); // | +BDD BDD_Operator_XNor (const BDD* this_ptr, const BDD* other); // & + +XBDDManager* XBDDManager_new(int varCount); +BDD XBDDManager_BddOne(XBDDManager* this_ptr); +BDD XBDDManager_BddZero(XBDDManager* this_ptr); +BDD XBDDManager_BddVar(XBDDManager* this_ptr, int varIndex); +BDD XBDDManager_Ite(XBDDManager* this_ptr, const BDD* f, const BDD* g, const BDD* h); + +void XBDDManager_ShowInfo(XBDDManager* this_ptr, double vtime); + +const XManager* XBDDManager_manager(const XBDDManager* this_ptr); +} diff --git a/c/Makefile b/c/Makefile new file mode 100644 --- /dev/null +++ b/c/Makefile @@ -0,0 +1,14 @@ + +C = g++ +CFLAGS = -g -c -shared -fPIC + +LIBFILE = libCacBDD.a + +default: + $(C) $(CFLAGS) -I../cpp -o libBDDNodeC.so BDDNodeC.cpp + rm -f $(LIBFILE) + ar rvs $(LIBFILE) libBDDNodeC.so + ar rvs $(LIBFILE) ../cpp/*.o + +clean: + rm -f *.a *.o *.so *.gch diff --git a/cpp/BDDNode.cpp b/cpp/BDDNode.cpp new file mode 100644 --- /dev/null +++ b/cpp/BDDNode.cpp @@ -0,0 +1,260 @@ +/***************************************************************************** +Copyright (c) 2012 - 2013, The Board of Trustees of the University of Beijing Technology and +the University of Griffith. +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are +met: + +* Redistributions of source code must retain the above + copyright notice, this list of conditions and the + following disclaimer. + +* Redistributions in binary form must reproduce the + above copyright notice, this list of conditions + and the following disclaimer in the documentation + and/or other materials provided with the distribution. + +* Neither the name of the University of Beijing Technology and + the University of Griffith nor the names of its contributors + may be used to endorse or promote products derived from this + software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS +IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, +THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR +PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR +CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. +*****************************************************************************/ + +/***************************************************************************** +written by + Guanfeng Lv, last updated 10/26/2012 +*****************************************************************************/ + +#include "BDDNode.h" +#include "Manager.h" +#include + +BDD::BDD(XManager *m, DD vNode) +{ + mgr = m; + node = vNode; + m->externalBDDs.insert(this); +} + +BDD::BDD(const BDD &right) +{ + mgr = right.mgr; + node = right.node; + mgr->externalBDDs.insert(this); +} + +BDD::BDD() +{ + mgr = 0; + node = 0; +} + +BDD::~BDD() +{ + if(mgr != NULL){ + mgr->externalBDDs.erase(this); + } +} + +XManager *BDD::manager() const +{ + return mgr; +} + +DD BDD::Node() const +{ + return node; +} + +BDD &BDD::operator=(const BDD& right) +{ + if (this == &right) return *this; + node = right.node; + mgr = right.manager(); + mgr->externalBDDs.insert(this); + return *this; +} + +inline XManager *BDD::checkSameManager( const BDD &other) const +{ + if (mgr != other.mgr) { + printf("\nERROR: Operands come from different manager.\n"); + } + return mgr; +} + +bool BDD::operator==(const BDD& other) const +{ + checkSameManager(other); + return node == other.node; +} + +bool BDD::operator!=(const BDD& other) const +{ + this->checkSameManager(other); + return node != other.node; +} + +BDD BDD::operator!() const +{ + return BDD(mgr, mgr->Not(node)); +} + +BDD BDD::operator+(const BDD& other) const +{ + XManager *mgr = this->checkSameManager(other); + DD result = mgr->Or(node, other.node); + + return BDD(mgr, result); +} + +BDD BDD::operator*( const BDD& other) const +{ + XManager *mgr = this->checkSameManager(other); + DD result = mgr->And(node, other.node); + + return BDD(mgr, result); +} + +BDD BDD::operator^(const BDD& other) const +{ + XManager *mgr = this->checkSameManager(other); + DD result = mgr->Xor(node, other.node); + + return BDD(mgr, result); +} + +BDD BDD::operator<(const BDD& other) const +{ + XManager *mgr = this->checkSameManager(other); + DD result = mgr->LessThan(node, other.node); + + return BDD(mgr, result); +} + +BDD BDD::operator>(const BDD& other) const +{ + XManager *mgr = this->checkSameManager(other); + DD result = mgr->MoreThan(node, other.node); + + return BDD(mgr, result); +} + +BDD BDD::operator<=(const BDD& other) const +{ + XManager *mgr = this->checkSameManager(other); + DD result = mgr->LessEqual(node, other.node); + + return BDD(mgr, result); +} + +BDD BDD::operator>=(const BDD& other) const +{ + XManager *mgr = this->checkSameManager(other); + DD result = mgr->MoreEqual(node, other.node); + + return BDD(mgr, result); +} + +BDD BDD::operator%(const BDD& other) const +{ + XManager *mgr = this->checkSameManager(other); + DD result = mgr->Nor(node, other.node); + return BDD(mgr, result); +} + +BDD BDD::operator|(const BDD& other) const +{ + XManager *mgr = this->checkSameManager(other); + DD result = mgr->Nand(node, other.node); + return BDD(mgr, result); +} + +BDD BDD::operator&(const BDD& other) const +{ + XManager *mgr = this->checkSameManager(other); + DD result = mgr->Xnor(node, other.node); + return BDD(mgr, result); +} + +int BDD::Variable() +{ + return mgr->Variable(node); +} + +BDD BDD::Then() const +{ + DD result = mgr->Then(node, mgr->Variable(node)); + return BDD(mgr, result); +} + +BDD BDD::Else() const +{ + DD result = mgr->Else(node, mgr->Variable(node)); + return BDD(mgr, result); +} + +BDD BDD::Exist(const BDD& cube) +{ + XManager *mgr = this->checkSameManager(cube); + DD result = mgr->Exist(node, cube.node); + return BDD(mgr, result); +} + +BDD BDD::Universal(const BDD& cube) +{ + XManager *mgr = this->checkSameManager(cube); + DD result = mgr->Universal(node, cube.node); + return BDD(mgr, result); +} + +BDD BDD::Restrict(const BDD& other) const +{ + XManager *mgr = this->checkSameManager(other); + DD result = mgr->Restrict(node, other.node); + return BDD(mgr, result); +} + +BDD BDD::Compose(int v, const BDD& other) const +{ + XManager *mgr = this->checkSameManager(other); + DD result = mgr->Compose(node, v, other.node); + return BDD(mgr, result); +} + +BDD BDD::Permute(const vector &permu) const +{ + int *x = new int[permu.size()]; + for(int i=0; iPermute(node, x); + delete []x; + return BDD(mgr, result); +} + +BDD BDD::AndExist(const BDD& other, const BDD& cube) +{ + XManager *mgr = this->checkSameManager(other); + DD result = mgr->AndExist(node, other.node, cube.node); + return BDD(mgr, result); +} + +void BDD::Support(vector &vars) +{ + mgr->Support(node, vars); +} diff --git a/cpp/BDDNode.h b/cpp/BDDNode.h new file mode 100644 --- /dev/null +++ b/cpp/BDDNode.h @@ -0,0 +1,121 @@ +/***************************************************************************** +Copyright (c) 2012 - 2013, The Board of Trustees of the University of Beijing Technology and +the University of Griffith. +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are +met: + +* Redistributions of source code must retain the above + copyright notice, this list of conditions and the + following disclaimer. + +* Redistributions in binary form must reproduce the + above copyright notice, this list of conditions + and the following disclaimer in the documentation + and/or other materials provided with the distribution. + +* Neither the name of the University of Beijing Technology and + the University of Griffith nor the names of its contributors + may be used to endorse or promote products derived from this + software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS +IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, +THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR +PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR +CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. +*****************************************************************************/ + +/***************************************************************************** +written by + Guanfeng Lv, last updated 10/26/2012 +*****************************************************************************/ + +#ifndef _BDDNODE_ +#define _BDDNODE_ + +#include "Manager.h" + +class BDD{ +private: + friend class XManager; + friend class XBDDManager; + DD node; + XManager *mgr; +public: + BDD(XManager *m, DD vNode); + BDD(const BDD &right); + BDD(); + ~BDD(); + + inline XManager *checkSameManager( const BDD &other) const; + bool operator==(const BDD& other) const; + bool operator!=(const BDD& other) const; + BDD& operator=(const BDD& right); + BDD operator!() const; // Not + BDD operator+(const BDD& other) const; // Or + BDD operator*(const BDD& other) const; // And + BDD operator^(const BDD& other) const; // Xor + BDD operator<(const BDD& other) const; // Less than + BDD operator>(const BDD& other) const; // More than + BDD operator<=(const BDD& other) const;// Less equal + BDD operator>=(const BDD& other) const;// More equal + BDD operator%(const BDD& other) const; // Nor + BDD operator|(const BDD& other) const; // Nand + BDD operator&(const BDD& other) const; // XNor + int Variable(); + BDD Then() const; + BDD Else() const; + BDD Exist(const BDD& cube); + BDD Universal(const BDD& cube); + BDD Restrict(const BDD& other) const; + BDD Compose(int v, const BDD& other) const; + BDD Permute(const vector &permu) const; + BDD AndExist(const BDD& other, const BDD& cube); + bool IsComp() { return (ISCOMP(node) != 0); } + void Support(vector &vars); + + XManager *manager() const; + DD Node() const; +}; + +class XBDDManager{ +private: + XManager *mgr; + +public: + XBDDManager(int varCount){ mgr = new XManager(varCount);} + ~XBDDManager(){ delete mgr; } + void Clear(int varCnt){ mgr->Clear(varCnt); } + + BDD BddOne(){ return BDD(mgr, mgr->One);} + BDD BddZero(){ return BDD(mgr, mgr->Zero);} + BDD BddVar(int varIndex){ return BDD(mgr, varIndex); } + BDD Ite(const BDD &f, const BDD &g, const BDD &h){ return BDD(mgr, mgr->ite(f.node, g.node, h.node)); }; + + void GarbageCollection(){ mgr->GarbageCollection(); }; + void SetMaxCacheSize(int v){ mgr->SetMaxCacheSize(v); }; + int GetUTableCount(){ return mgr->GetUTableCount(); }; + int GetCacheCount(){ return mgr->GetCacheCount(); }; + int NodeCount(){ return mgr->NodeCount(); }; + int DeadCount(){ return mgr->DeadCount(); } + double Get_CTable_HitRate() { return mgr->Get_CTable_HitRate(); } + double Get_UTable_HitRate() { return mgr->Get_UTable_HitRate(); } + XManager *manager() const { return mgr; }; + + int VarDistanceOf(BDD A, BDD B) { return mgr->VarDistanceOf(A.Node(), B.Node());} + int LargestPath(BDD from, vector &path){ return mgr->LargestPath(from.Node(), path); } + void ShowInfo(double vtime = 0){ mgr->ShowInfo(vtime); } + void ShowInfoToFile(const char *filename){ mgr->ShowInfoToFile(filename); }; + void ShowInfoToFile(const char *filename, const string &info){ mgr->ShowInfoToFile(filename, info); }; +}; + +#endif diff --git a/cpp/Base.h b/cpp/Base.h new file mode 100644 --- /dev/null +++ b/cpp/Base.h @@ -0,0 +1,78 @@ +/***************************************************************************** +Copyright (c) 2012 - 2013, The Board of Trustees of the University of Beijing Technology and +the University of Griffith. +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are +met: + +* Redistributions of source code must retain the above + copyright notice, this list of conditions and the + following disclaimer. + +* Redistributions in binary form must reproduce the + above copyright notice, this list of conditions + and the following disclaimer in the documentation + and/or other materials provided with the distribution. + +* Neither the name of the University of Beijing Technology and + the University of Griffith nor the names of its contributors + may be used to endorse or promote products derived from this + software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS +IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, +THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR +PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR +CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. +*****************************************************************************/ + +/***************************************************************************** +written by + Guanfeng Lv, last updated 10/26/2012 +*****************************************************************************/ + +#ifndef __BASE__ +#define __BASE__ + +#define Max(a,b) ((a > b)?a:b) +#define Min(a,b) ((a < b)?a:b) +//------------------------------------- +#define ONE_MILLION 1048576 +//------------------------------------- +#define DD int +#define ADDR(k) (k & 0x7FFFFFFF) +#define ISCOMP(A) (A & 0x80000000) +//------------------------------------- +#define EXIST 0x80000001 +#define RESTRICT 0x80000002 +#define AND 0x80000003 +#define XOR 0x80000004 +#define OP_MAX_VALUE 0x00000010 +//------------------------------------- +#define BDD_ITE 0x02 +#define BDD_AND_ABSTRACT 0x06 +#define BDD_XOR_EXIST_ABSTRACT 0x0a +#define BDD_COMPOSE_RECUR 0x0e +#define BDD_ITE_CONSTANT 0x22 +//------------------------------------- +#define DD_P1 12582917 +#define DD_P2 4256249 +#define DD_P3 741457 +//------------------------------------- +#define CACHE_DYN 0 +#define CACHE_FIX 1 +#define CACHE_OLD 2 +//===================================== + +#define Hash3(o,f,g,s) (((((unsigned)(unsigned long)(f) + (unsigned)(unsigned long)(o)) * DD_P1 + (unsigned)(unsigned long)(g)) * DD_P2) >> (s)) +#define Hash2(f,g,s) ((((unsigned)(unsigned long)(f) * DD_P1 + (unsigned)(unsigned long)(g)) * DD_P2) >> (s)) + +#endif diff --git a/cpp/CTable.cpp b/cpp/CTable.cpp new file mode 100644 --- /dev/null +++ b/cpp/CTable.cpp @@ -0,0 +1,146 @@ +/***************************************************************************** +Copyright (c) 2012 - 2013, The Board of Trustees of the University of Beijing Technology and +the University of Griffith. +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are +met: + +* Redistributions of source code must retain the above + copyright notice, this list of conditions and the + following disclaimer. + +* Redistributions in binary form must reproduce the + above copyright notice, this list of conditions + and the following disclaimer in the documentation + and/or other materials provided with the distribution. + +* Neither the name of the University of Beijing Technology and + the University of Griffith nor the names of its contributors + may be used to endorse or promote products derived from this + software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS +IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, +THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR +PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR +CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. +*****************************************************************************/ + +/***************************************************************************** +written by + Guanfeng Lv, last updated 10/26/2012 +*****************************************************************************/ + +#include "Base.h" +#include "CTable.h" +#include "Manager.h" +#include "Timer.h" +#include +using namespace std; + +XCTable::XCTable(XManager *manager, int vBitCount) +{ + mgr = manager; + count = (1 << vBitCount); + shiftSize = 32 - vBitCount; + + items = new CTableNode[count]; + + toAddCount = 0; + findCount = 0; + foundedCount = 0; + missCount = 0; +} + +XCTable::~XCTable() +{ + delete []items; +} + +void XCTable::Clear() +{ + for(int i=0; iNodeCount(); i++){ + int v = mgr->nodes[i].var; + DD t = mgr->nodes[i].Then; + DD e = mgr->nodes[i].Else; + Insert(v, t, e, i); + + } +} + +void XCTable::Expand(bool isInc) +{ + int newcount = count << 1; + if(!isInc) newcount = count >> 1; + + CTableNode *newitems = new CTableNode[newcount]; + int newshiftSize = shiftSize - 1; + if(!isInc) newshiftSize = shiftSize + 1; + + for(int i=0; i 0){ + Expand(); + } + //------------------------------------------------------- + int pos = Hash3(A, B, C, shiftSize); + items[pos].A = A; + items[pos].B = B; + items[pos].C = C; + items[pos].R = tmp; +} + +void XCTable::size_inc(int incCnt) +{ + if(toAddCount <= 0 && count <= mgr->maxCacheSize / 2 && mgr->GetAvailMem() > (long long)(count * sizeof(CTableNode))){ + toAddCount += incCnt; + } +} diff --git a/cpp/CTable.h b/cpp/CTable.h new file mode 100644 --- /dev/null +++ b/cpp/CTable.h @@ -0,0 +1,88 @@ +/***************************************************************************** +Copyright (c) 2012 - 2013, The Board of Trustees of the University of Beijing Technology and +the University of Griffith. +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are +met: + +* Redistributions of source code must retain the above + copyright notice, this list of conditions and the + following disclaimer. + +* Redistributions in binary form must reproduce the + above copyright notice, this list of conditions + and the following disclaimer in the documentation + and/or other materials provided with the distribution. + +* Neither the name of the University of Beijing Technology and + the University of Griffith nor the names of its contributors + may be used to endorse or promote products derived from this + software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS +IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, +THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR +PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR +CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. +*****************************************************************************/ + +/***************************************************************************** +written by + Guanfeng Lv, last updated 10/26/2012 +*****************************************************************************/ + +#ifndef _CTABLE_ +#define _CTABLE_ + +#include "DdNode.h" + +class XManager; + +class CTableNode{ +public: + DD A; + DD B; + DD C; + DD R; + CTableNode():A(0),B(0),C(0),R(0){}; + void SetValue(int a, int b, int c, int r){ A=a; B=b; C=c; R=r; }; +}; + +class XCTable{ +private: + friend class XManager; + XManager *mgr; + int count; + int shiftSize; + + CTableNode *items; + int toAddCount; + + long long findCount; + long long foundedCount; + long long missCount; //for cudd reward cache resize + void Refresh(); + +public: + XCTable(XManager *manager, int vBitCount); + ~XCTable(); + void Clear(); + + void Insert(DD A, DD B, DD C, DD tmp); + bool Find(DD A, DD B, DD C, DD &r); + + void size_inc(int addCount); + void Expand(bool isInc = true); + int Count(){ return count; } + double HitRate(){ return 1.0 * foundedCount / (findCount + 1); } +}; + +#endif diff --git a/cpp/DdNode.cpp b/cpp/DdNode.cpp new file mode 100644 --- /dev/null +++ b/cpp/DdNode.cpp @@ -0,0 +1,82 @@ +/***************************************************************************** +Copyright (c) 2012 - 2013, The Board of Trustees of the University of Beijing Technology and +the University of Griffith. +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are +met: + +* Redistributions of source code must retain the above + copyright notice, this list of conditions and the + following disclaimer. + +* Redistributions in binary form must reproduce the + above copyright notice, this list of conditions + and the following disclaimer in the documentation + and/or other materials provided with the distribution. + +* Neither the name of the University of Beijing Technology and + the University of Griffith nor the names of its contributors + may be used to endorse or promote products derived from this + software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS +IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, +THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR +PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR +CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. +*****************************************************************************/ + +/***************************************************************************** +written by + Guanfeng Lv, last updated 10/26/2012 +*****************************************************************************/ + +#include "DdNode.h" + +DdNodes::DdNodes() +{ + slots = NULL; +} + +DdNodes::~DdNodes() +{ + Clear(); +} + +void DdNodes::Init(int vSlotSize) +{ + typedef DdNode* PDdNode; + slots = new PDdNode[10000]; + for(int i=0; i<10000; i++){ + slots[i] = 0; + } + + slotSize = vSlotSize; + slots[0] = new DdNode[slotSize]; + for(int k=0; k +#include +#include + +using namespace std; + +class DdNode{ +public: + int var; + int Then; + int Else; + int Next; + DdNode():var(0),Then(0),Else(0),Next(0){}; + DdNode(DdNode &v) + { + var = v.var; + Then = v.Then; + Else = v.Else; + Next = v.Next; + } + DdNode& operator = (const DdNode& v) + { + var = v.var; + Then = v.Then; + Else = v.Else; + Next = v.Next; + return *this; + } + + void SetValue(int a, int b, int c, int d){ var = a; Then = b; Else = c; Next = d; }; +}; + +class DdNodes{ +private: + friend class XManager; + int slotCount; + int slotSize; + int nodeCount; + DdNode **slots; +public: + DdNodes(); + ~DdNodes(); + + int GetFreeNode(); + void Init(int vSlotSize); + void Clear(); + int NodeCount(){ return nodeCount;}; + + DdNode& operator [] (int index); +}; + +inline DdNode& DdNodes::operator [] (int index) +{ + int s = index / slotSize; + int i = index % slotSize; + return slots[s][i]; +} + +inline int DdNodes::GetFreeNode() +{ + if(nodeCount == slotCount * slotSize){ + slots[slotCount] = new DdNode[slotSize]; + + for(int k=0; k +#include +#include +#include +#include +#include +#include +using namespace std; + +XManager::XManager(int variableCount) +{ + varCount = variableCount; + maxCacheSize = 2147483647; + nodes.Init(1 * ONE_MILLION); + + UTable = new XUTable(this, 18); + CTable = new XCTable(this, 18); + + One = 0; + Zero = Not(One); + nodes[0].var = INT_MAX; + + + for(int i=1; i <= varCount; i++){ + UTable->Find_or_Add_Unique_Table(i, One, Zero); + } + + oldCHit = 0.0; + oldCallCount = 2000000; + curCallCount = 0; + adjustCTableType = CACHE_DYN; +} + +XManager::~XManager() +{ + delete UTable; + delete CTable; +} + +void XManager::Clear(int varCnt) +{ + varCount = varCnt; + nodes.Clear(); + nodes.Init(1 * ONE_MILLION); + UTable->Clear(); + CTable->Clear(); + nodes[0].var = INT_MAX; + for(int i=1; i <= varCount; i++){ + UTable->Find_or_Add_Unique_Table(i, One, Zero); + } +} + +DD XManager::AndRecur(DD f, DD g) +{ + AdjustCTable(); + DD F = ADDR(f); + DD G = ADDR(g); + + if(F == G){ + if(f == g) return (f); + else return Zero; + } + if(F == One){ + if( f == One) return g; + else return f; + } + if(G == One){ + if(g ==One) return f; + else return g; + } + + if(F > G){ + DD tmp = f; + f = g; + g = tmp; + F = ADDR(f); + G = ADDR(g); + } + + DD r; + bool b = CTable->Find(AND, f, g, r); + if(b){ return r;} + + int topf = nodes[F].var; + int topg = nodes[G].var; + int index; + DD fv, fnv, gv, gnv; + + if(topf <= topg){ + index = topf; + fv = nodes[F].Then; + fnv = nodes[F].Else; + + if(ISCOMP(f)){ + fv = Not(fv); + fnv = Not(fnv); + } + } + else{ + index = topg; + fv = fnv = f; + } + + if(topg <= topf){ + gv = nodes[G].Then; + gnv = nodes[G].Else; + if(ISCOMP(g)){ + gv = Not(gv); + gnv= Not(gnv); + } + } + else{ + gv = gnv = g; + } + + DD t = AndRecur(fv, gv); + DD e = AndRecur(fnv, gnv); + + if(t == e){ + r = t; + } + else{ + if(ISCOMP(t)){ + r = UTable->Find_or_Add_Unique_Table(index, Not(t), Not(e)); + r = Not(r); + } + else{ + r = UTable->Find_or_Add_Unique_Table(index, t, e); + } + } + + CTable->Insert(AND,f, g, r); + return r; +} + +DD XManager::XorRecur(DD f, DD g) +{ + AdjustCTable(); + if(f == g) return Zero; + if(f == Not(g)) return One; + if(ADDR(f) > ADDR(g)){ + DD tmp = f; + f = g; + g = tmp; + } + if(g == Zero) return f; + if(g == One) return Not(f); + if(ISCOMP(f)){ + f = Not(f); + g = Not(g); + } + + if(f == One) return Not(g); + + + DD r; + bool b = CTable->Find(XOR,f,g,r); + if(b) { return r; } + + int topf = nodes[ADDR(f)].var; + int topg = nodes[ADDR(g)].var; + int index; + DD fv, fnv, gv, gnv; + if(topf <= topg){ + index = topf; + fv = nodes[ADDR(f)].Then; + fnv= nodes[ADDR(f)].Else; + } + else{ + index = topg; + fv = fnv = f; + } + + if(topg <= topf){ + gv = nodes[ADDR(g)].Then; + gnv= nodes[ADDR(g)].Else; + if(ISCOMP(g)){ + gv = Not(gv); + gnv= Not(gnv); + } + } + else{ + gv = gnv = g; + } + + DD t = XorRecur(fv, gv); + DD e = XorRecur(fnv, gnv); + if(t == e) { r = t; } + else{ + if(ISCOMP(t)){ + r = UTable->Find_or_Add_Unique_Table(index, Not(t), Not(e)); + r = Not(r); + } + else{ + r = UTable->Find_or_Add_Unique_Table(index, t, e); + } + } + CTable->Insert(XOR,f,g,r); + return r; +} + +DD XManager::IteRecur(DD f, DD g, DD h) +{ + if(f == One) return g; + if(f == Zero) return h; + + + DD r; + if(g == One || f == g){ + if(h == Zero){ + return f; + } + else{ + r = AndRecur(Not(f), Not(h)); + return Not(r); + } + } + else if(g == Zero || f == Not(g)){ + if( h == One){ + return Not(f); + } + else{ + r = AndRecur(Not(f), h); + return r; + } + } + + + if(g == h){ + return g; + } + else if(g == Not(h)){ + r = XorRecur(f, h); + return r; + } + + AdjustCTable(); + + if (ISCOMP(f)) { + f = Not(f); + r = g; + g = h; + h = r; + } + int comple = 0; + if (ISCOMP(g)) { + g = Not(g); + h = Not(h); + comple = 1; + } + + int topf = nodes[ADDR(f)].var; + int topg = nodes[ADDR(g)].var; + int toph = nodes[ADDR(h)].var; + int v = Top_Variable(g,h); + + if(topf < v && nodes[ADDR(f)].Then == One && nodes[ADDR(f)].Else == Zero){ + r = UTable->Find_or_Add_Unique_Table(topf, g, h); + return (comple)?Not(r):r; + } + + bool b = CTable->Find(f,g,h,r); + if(b){ return (comple)?Not(r):r; } + + + int index; + DD fv, fnv, gv, gnv, hv, hnv; + if(topf <= v){ + v = Min(topf, v); + index = topf; + fv = nodes[ADDR(f)].Then; + fnv= nodes[ADDR(f)].Else; + } + else{ fv = fnv = f;} + + if(topg == v){ + index = topg; + gv = nodes[ADDR(g)].Then; + gnv= nodes[ADDR(g)].Else; + } + else{ gv = gnv = g;} + + if(toph == v){ + index = toph; + hv = nodes[ADDR(h)].Then; + hnv= nodes[ADDR(h)].Else; + if(ISCOMP(h)){ + hv = Not(hv); + hnv= Not(hnv); + } + } + else { hv = hnv = h; } + + DD t = IteRecur(fv, gv, hv); + DD e = IteRecur(fnv, gnv, hnv); + r = UTable->Find_or_Add_Unique_Table(index,t,e); + r = (t == e)?t:r; + CTable->Insert(f,g,h,r); + return (comple)?Not(r):r; +} + +DD XManager::ite(DD F, DD G, DD H) +{ + return IteRecur(F, G, H); +} + +DD XManager::And(const XVector
dds) +{ + if(dds.size() < 2) return Zero; + + DD r = And(dds[0], dds[1]); + for(int i=2; i dds) +{ + if(dds.size() < 2) return Zero; + + DD r = Or(dds[0], dds[1]); + for(int i=2; iget_value(ADDR(A)); + if(r != 0){ return (isComple)?Not(r):r; } + + DdNode *node = &nodes[ADDR(A)]; + DD T = PermuteRecur(node->Then, permu, visited); + DD E = PermuteRecur(node->Else, permu, visited); + + r = ite(permu[node->var], T, E); + + visited->set_value(ADDR(A), r); + r = (isComple)?Not(r):r; + return r; +} + +DD XManager::Permute(DD A, int *permu) +{ + XInts *visited = new XInts; + visited->set_size(NodeCount()); + DD r = PermuteRecur(A, permu, visited); + delete visited; + return r; +} + +DD XManager::ExistRecur(DD f, DD cube) +{ + if(ADDR(f) == 0 || cube == One){ + return f; + } + DdNode *fnode = &nodes[ADDR(f)]; + DdNode *cnode = &nodes[ADDR(cube)]; + + while (fnode->var > cnode->var) { + cube = cnode->Then; + cnode = &nodes[ADDR(cube)]; + if (cube == One) return(f); + } + + DD r; + bool b = CTable->Find(EXIST, f, cube, r); + if(b){ + return r; + } + + DD T = fnode->Then; + DD E = fnode->Else; + if (ISCOMP(f)){ + T = Not(T); + E = Not(E); + } + + if (fnode->var == cnode->var) { + if (T == One || E == One || T == Not(E)) { + return(One); + } + DD res1 = ExistRecur(T, cnode->Then); + if (res1 == One) { + CTable->Insert(EXIST, f, cube, One); + return(One); + } + DD res2 = ExistRecur(E, cnode->Then); + DD res = Or(res1, res2); + CTable->Insert(EXIST, f, cube, res); + return(res); + } + else { + DD res1 = ExistRecur(T, cube); + DD res2 = ExistRecur(E, cube); + DD res = ite(fnode->var, res1, res2); + CTable->Insert(EXIST, f, cube, res); + return(res); + } +} + +DD XManager::Exist(DD A, DD cube) +{ + return ExistRecur(A, cube); +} + +DD XManager::Universal(DD A, DD cube) +{ + DD X = Not(A); + return Not(Exist(X, cube)); +} + +DD XManager::AndExist(DD f, DD g, DD cube) +{ + AdjustCTable(); + + if(f == Zero || g == Zero || f == Not(g)) return Zero; + if(f == One && g == One) return One; + + if(cube == One) return (AndRecur(f, g)); + if(f == One || f == g) return (Exist(g, cube)); + if(g == One) return (Exist(f, cube)); + + + if(ADDR(f) > ADDR(g)){ + DD tmp = f; + f = g; + g = tmp; + } + + DD F = ADDR(f); + DD G = ADDR(g); + int topf = nodes[ADDR(f)].var; + int topg = nodes[ADDR(g)].var; + int top = Min(topf, topg); + int topcube = nodes[ADDR(cube)].var; + while(topcube < top){ + cube = nodes[ADDR(cube)].Then; + if(cube == One) return AndRecur(f, g); + topcube = nodes[ADDR(cube)].var; + } + + if(ISCOMP(cube) == 0){ + cube = Not(cube); + } + + DD r; + if(ISCOMP(f)){ + if(F < OP_MAX_VALUE){ + r = AndRecur(f, g); + r = Exist(r, cube); + return r; + } + } + + + bool b = CTable->Find(f, cube, g, r); + if(b){ + return r; + } + + DD ft, fe, gt, ge; + int index; + if(topf == top){ + index = nodes[F].var; + ft = nodes[F].Then; + fe = nodes[F].Else; + if(ISCOMP(f)){ + ft = Not(ft); + fe = Not(fe); + } + } + else{ + index = nodes[G].var; + ft = fe = f; + } + + if(topg == top){ + gt = nodes[G].Then; + ge = nodes[G].Else; + if(ISCOMP(g)){ + gt = Not(gt); + ge = Not(ge); + } + } + else{ + gt = ge = g; + } + + DD t, e; + if(topcube == top){ + DD ct = nodes[ADDR(cube)].Then; + t = AndExist(ft, gt, ct); + if(t == One || t == fe || t == ge){ + CTable->Insert(f, cube, g, t); + return t; + } + if(t == Not(fe)){ + e = Exist(ge, ct); + } + else if(t == Not(ge)){ + e = Exist(fe, ct); + } + else{ + e = AndExist(fe, ge, ct); + } + if(t == e){ + r = t; + } + else{ + r = AndRecur(Not(t), Not(e)); + r = Not(r); + } + } + else{ + t = AndExist(ft, gt, cube); + e = AndExist(fe, ge, cube); + if(t == e){ + r = t; + } + else{ + if(ISCOMP(t)){ + r = UTable->Find_or_Add_Unique_Table(index, Not(t), Not(e)); + r = Not(r); + } + else{ + r = UTable->Find_or_Add_Unique_Table(index, t, e); + } + } + } + CTable->Insert(f, cube, g, r); + return r; +} + +void XManager::Support(DD dd, vector &vars) +{ + int *index = new int[varCount+1]; + for(int i=0; i one; + XVector
two; + one.push_back(dd); + XVector
*cur = &one; + XVector
*nex = &two; + while(cur->size() > 0){ + for(int i=0; isize(); i++){ + int address = ADDR((*cur)[i]); + if(address != 0 && bits.get_value(address) == 0){ + bits.set_value(address, 1); + DdNode &node = nodes[address]; + index[node.var] = 1; + nex->push_back(node.Then); + nex->push_back(node.Else); + } + } + XVector
*tmp = cur; + cur = nex; + nex = tmp; + nex->clear(); + } + //---------------------------------- + for(int i=1; iFind(RESTRICT, F, C, r); + if(b){ + return r; + } + + int topf = nodes[ADDR(F)].var; + int topc = nodes[ADDR(C)].var; + if(topc < topf){ + DD H = nodes[ADDR(C)].Then; + DD L = nodes[ADDR(C)].Else; + if(ISCOMP(C)){ + H = Not(H); + L = Not(L); + } + DD r = Restrict(F, Or(H, L)); + CTable->Insert(RESTRICT, F, C, r); + return r; + } + else if(topf < topc){ + DD f1 = nodes[ADDR(F)].Then; + DD f0 = nodes[ADDR(F)].Else; + if(ISCOMP(F)){ + f1 = Not(f1); + f0 = Not(f0); + } + DD a1 = Restrict(f1, C); + DD a0 = Restrict(f0, C); + DD r = ite(topf, a1, a0); + CTable->Insert(RESTRICT, F, C, r); + return r; + } + else{ + DD f1 = nodes[ADDR(F)].Then; + DD f0 = nodes[ADDR(F)].Else; + if(ISCOMP(F)){ + f1 = Not(f1); + f0 = Not(f0); + } + DD H = nodes[ADDR(C)].Then; + DD L = nodes[ADDR(C)].Else; + if(ISCOMP(C)){ + H = Not(H); + L = Not(L); + } + DD r; + if(L == Zero){ + r = Restrict(f1, H); + } + else if(H == Zero){ + r = Restrict(f0, L); + } + else { + r = ite(topf, Restrict(f1, H), Restrict(f0, L)); + } + CTable->Insert(RESTRICT, F, C, r); + return r; + } +} + +DD XManager::Compose(DD f, int v, DD g) +{ + int topf = nodes[ADDR(f)].var; + if(topf > v){ + return f; + } + + bool comple = true; + DD F = f; + if(!ISCOMP(f)){ + comple = false; + F = Not(f); + } + DD r; + bool b = CTable->Find(v, F, g, r); + if(b){ + return (comple?r:Not(r)); + } + + DD f1, f0, g1, g0; + if(topf == v){ + f1 = Not(nodes[ADDR(F)].Then); + f0 = Not(nodes[ADDR(F)].Else); + r = ite(g, f1, f0); + } + else{ + int topg = nodes[ADDR(g)].var; + int top; + if(topf > topg){ + top = topg; + f1 = f0 = F; + } + else{ + top = topf; + f1 = Not(nodes[ADDR(F)].Then); + f0 = Not(nodes[ADDR(F)].Else); + } + + if(topg > topf){ + g1 = g0 = g; + } + else{ + g1 = nodes[ADDR(g)].Then; + g0 = nodes[ADDR(g)].Else; + if(ISCOMP(g)){ + g1 = Not(g1); + g0 = Not(g0); + } + } + DD t = Compose(f1, v, g1); + DD e = Compose(f0, v, g0); + r = ite(top, t, e); + } + CTable->Insert(v, F, g, r); + return (comple?r:Not(r)); +} + +//======================================================= + +int XManager::LargestPath(DD from, vector &path) +{ + double startTime = Timer::GetTime(); + + class XPathNode{ + public: + int priorId; + int length; + XPathNode():priorId(0),length(0){}; + }; + + path.clear(); + if(ADDR(from) >=NodeCount() || ADDR(from) <= 0){ + return 0; + } + XPathNode *ps = new XPathNode[NodeCount()]; + char *inIds = new char[NodeCount()]; + + XVector levelOne; + XVector levelTwo; + XVector *curLevel = &levelOne; + XVector *nextLevel= &levelTwo; + curLevel->push_back(from); + + for(int ki=nodes[ADDR(from)].var; ki<=varCount; ki++){ + if(curLevel->size() == 0) break; + memset(inIds, 0, NodeCount()); + for(int i=0; isize(); i++){ + if(!IsConstant((*curLevel)[i])){ + int cId = ADDR((*curLevel)[i]); + DdNode *curNode = &nodes[cId]; + DD T = curNode->Then; + DD E = curNode->Else; + if(ISCOMP((*curLevel)[i])){ + T = Not(T); + E = Not(E); + } + if(!IsConstant(T) && inIds[ADDR(T)] == 0){ + nextLevel->push_back(T); + inIds[ADDR(T)] = 1; + } + if(!IsConstant(E) && T != E && inIds[ADDR(E)] == 0){ + nextLevel->push_back(E); + inIds[ADDR(E)] = 1; + } + + if(T != Zero){ + int varBetween = this->VarDistanceOf(cId, T)-1; + if(ps[ADDR(T)].length < ps[cId].length + varBetween + 1){ + ps[ADDR(T)].priorId = (*curLevel)[i]; //cId; + ps[ADDR(T)].length = ps[cId].length + varBetween + 1; + } + } + if(E != Zero){ + int varBetween = this->VarDistanceOf(cId, E)-1; + if(ps[ADDR(E)].length < ps[cId].length + varBetween){ + ps[ADDR(E)].priorId = (*curLevel)[i]; //cId; + ps[ADDR(E)].length = ps[cId].length + varBetween; + } + } + } + } + + if(curLevel == &levelOne){ + levelOne.clear(); + curLevel = &levelTwo; + nextLevel= &levelOne; + } + else if(curLevel == &levelTwo){ + levelTwo.clear(); + curLevel = &levelOne; + nextLevel= &levelTwo; + } + } + + int i = 0; + while(ps[i].priorId != 0){ + int pId = ADDR(ps[i].priorId); + if(ADDR(nodes[pId].Then) == i){ + int fvar = nodes[pId].var; + int tvar = (i==0)?(varCount+1):nodes[i].var; + if(i == 0 && ISCOMP(ps[i].priorId)){ + fvar++; + } + for(int k=fvar; k::iterator it = externalBDDs.begin(); + for(; it != externalBDDs.end(); it++){ + BDD *b = (BDD *)*it; + c[ADDR(b->node)] = 1; + } + for(int i=NodeCount()-1; i>=1; i--){ + if(c[i]){ + DdNode *n = &nodes[i]; + c[ADDR(n->Then)] = 1; + c[ADDR(n->Else)] = 1; + } + } + + int zeroCnt = 0; + for(int i = varCount+1; i exDDs; + + set::iterator it = externalBDDs.begin(); + for(; it != externalBDDs.end(); it++){ + BDD *b = (BDD *)*it; + c[ADDR(b->node)] = 1; + exDDs.push_back(ADDR(b->node)); + } + + for(int i=NodeCount()-1; i>=1; i--){ + if(c[i]){ + DdNode *n = &nodes[i]; + c[ADDR(n->Then)] = 1; + c[ADDR(n->Else)] = 1; + } + } + + DD *ds = new DD[NodeCount()]; + for(int i=0; iIsComp()){ + b->node = Not(ds[ADDR(b->node)]); + } + else b->node = ds[b->node]; + } + + nodes.nodeCount = newcount; + + UTable->Refresh(); + CTable->Refresh(); + + delete []ds; + delete []c; +} + +int XManager::GetVariableCount() +{ + return varCount; +} + +int XManager::GetNodeCount() +{ + return NodeCount(); +} + +void XManager::PrintNode(DdNode *node) +{ + cout<var<<", Then:"<Then<<",Else:"<Else)<<",Next:"<Next<HitRate()<<", Time:"< +#include +#include +//#include +using namespace std; +//=================================================== +class XManager{ +private: + friend class XCTable; + friend class XUTable; + int varCount; + int maxCacheSize; + DdNodes nodes; + + double oldCHit; + long long oldCallCount; + long long curCallCount; + + + XUTable *UTable; + XCTable *CTable; + + int GetFreeNode(){ return nodes.GetFreeNode(); }; + DD PermuteRecur(DD A, int *permu, XInts *visited); + DD ExistRecur(DD f, DD cube); + DD AndRecur(DD f, DD g); + DD XorRecur(DD f, DD g); + DD IteRecur(DD f, DD g, DD h); + + int adjustCTableType; + void AdjustCTable(); + unsigned long GetAvailMem(); + +public: + set externalBDDs; + +public: + DD One; + DD Zero; + DD ite(DD F, DD G, DD H); + inline int Variable(DD A); + inline int Top_Variable(DD A, DD B); + inline int Top_Variable(DD A, DD B, DD C); + inline DD Then(DD A, int v); + inline DD Else(DD A, int v); + inline DD Not(DD A) { return A ^ 0x80000000; } + inline DD Or(DD A, DD B) { return Not(And(Not(A), Not(B)));} + inline DD Nor(DD A, DD B){ return And(Not(A), Not(B));} + inline DD And(DD A, DD B){ return AndRecur(A, B);} + inline DD Nand(DD A, DD B){ return Not(AndRecur(A, B));} + inline DD Xor(DD A, DD B) { return XorRecur(A, B);} + inline DD Xnor(DD A, DD B){ return XorRecur(A, Not(B));} + inline DD LessThan(DD A, DD B){ return ite(A,Zero,B); } + inline DD MoreThan(DD A, DD B){ return ite(A,Not(B),Zero); } + inline DD LessEqual(DD A, DD B){ return ite(A,B,One); } + inline DD MoreEqual(DD A, DD B){ return ite(A,One,Not(B)); }; + inline DD IsConstant(DD A) { return (ADDR(A)==0);}; + DD And(const XVector
dds); + DD Or(const XVector
dds); + DD Exist(DD A, DD cube); + DD Universal(DD A, DD cube); + DD Restrict(DD F, DD C); + DD Compose(DD f, int v, DD g); + DD Permute(DD A, int *permu); + DD AndExist(DD f, DD g, DD cube); + void Support(DD node, vector &vars); + + int VarDistanceOf(DD A, DD B); + int LargestPath(DD from, vector &path); + int NodeCount() {return nodes.NodeCount(); }; + int DeadCount(); + void GarbageCollection(); + +public: + XManager(int variableCount); + ~XManager(); + void Clear(int varCnt); + void ShowInfo(double vtime); + void ShowInfoToFile(const char *filename); + void ShowInfoToFile(const char *filename, const string &info); + void SetMaxCacheSize(int v){ maxCacheSize = v; }; + int GetVariableCount(); + int GetNodeCount(); + int GetUTableCount() { return UTable->count; }; + int GetCacheCount() { return CTable->Count(); }; + double Get_CTable_HitRate(){ return CTable->HitRate();}; + double Get_UTable_HitRate(){ return UTable->HitRate();}; + void PrintNode(DdNode *node); +}; +//====================================================== +inline int XManager::Variable(DD A) +{ + DdNode *n = &nodes[ADDR(A)]; + return n->var; +} + +inline int XManager::Top_Variable(DD A, DD B) +{ + DdNode *NA = &nodes[ADDR(A)]; + DdNode *NB = &nodes[ADDR(B)]; + return ((NA->var <= NB->var)?NA->var:NB->var); +} + +inline int XManager::Top_Variable(DD A, DD B, DD C) +{ + DdNode *NA = &nodes[ADDR(A)]; + DdNode *NB = &nodes[ADDR(B)]; + DdNode *NC = &nodes[ADDR(C)]; + + if (NA->var <= NB->var){ + if (NA->var <= NC->var) return NA->var; + return NC->var; + } + else{ + if (NB->var <= NC->var) return NB->var; + return NC->var; + } +}; + +inline DD XManager::Then(DD A, int v) +{ + DdNode *n = &nodes[ADDR(A)]; + if (n->var == v) { + if (ISCOMP(A)) return Not(n->Then); + else return n->Then; + } + return A; +}; + +inline DD XManager::Else(DD A, int v) +{ + DdNode *n = &nodes[ADDR(A)]; + if (n->var == v) { + if (ISCOMP(A)) return Not(n->Else); + else return n->Else; + } + return A; +}; + +inline void XManager::AdjustCTable() +{ + curCallCount++; + if(curCallCount >= oldCallCount){ + double curCHit = CTable->HitRate(); + if(curCHit >= oldCHit || CTable->count < NodeCount() * CTable->HitRate()){ + int addCount = 1; + CTable->size_inc(addCount); + } + oldCHit = curCHit; + oldCallCount = (curCallCount<<1); + if(GetAvailMem() < (ONE_MILLION << 8) ) GarbageCollection(); + if(GetAvailMem() < (ONE_MILLION << 8) ) CTable->Expand(false); + } +}; + +inline unsigned long XManager::GetAvailMem() +{ + return 1000000000; + //struct sysinfo info; + //sysinfo(&info); + //return info.freeram; +} + +inline int XManager::VarDistanceOf(DD A, DD B) +{ + int av = nodes[ADDR(A)].var; + int bv = nodes[ADDR(B)].var; + if(av == INT_MAX){ + if(bv == INT_MAX) return 0; + else return (varCount - bv + 1); + } + else{ + if(bv == INT_MAX){ + return (varCount - av + 1); + } + else{ + int t = av - bv; + return ((t > 0)?t:(-t)); + } + } +}; + +#endif diff --git a/cpp/OriginalMakefile b/cpp/OriginalMakefile new file mode 100644 --- /dev/null +++ b/cpp/OriginalMakefile @@ -0,0 +1,60 @@ +.SUFFIXES: .o .cc .u + +WHERE = . +CPP = g++ +CFLAGS = -g -O3 -Wno-deprecated -shared -fPIC + +CBINFLAGS = -g -O3 -Wno-deprecated + +INCLUDE = $(WHERE)/include + +#################################################### +File1 = ./main +File2 = ./UTable +File3 = ./Manager +File4 = ./CTable +File5 = ./BDDNode +File6 = ./DdNode + +SRC1 = $(File1).cpp +SRC2 = $(File2).cpp +SRC3 = $(File3).cpp +SRC4 = $(File4).cpp +SRC5 = $(File5).cpp +SRC6 = $(File6).cpp + +OBJ1 = $(File1).o +OBJ2 = $(File2).o +OBJ3 = $(File3).o +OBJ4 = $(File4).o +OBJ5 = $(File5).o +OBJ6 = $(File6).o + +OBJS = $(OBJ1) $(OBJ2) $(OBJ3) $(OBJ4) $(OBJ5) $(OBJ6) + +TARGET = t +#------------------------------------------------------ +$(TARGET): $(OBJS) + $(CPP) $(CBINFLAGS) -o $(TARGET) $(OBJS) $(LIBS) -lm + +$(OBJ1): $(SRC1) + $(CPP) -c $(SRC1) -I$(INCLUDE) $(CFLAGS) +$(OBJ2): $(SRC2) + $(CPP) -c $(SRC2) -I$(INCLUDE) $(CFLAGS) +$(OBJ3): $(SRC3) + $(CPP) -c $(SRC3) -I$(INCLUDE) $(CFLAGS) +$(OBJ4): $(SRC4) + $(CPP) -c $(SRC4) -I$(INCLUDE) $(CFLAGS) +$(OBJ5): $(SRC5) + $(CPP) -c $(SRC5) -I$(INCLUDE) $(CFLAGS) +$(OBJ6): $(SRC6) + $(CPP) -c $(SRC6) -I$(INCLUDE) $(CFLAGS) + +#------------------------------------------------------ +cl: #clean + rm -f *.o *.u mon.out gmon.out *.pixie *.Addrs *.Counts mnem.* \ + .pure core *.warnings *.cpp~ *.h~ Makefile~ + +cla: #clean all + rm -f $(TARGET) *.o *.cpp~ *.h~ Makefile~ +#------------------------------------------------------ diff --git a/cpp/README b/cpp/README new file mode 100644 --- /dev/null +++ b/cpp/README @@ -0,0 +1,23 @@ + +The CacBDD package is a package written in ANSI C++ for the manipulation of +ordered binary decision diagrams. + +It is easy to use it by typing: make. + +The file "main.cpp" gives a toy demo for how to use this package. + +CacBDD has been successfully built on the following configurations: + + PC runing Ubuntu (64bit) with gcc + PC runing Windows 7(64bit) with Visual C++ 2010 + + +Send feedback to: + +Guanfeng Lv +University of Beijing Technology, School of Comp.Sci and Tech. +lgfcube@gmail.com + +Kaile Su +Griffith University, IIIS. +kailepku@gmail.com diff --git a/cpp/Timer.h b/cpp/Timer.h new file mode 100644 --- /dev/null +++ b/cpp/Timer.h @@ -0,0 +1,73 @@ +/***************************************************************************** +Copyright (c) 2012 - 2013, The Board of Trustees of the University of Beijing Technology and +the University of Griffith. +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are +met: + +* Redistributions of source code must retain the above + copyright notice, this list of conditions and the + following disclaimer. + +* Redistributions in binary form must reproduce the + above copyright notice, this list of conditions + and the following disclaimer in the documentation + and/or other materials provided with the distribution. + +* Neither the name of the University of Beijing Technology and + the University of Griffith nor the names of its contributors + may be used to endorse or promote products derived from this + software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS +IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, +THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR +PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR +CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. +*****************************************************************************/ + +/***************************************************************************** +written by + Guanfeng Lv, last updated 10/26/2012 +*****************************************************************************/ + +#ifndef __TIMER__ +#define __TIMER__ + +#define WIN + +#ifdef WIN + #include +#else + #include + #include "sys/resource.h" +#endif + +class Timer{ +public: + static double GetTime(void) + { +#ifndef WIN + struct rusage ru; + getrusage(RUSAGE_SELF, &ru); + return ( ru.ru_utime.tv_sec*1000 + + ru.ru_utime.tv_usec/1000+ + ru.ru_stime.tv_sec*1000 + + ru.ru_stime.tv_usec/1000 ) / 1000.0; +#else + clock_t c = clock(); + double r = (double)(c) / CLOCKS_PER_SEC; + return r; +#endif + }; +}; + +#endif diff --git a/cpp/UTable.cpp b/cpp/UTable.cpp new file mode 100644 --- /dev/null +++ b/cpp/UTable.cpp @@ -0,0 +1,166 @@ +/***************************************************************************** +Copyright (c) 2012 - 2013, The Board of Trustees of the University of Beijing Technology and +the University of Griffith. +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are +met: + +* Redistributions of source code must retain the above + copyright notice, this list of conditions and the + following disclaimer. + +* Redistributions in binary form must reproduce the + above copyright notice, this list of conditions + and the following disclaimer in the documentation + and/or other materials provided with the distribution. + +* Neither the name of the University of Beijing Technology and + the University of Griffith nor the names of its contributors + may be used to endorse or promote products derived from this + software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS +IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, +THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR +PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR +CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. +*****************************************************************************/ + +/***************************************************************************** +written by + Guanfeng Lv, last updated 10/26/2012 +*****************************************************************************/ + +#include "UTable.h" +#include "Manager.h" +#include +#include +using namespace std; + +XUTable::XUTable(XManager *manager, int vBitCount) +{ + mgr = manager; + count = (1 << vBitCount); + shiftSize = 32 - vBitCount; + + items = new DD[count]; + memset(items, 0, sizeof(DD) * count); + + findCount = 0; + foundedCount = 0; +} + +XUTable::~XUTable() +{ + delete []items; +} + +void XUTable::Clear() +{ + memset(items, 0, sizeof(DD) * count); + findCount = 0; + foundedCount = 0; +} + +void XUTable::Refresh() +{ + memset(items, 0, sizeof(DD) * count); + + for(int i=1; iNodeCount(); i++){ + int v = mgr->nodes[i].var; + DD t = mgr->nodes[i].Then; + DD e = mgr->nodes[i].Else; + int pos = Hash3(v, t, e, shiftSize); + mgr->nodes[i].var = v; + mgr->nodes[i].Then = t; + mgr->nodes[i].Else = e; + mgr->nodes[i].Next = items[pos]; + items[pos] = i; + } + + findCount = 0; + foundedCount = 0; +} + +void XUTable::Expand() +{ + count = count << 1; + + delete []items; + items = new DD[count]; + memset(items, 0, sizeof(DD) * count); + + shiftSize = shiftSize - 1; + for(int i=1; iNodeCount(); i++){ + int v = mgr->nodes[i].var; + DD t = mgr->nodes[i].Then; + DD e = mgr->nodes[i].Else; + int pos = Hash3(v, t, e, shiftSize); + mgr->nodes[i].var = v; + mgr->nodes[i].Then = t; + mgr->nodes[i].Else = e; + mgr->nodes[i].Next = items[pos]; + items[pos] = i; + } + + if(mgr->adjustCTableType == CACHE_FIX || mgr->adjustCTableType == CACHE_OLD){ + mgr->CTable->size_inc(1); + } +} + +DD XUTable::Find_or_Add_Unique_Table(int v, DD A, DD B) +{ + if((mgr->NodeCount()>>2) > count){ Expand(); } + + findCount++; + bool IsNot = false; + + if (ISCOMP(A)){ + A = mgr->Not(A); + B = mgr->Not(B); + IsNot = true; + } + + int pos = Hash3(v, A, B, shiftSize); + + DD cur = items[pos]; + while(cur !=0 ){ + if(cur > ADDR(A) && cur > ADDR(B)){ + if( mgr->nodes[cur].var == v && mgr->nodes[cur].Then == A && mgr->nodes[cur].Else == B){ + foundedCount++; + if(IsNot) return mgr->Not(cur); + else return cur; + } + cur = mgr->nodes[cur].Next; + } + else{ + break; + } + } + int n = mgr->GetFreeNode(); + + mgr->nodes[n].var = v; + mgr->nodes[n].Then = A; + mgr->nodes[n].Else = B; + mgr->nodes[n].Next = items[pos]; + items[pos] = n; + if(IsNot) return mgr->Not(n); + return n; +} + +double XUTable::LinkLength() +{ + int c = 0; + for(int i=0; i 0) c++; + } + return (1.0 * mgr->NodeCount() / c); +} diff --git a/cpp/UTable.h b/cpp/UTable.h new file mode 100644 --- /dev/null +++ b/cpp/UTable.h @@ -0,0 +1,71 @@ +/***************************************************************************** +Copyright (c) 2012 - 2013, The Board of Trustees of the University of Beijing Technology and +the University of Griffith. +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are +met: + +* Redistributions of source code must retain the above + copyright notice, this list of conditions and the + following disclaimer. + +* Redistributions in binary form must reproduce the + above copyright notice, this list of conditions + and the following disclaimer in the documentation + and/or other materials provided with the distribution. + +* Neither the name of the University of Beijing Technology and + the University of Griffith nor the names of its contributors + may be used to endorse or promote products derived from this + software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS +IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, +THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR +PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR +CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. +*****************************************************************************/ + +/***************************************************************************** +written by + Guanfeng Lv, last updated 10/26/2012 +*****************************************************************************/ + +#ifndef _UTABLE_ +#define _UTABLE_ + +#include "DdNode.h" + +class XManager; + +class XUTable{ +private: + friend class XManager; + + XManager *mgr; + int count; + int shiftSize; + DD *items; + long long findCount; + long long foundedCount; + double LinkLength(); + void Refresh(); + +public: + XUTable(XManager *manager, int vBitCount); + ~XUTable(); + void Clear(); + void Expand(); + DD Find_or_Add_Unique_Table(int v, DD A, DD B); + double HitRate(){ return 1.0 * foundedCount / Max(findCount, 1); } +}; + +#endif diff --git a/cpp/XBits.h b/cpp/XBits.h new file mode 100644 --- /dev/null +++ b/cpp/XBits.h @@ -0,0 +1,113 @@ +/***************************************************************************** +Copyright (c) 2012 - 2013, The Board of Trustees of the University of Beijing Technology and +the University of Griffith. +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are +met: + +* Redistributions of source code must retain the above + copyright notice, this list of conditions and the + following disclaimer. + +* Redistributions in binary form must reproduce the + above copyright notice, this list of conditions + and the following disclaimer in the documentation + and/or other materials provided with the distribution. + +* Neither the name of the University of Beijing Technology and + the University of Griffith nor the names of its contributors + may be used to endorse or promote products derived from this + software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS +IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, +THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR +PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR +CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. +*****************************************************************************/ + +/***************************************************************************** +written by + Guanfeng Lv, last updated 10/26/2012 +*****************************************************************************/ + +#ifndef __XBITS__ +#define __XBITS__ + +#include + +typedef unsigned char XBYTE; +class XBits{ +private: + int bitSize; + int chrCount; + XBYTE *buffer; +public: + XBits():bitSize(0),chrCount(0),buffer(0){}; + ~XBits(){ + bitSize = 0; + chrCount = 0; + if(buffer){ + free(buffer); + buffer = NULL; + }; + } + inline void set_size(int vsize); + inline int get_size(); + inline void set_value(int index, int value); + inline int get_value(int index); +}; + +inline void XBits::set_size(int vsize) +{ + if(buffer){ + free(buffer); + buffer = NULL; + }; + bitSize = vsize; + chrCount = (bitSize >> 3) + 1; + buffer = (XBYTE *)realloc(buffer, chrCount); + memset(buffer, 0, chrCount); +} + +inline int XBits::get_size() +{ + return bitSize; +} + +inline void XBits::set_value(int index, int value) +{ + if(index >= bitSize){ + int addChrCnt = ((index-bitSize)>>3)+10000; + buffer = (XBYTE *)realloc(buffer, chrCount + addChrCnt); + memset(&buffer[chrCount], 0, addChrCnt); + chrCount += addChrCnt; + bitSize = index + addChrCnt * 8; + } + + XBYTE one = 0x80; + int a = (index >> 3); + if(value == 1){ + buffer[a] = (buffer[a] | (one >> (index % 8))); + } + else{ + buffer[a] = (buffer[a] & ~(one >> (index % 8))); + } +} + +inline int XBits::get_value(int index) +{ + int a = (index >> 3); + XBYTE r = ((buffer[a] >> (7 - index % 8)) & 0x01); + return r; +} + +#endif diff --git a/cpp/XFunction.h b/cpp/XFunction.h new file mode 100644 --- /dev/null +++ b/cpp/XFunction.h @@ -0,0 +1,83 @@ + +#ifndef _FUNCTION_ +#define _FUNCTION_ + +#include +#include +#include +#include +using namespace std; + +class XFunction{ +public: + static float format_float(float v, int dotCnt) //dotCnt + { + if(dotCnt > 6) dotCnt = 6; + + float k = pow(10.0f, dotCnt); + float i = floor(v * k) / k; + return i; + } + + static double format_double(double v, int dotCnt) //dotCnt + { + if(dotCnt > 6) dotCnt = 6; + + double k = pow(10.0f, dotCnt); + double i = floor(v * k) / k; + return i; + } + + static string Format(int v, int outlen) + { + char buf[50]; + memset(buf, 0, 50); + sprintf(buf, "%d", v); + string r = buf; + size_t k = r.length(); + for(int i=0; i +#include +using namespace std; + +class XInts{ +private: + int size; + int *buffer; +public: + XInts():size(0),buffer(0){}; + ~XInts(){ + size = 0; + if(buffer){ + free(buffer); + buffer = NULL; + }; + } + inline void set_size(int vsize); + inline int get_size(); + inline void set_value(int index, int value); + inline int get_value(int index); +}; + +inline void XInts::set_size(int vsize) +{ + if(buffer){ + free(buffer); + buffer = NULL; + } + size = vsize; + + buffer = (int *)realloc(buffer, size * sizeof(int)); + memset(buffer, 0, size * sizeof(int)); +} + +inline int XInts::get_size() +{ + return size; +} + +inline void XInts::set_value(int index, int value) +{ + if(index >= size){ + int addCount = (index - size)+1000; + buffer = (int *)realloc(buffer, (size + addCount)*sizeof(int)); + memset(&buffer[size], 0, addCount * sizeof(int)); + size += addCount; + } + buffer[index] = value; +} + +inline int XInts::get_value(int index) +{ + if(index >= size) return 0; + return buffer[index]; +} + +#endif diff --git a/cpp/XVector.h b/cpp/XVector.h new file mode 100644 --- /dev/null +++ b/cpp/XVector.h @@ -0,0 +1,286 @@ +/***************************************************************************** +Copyright (c) 2012 - 2013, The Board of Trustees of the University of Beijing Technology and +the University of Griffith. +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are +met: + +* Redistributions of source code must retain the above + copyright notice, this list of conditions and the + following disclaimer. + +* Redistributions in binary form must reproduce the + above copyright notice, this list of conditions + and the following disclaimer in the documentation + and/or other materials provided with the distribution. + +* Neither the name of the University of Beijing Technology and + the University of Griffith nor the names of its contributors + may be used to endorse or promote products derived from this + software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS +IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, +THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR +PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR +CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. +*****************************************************************************/ + +/***************************************************************************** +written by + Guanfeng Lv, last updated 10/26/2012 +*****************************************************************************/ + + +#ifndef __XVECTOR__ +#define __XVECTOR__ + +#include +#include +using namespace std; + +template class XVector +{ +private: + int _size; + int _capacity; + +public: + T * data; + + T& operator[] (int index) const; + XVector& operator = (const XVector& other); + int size() const { return _size; }; + + void init(int vSize); + void resize(int vSize); + void shrink(); + void expand(int cnt); + T& back(); + void pop_back(); + void push_back(const T& key); + void insert(int index, T& key); + void clear(); + void erase(int index); + void remove(T &x); + int find(T &x); + int capacity(); + void Print(); + + XVector(); + XVector(XVector& other); + XVector(int size); + ~XVector(); +}; + +template XVector::XVector() +{ + data = NULL; + _size = 0; + _capacity = 0; +} + +template XVector::XVector(int vSize) +{ + init(vSize); +} + +template void XVector::init(int vSize) +{ + clear(); + + data = NULL; + _size = vSize; + _capacity = vSize; + data = (T*)realloc(data, _size * sizeof(T)); + for(int i=0; i<_size; i++){ + new (&data[i]) T(); + } +} + +template void XVector::resize(int vSize) +{ + if(vSize > _size){ + for(int i=_size; i XVector::XVector(XVector& other) +{ + data = NULL; + data = (T*)realloc(data, other.size() * sizeof(T)); + + for(int i=0;i XVector::~XVector() +{ + clear(); +} + +template inline void XVector::clear() +{ + if (data != 0) + { + for (int i = 0; i < _size; i++) + { + data[i].~T(); + + } + _size = 0; + free(data); + data = 0; + _capacity = 0; + } +} + +template inline int XVector::capacity() +{ + return _capacity; +} + +template inline void XVector::shrink() +{ + _capacity = _size; + data = (T*)realloc(data, _capacity * sizeof(T)); +} + +template inline void XVector::expand(int cnt) +{ + _capacity += cnt; + data = (T*)realloc(data, _capacity * sizeof(T)); +} + +template void XVector::insert(int x, T& key) +{ + if(_size == 0){ + push_back(key); + } + else{ + if (_size == _capacity) + { + _capacity = (2 > ((_capacity*3+1)>>1))?2:((_capacity*3+1)>>1); + data = (T*)realloc(data, _capacity * sizeof(T)); + } + _size++; + new (&data[_size-1]) T(); + + if(x >= _size-1) push_back(key); + else{ + for(int i= _size-1;i>=x;i--){ + data [i+1] = data[i]; + } + data[x] = key; + } + } +} + +templateinline void XVector::remove(T &x) +{ + for ( int i=0; i<_size; i++){ + if (data[i] == x){ + data[i].~T(); + data[i] = data[_size-1]; + data[_size-1].~T(); + _size--; + break; + } + } +} + +templateinline void XVector::erase(int index) +{ + if(index == _size-1) pop_back(); + else + { + data[index].~T(); + data[index] = data[_size-1]; + data[_size-1].~T(); + _size--; + } +} + +templateinline void XVector::push_back(const T& elem) +{ + if(_size == 0){ + _capacity = _size = 1; + data = (T*)realloc(data, _capacity * sizeof(T)); + new (&data[_size-1]) T(); + data[_size-1] = elem; + } + else{ + if (_size == _capacity){ + _capacity = (2 > ((_capacity*3+1)>>1))?2:((_capacity*3+1)>>1); + data = (T*)realloc(data, _capacity * sizeof(T)); + } + new (&data[_size]) T(); + data[_size] = elem; + _size++; + } +} + +template inline void XVector::pop_back() +{ + if(_size > 0){ + _size--; + data[_size].~T(); + } +} + +templateinline T& XVector::operator[] (int index) const +{ + return data[index]; +} + +templateinline XVector& XVector::operator = (const XVector& other) +{ + if(size() > 0) clear(); + data = 0; + if(_capacity < other.size()) data = (T*)malloc(other.size() * sizeof(T)); + + for(int i=0; iinline T& XVector::back() +{ + return data[_size-1]; +} + +template inline int XVector::find(T &x) +{ + for (int i = 0; i < _size; i++) { + if (data[i] == x) return i; + } + return -1; +} + +#endif diff --git a/cpp/main.cpp b/cpp/main.cpp new file mode 100644 --- /dev/null +++ b/cpp/main.cpp @@ -0,0 +1,67 @@ +/***************************************************************************** +Copyright (c) 2012 - 2013, The Board of Trustees of the University of Beijing Technology and +the University of Griffith. +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are +met: + +* Redistributions of source code must retain the above + copyright notice, this list of conditions and the + following disclaimer. + +* Redistributions in binary form must reproduce the + above copyright notice, this list of conditions + and the following disclaimer in the documentation + and/or other materials provided with the distribution. + +* Neither the name of the University of Beijing Technology and + the University of Griffith nor the names of its contributors + may be used to endorse or promote products derived from this + software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS +IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, +THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR +PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR +CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. +*****************************************************************************/ + +/***************************************************************************** +written by + Guanfeng Lv, last updated 10/26/2012 +*****************************************************************************/ + + +#include "BDDNode.h" + +int main(int argc, char **argv) +{ + + int vc = 6; + XBDDManager mgr(vc); + + BDD *x = new BDD[vc+1]; + for(int i=1; i<=vc; i++){ + x[i] = mgr.BddVar(i); + } + + BDD r = (!x[4] + !x[6]) * (!x[3] + !x[6]) * (!x[2] + !x[5]); + + BDD v = mgr.BddOne(); + if (r == v) cout<<"equal to one"< Bdd +finalize ptr = Bdd (unsafePerformIO $ newForeignPtr finalizerFree ptr) + +finalizeMgr :: Ptr CacXBddManager -> XBddManager +finalizeMgr ptr = XBddManager (unsafePerformIO $ newForeignPtr finalizerFree ptr) + +type CacXBddManager = () +newtype XBddManager = XBddManager (ForeignPtr CacXBddManager) + +type NullOp = Ptr CacBDD -> Ptr CacXBddManager -> IO (Ptr CacBDD) +type UnaryOp = Ptr CacBDD -> Ptr CacBDD -> IO (Ptr CacBDD) +type BinaryOp = Ptr CacBDD -> Ptr CacBDD -> Ptr CacBDD -> IO (Ptr CacBDD) + +foreign import ccall unsafe "BDDNodeC.h BDD_new" bdd_new :: Word -> IO (Ptr CacBDD) +foreign import ccall unsafe "BDDNodeC.h XBDDManager_new" xBddManager_new :: CInt -> IO (Ptr CacXBddManager) +foreign import ccall unsafe "BDDNodeC.h XBDDManager_ShowInfo" xBddManager_showInfo :: Ptr CacXBddManager -> IO () +foreign import ccall unsafe "BDDNodeC.h XBDDManager_BddOne" xBddManager_BddOne :: NullOp +foreign import ccall unsafe "BDDNodeC.h XBDDManager_BddZero" xBddManager_BddZero :: NullOp +foreign import ccall unsafe "BDDNodeC.h XBDDManager_BddVar" xBddManager_BddVar :: Ptr CacBDD -> Ptr CacXBddManager -> CInt -> IO (Ptr CacBDD) +foreign import ccall unsafe "BDDNodeC.h XBDDManager_Ite" xBddManager_Ite :: Ptr CacBDD -> Ptr CacXBddManager -> BinaryOp +foreign import ccall unsafe "BDDNodeC.h BDD_Operator_Equal" bdd_Operator_Equal :: Ptr CacBDD -> Ptr CacBDD -> IO Bool +foreign import ccall unsafe "BDDNodeC.h BDD_Operator_Not" bdd_Operator_Not :: UnaryOp +foreign import ccall unsafe "BDDNodeC.h BDD_Operator_Or" bdd_Operator_Or :: BinaryOp +foreign import ccall unsafe "BDDNodeC.h BDD_Operator_And" bdd_Operator_And :: BinaryOp +foreign import ccall unsafe "BDDNodeC.h BDD_Operator_Xor" bdd_Operator_Xor :: BinaryOp +foreign import ccall unsafe "BDDNodeC.h BDD_Exist" bdd_Exist :: BinaryOp +foreign import ccall unsafe "BDDNodeC.h BDD_Universal" bdd_Universal :: BinaryOp +foreign import ccall unsafe "BDDNodeC.h BDD_Restrict" bdd_Restrict :: BinaryOp +foreign import ccall unsafe "BDDNodeC.h BDD_Variable" bdd_Variable :: Ptr CacBDD -> IO CInt +foreign import ccall unsafe "BDDNodeC.h BDD_Then" bdd_Then :: UnaryOp +foreign import ccall unsafe "BDDNodeC.h BDD_Else" bdd_Else :: UnaryOp + +-- | The maximum number of variables +maximumvar :: Int +maximumvar = 1048576 + +manager :: XBddManager +manager = finalizeMgr (unsafePerformIO $ xBddManager_new (fromIntegral maximumvar)) +{-# NOINLINE manager #-} + +-- | This should cover BDDOne, BddZero +fromManager :: NullOp -> Bdd +fromManager nulloperator = let (XBddManager mptr) = manager in + finalize $ unsafePerformIO $ + withForeignPtr mptr $ nulloperator (unsafePerformIO (bdd_new 8)) +{-# NOINLINE fromManager #-} + +withBDD :: UnaryOp -> Bdd -> Bdd +withBDD unioperator (Bdd fptr) = finalize $ unsafePerformIO $ + withForeignPtr fptr $ unioperator (unsafePerformIO (bdd_new 8)) +{-# NOINLINE withBDD #-} + +withTwoBDDs :: BinaryOp -> Bdd -> Bdd -> Bdd +withTwoBDDs binoperator (Bdd fptr1) (Bdd fptr2) = finalize $ unsafePerformIO $ + withForeignPtr fptr1 $ + withForeignPtr fptr2 . binoperator (unsafePerformIO (bdd_new 8)) +{-# NOINLINE withTwoBDDs #-} + +fromBDD :: (Ptr CacBDD -> IO a) -> Bdd -> a +fromBDD property (Bdd fptr1) = unsafePerformIO $ + withForeignPtr fptr1 property +{-# NOINLINE fromBDD #-} + +fromTwoBDDs :: (Ptr CacBDD -> Ptr CacBDD -> IO a) -> Bdd -> Bdd -> a +fromTwoBDDs binproperty (Bdd fptr1) (Bdd fptr2) = unsafePerformIO $ + withForeignPtr fptr1 $ + withForeignPtr fptr2 . binproperty +{-# NOINLINE fromTwoBDDs #-} + +-- | Restrict a single variable to a given value +restrict :: Bdd -> (Int,Bool) -> Bdd +restrict b (n,bit) = withTwoBDDs bdd_Restrict b (if bit then var n else neg (var n)) +{-# NOINLINE restrict #-} + +-- | Restrict with a (partial) assignment +restrictSet :: Bdd -> Assignment -> Bdd +restrictSet b bits = withTwoBDDs bdd_Restrict b (conSet $ map (\(n,bit) -> if bit then var n else neg (var n)) bits) +{-# NOINLINE restrictSet #-} + +-- | Restrict with a law +restrictLaw :: Bdd -> Bdd -> Bdd +restrictLaw = withTwoBDDs bdd_Restrict +{-# NOINLINE restrictLaw #-} + +-- | Existential Quantification +exists :: Int -> Bdd -> Bdd +exists n b = withTwoBDDs bdd_Exist b (var n) +{-# NOINLINE exists #-} + +-- | Universal Quantification +forall :: Int -> Bdd -> Bdd +forall n b = withTwoBDDs bdd_Universal b (var n) +{-# NOINLINE forall #-} + +-- | Big Existential Quantification +existsSet :: [Int] -> Bdd -> Bdd +existsSet ns b = foldl (flip exists) b ns + +-- | Big Universal Quantification +forallSet :: [Int] -> Bdd -> Bdd +forallSet ns b = foldl (flip forall) b ns + +-- | True constant +top :: Bdd +top = fromManager xBddManager_BddOne +{-# NOINLINE top #-} + +-- | False constant +bot :: Bdd +bot = fromManager xBddManager_BddZero +{-# NOINLINE bot #-} + +-- | Variable, indexed by any integer from 0 to 1.000.000 +-- FIXME: Segfaults if n is negative or out of range. +-- Can we add a safety check without affecting performance? +var :: Int -> Bdd +var n = fromManager (\bptr mptr -> xBddManager_BddVar bptr mptr (fromIntegral (n+1))) +{-# NOINLINE var #-} + +-- | If ... then ... else ... +ifthenelse :: Bdd -> Bdd -> Bdd -> Bdd +ifthenelse (Bdd test) (Bdd yes) (Bdd no) = + let (XBddManager mptr) = manager in + finalize $ unsafePerformIO $ + withForeignPtr test (\t -> + withForeignPtr yes (\y -> + withForeignPtr no (\n -> + withForeignPtr mptr (\m -> xBddManager_Ite (unsafePerformIO (bdd_new 8)) m t y n)))) +{-# NOINLINE ifthenelse #-} + +instance Eq Bdd where + b1 == b2 = same b1 b2 + +same :: Bdd -> Bdd -> Bool +same = fromTwoBDDs bdd_Operator_Equal +{-# NOINLINE same #-} + +-- | Negation +neg :: Bdd -> Bdd +neg = withBDD bdd_Operator_Not +{-# NOINLINE neg #-} + +-- | Equivalence aka Biimplication +equ :: Bdd -> Bdd -> Bdd +equ b1 b2 = con (imp b1 b2) (imp b2 b1) -- ugly... +{-# NOINLINE equ #-} + +-- | Implication, via disjunction and negation. +-- Somehow this is faster than calling LessEqual? +imp :: Bdd -> Bdd -> Bdd +imp b1 = dis (neg b1) +{-# NOINLINE imp #-} + +-- | Conjunction +con :: Bdd -> Bdd -> Bdd +con = withTwoBDDs bdd_Operator_And +{-# NOINLINE con #-} + +-- | Disjunction +dis :: Bdd -> Bdd -> Bdd +dis = withTwoBDDs bdd_Operator_Or +{-# NOINLINE dis #-} + +-- | Exclusive Or +xor :: Bdd -> Bdd -> Bdd +xor = withTwoBDDs bdd_Operator_Xor +{-# NOINLINE xor #-} + +-- | Big Conjunction +conSet :: [Bdd] -> Bdd +conSet [] = top +conSet (b:bs) = + if bot `elem` (b:bs) + then bot + else foldl con b bs +{-# NOINLINE conSet #-} + +-- | Big Disjunction +disSet :: [Bdd] -> Bdd +disSet [] = bot +disSet (b:bs) = + if top `elem` (b:bs) + then top + else foldl dis b bs +{-# NOINLINE disSet #-} + +-- | Big Xor +xorSet :: [Bdd] -> Bdd +xorSet [] = bot +xorSet (b:bs) = foldl xor b bs +{-# NOINLINE xorSet #-} + +-- | Greatest fixpoint for a given operator. +gfp :: (Bdd -> Bdd) -> Bdd +gfp operator = gfpStep top (operator top) where + gfpStep :: Bdd -> Bdd -> Bdd + gfpStep current next = + if current == next + then current + else gfpStep next (operator next) + +-- | Then-branch of a given BDD, setting firstVarOf to True. +thenOf :: Bdd -> Bdd +thenOf = withBDD bdd_Then + +-- | Else-branch of a given BDD, setting firstVarOf to False. +elseOf :: Bdd -> Bdd +elseOf = withBDD bdd_Else + +-- | The first variable of a given BDD, if there is one. +firstVarOf :: Bdd -> Maybe Int +firstVarOf b + | b == bot = Nothing + | b == top = Nothing + | otherwise = Just (fromIntegral (fromBDD bdd_Variable b) -(1::Int)) + +-- | The maximum variable of a given BDD, if there is one. +maxVarOf :: Bdd -> Maybe Int +maxVarOf b + | b == bot = Nothing + | b == top = Nothing + | otherwise = maximum [ Just $ fromIntegral v - (1::Int), m1, m2 ] where + v = fromBDD bdd_Variable b + m1 = maxVarOf $ thenOf b + m2 = maxVarOf $ elseOf b + +-- | All variables in a given BDD, *not* sorted, lazy. +allVarsOf :: Bdd -> [Int] +allVarsOf b + | b == bot = [] + | b == top = [] + | otherwise = let (Just n) = firstVarOf b in n : nub (allVarsOf (thenOf b) ++ allVarsOf (elseOf b)) + +-- | All variables in a given BDD, sorted, *not* lazy. +allVarsOfSorted :: Bdd -> [Int] +allVarsOfSorted = sort . allVarsOf + +-- | List all the sub-BDDs of a given BDD. +subsOf :: Bdd -> [Bdd] +subsOf b + | b == bot = [] + | b == top = [] + | otherwise = nub $ b : (subsOf (thenOf b) ++ subsOf (elseOf b)) + +-- | Size of the BDD, should be the number of non-terminal nodes. +sizeOf :: Bdd -> Int +sizeOf = length.subsOf + +-- FIXME: Should we print outermost brackets around non-constant BDDs? +instance Show Bdd where + show b = show (unravel b) + +-- TODO: add a Read instance and test that Show and Read are inverses of each other + +-- | A simple tree definition to show BDDs as text. +data BddTree = Bot | Top | Var Int BddTree BddTree deriving (Show) + +-- | Convert a BDD to a tree. +unravel :: Bdd -> BddTree +unravel b + | b == bot = Bot + | b == top = Top + | otherwise = Var n (unravel (thenOf b)) (unravel (elseOf b)) where (Just n) = firstVarOf b + +-- | Convert a tree to a BDD. +ravel :: BddTree -> Bdd +ravel Bot = bot +ravel Top = top +ravel (Var n nthen nelse) = ifthenelse (var n) (ravel nthen) (ravel nelse) + +-- | Evaluate a BDD given an assignment. +-- Returns Nothing if the assignment does not cover allVarsOf b. +evaluate :: Bdd -> Assignment -> Maybe Bool +evaluate b ass = + if all (`elem` map fst ass) (allVarsOf b) + then Just $ top == restrictSet b ass + else Nothing + +-- | Evaluate a BDD given a total assignment function. +evaluateFun :: Bdd -> (Int -> Bool) -> Bool +evaluateFun b f + | b == bot = False + | b == top = True + | otherwise = + let (Just n) = firstVarOf b + in evaluateFun ((if f n then thenOf else elseOf) b) f + +-- | Get all satisfying assignments. These will be partial, i.e. only +-- contain (a subset of) the variables that actually occur in the BDD. +allSats :: Bdd -> [Assignment] +allSats b + | b == bot = [] + | b == top = [ [] ] + | otherwise = + [ (n,True):rest | rest <- allSats (thenOf b) ] ++ [ (n,False):rest | rest <- allSats (elseOf b) ] + where (Just n) = firstVarOf b + +-- | Get the lexicographically smallest satisfying assignment, if there is any. +anySat :: Bdd -> Maybe Assignment +anySat b + | b == bot = Nothing + | b == top = Just [] + | otherwise = Just ((n,hastobetrue):rest) where + hastobetrue = elseOf b == bot + (Just n) = firstVarOf b + (Just rest) = if hastobetrue then anySat (thenOf b) else anySat (elseOf b) + +-- | Given a set of all variables, complete an assignment. +completeAss :: [Int] -> Assignment -> [Assignment] +completeAss allvars ass = + if null (addvars ass) + then [ass] + else concatMap (completeAss allvars) (extend ass (head (addvars ass))) + where + addvars s = allvars \\ sort (map fst s) + extend s v = [ (v,False):s, (v,True):s ] + +-- | Get all complete assignments, given a set of all variables. +-- In particular this will include variables not in the BDD. +allSatsWith :: [Int] -> Bdd -> [Assignment] +allSatsWith allvars b = concatMap (completeAss allvars) (allSats b) + +-- | Given a set of all variables, get the number of satisfying assignments. +-- Note that allvars should be nub'd and sorted. +satCountWith :: [Int] -> Bdd -> Int +satCountWith allvars b + | b == top = 2 ^ length allvars + | b == bot = 0 + | otherwise = (2 ^ length varsjumped) * posbelow where + (Just curvar) = firstVarOf b + varsjumped = filter (< curvar) allvars + varsleft = filter (> curvar) allvars + posbelow = sum [satCountWith varsleft (branch b) | branch <- [thenOf,elseOf] ] + +-- | Given a set of all variables, get the lexicographically smallest complete +-- satisfying assignment, if there is any. +anySatWith :: [Int] -> Bdd -> Maybe Assignment +anySatWith allvars b = case anySat b of + Nothing -> Nothing + Just partass -> Just $ head $ completeAss allvars partass + +-- | Relabel variables according to the given mapping. +relabel :: [(Int,Int)] -> Bdd -> Bdd +relabel [] b = b +relabel rel@((n,newn):rest) b + | b == bot = b + | b == top = b + | otherwise = case compare n (fromJust (firstVarOf b)) of + LT -> relabel rest b + EQ -> ifthenelse (var newn) (relabel rest (thenOf b)) (relabel rest (elseOf b)) + GT -> ifthenelse (var (fromJust (firstVarOf b))) (relabel rel (thenOf b)) (relabel rel (elseOf b)) + +-- | Show internal statistics. +showInfo :: IO () +showInfo = withForeignPtr mptr xBddManager_showInfo where (XBddManager mptr) = manager + +-- | QuickCheck Arbitrary instances for BDDs +instance Arbitrary Bdd where + arbitrary = sized randombdd + +randomvarnumber :: Gen Int +randomvarnumber = choose (0, 100) + +randombdd :: Int -> Gen Bdd +randombdd 0 = oneof + [ pure top + , pure bot + , var <$> randomvarnumber + ] +randombdd n = oneof + [ var <$> randomvarnumber + , neg <$> smallerbdd + , con <$> smallerbdd <*> smallerbdd + , dis <$> smallerbdd <*> smallerbdd + , imp <$> smallerbdd <*> smallerbdd + , equ <$> smallerbdd <*> smallerbdd + , xor <$> smallerbdd <*> smallerbdd + , exists <$> randomvarnumber <*> smallerbdd + , existsSet <$> listOf randomvarnumber <*> smallerbdd + , forall <$> randomvarnumber <*> smallerbdd + , forallSet <$> listOf randomvarnumber <*> smallerbdd + ] + where + smallerbdd = randombdd (min (n `div` 2) 10) diff --git a/hs/Data/HasCacBDD/Visuals.hs b/hs/Data/HasCacBDD/Visuals.hs new file mode 100644 --- /dev/null +++ b/hs/Data/HasCacBDD/Visuals.hs @@ -0,0 +1,75 @@ +-- | Very simple visualisation of BDDs using /dot/. + +module Data.HasCacBDD.Visuals ( + genGraph, + genGraphWith, + showGraph, + svgGraph +) where + +import Data.HasCacBDD +import System.Process +import System.IO + +-- | Generate a string which describes the BDD in the dot language. +genGraph :: Bdd -> String +genGraph = genGraphWith show + +-- | Given a function to show variables, generate a string which describes the BDD in the dot language. +genGraphWith :: (Int -> String) -> Bdd -> String +genGraphWith myShow myb + | myb == bot = "digraph g { Bot [label=\"0\",shape=\"box\"]; }" + | myb == top = "digraph g { Top [label=\"1\",shape=\"box\"]; }" + | otherwise = "strict digraph g {\n" ++ links ++ sinks ++ rankings ++ "}" where + (links,topdone) = genGraphStep [] myb + genGraphStep :: [(Bdd,Int)] -> Bdd -> (String,[(Bdd,Int)]) + genGraphStep done curB = case (lookup curB done, curB == top || curB == bot) of + (_ ,True) -> ("",done) + (Just _, _) -> ("",done) + (Nothing,False) -> + let + thisn = if null done then 0 else maximum (map snd done) + 1 + thisnstr = show thisn + (Just thisvar) = firstVarOf curB + out1 = "n" ++ thisnstr ++ " [label=\"" ++ myShow thisvar ++ "\",shape=\"circle\"];\n" + lhs = thenOf curB + (lhsoutput,lhsdone) = genGraphStep ((curB,thisn):done) lhs + (Just leftn) = lookup lhs lhsdone + out2 + | lhs == top = "n"++ thisnstr ++" -> Top;\n" + | lhs == bot = "n"++ thisnstr ++" -> Bot;\n" + | otherwise = "n"++ thisnstr ++" -> n" ++ show leftn ++";\n" ++ lhsoutput + rhs = elseOf curB + (rhsoutput,rhsdone) = genGraphStep lhsdone rhs + (Just rightn) = lookup rhs rhsdone + out3 + | rhs == top = "n"++ thisnstr ++" -> Top [style=dashed];\n" + | rhs == bot = "n"++ thisnstr ++" -> Bot [style=dashed];\n" + | otherwise = "n"++ thisnstr ++" -> n"++ show rightn ++" [style=dashed];\n" ++ rhsoutput + in (out1 ++ out2 ++ out3, rhsdone) + sinks = "Bot [label=\"0\",shape=\"box\"];\n" ++ "Top [label=\"1\",shape=\"box\"];\n" + rankings = concat [ "{ rank=same; "++ unwords (nodesOf v) ++ " }\n" | v <- allVarsOf myb ] + nodesOf v = map (("n"++).show.snd) $ filter ( \(b,_) -> firstVarOf b == Just v ) topdone + +-- | Display the graph of a BDD with dot. +showGraph :: Bdd -> IO () +showGraph b = do + (inp,_,_,pid) <- runInteractiveProcess "/usr/bin/dot" ["-Tx11"] Nothing Nothing + hPutStr inp (genGraph b) + hFlush inp + hClose inp + _ <- waitForProcess pid + return () + +-- | Generate SVG of a BDD with dot. +svgGraph :: Bdd -> IO String +svgGraph b = do + (inp,out,_,pid) <- runInteractiveProcess "/usr/bin/dot" ["-Tsvg" ] Nothing Nothing + hPutStr inp (genGraph b) + hSetBinaryMode inp False + hSetBinaryMode out False + hFlush inp + hClose inp + outstring <- hGetContents out + _ <- waitForProcess pid + return $ (unlines.tail.lines) outstring diff --git a/stack.yaml b/stack.yaml new file mode 100644 --- /dev/null +++ b/stack.yaml @@ -0,0 +1,3 @@ +resolver: lts-8.0 +packages: +- '.' diff --git a/tests/Basics.hs b/tests/Basics.hs new file mode 100644 --- /dev/null +++ b/tests/Basics.hs @@ -0,0 +1,44 @@ +module Main where + +import Data.HasCacBDD +import System.Exit + +main :: IO () +main = do + putStrLn "\nRunning basic tests ..." + if all snd tests + then do + putStrLn "All passed." + exitSuccess + else do + putStrLn "FAILURES:" + let failures = filter (not.snd) tests + mapM_ (putStrLn . fst) failures + putStrLn "All results:" + mapM_ print tests + exitFailure + +tests :: [(String,Bool)] +tests = + [ ("top == top", top == top) + , ("top /= bot", top /= bot) + , ("bot /= top", bot /= top) + , ("bot == bot", bot == bot) + , ("neg bot == top", neg bot == top) + , ("neg bot /= bot", neg bot /= bot) + , ("var 1 == var 1", var 1 == var 1) + , ("var 5 /= var 7", var 5 /= var 7) + , ("null (allSats bot)", null (allSats bot)) + , ("allSats top == [[]]", allSats top == [[]]) + , ("var 3 == con (var 3) top", var 3 == con (var 3) top) + , ("var 4 /= con (var 3) top", var 4 /= con (var 3) top) + , ("equ (var 1) (var 1) == top", equ (var 1) (var 1) == top) + , ("exists 1 (neg $ var 1) == top", exists 1 (neg $ var 1) == top) + , ("exists 1 (neg $ var 2) /= top", exists 1 (neg $ var 2) /= top) + , ("gfp (\b -> con b (var 3)) == var 3", gfp (\b -> con b (var 3)) == var 3) + , ("imp (conSet [var 1, var 0]) (var 1) == top", imp (conSet [var 1, var 0]) (var 1) == top) + , ("imp (conSet [var 0, var 1]) (var 0) == top", imp (conSet [var 0, var 1]) (var 0) == top) + , ("imp (con (var 0) (var 1)) (var 0) == top", imp (con (var 0) (var 1)) (var 0) == top) + , ("show top == \"Top\"", show top == "Top") + , ("show bot == \"Bot\"", show bot == "Bot") + ] diff --git a/tests/Example.hs b/tests/Example.hs new file mode 100644 --- /dev/null +++ b/tests/Example.hs @@ -0,0 +1,44 @@ +module Main +where + +import Data.HasCacBDD +import System.Exit +import System.IO + +main :: IO () +main = do + hSetBuffering stdout NoBuffering + putStrLn "Creating some BDDs:" + putStrLn $ "top : " ++ show top + putStrLn $ "bot : " ++ show bot + putStrLn $ "var1: " ++ show (var 1) + putStrLn $ "var1: " ++ show (var 1) + putStrLn $ "var2: " ++ show (var 2) + putStrLn "\nChecking some tautologies:" + print $ bot == bot + print $ top == top + print $ var 1 == var 1 + print $ imp (var 1) (var 1) == top + print $ equ (var 1) (var 1) == top + print $ exists 1 (neg $ var 1) == top + print $ gfp (\b -> con b (var 3)) == var 3 + print $ imp (conSet [var 1, var 0]) (var 1) == top + print $ imp (conSet [var 0, var 1]) (var 0) == top + print $ imp (con (var 0) (var 1)) (var 0) == top + putStrLn "\nAnd some contradictions:" + print $ bot == top + print $ top == bot + print $ var 1 == top + print $ dis (var 1) (neg $ var 2) == top + print $ dis (var 1) (var 2) == top + print $ var 1 == var 2 + print $ forall 1 (var 1) == top + putStrLn "\nLaws from de Morgan:" + print $ dis (neg $ var 1) (neg $ var 2) == neg (con (var 1) (var 2)) + print $ con (neg $ var 1) (neg $ var 2) == neg (dis (var 1) (var 2)) + putStrLn "\nThe example from CacBDDs main.cpp: (!x[4] + !x[6]) * (!x[3] + !x[6]) * (!x[2] + !x[5])" + let cacExample = conSet [ dis (neg (var 4)) (neg (var 6)) , neg (var 3) `dis` neg (var 6), neg (var 2) `dis` neg (var 5) ] + print cacExample + print $ cacExample == top + putStrLn "Good Bye." + exitSuccess diff --git a/tests/Tautologies.hs b/tests/Tautologies.hs new file mode 100644 --- /dev/null +++ b/tests/Tautologies.hs @@ -0,0 +1,63 @@ +module Main where + +import Control.Monad +import Data.HasCacBDD +import Data.List +import Data.Maybe +import Data.Tuple +import Text.Printf +import Test.QuickCheck +import Test.QuickCheck.Test +import System.Exit + +main :: IO () +main = do + results <- mapM (\(s,a) -> printf "%-25s: " s >> a) tests + unless (all isSuccess results) exitFailure + showInfo + +tests :: [(String, IO Result)] +tests = + [("selfEqual", quickCheckResult (\b -> (b::Bdd) == b)) + ,("idSymmetry", quickCheckResult (\a b -> ((a::Bdd) == (b::Bdd)) == (b == a))) + ,("singleNegation", quickCheckResult (\b -> neg b /= b)) + ,("doubleNegation", quickCheckResult (\b -> neg (neg b) == b)) + ,("selfImp", quickCheckResult (\b -> imp b b == top)) + ,("selfEqu", quickCheckResult (\b -> equ b b == top)) + ,("selfXor", quickCheckResult (\b -> xor b b == bot)) + ,("excludedMiddle", quickCheckResult (\b -> b `dis` neg b == top)) + ,("deMorganOne", quickCheckResult (\a b -> neg (a `con` b) == (neg a `dis` neg b))) + ,("deMorganTwo", quickCheckResult (\a b -> neg (a `dis` b) == (neg a `con` neg b))) + ,("identityOne", quickCheckResult (\as b -> conSet as `imp` b == disSet (map neg as) `dis` b)) + ,("conElim", quickCheckResult (\a b -> imp (con a b) a == top)) + ,("conElim3", quickCheckResult (\a b c -> imp (conSet [a, b, c]) a == top)) + ,("negNotEqual", quickCheckResult (\b -> neg b /= b)) + ,("quantifDuality", quickCheckResult (forAll (elements [0..maximumvar]) (\n b -> forall n b == neg (exists n (neg b))))) + ,("allSats", quickCheckResult (\b -> all (\s -> restrictSet b s == top) (allSats b))) + ,("anySat", quickCheckResult (\b -> if b==bot then isNothing (anySat b) else restrictSet b (fromJust $ anySat b) == top)) + ,("ifthenelse", quickCheckResult (\a b c -> ifthenelse a b c == neg (dis (con a (neg b)) (con (neg a) (neg c))))) + ,("ravel-unravel", quickCheckResult (\b -> b == ravel (unravel b))) + ,("firstVarOf", quickCheckResult (\b -> if b `elem` [bot,top] then isNothing (firstVarOf b) else Just (head (allVarsOfSorted b)) == firstVarOf b)) + ,("maxVarOf", quickCheckResult (\b -> if b `elem` [bot,top] then isNothing (maxVarOf b) else Just (last (allVarsOfSorted b)) == maxVarOf b)) + ,("thenOf", quickCheckResult (\b -> if b `elem` [bot,top] then thenOf b == b else thenOf b == restrict b (fromJust $ firstVarOf b, True ))) + ,("elseOf", quickCheckResult (\b -> if b `elem` [bot,top] then elseOf b == b else elseOf b == restrict b (fromJust $ firstVarOf b, False))) + ,("deMorganOneSet", quickCheckResult (\as -> neg (conSet as) == disSet (map neg as))) + ,("deMorganTwoSet", quickCheckResult (\as -> neg (disSet as) == conSet (map neg as))) + ,("xorSetCommute", quickCheckResult (\a as -> xorSet (a:as) == xor (xorSet as) a)) + ,("gfpCon", quickCheckResult (\b -> gfp (`con` b) == b)) + ,("sizeNeg", quickCheckResult (\b -> sizeOf b == sizeOf (neg b))) + ,("restrictLaw", quickCheckResult (\a b -> b `imp` equ (restrictLaw a b) a == top)) + ,("evaluate", quickCheckResult (\b -> all (\s -> evaluate b s == Just True) (allSatsWith (allVarsOf b) b))) + ,("evaluateFun", quickCheckResult (\b -> all (\s -> evaluateFun b (\n -> fromJust $ lookup n s)) (allSats b))) + ,("allSatsWith", quickCheckResult (\b -> all (\s -> restrictSet b s == top) (allSatsWith (allVarsOf b) b))) + ,("anySatWith", quickCheckResult (\b -> let vs = allVarsOf b in if b==bot then isNothing (anySatWith vs b) else restrictSet b (fromJust $ anySatWith vs b) == top)) + ,("satCountWith", quickCheckResult (\b -> let vs = allVarsOf b in length (allSatsWith vs b) == satCountWith vs b)) + ,("subsOf", quickCheckResult (\b -> all (`elem` subsOf b) (subsOf $ thenOf b))) + , let relabelTest b c = relabel gnippam (relabel mapping b) == b where + vs = reverse $ nub (allVarsOf b ++ allVarsOf c) + mapping = zip vs (map (+100) vs) + gnippam = map swap mapping + in ("relabel", quickCheckResult relabelTest) + , ("show", quickCheckResult (\a b -> (show (unravel a) == show (unravel b)) == (a == (b::Bdd)))) + , ("showList", quickCheckResult (\a b -> (showList [unravel a] "" == showList [unravel b] "") == (a == (b::Bdd)))) + ]