HasCacBDD (empty) → 0.1.0.0
raw patch · 33 files changed
+4452/−0 lines, 33 filesdep +HasCacBDDdep +QuickCheckdep +basebuild-type:Customsetup-changed
Dependencies added: HasCacBDD, QuickCheck, base, process
Files
- HasCacBDD.cabal +75/−0
- LICENSE +340/−0
- README.md +8/−0
- Setup.hs +58/−0
- c/BDDNodeC.cpp +60/−0
- c/BDDNodeC.h +39/−0
- c/Makefile +14/−0
- cpp/BDDNode.cpp +260/−0
- cpp/BDDNode.h +121/−0
- cpp/Base.h +78/−0
- cpp/CTable.cpp +146/−0
- cpp/CTable.h +88/−0
- cpp/DdNode.cpp +82/−0
- cpp/DdNode.h +120/−0
- cpp/Makefile +14/−0
- cpp/Manager.cpp +1014/−0
- cpp/Manager.h +232/−0
- cpp/OriginalMakefile +60/−0
- cpp/README +23/−0
- cpp/Timer.h +73/−0
- cpp/UTable.cpp +166/−0
- cpp/UTable.h +71/−0
- cpp/XBits.h +113/−0
- cpp/XFunction.h +83/−0
- cpp/XInts.h +104/−0
- cpp/XVector.h +286/−0
- cpp/main.cpp +67/−0
- hs/Data/HasCacBDD.hs +428/−0
- hs/Data/HasCacBDD/Visuals.hs +75/−0
- stack.yaml +3/−0
- tests/Basics.hs +44/−0
- tests/Example.hs +44/−0
- tests/Tautologies.hs +63/−0
+ HasCacBDD.cabal view
@@ -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 <http://kailesu.net/CacBDD> 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
+ LICENSE view
@@ -0,0 +1,340 @@+ GNU GENERAL PUBLIC LICENSE+ Version 2, June 1991++ Copyright (C) 1989, 1991 Free Software Foundation, Inc., <http://fsf.org/>+ 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.+
+ README.md view
@@ -0,0 +1,8 @@+HasCacBDD+=========++[](https://travis-ci.org/m4lvin/HasCacBDD)++Haskell bindings for CacBDD, a Binary Decision Diagram (BDD) package with dynamic cache management.++Original C++ code from <http://kailesu.net/CacBDD> and a C wrapper are included.
+ Setup.hs view
@@ -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"]
+ c/BDDNodeC.cpp view
@@ -0,0 +1,60 @@+#include "BDDNodeC.h"++#include "BDDNode.h"+#include <stdio.h>++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<int>* 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(); }
+ c/BDDNodeC.h view
@@ -0,0 +1,39 @@+#include <BDDNode.h>++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<int>* 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);+}
+ c/Makefile view
@@ -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
+ cpp/BDDNode.cpp view
@@ -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 <cstdio> + +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<int> &permu) const +{ + int *x = new int[permu.size()]; + for(int i=0; i<permu.size(); i++){ + x[i] = permu[i]; + } + DD result = mgr->Permute(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<int> &vars) +{ + mgr->Support(node, vars); +}
+ cpp/BDDNode.h view
@@ -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<int> &permu) const; + BDD AndExist(const BDD& other, const BDD& cube); + bool IsComp() { return (ISCOMP(node) != 0); } + void Support(vector<int> &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<int> &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
+ cpp/Base.h view
@@ -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
+ cpp/CTable.cpp view
@@ -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 <iostream> +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; i<count; i++){ + items[i].SetValue(0,0,0,0); + } + toAddCount = 0; + findCount = 0; + foundedCount = 0; + missCount = 0; +} + +void XCTable::Refresh() +{ + Clear(); + + for(int i=1; i<mgr->NodeCount(); 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<count; i++){ + int pos = Hash3(items[i].A, items[i].B, items[i].C, newshiftSize); + newitems[pos].A = items[i].A; + newitems[pos].B = items[i].B; + newitems[pos].C = items[i].C; + newitems[pos].R = items[i].R; + } + delete []items; + items = newitems; + count = newcount; + shiftSize = newshiftSize; + toAddCount = 0; +} + +bool XCTable::Find(DD A, DD B, DD C, DD &r) +{ + findCount++; + int pos = Hash3(A, B, C, shiftSize); + if ((A == items[pos].A)&&(B == items[pos].B)&&(C == items[pos].C)){ + foundedCount++; + r = items[pos].R; + return true; + } + missCount++; + return false; +} + +void XCTable::Insert(DD A, DD B, DD C, DD tmp) +{ + if(toAddCount > 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; + } +}
+ cpp/CTable.h view
@@ -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
+ cpp/DdNode.cpp view
@@ -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<slotSize; k++){ + slots[0][k].SetValue(0,0,0,0); + } + + slotCount = 1; + nodeCount = 1; +} + +void DdNodes::Clear() +{ + if(slots == NULL) return ; + + for(int i=0; i<slotCount; i++){ + delete [](slots[i]); + slots[i] = NULL; + } + delete []slots; + slots = NULL; +}
+ cpp/DdNode.h view
@@ -0,0 +1,120 @@+/***************************************************************************** +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 _DDNODE_ +#define _DDNODE_ + +#include "Base.h" +#include <stdlib.h> +#include <iostream> +#include <assert.h> + +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<slotSize; k++){ + slots[slotCount][k].SetValue(0,0,0,0); + } + slotCount++; + + } + nodeCount++; + return (nodeCount - 1); +}; + +#endif
+ cpp/Makefile view
@@ -0,0 +1,14 @@+.SUFFIXES: .o .cc .u++CPP = g+++CFLAGS = -g -O3 -Wno-deprecated -shared -fPIC++default:+ $(CPP) -c UTable.cpp $(CFLAGS)+ $(CPP) -c Manager.cpp $(CFLAGS)+ $(CPP) -c CTable.cpp $(CFLAGS)+ $(CPP) -c BDDNode.cpp $(CFLAGS)+ $(CPP) -c DdNode.cpp $(CFLAGS)++clean:+ rm -f *.o
+ cpp/Manager.cpp view
@@ -0,0 +1,1014 @@+/***************************************************************************** +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 and Kaile Su, last updated 14/07/2015 +*****************************************************************************/ + +#include "Base.h" +#include "Manager.h" +#include "Timer.h" +#include "XBits.h" +#include "XFunction.h" +#include "BDDNode.h" + +#include <cstdio> +#include <assert.h> +#include <cmath> +#include <limits.h> +#include <iostream> +#include <algorithm> +#include <fstream> +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<DD> dds) +{ + if(dds.size() < 2) return Zero; + + DD r = And(dds[0], dds[1]); + for(int i=2; i<dds.size(); i++){ + r = And(r, dds[i]); + } + return r; +} + +DD XManager::Or(const XVector<DD> dds) +{ + if(dds.size() < 2) return Zero; + + DD r = Or(dds[0], dds[1]); + for(int i=2; i<dds.size(); i++){ + r = Or(r, dds[i]); + } + return r; +} + +DD XManager::PermuteRecur(DD A, int *permu, XInts *visited) +{ + if(A == One || A == Zero) return A; + + int isComple = ISCOMP(A); + DD r = visited->get_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<int> &vars) +{ + int *index = new int[varCount+1]; + for(int i=0; i<varCount+1; i++){ + index[i] = 0; + } + //---------------------------------- + XBits bits; + bits.set_size(NodeCount()); + + XVector<DD> one; + XVector<DD> two; + one.push_back(dd); + XVector<DD> *cur = &one; + XVector<DD> *nex = &two; + while(cur->size() > 0){ + for(int i=0; i<cur->size(); 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<DD> *tmp = cur; + cur = nex; + nex = tmp; + nex->clear(); + } + //---------------------------------- + for(int i=1; i<varCount+1; i++){ + if(index[i] == 1) vars.push_back(i); + } + delete []index; +} + +DD XManager::Restrict(DD F, DD C) +{ + if (C == One) return F; + if (C == Zero) return Zero; + if ((F == One)||(F == Zero)) return F; + if (F == C) return One; + if (F == !C) return Zero; + + DD r; + bool b = CTable->Find(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<int> &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<int> levelOne; + XVector<int> levelTwo; + XVector<int> *curLevel = &levelOne; + XVector<int> *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; i<curLevel->size(); 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<tvar; k++){ + path.push_back(k); + } + } + else if(ADDR(nodes[pId].Else) == i){ + int fvar = nodes[pId].var; + int tvar = (i==0)?(varCount+1):nodes[i].var; + for(int k=fvar+1; k<tvar; k++){ + path.push_back(k); + } + } + i = pId; + } + for(int k=1; k<nodes[ADDR(from)].var; k++){ + path.push_back(k); + } + delete []ps; + delete []inIds; + + return (int)path.size(); +} + +int XManager::DeadCount() +{ + char *c = new char[NodeCount()]; + memset(c, 0, NodeCount()); + + set<void *>::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<NodeCount(); i++){ + if(c[i] == 0){ + zeroCnt++; + } + } + + delete []c; + return zeroCnt; +} + +void XManager::GarbageCollection() +{ + char *c = new char[NodeCount()]; + memset(c, 0, NodeCount()); + for(int i=0; i<=varCount; i++) c[i] = 1; + vector<DD> exDDs; + + set<void *>::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; i<NodeCount(); i++){ + ds[i] = i; + } + int curDead = varCount+1; + int curLive = varCount+1; + int newcount; + + for(int i = varCount+1; i<NodeCount(); i++){ + if(c[i] == 1){ + newcount = i; + for(int k=curDead; k<i; k++){ + if(c[k] == 0){ + ds[i] = k; + nodes[k] = nodes[i]; + c[i] = 0; + c[k] = 1; + curDead = k+1; + newcount = k+1; + break; + } + } + } + } + + for(int i = varCount+1; i<NodeCount(); i++){ + nodes[i].Then = ds[nodes[i].Then]; + + bool iscomp = false; + if(ISCOMP(nodes[i].Else)) iscomp = true; + + nodes[i].Else = ds[ADDR(nodes[i].Else)]; + if(iscomp){ + nodes[i].Else = Not(nodes[i].Else); + } + } + + it = externalBDDs.begin(); + for(; it != externalBDDs.end(); it++){ + BDD *b = (BDD *)*it; + + if(b->IsComp()){ + 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<<node->var<<", Then:"<<node->Then<<",Else:"<<ADDR(node->Else)<<",Next:"<<node->Next<<endl; +} + +void XManager::ShowInfo(double vtime) +{ + double mem = (20.0*(NodeCount() + GetCacheCount()) + 4.0*GetUTableCount()) / ONE_MILLION; + cout<<"NC:"<<GetNodeCount()<<", CC:"<<GetCacheCount()<<", Mem:"<<mem<<", Hit:"<<CTable->HitRate()<<", Time:"<<vtime<<endl; + cout<<"==============================================================================="<<endl; +} + +void XManager::ShowInfoToFile(const char *filename) +{ + static double startTime = Timer::GetTime(); + double diff = Timer::GetTime() - startTime; + double mem = (20.0*(NodeCount() + GetCacheCount()) + 4.0*GetUTableCount()) / ONE_MILLION; + + fstream fs; + fs.open(filename, ios::out | ios::app); + + fs<<" NC:"<<XFunction::Format(NodeCount(),10); + fs<<", CC:"<<XFunction::Format(GetCacheCount() / ONE_MILLION, 6); + fs<<", Mem:"<<XFunction::Format(mem,10); + fs<<", Hit:"<<XFunction::Format(Get_CTable_HitRate(),10,3); + fs<<", Time:"<<XFunction::Format(diff,10,3); + + fs<<endl; + + fs.close(); +} + +void XManager::ShowInfoToFile(const char *filename, const string &info) +{ + fstream fs; + fs.open(filename, ios::out | ios::app); + fs<<info<<endl; + fs.close(); +}
+ cpp/Manager.h view
@@ -0,0 +1,232 @@+/***************************************************************************** +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 _MANAGER_ +#define _MANAGER_ + +#include "UTable.h" +#include "CTable.h" +#include "XVector.h" +#include "XBits.h" +#include "XInts.h" +#include <limits.h> +#include <vector> +#include <set> +//#include <sys/sysinfo.h> +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<void *> 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<DD> dds); + DD Or(const XVector<DD> 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<int> &vars); + + int VarDistanceOf(DD A, DD B); + int LargestPath(DD from, vector<int> &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
+ cpp/OriginalMakefile view
@@ -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~+#------------------------------------------------------
+ cpp/README view
@@ -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
+ cpp/Timer.h view
@@ -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 <time.h> +#else + #include <sys/time.h> + #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
+ cpp/UTable.cpp view
@@ -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 <cmath> +#include <iostream> +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; i<mgr->NodeCount(); 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; i<mgr->NodeCount(); 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<count; i++){ + if(items[i] > 0) c++; + } + return (1.0 * mgr->NodeCount() / c); +}
+ cpp/UTable.h view
@@ -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
+ cpp/XBits.h view
@@ -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 <memory.h> + +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
+ cpp/XFunction.h view
@@ -0,0 +1,83 @@+ +#ifndef _FUNCTION_ +#define _FUNCTION_ + +#include <stdio.h> +#include <cmath> +#include <iostream> +#include <string> +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<outlen-k; i++){ + r = r+' '; + } + return r; + } + + static string Format(long long v, int outlen) + { + char buf[50]; + memset(buf, 0, 50); + sprintf(buf, "%lld", v); + string r = buf; + size_t k = r.length(); + for(int i=0; i<outlen-k; i++){ + r = r+' '; + } + return r; + } + + static string Format(double v, int outlen, int dotlen = 2) + { + v = format_double(v, dotlen); + char buf[50]; + memset(buf, 0, 50); + sprintf(buf, "%f", v); + string r = buf; + int k = (int)r.length(); + for(int i=0; i<outlen-k; i++){ + r = r+' '; + } + return r; + } + + static string Format(const char *v, int slen, int outlen) + { + if(outlen < slen){ outlen = slen; } + + string r = v; + for(int i=0; i<outlen - slen; i++){ + r = r + ' '; + } + return r; + } +}; + +#endif
+ cpp/XInts.h view
@@ -0,0 +1,104 @@+/***************************************************************************** +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 __XINTS__ +#define __XINTS__ + +#include <memory.h> +#include <iostream> +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
+ cpp/XVector.h view
@@ -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 <stdlib.h> +#include <new> +using namespace std; + +template <class T> class XVector +{ +private: + int _size; + int _capacity; + +public: + T * data; + + T& operator[] (int index) const; + XVector<T>& operator = (const XVector<T>& 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<T>& other); + XVector(int size); + ~XVector(); +}; + +template<class T> XVector<T>::XVector() +{ + data = NULL; + _size = 0; + _capacity = 0; +} + +template<class T> XVector<T>::XVector(int vSize) +{ + init(vSize); +} + +template<class T> void XVector<T>::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<class T> void XVector<T>::resize(int vSize) +{ + if(vSize > _size){ + for(int i=_size; i<vSize; i++){ + T t; + push_back(t); + } + _size = vSize; + } + else if(vSize < _size){ + for(int i=0; i<_size - vSize; i++){ + pop_back(); + } + _size = vSize; + } +} + +template<class T> XVector<T>::XVector(XVector<T>& other) +{ + data = NULL; + data = (T*)realloc(data, other.size() * sizeof(T)); + + for(int i=0;i<other.size();i++){ + data[i] = other.data[i]; + } + _size = other.size(); + _capacity = _size; +} + +template<class T> XVector<T>::~XVector() +{ + clear(); +} + +template<class T> inline void XVector<T>::clear() +{ + if (data != 0) + { + for (int i = 0; i < _size; i++) + { + data[i].~T(); + + } + _size = 0; + free(data); + data = 0; + _capacity = 0; + } +} + +template<class T> inline int XVector<T>::capacity() +{ + return _capacity; +} + +template<class T> inline void XVector<T>::shrink() +{ + _capacity = _size; + data = (T*)realloc(data, _capacity * sizeof(T)); +} + +template<class T> inline void XVector<T>::expand(int cnt) +{ + _capacity += cnt; + data = (T*)realloc(data, _capacity * sizeof(T)); +} + +template<class T> void XVector<T>::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; + } + } +} + +template<class T>inline void XVector<T>::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; + } + } +} + +template<class T>inline void XVector<T>::erase(int index) +{ + if(index == _size-1) pop_back(); + else + { + data[index].~T(); + data[index] = data[_size-1]; + data[_size-1].~T(); + _size--; + } +} + +template<class T>inline void XVector<T>::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<class T> inline void XVector<T>::pop_back() +{ + if(_size > 0){ + _size--; + data[_size].~T(); + } +} + +template<class T>inline T& XVector<T>::operator[] (int index) const +{ + return data[index]; +} + +template<class T>inline XVector<T>& XVector<T>::operator = (const XVector<T>& other) +{ + if(size() > 0) clear(); + data = 0; + if(_capacity < other.size()) data = (T*)malloc(other.size() * sizeof(T)); + + for(int i=0; i<other.size(); i++){ + data[i] = other.data[i]; + } + + _size = other.size(); + _capacity = _size; + + return *this; +} + +template<class T>inline T& XVector<T>::back() +{ + return data[_size-1]; +} + +template<class T> inline int XVector<T>::find(T &x) +{ + for (int i = 0; i < _size; i++) { + if (data[i] == x) return i; + } + return -1; +} + +#endif
+ cpp/main.cpp view
@@ -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"<<endl; + else cout<<"not equal to one"<<endl; + + mgr.ShowInfo(); + + delete []x; + + return 0; +}
+ hs/Data/HasCacBDD.hs view
@@ -0,0 +1,428 @@+-- | Haskell bindings for CacBDD, a BDD Package with Dynamic Cache Management.++{-# LANGUAGE ForeignFunctionInterface #-}+module Data.HasCacBDD (+ -- * Types+ Bdd, Assignment,+ -- * Creation of new BDDs+ top, bot, var,+ -- * Combination and Manipulation of BDDs+ neg, con, dis, imp, equ, xor, conSet, disSet, xorSet,+ exists, forall, forallSet, existsSet,+ restrict, restrictSet, restrictLaw,+ ifthenelse, gfp, relabel,+ -- * Evaluation+ evaluate, evaluateFun,+ -- * Get satisfying assignments+ allSats, allSatsWith, satCountWith, anySat, anySatWith,+ -- * Variables+ firstVarOf, maxVarOf, allVarsOf, allVarsOfSorted,+ -- * Sub-BDDs and length+ thenOf, elseOf, subsOf, sizeOf,+ -- * Show and convert to trees+ BddTree(..), unravel, ravel,+ -- * Print some debugging information+ maximumvar, showInfo+) where++import Foreign.C+import Foreign.Ptr (Ptr)+import Foreign (ForeignPtr, newForeignPtr, withForeignPtr, finalizerFree)+import System.IO.Unsafe+import Data.List (nub,(\\),sort)+import Data.Maybe (fromJust)+import Test.QuickCheck (Arbitrary, Gen, arbitrary, choose, oneof, sized, listOf)++-- | The CacBDD datatype has no structure because+-- from our perspective BDDs are just pointers.+newtype Bdd = Bdd (ForeignPtr CacBDD)+type CacBDD = ()++-- | An assignment of boolean values to variables/integers.+type Assignment = [(Int,Bool)]++-- | We attach the free() finalizer to our BDDs.+finalize :: Ptr CacBDD -> 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)
+ hs/Data/HasCacBDD/Visuals.hs view
@@ -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
+ stack.yaml view
@@ -0,0 +1,3 @@+resolver: lts-8.0+packages:+- '.'
+ tests/Basics.hs view
@@ -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")+ ]
+ tests/Example.hs view
@@ -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
+ tests/Tautologies.hs view
@@ -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))))+ ]