diff options
87 files changed, 9051 insertions, 0 deletions
@@ -0,0 +1,674 @@ + GNU GENERAL PUBLIC LICENSE + Version 3, 29 June 2007 + + Copyright (C) 2007 Free Software Foundation, Inc. <http://fsf.org/> + Everyone is permitted to copy and distribute verbatim copies + of this license document, but changing it is not allowed. + + Preamble + + The GNU General Public License is a free, copyleft license for +software and other kinds of works. + + The licenses for most software and other practical works are designed +to take away your freedom to share and change the works. By contrast, +the GNU General Public License is intended to guarantee your freedom to +share and change all versions of a program--to make sure it remains free +software for all its users. We, the Free Software Foundation, use the +GNU General Public License for most of our software; it applies also to +any other work released this way by its authors. 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 +them 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 prevent others from denying you +these rights or asking you to surrender the rights. Therefore, you have +certain responsibilities if you distribute copies of the software, or if +you modify it: responsibilities to respect the freedom of others. + + For example, if you distribute copies of such a program, whether +gratis or for a fee, you must pass on to the recipients the same +freedoms that you received. 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. + + Developers that use the GNU GPL protect your rights with two steps: +(1) assert copyright on the software, and (2) offer you this License +giving you legal permission to copy, distribute and/or modify it. + + For the developers' and authors' protection, the GPL clearly explains +that there is no warranty for this free software. For both users' and +authors' sake, the GPL requires that modified versions be marked as +changed, so that their problems will not be attributed erroneously to +authors of previous versions. + + Some devices are designed to deny users access to install or run +modified versions of the software inside them, although the manufacturer +can do so. This is fundamentally incompatible with the aim of +protecting users' freedom to change the software. The systematic +pattern of such abuse occurs in the area of products for individuals to +use, which is precisely where it is most unacceptable. Therefore, we +have designed this version of the GPL to prohibit the practice for those +products. If such problems arise substantially in other domains, we +stand ready to extend this provision to those domains in future versions +of the GPL, as needed to protect the freedom of users. + + Finally, every program is threatened constantly by software patents. +States should not allow patents to restrict development and use of +software on general-purpose computers, but in those that do, we wish to +avoid the special danger that patents applied to a free program could +make it effectively proprietary. To prevent this, the GPL assures that +patents cannot be used to render the program non-free. + + The precise terms and conditions for copying, distribution and +modification follow. + + TERMS AND CONDITIONS + + 0. Definitions. + + "This License" refers to version 3 of the GNU General Public License. + + "Copyright" also means copyright-like laws that apply to other kinds of +works, such as semiconductor masks. + + "The Program" refers to any copyrightable work licensed under this +License. Each licensee is addressed as "you". "Licensees" and +"recipients" may be individuals or organizations. + + To "modify" a work means to copy from or adapt all or part of the work +in a fashion requiring copyright permission, other than the making of an +exact copy. The resulting work is called a "modified version" of the +earlier work or a work "based on" the earlier work. + + A "covered work" means either the unmodified Program or a work based +on the Program. + + To "propagate" a work means to do anything with it that, without +permission, would make you directly or secondarily liable for +infringement under applicable copyright law, except executing it on a +computer or modifying a private copy. Propagation includes copying, +distribution (with or without modification), making available to the +public, and in some countries other activities as well. + + To "convey" a work means any kind of propagation that enables other +parties to make or receive copies. Mere interaction with a user through +a computer network, with no transfer of a copy, is not conveying. + + An interactive user interface displays "Appropriate Legal Notices" +to the extent that it includes a convenient and prominently visible +feature that (1) displays an appropriate copyright notice, and (2) +tells the user that there is no warranty for the work (except to the +extent that warranties are provided), that licensees may convey the +work under this License, and how to view a copy of this License. If +the interface presents a list of user commands or options, such as a +menu, a prominent item in the list meets this criterion. + + 1. Source Code. + + The "source code" for a work means the preferred form of the work +for making modifications to it. "Object code" means any non-source +form of a work. + + A "Standard Interface" means an interface that either is an official +standard defined by a recognized standards body, or, in the case of +interfaces specified for a particular programming language, one that +is widely used among developers working in that language. + + The "System Libraries" of an executable work include anything, other +than the work as a whole, that (a) is included in the normal form of +packaging a Major Component, but which is not part of that Major +Component, and (b) serves only to enable use of the work with that +Major Component, or to implement a Standard Interface for which an +implementation is available to the public in source code form. A +"Major Component", in this context, means a major essential component +(kernel, window system, and so on) of the specific operating system +(if any) on which the executable work runs, or a compiler used to +produce the work, or an object code interpreter used to run it. + + The "Corresponding Source" for a work in object code form means all +the source code needed to generate, install, and (for an executable +work) run the object code and to modify the work, including scripts to +control those activities. However, it does not include the work's +System Libraries, or general-purpose tools or generally available free +programs which are used unmodified in performing those activities but +which are not part of the work. For example, Corresponding Source +includes interface definition files associated with source files for +the work, and the source code for shared libraries and dynamically +linked subprograms that the work is specifically designed to require, +such as by intimate data communication or control flow between those +subprograms and other parts of the work. + + The Corresponding Source need not include anything that users +can regenerate automatically from other parts of the Corresponding +Source. + + The Corresponding Source for a work in source code form is that +same work. + + 2. Basic Permissions. + + All rights granted under this License are granted for the term of +copyright on the Program, and are irrevocable provided the stated +conditions are met. This License explicitly affirms your unlimited +permission to run the unmodified Program. The output from running a +covered work is covered by this License only if the output, given its +content, constitutes a covered work. This License acknowledges your +rights of fair use or other equivalent, as provided by copyright law. + + You may make, run and propagate covered works that you do not +convey, without conditions so long as your license otherwise remains +in force. You may convey covered works to others for the sole purpose +of having them make modifications exclusively for you, or provide you +with facilities for running those works, provided that you comply with +the terms of this License in conveying all material for which you do +not control copyright. Those thus making or running the covered works +for you must do so exclusively on your behalf, under your direction +and control, on terms that prohibit them from making any copies of +your copyrighted material outside their relationship with you. + + Conveying under any other circumstances is permitted solely under +the conditions stated below. Sublicensing is not allowed; section 10 +makes it unnecessary. + + 3. Protecting Users' Legal Rights From Anti-Circumvention Law. + + No covered work shall be deemed part of an effective technological +measure under any applicable law fulfilling obligations under article +11 of the WIPO copyright treaty adopted on 20 December 1996, or +similar laws prohibiting or restricting circumvention of such +measures. + + When you convey a covered work, you waive any legal power to forbid +circumvention of technological measures to the extent such circumvention +is effected by exercising rights under this License with respect to +the covered work, and you disclaim any intention to limit operation or +modification of the work as a means of enforcing, against the work's +users, your or third parties' legal rights to forbid circumvention of +technological measures. + + 4. Conveying Verbatim Copies. + + You may convey 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; +keep intact all notices stating that this License and any +non-permissive terms added in accord with section 7 apply to the code; +keep intact all notices of the absence of any warranty; and give all +recipients a copy of this License along with the Program. + + You may charge any price or no price for each copy that you convey, +and you may offer support or warranty protection for a fee. + + 5. Conveying Modified Source Versions. + + You may convey a work based on the Program, or the modifications to +produce it from the Program, in the form of source code under the +terms of section 4, provided that you also meet all of these conditions: + + a) The work must carry prominent notices stating that you modified + it, and giving a relevant date. + + b) The work must carry prominent notices stating that it is + released under this License and any conditions added under section + 7. This requirement modifies the requirement in section 4 to + "keep intact all notices". + + c) You must license the entire work, as a whole, under this + License to anyone who comes into possession of a copy. This + License will therefore apply, along with any applicable section 7 + additional terms, to the whole of the work, and all its parts, + regardless of how they are packaged. This License gives no + permission to license the work in any other way, but it does not + invalidate such permission if you have separately received it. + + d) If the work has interactive user interfaces, each must display + Appropriate Legal Notices; however, if the Program has interactive + interfaces that do not display Appropriate Legal Notices, your + work need not make them do so. + + A compilation of a covered work with other separate and independent +works, which are not by their nature extensions of the covered work, +and which are not combined with it such as to form a larger program, +in or on a volume of a storage or distribution medium, is called an +"aggregate" if the compilation and its resulting copyright are not +used to limit the access or legal rights of the compilation's users +beyond what the individual works permit. Inclusion of a covered work +in an aggregate does not cause this License to apply to the other +parts of the aggregate. + + 6. Conveying Non-Source Forms. + + You may convey a covered work in object code form under the terms +of sections 4 and 5, provided that you also convey the +machine-readable Corresponding Source under the terms of this License, +in one of these ways: + + a) Convey the object code in, or embodied in, a physical product + (including a physical distribution medium), accompanied by the + Corresponding Source fixed on a durable physical medium + customarily used for software interchange. + + b) Convey the object code in, or embodied in, a physical product + (including a physical distribution medium), accompanied by a + written offer, valid for at least three years and valid for as + long as you offer spare parts or customer support for that product + model, to give anyone who possesses the object code either (1) a + copy of the Corresponding Source for all the software in the + product that is covered by this License, on a durable physical + medium customarily used for software interchange, for a price no + more than your reasonable cost of physically performing this + conveying of source, or (2) access to copy the + Corresponding Source from a network server at no charge. + + c) Convey individual copies of the object code with a copy of the + written offer to provide the Corresponding Source. This + alternative is allowed only occasionally and noncommercially, and + only if you received the object code with such an offer, in accord + with subsection 6b. + + d) Convey the object code by offering access from a designated + place (gratis or for a charge), and offer equivalent access to the + Corresponding Source in the same way through the same place at no + further charge. You need not require recipients to copy the + Corresponding Source along with the object code. If the place to + copy the object code is a network server, the Corresponding Source + may be on a different server (operated by you or a third party) + that supports equivalent copying facilities, provided you maintain + clear directions next to the object code saying where to find the + Corresponding Source. Regardless of what server hosts the + Corresponding Source, you remain obligated to ensure that it is + available for as long as needed to satisfy these requirements. + + e) Convey the object code using peer-to-peer transmission, provided + you inform other peers where the object code and Corresponding + Source of the work are being offered to the general public at no + charge under subsection 6d. + + A separable portion of the object code, whose source code is excluded +from the Corresponding Source as a System Library, need not be +included in conveying the object code work. + + A "User Product" is either (1) a "consumer product", which means any +tangible personal property which is normally used for personal, family, +or household purposes, or (2) anything designed or sold for incorporation +into a dwelling. In determining whether a product is a consumer product, +doubtful cases shall be resolved in favor of coverage. For a particular +product received by a particular user, "normally used" refers to a +typical or common use of that class of product, regardless of the status +of the particular user or of the way in which the particular user +actually uses, or expects or is expected to use, the product. A product +is a consumer product regardless of whether the product has substantial +commercial, industrial or non-consumer uses, unless such uses represent +the only significant mode of use of the product. + + "Installation Information" for a User Product means any methods, +procedures, authorization keys, or other information required to install +and execute modified versions of a covered work in that User Product from +a modified version of its Corresponding Source. The information must +suffice to ensure that the continued functioning of the modified object +code is in no case prevented or interfered with solely because +modification has been made. + + If you convey an object code work under this section in, or with, or +specifically for use in, a User Product, and the conveying occurs as +part of a transaction in which the right of possession and use of the +User Product is transferred to the recipient in perpetuity or for a +fixed term (regardless of how the transaction is characterized), the +Corresponding Source conveyed under this section must be accompanied +by the Installation Information. But this requirement does not apply +if neither you nor any third party retains the ability to install +modified object code on the User Product (for example, the work has +been installed in ROM). + + The requirement to provide Installation Information does not include a +requirement to continue to provide support service, warranty, or updates +for a work that has been modified or installed by the recipient, or for +the User Product in which it has been modified or installed. Access to a +network may be denied when the modification itself materially and +adversely affects the operation of the network or violates the rules and +protocols for communication across the network. + + Corresponding Source conveyed, and Installation Information provided, +in accord with this section must be in a format that is publicly +documented (and with an implementation available to the public in +source code form), and must require no special password or key for +unpacking, reading or copying. + + 7. Additional Terms. + + "Additional permissions" are terms that supplement the terms of this +License by making exceptions from one or more of its conditions. +Additional permissions that are applicable to the entire Program shall +be treated as though they were included in this License, to the extent +that they are valid under applicable law. If additional permissions +apply only to part of the Program, that part may be used separately +under those permissions, but the entire Program remains governed by +this License without regard to the additional permissions. + + When you convey a copy of a covered work, you may at your option +remove any additional permissions from that copy, or from any part of +it. (Additional permissions may be written to require their own +removal in certain cases when you modify the work.) You may place +additional permissions on material, added by you to a covered work, +for which you have or can give appropriate copyright permission. + + Notwithstanding any other provision of this License, for material you +add to a covered work, you may (if authorized by the copyright holders of +that material) supplement the terms of this License with terms: + + a) Disclaiming warranty or limiting liability differently from the + terms of sections 15 and 16 of this License; or + + b) Requiring preservation of specified reasonable legal notices or + author attributions in that material or in the Appropriate Legal + Notices displayed by works containing it; or + + c) Prohibiting misrepresentation of the origin of that material, or + requiring that modified versions of such material be marked in + reasonable ways as different from the original version; or + + d) Limiting the use for publicity purposes of names of licensors or + authors of the material; or + + e) Declining to grant rights under trademark law for use of some + trade names, trademarks, or service marks; or + + f) Requiring indemnification of licensors and authors of that + material by anyone who conveys the material (or modified versions of + it) with contractual assumptions of liability to the recipient, for + any liability that these contractual assumptions directly impose on + those licensors and authors. + + All other non-permissive additional terms are considered "further +restrictions" within the meaning of section 10. If the Program as you +received it, or any part of it, contains a notice stating that it is +governed by this License along with a term that is a further +restriction, you may remove that term. If a license document contains +a further restriction but permits relicensing or conveying under this +License, you may add to a covered work material governed by the terms +of that license document, provided that the further restriction does +not survive such relicensing or conveying. + + If you add terms to a covered work in accord with this section, you +must place, in the relevant source files, a statement of the +additional terms that apply to those files, or a notice indicating +where to find the applicable terms. + + Additional terms, permissive or non-permissive, may be stated in the +form of a separately written license, or stated as exceptions; +the above requirements apply either way. + + 8. Termination. + + You may not propagate or modify a covered work except as expressly +provided under this License. Any attempt otherwise to propagate or +modify it is void, and will automatically terminate your rights under +this License (including any patent licenses granted under the third +paragraph of section 11). + + However, if you cease all violation of this License, then your +license from a particular copyright holder is reinstated (a) +provisionally, unless and until the copyright holder explicitly and +finally terminates your license, and (b) permanently, if the copyright +holder fails to notify you of the violation by some reasonable means +prior to 60 days after the cessation. + + Moreover, your license from a particular copyright holder is +reinstated permanently if the copyright holder notifies you of the +violation by some reasonable means, this is the first time you have +received notice of violation of this License (for any work) from that +copyright holder, and you cure the violation prior to 30 days after +your receipt of the notice. + + Termination of your rights under this section does not terminate the +licenses of parties who have received copies or rights from you under +this License. If your rights have been terminated and not permanently +reinstated, you do not qualify to receive new licenses for the same +material under section 10. + + 9. Acceptance Not Required for Having Copies. + + You are not required to accept this License in order to receive or +run a copy of the Program. Ancillary propagation of a covered work +occurring solely as a consequence of using peer-to-peer transmission +to receive a copy likewise does not require acceptance. However, +nothing other than this License grants you permission to propagate or +modify any covered work. These actions infringe copyright if you do +not accept this License. Therefore, by modifying or propagating a +covered work, you indicate your acceptance of this License to do so. + + 10. Automatic Licensing of Downstream Recipients. + + Each time you convey a covered work, the recipient automatically +receives a license from the original licensors, to run, modify and +propagate that work, subject to this License. You are not responsible +for enforcing compliance by third parties with this License. + + An "entity transaction" is a transaction transferring control of an +organization, or substantially all assets of one, or subdividing an +organization, or merging organizations. If propagation of a covered +work results from an entity transaction, each party to that +transaction who receives a copy of the work also receives whatever +licenses to the work the party's predecessor in interest had or could +give under the previous paragraph, plus a right to possession of the +Corresponding Source of the work from the predecessor in interest, if +the predecessor has it or can get it with reasonable efforts. + + You may not impose any further restrictions on the exercise of the +rights granted or affirmed under this License. For example, you may +not impose a license fee, royalty, or other charge for exercise of +rights granted under this License, and you may not initiate litigation +(including a cross-claim or counterclaim in a lawsuit) alleging that +any patent claim is infringed by making, using, selling, offering for +sale, or importing the Program or any portion of it. + + 11. Patents. + + A "contributor" is a copyright holder who authorizes use under this +License of the Program or a work on which the Program is based. The +work thus licensed is called the contributor's "contributor version". + + A contributor's "essential patent claims" are all patent claims +owned or controlled by the contributor, whether already acquired or +hereafter acquired, that would be infringed by some manner, permitted +by this License, of making, using, or selling its contributor version, +but do not include claims that would be infringed only as a +consequence of further modification of the contributor version. For +purposes of this definition, "control" includes the right to grant +patent sublicenses in a manner consistent with the requirements of +this License. + + Each contributor grants you a non-exclusive, worldwide, royalty-free +patent license under the contributor's essential patent claims, to +make, use, sell, offer for sale, import and otherwise run, modify and +propagate the contents of its contributor version. + + In the following three paragraphs, a "patent license" is any express +agreement or commitment, however denominated, not to enforce a patent +(such as an express permission to practice a patent or covenant not to +sue for patent infringement). To "grant" such a patent license to a +party means to make such an agreement or commitment not to enforce a +patent against the party. + + If you convey a covered work, knowingly relying on a patent license, +and the Corresponding Source of the work is not available for anyone +to copy, free of charge and under the terms of this License, through a +publicly available network server or other readily accessible means, +then you must either (1) cause the Corresponding Source to be so +available, or (2) arrange to deprive yourself of the benefit of the +patent license for this particular work, or (3) arrange, in a manner +consistent with the requirements of this License, to extend the patent +license to downstream recipients. "Knowingly relying" means you have +actual knowledge that, but for the patent license, your conveying the +covered work in a country, or your recipient's use of the covered work +in a country, would infringe one or more identifiable patents in that +country that you have reason to believe are valid. + + If, pursuant to or in connection with a single transaction or +arrangement, you convey, or propagate by procuring conveyance of, a +covered work, and grant a patent license to some of the parties +receiving the covered work authorizing them to use, propagate, modify +or convey a specific copy of the covered work, then the patent license +you grant is automatically extended to all recipients of the covered +work and works based on it. + + A patent license is "discriminatory" if it does not include within +the scope of its coverage, prohibits the exercise of, or is +conditioned on the non-exercise of one or more of the rights that are +specifically granted under this License. You may not convey a covered +work if you are a party to an arrangement with a third party that is +in the business of distributing software, under which you make payment +to the third party based on the extent of your activity of conveying +the work, and under which the third party grants, to any of the +parties who would receive the covered work from you, a discriminatory +patent license (a) in connection with copies of the covered work +conveyed by you (or copies made from those copies), or (b) primarily +for and in connection with specific products or compilations that +contain the covered work, unless you entered into that arrangement, +or that patent license was granted, prior to 28 March 2007. + + Nothing in this License shall be construed as excluding or limiting +any implied license or other defenses to infringement that may +otherwise be available to you under applicable patent law. + + 12. No Surrender of Others' Freedom. + + If 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 convey a +covered work so as to satisfy simultaneously your obligations under this +License and any other pertinent obligations, then as a consequence you may +not convey it at all. For example, if you agree to terms that obligate you +to collect a royalty for further conveying from those to whom you convey +the Program, the only way you could satisfy both those terms and this +License would be to refrain entirely from conveying the Program. + + 13. Use with the GNU Affero General Public License. + + Notwithstanding any other provision of this License, you have +permission to link or combine any covered work with a work licensed +under version 3 of the GNU Affero General Public License into a single +combined work, and to convey the resulting work. The terms of this +License will continue to apply to the part which is the covered work, +but the special requirements of the GNU Affero General Public License, +section 13, concerning interaction through a network will apply to the +combination as such. + + 14. Revised Versions of this License. + + The Free Software Foundation may publish revised and/or new versions of +the GNU 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 that a certain numbered version of the GNU General +Public License "or any later version" applies to it, you have the +option of following the terms and conditions either of that numbered +version or of any later version published by the Free Software +Foundation. If the Program does not specify a version number of the +GNU General Public License, you may choose any version ever published +by the Free Software Foundation. + + If the Program specifies that a proxy can decide which future +versions of the GNU General Public License can be used, that proxy's +public statement of acceptance of a version permanently authorizes you +to choose that version for the Program. + + Later license versions may give you additional or different +permissions. However, no additional obligations are imposed on any +author or copyright holder as a result of your choosing to follow a +later version. + + 15. Disclaimer of Warranty. + + 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. + + 16. Limitation of Liability. + + IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGREED TO IN WRITING +WILL ANY COPYRIGHT HOLDER, OR ANY OTHER PARTY WHO MODIFIES AND/OR CONVEYS +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. + + 17. Interpretation of Sections 15 and 16. + + If the disclaimer of warranty and limitation of liability provided +above cannot be given local legal effect according to their terms, +reviewing courts shall apply local law that most closely approximates +an absolute waiver of all civil liability in connection with the +Program, unless a warranty or assumption of liability accompanies a +copy of the Program in return for a fee. + + 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 +state the exclusion of warranty; and each file should have at least +the "copyright" line and a pointer to where the full notice is found. + + <one line to give the program's name and a brief idea of what it does.> + Copyright (C) <year> <name of author> + + 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 3 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, see <http://www.gnu.org/licenses/>. + +Also add information on how to contact you by electronic and paper mail. + + If the program does terminal interaction, make it output a short +notice like this when it starts in an interactive mode: + + <program> Copyright (C) <year> <name of author> + This program 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, your program's commands +might be different; for a GUI interface, you would use an "about box". + + You should also get your employer (if you work as a programmer) or school, +if any, to sign a "copyright disclaimer" for the program, if necessary. +For more information on this, and how to apply and follow the GNU GPL, see +<http://www.gnu.org/licenses/>. + + The GNU 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. But first, please read +<http://www.gnu.org/philosophy/why-not-lgpl.html>. diff --git a/Makefile b/Makefile new file mode 100644 index 0000000..6589e93 --- /dev/null +++ b/Makefile @@ -0,0 +1,70 @@ +# The target +TARGET = casa-1.1b + +# The compiler options +CC = g++ +CFLAGS = \ + -Wredundant-decls -Wall -Werror -g \ + -Icasa -Icommon -Icommon/utility -Iminisat/solver -Iminisat/include \ + -DSEARCH_PROGRESS +LFLAGS = +DFLAGS = -MM + +#the .C files, without their extensions +COMBINATORICS_SOURCES = PascalTriangle Combinadic CombinadicIterator +MINISAT_SOURCES = Solver +SAT_SOURCES = SAT +IO_SOURCES = Usage SpecificationFile ConstraintFile OutputFile +STATE_SOURCES = CoveringArray CoveringArrayEntry CoveringArrayRow CoveringArraySubRow +SPACE_SOURCES = CoveringArraySpace SingleChangeSpace GraftSpace +BOOKKEEPING_SOURCES = Options +ANNEALING_SOURCES = Anneal AnnealingSuccess Bounds AnnealingPartitioner +ALGORITHM_SOURCES = BinarySearch +MAIN_SOURCES = Main +SOURCES = \ + $(COMBINATORICS_SOURCES:%=common/utility/%) \ + $(MINISAT_SOURCES:%=minisat/solver/%) \ + $(SAT_SOURCES:%=casa/sat/%) \ + $(IO_SOURCES:%=casa/io/%) \ + $(STATE_SOURCES:%=casa/covering/state/%) \ + $(SPACE_SOURCES:%=casa/covering/space/%) \ + $(BOOKKEEPING_SOURCES:%=casa/covering/bookkeeping/%) \ + $(ANNEALING_SOURCES:%=casa/annealing/%) \ + $(ALGORITHM_SOURCES:%=casa/algorithms/%) \ + $(MAIN_SOURCES:%=casa/%) + +# The rules +all: $(TARGET) TAGS + +$(TARGET): $(SOURCES:%=%.o) + $(CC) -o $@ $(filter %.o,$^) $(LFLAGS) + +$(SOURCES:%=%.o): Makefile + $(CC) -c -o $@ $(@:%.o=%.C) $(CFLAGS) + +$(SOURCES:%=%.d): %.d:%.C Makefile + $(CC) $(DFLAGS) $(@:%.d=%.C) $(CFLAGS) | sed 's,.*\.o:,$(@:%.d=%.o) $@: ,g' > $@ +ifneq ($(MAKECMDGOALS),clean) +ifneq ($(MAKECMDGOALS),distclean) +-include $(SOURCES:%=%.d) +endif +endif + +Dependencies: $(SOURCES:%=%.d) + sed -e 's/://g' -e 's/[^ ][^ ]*\.d//g' -e 's/[^ ][^ ]*\.o//g' -e 's/[ \\][ \\]*/ /g' $(SOURCES:%=%.d) | tr ' ' "\n" | sort | uniq | tr "\n" ' ' | sed 's/^/ALL_INPUTS =/' > $@ +ifneq ($(MAKECMDGOALS),clean) +ifneq ($(MAKECMDGOALS),distclean) +-include Dependencies +endif +endif + +TAGS: $(ALL_INPUTS) + etags $^ + +clean: + -$(RM) $(TARGET) $(SOURCES:%=%.o) + +distclean: clean + -$(RM) $(SOURCES:%=%.d) Dependencies TAGS + +.PHONY: all clean distclean diff --git a/casa/Main.C b/casa/Main.C new file mode 100644 index 0000000..63e7859 --- /dev/null +++ b/casa/Main.C @@ -0,0 +1,80 @@ +// Copyright 2008, 2009 Brady J. Garvin + +// This file is part of Covering Arrays by Simulated Annealing (CASA). + +// CASA 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 3 of the License, or +// (at your option) any later version. + +// CASA 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 CASA. If not, see <http://www.gnu.org/licenses/>. + + +#include <cstdlib> +#include <ctime> +#include <iostream> +#include <sstream> + +#include "io/Usage.H" +#include "io/SpecificationFile.H" +#include "io/ConstraintFile.H" +#include "io/OutputFile.H" + +#include "covering/state/CoveringArray.H" + +#include "annealing/Anneal.H" + +using namespace std; + +int main(int argc, char**argv) { + // Absorb the command line arguments into shared variables. + parseOptions(argc, argv); + // Process the random seed. + if (!seeded) { + seed = time(NULL); + cout << "Choosing random seed " << seed << endl; + } + srand(seed); + // Process the specification file. + SpecificationFile specification(modelFile); + // Process the constraints file. + ConstraintFile constraints(constraintFile ? constraintFile : ""); + // ready the output file + ostringstream defaultOutputFile("anneal", ios::out | ios::app); + if (!outputFile) { + defaultOutputFile << '.' << seed; + defaultOutputFile << ".out"; + cout << "Using output filename " << defaultOutputFile.str() << endl; + } + OutputFile output(outputFile ? outputFile : defaultOutputFile.str()); + + // Start the core algorithm. + if (verbose) { + cout << "Passing control to primary algorithm" << endl; + } + CoveringArray solution = + anneal + (specification, + constraints, + iterations, + startingTemperature, + decrement); + if (verbose) { + cout << "Control returned from primary algorithm" << endl; + } + + // Store the results in the output file. + output.setCoveringArray(solution); + output.write(); + + if (verbose) { + cout << "Done" << endl; + } + return 0; +} diff --git a/casa/algorithms/BinarySearch.C b/casa/algorithms/BinarySearch.C new file mode 100644 index 0000000..4ee02bc --- /dev/null +++ b/casa/algorithms/BinarySearch.C @@ -0,0 +1,37 @@ +// Copyright 2008, 2009 Brady J. Garvin + +// This file is part of Covering Arrays by Simulated Annealing (CASA). + +// CASA 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 3 of the License, or +// (at your option) any later version. + +// CASA 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 CASA. If not, see <http://www.gnu.org/licenses/>. + + +#include <cassert> +#include "algorithms/BinarySearch.H" + +unsigned BinarySearch::operator ()(unsigned offset, unsigned size) { + unsigned result = offset + size; + while (size) { + unsigned division = partitioner(offset, size); + assert(division - offset < size); + if (predicate(division)) { + size = division - offset; + result = division; + } else { + ++division; + size += offset - division; + offset = division; + } + } + return result; +} diff --git a/casa/algorithms/BinarySearch.H b/casa/algorithms/BinarySearch.H new file mode 100644 index 0000000..43d2e2d --- /dev/null +++ b/casa/algorithms/BinarySearch.H @@ -0,0 +1,49 @@ +// Copyright 2008, 2009 Brady J. Garvin + +// This file is part of Covering Arrays by Simulated Annealing (CASA). + +// CASA 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 3 of the License, or +// (at your option) any later version. + +// CASA 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 CASA. If not, see <http://www.gnu.org/licenses/>. + + +#ifndef BINARY_SEARCH_H +#define BINARY_SEARCH_H + +class Partitioner { +public: + virtual ~Partitioner() {} + virtual unsigned operator ()(unsigned offset, unsigned size) = 0; +}; + +class ExpensiveUnaryPredicate { +public: + virtual ~ExpensiveUnaryPredicate() {} + virtual bool operator ()(unsigned index) const = 0; +}; + +class BinarySearch { +protected: + const ExpensiveUnaryPredicate& predicate; + Partitioner& partitioner; +public: + BinarySearch + (const ExpensiveUnaryPredicate&predicate, Partitioner&partitioner) : + predicate(predicate), + partitioner(partitioner) {} + virtual ~BinarySearch() {} + // Returns the smallest index for which the predicate returns true, using the + // partitioner to reduce the comparison cost. + unsigned operator ()(unsigned offset, unsigned size); +}; + +#endif diff --git a/casa/annealing/Anneal.C b/casa/annealing/Anneal.C new file mode 100644 index 0000000..b77e344 --- /dev/null +++ b/casa/annealing/Anneal.C @@ -0,0 +1,152 @@ +// Copyright 2008, 2009 Brady J. Garvin + +// This file is part of Covering Arrays by Simulated Annealing (CASA). + +// CASA 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 3 of the License, or +// (at your option) any later version. + +// CASA 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 CASA. If not, see <http://www.gnu.org/licenses/>. + + +#include "io/Usage.H" + +#include "annealing/Anneal.H" +#include "annealing/Bounds.H" +#include "annealing/AnnealingSuccess.H" +#include "annealing/AnnealingPartitioner.H" + +#include "search/Search.H" +#include "search/StateGuide.H" + +#include "covering/space/SingleChangeSpace.H" +#include "covering/space/GraftSpace.H" +#include "covering/heuristic/CoveringArrayHeuristic.H" +#include "covering/goal/CoverageGoal.H" +#include "covering/filter/CoveringArrayAnnealingFilter.H" +#include "covering/report/IterationReport.H" + +#include "algorithms/BinarySearch.H" + +CoveringArray anneal + (const SpecificationFile&specification, + const ConstraintFile&constraints, + unsigned iterations, + double startingTemperature, + double decrement) { + std::cout << "Setting up annealing framework" << std::endl; + // Build and connect all of the pieces of the search. + // For simulated annealing: + SearchConfiguration configuration(false,true,1U,0U); +#ifdef WITHOUT_INNER + SingleChangeSpace space +#else + GraftSpace space +#endif + (specification.getStrength(), specification.getOptions()); + // Add the constraints. + { + SATSolver&solver = space.getSolver(); + const Array<InputClause>&clauses = constraints.getClauses(); + for (unsigned i = clauses.getSize(); i--;) { + solver.addClause(const_cast<InputClause&>(clauses[i])); + } + } + CoveringArrayHeuristic heuristic; + StateGuide<CoveringArray, CoverageCost>guide; + CoverageGoal goal(space.computeTargetCoverage()); + CoveringArrayAnnealingFilter filter(startingTemperature,decrement); + IterationReport iterationReport; + Search<CoveringArray, CoverageCost>search + (configuration, &space, &heuristic, &guide, &goal, &filter, true); + AnnealingPartitioner partitioner; + // Add the listeners. + { + // For cooling: + ((EventSource<SearchIteration>&)search).addListener(filter); + typedef EventSource<SearchFinish<CoveringArray, CoverageCost> > + FinishEventSourceT; + // Structure start states: + ((FinishEventSourceT&)search).addListener(space); + // Use search feedback to guide the outer search: + ((FinishEventSourceT&)search).addListener(partitioner); + // Give reports on iterations taken: + ((FinishEventSourceT&)search).addListener(iterationReport); + } + CoveringArray initialSolution + (0, + specification.getStrength(), + specification.getOptions(), + space.getSolver()); + + // Here we go... + std::cout << "Annealing" +#ifdef WITHOUT_INNER + << " (without t-set replacement)" +#endif +#ifdef WITHOUT_OUTER + << " (without extra outer search)" +#endif + << std::endl; + unsigned lower = + computeLowerBound(specification.getStrength(), specification.getOptions()); + unsigned upper = + computeUpperBound(specification.getStrength(), specification.getOptions()); + AnnealingSuccess annealingSuccess(search, iterations, initialSolution); + + std::cout << "Suspect that the optimum number of rows is in [" << lower << + ".." << upper << ']' << std::endl; + std::cout << "Starting binary search" << std::endl; + BinarySearch binarySearch(annealingSuccess, partitioner); + unsigned result = binarySearch(lower, upper + 1 - lower); + while (result > upper) { + upper <<= 1; + std::cout << "Trying more conservative upper bound " << upper << std::endl; + result = binarySearch(lower, upper + 1 - lower); + } +#ifndef WITHOUT_OUTER + do { + if (result == lower) { + if (lower > 5) { + lower -= 5; + } else { + --lower; + if (!lower) { + break; + } + } + std::cout << "Trying less conservative lower bound " << lower << + std::endl; + } + unsigned lastResult = result; + unsigned upped = 0; + do { + if (lastResult == result) { + iterations *= 2; + annealingSuccess.setIterations(iterations); + std::cout << "Upping iterations to " << iterations << std::endl; + ++upped; + } else { + upped = 0; + } + lastResult = result; + std::cout << "Restarting binary search with best result at " << + lastResult << " rows" << std::endl; + filter.setTemperature(startingTemperature); + result = binarySearch(lower, lastResult - lower); + } while ((result < lastResult || upped < retries) && result > lower); + } while (result == lower); +#endif + std::cout << "Giving up with best result at " << result << " rows" << + std::endl; + std::cout << "Total cost of computation: " << iterationReport.getTotal() << + " iteration(s)" << std::endl; + return annealingSuccess.getSolution(); +} diff --git a/casa/annealing/Anneal.H b/casa/annealing/Anneal.H new file mode 100644 index 0000000..8eaa6b1 --- /dev/null +++ b/casa/annealing/Anneal.H @@ -0,0 +1,33 @@ +// Copyright 2008, 2009 Brady J. Garvin + +// This file is part of Covering Arrays by Simulated Annealing (CASA). + +// CASA 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 3 of the License, or +// (at your option) any later version. + +// CASA 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 CASA. If not, see <http://www.gnu.org/licenses/>. + +#ifndef ANNEAL_H +#define ANNEAL_H + +#include "io/SpecificationFile.H" +#include "io/ConstraintFile.H" + +#include "covering/state/CoveringArray.H" + +CoveringArray anneal + (const SpecificationFile&specification, + const ConstraintFile&constraints, + unsigned iterations, + double startingTemperature, + double decrement); + +#endif diff --git a/casa/annealing/AnnealingFilter.H b/casa/annealing/AnnealingFilter.H new file mode 100644 index 0000000..f787ae4 --- /dev/null +++ b/casa/annealing/AnnealingFilter.H @@ -0,0 +1,93 @@ +// Copyright 2008, 2009 Brady J. Garvin + +// This file is part of Covering Arrays by Simulated Annealing (CASA). + +// CASA 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 3 of the License, or +// (at your option) any later version. + +// CASA 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 CASA. If not, see <http://www.gnu.org/licenses/>. + + +#ifndef ANNEALING_FILTER_H +#define ANNEALING_FILTER_H + +#include <cassert> +#include <iostream> + +#include "search/GreedyFilter.H" +#include "events/Listener.H" + +// Decides, according to the rules of simulated annealing, when to take good +// moves and when to take bad ones. + +// Should be added as a listener to search iterations in order that cooling be +// synchronized with the search. + +template<class STATE, class COST>class AnnealingFilter : + public GreedyFilter<STATE,COST>, + public Listener<SearchIteration> { + + typedef Heuristic<STATE,COST> HeuristicT; + typedef Goal<STATE> GoalT; + + double temperature; + const double decay; + +public: + AnnealingFilter(double temperature, double decay) : + temperature(temperature), + decay(decay) { + assert(0 <= decay); + assert(decay <= 1); + } + virtual ~AnnealingFilter() {} + + void setTemperature(double temperature) { + this->temperature = temperature; + } + + virtual double convertToDelta(COST childEstimate, COST parentEstimate) const + = 0; + + void signal(const SearchIteration&message) { + temperature *= decay; + } + + void operator() + (std::set<STATE>&children, + const STATE&parent, + const HeuristicT&heuristic, + const GoalT&goal) const { + GreedyFilter<STATE,COST>::operator()(children, heuristic, goal); + assert(children.size() <= 1); + if (children.size()) { + typename std::set<STATE>::iterator child = children.begin(); + COST childEstimate = heuristic.estimate(*child, goal); + COST parentEstimate = heuristic.estimate(parent, goal); + if (!(parentEstimate < childEstimate)) { + // Always take good moves. + return; + } + double delta = convertToDelta(childEstimate, parentEstimate); + double probability = exp(delta / temperature); + int boundary = (int)(probability * RAND_MAX); + if (rand() < boundary) { + // Sometimes take bad moves. + return; + } + children.clear(); + } + // When no moves are possible or a bad move is rejected, keep the parent. + children.insert(parent); + } +}; + +#endif diff --git a/casa/annealing/AnnealingPartitioner.C b/casa/annealing/AnnealingPartitioner.C new file mode 100644 index 0000000..396d193 --- /dev/null +++ b/casa/annealing/AnnealingPartitioner.C @@ -0,0 +1,58 @@ +// Copyright 2008, 2009 Brady J. Garvin + +// This file is part of Covering Arrays by Simulated Annealing (CASA). + +// CASA 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 3 of the License, or +// (at your option) any later version. + +// CASA 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 CASA. If not, see <http://www.gnu.org/licenses/>. + + +#include "annealing/AnnealingPartitioner.H" +#include "io/Usage.H" + +using namespace std; + +unsigned AnnealingPartitioner::operator ()(unsigned offset, unsigned size) { + if (guess && guess - offset < size) { + return guess; + } + return offset + (unsigned)(searchPartition * size); +} + +void AnnealingPartitioner::signal + (const SearchFinish<CoveringArray, CoverageCost>&finish) { + set<const Node<CoveringArray, CoverageCost>*>best = finish.source.getBest(); + if (!best.size()) { + guess = 0; + return; + } + const CoveringArray&state = (*best.begin())->getState(); + assert(state.isTrackingNoncoverage()); + if (finish.results.size()) { + if (finish.iterations < 128) { + lastGuess = guess; + guess = 0; + } else { + unsigned ratio = finish.maxIterations / finish.iterations; + unsigned delta = guess - lastGuess; + lastGuess = guess; + if (delta > 0){ + for (guess = state.getRows(); ratio; --guess, ratio >>= 1); + } else { + for (guess = state.getRows() + delta; ratio; --guess, ratio >>= 2); + } + } + } else { + lastGuess = guess; + guess = state.getRows() + state.getNoncoverage().size() / 2; + } +} diff --git a/casa/annealing/AnnealingPartitioner.H b/casa/annealing/AnnealingPartitioner.H new file mode 100644 index 0000000..34fd564 --- /dev/null +++ b/casa/annealing/AnnealingPartitioner.H @@ -0,0 +1,43 @@ +// Copyright 2008, 2009 Brady J. Garvin + +// This file is part of Covering Arrays by Simulated Annealing (CASA). + +// CASA 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 3 of the License, or +// (at your option) any later version. + +// CASA 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 CASA. If not, see <http://www.gnu.org/licenses/>. + + +#ifndef ANNEALING_PARTITIONER_H +#define ANNEALING_PARTITIONER_H + +#include "algorithms/BinarySearch.H" +#include "events/Listener.H" +#include "search/SearchFinish.H" + +#include "covering/state/CoveringArray.H" +#include "covering/cost/CoverageCost.H" + +class AnnealingPartitioner : + public Partitioner, + public Listener<SearchFinish<CoveringArray,CoverageCost> > { +protected: + unsigned guess; + unsigned lastGuess; +public: + AnnealingPartitioner() : + guess(0), + lastGuess(0) {} + unsigned operator ()(unsigned offset, unsigned size); + void signal(const SearchFinish<CoveringArray, CoverageCost>&finish); +}; + +#endif diff --git a/casa/annealing/AnnealingSuccess.C b/casa/annealing/AnnealingSuccess.C new file mode 100644 index 0000000..f7199f2 --- /dev/null +++ b/casa/annealing/AnnealingSuccess.C @@ -0,0 +1,47 @@ +// Copyright 2008, 2009 Brady J. Garvin + +// This file is part of Covering Arrays by Simulated Annealing (CASA). + +// CASA 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 3 of the License, or +// (at your option) any later version. + +// CASA 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 CASA. If not, see <http://www.gnu.org/licenses/>. + + +#include <iostream> + +#include "covering/space/CoveringArraySpace.H" +#include "annealing/AnnealingSuccess.H" + +using namespace std; + +bool AnnealingSuccess::operator ()(unsigned rows) const { + bool result; + cout << "Trying " << rows << " rows" << endl; + const CoveringArraySpace*space = + dynamic_cast<const CoveringArraySpace*>(search.getSpace()); + assert(space); + cout << "Building start state" << endl; + CoveringArray startState = space->createStartState(rows); + search.addStartState(startState); + cout << "Searching" << endl; + set<NodeT*>solutions = search.search(iterations, false); + if (solutions.empty()) { + cout << "Failed to meet coverage with " << rows << " rows" << endl; + result = false; + } else { + cout << "Met coverage with " << rows << " rows" << endl; + result = true; + solution = (*solutions.begin())->getState(); + } + search.clear(); + return result; +} diff --git a/casa/annealing/AnnealingSuccess.H b/casa/annealing/AnnealingSuccess.H new file mode 100644 index 0000000..d108f2d --- /dev/null +++ b/casa/annealing/AnnealingSuccess.H @@ -0,0 +1,57 @@ +// Copyright 2008, 2009 Brady J. Garvin + +// This file is part of Covering Arrays by Simulated Annealing (CASA). + +// CASA 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 3 of the License, or +// (at your option) any later version. + +// CASA 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 CASA. If not, see <http://www.gnu.org/licenses/>. + + +#ifndef ANNEALING_SUCCESS_H +#define ANNEALING_SUCCESS_H + +#include "algorithms/BinarySearch.H" +#include "search/Search.H" + +#include "covering/state/CoveringArray.H" +#include "covering/cost/CoverageCost.H" + +class AnnealingSuccess : public ExpensiveUnaryPredicate { +protected: + typedef Node<CoveringArray, CoverageCost> + NodeT; + + Search<CoveringArray, CoverageCost>& search; + unsigned iterations; + mutable CoveringArray solution; + +public: + AnnealingSuccess + (Search<CoveringArray, CoverageCost>&search, + unsigned iterations, + const CoveringArray&initialSolution) : + search(search), + iterations(iterations), + solution(initialSolution) {} + + bool operator ()(unsigned rows) const; + + void setIterations(unsigned iterations) { + this->iterations = iterations; + } + + const CoveringArray&getSolution() const { + return solution; + } +}; + +#endif diff --git a/casa/annealing/Bounds.C b/casa/annealing/Bounds.C new file mode 100644 index 0000000..8e087e9 --- /dev/null +++ b/casa/annealing/Bounds.C @@ -0,0 +1,66 @@ +// Copyright 2008, 2009 Brady J. Garvin + +// This file is part of Covering Arrays by Simulated Annealing (CASA). + +// CASA 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 3 of the License, or +// (at your option) any later version. + +// CASA 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 CASA. If not, see <http://www.gnu.org/licenses/>. + + +#include <cmath> +#include <algorithm> +#include <functional> + +#include "annealing/Bounds.H" + +using namespace std; + +#ifndef UPPER_BOUND_SCALING_FACTOR +#define UPPER_BOUND_SCALING_FACTOR 5 +#endif + +unsigned computeLowerBound(unsigned strength, const Options&options) { + if (lowerBound) { + return lowerBound; + } + static greater<unsigned>backwards; + unsigned result = 1; + Array<unsigned>symbolCounts(options.getSize()); + for (unsigned i = symbolCounts.getSize(); i--;) { + symbolCounts[i] = options.getSymbolCount(i); + } + partial_sort + (symbolCounts + 0, + symbolCounts + strength, + symbolCounts + symbolCounts.getSize(), + backwards); + for (unsigned i = strength; i--;) { + result *= symbolCounts[i]; + } + return result; +} + +unsigned computeUpperBound(unsigned strength, const Options&options) { + if (upperBound) { + return upperBound; + } + unsigned max = 0; + Array<unsigned>symbolCounts(options.getSize()); + for (unsigned i = symbolCounts.getSize(); i--;) { + unsigned candidate = options.getSymbolCount(i); + if (candidate > max) { + max = candidate; + } + } + return (unsigned)(UPPER_BOUND_SCALING_FACTOR * + pow((double)max, (double)strength)); +} diff --git a/casa/annealing/Bounds.H b/casa/annealing/Bounds.H new file mode 100644 index 0000000..2062dfa --- /dev/null +++ b/casa/annealing/Bounds.H @@ -0,0 +1,28 @@ +// Copyright 2008, 2009 Brady J. Garvin + +// This file is part of Covering Arrays by Simulated Annealing (CASA). + +// CASA 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 3 of the License, or +// (at your option) any later version. + +// CASA 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 CASA. If not, see <http://www.gnu.org/licenses/>. + + +#ifndef BOUNDS_H +#define BOUNDS_H + +#include "io/Usage.H" +#include "covering/bookkeeping/Options.H" + +unsigned computeLowerBound(unsigned strength, const Options&options); +unsigned computeUpperBound(unsigned strength, const Options&options); + +#endif diff --git a/casa/covering/bookkeeping/Coverage.H b/casa/covering/bookkeeping/Coverage.H new file mode 100644 index 0000000..c0ce2b3 --- /dev/null +++ b/casa/covering/bookkeeping/Coverage.H @@ -0,0 +1,313 @@ +// Copyright 2008, 2009 Brady J. Garvin + +// This file is part of Covering Arrays by Simulated Annealing (CASA). + +// CASA 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 3 of the License, or +// (at your option) any later version. + +// CASA 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 CASA. If not, see <http://www.gnu.org/licenses/>. + + +#ifndef COVERAGE_H +#define COVERAGE_H + +#include "PascalTriangle.H" +#include "Combinadic.H" + +#include "SubstitutionArray.H" + +#include "covering/bookkeeping/Options.H" + +template<class T>class Coverage { +protected: + unsigned strength; + Options options; + // The offsets are indices into the contents array; entry offsets[i], where i + // is the combinadic encoding of a set of columns, is the beginning of the + // contents for that column set's t-sets. + Array<unsigned> offsets; + SubstitutionArray<T> contents; + +public: + Coverage(unsigned strength, Options options) : + strength(strength), + options(options), + offsets(triangle.nCr(options.getSize(), strength)) { + unsigned size = 0; + unsigned offsetIndex = 0; + for (Array<unsigned>columns = combinadic.begin(strength); + columns[strength - 1] < options.getSize(); + combinadic.next(columns)) { + unsigned blockSize = 1; + for (unsigned i = strength; i--;) { + blockSize *= options.getSymbolCount(columns[i]); + } + offsets[offsetIndex++] = size; + size += blockSize; + } + contents = Array<T>(size); + } + + Coverage(const Coverage©) : + strength(copy.strength), + options(copy.options), + offsets(copy.offsets), + contents(copy.contents) {} + +protected: + // The method encode, in its various forms, is responsible for converting a + // sorted t-set to an index into the contents array. + + // These hinted versions of encode are for when some information has already + // been computed. indexHint is the combinadic encoding of the set of columns; + // columnsHint is this set of columns in sorted order; firstsHint is an array + // of corresponding first symbols; and countsHint is an array of symbol counts + // for each column. + unsigned encode + (unsigned indexHint, + Array<unsigned>columnsHint, + Array<unsigned>firstsHint, + Array<unsigned>countsHint, + Array<unsigned>sortedCombination) const { + assert(sortedCombination.getSize() == strength); + assert(indexHint < offsets.getSize()); + unsigned offset = offsets[indexHint]; + unsigned index = 0; + for (unsigned i = strength; i--;) { + unsigned column = columnsHint[i]; + unsigned base = firstsHint[column]; + unsigned count = countsHint[column]; + index *= count; + index += sortedCombination[i] - base; + } + return offset + index; + } + + unsigned encode + (Array<unsigned>columnsHint, + Array<unsigned>firstsHint, + Array<unsigned>countsHint, + Array<unsigned>sortedCombination) const { + return encode + (combinadic.encode(columnsHint), + columnsHint, + firstsHint, + countsHint, + sortedCombination); + } + + unsigned encode(Array<unsigned>sortedCombination) const { + assert(sortedCombination.getSize() == strength); + Array<unsigned>columns(strength); + for (unsigned i = strength; i--;) { + columns[i] = options.getOption(sortedCombination[i]); + } + unsigned offsetIndex = combinadic.encode(columns); + assert(offsetIndex < offsets.getSize()); + unsigned offset = offsets[offsetIndex]; + unsigned index = 0; + for (unsigned i = strength; i--;) { + unsigned column = columns[i]; + unsigned base = options.getFirstSymbol(column); + unsigned count = options.getSymbolCount(column); + index *= count; + index += sortedCombination[i] - base; + } + return offset + index; + } + + // The method decode, of course, does the opposite of encode. + Array<unsigned>decode(unsigned encoding) const { + unsigned offsetIndex = offsets.getSize(); + while (offsets[--offsetIndex] > encoding); + unsigned index = encoding - offsets[offsetIndex]; + Array<unsigned>columns = combinadic.decode(offsetIndex, strength); + Array<unsigned>result(strength); + for (unsigned i = 0; i < strength; ++i) { + unsigned column = columns[i]; + unsigned base = options.getFirstSymbol(column); + unsigned count = options.getSymbolCount(column); + unsigned digit = index % count; + index -= digit; + index /= count; + result[i] = base + digit; + } + assert(encode(result) == encoding); + return result; + } + +public: + unsigned getStrength() const { + return strength; + } + const Options&getOptions() const { + return options; + } + + class Entry{ + protected: + Coverage& owner; + unsigned index; + public: + Entry(const Coverage&owner,unsigned index) : + owner(const_cast<Coverage&>(owner)), + index(index) {} + operator T() const { + return owner.contents[index]; + } + Entry&operator =(const T&value) { + owner.contents[index] = value; + return *this; + } + Entry&operator --() { + --owner.contents[index]; + return *this; + } + Entry&operator ++() { + ++owner.contents[index]; + return *this; + } + }; + + const Entry operator[](Array<unsigned>sortedCombination) const { + return Entry(*this, encode(sortedCombination)); + } + Entry operator [](Array<unsigned>sortedCombination) { + return Entry(*this, encode(sortedCombination)); + } + + // The methods named hintGet work like the [] operator with the aforementioned + // hints. + const Entry hintGet + (unsigned indexHint, + Array<unsigned>columnsHint, + Array<unsigned>firstsHint, + Array<unsigned>countsHint, + Array<unsigned>sortedCombination) const { + return Entry + (*this, + encode + (indexHint, columnsHint, firstsHint, countsHint, sortedCombination)); + } + + Entry hintGet + (unsigned indexHint, + Array<unsigned>columnsHint, + Array<unsigned>firstsHint, + Array<unsigned>countsHint, + Array<unsigned>sortedCombination) { + return Entry + (*this, + encode + (indexHint, columnsHint, firstsHint, countsHint, sortedCombination)); + } + + const Entry hintGet + (Array<unsigned>columnsHint, + Array<unsigned>firstsHint, + Array<unsigned>countsHint, + Array<unsigned>sortedCombination) const { + return Entry + (*this, + encode(columnsHint, firstsHint, countsHint, sortedCombination)); + } + + Entry hintGet + (Array<unsigned>columnsHint, + Array<unsigned>firstsHint, + Array<unsigned>countsHint, + Array<unsigned>sortedCombination) { + return Entry + (*this, + encode(columnsHint, firstsHint, countsHint, sortedCombination)); + } + + class iterator { + protected: + Coverage& owner; + unsigned index; + public: + iterator(Coverage&owner, unsigned index) : + owner(owner), + index(index) {} + const Entry operator *() const { + return Entry(owner, index); + } + Entry operator *() { + return Entry(owner, index); + } + iterator&operator ++() { + ++index; + return *this; + } + bool operator ==(const iterator&other) const { + return &owner == &other.owner && index == other.index; + } + bool operator !=(const iterator&other) const { + return &owner != &other.owner || index != other.index; + } + Array<unsigned>getCombination() const { + return owner.decode(index); + } + }; + + class const_iterator { + protected: + const Coverage& owner; + unsigned index; + public: + const_iterator(const Coverage&owner, unsigned index) : + owner(owner), + index(index) {} + const_iterator(const iterator©) : + owner(copy.owner), + index(copy.index) {} + const Entry operator *() const { + return Entry(owner, index); + } + const_iterator&operator ++() { + ++index; + return *this; + } + bool operator ==(const const_iterator&other) const { + return &owner == &other.owner && index == other.index; + } + bool operator != (const const_iterator&other) const { + return &owner != &other.owner || index != other.index; + } + Array<unsigned>getCombination() const { + return owner.decode(index); + } + }; + + iterator begin() { + return iterator(*this, 0); + } + const_iterator begin() const { + return const_iterator(*this, 0); + } + iterator end() { + return iterator(*this, contents.getSize()); + } + const_iterator end() const { + return const_iterator(*this, contents.getSize()); + } + + unsigned getSize() const { + return contents.getSize(); + } + + void fill(const T&filler) { + contents.fill(filler); + } +}; + +#endif diff --git a/casa/covering/bookkeeping/Options.C b/casa/covering/bookkeeping/Options.C new file mode 100644 index 0000000..cd3c911 --- /dev/null +++ b/casa/covering/bookkeeping/Options.C @@ -0,0 +1,102 @@ +// Copyright 2008, 2009 Brady J. Garvin + +// This file is part of Covering Arrays by Simulated Annealing (CASA). + +// CASA 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 3 of the License, or +// (at your option) any later version. + +// CASA 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 CASA. If not, see <http://www.gnu.org/licenses/>. + + +#include "covering/bookkeeping/Options.H" + +Options::Options() : + cumulativeValueCounts(0), + owningOptions(0) {} + +Options::Options(Array<unsigned>values) : + cumulativeValueCounts(values.getSize()) { + unsigned cumulativeValueCount = 0; + for (unsigned i = 0; i < values.getSize(); ++i) { + cumulativeValueCount += values[i]; + cumulativeValueCounts[i] = cumulativeValueCount; + } + owningOptions = Array<unsigned>(cumulativeValueCount); + for (unsigned i = 0, j = 0; i < values.getSize(); ++i) { + for (unsigned k = values[i]; k--;) { + owningOptions[j++] = i; + } + } +} + +Options::Options(const Options©) : + cumulativeValueCounts(copy.cumulativeValueCounts), + owningOptions(copy.owningOptions) {} + +unsigned Options::getSize() const { + return cumulativeValueCounts.getSize(); +} + +unsigned Options::getFirstSymbol(unsigned option) const { + return option ? cumulativeValueCounts[option - 1] : 0; +} + +Array<unsigned>Options::getFirstSymbols() const { + unsigned size = cumulativeValueCounts.getSize(); + Array<unsigned>result(size); + for (unsigned i = size; i-- > 1;) { + result[i] = cumulativeValueCounts[i - 1]; + } + if (size) { + result[0] = 0; + } + return result; +} + +unsigned Options::getSymbolCount(unsigned option) const { + return option ? + (cumulativeValueCounts[option] - cumulativeValueCounts[option - 1]) : + cumulativeValueCounts[0]; +} + +Array<unsigned>Options::getSymbolCounts() const { + unsigned size = cumulativeValueCounts.getSize(); + Array<unsigned>result(size); + for (unsigned i = size; i-- > 1;) { + result[i] = cumulativeValueCounts[i] - cumulativeValueCounts[i - 1]; + } + if (size) { + result[0] = cumulativeValueCounts[0]; + } + return result; +} + +unsigned Options::getLastSymbol(unsigned option) const { + return cumulativeValueCounts[option] - 1; +} + +unsigned Options::getRandomSymbol(unsigned option) const { + return rand() % getSymbolCount(option) + getFirstSymbol(option); +} + +unsigned Options::getOtherRandomSymbol(unsigned option, unsigned exclude) + const { + unsigned count = getSymbolCount(option); + if (count == 1) { + return getFirstSymbol(option); + } + unsigned result = rand() % (count - 1) + getFirstSymbol(option); + return (result >= exclude) ? (result + 1) : result; +} + +unsigned Options::getOption(unsigned symbol) const { + return owningOptions[symbol]; +} diff --git a/casa/covering/bookkeeping/Options.H b/casa/covering/bookkeeping/Options.H new file mode 100644 index 0000000..ee047a4 --- /dev/null +++ b/casa/covering/bookkeeping/Options.H @@ -0,0 +1,50 @@ +// Copyright 2008, 2009 Brady J. Garvin + +// This file is part of Covering Arrays by Simulated Annealing (CASA). + +// CASA 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 3 of the License, or +// (at your option) any later version. + +// CASA 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 CASA. If not, see <http://www.gnu.org/licenses/>. + + +#ifndef OPTIONS_H +#define OPTIONS_H + +#include <cstdlib> +#include <utility> + +#include "Array.H" + +class Options { +protected: + // The entry cumulativeValueCounts[i] is the number of values in options 0 + // through i, inclusive. + Array<unsigned> cumulativeValueCounts; + // The entry owningOptions[i] is the option that the value i belongs to. + Array<unsigned> owningOptions; + +public: + Options(); + Options(Array<unsigned>valueCounts); + Options(const Options©); + unsigned getSize() const; + unsigned getFirstSymbol(unsigned option) const; + Array<unsigned>getFirstSymbols() const; + unsigned getSymbolCount(unsigned option) const; + Array<unsigned>getSymbolCounts() const; + unsigned getLastSymbol(unsigned option) const; + unsigned getRandomSymbol(unsigned option) const; + unsigned getOtherRandomSymbol(unsigned option, unsigned exclude) const; + unsigned getOption(unsigned symbol) const; +}; + +#endif diff --git a/casa/covering/cost/CoverageCost.H b/casa/covering/cost/CoverageCost.H new file mode 100644 index 0000000..524a240 --- /dev/null +++ b/casa/covering/cost/CoverageCost.H @@ -0,0 +1,72 @@ +// Copyright 2008, 2009 Brady J. Garvin + +// This file is part of Covering Arrays by Simulated Annealing (CASA). + +// CASA 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 3 of the License, or +// (at your option) any later version. + +// CASA 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 CASA. If not, see <http://www.gnu.org/licenses/>. + + +#ifndef COVERAGE_COST_H +#define COVERAGE_COST_H + +#include <cassert> + +class CoverageCost { +protected: + unsigned noncoverage; + unsigned multipleCoverage; + +public: + // So we can initialize an object from a literal zero: + CoverageCost(unsigned zero = 0) : + noncoverage(0), + multipleCoverage(0) { + assert(!zero); + } + CoverageCost(unsigned noncoverage, unsigned multipleCoverage) : + noncoverage(noncoverage), + multipleCoverage(multipleCoverage) {} + + unsigned getNoncoverage() const { + return noncoverage; + } + unsigned getMultipleCoverage() const { + return multipleCoverage; + } + + bool operator <(const CoverageCost&other) const { + if (noncoverage < other.noncoverage) { + return true; + } + if (noncoverage > other.noncoverage) { + return false; + } + return multipleCoverage < other.multipleCoverage; + } + bool operator <=(const CoverageCost&other) const { + if (noncoverage < other.noncoverage) { + return true; + } + if (noncoverage > other.noncoverage) { + return false; + } + return multipleCoverage <= other.multipleCoverage; + } + bool operator ==(const CoverageCost&other) const { + return + noncoverage == other.noncoverage && + multipleCoverage == other.multipleCoverage; + } +}; + +#endif diff --git a/casa/covering/filter/CoveringArrayAnnealingFilter.H b/casa/covering/filter/CoveringArrayAnnealingFilter.H new file mode 100644 index 0000000..f876e8f --- /dev/null +++ b/casa/covering/filter/CoveringArrayAnnealingFilter.H @@ -0,0 +1,49 @@ +// Copyright 2008, 2009 Brady J. Garvin + +// This file is part of Covering Arrays by Simulated Annealing (CASA). + +// CASA 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 3 of the License, or +// (at your option) any later version. + +// CASA 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 CASA. If not, see <http://www.gnu.org/licenses/>. + + +#ifndef COVERING_ARRAY_ANNEALING_FILTER_H +#define COVERING_ARRAY_ANNEALING_FILTER_H + +#include "annealing/AnnealingFilter.H" + +#include "covering/state/CoveringArray.H" +#include "covering/cost/CoverageCost.H" + +#ifndef MULTIPLE_COVERAGE_WEIGHT +#define MULTIPLE_COVERAGE_WEIGHT 0.1L +#endif + +class CoveringArrayAnnealingFilter : + public AnnealingFilter<CoveringArray, CoverageCost> { +public: + CoveringArrayAnnealingFilter(double temperature, double decay) : + AnnealingFilter<CoveringArray, CoverageCost>(temperature, decay) {} + + double convertToDelta(CoverageCost childEstimate, CoverageCost parentEstimate) + const { + unsigned childNoncoverage = childEstimate.getNoncoverage(); + unsigned parentNoncoverage = parentEstimate.getNoncoverage(); + unsigned childMultipleCoverage = childEstimate.getMultipleCoverage(); + unsigned parentMultipleCoverage = parentEstimate.getMultipleCoverage(); + return -(double)(childNoncoverage - parentNoncoverage) - + MULTIPLE_COVERAGE_WEIGHT * + (childMultipleCoverage - parentMultipleCoverage); + } +}; + +#endif diff --git a/casa/covering/goal/CoverageGoal.H b/casa/covering/goal/CoverageGoal.H new file mode 100644 index 0000000..c4e0693 --- /dev/null +++ b/casa/covering/goal/CoverageGoal.H @@ -0,0 +1,43 @@ +// Copyright 2008, 2009 Brady J. Garvin + +// This file is part of Covering Arrays by Simulated Annealing (CASA). + +// CASA 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 3 of the License, or +// (at your option) any later version. + +// CASA 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 CASA. If not, see <http://www.gnu.org/licenses/>. + + +#ifndef COVERAGE_GOAL_H +#define COVERAGE_GOAL_H + +#include "search/Goal.H" + +#include "covering/state/CoveringArray.H" + +class CoverageGoal : public Goal<CoveringArray> { +protected: + unsigned targetCoverage; +public: + CoverageGoal(unsigned targetCoverage) : + targetCoverage(targetCoverage) {} + + unsigned getTargetCoverage() { + return targetCoverage; + } + + bool isGoal(const CoveringArray&array) { + assert(array.getCoverageCount() <= targetCoverage); + return array.getCoverageCount() == targetCoverage; + } +}; + +#endif diff --git a/casa/covering/heuristic/CoveringArrayHeuristic.H b/casa/covering/heuristic/CoveringArrayHeuristic.H new file mode 100644 index 0000000..61214b8 --- /dev/null +++ b/casa/covering/heuristic/CoveringArrayHeuristic.H @@ -0,0 +1,37 @@ +// Copyright 2008, 2009 Brady J. Garvin + +// This file is part of Covering Arrays by Simulated Annealing (CASA). + +// CASA 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 3 of the License, or +// (at your option) any later version. + +// CASA 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 CASA. If not, see <http://www.gnu.org/licenses/>. + + +#ifndef COVERING_ARRAY_HEURISTIC_H +#define COVERING_ARRAY_HEURISTIC_H + +#include "search/Heuristic.H" + +#include "covering/state/CoveringArray.H" +#include "covering/goal/CoverageGoal.H" + +class CoveringArrayHeuristic : public Heuristic<CoveringArray, CoverageCost> { + CoverageCost estimate + (const CoveringArray&state, const Goal<CoveringArray>&goal) const { + unsigned targetCoverage = ((CoverageGoal&)goal).getTargetCoverage(); + return CoverageCost + (targetCoverage - state.getCoverageCount(), + state.getMultipleCoverageCount()); + } +}; + +#endif diff --git a/casa/covering/report/IterationReport.H b/casa/covering/report/IterationReport.H new file mode 100644 index 0000000..7799b88 --- /dev/null +++ b/casa/covering/report/IterationReport.H @@ -0,0 +1,53 @@ +// Copyright 2008, 2009 Brady J. Garvin + +// This file is part of Covering Arrays by Simulated Annealing (CASA). + +// CASA 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 3 of the License, or +// (at your option) any later version. + +// CASA 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 CASA. If not, see <http://www.gnu.org/licenses/>. + + +#ifndef ITERATION_REPORT_H +#define ITERATION_REPORT_H + +#include <iostream> + +class IterationReport : + public Listener<SearchFinish<CoveringArray, CoverageCost> > { +protected: + unsigned total; +public: + IterationReport() : + total(0) {} + void signal(const SearchFinish<CoveringArray, CoverageCost>&finish) { + std::set<const Node<CoveringArray, CoverageCost>*>best = + finish.source.getBest(); + if (best.size()) { + const CoveringArray&state = (*best.begin())->getState(); + assert(state.isTrackingNoncoverage()); + std::cout << "Search stopped after " << finish.iterations << '/' << + finish.maxIterations << " iteration(s) with " << + state.getNoncoverage().size() << " uncovered t-sets and " << + state.getMultipleCoverageCount() << " multicovered t-sets" << std::endl; + } else { + std::cout << "Search stopped after " << finish.iterations << '/' << + finish.maxIterations << " iteration(s) with no results" << std::endl; + } + total += finish.iterations; + std::cout << "Used " << total << " total iterations thus far" << std::endl; + } + unsigned getTotal() const { + return total; + } +}; + +#endif diff --git a/casa/covering/space/CoveringArraySpace.C b/casa/covering/space/CoveringArraySpace.C new file mode 100644 index 0000000..6287bd3 --- /dev/null +++ b/casa/covering/space/CoveringArraySpace.C @@ -0,0 +1,80 @@ +// Copyright 2008, 2009 Brady J. Garvin + +// This file is part of Covering Arrays by Simulated Annealing (CASA). + +// CASA 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 3 of the License, or +// (at your option) any later version. + +// CASA 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 CASA. If not, see <http://www.gnu.org/licenses/>. + + +#include "covering/space/CoveringArraySpace.H" + +CoveringArraySpace::CoveringArraySpace(unsigned strength, Options options) : + strength(strength), options(options) { + assert(strength <= options.getSize()); + for (unsigned i = options.getSize(); i--;) { + // The clause atLeast requires that each column be filled. + InputClause atLeast; + for (unsigned + j = options.getFirstSymbol(i), + limit = options.getLastSymbol(i); + j <= limit; + ++j) { + atLeast.append(InputTerm(false, j)); + } + solver.addClause(atLeast); + // The clauses atMost require that each pairing of symbols from an option + // show at least one absence. + for (unsigned + j = options.getFirstSymbol(i), + limit = options.getLastSymbol(i); + j <= limit; ++j) { + for (unsigned k = j + 1; k <= limit; ++k) { + InputClause atMost; + atMost.append(InputTerm(true, j)); + atMost.append(InputTerm(true, k)); + solver.addClause(atMost); + } + } + } +} + +unsigned CoveringArraySpace::computeTargetCoverage() const { + unsigned result = 0; + for (Array<unsigned>columns = combinadic.begin(strength); + columns[strength - 1] < options.getSize(); + combinadic.next(columns)) { + // Initialization: + Array<InputTerm>combination(columns.getSize()); + for (unsigned i = columns.getSize(); i--;) { + combination[i] = InputTerm(false, options.getFirstSymbol(columns[i])); + } + // Body: + loop: + { + InputKnown known(combination); + if (solver(known)) { + ++result; + } + } + // Advance: + for (unsigned i = columns.getSize(); i--;) { + unsigned next = combination[i].getVariable() + 1; + if (next <= options.getLastSymbol(columns[i])) { + combination[i] = InputTerm(false, next); + goto loop; + } + combination[i] = InputTerm(false, options.getFirstSymbol(columns[i])); + } + } + return result; +} diff --git a/casa/covering/space/CoveringArraySpace.H b/casa/covering/space/CoveringArraySpace.H new file mode 100644 index 0000000..e4702a5 --- /dev/null +++ b/casa/covering/space/CoveringArraySpace.H @@ -0,0 +1,52 @@ +// Copyright 2008, 2009 Brady J. Garvin + +// This file is part of Covering Arrays by Simulated Annealing (CASA). + +// CASA 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 3 of the License, or +// (at your option) any later version. + +// CASA 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 CASA. If not, see <http://www.gnu.org/licenses/>. + + +#ifndef COVERING_ARRAY_SPACE_H +#define COVERING_ARRAY_SPACE_H + +#include <cassert> + +#include "Array.H" + +#include "search/StateSpace.H" + +#include "covering/state/CoveringArray.H" +#include "covering/bookkeeping/Options.H" +#include "covering/cost/CoverageCost.H" + +#include "sat/SAT.H" + +class CoveringArraySpace : public StateSpace<CoveringArray, CoverageCost>{ +protected: + unsigned strength; + Options options; + mutable SATSolver solver; +public: + CoveringArraySpace(unsigned strength, Options options); + virtual ~CoveringArraySpace() {} + virtual CoveringArray createStartState(unsigned rows) const = 0; + SATSolver&getSolver() { + return solver; + } + const SATSolver&getSolver() const { + return solver; + } + unsigned computeTargetCoverage() const; +}; + +#endif diff --git a/casa/covering/space/GraftSpace.C b/casa/covering/space/GraftSpace.C new file mode 100644 index 0000000..daa84e0 --- /dev/null +++ b/casa/covering/space/GraftSpace.C @@ -0,0 +1,187 @@ +// Copyright 2008, 2009 Brady J. Garvin + +// This file is part of Covering Arrays by Simulated Annealing (CASA). + +// CASA 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 3 of the License, or +// (at your option) any later version. + +// CASA 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 CASA. If not, see <http://www.gnu.org/licenses/>. + + +#include <algorithm> + +#include "utility/igreater.H" + +#include "covering/space/GraftSpace.H" + +using namespace std; + +#ifndef MAXIMUM_SUBROW_CHANGE_FAILED_ATTEMPTS +#define MAXIMUM_SUBROW_CHANGE_FAILED_ATTEMPTS 32 +#endif + +Array<unsigned>GraftSpace::createRandomMatchingRow(InputKnown&known) const { + Array<unsigned>result(options.getSize()); + for (unsigned i = options.getSize(); i--;) { + vector<unsigned>candidates; + for (unsigned + j = options.getSymbolCount(i), + base = options.getFirstSymbol(i); + j--;) { + candidates.push_back(base + j); + } + unsigned index = rand() % candidates.size(); + unsigned symbol = candidates[index]; + known.append(InputTerm(false, symbol)); + while (!solver(known)) { + known.undoAppend(); + candidates[index] = candidates[candidates.size() - 1]; + candidates.pop_back(); + index = rand() % candidates.size(); + symbol = candidates[index]; + known.append(InputTerm(false, symbol)); + } + result[i] = symbol; + } + return result; +} + +CoveringArray GraftSpace::createStartState(unsigned rows) const { + CoveringArray result(rows, strength, options, solver); + unsigned i = rows; + while (i-->resurrectionBuffer.size()) { + InputKnown known; + result.setBackingArrayRow(i, createRandomMatchingRow(known)); + } + if (resurrectionBuffer.size()) { + for (++i;i--;) { + Array<unsigned>row = resurrectionBuffer[i]; + // We must deep copy to preserve the resurrection buffer. + for (unsigned j = options.getSize(); j--;) { + result.setBackingArrayEntry(i, j, row[j]); + } + } + } + result.setTrackingCoverage(true); + result.setTrackingNoncoverage(true); + return result; +} + +CoverageCost GraftSpace::getTraveled(const CoveringArray&start) const { + return 0; +} + +CoverageCost GraftSpace::getTraveled + (const Node<CoveringArray, CoverageCost>&parent,const CoveringArray&state) + const { + return 0; +} + +set<CoveringArray>GraftSpace::getChildren + (const CoveringArray&state, float proportion) const { + assert(false); // Unimplemented. + return getChildren(state, (unsigned)1); +} + +set<CoveringArray>GraftSpace::getChildren + (const CoveringArray&state, unsigned count) const { + set<CoveringArray>result; + unsigned rows = state.getRows(); + assert(options.getSize() == state.getOptions()); + assert(state.isTrackingNoncoverage()); + const set<Array<unsigned>, ArrayComparator<unsigned> >&noncoverage = + state.getNoncoverage(); + if (noncoverage.empty()){ + return result; + } + unsigned attempts = 0; + for (unsigned i = count; i; ++attempts) { + unsigned row = rand() % rows; + set<Array<unsigned>, ArrayComparator<unsigned> >::const_iterator + combinationIterator = noncoverage.begin(); + unsigned combinationIndex = rand() % noncoverage.size(); + while (combinationIndex--) { + ++combinationIterator; + } + Array<unsigned>combination = *combinationIterator; + Array<unsigned>columns(strength); + InputKnown known; + if (attempts < MAXIMUM_SUBROW_CHANGE_FAILED_ATTEMPTS) { + for (unsigned j = strength; j--;) { + columns[j] = options.getOption(combination[j]); + } + for (unsigned j = options.getSize(), k = strength; j--;) { + if (k && columns[k-1] == j) { + unsigned symbol = combination[--k]; + known.append(InputTerm(false, symbol)); + } else { + assert(!k || columns[k - 1] < j); + unsigned symbol = state(row, j); + known.append(InputTerm(false, symbol)); + } + } + if (solver(known)) { + CoveringArray child = state; + child(row, columns) = combination; + result.insert(child); + --i; + attempts = 0; + } + } else { + cout << "Considering a full row change" << endl; + for (unsigned k = strength; k--;) { + known.append(InputTerm(false, combination[k])); + } + CoveringArray child = state; + child(row) = createRandomMatchingRow(known); + result.insert(child); + --i; + attempts = 0; + } + } + return result; +} + +void GraftSpace::signal(const SearchFinish<CoveringArray, CoverageCost>&finish) { + const set<const Node<CoveringArray, CoverageCost>*>&best = + finish.source.getBest(); + if (best.empty()) { + return; + } + const CoveringArray&solution = (*best.begin())->getState(); + unsigned rowCount = solution.getRows(); + unsigned optionCount = solution.getOptions(); + resurrectionBuffer.reserve(rowCount); + while (resurrectionBuffer.size() < rowCount) { + resurrectionBuffer.push_back(Array<unsigned>()); + } + cout << "Sorting rows for distinct coverage" << endl; + Array<unsigned>distinctCoverage = solution.countDistinctCoverage(); + Array<unsigned>permutation(rowCount); + for (unsigned i = rowCount; i--;) { + permutation[i] = i; + } + igreater<unsigned>betterDistinctCoverage(distinctCoverage); + sort(permutation + 0, permutation + rowCount, betterDistinctCoverage); + cout << "Saving rows in resurrection buffer" << endl; + for (unsigned i = rowCount; i--;) { + unsigned p = permutation[i]; + Array<unsigned>row = Array<unsigned>(optionCount); + for (unsigned j = optionCount; j--;) { + row[j] = solution(p, j); + } + resurrectionBuffer[i] = row; + } +} + +void GraftSpace::clearResurrectionBuffer() { + resurrectionBuffer.clear(); +} diff --git a/casa/covering/space/GraftSpace.H b/casa/covering/space/GraftSpace.H new file mode 100644 index 0000000..abd7b84 --- /dev/null +++ b/casa/covering/space/GraftSpace.H @@ -0,0 +1,60 @@ +// Copyright 2008, 2009 Brady J. Garvin + +// This file is part of Covering Arrays by Simulated Annealing (CASA). + +// CASA 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 3 of the License, or +// (at your option) any later version. + +// CASA 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 CASA. If not, see <http://www.gnu.org/licenses/>. + + +#ifndef GRAFT_SPACE_H +#define GRAFT_SPACE_H + +#include <vector> +#include <iostream> + +#include "Array.H" + +#include "covering/space/CoveringArraySpace.H" +#include "covering/cost/CoverageCost.H" + +#include "events/Listener.H" +#include "search/SearchFinish.H" + +class GraftSpace : + public CoveringArraySpace, + public Listener<SearchFinish<CoveringArray, CoverageCost> > { +protected: + std::vector<Array<unsigned> > resurrectionBuffer; + +public: + GraftSpace(unsigned strength, Options options) : + CoveringArraySpace(strength, options) {} + +protected: + Array<unsigned>createRandomMatchingRow(InputKnown&known) const; + +public: + CoveringArray createStartState(unsigned rows) const; + CoverageCost getTraveled(const CoveringArray&start) const; + CoverageCost getTraveled + (const Node<CoveringArray, CoverageCost>&parent, const CoveringArray&state) + const; + std::set<CoveringArray>getChildren + (const CoveringArray&state, float proportion) const; + std::set<CoveringArray>getChildren + (const CoveringArray&state,unsigned count) const; + void signal(const SearchFinish<CoveringArray, CoverageCost>&finish); + void clearResurrectionBuffer(); +}; + +#endif diff --git a/casa/covering/space/SingleChangeSpace.C b/casa/covering/space/SingleChangeSpace.C new file mode 100644 index 0000000..96c4146 --- /dev/null +++ b/casa/covering/space/SingleChangeSpace.C @@ -0,0 +1,175 @@ +// Copyright 2008, 2009 Brady J. Garvin + +// This file is part of Covering Arrays by Simulated Annealing (CASA). + +// CASA 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 3 of the License, or +// (at your option) any later version. + +// CASA 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 CASA. If not, see <http://www.gnu.org/licenses/>. + + +#include <iostream> +#include <algorithm> + +#include "utility/igreater.H" + +#include "covering/space/SingleChangeSpace.H" + +using namespace std; + +#ifndef MAXIMUM_SINGLE_CHANGE_FAILED_ATTEMPTS +#define MAXIMUM_SINGLE_CHANGE_FAILED_ATTEMPTS 32 +#endif + +Array<unsigned>SingleChangeSpace::createRandomMatchingRow + (InputKnown&known) const { + Array<unsigned>result(options.getSize()); + for (unsigned i = options.getSize(); i--;) { + vector<unsigned>candidates; + for (unsigned + j = options.getSymbolCount(i), + base = options.getFirstSymbol(i); + j--;) { + candidates.push_back(base + j); + } + unsigned index = rand() % candidates.size(); + unsigned symbol = candidates[index]; + known.append(InputTerm(false, symbol)); + while (!solver(known)) { + known.undoAppend(); + candidates[index] = candidates[candidates.size() - 1]; + candidates.pop_back(); + index = rand() % candidates.size(); + symbol = candidates[index]; + known.append(InputTerm(false, symbol)); + } + result[i] = symbol; + } + return result; +} + +CoveringArray SingleChangeSpace::createStartState(unsigned rows) const { + CoveringArray result(rows, strength, options, solver); + unsigned i = rows; + while (i-->resurrectionBuffer.size()) { + InputKnown known; + result.setBackingArrayRow(i, createRandomMatchingRow(known)); + } + if (resurrectionBuffer.size()) { + for (++i; i--;) { + Array<unsigned>row = resurrectionBuffer[i]; + // We must deep copy to preserve the resurrection buffer. + for (unsigned j = options.getSize(); j--;) { + result.setBackingArrayEntry(i, j, row[j]); + } + } + } + result.setTrackingCoverage(true); + result.setTrackingNoncoverage(true); + return result; +} + +CoverageCost SingleChangeSpace::getTraveled(const CoveringArray&start) const { + return 0; +} + +CoverageCost SingleChangeSpace::getTraveled + (const Node<CoveringArray, CoverageCost>&parent, const CoveringArray&state) + const { + return 0; +} + +set<CoveringArray>SingleChangeSpace::getChildren + (const CoveringArray&state, float proportion) const { + assert(false); // Unimplemented + return getChildren(state, (unsigned)1); +} + +set<CoveringArray>SingleChangeSpace::getChildren + (const CoveringArray&state, unsigned count) const { + set<CoveringArray>result; + unsigned rows = state.getRows(); + assert(options.getSize() == state.getOptions()); + assert(state.isTrackingNoncoverage()); + const set<Array<unsigned>, ArrayComparator<unsigned> >&noncoverage = + state.getNoncoverage(); + if (noncoverage.empty()) { + return result; + } + unsigned attempts = 0; + for (unsigned i = count; i; ++attempts) { + unsigned row = rand() % rows; + unsigned option = rand() % options.getSize(); + unsigned value = options.getOtherRandomSymbol(option, state(row, option)); + InputKnown known; + known.append(InputTerm(false, value)); + if (attempts < MAXIMUM_SINGLE_CHANGE_FAILED_ATTEMPTS) { + for (unsigned j = 0; j < option; ++j) { + known.append(InputTerm(false, state(row, j))); + } + for (unsigned j = option + 1; j < options.getSize(); ++j) { + known.append(InputTerm(false, state(row, j))); + } + if (solver(known)) { + CoveringArray child = state; + child(row, option) = value; + result.insert(child); + --i; + attempts = 0; + } + } else { + cout << "Considering a full row change" << endl; + CoveringArray child = state; + child(row) = createRandomMatchingRow(known); + result.insert(child); + --i; + attempts = 0; + } + } + return result; +} + +void SingleChangeSpace::signal + (const SearchFinish<CoveringArray, CoverageCost>&finish) { + const set<const Node<CoveringArray, CoverageCost>*>&best = + finish.source.getBest(); + if (best.empty()) { + return; + } + const CoveringArray&solution = (*best.begin())->getState(); + unsigned rowCount = solution.getRows(); + unsigned optionCount = solution.getOptions(); + resurrectionBuffer.reserve(rowCount); + while (resurrectionBuffer.size() < rowCount) { + resurrectionBuffer.push_back(Array<unsigned>()); + } + cout << "Sorting rows for distinct coverage" << endl; + Array<unsigned>distinctCoverage = solution.countDistinctCoverage(); + Array<unsigned>permutation(rowCount); + for (unsigned i = rowCount; i--;) { + permutation[i] = i; + } + igreater<unsigned>betterDistinctCoverage(distinctCoverage); + sort(permutation + 0, permutation + rowCount, betterDistinctCoverage); + cout << "Saving rows in resurrection buffer" << endl; + for (unsigned i = rowCount; i--;) { + unsigned p = permutation[i]; + Array<unsigned>row(optionCount); + for (unsigned j = optionCount; j--;) { + row[j] = solution(p,j); + } + resurrectionBuffer[i] = row; + } +} + +void SingleChangeSpace::clearResurrectionBuffer() { + resurrectionBuffer.clear(); +} diff --git a/casa/covering/space/SingleChangeSpace.H b/casa/covering/space/SingleChangeSpace.H new file mode 100644 index 0000000..66efbc3 --- /dev/null +++ b/casa/covering/space/SingleChangeSpace.H @@ -0,0 +1,61 @@ +// Copyright 2008, 2009 Brady J. Garvin + +// This file is part of Covering Arrays by Simulated Annealing (CASA). + +// CASA 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 3 of the License, or +// (at your option) any later version. + +// CASA 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 CASA. If not, see <http://www.gnu.org/licenses/>. + + +#ifndef SINGLE_CHANGE_SPACE_H +#define SINGLE_CHANGE_SPACE_H + +#include <cstdlib> +#include <cassert> +#include <vector> + +#include "Array.H" + +#include "covering/space/CoveringArraySpace.H" +#include "covering/cost/CoverageCost.H" + +#include "events/Listener.H" +#include "search/SearchFinish.H" + +class SingleChangeSpace : + public CoveringArraySpace, + public Listener<SearchFinish<CoveringArray, CoverageCost> > { +protected: + std::vector<Array<unsigned> > resurrectionBuffer; + +public: + SingleChangeSpace(unsigned strength, Options options) : + CoveringArraySpace(strength, options) {} + +protected: + Array<unsigned>createRandomMatchingRow(InputKnown&known) const; + +public: + CoveringArray createStartState(unsigned rows) const; + CoverageCost getTraveled(const CoveringArray&start) const; + CoverageCost getTraveled + (const Node<CoveringArray, CoverageCost>&parent, + const CoveringArray&state) const; + std::set<CoveringArray>getChildren + (const CoveringArray&state, float proportion) const; + std::set<CoveringArray>getChildren + (const CoveringArray&state, unsigned count) const; + void signal(const SearchFinish<CoveringArray, CoverageCost>&finish); + void clearResurrectionBuffer(); +}; + +#endif diff --git a/casa/covering/state/CoveringArray.C b/casa/covering/state/CoveringArray.C new file mode 100644 index 0000000..e5aca80 --- /dev/null +++ b/casa/covering/state/CoveringArray.C @@ -0,0 +1,274 @@ +// Copyright 2008, 2009 Brady J. Garvin + +// This file is part of Covering Arrays by Simulated Annealing (CASA). + +// CASA 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 3 of the License, or +// (at your option) any later version. + +// CASA 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 CASA. If not, see <http://www.gnu.org/licenses/>. + + +#include "covering/state/CoveringArray.H" + +using namespace std; + +#ifndef MAXIMUM_COVERING_ARRAY_SUBSTITUTION +#define MAXIMUM_COVERING_ARRAY_SUBSTITUTION 0x40 +#endif + +CoveringArray::CoveringArray + (unsigned rows, unsigned strength, Options options, SATSolver&solver) : + array(rows), + substitutions(new map<pair<unsigned, unsigned>, unsigned>()), + solver(&solver), + trackingCoverage(false), + trackingNoncoverage(false), + coverageCount(0), + multipleCoverageCount(0), + coverage(strength, options), + noncoverage(new set<Array<unsigned>, ArrayComparator<unsigned> >()) { + for (unsigned i = rows; i--;) { + array[i] = Array<unsigned>(options.getSize()); + } + coverage.fill(0); +} + +CoveringArray::CoveringArray(const CoveringArray©) : + array(copy.array), + substitutions(copy.substitutions), + solver(copy.solver), + trackingCoverage(copy.trackingCoverage), + trackingNoncoverage(copy.trackingNoncoverage), + coverageCount(copy.coverageCount), + multipleCoverageCount(copy.multipleCoverageCount), + coverage(copy.coverage), + noncoverage(copy.noncoverage) { + assert(array); +} + +void CoveringArray::setBackingArrayEntry + (unsigned row, unsigned option, unsigned value) { + assert(!substitutions->size()); + array[row][option] = value; +} + +void CoveringArray::setBackingArrayRow(unsigned row, Array<unsigned>value) { + assert(!substitutions->size()); + array[row] = value; +} + +unsigned CoveringArray::getCoverageCount() const { + return coverageCount; +} + +unsigned CoveringArray::getMultipleCoverageCount() const { + return multipleCoverageCount; +} + +Array<unsigned>CoveringArray::countDistinctCoverage() const { + assert(trackingCoverage); + Array<unsigned>result(array.getSize()); + result.fill(0); + unsigned strength = coverage.getStrength(); + unsigned limit = coverage.getOptions().getSize(); + Array<unsigned>firsts = coverage.getOptions().getFirstSymbols(); + Array<unsigned>counts = coverage.getOptions().getSymbolCounts(); + unsigned hint = 0; + for (Array<unsigned> + columns = combinadic.begin(strength), + symbols(strength); + columns[strength - 1]<limit; + combinadic.next(columns), ++hint) { + for (unsigned i = array.getSize(); i--;) { + for (unsigned j = strength; j--;) { + symbols[j] = (*this)(i, columns[j]); + } + if (coverage.hintGet(hint, columns, firsts, counts, symbols) == 1) { + ++result[i]; + } + } + } + return result; +} + +bool CoveringArray::operator <(const CoveringArray&other) const { + return this < &other; +} +bool CoveringArray::operator >(const CoveringArray&other) const { + return this > &other; +} +bool CoveringArray::operator ==(const CoveringArray&other) const { + return this == &other; +} +bool CoveringArray::operator !=(const CoveringArray&other) const { + return this != &other; +} + +void CoveringArray::finalizeSubstitutions() { + unsigned outer = getRows(); + unsigned inner = getOptions(); + Array<Array<unsigned> >replacement(outer); + for (unsigned i = outer; i--;) { + replacement[i] = Array<unsigned>(inner); + for (unsigned j = inner; j--;) { + replacement[i][j] = array[i][j]; + } + } + for (map<pair<unsigned, unsigned>, unsigned>::const_iterator + iterator = substitutions->begin(), + end = substitutions->end(); + iterator != end; + ++iterator) { + const pair<unsigned, unsigned>&location = iterator->first; + replacement[location.first][location.second] = iterator->second; + } + substitutions->clear(); + array = replacement; +} + +void CoveringArray::autoFinalizeSubstitutions() { + if (substitutions->size() > MAXIMUM_COVERING_ARRAY_SUBSTITUTION) { + finalizeSubstitutions(); + } +} + +bool CoveringArray::isTrackingCoverage() const { + return trackingCoverage; +} + +void CoveringArray::setTrackingCoverage(bool trackingCoverage) { + if (this->trackingCoverage) { + this->trackingCoverage = trackingCoverage; + return; + } + this->trackingCoverage = trackingCoverage; + if (trackingCoverage) { + unsigned strength = coverage.getStrength(); + unsigned limit = coverage.getOptions().getSize(); + Array<unsigned>firsts = coverage.getOptions().getFirstSymbols(); + Array<unsigned>counts = coverage.getOptions().getSymbolCounts(); + coverage.fill(0); + coverageCount = 0; + multipleCoverageCount = 0; + if (substitutions->size()) { + unsigned hint = 0; + for (Array<unsigned> + columns = combinadic.begin(strength), + symbols(strength); + columns[strength - 1] < limit; + combinadic.next(columns), ++hint) { + for (unsigned i = array.getSize();i--;) { + for (unsigned j = strength;j--;) { + symbols[j] = (*this)(i, columns[j]); + } + unsigned newCoverage = + ++coverage.hintGet(hint, columns, firsts, counts, symbols); + if (newCoverage == 1) { + ++coverageCount; + } + if (newCoverage>1) { + ++multipleCoverageCount; + } + } + } + } else { + // A special common case where we can bypass the () operator: + unsigned hint = 0; + for (Array<unsigned> + columns = combinadic.begin(strength), + symbols(strength); + columns[strength - 1] < limit; + combinadic.next(columns), ++hint) { + for (unsigned i = array.getSize(); i--;) { + for (unsigned j = strength; j--;) { + symbols[j] = array[i][columns[j]]; + } + unsigned newCoverage = + ++coverage.hintGet(hint, columns, firsts, counts, symbols); + if (newCoverage == 1) { + ++coverageCount; + } + if (newCoverage>1) { + ++multipleCoverageCount; + } + } + } + } + } +} + +bool CoveringArray::isTrackingNoncoverage() const { + return trackingNoncoverage; +} + +void CoveringArray::setTrackingNoncoverage(bool trackingNoncoverage) { + if (this->trackingNoncoverage) { + this->trackingNoncoverage = trackingNoncoverage; + if (!trackingNoncoverage) { + noncoverage->clear(); + } + return; + } + this->trackingNoncoverage = trackingNoncoverage; + if (trackingNoncoverage) { + assert(trackingCoverage); + assert(noncoverage->empty()); +#ifndef NDEBUG + unsigned impossible = 0; +#endif + for (Coverage<unsigned>::iterator + iterator = coverage.begin(), + end = coverage.end(); + iterator != end; + ++iterator) { + if (!*iterator) { + InputKnown known; + Array<unsigned>combination = iterator.getCombination(); + for (unsigned i = combination.getSize(); i--;) { + known.append(InputTerm(false, combination[i])); + } + if ((*solver)(known)) { + noncoverage->insert(combination); + } +#ifndef NDEBUG + else { + ++impossible; + } +#endif + } + } + assert(coverageCount + noncoverage->size() + impossible == + coverage.getSize()); + } +} + +const set<Array<unsigned>, ArrayComparator<unsigned> >& + CoveringArray::getNoncoverage() const { + return *noncoverage; +} + +ostream&operator <<(ostream&out, const CoveringArray&array) { + out << '{'; + for (unsigned i = 0; i < array.getRows(); ++i) { + out << '['; + for (unsigned j = 0; j < array.getOptions(); ++j) { + out << array(i,j) << ','; + } + out << "X],"; + } + out << "X} -> "; + if (array.isTrackingCoverage()) { + out << array.getCoverageCount(); + }else{ + out << '?'; + } + return out; +} diff --git a/casa/covering/state/CoveringArray.H b/casa/covering/state/CoveringArray.H new file mode 100644 index 0000000..6241230 --- /dev/null +++ b/casa/covering/state/CoveringArray.H @@ -0,0 +1,166 @@ +// Copyright 2008, 2009 Brady J. Garvin + +// This file is part of Covering Arrays by Simulated Annealing (CASA). + +// CASA 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 3 of the License, or +// (at your option) any later version. + +// CASA 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 CASA. If not, see <http://www.gnu.org/licenses/>. + + +#ifndef COVERING_ARRAY_H +#define COVERING_ARRAY_H + +#include <cassert> +#include <iostream> +#include <set> +#include <map> + +#include "Lazy.H" +#include "Array.H" + +#include "covering/bookkeeping/Coverage.H" + +#include "sat/SAT.H" + + +class CoveringArray { +protected: + // The first index is the test configuration (row). + // The second index is the option (column). + Array<Array<unsigned> > array; + Lazy<std::map<std::pair<unsigned, unsigned>, unsigned> > + substitutions; + + SATSolver* solver; + + bool trackingCoverage; + bool trackingNoncoverage; + + unsigned coverageCount; + unsigned multipleCoverageCount; + Coverage<unsigned> coverage; + Lazy<std::set<Array<unsigned>, ArrayComparator<unsigned> > > + noncoverage; + +public: + CoveringArray + (unsigned rows, unsigned strength, Options options, SATSolver&solver); + CoveringArray(const CoveringArray©); + + unsigned getRows() const { + return array.getSize(); + } + unsigned getOptions() const { + return array.getSize() ? array[0].getSize() : 0; + } + + void setBackingArrayEntry(unsigned row, unsigned option, unsigned value); + void setBackingArrayRow(unsigned row, Array<unsigned>value); + + class Entry { + protected: + CoveringArray& owner; + unsigned row; + unsigned option; + public: + Entry(CoveringArray&owner, unsigned row, unsigned option) : + owner(owner), + row(row), + option(option) {} + protected: + void updateTracking(unsigned value); + public: + operator unsigned() const; + Entry&operator =(unsigned value); + }; + + // Warning: CoveringArray::Row assumes that constraints are always satisfied. + class Row { + protected: + CoveringArray& owner; + unsigned row; + public: + Row(CoveringArray&owner, unsigned row) : + owner(owner), + row(row) {} + protected: + void updateTracking(const Array<unsigned>values); + public: + operator Array<unsigned>() const; + Row&operator =(const Array<unsigned>values); + }; + + // Warning: CoveringArray::SubRow assumes that constraints are always + // satisfied. + class SubRow { + protected: + CoveringArray& owner; + unsigned row; + Array<unsigned> columns; + public: + SubRow(CoveringArray&owner, unsigned row, Array<unsigned>columns) : + owner(owner), + row(row), + columns(columns) {} + protected: + void updateTracking(const Array<unsigned>values); + public: + operator Array<unsigned>() const; + SubRow&operator =(const Array<unsigned>values); + }; + + Entry operator ()(unsigned row, unsigned option) { + return Entry(*this, row, option); + } + const Entry operator ()(unsigned row, unsigned option) const { + return Entry(*const_cast<CoveringArray*>(this), row, option); + } + + Row operator ()(unsigned row) { + return Row(*this, row); + } + const Row operator ()(unsigned row) const { + return Row(*const_cast<CoveringArray*>(this), row); + } + + SubRow operator ()(unsigned row, Array<unsigned>columns) { + return SubRow(*this, row, columns); + } + const SubRow operator ()(unsigned row, Array<unsigned>columns) const { + return SubRow(*const_cast<CoveringArray*>(this), row, columns); + } + + unsigned getCoverageCount() const; + unsigned getMultipleCoverageCount() const; + Array<unsigned>countDistinctCoverage() const; + + bool operator <(const CoveringArray&other) const; + bool operator >(const CoveringArray&other) const; + bool operator ==(const CoveringArray&other) const; + bool operator !=(const CoveringArray&other) const; + + void finalizeSubstitutions(); + void autoFinalizeSubstitutions(); + + bool isTrackingCoverage() const; + void setTrackingCoverage(bool trackingCoverage); + + bool isTrackingNoncoverage() const; + void setTrackingNoncoverage(bool trackingNoncoverage); + + const std::set<Array<unsigned>, ArrayComparator<unsigned> >&getNoncoverage() + const; +}; + +std::ostream&operator <<(std::ostream&out,const CoveringArray&array); + +#endif diff --git a/casa/covering/state/CoveringArrayEntry.C b/casa/covering/state/CoveringArrayEntry.C new file mode 100644 index 0000000..73e6e24 --- /dev/null +++ b/casa/covering/state/CoveringArrayEntry.C @@ -0,0 +1,102 @@ +// Copyright 2008, 2009 Brady J. Garvin + +// This file is part of Covering Arrays by Simulated Annealing (CASA). + +// CASA 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 3 of the License, or +// (at your option) any later version. + +// CASA 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 CASA. If not, see <http://www.gnu.org/licenses/>. + + +#include "covering/state/CoveringArray.H" + +using namespace std; + +void CoveringArray::Entry::updateTracking(unsigned value) { + if (owner(row,option) == value) { + return; + } + unsigned strength = owner.coverage.getStrength(); + unsigned limit = owner.coverage.getOptions().getSize(); + Array<unsigned>firsts = owner.coverage.getOptions().getFirstSymbols(); + Array<unsigned>counts = owner.coverage.getOptions().getSymbolCounts(); + unsigned hint = 0; + for (Array<unsigned> + columns = combinadic.begin(strength), + symbols(strength); + columns[strength - 1] < limit; + combinadic.next(columns), ++hint) { + for (unsigned i = strength; i--;) { + if (columns[i] == option) { + for (unsigned j = strength; j--;) { + symbols[j] = owner(row, columns[j]); + } + InputKnown oldKnown(symbols); + if ((*owner.solver)(oldKnown) && + --owner.coverage.hintGet(hint, columns, firsts, counts, symbols) == + 0) { + --owner.coverageCount; + if (owner.trackingNoncoverage) { + Array<unsigned>separateCopyOfSymbols(symbols.getSize()); + for (unsigned j = symbols.getSize(); j--;) { + separateCopyOfSymbols[j] = symbols[j]; + } + bool successfulInsertion = + owner.noncoverage->insert(separateCopyOfSymbols).second; + assert(successfulInsertion); + (void)successfulInsertion; // This is unused without assertions. + } + } else { + --owner.multipleCoverageCount; + } + symbols[i] = value; + InputKnown newKnown(symbols); + if ((*owner.solver)(newKnown) && + ++owner.coverage.hintGet(hint, columns, firsts, counts, symbols) == + 1) { + ++owner.coverageCount; + if (owner.trackingNoncoverage) { + Array<unsigned>separateCopyOfSymbols(symbols.getSize()); + for (unsigned j = symbols.getSize(); j--;) { + separateCopyOfSymbols[j] = symbols[j]; + } + bool successfulErasure = + (bool)owner.noncoverage->erase(separateCopyOfSymbols); + assert(successfulErasure); + (void)successfulErasure; // This is unused without assertions. + } + } else { + ++owner.multipleCoverageCount; + } + break; + } + } + } + owner.autoFinalizeSubstitutions(); +} + +CoveringArray::Entry::operator unsigned() const { + map<pair<unsigned, unsigned>, unsigned>::const_iterator + substitution = + owner.substitutions->find(pair<unsigned, unsigned>(row,option)), + end = owner.substitutions->end(); + return (substitution == end) ? + owner.array[row][option] : + substitution->second; +} + +CoveringArray::Entry&CoveringArray::Entry::operator =(unsigned value) { + if (owner.trackingCoverage) { + updateTracking(value); + } + (*owner.substitutions)[pair<unsigned, unsigned>(row, option)] = value; + return *this; +} diff --git a/casa/covering/state/CoveringArrayRow.C b/casa/covering/state/CoveringArrayRow.C new file mode 100644 index 0000000..10f0a45 --- /dev/null +++ b/casa/covering/state/CoveringArrayRow.C @@ -0,0 +1,113 @@ +// Copyright 2008, 2009 Brady J. Garvin + +// This file is part of Covering Arrays by Simulated Annealing (CASA). + +// CASA 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 3 of the License, or +// (at your option) any later version. + +// CASA 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 CASA. If not, see <http://www.gnu.org/licenses/>. + + +#include "covering/state/CoveringArray.H" + +using namespace std; + +void CoveringArray::Row::updateTracking(const Array<unsigned>values) { + unsigned size = values.getSize(); + assert(size == owner.getOptions()); + unsigned strength = owner.coverage.getStrength(); + unsigned limit = owner.coverage.getOptions().getSize(); + Array<unsigned>oldRow(size); + for (unsigned i = size; i--;) { + oldRow[i] = owner(row, i); + } + Array<unsigned>firsts = owner.coverage.getOptions().getFirstSymbols(); + Array<unsigned>counts = owner.coverage.getOptions().getSymbolCounts(); + unsigned hint = 0; + for (Array<unsigned> + columns = combinadic.begin(strength), + oldSymbols(strength), + newSymbols(strength); + columns[strength - 1] < limit; + combinadic.next(columns), ++hint) { + bool unchanged = true; + for (unsigned j = strength; j--;) { + unsigned column = columns[j]; + oldSymbols[j] = oldRow[column]; + newSymbols[j] = values[column]; + if (oldSymbols[j] != newSymbols[j]) { + unchanged = false; + } + } + if (unchanged) { + continue; + } + InputKnown oldKnown(oldSymbols); + InputKnown newKnown(newSymbols); + if (--owner.coverage.hintGet(hint, columns, firsts, counts, oldSymbols) == + 0) { + --owner.coverageCount; + if (owner.trackingNoncoverage) { + Array<unsigned>separateCopyOfSymbols(oldSymbols.getSize()); + for (unsigned j = oldSymbols.getSize(); j--;) { + separateCopyOfSymbols[j] = oldSymbols[j]; + } + bool successfulInsertion = + owner.noncoverage->insert(separateCopyOfSymbols).second; + assert(successfulInsertion); + (void)successfulInsertion; //This is unused without assertions. + } + } else { + --owner.multipleCoverageCount; + } + if (++owner.coverage.hintGet(hint, columns, firsts, counts, newSymbols) == + 1) { + ++owner.coverageCount; + if (owner.trackingNoncoverage) { + Array<unsigned>separateCopyOfSymbols(newSymbols.getSize()); + for (unsigned j = newSymbols.getSize(); j--;) { + separateCopyOfSymbols[j] = newSymbols[j]; + } + bool successfulErasure = + (bool)owner.noncoverage->erase(separateCopyOfSymbols); + assert(successfulErasure); + (void)successfulErasure; // This is unused without assertions. + } + } else { + ++owner.multipleCoverageCount; + } + } + owner.autoFinalizeSubstitutions(); +} + +CoveringArray::Row::operator Array<unsigned>() const { + typedef map<pair<unsigned,unsigned>,unsigned>::const_iterator Substitution; + Substitution end = owner.substitutions->end(); + Array<unsigned>result(owner.getOptions()); + for (pair<unsigned, unsigned>key(row, result.getSize()); key.second--;) { + Substitution substitution = owner.substitutions->find(key); + result[key.second] = + (substitution == end) ? + owner.array[row][key.second] : + substitution->second; + } + return result; +} + +CoveringArray::Row&CoveringArray::Row::operator =(const Array<unsigned>values) { + if (owner.trackingCoverage) { + updateTracking(values); + } + for (pair<unsigned, unsigned>key(row, owner.getOptions()); key.second--;) { + (*owner.substitutions)[key] = values[key.second]; + } + return *this; +} diff --git a/casa/covering/state/CoveringArraySubRow.C b/casa/covering/state/CoveringArraySubRow.C new file mode 100644 index 0000000..b66f546 --- /dev/null +++ b/casa/covering/state/CoveringArraySubRow.C @@ -0,0 +1,129 @@ +// Copyright 2008, 2009 Brady J. Garvin + +// This file is part of Covering Arrays by Simulated Annealing (CASA). + +// CASA 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 3 of the License, or +// (at your option) any later version. + +// CASA 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 CASA. If not, see <http://www.gnu.org/licenses/>. + + +#include "covering/state/CoveringArray.H" +#include "CombinadicIterator.H" + +using namespace std; + +void CoveringArray::SubRow::updateTracking(const Array<unsigned>values) { + assert(values.getSize() == columns.getSize()); + const Options&options = owner.coverage.getOptions(); + unsigned strength = owner.coverage.getStrength(); + unsigned limit = options.getSize(); + unsigned changes = 0; + Array<unsigned>oldRow(limit); + Array<unsigned>newRow(limit); + Array<unsigned>changedColumns(columns.getSize()); + for (unsigned i = limit; i--;) { + oldRow[i] = owner(row, i); + } + for (unsigned i = limit, j = values.getSize(); i--;) { + if (j && (columns[j - 1] == i)) { + newRow[i] = values[--j]; + } else { + newRow[i] = oldRow[i]; + } + } + for (unsigned i = 0; i < limit; ++i) { + if (newRow[i] != oldRow[i]) { + changedColumns[changes++] = i; + } + } + changedColumns = Array<unsigned>(changedColumns, changes); + Array<unsigned>firsts = options.getFirstSymbols(); + Array<unsigned>counts = options.getSymbolCounts(); + for (CombinadicIterator combo(limit, strength, changedColumns); + combo; + ++combo) { + const Array<unsigned>updateColumns = *combo; + Array<unsigned>oldSymbols(strength); + Array<unsigned>newSymbols(strength); + for (unsigned j = strength; j--;) { + unsigned column = updateColumns[j]; + oldSymbols[j] = oldRow[column]; + newSymbols[j] = newRow[column]; + } + Coverage<unsigned>::Entry lost = + owner.coverage.hintGet(updateColumns, firsts, counts, oldSymbols); + assert(lost); // Assert that what we lost is something we had to lose. + if (--lost == 0) { + --owner.coverageCount; + if (owner.trackingNoncoverage) { + Array<unsigned>separateCopyOfSymbols(oldSymbols.getSize()); + for (unsigned j = oldSymbols.getSize(); j--;) { + separateCopyOfSymbols[j] = oldSymbols[j]; + } + bool successfulInsertion = + owner.noncoverage->insert(separateCopyOfSymbols).second; + assert(successfulInsertion); + (void)successfulInsertion; // This is unused without assertions. + } + } else { + --owner.multipleCoverageCount; + } + Coverage<unsigned>::Entry gained = + owner.coverage.hintGet(updateColumns, firsts, counts, newSymbols); + if (++gained == 1) { + ++owner.coverageCount; + if (owner.trackingNoncoverage) { + Array<unsigned>separateCopyOfSymbols(newSymbols.getSize()); + for (unsigned j = newSymbols.getSize(); j--;) { + separateCopyOfSymbols[j] = newSymbols[j]; + } + bool successfulErasure = + (bool)owner.noncoverage->erase(separateCopyOfSymbols); + assert(successfulErasure); + (void)successfulErasure; // This is unused without assertions. + } + } else { + ++owner.multipleCoverageCount; + } + } + owner.autoFinalizeSubstitutions(); +} + +CoveringArray::SubRow::operator Array<unsigned>() const { + typedef map<pair<unsigned, unsigned>, unsigned>::const_iterator Substitution; + Substitution end = owner.substitutions->end(); + unsigned size = columns.getSize(); + Array<unsigned>result(size); + pair<unsigned, unsigned>key(row,0); + for (unsigned i = size; i--;) { + key.second = columns[i]; + Substitution substitution = owner.substitutions->find(key); + result[i] = + (substitution == end) ? + owner.array[row][key.second] : + substitution->second; + } + return result; +} +CoveringArray::SubRow&CoveringArray::SubRow::operator = + (const Array<unsigned>values) { + assert(values.getSize() == columns.getSize()); + if (owner.trackingCoverage) { + updateTracking(values); + } + pair<unsigned, unsigned>key(row, 0); + for (unsigned i = columns.getSize(); i--;) { + key.second = columns[i]; + (*owner.substitutions)[key] = values[i]; + } + return *this; +} diff --git a/casa/events/EventSource.H b/casa/events/EventSource.H new file mode 100644 index 0000000..38097f4 --- /dev/null +++ b/casa/events/EventSource.H @@ -0,0 +1,59 @@ +// Copyright 2008, 2009 Brady J. Garvin + +// This file is part of Covering Arrays by Simulated Annealing (CASA). + +// CASA 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 3 of the License, or +// (at your option) any later version. + +// CASA 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 CASA. If not, see <http://www.gnu.org/licenses/>. + + +#ifndef EVENT_SOURCE_H +#define EVENT_SOURCE_H + +#include <set> +#include "events/Listener.H" + +template<class MESSAGE>class EventSource { +public: + typedef Listener<MESSAGE> ListenerT; + +private: + std::set<ListenerT*> listeners; + +public: + virtual ~EventSource() {} + bool isListener(const ListenerT&listener) const { + return listeners.find(&listener) != listeners.end(); + } + void addListener(ListenerT&listener) { + listeners.insert(&listener); + } + void removeListener(ListenerT&listener) { + listeners.erase(&listener); + } + void removeAllListeners() { + listeners.clear(); + } + +protected: + void dispatch(const MESSAGE&message) { + for(typename std::set<ListenerT*>::iterator iterator = + listeners.begin(), + end = listeners.end(); + iterator != end; + ++iterator) { + (*iterator)->signal(message); + } + } +}; + +#endif diff --git a/casa/events/Listener.H b/casa/events/Listener.H new file mode 100644 index 0000000..45831de --- /dev/null +++ b/casa/events/Listener.H @@ -0,0 +1,28 @@ +// Copyright 2008, 2009 Brady J. Garvin + +// This file is part of Covering Arrays by Simulated Annealing (CASA). + +// CASA 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 3 of the License, or +// (at your option) any later version. + +// CASA 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 CASA. If not, see <http://www.gnu.org/licenses/>. + + +#ifndef LISTENER_H +#define LISTENER_H + +template<class MESSAGE>class Listener { +public: + virtual ~Listener() {} + virtual void signal(const MESSAGE&message) = 0; +}; + +#endif diff --git a/casa/io/ConstraintFile.C b/casa/io/ConstraintFile.C new file mode 100644 index 0000000..6ea05b2 --- /dev/null +++ b/casa/io/ConstraintFile.C @@ -0,0 +1,50 @@ +// Copyright 2008, 2009 Brady J. Garvin + +// This file is part of Covering Arrays by Simulated Annealing (CASA). + +// CASA 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 3 of the License, or +// (at your option) any later version. + +// CASA 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 CASA. If not, see <http://www.gnu.org/licenses/>. + + +#include "io/ConstraintFile.H" + +using namespace std; + +ConstraintFile::ConstraintFile(const string&filename) { + if (!filename.size()) { + return; + } + ifstream fileInputStream(filename.data()); + unsigned clauseCount; + fileInputStream >> clauseCount; + clauses = Array<InputClause>(clauseCount); + for (unsigned i = 0; i < clauseCount; ++i) { + InputClause&clause = clauses[i]; + unsigned termCount; + fileInputStream >> termCount; + while (termCount--) { + char sign; + unsigned symbol; + do { + fileInputStream >> sign; + } while (sign != '-' && sign != '+'); + fileInputStream >> symbol; + clause.append(InputTerm(sign == '-', symbol)); + } + } + fileInputStream.close(); +} + +const Array<InputClause>&ConstraintFile::getClauses() const { + return clauses; +} diff --git a/casa/io/ConstraintFile.H b/casa/io/ConstraintFile.H new file mode 100644 index 0000000..cfdb685 --- /dev/null +++ b/casa/io/ConstraintFile.H @@ -0,0 +1,35 @@ +// Copyright 2008, 2009 Brady J. Garvin + +// This file is part of Covering Arrays by Simulated Annealing (CASA). + +// CASA 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 3 of the License, or +// (at your option) any later version. + +// CASA 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 CASA. If not, see <http://www.gnu.org/licenses/>. + + +#ifndef CONSTRAINT_FILE_H +#define CONSTRAINT_FILE_H + +#include <fstream> +#include <string> + +#include "Array.H" +#include "sat/SAT.H" + +class ConstraintFile { + Array<InputClause> clauses; +public: + ConstraintFile(const std::string&filename); + const Array<InputClause>&getClauses() const; +}; + +#endif diff --git a/casa/io/OutputFile.C b/casa/io/OutputFile.C new file mode 100644 index 0000000..43000ff --- /dev/null +++ b/casa/io/OutputFile.C @@ -0,0 +1,50 @@ +// Copyright 2008, 2009 Brady J. Garvin + +// This file is part of Covering Arrays by Simulated Annealing (CASA). + +// CASA 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 3 of the License, or +// (at your option) any later version. + +// CASA 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 CASA. If not, see <http://www.gnu.org/licenses/>. + + +#include "io/OutputFile.H" + +using namespace std; + +OutputFile::OutputFile(const string&filename) : + filename(filename) {} + +void OutputFile::setCoveringArray(const CoveringArray&array) { + unsigned rows = array.getRows(); + unsigned options = array.getOptions(); + this->array = Array<Array<unsigned> >(rows); + for (unsigned i = rows; i--;) { + Array<unsigned>&row = this->array[i] = Array<unsigned>(options); + for (unsigned j = options; j--;) { + row[j] = array(i, j); + } + } +} + +void OutputFile::write() const { + ofstream fileOutputStream(filename.data()); + fileOutputStream << array.getSize() << '\n'; + for (unsigned i = 0;i < array.getSize(); ++i) { + const Array<unsigned>&row = array[i]; + fileOutputStream << row[0]; + for (unsigned j = 1; j < row.getSize(); ++j) { + fileOutputStream << ' ' << row[j]; + } + fileOutputStream << '\n'; + } + fileOutputStream.close(); +} diff --git a/casa/io/OutputFile.H b/casa/io/OutputFile.H new file mode 100644 index 0000000..b89345b --- /dev/null +++ b/casa/io/OutputFile.H @@ -0,0 +1,38 @@ +// Copyright 2008, 2009 Brady J. Garvin + +// This file is part of Covering Arrays by Simulated Annealing (CASA). + +// CASA 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 3 of the License, or +// (at your option) any later version. + +// CASA 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 CASA. If not, see <http://www.gnu.org/licenses/>. + + +#ifndef OUTPUT_FILE_H +#define OUTPUT_FILE_H + +#include <fstream> +#include <string> + +#include "Array.H" +#include "covering/state/CoveringArray.H" + +class OutputFile { +protected: + std::string filename; + Array<Array<unsigned> > array; +public: + OutputFile(const std::string&filename); + void setCoveringArray(const CoveringArray&array); + void write() const; +}; + +#endif diff --git a/casa/io/SpecificationFile.C b/casa/io/SpecificationFile.C new file mode 100644 index 0000000..8fba427 --- /dev/null +++ b/casa/io/SpecificationFile.C @@ -0,0 +1,39 @@ +// Copyright 2008, 2009 Brady J. Garvin + +// This file is part of Covering Arrays by Simulated Annealing (CASA). + +// CASA 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 3 of the License, or +// (at your option) any later version. + +// CASA 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 CASA. If not, see <http://www.gnu.org/licenses/>. + + +#include "io/SpecificationFile.H" + +using namespace std; + +SpecificationFile::SpecificationFile(const string&filename) { + ifstream fileInputStream(filename.data()); + unsigned optionCount; + fileInputStream >> strength >> optionCount; + Array<unsigned>values(optionCount); + for(unsigned i = 0; i < optionCount; ++i) { + fileInputStream >> values[i]; + } + options = Options(values); + fileInputStream.close(); +} +unsigned SpecificationFile::getStrength() const { + return strength; +} +const Options&SpecificationFile::getOptions() const { + return options; +} diff --git a/casa/io/SpecificationFile.H b/casa/io/SpecificationFile.H new file mode 100644 index 0000000..b027460 --- /dev/null +++ b/casa/io/SpecificationFile.H @@ -0,0 +1,37 @@ +// Copyright 2008, 2009 Brady J. Garvin + +// This file is part of Covering Arrays by Simulated Annealing (CASA). + +// CASA 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 3 of the License, or +// (at your option) any later version. + +// CASA 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 CASA. If not, see <http://www.gnu.org/licenses/>. + + +#ifndef SPECIFICATION_FILE_H +#define SPECIFICATION_FILE_H + +#include <fstream> +#include <string> + +#include "Array.H" +#include "covering/bookkeeping/Options.H" + +class SpecificationFile { + unsigned strength; + Options options; +public: + SpecificationFile(const std::string&filename); + unsigned getStrength() const; + const Options&getOptions() const; +}; + +#endif diff --git a/casa/io/Usage.C b/casa/io/Usage.C new file mode 100644 index 0000000..676e374 --- /dev/null +++ b/casa/io/Usage.C @@ -0,0 +1,187 @@ +// Copyright 2008, 2009 Brady J. Garvin + +// This file is part of Covering Arrays by Simulated Annealing (CASA). + +// CASA 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 3 of the License, or +// (at your option) any later version. + +// CASA 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 CASA. If not, see <http://www.gnu.org/licenses/>. + + +#include <cstdlib> +#include <iostream> +#include <posix/getopt.h> + +#include "io/Usage.H" + +using namespace std; + +const char*PROGRAM_NAME = + "Covering Arrays by Simulated Annealing (CASA)"; + +const char*PROGRAM_VERSION = + "1.1b"; + +const char*BUG_ADDRESS = + "bgarvin@cse.unl.edu"; + +static const char*PROGRAM_DOC = + "Builds mixed-level covering arrays under constraints\n" + "\n" + "Copyright 2008, 2009 Brady J. Garvin\n" + "\n" + "CASA is free software: you can redistribute it and/or modify it\n" + "under the terms of the GNU General Public License as published by\n" + "the Free Software Foundation, either version 3 of the License, or\n" + "(at your option) any later version.\n" + "\n" + "CASA is distributed in the hope that it will be useful, but\n" + "WITHOUT ANY WARRANTY; without even the implied warranty of\n" + "MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the\n" + "GNU General Public License for more details.\n" + "\n" + "You should have received a copy of the GNU General Public License\n" + "along with CASA. If not, see <http://www.gnu.org/licenses/>.\n"; + +static const char*USAGE_DOC = + "[OPTIONS] [MODEL_FILE]"; + +static const char*ARG_DOC = + " -o, --output [FILE] write to the given file, regardless of seed\n" + " -c, --constrain [FILE] incorporate the given constraint file\n" + "\n" + " -s, --seed [SEED] set the seed value for the random number generator\n" + "\n" + " -i, --iterations [COUNT] set the initial number of iterations allowed at each array size\n" + " -r, --retries [COUNT] set the number of retries allowed at the same array size\n" + " -p, --partition [RATIO] set the weight of the upper bound in the binary search parition\n" + "\n" + " -t, --temperature [TEMP] set the initial temperature\n" + " -d, --multiplier [RATIO] set the temperature multiplier applied each iteration\n" + "\n" + " -l, --lower-bound [SIZE] let the covering array be no smaller than the given size\n" + " -u, --upper-bound [SIZE] let the covering array be no larger than the given size\n" + " -n, --known-size [SIZE] lock the covering array at the given size\n" + "\n" + " -v, --version show the current version and exit\n" + " -h, --help show this help and exit\n"; + +static const char*shortOptions = + "o:c:s:i:r:p:t:d:l:u:n:vh"; + +static struct option longOptions[] = { + {"output", required_argument, NULL, 'o'}, + {"constrain", required_argument, NULL, 'c'}, + {"seed", required_argument, NULL, 's'}, + {"iterations", required_argument, NULL, 'i'}, + {"retries", required_argument, NULL, 'r'}, + {"partition", required_argument, NULL, 'p'}, + {"temperature", required_argument, NULL, 't'}, + {"decrement", required_argument, NULL, 'd'}, + {"lower-bound", required_argument, NULL, 'l'}, + {"upper-bound", required_argument, NULL, 'u'}, + {"known-size", required_argument, NULL, 'n'}, + {"version", no_argument, NULL, 'v'}, + {"help", no_argument, NULL, 'h'}, + {0, 0, 0, 0 }}; + +bool verbose = true; +const char* modelFile = NULL; +const char* constraintFile = NULL; +const char* outputFile = NULL; +bool seeded = false; +int seed; +double startingTemperature = 0.5L; +double decrement = 0.99999L; +unsigned iterations = 256; +unsigned retries = 2; +unsigned lowerBound = 0; +unsigned upperBound = 0; +double searchPartition = 2.L/3.L; + +static void version() { + cerr << PROGRAM_NAME << ' ' << PROGRAM_VERSION << '\n'; + exit(0); +} + +static const char*name; +static void usage(int error) { + cerr << PROGRAM_NAME << ' ' << PROGRAM_VERSION << " - " << PROGRAM_DOC << + "\n\nUsage: " << name << ' ' << USAGE_DOC << "\n\n" << ARG_DOC << "\n\n" << + "Send bug reports to <" << BUG_ADDRESS << ">.\n"; + exit(error); +} + +void parseOptions(int argc, char*const*argv) { + name = *argv; + bool seen[256]; + (void)seen; // Workaround for a bug in some versions of GCC + for (unsigned i = 256; i-- > 0;) { + seen[i] = false; + } + for (;;) { + int index = 0; + int found = getopt_long(argc, argv, shortOptions, longOptions, &index); + switch (found) { + case 'o': // output + outputFile = optarg; + break; + case 'c': // constrain + constraintFile = optarg; + break; + case 's': // seed + seeded = true; + seed = atoi(optarg); + break; + case 'i': // iterations + iterations = atoi(optarg); + break; + case 'r': // retries + retries = atoi(optarg); + break; + case 'p': // partition + searchPartition = atof(optarg); + break; + case 't': // temperature + startingTemperature = atof(optarg); + break; + case 'd': // decrement + decrement = atof(optarg); + break; + case 'l': // lower-bound + lowerBound = atoi(optarg); + break; + case 'u': // upper-bound + upperBound = atoi(optarg); + break; + case 'n': // known-size + lowerBound = upperBound = atoi(optarg); + break; + case 'v': // version + version(); + break; + case 'h': // help + usage(0); + break; + default: // done with options + if (argc - optind < 1) { + usage(1); + } + if (argc - optind > 1) { + cerr << "Warning: ignoring extraneous arguments after model file ``" << + argv[optind] << "''." << endl; + } + modelFile = argv[optind]; + return; + } + seen[(unsigned)found] = true; + } +} diff --git a/casa/io/Usage.H b/casa/io/Usage.H new file mode 100644 index 0000000..a817be3 --- /dev/null +++ b/casa/io/Usage.H @@ -0,0 +1,38 @@ +// Copyright 2008, 2009 Brady J. Garvin + +// This file is part of Covering Arrays by Simulated Annealing (CASA). + +// CASA 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 3 of the License, or +// (at your option) any later version. + +// CASA 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 CASA. If not, see <http://www.gnu.org/licenses/>. + + +#ifndef USAGE_H +#define USAGE_H + +extern bool verbose; +extern const char* modelFile; +extern const char* constraintFile; +extern const char* outputFile; +extern bool seeded; +extern int seed; +extern double startingTemperature; +extern double decrement; +extern unsigned iterations; +extern unsigned retries; +extern unsigned lowerBound; +extern unsigned upperBound; +extern double searchPartition; + +void parseOptions(int argc, char*const*argv); + +#endif diff --git a/casa/sat/SAT.C b/casa/sat/SAT.C new file mode 100644 index 0000000..161049b --- /dev/null +++ b/casa/sat/SAT.C @@ -0,0 +1,81 @@ +// Copyright 2008, 2009 Brady J. Garvin + +// This file is part of Covering Arrays by Simulated Annealing (CASA). + +// CASA 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 3 of the License, or +// (at your option) any later version. + +// CASA 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 CASA. If not, see <http://www.gnu.org/licenses/>. + + +// Other SAT solvers can be substituted by altering SAT.H and SAT.C. + +#include "sat/SAT.H" + +InputClause::InputClause() : + maxVariable(-1) {} + +InputClause::InputClause(Array<InputTerm>terms) : + maxVariable(-1) { + unsigned size = terms.getSize(); + for (unsigned i = 0; i < size; ++i) { + append(terms[i]); + } +} + +InputClause::InputClause(Array<unsigned>symbols) : + maxVariable(-1) { + unsigned size = symbols.getSize(); + for (unsigned i = 0; i < size; ++i) { + append(InputTerm(false, symbols[i])); + } +} + +InputClause::~InputClause() {} + +InputClause::operator vec<Lit>&() { + return literals; +} +InputClause::operator const vec<Lit>&() const { + return literals; +} + +void InputClause::clear(){ + literals.clear(); +} + +void InputClause::append(InputTerm term) { + int variable = term.getVariable(); + if (variable > maxVariable) { + maxVariable = variable; + } + literals.push(term.isNegated() ? ~Lit(variable) : Lit(variable)); +} + +void InputClause::undoAppend() { + literals.pop(); +} + +void SATSolver::reserve(int variables) { + while (variables >= solver.nVars()) { + solver.newVar(); + } +} + +void SATSolver::addClause(InputClause&clause) { + reserve(clause.getMaxVariable()); + solver.addClause(clause); +} + +bool SATSolver::operator()(const InputKnown&known) { + reserve(known.getMaxVariable()); + return solver.simplify() && solver.solve(known); +} diff --git a/casa/sat/SAT.H b/casa/sat/SAT.H new file mode 100644 index 0000000..0dd3467 --- /dev/null +++ b/casa/sat/SAT.H @@ -0,0 +1,92 @@ +// Copyright 2008, 2009 Brady J. Garvin + +// This file is part of Covering Arrays by Simulated Annealing (CASA). + +// CASA 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 3 of the License, or +// (at your option) any later version. + +// CASA 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 CASA. If not, see <http://www.gnu.org/licenses/>. + + +// Other SAT solvers can be substituted by altering SAT.H and SAT.C. + +#ifndef SAT_H +#define SAT_H + +#include "Array.H" +#include "Solver.H" + +// A literal in a SAT clause. +class InputTerm { +protected: + int encoding; +public: + InputTerm() : + encoding(0) {} + InputTerm(int encoding) : + encoding(encoding) {} + InputTerm(bool negated, int variable) : + encoding( (variable << 1) | (int)negated) {} + + operator int() const { + return encoding; + } + InputTerm&operator =(int encoding) { + this->encoding = encoding; + return *this; + } + + bool isNegated() const { + return encoding & 1; + } + int getVariable() const { + return encoding >> 1; + } +}; + +// A SAT clause. +class InputClause { +protected: + int maxVariable; + vec<Lit> literals; +public: + InputClause(); + InputClause(Array<InputTerm>terms); + InputClause(Array<unsigned>symbols); + virtual ~InputClause(); + + operator vec<Lit>&(); + operator const vec<Lit>&() const; + + int getMaxVariable() const { + return maxVariable; + } + + void clear(); + void append(InputTerm term); + void undoAppend(); +}; + +// A partial assignment. +typedef InputClause InputKnown; + +// A solver-wrapping class. +class SATSolver { +protected: + // The miniSAT implementation. + Solver solver; +public: + void reserve(int variables); + void addClause(InputClause&clause); + bool operator ()(const InputKnown&known); +}; + +#endif diff --git a/casa/search/Filter.H b/casa/search/Filter.H new file mode 100644 index 0000000..071eb71 --- /dev/null +++ b/casa/search/Filter.H @@ -0,0 +1,60 @@ +// Copyright 2008, 2009 Brady J. Garvin + +// This file is part of Covering Arrays by Simulated Annealing (CASA). + +// CASA 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 3 of the License, or +// (at your option) any later version. + +// CASA 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 CASA. If not, see <http://www.gnu.org/licenses/>. + + +#ifndef FILTER_H +#define FILTER_H + +#include <set> + +#include "search/Heuristic.H" +#include "search/Goal.H" + +// Controls which children (immediately reachable neighbors) are explored by a +// search. The filtering happens after children are enumerated; limitations that +// apply to the enumeration process itself (such as only computing a fixed +// number of random children) are better managed by the parameters in a +// SearchConfiguration, which are passed to the getChildren() method of the +// StateSpace. + +template<class STATE, class COST>class Filter { +public: + typedef Heuristic<STATE,COST> HeuristicT; + typedef Goal<STATE> GoalT; + + virtual ~Filter() {} + + // Mutates the children set; the heuristic and goal may guide the mutation. + virtual void operator() + (std::set<STATE>&children, const HeuristicT&heuristic, const GoalT&goal) + const {} + + // Just as the other operator(), but, at the filter's option, the parent may + // be considered to be its own child. This is useful, for example, when the + // SearchConfiguration is sampling a random subset of the children and the + // filter would prefer a different pool to choose from. + virtual void operator() + (std::set<STATE>&children, + const STATE&parent, + const HeuristicT&heuristic, + const GoalT&goal) const { + children.insert(parent); + operator()(children, heuristic, goal); + } +}; + +#endif diff --git a/casa/search/Goal.H b/casa/search/Goal.H new file mode 100644 index 0000000..d7209c8 --- /dev/null +++ b/casa/search/Goal.H @@ -0,0 +1,32 @@ +// Copyright 2008, 2009 Brady J. Garvin + +// This file is part of Covering Arrays by Simulated Annealing (CASA). + +// CASA 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 3 of the License, or +// (at your option) any later version. + +// CASA 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 CASA. If not, see <http://www.gnu.org/licenses/>. + + +#ifndef GOAL_H +#define GOAL_H + +// Decides when a search should terminate because it has found a solution. In +// some applications the goal's RTTI is also used to inform other search objects +// (such as the heuristic). + +template<class STATE>class Goal { +public: + virtual ~Goal() {} + virtual bool isGoal(const STATE&state) = 0; +}; + +#endif diff --git a/casa/search/GreedyFilter.H b/casa/search/GreedyFilter.H new file mode 100644 index 0000000..47ddef4 --- /dev/null +++ b/casa/search/GreedyFilter.H @@ -0,0 +1,64 @@ +// Copyright 2008, 2009 Brady J. Garvin + +// This file is part of Covering Arrays by Simulated Annealing (CASA). + +// CASA 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 3 of the License, or +// (at your option) any later version. + +// CASA 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 CASA. If not, see <http://www.gnu.org/licenses/>. + + +#ifndef GREEDYFILTER_H +#define GREEDYFILTER_H + +#include "search/Filter.H" + +// A specialization of Filter where only the heuristically best child is +// explored. Furthermore, if given the option to treat the parent as a child, +// the filter will only have the search explore children if at least one of them +// is heuristically better than the parent. + +template<class STATE, class COST>class GreedyFilter : + public Filter<STATE, COST> { + typedef Heuristic<STATE, COST> HeuristicT; + typedef Goal<STATE> GoalT; + +public: + void operator() + (std::set<STATE>&children, const HeuristicT&heuristic, const GoalT&goal) + const { + typename std::set<STATE>::iterator best = children.end(); + COST score = 0; + for(typename std::set<STATE>::iterator + iterator = children.begin(), + end = children.end(); + iterator != end; + ++iterator) { + COST estimate = heuristic.estimate(*iterator, goal); + if (best == children.end() || estimate < score) { + best = iterator; + score = estimate; + } + } + for(typename std::set<STATE>::iterator + iterator = children.begin(), + end = children.end(); + iterator != end;){ + if (iterator == best) { + ++iterator; + } else { + children.erase(iterator++); + } + } + } +}; + +#endif diff --git a/casa/search/Guide.H b/casa/search/Guide.H new file mode 100644 index 0000000..797d39f --- /dev/null +++ b/casa/search/Guide.H @@ -0,0 +1,34 @@ +// Copyright 2008, 2009 Brady J. Garvin + +// This file is part of Covering Arrays by Simulated Annealing (CASA). + +// CASA 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 3 of the License, or +// (at your option) any later version. + +// CASA 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 CASA. If not, see <http://www.gnu.org/licenses/>. + + +#ifndef GUIDE_H +#define GUIDE_H + +// Decides the order in which states are explored. Usual policies include +// visiting the heuristically best states first, visiting states whose distance +// from the start state added to the heuristic is minimal, visiting states +// randomly, etc. There is provision to treat start states specially. + +template<class STATE, class COST>class Guide { +public: + virtual ~Guide() {} + virtual COST rankStart(const Node<STATE, COST>&start) const = 0; + virtual COST rank(const Node<STATE, COST>&node) const = 0; +}; + +#endif diff --git a/casa/search/Heuristic.H b/casa/search/Heuristic.H new file mode 100644 index 0000000..40affe5 --- /dev/null +++ b/casa/search/Heuristic.H @@ -0,0 +1,32 @@ +// Copyright 2008, 2009 Brady J. Garvin + +// This file is part of Covering Arrays by Simulated Annealing (CASA). + +// CASA 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 3 of the License, or +// (at your option) any later version. + +// CASA 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 CASA. If not, see <http://www.gnu.org/licenses/>. + + +#ifndef HEURISTIC_H +#define HEURISTIC_H + +#include "search/Goal.H" + +// Rates the quality of a state (never a path). + +template<class STATE, class COST>class Heuristic { +public: + virtual ~Heuristic() {} + virtual COST estimate(const STATE&state, const Goal<STATE>&goal) const = 0; +}; + +#endif diff --git a/casa/search/Node.H b/casa/search/Node.H new file mode 100644 index 0000000..5e5b478 --- /dev/null +++ b/casa/search/Node.H @@ -0,0 +1,137 @@ +// Copyright 2008, 2009 Brady J. Garvin + +// This file is part of Covering Arrays by Simulated Annealing (CASA). + +// CASA 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 3 of the License, or +// (at your option) any later version. + +// CASA 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 CASA. If not, see <http://www.gnu.org/licenses/>. + + +#ifndef NODE_H +#define NODE_H + +#include <cassert> +#include <iostream> +#include <set> + +// Represents an explored state, its heuristic estimate, the best known path +// leading to that state, and other nodes whose best paths this state is on. + +template<class STATE, class COST>class Node { +protected: + typedef Node<STATE,COST>* Edge; + + // The node immediately preceding this one on a best path. + Edge parent; + // The state. + const STATE state; + // The distance from the start state along the best path. + COST traveled; + // The heuristic estimate of the distance to a goal state. + COST estimate; + // The set of nodes who have this one as their parent. + std::set<Edge> children; + +public: + Node(Edge parent, const STATE&state, COST traveled, COST estimate) : + parent(parent), + state(state), + traveled(traveled), + estimate(estimate) { + if (parent) { + parent->children.insert(this); + } + } + + virtual ~Node() { + if (parent) { + parent->removeChild(this); + } + for (typename std::set<Edge>::iterator + iterator = children.begin(), + end = children.end(); + iterator != end;) { + Edge child = *iterator; + ++iterator; + removeChild(child); + } + } + + const STATE&getState() const { + return state; + } + + COST getTraveled() const { + return traveled; + } + void setTraveled(COST traveled) { + this->traveled = traveled; + } + + COST getEstimate() const { + return estimate; + } + void setEstimate(COST estimate) { + this->estimate = estimate; + } + + Edge getParent() const { + return parent; + } + + const std::set<Edge>&getChildren() const { + return children; + } + + void addChild(Edge child) { + assert(child); + if (child->parent) { + if (child->parent == this) { + return; + } + child->parent->removeChild(child); + } + child->parent = this; + children.insert(child); + } + + void removeChild(Edge child) { + assert(child); + if (child->parent != this) { + return; + } + child->parent = NULL; + children.erase(child); + } + + // Comparisons are made solely by state. +#define COMP(op) bool operator op(const Node&other) const { \ + return state op other.state; \ + } + COMP(<); + COMP(>); + COMP(==); + COMP(!=); +#undef COMP +}; + +template<class STATE, class COST>std::ostream&operator << + (std::ostream&out, const Node<STATE, COST>node) { + out << node.getState() << '(' << node.getTraveled() << '+' << + node.getEstimate() << "*)"; + if (node.getParent()) { + return out << "<-" << *node.getParent(); + } + return out; +} + +#endif diff --git a/casa/search/Search.H b/casa/search/Search.H new file mode 100644 index 0000000..0524ea5 --- /dev/null +++ b/casa/search/Search.H @@ -0,0 +1,460 @@ +// Copyright 2008, 2009 Brady J. Garvin + +// This file is part of Covering Arrays by Simulated Annealing (CASA). + +// CASA 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 3 of the License, or +// (at your option) any later version. + +// CASA 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 CASA. If not, see <http://www.gnu.org/licenses/>. + + +#ifndef SEARCH_H +#define SEARCH_H + +#include <cassert> +#include <vector> +#include <set> + +#include "utility/pless.H" +#include "utility/relation.H" + +#include "events/EventSource.H" + +#include "search/SearchConfiguration.H" +#include "search/Node.H" +#include "search/StateSpace.H" +#include "search/Heuristic.H" +#include "search/Guide.H" +#include "search/Goal.H" +#include "search/Filter.H" +#include "search/SearchIteration.H" +#include "search/SearchFinish.H" + +// A highly parameterized searching object. + +// Clients of this code mostly need to understand the objects passed at +// construction time and, if pathfinding, fulfill the assumption that shortening +// a path prefix will shorten an entire path. The complexity here is merely for +// careful bookkeeping and memory management. + +// The general calling pattern is: +// <constructor> +// foreach search { +// addStartState(...); +// // Possibly more calls to addStartState(...) +// search(...); +// ... = getBest() // If we care about the best results +// // Possibly more calls to search(...) if the search is restartable +// clear(); +// } +// <destructor> + +template<class STATE, class COST>class Search : + public EventSource<SearchIteration>, + public EventSource<SearchFinish<STATE, COST> > { +public: + typedef Node<STATE, COST> NodeT; + +protected: + typedef relation<NodeT*, COST, true, false, pless<NodeT> > + VisitSetT; + typedef StateSpace<STATE, COST> + StateSpaceT; + typedef Heuristic<STATE, COST> + HeuristicT; + typedef Guide<STATE, COST> + GuideT; + typedef Goal<STATE> GoalT; + typedef Filter<STATE,COST> FilterT; + typedef SearchFinish<STATE, COST> + SearchFinishT; + + SearchConfiguration configuration; + StateSpaceT* space; + HeuristicT* heuristic; + GuideT* guide; + GoalT* goal; + FilterT* filter; + bool oneBest; + VisitSetT open; + VisitSetT closed; + std::set<const NodeT*> best; + COST bestRank; + +public: + // See the classes SearchConfiguration, StateSpace, Heuristic, Guide, Goal, + // and Filter for documentation on their role in search. The parameter + // oneBest does not affect the method of search, but merely how many solutions + // are remembered in the case of a tie in the guide's ranking. + Search + (SearchConfiguration configuration, + StateSpaceT*space, + HeuristicT*heuristic, + GuideT*guide, + GoalT*goal, + FilterT*filter, + bool oneBest) : + configuration(configuration), + space(space), + heuristic(heuristic), + guide(guide), + goal(goal), + filter(filter), + oneBest(oneBest) { + assert(space); + assert(heuristic); + assert(guide); + assert(goal); + assert(filter); + } + + virtual ~Search() { + clear(); + } + +protected: + // A leak-free way to clear the set of best nodes. + void clearBest() { + if (!configuration.useClosed) { + for (typename std::set<const NodeT*>::const_iterator + iterator = best.begin(), + end = best.end(); + iterator != end; + ++iterator) { + NodeT*node = const_cast<NodeT*>(*iterator); + if (open.key_find(node) == open.key_end()) { + delete node; + } + } + } + best.clear(); + } + + // See if the given node with the given guide ranking should be entered into + // the set of best nodes. + void updateBest(const NodeT&node, COST rank) { + if (rank < bestRank) { + clearBest(); + } + if (best.empty()) { + best.insert(&node); + bestRank = rank; + } else if (rank == bestRank) { + if (oneBest) clearBest(); + best.insert(&node); + } + } + + // Pop the best ranked node from the set of nodes that have been seen but not + // explored. + NodeT&popBestOpen() { + assert(!open.empty()); + typename VisitSetT::data_iterator pop = open.data_begin(); + assert(pop->second); + if (configuration.useClosed) { + closed.key_insert(pop->second, pop->first); + } + NodeT&result = *(pop->second); + open.data_erase(pop); + return result; + } + + // Get the children (immediately reachable neighbors) according to the + // SearchConfiguration. + std::set<STATE>getChildren(const NodeT&parent) { + if (configuration.proportionChildren) { + return space->getChildren + (parent.getState(), configuration.childrenAsk.proportion); + } + return space->getChildren + (parent.getState(), configuration.childrenAsk.count); + } + + // Return true if a node should be discarded because we have seen a better one + // representing the same state, but not explored it yet. Also, forget about + // any nodes that we have seen but not explored if they represent the same + // state but are worse. + bool replaceInOpen(NodeT&parent, NodeT&node, COST traveled) { + typename VisitSetT::key_iterator similar = open.key_find(&node); + if (similar == open.key_end()) { + // The node does not have an already seen state. + return false; + } + NodeT*visited = similar->first; + assert(visited); + if (visited->getTraveled() <= traveled) { + // The node has an already seen state and cannot improve a path; discard + // it. + return true; + } + // The node has an already seen state, but may improve some paths; use it + // instead. + if (configuration.useClosed) { + parent.addChild(visited); + } + visited->setTraveled(traveled); + open.key_erase(similar); + COST rank = guide->rank(*visited); + open.key_insert(visited, rank); + updateBest(*visited, rank); + return true; + } + + // Correct any out-of-date distance calculations when we change a path prefix. + // The arguments are the newly connected parent and child nodes. + void updateTraveled(NodeT&parent, NodeT&visited) { + // Setup to DFS from the visited node. + std::set<NodeT*>parentSet; + std::set<NodeT*>visitedSet; + parentSet.insert(&parent); + visitedSet.insert(&visited); + std::vector<const std::set<NodeT*>*>extrusion; + std::vector<typename std::set<NodeT*>::const_iterator>path; + extrusion.push_back(&parentSet); + path.push_back(extrusion.back()->begin()); + extrusion.push_back(&visitedSet); + path.push_back(extrusion.back()->begin()); + // Run the DFS, updating traveled distances and resorting. + for (;;) { + if (path.back() == extrusion.back()->end()) { + path.pop_back(); + extrusion.pop_back(); + if (path.empty()) { + break; + } + ++path.back(); + } else { + typename + std::vector<typename std::set<NodeT*>::const_iterator>:: + const_reverse_iterator back = path.rbegin(); + NodeT&update = ***back; + assert(&update); + ++back; + NodeT&source = ***back; + assert(&source); + update.setTraveled(space->getTraveled(source, update.getState())); + COST rank = guide->rank(update); + typename VisitSetT::key_iterator moribund = open.key_find(&update); + if (moribund != open.key_end()) { + open.key_erase(moribund); + open.key_insert(&update, rank); + updateBest(update, rank); + ++path.back(); + } else { + moribund = closed.key_find(&update); + assert(moribund != closed.key_end()); + closed.key_erase(moribund); + closed.key_insert(&update, rank); + updateBest(update, rank); + // Push children. + extrusion.push_back(&update.getChildren()); + path.push_back(extrusion.back()->begin()); + } + } + } + } + + // Return true if a node should be discarded because we have explored a better + // node representing the same state. Also, forget about any nodes that we + // have explored if they represent the same state but are worse. + bool replaceInClosed(NodeT&parent, NodeT&node, COST traveled) { + typename VisitSetT::key_iterator similar = closed.key_find(&node); + if (similar == closed.key_end()) { + // The node does not have an already explored state. + return false; + } + NodeT*visited = similar->first; + assert(visited); + if (visited->getTraveled() <= traveled) { + // The node has an already explored state and cannot improve a path; + // discard it. + return true; + } + // The node has an already explored state, but will improve some paths; use + // it instead. + parent.addChild(visited); + updateTraveled(parent, *visited); + return true; + } + + //Add a newly seen node to the set of seen but not yet explored nodes. + void addNew(NodeT*node) { + COST rank = guide->rank(*node); + open.key_insert(node,rank); + updateBest(*node,rank); + } + +public: + // Add a start state before searching. + void addStartState(const STATE&start) { + NodeT*node = + new NodeT + (NULL, + start, + space->getTraveled(start), + heuristic->estimate(start, *goal)); + addNew(node); + } + + // Try to find a goal in the given budget. If restartable is true the search + // can be resumed by a later call to this method. + std::set<NodeT*>search(unsigned iterations, bool restartable) { + std::set<NodeT*>result; + if (open.empty()) { + return result; + } + for (unsigned i = iterations, j = configuration.prunePeriod; + i-- && result.empty();) { +#ifdef SEARCH_PROGRESS + if (!(i & 0x3FF)) { + std::cout << i << " iterations left after this one" << std::endl; + } +#endif + NodeT&parent = popBestOpen(); + // If it is time to prune exploration to the most promising frontier: + if (!--j) { + j = configuration.prunePeriod; + std::set<const NodeT*>lineage; + typename std::set<const NodeT*>::const_iterator + lineageEnd = lineage.end(); + for (const NodeT*k = &parent; k; k = k->getParent()) { + lineage.insert(k); + } + for (typename VisitSetT::key_iterator + k = closed.key_begin(), + kend = closed.key_end(); + k != kend;) { + if (lineage.find(k->first) == lineageEnd) { + delete k->first; + closed.key_erase(k++); + } else { + ++k; + } + } + for (typename VisitSetT::key_iterator + k = open.key_begin(), + kend = open.key_end(); + k != kend;++k) { + delete k->first; + } + open.clear(); + } + // Explore. + std::set<STATE>children = getChildren(parent); + if (configuration.retryChildren) { + (*filter)(children, parent.getState(), *heuristic, *goal); + } else { + (*filter)(children, *heuristic, *goal); + } + // The flag to decide if the parent information can be deleted. It is + // true when we aren't looking for paths and the parent isn't part of the + // best set. + bool parentMoribund = false; + if (!configuration.useClosed) { + typename std::set<const NodeT*>::const_iterator + asBest = best.find(&parent), + bestEnd = best.end(); + if (asBest == bestEnd) { + parentMoribund = true; + } + } + // See children. + for (typename std::set<STATE>::const_iterator + iterator = children.begin(), + end = children.end(); + iterator != end; + ++iterator) { + COST traveled = space->getTraveled(parent, *iterator); + NodeT*node = + new NodeT + (configuration.useClosed ? &parent : NULL, + *iterator, + traveled, + heuristic->estimate(*iterator, *goal)); + if (replaceInOpen(parent, *node, traveled)) { + // The new node was beaten by something in the open set. + delete node; + } else if (configuration.useClosed && + replaceInClosed(parent, *node, traveled)) { + // The new node was beaten by something in the closed set. + delete node; + } else { + // The new node is worth exploring. + addNew(node); + // Track goals. + if (goal->isGoal(*iterator)) { + result.insert(node); + // If we are just interested in finding a goal, we can return now. + if (!restartable) { + if (parentMoribund) { + delete &parent; + } + // Complete the search. + SearchFinishT finish(*this, result, iterations - i, iterations); + EventSource<SearchFinishT>::dispatch(finish); + return result; + } + } + } + } + if (parentMoribund) { + delete &parent; + } + // Complete the iteration. + SearchIteration iteration; + EventSource<SearchIteration>::dispatch(iteration); + } + // Complete the search. + SearchFinishT finish(*this, result, iterations, iterations); + EventSource<SearchFinishT>::dispatch(finish); + return result; + } + +#define GET_SET(type, member, capMember) \ + const type get ## capMember() const { \ + return member; \ + } \ + void set ## capMember(const type&member) { \ + this->member = member; \ + } + GET_SET(SearchConfiguration, configuration, SearchConfiguration); + GET_SET(StateSpaceT*, space, Space); + GET_SET(HeuristicT*, heuristic, Heuristic); + GET_SET(GuideT*, guide, Guide); + GET_SET(GoalT*, goal, Goal); +#undef GET_SET + + const std::set<const NodeT*>getBest() const { + return best; + } + + void clear() { + clearBest(); + for (typename VisitSetT::key_iterator + k = open.key_begin(), + kend = open.key_end(); + k != kend; + ++k) { + delete k->first; + } + open.clear(); + for (typename VisitSetT::key_iterator + k = closed.key_begin(), + kend = closed.key_end(); + k != kend; + ++k) { + delete k->first; + } + closed.clear(); + } +}; + +#endif diff --git a/casa/search/SearchConfiguration.H b/casa/search/SearchConfiguration.H new file mode 100644 index 0000000..469a6ae --- /dev/null +++ b/casa/search/SearchConfiguration.H @@ -0,0 +1,99 @@ +// Copyright 2008, 2009 Brady J. Garvin + +// This file is part of Covering Arrays by Simulated Annealing (CASA). + +// CASA 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 3 of the License, or +// (at your option) any later version. + +// CASA 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 CASA. If not, see <http://www.gnu.org/licenses/>. + + +#ifndef SEARCH_CONFIGURATION_H +#define SEARCH_CONFIGURATION_H + +// Controls behaviors of the search that are parameterized by value, not code. + +struct SearchConfiguration { + // Should we keep a history of where we've been? + // Defaults to true. + // If false: + // Nodes are always without parent, so the search cannot find paths. + // States that have been visited and expanded may be visited and expanded + // again. + bool useClosed; + + // Should we allow a parent to consider itself its own child? + // Defaults to false. + // If true: + // Node's states are forcibly added to their own sets of children. + // Filters can therefore choose the trivial (no-move) transition, like in + // hill-climbing. + // The search may spin at local maxima. + bool retryChildren; + + // Should we limit the number of children by a proportion rather than a count? + // Defaults to true. + // If true: + // The state space is asked to enumerate a fixed proportion of children. + // States with more children will have longer enumerations. + // If false: + // The state space is asked to enumerate a fixed number of children. + // States with too few children will have all of them listed. + // States with too many children will not. + bool proportionChildren; + + // How many children should we ask for? + // (See the documentation of proportionChildren above.) + union { + float proportion; + unsigned count; + } childrenAsk; + + // How many iterations before each pruning of the space? + // Defaults to zero, which is treated as infinity. + // If nonzero: + // After the given number of iterations, the search will forget all visits + // except for the best nodes in the closed and open sets. + // This is sometimes an appropriate way to trade performance for memory. + unsigned prunePeriod; + + SearchConfiguration() : + useClosed(true), + retryChildren(false), + proportionChildren(true), + prunePeriod(0) { + childrenAsk.proportion = 1; + } + SearchConfiguration + (bool useClosed, + bool retryChildren, + float proportion, + unsigned prunePeriod) : + useClosed(useClosed), + retryChildren(retryChildren), + proportionChildren(true), + prunePeriod(prunePeriod) { + childrenAsk.proportion = proportion; + } + SearchConfiguration + (bool useClosed, + bool retryChildren, + unsigned count, + unsigned prunePeriod) : + useClosed(useClosed), + retryChildren(retryChildren), + proportionChildren(false), + prunePeriod(prunePeriod) { + childrenAsk.count = count; + } +}; + +#endif diff --git a/casa/search/SearchFinish.H b/casa/search/SearchFinish.H new file mode 100644 index 0000000..67d4835 --- /dev/null +++ b/casa/search/SearchFinish.H @@ -0,0 +1,55 @@ +// Copyright 2008, 2009 Brady J. Garvin + +// This file is part of Covering Arrays by Simulated Annealing (CASA). + +// CASA 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 3 of the License, or +// (at your option) any later version. + +// CASA 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 CASA. If not, see <http://www.gnu.org/licenses/>. + + +#ifndef SEARCH_FINISH_H +#define SEARCH_FINISH_H + +#include <set> + +#include "search/Node.H" + +// A forward declaration for when this header is included by Search.H: +template<class, class>class Search; + +// A message broadcast when a search finishes (even if it was unsuccessful). + +template<class STATE, class COST>class SearchFinish { +public: + typedef Search<STATE, COST> SearchT; + typedef Node<STATE, COST> NodeT; + + const SearchT& source; + std::set<NodeT*> results; + unsigned iterations; + unsigned maxIterations; + + SearchFinish + (const SearchT&source, + const std::set<NodeT*>&results, + unsigned iterations, + unsigned maxIterations) : + source(source), + results(results), + iterations(iterations), + maxIterations(maxIterations) {} +}; + +// For inclusion from anywhere but Search.H: +#include "search/Search.H" + +#endif diff --git a/casa/search/SearchIteration.H b/casa/search/SearchIteration.H new file mode 100644 index 0000000..41a267a --- /dev/null +++ b/casa/search/SearchIteration.H @@ -0,0 +1,28 @@ +// Copyright 2008, 2009 Brady J. Garvin + +// This file is part of Covering Arrays by Simulated Annealing (CASA). + +// CASA 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 3 of the License, or +// (at your option) any later version. + +// CASA 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 CASA. If not, see <http://www.gnu.org/licenses/>. + + +#ifndef SEARCH_ITERATION_H +#define SEARCH_ITERATION_H + +// A message broadcast when a search completes an iteration but does not finish. + +class SearchIteration { + // Information about the progress of search could go here. +}; + +#endif diff --git a/casa/search/StateGuide.H b/casa/search/StateGuide.H new file mode 100644 index 0000000..0551904 --- /dev/null +++ b/casa/search/StateGuide.H @@ -0,0 +1,34 @@ +// Copyright 2008, 2009 Brady J. Garvin + +// This file is part of Covering Arrays by Simulated Annealing (CASA). + +// CASA 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 3 of the License, or +// (at your option) any later version. + +// CASA 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 CASA. If not, see <http://www.gnu.org/licenses/>. + + +#ifndef STATE_GUIDE_H +#define STATE_GUIDE_H + +// A specialized guide that ranks strictly by the states' heuristic estimates. + +template<class STATE, class COST>class StateGuide : public Guide<STATE, COST> { +public: + COST rankStart(const Node<STATE, COST>&start) const { + return start.getEstimate(); + } + COST rank(const Node<STATE, COST>&node) const { + return node.getEstimate(); + } +}; + +#endif diff --git a/casa/search/StateSpace.H b/casa/search/StateSpace.H new file mode 100644 index 0000000..5003f9b --- /dev/null +++ b/casa/search/StateSpace.H @@ -0,0 +1,50 @@ +// Copyright 2008, 2009 Brady J. Garvin + +// This file is part of Covering Arrays by Simulated Annealing (CASA). + +// CASA 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 3 of the License, or +// (at your option) any later version. + +// CASA 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 CASA. If not, see <http://www.gnu.org/licenses/>. + + +#ifndef STATE_SPACE_H +#define STATE_SPACE_H + +#include <set> + +#include "search/Node.H" + +// A description of a state space, namely the state interconnections and +// distances (for pathfinding rather than statefinding). + +template<class STATE, class COST>class StateSpace { +public: + virtual ~StateSpace() {} + + // Determine the distance incurred by starting at the given state. + virtual COST getTraveled(const STATE&start) const = 0; + + // Determine the total distance traveled to reach state after taking the best + // known path reaching parent. + virtual COST getTraveled(const Node<STATE, COST>&parent, const STATE&state) + const = 0; + + // Enumerate a fixed fraction of the children of state, rounding up. + virtual std::set<STATE>getChildren(const STATE&state, float proportion) + const = 0; + + // Enumerate the children of state up to some limit. + virtual std::set<STATE>getChildren(const STATE&state, unsigned count) + const = 0; +}; + +#endif diff --git a/common/posix/getopt.h b/common/posix/getopt.h new file mode 100644 index 0000000..feea50c --- /dev/null +++ b/common/posix/getopt.h @@ -0,0 +1,177 @@ +/* Declarations for getopt. + Copyright (C) 1989-1994,1996-1999,2001,2003,2004 + Free Software Foundation, Inc. + This file is part of the GNU C Library. + + The GNU C Library is free software; you can redistribute it and/or + modify it under the terms of the GNU Lesser General Public + License as published by the Free Software Foundation; either + version 2.1 of the License, or (at your option) any later version. + + The GNU C Library is distributed in the hope that it will be useful, + but WITHOUT ANY WARRANTY; without even the implied warranty of + MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU + Lesser General Public License for more details. + + You should have received a copy of the GNU Lesser General Public + License along with the GNU C Library; if not, write to the Free + Software Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA + 02111-1307 USA. */ + +#ifndef _GETOPT_H + +#ifndef __need_getopt +# define _GETOPT_H 1 +#endif + +/* If __GNU_LIBRARY__ is not already defined, either we are being used + standalone, or this is the first header included in the source file. + If we are being used with glibc, we need to include <features.h>, but + that does not exist if we are standalone. So: if __GNU_LIBRARY__ is + not defined, include <ctype.h>, which will pull in <features.h> for us + if it's from glibc. (Why ctype.h? It's guaranteed to exist and it + doesn't flood the namespace with stuff the way some other headers do.) */ +#if !defined __GNU_LIBRARY__ +# include <ctype.h> +#endif + +#ifndef __THROW +# ifndef __GNUC_PREREQ +# define __GNUC_PREREQ(maj, min) (0) +# endif +# if defined __cplusplus && __GNUC_PREREQ (2,8) +# define __THROW throw () +# else +# define __THROW +# endif +#endif + +#ifdef __cplusplus +extern "C" { +#endif + +/* For communication from `getopt' to the caller. + When `getopt' finds an option that takes an argument, + the argument value is returned here. + Also, when `ordering' is RETURN_IN_ORDER, + each non-option ARGV-element is returned here. */ + +extern char *optarg; + +/* Index in ARGV of the next element to be scanned. + This is used for communication to and from the caller + and for communication between successive calls to `getopt'. + + On entry to `getopt', zero means this is the first call; initialize. + + When `getopt' returns -1, this is the index of the first of the + non-option elements that the caller should itself scan. + + Otherwise, `optind' communicates from one call to the next + how much of ARGV has been scanned so far. */ + +extern int optind; + +/* Callers store zero here to inhibit the error message `getopt' prints + for unrecognized options. */ + +extern int opterr; + +/* Set to an option character which was unrecognized. */ + +extern int optopt; + +#ifndef __need_getopt +/* Describe the long-named options requested by the application. + The LONG_OPTIONS argument to getopt_long or getopt_long_only is a vector + of `struct option' terminated by an element containing a name which is + zero. + + The field `has_arg' is: + no_argument (or 0) if the option does not take an argument, + required_argument (or 1) if the option requires an argument, + optional_argument (or 2) if the option takes an optional argument. + + If the field `flag' is not NULL, it points to a variable that is set + to the value given in the field `val' when the option is found, but + left unchanged if the option is not found. + + To have a long-named option do something other than set an `int' to + a compiled-in constant, such as set a value from `optarg', set the + option's `flag' field to zero and its `val' field to a nonzero + value (the equivalent single-letter option character, if there is + one). For long options that have a zero `flag' field, `getopt' + returns the contents of the `val' field. */ + +struct option +{ + const char *name; + /* has_arg can't be an enum because some compilers complain about + type mismatches in all the code that assumes it is an int. */ + int has_arg; + int *flag; + int val; +}; + +/* Names for the values of the `has_arg' field of `struct option'. */ + +# define no_argument 0 +# define required_argument 1 +# define optional_argument 2 +#endif /* need getopt */ + + +/* Get definitions and prototypes for functions to process the + arguments in ARGV (ARGC of them, minus the program name) for + options given in OPTS. + + Return the option character from OPTS just read. Return -1 when + there are no more options. For unrecognized options, or options + missing arguments, `optopt' is set to the option letter, and '?' is + returned. + + The OPTS string is a list of characters which are recognized option + letters, optionally followed by colons, specifying that that letter + takes an argument, to be placed in `optarg'. + + If a letter in OPTS is followed by two colons, its argument is + optional. This behavior is specific to the GNU `getopt'. + + The argument `--' causes premature termination of argument + scanning, explicitly telling `getopt' that there are no more + options. + + If OPTS begins with `--', then non-option arguments are treated as + arguments to the option '\0'. This behavior is specific to the GNU + `getopt'. */ + +#ifdef __GNU_LIBRARY__ +/* Many other libraries have conflicting prototypes for getopt, with + differences in the consts, in stdlib.h. To avoid compilation + errors, only prototype getopt for the GNU C library. */ +extern int getopt (int ___argc, char *const *___argv, const char *__shortopts) + __THROW; +/*#else // not __GNU_LIBRARY__ // +extern int getopt ();*/ +#endif /* __GNU_LIBRARY__ */ + +#ifndef __need_getopt +extern int getopt_long (int ___argc, char *const *___argv, + const char *__shortopts, + const struct option *__longopts, int *__longind) + __THROW; +extern int getopt_long_only (int ___argc, char *const *___argv, + const char *__shortopts, + const struct option *__longopts, int *__longind) + __THROW; + +#endif + +#ifdef __cplusplus +} +#endif + +/* Make sure we later can get all the definitions and declarations. */ +#undef __need_getopt + +#endif /* getopt.h */ diff --git a/common/utility/Array.H b/common/utility/Array.H new file mode 100644 index 0000000..155bad7 --- /dev/null +++ b/common/utility/Array.H @@ -0,0 +1,128 @@ +// Copyright 2008, 2009 Brady J. Garvin + +// This file is part of Covering Arrays by Simulated Annealing (CASA). + +// CASA 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 3 of the License, or +// (at your option) any later version. + +// CASA 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 CASA. If not, see <http://www.gnu.org/licenses/>. + + +#ifndef ARRAY_H +#define ARRAY_H + +#include <iostream> + +template<class T>class Array { +protected: + unsigned size; + T* array; + unsigned* referenceCount; + + void destroy() { + if (referenceCount && !(--*referenceCount)) { + delete[] array; + delete referenceCount; + } + array = NULL; + } + +public: + Array() : + size(0), + array(NULL), + referenceCount(NULL) {} + Array(unsigned size) : + size(size), + array(new T[size]), + referenceCount(new unsigned(1)) {} + Array(const T*raw, unsigned size) : + size(size), + array(new T[size]), + referenceCount(new unsigned(1)) { + for (unsigned i = size; i-- > 0;) { + array[i] = raw[i]; + } + } + Array(const Array©) : + size(copy.size), + array(copy.array), + referenceCount(copy.referenceCount) { + if (referenceCount) { + ++*referenceCount; + } + } + + Array&operator =(const Array©) { + destroy(); + size = copy.size; + array = copy.array; + referenceCount = copy.referenceCount; + ++*referenceCount; + return *this; + } + + virtual ~Array() { + destroy(); + } + + unsigned getSize() const { + return size; + } + + operator const T*() const { + return array; + } + operator T*() { + return array; + } + + void fill(const T&filler) { + for (unsigned i = size; i--;) { + array[i] = filler; + } + } +}; + +template<class T>std::ostream&operator << + (std::ostream&out, const Array<T>&array) { + out << '['; + for (unsigned i = 0; i < array.getSize(); ++i) { + out << array[i] << ','; + } + return out << "X]"; +} + +template<class T,class COMPARE = std::less<T> >class ArrayComparator { +public: + bool operator()(const Array<T>&left, const Array<T>&right) const { + static COMPARE compare; + unsigned leftSize = left.getSize(); + unsigned rightSize = right.getSize(); + if (leftSize < rightSize) { + return true; + } + if (leftSize > rightSize) { + return false; + } + for (unsigned i = 0; i < leftSize; ++i) { + if (compare(left[i], right[i])) { + return true; + } + if (compare(right[i], left[i])) { + return false; + } + } + return false; + } +}; + +#endif diff --git a/common/utility/Combinadic.C b/common/utility/Combinadic.C new file mode 100644 index 0000000..812a7d1 --- /dev/null +++ b/common/utility/Combinadic.C @@ -0,0 +1,129 @@ +// Copyright 2008, 2009 Brady J. Garvin + +// This file is part of Covering Arrays by Simulated Annealing (CASA). + +// CASA 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 3 of the License, or +// (at your option) any later version. + +// CASA 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 CASA. If not, see <http://www.gnu.org/licenses/>. + + +#include <cassert> + +#include "Combinadic.H" + +using namespace std; + +static double TWO_PI = 2 * M_PI; +static double INVERSE_E = 1 / M_E; + +// We want result to approximately satisfy +// cardinality! * encoding = result * (result-1) * ... * (result-(cardinality-1)) +// The right-hand side usually has degree >= 5, so we need to trivialize it a bit. +// It can be replaced with the overapproximation: +// cardinality! * encoding = (result - (cardinality-1) / 2) ^ cardinality +// Factorials are also expensive, so we use Stirling's approximation: +// sqrt(TWO_PI * cardinality) * ((cardinality / e) ^ cardinality) * encoding = +// (result - (cardinality-1) / 2) ^ cardinality +// Now, to solve for result, take the cardinality'th root of both sides: +// (cardinality / e) * +// (encoding * sqrt(TWO_PI * cardinality)) ^ (1 / cardinality) = +// result - (cardinality - 1)/2 +// And then rearrange that and add a half to make the flooring round to nearest: +// result = +// (cardinality / e) * +// (encoding * sqrt(TWO_PI * cardinality)) ^ (1 / cardinality) + +// cardinality / 2 = +// ((1 / e) * +// (encoding * sqrt(TWO_PI * cardinality)) ^ (1 / cardinality) + 0.5) * +// cardinality +unsigned Combinadic::guessLastMember(unsigned encoding, unsigned cardinality) { + double scaledEncoding = encoding * sqrt(TWO_PI * cardinality); + double rootOfEncoding = pow(scaledEncoding, 1.0 / cardinality); + return (unsigned)((INVERSE_E * rootOfEncoding + 0.5) * (double)cardinality); +} + +pair<unsigned, unsigned>Combinadic::getLastMemberAndContribution + (unsigned encoding, unsigned cardinality) { + unsigned member = guessLastMember(encoding, cardinality); + unsigned contribution = triangle.nCr(member, cardinality); + if (contribution > encoding) { + do { + contribution = triangle.nCr(--member, cardinality); + } while (contribution > encoding); + } else { + unsigned nextContribution = triangle.nCr(member + 1, cardinality); + while (nextContribution <= encoding) { + ++member; + contribution = nextContribution; + nextContribution = triangle.nCr(member + 1, cardinality); + } + } + return pair<unsigned, unsigned>(member, contribution); +} + +unsigned Combinadic::encode(Array<unsigned>sortedSubset) { + unsigned result = 0; + for (unsigned i = 0; i < sortedSubset.getSize(); ++i) { + result += triangle.nCr(sortedSubset[i], i + 1); + } + return result; +} + +Array<unsigned>Combinadic::decode(unsigned encoding, unsigned cardinality) { + Array<unsigned>result(cardinality); + for (unsigned i = cardinality; i;) { + pair<unsigned, unsigned>memberAndContribution = + getLastMemberAndContribution(encoding, i); + result[--i] = memberAndContribution.first; + encoding -= memberAndContribution.second; + } + return result; +} + +Array<unsigned>Combinadic::begin(unsigned size) const { + Array<unsigned>result(size); + for(unsigned i = size; i-- ;) { + result[i]=i; + } + return result; +} + +void Combinadic::previous(Array<unsigned>sortedSubset) const { + assert(sortedSubset.getSize()); + unsigned limit = sortedSubset.getSize(); + for(unsigned i = 0; i < limit; ++i) { + unsigned entry = sortedSubset[i]; + if (entry > i) { + do { + sortedSubset[i] = --entry; + } while (i-- > 0); + return; + } + } +} + +void Combinadic::next(Array<unsigned>sortedSubset) const { + assert(sortedSubset.getSize()); + unsigned limit = sortedSubset.getSize() - 1, ceiling = sortedSubset[0]; + for (unsigned i = 0; i < limit; ++i) { + unsigned entry = ceiling + 1; + ceiling = sortedSubset[i + 1]; + if (entry < ceiling) { + sortedSubset[i] = entry; + return; + } + sortedSubset[i] = i; + } + ++sortedSubset[limit]; +} + +Combinadic combinadic; diff --git a/common/utility/Combinadic.H b/common/utility/Combinadic.H new file mode 100644 index 0000000..5edca67 --- /dev/null +++ b/common/utility/Combinadic.H @@ -0,0 +1,42 @@ +// Copyright 2008, 2009 Brady J. Garvin + +// This file is part of Covering Arrays by Simulated Annealing (CASA). + +// CASA 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 3 of the License, or +// (at your option) any later version. + +// CASA 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 CASA. If not, see <http://www.gnu.org/licenses/>. + + +#ifndef COMBINADIC_H +#define COMBINADIC_H + +#include <math.h> + +#include "Array.H" +#include "PascalTriangle.H" + +class Combinadic { +protected: + unsigned guessLastMember(unsigned encoding, unsigned cardinality); + std::pair<unsigned, unsigned>getLastMemberAndContribution + (unsigned encoding, unsigned cardinality); +public: + unsigned encode(Array<unsigned>sortedSubset); + Array<unsigned>decode(unsigned encoding, unsigned cardinality); + Array<unsigned>begin(unsigned size) const; + void previous(Array<unsigned>sortedSubset) const; + void next(Array<unsigned>sortedSubset) const; +}; + +extern Combinadic combinadic; + +#endif diff --git a/common/utility/CombinadicIterator.C b/common/utility/CombinadicIterator.C new file mode 100644 index 0000000..15152cb --- /dev/null +++ b/common/utility/CombinadicIterator.C @@ -0,0 +1,104 @@ +// Copyright 2008, 2009 Brady J. Garvin + +// This file is part of Covering Arrays by Simulated Annealing (CASA). + +// CASA 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 3 of the License, or +// (at your option) any later version. + +// CASA 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 CASA. If not, see <http://www.gnu.org/licenses/>. + + +#include <cassert> +#include <algorithm> + +#include "CombinadicIterator.H" + +using namespace std; + +CombinadicIterator::CombinadicIterator + (unsigned populationSize, unsigned sampleSize, Array<unsigned>relevant) : + populationSize(populationSize), + relevant(relevant), + notRelevant(populationSize - relevant.getSize()), + minimumRelevance(max((int)sampleSize - (int)notRelevant.getSize(), 1)), + maximumRelevance(min(relevant.getSize(), sampleSize)), + choiceFromRelevant(combinadic.begin(maximumRelevance)), + choiceFromNotRelevant(combinadic.begin(sampleSize - maximumRelevance)), + relevantCombination(sampleSize), + combination(sampleSize) { + assert(sampleSize <= populationSize); + for (unsigned i = 0, j = 0, k = 0; i < notRelevant.getSize(); ++i, ++j) { + while (k < relevant.getSize() && relevant[k] == j) { + ++j; + ++k; + } + notRelevant[i] = j; + } + updateCombinationFromRelevant(); + updateCombination(); +} + +void CombinadicIterator::updateCombinationFromRelevant() { + for (unsigned i = maximumRelevance; i--;) { + relevantCombination[i] = relevant[choiceFromRelevant[i]]; + } +} + +void CombinadicIterator::updateCombination() { + for (unsigned i = combination.getSize(); i-- > maximumRelevance;) { + combination[i] = notRelevant[choiceFromNotRelevant[i - maximumRelevance]]; + } + for (unsigned i = maximumRelevance; i--;) { + combination[i] = relevantCombination[i]; + } + sort(combination + 0, combination + combination.getSize()); +} + +const Array<unsigned>CombinadicIterator::operator *() const { +#ifndef NDEBUG + for (unsigned i = combination.getSize(); --i;) { + assert(combination[i - 1] < combination[i]); + } +#endif + return combination; +} + +CombinadicIterator::operator bool() const { + return combination.getSize(); +} + +CombinadicIterator&CombinadicIterator::operator ++() { + if (!combination.getSize()) { + return *this; + } + bool someFromNotRelevant = choiceFromNotRelevant.getSize(); + if (someFromNotRelevant) { + combinadic.next(choiceFromNotRelevant); + } + if (!someFromNotRelevant || + choiceFromNotRelevant[choiceFromNotRelevant.getSize() - 1] >= + populationSize - relevant.getSize()) { + combinadic.next(choiceFromRelevant); + if (choiceFromRelevant[maximumRelevance - 1] >= relevant.getSize()) { + --maximumRelevance; + if (maximumRelevance < minimumRelevance) { + combination = Array<unsigned>(0); + return *this; + } + choiceFromRelevant = combinadic.begin(maximumRelevance); + } + updateCombinationFromRelevant(); + choiceFromNotRelevant = + combinadic.begin(combination.getSize() - maximumRelevance); + } + updateCombination(); + return *this; +} diff --git a/common/utility/CombinadicIterator.H b/common/utility/CombinadicIterator.H new file mode 100644 index 0000000..faeed39 --- /dev/null +++ b/common/utility/CombinadicIterator.H @@ -0,0 +1,51 @@ +// Copyright 2008, 2009 Brady J. Garvin + +// This file is part of Covering Arrays by Simulated Annealing (CASA). + +// CASA 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 3 of the License, or +// (at your option) any later version. + +// CASA 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 CASA. If not, see <http://www.gnu.org/licenses/>. + + +#ifndef COMBINADIC_ITERATOR_H +#define COMBINADIC_ITERATOR_H + +#include "Combinadic.H" + +class CombinadicIterator { +protected: + unsigned populationSize; + // The iteration will skip sets whose intersection with relevant is empty. + Array<unsigned> relevant; + Array<unsigned> notRelevant; + + unsigned minimumRelevance; + unsigned maximumRelevance; + + Array<unsigned> choiceFromRelevant; + Array<unsigned> choiceFromNotRelevant; + + Array<unsigned> relevantCombination; + Array<unsigned> combination; +public: + CombinadicIterator + (unsigned populationSize, unsigned sampleSize, Array<unsigned>relevant); +protected: + void updateCombinationFromRelevant(); + void updateCombination(); +public: + const Array<unsigned>operator *() const; + operator bool() const; + CombinadicIterator&operator ++(); +}; + +#endif diff --git a/common/utility/Lazy.H b/common/utility/Lazy.H new file mode 100644 index 0000000..84bf426 --- /dev/null +++ b/common/utility/Lazy.H @@ -0,0 +1,110 @@ +// Copyright 2008, 2009 Brady J. Garvin + +// This file is part of Covering Arrays by Simulated Annealing (CASA). + +// CASA 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 3 of the License, or +// (at your option) any later version. + +// CASA 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 CASA. If not, see <http://www.gnu.org/licenses/>. + + +#ifndef LAZY_H +#define LAZY_H + +#include <cassert> +#include <iostream> + +template<class T>class Lazy { +protected: + T* implementation; + unsigned* referenceCount; + + void destroy() { + if (referenceCount) { + assert(implementation); + if (!(--*referenceCount)) { + delete implementation; + delete referenceCount; + } + implementation = NULL; + } else { + assert(!implementation); + } + } + +public: + Lazy() : + implementation(NULL), + referenceCount(NULL) {} + Lazy(T*implementation) : + implementation(implementation), + referenceCount(implementation ? new unsigned(1) : NULL) {} + Lazy(const Lazy©) : + implementation(copy.implementation), + referenceCount(copy.referenceCount) { + if (implementation) { + assert(referenceCount); + ++*referenceCount; + } else { + assert(!referenceCount); + } + } + + Lazy&operator =(T*implementation) { + destroy(); + this->implementation = implementation; + this->referenceCount = implementation ? new unsigned(1) : NULL; + return *this; + } + Lazy&operator =(const Lazy©) { + destroy(); + implementation = copy.implementation; + if (implementation) { + referenceCount = copy.referenceCount; + assert(referenceCount); + ++*referenceCount; + } else { + assert(!copy.referenceCount); + referenceCount = NULL; + } + return *this; + } + + virtual ~Lazy(){ + destroy(); + } + + const T*operator ->() const { + return implementation; + } + T*operator ->() { + if (referenceCount) { + assert(implementation); + if (*referenceCount > 1) { + T*copy = new T(*implementation); + destroy(); + implementation = copy; + referenceCount = new unsigned(1); + } + } else { + assert(!implementation); + } + return implementation; + } + operator const T*() const { + return operator ->(); + } + operator T*() { + return operator ->(); + } +}; + +#endif diff --git a/common/utility/PascalTriangle.C b/common/utility/PascalTriangle.C new file mode 100644 index 0000000..5a7c378 --- /dev/null +++ b/common/utility/PascalTriangle.C @@ -0,0 +1,52 @@ +// Copyright 2008, 2009 Brady J. Garvin + +// This file is part of Covering Arrays by Simulated Annealing (CASA). + +// CASA 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 3 of the License, or +// (at your option) any later version. + +// CASA 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 CASA. If not, see <http://www.gnu.org/licenses/>. + + +#include "PascalTriangle.H" + +PascalTriangle::PascalTriangle() { + Array<unsigned>root(1); + root[0] = 1; + table.push_back(root); +} + +void PascalTriangle::addRows(unsigned targetDepth) { + while (table.size() <= targetDepth) { + unsigned depth = table.size(); + Array<unsigned>line(depth + 1); + Array<unsigned>source = table[depth - 1]; + table.push_back(line); + line[0] = 1; + for (unsigned column = 1, trail = source[0]; column < depth; ++column) { + line[column] = trail; + line[column] += trail = source[column]; + } + line[depth] = 1; + } +} + +unsigned PascalTriangle::nCr(unsigned n, unsigned r) { + if (n >= table.size()) { + addRows(n); + } + if (r > n) { + return 0; + } + return table[n][r]; +} + +PascalTriangle triangle; diff --git a/common/utility/PascalTriangle.H b/common/utility/PascalTriangle.H new file mode 100644 index 0000000..fd7c5e0 --- /dev/null +++ b/common/utility/PascalTriangle.H @@ -0,0 +1,38 @@ +// Copyright 2008, 2009 Brady J. Garvin + +// This file is part of Covering Arrays by Simulated Annealing (CASA). + +// CASA 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 3 of the License, or +// (at your option) any later version. + +// CASA 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 CASA. If not, see <http://www.gnu.org/licenses/>. + + +#ifndef PASCAL_TRIANGLE_H +#define PASCAL_TRIANGLE_H + +#include <vector> + +#include "Array.H" + +class PascalTriangle { +protected: + // A table of n choose r, indexed by n then r. + std::vector<Array<unsigned> > table; +public: + PascalTriangle(); + void addRows(unsigned targetDepth); + unsigned nCr(unsigned n, unsigned r); +}; + +extern PascalTriangle triangle; + +#endif diff --git a/common/utility/SubstitutionArray.H b/common/utility/SubstitutionArray.H new file mode 100644 index 0000000..48bfbca --- /dev/null +++ b/common/utility/SubstitutionArray.H @@ -0,0 +1,191 @@ +// Copyright 2008, 2009 Brady J. Garvin + +// This file is part of Covering Arrays by Simulated Annealing (CASA). + +// CASA 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 3 of the License, or +// (at your option) any later version. + +// CASA 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 CASA. If not, see <http://www.gnu.org/licenses/>. + + +#ifndef SUBSTITUTION_ARRAY_H +#define SUBSTITUTION_ARRAY_H + +#include <iostream> +#include <map> + +#include "Array.H" +#include "Lazy.H" + +#ifndef MAXIMUM_SUBSTITUTION_PROPORTION +#define MAXIMUM_SUBSTITUTION_PROPORTION 0.1F +#endif + +template<class T>class SubstitutionArray : protected Array<T> { +protected: + Lazy<std::map<unsigned, T> > substitutions; + unsigned maximumSubstitutions; + +public: + SubstitutionArray() : Array<T>() {} + SubstitutionArray(unsigned size) : + Array<T>(size), + maximumSubstitutions(MAXIMUM_SUBSTITUTION_PROPORTION * size) {} + SubstitutionArray(const T*raw, unsigned size) : + Array<T>(raw, size), + maximumSubstitutions(MAXIMUM_SUBSTITUTION_PROPORTION * size) {} + SubstitutionArray(const Array<T>©) : + Array<T>(copy), + maximumSubstitutions(MAXIMUM_SUBSTITUTION_PROPORTION * Array<T>::size) {} + SubstitutionArray(const SubstitutionArray©) : + Array<T>((const Array<T>&)copy), + substitutions(copy.substitutions), + maximumSubstitutions(copy.maximumSubstitutions) {} + + SubstitutionArray&operator =(const Array<T>©) { + Array<T>::operator =(copy); + substitutions = NULL; + maximumSubstitutions = MAXIMUM_SUBSTITUTION_PROPORTION * Array<T>::size; + return *this; + } + SubstitutionArray&operator =(const SubstitutionArray<T>©) { + Array<T>::operator =((const Array<T>&)copy); + substitutions = copy.substitutions; + maximumSubstitutions = MAXIMUM_SUBSTITUTION_PROPORTION * Array<T>::size; + return *this; + } + + unsigned getSize() const { + return Array<T>::getSize(); + } + + class Entry { + protected: + SubstitutionArray& owner; + unsigned index; + public: + Entry(const SubstitutionArray&owner, unsigned index) : + owner(const_cast<SubstitutionArray&>(owner)), + index(index) {} + + operator T() const { + if (owner.substitutions) { + std::map<unsigned, unsigned>::const_iterator substitution = + owner.substitutions->find(index); + if (substitution != owner.substitutions->end()) { + return substitution->second; + } + } + return owner.array[index]; + } + + Entry&operator =(const T&value) { + if (*owner.referenceCount > 1) { + if (!owner.substitutions) { + owner.substitutions = new std::map<unsigned, T>(); + } + (*owner.substitutions)[index] = value; + owner.autoFinalizeSubstitutions(); + } else { + owner.array[index] = value; + } + return *this; + } + + Entry&operator --() { + T old = operator T(); + return operator =(--old); + } + Entry&operator ++() { + T old = operator T(); + return operator =(++old); + } + }; + + const Entry operator[](unsigned index) const { + return Entry(*this, index); + } + Entry operator[](unsigned index) { + return Entry(*this, index); + } + + void fill(const T&filler) { + if (*Array<T>::referenceCount > 1) { + Array<T>::destroy(); + Array<T>::array = new T[Array<T>::size]; + Array<T>::referenceCount = new unsigned(1); + substitutions = NULL; + } + Array<T>::fill(filler); + } + + void finalizeSubstitutions() { + if (!substitutions) { + return; + } + T*replacement = new T[Array<T>::size]; + for (unsigned i = Array<T>::size; i--;) { + replacement[i] = Array<T>::array[i]; + } + for (typename std::map<unsigned, T>::const_iterator iterator = + substitutions->begin(), + end = substitutions->end(); + iterator != end; ++iterator) { + replacement[iterator->first] = iterator->second; + } + Array<T>::destroy(); + Array<T>::array = replacement; + Array<T>::referenceCount = new unsigned(1); + substitutions->clear(); + } + + void autoFinalizeSubstitutions(){ + if (substitutions && substitutions->size() > maximumSubstitutions) { + finalizeSubstitutions(); + } + } +}; + +template<class T>std::ostream&operator << + (std::ostream&out, const SubstitutionArray<T>&array) { + out << '['; + for (unsigned i = 0; i < array.getSize(); ++i) { + out << array[i] << ','; + } + return out << "X]"; +} + +template<class T, class COMPARE = std::less<T> > + class SubstitutionArrayComparator { +public: + bool operator()(const Array<T>&left,const Array<T>&right) { + static COMPARE compare; + unsigned leftSize = left.getSize(); + unsigned rightSize = right.getSize(); + if (leftSize < rightSize) { + return true; + } + if (leftSize > rightSize) { + return false; + } + for (unsigned i = 0; i < leftSize; ++i) { + if (compare(left[i], right[i])) { + return true; + } + if (compare(right[i], left[i])) { + return false; + } + } + return false; + } +}; + +#endif diff --git a/common/utility/igreater.H b/common/utility/igreater.H new file mode 100644 index 0000000..a32d62c --- /dev/null +++ b/common/utility/igreater.H @@ -0,0 +1,36 @@ +// Copyright 2008, 2009 Brady J. Garvin + +// This file is part of Covering Arrays by Simulated Annealing (CASA). + +// CASA 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 3 of the License, or +// (at your option) any later version. + +// CASA 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 CASA. If not, see <http://www.gnu.org/licenses/>. + + +#ifndef IGREATER_H +#define IGREATER_H + +// Compares two indices by the elements in an array at those locations. Returns +// true if the left indexth element is greater than the right indexth element. + +template<class T>class igreater { +protected: + const T* array; +public: + igreater(const T*array) : + array(array) {} + bool operator ()(unsigned left, unsigned right) const { + return array[right] < array[left]; + } +}; + +#endif diff --git a/common/utility/iless.H b/common/utility/iless.H new file mode 100644 index 0000000..58aa7dc --- /dev/null +++ b/common/utility/iless.H @@ -0,0 +1,36 @@ +// Copyright 2008, 2009 Brady J. Garvin + +// This file is part of Covering Arrays by Simulated Annealing (CASA). + +// CASA 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 3 of the License, or +// (at your option) any later version. + +// CASA 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 CASA. If not, see <http://www.gnu.org/licenses/>. + + +#ifndef ILESS_H +#define ILESS_H + +// Compares two indices by the elements in an array at those locations. Returns +// true if the left indexth element is less than the right indexth element. + +template<class T>class iless { +protected: + const T* array; +public: + iless(const T*array) : + array(array) {} + bool operator ()(unsigned left, unsigned right) const { + return array[left] < array[right]; + } +}; + +#endif diff --git a/common/utility/pgreater.H b/common/utility/pgreater.H new file mode 100644 index 0000000..6a0a007 --- /dev/null +++ b/common/utility/pgreater.H @@ -0,0 +1,32 @@ +// Copyright 2008, 2009 Brady J. Garvin + +// This file is part of Covering Arrays by Simulated Annealing (CASA). + +// CASA 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 3 of the License, or +// (at your option) any later version. + +// CASA 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 CASA. If not, see <http://www.gnu.org/licenses/>. + + +#ifndef PGREATER_H +#define PGREATER_H + +// Compares two pointers by the objects they point to. Returns true if +// dereferenced left is greater than dereferenced right. + +template<class T>class pgreater { +public: + bool operator ()(const T*left, const T*right) const { + return *right < *left; + } +}; + +#endif diff --git a/common/utility/pless.H b/common/utility/pless.H new file mode 100644 index 0000000..f79d76a --- /dev/null +++ b/common/utility/pless.H @@ -0,0 +1,32 @@ +// Copyright 2008, 2009 Brady J. Garvin + +// This file is part of Covering Arrays by Simulated Annealing (CASA). + +// CASA 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 3 of the License, or +// (at your option) any later version. + +// CASA 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 CASA. If not, see <http://www.gnu.org/licenses/>. + + +#ifndef PLESS_H +#define PLESS_H + +// Compares two pointers by the objects they point to. Returns true if +// dereferenced left is less than dereferenced right. + +template<class T>class pless { +public: + bool operator ()(const T*left, const T*right) const { + return *left < *right; + } +}; + +#endif diff --git a/common/utility/relation.H b/common/utility/relation.H new file mode 100644 index 0000000..1c5f0ad --- /dev/null +++ b/common/utility/relation.H @@ -0,0 +1,260 @@ +// Copyright 2008, 2009 Brady J. Garvin + +// This file is part of Covering Arrays by Simulated Annealing (CASA). + +// CASA 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 3 of the License, or +// (at your option) any later version. + +// CASA 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 CASA. If not, see <http://www.gnu.org/licenses/>. + + +#ifndef RELATION_H +#define RELATION_H + +#include <cassert> +#include <iostream> +#include <set> +#include <map> + +// A bidirectional (multi-)map where either the either the key or data type (or +// both) can be forced to be unique. + +// Naming conventions (including abbreviations in identifier names) here +// resemble those used in the STL, rather than the more Java-like standard in +// the other code. + +template<class key_type, class data_type, bool unique_key, bool unique_data, + class key_compare = std::less<key_type>, + class data_compare = std::less<data_type> >class relation { +protected: + typedef relation + <key_type, data_type, unique_key, unique_data, key_compare, data_compare> + relation_type; + + std::multimap<key_type, data_type, key_compare> + by_key; + std::multimap<data_type, key_type, data_compare> + by_data; +public: + typedef unsigned size_type; + typedef int difference_type; + + // By-key iterators: +#define KEY(type) \ + typedef typename std::multimap<key_type, data_type, key_compare>::type \ + key_ ## type + KEY(iterator); + KEY(const_iterator); + KEY(reverse_iterator); + KEY(const_reverse_iterator); +#undef KEY + + // By-data iterators: +#define DATA(type) \ + typedef typename std::multimap<data_type, key_type, data_compare>::type \ + data_ ## type + DATA(iterator); + DATA(const_iterator); + DATA(reverse_iterator); + DATA(const_reverse_iterator); +#undef DATA + + // Create, copy, and delete: + relation() {} + relation(const key_compare&key_comp, const data_compare&data_comp) : + by_key(key_comp), + by_data(data_comp) {} + relation(const relation_type©) : + by_key(copy.by_key), + by_data(copy.by_data) {} + relation&operator =(const relation_type©) { + by_key = copy.by_key; + by_data = copy.by_data; + } + void swap(relation_type&other) { + by_key.swap(other.by_key); + by_data.swap(other.by_data); + } + virtual ~relation() {} + // Access and mutate: + // By key: + key_compare key_comp() const { + return by_key.key_comp(); + } +#define KEY(method, constness) key_ ## method() constness { \ + return by_key.method(); \ + } + key_iterator KEY(begin,); + key_iterator KEY(end,); + key_const_iterator KEY(begin, const); + key_const_iterator KEY(end, const); + key_reverse_iterator KEY(rbegin,); + key_reverse_iterator KEY(rend,); + key_const_reverse_iterator KEY(rbegin, const); + key_const_reverse_iterator KEY(rend, const); +#undef KEY +#define KEY(method,constness) key_ ## method(const key_type&key) constness { \ + return by_key.method(key); \ + } + key_iterator KEY(find,); + size_type KEY(count,); + key_iterator KEY(lower_bound,); + key_const_iterator KEY(lower_bound, const); + key_iterator KEY(upper_bound,); + key_const_iterator KEY(upper_bound, const); + std::pair<key_iterator, key_iterator> KEY(equal_range,); + std::pair<key_const_iterator, key_const_iterator> KEY(equal_range, const); +#undef KEY + // (Return whether insertion was successful as second.) + std::pair<key_iterator, bool>key_insert + (const key_type&key, const data_type&data) { + key_iterator key_hint = by_key.find(key); + data_iterator data_hint = by_data.find(data); + if ((unique_key && key_hint != by_key.end()) || + (unique_data && data_hint != by_data.end())) { + return std::pair<key_iterator, bool>(by_key.end(), false); + } + by_data.insert(data_hint, std::pair<data_type, key_type>(data, key)); + return std::pair<key_iterator, bool> + (by_key.insert + (key_hint, std::pair<key_type, data_type>(key, data)), true); + } + void key_erase(key_iterator pos) { + std::pair<data_iterator, data_iterator>data_pos = + by_data.equal_range(pos->second); + key_type match = pos->first; + for (; data_pos.first != data_pos.second; ++data_pos.first) { + key_type&candidate = data_pos.first->second; + if (!by_key.key_comp()(candidate, match) && + !by_key.key_comp()(match, candidate)) { + by_key.erase(pos); + by_data.erase(data_pos.first); + return; + } + } + assert(false); + } + size_type key_erase(const key_type&key) { + size_type result = 0; + std::pair<key_iterator, key_iterator>range = by_key.equal_range(key); + while (range.first != range.second) { + key_iterator tag = range.first++; + erase(tag); + ++result; + } + return result; + } + + // By data: + data_compare data_comp() const { + return by_data.data_comp(); + } +#define DATA(method, constness) data_ ## method() constness { \ + return by_data.method(); \ + } + data_iterator DATA(begin,); + data_iterator DATA(end,); + data_const_iterator DATA(begin, const); + data_const_iterator DATA(end, const); + data_reverse_iterator DATA(rbegin,); + data_reverse_iterator DATA(rend,); + data_const_reverse_iterator DATA(rbegin, const); + data_const_reverse_iterator DATA(rend, const); +#undef DATA +#define DATA(method, constness) \ + data_ ## method(const data_type&data) constness { \ + return by_data.method(data); \ + } + data_iterator DATA(find,); + size_type DATA(count,); + data_iterator DATA(lower_bound,); + data_const_iterator DATA(lower_bound, const); + data_iterator DATA(upper_bound,); + data_const_iterator DATA(upper_bound, const); + std::pair<data_iterator, data_iterator> DATA(equal_range,); + std::pair<data_const_iterator, data_const_iterator> DATA(equal_range, const); +#undef DATA + // (Return whether insertion was successful as second.) + std::pair<data_iterator, bool>data_insert + (const key_type&key, const data_type&data) { + key_iterator key_hint = by_key.find(key); + data_iterator data_hint = by_data.find(data); + if ((unique_key && key_hint != by_key.end()) || + (unique_data && data_hint != by_data.end())) { + return std::pair<data_iterator, bool>(by_data.end(), false); + } + by_key.insert(key_hint, std::pair<key_type, data_type>(key, data)); + return std::pair<data_iterator, bool> + (by_data.insert + (data_hint, std::pair<data_type, key_type>(data, key)), true); + } + void data_erase(data_iterator pos) { + std::pair<key_iterator, key_iterator>key_pos = by_key.equal_range(pos->second); + data_type match = pos->first; + for (; key_pos.first != key_pos.second; ++key_pos.first) { + data_type&candidate = key_pos.first->second; + if (!by_data.key_comp()(candidate, match) && + !by_data.key_comp()(match, candidate)) { + by_data.erase(pos); + by_key.erase(key_pos.first); + return; + } + } + assert(false); + } + size_type data_erase(const data_type&data) { + size_type result = 0; + std::pair<data_iterator, data_iterator>range = by_data.equal_range(data); + while (range.first != range.second) { + data_iterator tag = range.first++; + erase(tag); + ++result; + } + return result; + } + + // Others: + void clear() { + by_key.clear(); + by_data.clear(); + } + size_type size() const { + assert(by_key.size() == by_data.size()); + return by_key.size(); + } + size_type max_size() const { + assert(by_key.max_size() == by_data.max_size()); + return by_key.max_size(); + } + bool empty() const { + assert(by_key.empty() == by_data.empty()); + return by_key.empty(); + } +}; + +template<class key_type, class data_type, bool unique_key, bool unique_data, + class key_compare, class data_compare>std::ostream&operator << + (std::ostream&out, + const relation<key_type, data_type, unique_key, unique_data, key_compare, + data_compare>&rel) { + out << "relation{\n"; + for (typename relation<key_type, data_type, unique_key, unique_data, + key_compare, data_compare>::key_const_iterator iterator = + rel.key_begin(), + end = rel.key_end(); + iterator != end; + ++iterator) { + out << " " << *(iterator->first) << " with " << iterator->second << '\n'; + } + return out << "}\n"; +} + +#endif diff --git a/example.citmodel b/example.citmodel new file mode 100644 index 0000000..a6126d6 --- /dev/null +++ b/example.citmodel @@ -0,0 +1,3 @@ +4 +5 +2 2 2 2 3 diff --git a/example.constraints b/example.constraints new file mode 100644 index 0000000..9fbe7bb --- /dev/null +++ b/example.constraints @@ -0,0 +1,5 @@ +2 +2 +- 0 - 8 +3 +- 3 + 4 + 7 diff --git a/example.coveringarray b/example.coveringarray new file mode 100644 index 0000000..f075abf --- /dev/null +++ b/example.coveringarray @@ -0,0 +1,28 @@ +27 +0 2 4 6 9 +0 2 4 7 10 +0 2 5 6 10 +0 2 5 6 9 +0 2 5 7 9 +0 3 4 6 10 +0 3 4 6 9 +0 3 4 7 9 +0 3 5 7 10 +0 3 5 7 9 +1 2 4 6 10 +1 2 4 6 8 +1 2 4 7 8 +1 2 4 7 9 +1 2 5 6 10 +1 2 5 6 8 +1 2 5 6 9 +1 2 5 7 10 +1 2 5 7 8 +1 3 4 6 10 +1 3 4 6 8 +1 3 4 6 9 +1 3 4 7 10 +1 3 4 7 8 +1 3 5 7 10 +1 3 5 7 8 +1 3 5 7 9 diff --git a/minisat/LICENSE b/minisat/LICENSE new file mode 100644 index 0000000..c87a327 --- /dev/null +++ b/minisat/LICENSE @@ -0,0 +1,20 @@ +MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson + +Permission is hereby granted, free of charge, to any person obtaining a +copy of this software and associated documentation files (the +"Software"), to deal in the Software without restriction, including +without limitation the rights to use, copy, modify, merge, publish, +distribute, sublicense, and/or sell copies of the Software, and to +permit persons to whom the Software is furnished to do so, subject to +the following conditions: + +The above copyright notice and this permission notice shall be included +in all copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS +OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF +MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE +LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION +OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION +WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. diff --git a/minisat/include/Alg.h b/minisat/include/Alg.h new file mode 100644 index 0000000..240962d --- /dev/null +++ b/minisat/include/Alg.h @@ -0,0 +1,57 @@ +/*******************************************************************************************[Alg.h] +MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson + +Permission is hereby granted, free of charge, to any person obtaining a copy of this software and +associated documentation files (the "Software"), to deal in the Software without restriction, +including without limitation the rights to use, copy, modify, merge, publish, distribute, +sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all copies or +substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT +NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, +DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT +OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +**************************************************************************************************/ + +#ifndef Alg_h +#define Alg_h + +//================================================================================================= +// Useful functions on vectors + + +#if 1 +template<class V, class T> +static inline void remove(V& ts, const T& t) +{ + int j = 0; + for (; j < ts.size() && ts[j] != t; j++); + assert(j < ts.size()); + for (; j < ts.size()-1; j++) ts[j] = ts[j+1]; + ts.pop(); +} +#else +template<class V, class T> +static inline void remove(V& ts, const T& t) +{ + int j = 0; + for (; j < ts.size() && ts[j] != t; j++); + assert(j < ts.size()); + ts[j] = ts.last(); + ts.pop(); +} +#endif + +template<class V, class T> +static inline bool find(V& ts, const T& t) +{ + int j = 0; + for (; j < ts.size() && ts[j] != t; j++); + return j < ts.size(); +} + +#endif diff --git a/minisat/include/BasicHeap.h b/minisat/include/BasicHeap.h new file mode 100644 index 0000000..556d98f --- /dev/null +++ b/minisat/include/BasicHeap.h @@ -0,0 +1,98 @@ +/******************************************************************************************[Heap.h] +MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson + +Permission is hereby granted, free of charge, to any person obtaining a copy of this software and +associated documentation files (the "Software"), to deal in the Software without restriction, +including without limitation the rights to use, copy, modify, merge, publish, distribute, +sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all copies or +substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT +NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, +DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT +OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +**************************************************************************************************/ + +#ifndef BasicHeap_h +#define BasicHeap_h + +#include "Vec.h" + +//================================================================================================= +// A heap implementation with support for decrease/increase key. + + +template<class Comp> +class BasicHeap { + Comp lt; + vec<int> heap; // heap of ints + + // Index "traversal" functions + static inline int left (int i) { return i*2+1; } + static inline int right (int i) { return (i+1)*2; } + static inline int parent(int i) { return (i-1) >> 1; } + + inline void percolateUp(int i) + { + int x = heap[i]; + while (i != 0 && lt(x, heap[parent(i)])){ + heap[i] = heap[parent(i)]; + i = parent(i); + } + heap [i] = x; + } + + + inline void percolateDown(int i) + { + int x = heap[i]; + while (left(i) < heap.size()){ + int child = right(i) < heap.size() && lt(heap[right(i)], heap[left(i)]) ? right(i) : left(i); + if (!lt(heap[child], x)) break; + heap[i] = heap[child]; + i = child; + } + heap[i] = x; + } + + + bool heapProperty(int i) { + return i >= heap.size() + || ((i == 0 || !lt(heap[i], heap[parent(i)])) && heapProperty(left(i)) && heapProperty(right(i))); } + + + public: + BasicHeap(const C& c) : comp(c) { } + + int size () const { return heap.size(); } + bool empty () const { return heap.size() == 0; } + int operator[](int index) const { return heap[index+1]; } + void clear (bool dealloc = false) { heap.clear(dealloc); } + void insert (int n) { heap.push(n); percolateUp(heap.size()-1); } + + + int removeMin() { + int r = heap[0]; + heap[0] = heap.last(); + heap.pop(); + if (heap.size() > 1) percolateDown(0); + return r; + } + + + // DEBUG: consistency checking + bool heapProperty() { + return heapProperty(1); } + + + // COMPAT: should be removed + int getmin () { return removeMin(); } +}; + + +//================================================================================================= +#endif diff --git a/minisat/include/BoxedVec.h b/minisat/include/BoxedVec.h new file mode 100644 index 0000000..bddf410 --- /dev/null +++ b/minisat/include/BoxedVec.h @@ -0,0 +1,147 @@ +/*******************************************************************************************[Vec.h] +MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson + +Permission is hereby granted, free of charge, to any person obtaining a copy of this software and +associated documentation files (the "Software"), to deal in the Software without restriction, +including without limitation the rights to use, copy, modify, merge, publish, distribute, +sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all copies or +substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT +NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, +DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT +OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +**************************************************************************************************/ + +#ifndef BoxedVec_h +#define BoxedVec_h + +#include <cstdlib> +#include <cassert> +#include <new> + +//================================================================================================= +// Automatically resizable arrays +// +// NOTE! Don't use this vector on datatypes that cannot be re-located in memory (with realloc) + +template<class T> +class bvec { + + static inline int imin(int x, int y) { + int mask = (x-y) >> (sizeof(int)*8-1); + return (x&mask) + (y&(~mask)); } + + static inline int imax(int x, int y) { + int mask = (y-x) >> (sizeof(int)*8-1); + return (x&mask) + (y&(~mask)); } + + struct Vec_t { + int sz; + int cap; + T data[0]; + + static Vec_t* alloc(Vec_t* x, int size){ + x = (Vec_t*)realloc((void*)x, sizeof(Vec_t) + sizeof(T)*size); + x->cap = size; + return x; + } + + }; + + Vec_t* ref; + + static const int init_size = 2; + static int nextSize (int current) { return (current * 3 + 1) >> 1; } + static int fitSize (int needed) { int x; for (x = init_size; needed > x; x = nextSize(x)); return x; } + + void fill (int size) { + assert(ref != NULL); + for (T* i = ref->data; i < ref->data + size; i++) + new (i) T(); + } + + void fill (int size, const T& pad) { + assert(ref != NULL); + for (T* i = ref->data; i < ref->data + size; i++) + new (i) T(pad); + } + + // Don't allow copying (error prone): + altvec<T>& operator = (altvec<T>& other) { assert(0); } + altvec (altvec<T>& other) { assert(0); } + +public: + void clear (bool dealloc = false) { + if (ref != NULL){ + for (int i = 0; i < ref->sz; i++) + (*ref).data[i].~T(); + + if (dealloc) { + free(ref); ref = NULL; + }else + ref->sz = 0; + } + } + + // Constructors: + altvec(void) : ref (NULL) { } + altvec(int size) : ref (Vec_t::alloc(NULL, fitSize(size))) { fill(size); ref->sz = size; } + altvec(int size, const T& pad) : ref (Vec_t::alloc(NULL, fitSize(size))) { fill(size, pad); ref->sz = size; } + ~altvec(void) { clear(true); } + + // Ownership of underlying array: + operator T* (void) { return ref->data; } // (unsafe but convenient) + operator const T* (void) const { return ref->data; } + + // Size operations: + int size (void) const { return ref != NULL ? ref->sz : 0; } + + void pop (void) { assert(ref != NULL && ref->sz > 0); int last = --ref->sz; ref->data[last].~T(); } + void push (const T& elem) { + int size = ref != NULL ? ref->sz : 0; + int cap = ref != NULL ? ref->cap : 0; + if (size == cap){ + cap = cap != 0 ? nextSize(cap) : init_size; + ref = Vec_t::alloc(ref, cap); + } + //new (&ref->data[size]) T(elem); + ref->data[size] = elem; + ref->sz = size+1; + } + + void push () { + int size = ref != NULL ? ref->sz : 0; + int cap = ref != NULL ? ref->cap : 0; + if (size == cap){ + cap = cap != 0 ? nextSize(cap) : init_size; + ref = Vec_t::alloc(ref, cap); + } + new (&ref->data[size]) T(); + ref->sz = size+1; + } + + void shrink (int nelems) { for (int i = 0; i < nelems; i++) pop(); } + void shrink_(int nelems) { for (int i = 0; i < nelems; i++) pop(); } + void growTo (int size) { while (this->size() < size) push(); } + void growTo (int size, const T& pad) { while (this->size() < size) push(pad); } + void capacity (int size) { growTo(size); } + + const T& last (void) const { return ref->data[ref->sz-1]; } + T& last (void) { return ref->data[ref->sz-1]; } + + // Vector interface: + const T& operator [] (int index) const { return ref->data[index]; } + T& operator [] (int index) { return ref->data[index]; } + + void copyTo(altvec<T>& copy) const { copy.clear(); for (int i = 0; i < size(); i++) copy.push(ref->data[i]); } + void moveTo(altvec<T>& dest) { dest.clear(true); dest.ref = ref; ref = NULL; } + +}; + + +#endif diff --git a/minisat/include/Heap.h b/minisat/include/Heap.h new file mode 100644 index 0000000..b07ccd1 --- /dev/null +++ b/minisat/include/Heap.h @@ -0,0 +1,169 @@ +/******************************************************************************************[Heap.h] +MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson + +Permission is hereby granted, free of charge, to any person obtaining a copy of this software and +associated documentation files (the "Software"), to deal in the Software without restriction, +including without limitation the rights to use, copy, modify, merge, publish, distribute, +sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all copies or +substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT +NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, +DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT +OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +**************************************************************************************************/ + +#ifndef Heap_h +#define Heap_h + +#include "Vec.h" + +//================================================================================================= +// A heap implementation with support for decrease/increase key. + + +template<class Comp> +class Heap { + Comp lt; + vec<int> heap; // heap of ints + vec<int> indices; // int -> index in heap + + // Index "traversal" functions + static inline int left (int i) { return i*2+1; } + static inline int right (int i) { return (i+1)*2; } + static inline int parent(int i) { return (i-1) >> 1; } + + + inline void percolateUp(int i) + { + int x = heap[i]; + while (i != 0 && lt(x, heap[parent(i)])){ + heap[i] = heap[parent(i)]; + indices[heap[i]] = i; + i = parent(i); + } + heap [i] = x; + indices[x] = i; + } + + + inline void percolateDown(int i) + { + int x = heap[i]; + while (left(i) < heap.size()){ + int child = right(i) < heap.size() && lt(heap[right(i)], heap[left(i)]) ? right(i) : left(i); + if (!lt(heap[child], x)) break; + heap[i] = heap[child]; + indices[heap[i]] = i; + i = child; + } + heap [i] = x; + indices[x] = i; + } + + + bool heapProperty (int i) const { + return i >= heap.size() + || ((i == 0 || !lt(heap[i], heap[parent(i)])) && heapProperty(left(i)) && heapProperty(right(i))); } + + + public: + Heap(const Comp& c) : lt(c) { } + + int size () const { return heap.size(); } + bool empty () const { return heap.size() == 0; } + bool inHeap (int n) const { return n < indices.size() && indices[n] >= 0; } + int operator[](int index) const { assert(index < heap.size()); return heap[index]; } + + void decrease (int n) { assert(inHeap(n)); percolateUp(indices[n]); } + + // RENAME WHEN THE DEPRECATED INCREASE IS REMOVED. + void increase_ (int n) { assert(inHeap(n)); percolateDown(indices[n]); } + + + void insert(int n) + { + indices.growTo(n+1, -1); + assert(!inHeap(n)); + + indices[n] = heap.size(); + heap.push(n); + percolateUp(indices[n]); + } + + + int removeMin() + { + int x = heap[0]; + heap[0] = heap.last(); + indices[heap[0]] = 0; + indices[x] = -1; + heap.pop(); + if (heap.size() > 1) percolateDown(0); + return x; + } + + + void clear(bool dealloc = false) + { + for (int i = 0; i < heap.size(); i++) + indices[heap[i]] = -1; +#ifdef NDEBUG + for (int i = 0; i < indices.size(); i++) + assert(indices[i] == -1); +#endif + heap.clear(dealloc); + } + + + // Fool proof variant of insert/decrease/increase + void update (int n) + { + if (!inHeap(n)) + insert(n); + else { + percolateUp(indices[n]); + percolateDown(indices[n]); + } + } + + + // Delete elements from the heap using a given filter function (-object). + // *** this could probaly be replaced with a more general "buildHeap(vec<int>&)" method *** + template <class F> + void filter(const F& filt) { + int i,j; + for (i = j = 0; i < heap.size(); i++) + if (filt(heap[i])){ + heap[j] = heap[i]; + indices[heap[i]] = j++; + }else + indices[heap[i]] = -1; + + heap.shrink(i - j); + for (int i = heap.size() / 2 - 1; i >= 0; i--) + percolateDown(i); + + assert(heapProperty()); + } + + + // DEBUG: consistency checking + bool heapProperty() const { + return heapProperty(1); } + + + // COMPAT: should be removed + void setBounds (int n) { } + void increase (int n) { decrease(n); } + int getmin () { return removeMin(); } + +}; + + +//================================================================================================= +#endif diff --git a/minisat/include/Map.h b/minisat/include/Map.h new file mode 100644 index 0000000..b6d76a3 --- /dev/null +++ b/minisat/include/Map.h @@ -0,0 +1,118 @@ +/*******************************************************************************************[Map.h] +MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson + +Permission is hereby granted, free of charge, to any person obtaining a copy of this software and +associated documentation files (the "Software"), to deal in the Software without restriction, +including without limitation the rights to use, copy, modify, merge, publish, distribute, +sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all copies or +substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT +NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, +DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT +OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +**************************************************************************************************/ + +#ifndef Map_h +#define Map_h + +#include <stdint.h> + +#include "Vec.h" + +//================================================================================================= +// Default hash/equals functions +// + +template<class K> struct Hash { uint32_t operator()(const K& k) const { return hash(k); } }; +template<class K> struct Equal { bool operator()(const K& k1, const K& k2) const { return k1 == k2; } }; + +template<class K> struct DeepHash { uint32_t operator()(const K* k) const { return hash(*k); } }; +template<class K> struct DeepEqual { bool operator()(const K* k1, const K* k2) const { return *k1 == *k2; } }; + +//================================================================================================= +// Some primes +// + +static const int nprimes = 25; +static const int primes [nprimes] = { 31, 73, 151, 313, 643, 1291, 2593, 5233, 10501, 21013, 42073, 84181, 168451, 337219, 674701, 1349473, 2699299, 5398891, 10798093, 21596719, 43193641, 86387383, 172775299, 345550609, 691101253 }; + +//================================================================================================= +// Hash table implementation of Maps +// + +template<class K, class D, class H = Hash<K>, class E = Equal<K> > +class Map { + struct Pair { K key; D data; }; + + H hash; + E equals; + + vec<Pair>* table; + int cap; + int size; + + // Don't allow copying (error prone): + Map<K,D,H,E>& operator = (Map<K,D,H,E>& other) { assert(0); } + Map (Map<K,D,H,E>& other) { assert(0); } + + int32_t index (const K& k) const { return hash(k) % cap; } + void _insert (const K& k, const D& d) { table[index(k)].push(); table[index(k)].last().key = k; table[index(k)].last().data = d; } + void rehash () { + const vec<Pair>* old = table; + + int newsize = primes[0]; + for (int i = 1; newsize <= cap && i < nprimes; i++) + newsize = primes[i]; + + table = new vec<Pair>[newsize]; + + for (int i = 0; i < cap; i++){ + for (int j = 0; j < old[i].size(); j++){ + _insert(old[i][j].key, old[i][j].data); }} + + delete [] old; + + cap = newsize; + } + + + public: + + Map () : table(NULL), cap(0), size(0) {} + Map (const H& h, const E& e) : Map(), hash(h), equals(e) {} + ~Map () { delete [] table; } + + void insert (const K& k, const D& d) { if (size+1 > cap / 2) rehash(); _insert(k, d); size++; } + bool peek (const K& k, D& d) { + if (size == 0) return false; + const vec<Pair>& ps = table[index(k)]; + for (int i = 0; i < ps.size(); i++) + if (equals(ps[i].key, k)){ + d = ps[i].data; + return true; } + return false; + } + + void remove (const K& k) { + assert(table != NULL); + vec<Pair>& ps = table[index(k)]; + int j = 0; + for (; j < ps.size() && !equals(ps[j].key, k); j++); + assert(j < ps.size()); + ps[j] = ps.last(); + ps.pop(); + } + + void clear () { + cap = size = 0; + delete [] table; + table = NULL; + } +}; + +#endif diff --git a/minisat/include/Queue.h b/minisat/include/Queue.h new file mode 100644 index 0000000..2cc110c --- /dev/null +++ b/minisat/include/Queue.h @@ -0,0 +1,82 @@ +/*****************************************************************************************[Queue.h] +MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson + +Permission is hereby granted, free of charge, to any person obtaining a copy of this software and +associated documentation files (the "Software"), to deal in the Software without restriction, +including without limitation the rights to use, copy, modify, merge, publish, distribute, +sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all copies or +substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT +NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, +DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT +OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +**************************************************************************************************/ + +#ifndef Queue_h +#define Queue_h + +#include "Vec.h" + +//================================================================================================= + + +template <class T> +class Queue { + vec<T> elems; + int first; + +public: + Queue(void) : first(0) { } + + void insert(T x) { elems.push(x); } + T peek () const { return elems[first]; } + void pop () { first++; } + + void clear(bool dealloc = false) { elems.clear(dealloc); first = 0; } + int size(void) { return elems.size() - first; } + + //bool has(T x) { for (int i = first; i < elems.size(); i++) if (elems[i] == x) return true; return false; } + + const T& operator [] (int index) const { return elems[first + index]; } + +}; + +//template<class T> +//class Queue { +// vec<T> buf; +// int first; +// int end; +// +//public: +// typedef T Key; +// +// Queue() : buf(1), first(0), end(0) {} +// +// void clear () { buf.shrinkTo(1); first = end = 0; } +// int size () { return (end >= first) ? end - first : end - first + buf.size(); } +// +// T peek () { assert(first != end); return buf[first]; } +// void pop () { assert(first != end); first++; if (first == buf.size()) first = 0; } +// void insert(T elem) { // INVARIANT: buf[end] is always unused +// buf[end++] = elem; +// if (end == buf.size()) end = 0; +// if (first == end){ // Resize: +// vec<T> tmp((buf.size()*3 + 1) >> 1); +// //**/printf("queue alloc: %d elems (%.1f MB)\n", tmp.size(), tmp.size() * sizeof(T) / 1000000.0); +// int i = 0; +// for (int j = first; j < buf.size(); j++) tmp[i++] = buf[j]; +// for (int j = 0 ; j < end ; j++) tmp[i++] = buf[j]; +// first = 0; +// end = buf.size(); +// tmp.moveTo(buf); +// } +// } +//}; + +//================================================================================================= +#endif diff --git a/minisat/include/Sort.h b/minisat/include/Sort.h new file mode 100644 index 0000000..1f301f5 --- /dev/null +++ b/minisat/include/Sort.h @@ -0,0 +1,93 @@ +/******************************************************************************************[Sort.h] +MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson + +Permission is hereby granted, free of charge, to any person obtaining a copy of this software and +associated documentation files (the "Software"), to deal in the Software without restriction, +including without limitation the rights to use, copy, modify, merge, publish, distribute, +sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all copies or +substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT +NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, +DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT +OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +**************************************************************************************************/ + +#ifndef Sort_h +#define Sort_h + +#include "Vec.h" + +//================================================================================================= +// Some sorting algorithms for vec's + + +template<class T> +struct LessThan_default { + bool operator () (T x, T y) { return x < y; } +}; + + +template <class T, class LessThan> +void selectionSort(T* array, int size, LessThan lt) +{ + int i, j, best_i; + T tmp; + + for (i = 0; i < size-1; i++){ + best_i = i; + for (j = i+1; j < size; j++){ + if (lt(array[j], array[best_i])) + best_i = j; + } + tmp = array[i]; array[i] = array[best_i]; array[best_i] = tmp; + } +} +template <class T> static inline void selectionSort(T* array, int size) { + selectionSort(array, size, LessThan_default<T>()); } + +template <class T, class LessThan> +void sort(T* array, int size, LessThan lt) +{ + if (size <= 15) + selectionSort(array, size, lt); + + else{ + T pivot = array[size / 2]; + T tmp; + int i = -1; + int j = size; + + for(;;){ + do i++; while(lt(array[i], pivot)); + do j--; while(lt(pivot, array[j])); + + if (i >= j) break; + + tmp = array[i]; array[i] = array[j]; array[j] = tmp; + } + + sort(array , i , lt); + sort(&array[i], size-i, lt); + } +} +template <class T> static inline void sort(T* array, int size) { + sort(array, size, LessThan_default<T>()); } + + +//================================================================================================= +// For 'vec's: + + +template <class T, class LessThan> void sort(vec<T>& v, LessThan lt) { + sort((T*)v, v.size(), lt); } +template <class T> void sort(vec<T>& v) { + sort(v, LessThan_default<T>()); } + + +//================================================================================================= +#endif diff --git a/minisat/include/Vec.h b/minisat/include/Vec.h new file mode 100644 index 0000000..e780aa1 --- /dev/null +++ b/minisat/include/Vec.h @@ -0,0 +1,133 @@ +/*******************************************************************************************[Vec.h] +MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson + +Permission is hereby granted, free of charge, to any person obtaining a copy of this software and +associated documentation files (the "Software"), to deal in the Software without restriction, +including without limitation the rights to use, copy, modify, merge, publish, distribute, +sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all copies or +substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT +NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, +DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT +OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +**************************************************************************************************/ + +#ifndef Vec_h +#define Vec_h + +#include <cstdlib> +#include <cassert> +#include <new> + +//================================================================================================= +// Automatically resizable arrays +// +// NOTE! Don't use this vector on datatypes that cannot be re-located in memory (with realloc) + +template<class T> +class vec { + T* data; + int sz; + int cap; + + void init(int size, const T& pad); + void grow(int min_cap); + + // Don't allow copying (error prone): + vec<T>& operator = (vec<T>& other) { assert(0); return *this; } + vec (vec<T>& other) { assert(0); } + + static inline int imin(int x, int y) { + int mask = (x-y) >> (sizeof(int)*8-1); + return (x&mask) + (y&(~mask)); } + + static inline int imax(int x, int y) { + int mask = (y-x) >> (sizeof(int)*8-1); + return (x&mask) + (y&(~mask)); } + +public: + // Types: + typedef int Key; + typedef T Datum; + + // Constructors: + vec(void) : data(NULL) , sz(0) , cap(0) { } + vec(int size) : data(NULL) , sz(0) , cap(0) { growTo(size); } + vec(int size, const T& pad) : data(NULL) , sz(0) , cap(0) { growTo(size, pad); } + vec(T* array, int size) : data(array), sz(size), cap(size) { } // (takes ownership of array -- will be deallocated with 'free()') + ~vec(void) { clear(true); } + + // Ownership of underlying array: + T* release (void) { T* ret = data; data = NULL; sz = 0; cap = 0; return ret; } + operator T* (void) { return data; } // (unsafe but convenient) + operator const T* (void) const { return data; } + + // Size operations: + int size (void) const { return sz; } + void shrink (int nelems) { assert(nelems <= sz); for (int i = 0; i < nelems; i++) sz--, data[sz].~T(); } + void shrink_(int nelems) { assert(nelems <= sz); sz -= nelems; } + void pop (void) { sz--, data[sz].~T(); } + void growTo (int size); + void growTo (int size, const T& pad); + void clear (bool dealloc = false); + void capacity (int size) { grow(size); } + + // Stack interface: +#if 1 + void push (void) { if (sz == cap) { cap = imax(2, (cap*3+1)>>1); data = (T*)realloc(data, cap * sizeof(T)); } new (&data[sz]) T(); sz++; } + //void push (const T& elem) { if (sz == cap) { cap = imax(2, (cap*3+1)>>1); data = (T*)realloc(data, cap * sizeof(T)); } new (&data[sz]) T(elem); sz++; } + void push (const T& elem) { if (sz == cap) { cap = imax(2, (cap*3+1)>>1); data = (T*)realloc(data, cap * sizeof(T)); } data[sz++] = elem; } + void push_ (const T& elem) { assert(sz < cap); data[sz++] = elem; } +#else + void push (void) { if (sz == cap) grow(sz+1); new (&data[sz]) T() ; sz++; } + void push (const T& elem) { if (sz == cap) grow(sz+1); new (&data[sz]) T(elem); sz++; } +#endif + + const T& last (void) const { return data[sz-1]; } + T& last (void) { return data[sz-1]; } + + // Vector interface: + const T& operator [] (int index) const { return data[index]; } + T& operator [] (int index) { return data[index]; } + + + // Duplicatation (preferred instead): + void copyTo(vec<T>& copy) const { copy.clear(); copy.growTo(sz); for (int i = 0; i < sz; i++) new (©[i]) T(data[i]); } + void moveTo(vec<T>& dest) { dest.clear(true); dest.data = data; dest.sz = sz; dest.cap = cap; data = NULL; sz = 0; cap = 0; } +}; + +template<class T> +void vec<T>::grow(int min_cap) { + if (min_cap <= cap) return; + if (cap == 0) cap = (min_cap >= 2) ? min_cap : 2; + else do cap = (cap*3+1) >> 1; while (cap < min_cap); + data = (T*)realloc(data, cap * sizeof(T)); } + +template<class T> +void vec<T>::growTo(int size, const T& pad) { + if (sz >= size) return; + grow(size); + for (int i = sz; i < size; i++) new (&data[i]) T(pad); + sz = size; } + +template<class T> +void vec<T>::growTo(int size) { + if (sz >= size) return; + grow(size); + for (int i = sz; i < size; i++) new (&data[i]) T(); + sz = size; } + +template<class T> +void vec<T>::clear(bool dealloc) { + if (data != NULL){ + for (int i = 0; i < sz; i++) data[i].~T(); + sz = 0; + if (dealloc) free(data), data = NULL, cap = 0; } } + + +#endif diff --git a/minisat/solver/Solver.C b/minisat/solver/Solver.C new file mode 100644 index 0000000..54b45d9 --- /dev/null +++ b/minisat/solver/Solver.C @@ -0,0 +1,746 @@ +/****************************************************************************************[Solver.C] +MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson + +Permission is hereby granted, free of charge, to any person obtaining a copy of this software and +associated documentation files (the "Software"), to deal in the Software without restriction, +including without limitation the rights to use, copy, modify, merge, publish, distribute, +sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all copies or +substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT +NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, +DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT +OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +**************************************************************************************************/ + +#include "Solver.H" +#include "Sort.h" +#include <cmath> + + +//================================================================================================= +// Constructor/Destructor: + + +Solver::Solver() : + + // Parameters: (formerly in 'SearchParams') + var_decay(1 / 0.95), clause_decay(1 / 0.999), random_var_freq(0.02) + , restart_first(100), restart_inc(1.5), learntsize_factor((double)1/(double)3), learntsize_inc(1.1) + + // More parameters: + // + , expensive_ccmin (true) + , polarity_mode (polarity_false) + , verbosity (0) + + // Statistics: (formerly in 'SolverStats') + // + , starts(0), decisions(0), rnd_decisions(0), propagations(0), conflicts(0) + , clauses_literals(0), learnts_literals(0), max_literals(0), tot_literals(0) + + , ok (true) + , cla_inc (1) + , var_inc (1) + , qhead (0) + , simpDB_assigns (-1) + , simpDB_props (0) + , order_heap (VarOrderLt(activity)) + , random_seed (91648253) + , progress_estimate(0) + , remove_satisfied (true) +{} + + +Solver::~Solver() +{ + for (int i = 0; i < learnts.size(); i++) free(learnts[i]); + for (int i = 0; i < clauses.size(); i++) free(clauses[i]); +} + + +//================================================================================================= +// Minor methods: + + +// Creates a new SAT variable in the solver. If 'decision_var' is cleared, variable will not be +// used as a decision variable (NOTE! This has effects on the meaning of a SATISFIABLE result). +// +Var Solver::newVar(bool sign, bool dvar) +{ + int v = nVars(); + watches .push(); // (list for positive literal) + watches .push(); // (list for negative literal) + reason .push(NULL); + assigns .push(toInt(l_Undef)); + level .push(-1); + activity .push(0); + seen .push(0); + + polarity .push((char)sign); + decision_var.push((char)dvar); + + insertVarOrder(v); + return v; +} + + +bool Solver::addClause(vec<Lit>& ps) +{ + assert(decisionLevel() == 0); + + if (!ok) + return false; + else{ + // Check if clause is satisfied and remove false/duplicate literals: + sort(ps); + Lit p; int i, j; + for (i = j = 0, p = lit_Undef; i < ps.size(); i++) + if (value(ps[i]) == l_True || ps[i] == ~p) + return true; + else if (value(ps[i]) != l_False && ps[i] != p) + ps[j++] = p = ps[i]; + ps.shrink(i - j); + } + + if (ps.size() == 0) + return ok = false; + else if (ps.size() == 1){ + assert(value(ps[0]) == l_Undef); + uncheckedEnqueue(ps[0]); + return ok = (propagate() == NULL); + }else{ + Clause* c = Clause_new(ps, false); + clauses.push(c); + attachClause(*c); + } + + return true; +} + + +void Solver::attachClause(Clause& c) { + assert(c.size() > 1); + watches[toInt(~c[0])].push(&c); + watches[toInt(~c[1])].push(&c); + if (c.learnt()) learnts_literals += c.size(); + else clauses_literals += c.size(); } + + +void Solver::detachClause(Clause& c) { + assert(c.size() > 1); + assert(find(watches[toInt(~c[0])], &c)); + assert(find(watches[toInt(~c[1])], &c)); + remove(watches[toInt(~c[0])], &c); + remove(watches[toInt(~c[1])], &c); + if (c.learnt()) learnts_literals -= c.size(); + else clauses_literals -= c.size(); } + + +void Solver::removeClause(Clause& c) { + detachClause(c); + free(&c); } + + +bool Solver::satisfied(const Clause& c) const { + for (int i = 0; i < c.size(); i++) + if (value(c[i]) == l_True) + return true; + return false; } + + +// Revert to the state at given level (keeping all assignment at 'level' but not beyond). +// +void Solver::cancelUntil(int level) { + if (decisionLevel() > level){ + for (int c = trail.size()-1; c >= trail_lim[level]; c--){ + Var x = var(trail[c]); + assigns[x] = toInt(l_Undef); + insertVarOrder(x); } + qhead = trail_lim[level]; + trail.shrink(trail.size() - trail_lim[level]); + trail_lim.shrink(trail_lim.size() - level); + } } + + +//================================================================================================= +// Major methods: + + +Lit Solver::pickBranchLit(int polarity_mode, double random_var_freq) +{ + Var next = var_Undef; + + // Random decision: + if (drand(random_seed) < random_var_freq && !order_heap.empty()){ + next = order_heap[irand(random_seed,order_heap.size())]; + if (toLbool(assigns[next]) == l_Undef && decision_var[next]) + rnd_decisions++; } + + // Activity based decision: + while (next == var_Undef || toLbool(assigns[next]) != l_Undef || !decision_var[next]) + if (order_heap.empty()){ + next = var_Undef; + break; + }else + next = order_heap.removeMin(); + + bool sign = false; + switch (polarity_mode){ + case polarity_true: sign = false; break; + case polarity_false: sign = true; break; + case polarity_user: sign = polarity[next]; break; + case polarity_rnd: sign = irand(random_seed, 2); break; + default: assert(false); } + + return next == var_Undef ? lit_Undef : Lit(next, sign); +} + + +/*_________________________________________________________________________________________________ +| +| analyze : (confl : Clause*) (out_learnt : vec<Lit>&) (out_btlevel : int&) -> [void] +| +| Description: +| Analyze conflict and produce a reason clause. +| +| Pre-conditions: +| * 'out_learnt' is assumed to be cleared. +| * Current decision level must be greater than root level. +| +| Post-conditions: +| * 'out_learnt[0]' is the asserting literal at level 'out_btlevel'. +| +| Effect: +| Will undo part of the trail, upto but not beyond the assumption of the current decision level. +|________________________________________________________________________________________________@*/ +void Solver::analyze(Clause* confl, vec<Lit>& out_learnt, int& out_btlevel) +{ + int pathC = 0; + Lit p = lit_Undef; + + // Generate conflict clause: + // + out_learnt.push(); // (leave room for the asserting literal) + int index = trail.size() - 1; + out_btlevel = 0; + + do{ + assert(confl != NULL); // (otherwise should be UIP) + Clause& c = *confl; + + if (c.learnt()) + claBumpActivity(c); + + for (int j = (p == lit_Undef) ? 0 : 1; j < c.size(); j++){ + Lit q = c[j]; + + if (!seen[var(q)] && level[var(q)] > 0){ + varBumpActivity(var(q)); + seen[var(q)] = 1; + if (level[var(q)] >= decisionLevel()) + pathC++; + else{ + out_learnt.push(q); + if (level[var(q)] > out_btlevel) + out_btlevel = level[var(q)]; + } + } + } + + // Select next clause to look at: + while (!seen[var(trail[index--])]); + p = trail[index+1]; + confl = reason[var(p)]; + seen[var(p)] = 0; + pathC--; + + }while (pathC > 0); + out_learnt[0] = ~p; + + // Simplify conflict clause: + // + int i, j; + if (expensive_ccmin){ + uint32_t abstract_level = 0; + for (i = 1; i < out_learnt.size(); i++) + abstract_level |= abstractLevel(var(out_learnt[i])); // (maintain an abstraction of levels involved in conflict) + + out_learnt.copyTo(analyze_toclear); + for (i = j = 1; i < out_learnt.size(); i++) + if (reason[var(out_learnt[i])] == NULL || !litRedundant(out_learnt[i], abstract_level)) + out_learnt[j++] = out_learnt[i]; + }else{ + out_learnt.copyTo(analyze_toclear); + for (i = j = 1; i < out_learnt.size(); i++){ + Clause& c = *reason[var(out_learnt[i])]; + for (int k = 1; k < c.size(); k++) + if (!seen[var(c[k])] && level[var(c[k])] > 0){ + out_learnt[j++] = out_learnt[i]; + break; } + } + } + max_literals += out_learnt.size(); + out_learnt.shrink(i - j); + tot_literals += out_learnt.size(); + + // Find correct backtrack level: + // + if (out_learnt.size() == 1) + out_btlevel = 0; + else{ + int max_i = 1; + for (int i = 2; i < out_learnt.size(); i++) + if (level[var(out_learnt[i])] > level[var(out_learnt[max_i])]) + max_i = i; + Lit p = out_learnt[max_i]; + out_learnt[max_i] = out_learnt[1]; + out_learnt[1] = p; + out_btlevel = level[var(p)]; + } + + + for (int j = 0; j < analyze_toclear.size(); j++) seen[var(analyze_toclear[j])] = 0; // ('seen[]' is now cleared) +} + + +// Check if 'p' can be removed. 'abstract_levels' is used to abort early if the algorithm is +// visiting literals at levels that cannot be removed later. +bool Solver::litRedundant(Lit p, uint32_t abstract_levels) +{ + analyze_stack.clear(); analyze_stack.push(p); + int top = analyze_toclear.size(); + while (analyze_stack.size() > 0){ + assert(reason[var(analyze_stack.last())] != NULL); + Clause& c = *reason[var(analyze_stack.last())]; analyze_stack.pop(); + + for (int i = 1; i < c.size(); i++){ + Lit p = c[i]; + if (!seen[var(p)] && level[var(p)] > 0){ + if (reason[var(p)] != NULL && (abstractLevel(var(p)) & abstract_levels) != 0){ + seen[var(p)] = 1; + analyze_stack.push(p); + analyze_toclear.push(p); + }else{ + for (int j = top; j < analyze_toclear.size(); j++) + seen[var(analyze_toclear[j])] = 0; + analyze_toclear.shrink(analyze_toclear.size() - top); + return false; + } + } + } + } + + return true; +} + + +/*_________________________________________________________________________________________________ +| +| analyzeFinal : (p : Lit) -> [void] +| +| Description: +| Specialized analysis procedure to express the final conflict in terms of assumptions. +| Calculates the (possibly empty) set of assumptions that led to the assignment of 'p', and +| stores the result in 'out_conflict'. +|________________________________________________________________________________________________@*/ +void Solver::analyzeFinal(Lit p, vec<Lit>& out_conflict) +{ + out_conflict.clear(); + out_conflict.push(p); + + if (decisionLevel() == 0) + return; + + seen[var(p)] = 1; + + for (int i = trail.size()-1; i >= trail_lim[0]; i--){ + Var x = var(trail[i]); + if (seen[x]){ + if (reason[x] == NULL){ + assert(level[x] > 0); + out_conflict.push(~trail[i]); + }else{ + Clause& c = *reason[x]; + for (int j = 1; j < c.size(); j++) + if (level[var(c[j])] > 0) + seen[var(c[j])] = 1; + } + seen[x] = 0; + } + } + + seen[var(p)] = 0; +} + + +void Solver::uncheckedEnqueue(Lit p, Clause* from) +{ + assert(value(p) == l_Undef); + assigns [var(p)] = toInt(lbool(!sign(p))); // <<== abstract but not uttermost effecient + level [var(p)] = decisionLevel(); + reason [var(p)] = from; + trail.push(p); +} + + +/*_________________________________________________________________________________________________ +| +| propagate : [void] -> [Clause*] +| +| Description: +| Propagates all enqueued facts. If a conflict arises, the conflicting clause is returned, +| otherwise NULL. +| +| Post-conditions: +| * the propagation queue is empty, even if there was a conflict. +|________________________________________________________________________________________________@*/ +Clause* Solver::propagate() +{ + Clause* confl = NULL; + int num_props = 0; + + while (qhead < trail.size()){ + Lit p = trail[qhead++]; // 'p' is enqueued fact to propagate. + vec<Clause*>& ws = watches[toInt(p)]; + Clause **i, **j, **end; + num_props++; + + for (i = j = (Clause**)ws, end = i + ws.size(); i != end;){ + Clause& c = **i++; + + // Make sure the false literal is data[1]: + Lit false_lit = ~p; + if (c[0] == false_lit) + c[0] = c[1], c[1] = false_lit; + + assert(c[1] == false_lit); + + // If 0th watch is true, then clause is already satisfied. + Lit first = c[0]; + if (value(first) == l_True){ + *j++ = &c; + }else{ + // Look for new watch: + for (int k = 2; k < c.size(); k++) + if (value(c[k]) != l_False){ + c[1] = c[k]; c[k] = false_lit; + watches[toInt(~c[1])].push(&c); + goto FoundWatch; } + + // Did not find watch -- clause is unit under assignment: + *j++ = &c; + if (value(first) == l_False){ + confl = &c; + qhead = trail.size(); + // Copy the remaining watches: + while (i < end) + *j++ = *i++; + }else + uncheckedEnqueue(first, &c); + } + FoundWatch:; + } + ws.shrink(i - j); + } + propagations += num_props; + simpDB_props -= num_props; + + return confl; +} + +/*_________________________________________________________________________________________________ +| +| reduceDB : () -> [void] +| +| Description: +| Remove half of the learnt clauses, minus the clauses locked by the current assignment. Locked +| clauses are clauses that are reason to some assignment. Binary clauses are never removed. +|________________________________________________________________________________________________@*/ +struct reduceDB_lt { bool operator () (Clause* x, Clause* y) { return x->size() > 2 && (y->size() == 2 || x->activity() < y->activity()); } }; +void Solver::reduceDB() +{ + int i, j; + double extra_lim = cla_inc / learnts.size(); // Remove any clause below this activity + + sort(learnts, reduceDB_lt()); + for (i = j = 0; i < learnts.size() / 2; i++){ + if (learnts[i]->size() > 2 && !locked(*learnts[i])) + removeClause(*learnts[i]); + else + learnts[j++] = learnts[i]; + } + for (; i < learnts.size(); i++){ + if (learnts[i]->size() > 2 && !locked(*learnts[i]) && learnts[i]->activity() < extra_lim) + removeClause(*learnts[i]); + else + learnts[j++] = learnts[i]; + } + learnts.shrink(i - j); +} + + +void Solver::removeSatisfied(vec<Clause*>& cs) +{ + int i,j; + for (i = j = 0; i < cs.size(); i++){ + if (satisfied(*cs[i])) + removeClause(*cs[i]); + else + cs[j++] = cs[i]; + } + cs.shrink(i - j); +} + + +/*_________________________________________________________________________________________________ +| +| simplify : [void] -> [bool] +| +| Description: +| Simplify the clause database according to the current top-level assigment. Currently, the only +| thing done here is the removal of satisfied clauses, but more things can be put here. +|________________________________________________________________________________________________@*/ +bool Solver::simplify() +{ + assert(decisionLevel() == 0); + + if (!ok || propagate() != NULL) + return ok = false; + + if (nAssigns() == simpDB_assigns || (simpDB_props > 0)) + return true; + + // Remove satisfied clauses: + removeSatisfied(learnts); + if (remove_satisfied) // Can be turned off. + removeSatisfied(clauses); + + // Remove fixed variables from the variable heap: + order_heap.filter(VarFilter(*this)); + + simpDB_assigns = nAssigns(); + simpDB_props = clauses_literals + learnts_literals; // (shouldn't depend on stats really, but it will do for now) + + return true; +} + + +/*_________________________________________________________________________________________________ +| +| search : (nof_conflicts : int) (nof_learnts : int) (params : const SearchParams&) -> [lbool] +| +| Description: +| Search for a model the specified number of conflicts, keeping the number of learnt clauses +| below the provided limit. NOTE! Use negative value for 'nof_conflicts' or 'nof_learnts' to +| indicate infinity. +| +| Output: +| 'l_True' if a partial assigment that is consistent with respect to the clauseset is found. If +| all variables are decision variables, this means that the clause set is satisfiable. 'l_False' +| if the clause set is unsatisfiable. 'l_Undef' if the bound on number of conflicts is reached. +|________________________________________________________________________________________________@*/ +lbool Solver::search(int nof_conflicts, int nof_learnts) +{ + assert(ok); + int backtrack_level; + int conflictC = 0; + vec<Lit> learnt_clause; + + starts++; + + bool first = true; + (void)first; + + for (;;){ + Clause* confl = propagate(); + if (confl != NULL){ + // CONFLICT + conflicts++; conflictC++; + if (decisionLevel() == 0) return l_False; + + first = false; + + learnt_clause.clear(); + analyze(confl, learnt_clause, backtrack_level); + cancelUntil(backtrack_level); + assert(value(learnt_clause[0]) == l_Undef); + + if (learnt_clause.size() == 1){ + uncheckedEnqueue(learnt_clause[0]); + }else{ + Clause* c = Clause_new(learnt_clause, true); + learnts.push(c); + attachClause(*c); + claBumpActivity(*c); + uncheckedEnqueue(learnt_clause[0], c); + } + + varDecayActivity(); + claDecayActivity(); + + }else{ + // NO CONFLICT + + if (nof_conflicts >= 0 && conflictC >= nof_conflicts){ + // Reached bound on number of conflicts: + progress_estimate = progressEstimate(); + cancelUntil(0); + return l_Undef; } + + // Simplify the set of problem clauses: + if (decisionLevel() == 0 && !simplify()) + return l_False; + + if (nof_learnts >= 0 && learnts.size()-nAssigns() >= nof_learnts) + // Reduce the set of learnt clauses: + reduceDB(); + + Lit next = lit_Undef; + while (decisionLevel() < assumptions.size()){ + // Perform user provided assumption: + Lit p = assumptions[decisionLevel()]; + if (value(p) == l_True){ + // Dummy decision level: + newDecisionLevel(); + }else if (value(p) == l_False){ + analyzeFinal(~p, conflict); + return l_False; + }else{ + next = p; + break; + } + } + + if (next == lit_Undef){ + // New variable decision: + decisions++; + next = pickBranchLit(polarity_mode, random_var_freq); + + if (next == lit_Undef) + // Model found: + return l_True; + } + + // Increase decision level and enqueue 'next' + assert(value(next) == l_Undef); + newDecisionLevel(); + uncheckedEnqueue(next); + } + } +} + + +double Solver::progressEstimate() const +{ + double progress = 0; + double F = 1.0 / nVars(); + + for (int i = 0; i <= decisionLevel(); i++){ + int beg = i == 0 ? 0 : trail_lim[i - 1]; + int end = i == decisionLevel() ? trail.size() : trail_lim[i]; + progress += pow(F, i) * (end - beg); + } + + return progress / nVars(); +} + + +bool Solver::solve(const vec<Lit>& assumps,bool cleanup) +{ + model.clear(); + conflict.clear(); + + if (!ok) return false; + + assumps.copyTo(assumptions); + + double nof_conflicts = restart_first; + double nof_learnts = nClauses() * learntsize_factor; + lbool status = l_Undef; + + if (verbosity >= 1){ + reportf("============================[ Search Statistics ]==============================\n"); + reportf("| Conflicts | ORIGINAL | LEARNT | Progress |\n"); + reportf("| | Vars Clauses Literals | Limit Clauses Lit/Cl | |\n"); + reportf("===============================================================================\n"); + } + + // Search: + while (status == l_Undef){ + if (verbosity >= 1) + reportf("| %9d | %7d %8d %8d | %8d %8d %6.0f | %6.3f %% |\n", (int)conflicts, order_heap.size(), nClauses(), (int)clauses_literals, (int)nof_learnts, nLearnts(), (double)learnts_literals/nLearnts(), progress_estimate*100), fflush(stdout); + status = search((int)nof_conflicts, (int)nof_learnts); + nof_conflicts *= restart_inc; + nof_learnts *= learntsize_inc; + } + + if (verbosity >= 1) + reportf("===============================================================================\n"); + + + if (status == l_True){ + // Extend & copy model: + model.growTo(nVars()); + for (int i = 0; i < nVars(); i++) model[i] = value(i); +#ifndef NDEBUG + verifyModel(); +#endif + }else{ + assert(status == l_False); + if (conflict.size() == 0) + ok = false; + } + + if(cleanup) cancelUntil(0); + return status == l_True; +} + +void Solver::clearTrail(){ + cancelUntil(0); +} + +//================================================================================================= +// Debug methods: + + +void Solver::verifyModel() +{ + bool failed = false; + for (int i = 0; i < clauses.size(); i++){ + assert(clauses[i]->mark() == 0); + Clause& c = *clauses[i]; + for (int j = 0; j < c.size(); j++) + if (modelValue(c[j]) == l_True) + goto next; + + reportf("unsatisfied clause: "); + printClause(*clauses[i]); + reportf("\n"); + failed = true; + next:; + } + + assert(!failed); + + ///reportf("Verified %d original clauses.\n", clauses.size()); +} + + +void Solver::checkLiteralCount() +{ + // Check that sizes are calculated correctly: + int cnt = 0; + for (int i = 0; i < clauses.size(); i++) + if (clauses[i]->mark() == 0) + cnt += clauses[i]->size(); + + if ((int)clauses_literals != cnt){ + fprintf(stderr, "literal count: %d, real value = %d\n", (int)clauses_literals, cnt); + assert((int)clauses_literals == cnt); + } +} diff --git a/minisat/solver/Solver.H b/minisat/solver/Solver.H new file mode 100644 index 0000000..80c8337 --- /dev/null +++ b/minisat/solver/Solver.H @@ -0,0 +1,309 @@ +/****************************************************************************************[Solver.h] +MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson + +Permission is hereby granted, free of charge, to any person obtaining a copy of this software and +associated documentation files (the "Software"), to deal in the Software without restriction, +including without limitation the rights to use, copy, modify, merge, publish, distribute, +sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all copies or +substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT +NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, +DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT +OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +**************************************************************************************************/ + +#ifndef Solver_h +#define Solver_h + +#include <cstdio> + +#include "Vec.h" +#include "Heap.h" +#include "Alg.h" + +#include "SolverTypes.H" + + +//================================================================================================= +// Solver -- the main class: + + +class Solver { +public: + + // Constructor/Destructor: + // + Solver(); + ~Solver(); + + // Problem specification: + // + Var newVar (bool polarity = true, bool dvar = true); // Add a new variable with parameters specifying variable mode. + bool addClause (vec<Lit>& ps); // Add a clause to the solver. NOTE! 'ps' may be shrunk by this method! + + // Solving: + // + bool simplify (); // Removes already satisfied clauses. + bool solve (const vec<Lit>& assumps,bool cleanup=true); // Search for a model that respects a given set of assumptions. + bool solve (); // Search without assumptions. + bool okay () const; // FALSE means solver is in a conflicting state + + void clearTrail(); + + // Variable mode: + // + void setPolarity (Var v, bool b); // Declare which polarity the decision heuristic should use for a variable. Requires mode 'polarity_user'. + void setDecisionVar (Var v, bool b); // Declare if a variable should be eligible for selection in the decision heuristic. + + // Read state: + // + lbool value (Var x) const; // The current value of a variable. + lbool value (Lit p) const; // The current value of a literal. + lbool modelValue (Lit p) const; // The value of a literal in the last model. The last call to solve must have been satisfiable. + int nAssigns () const; // The current number of assigned literals. + int nClauses () const; // The current number of original clauses. + int nLearnts () const; // The current number of learnt clauses. + int nVars () const; // The current number of variables. + + // Extra results: (read-only member variable) + // + vec<lbool> model; // If problem is satisfiable, this vector contains the model (if any). + vec<Lit> conflict; // If problem is unsatisfiable (possibly under assumptions), + // this vector represent the final conflict clause expressed in the assumptions. + + //ADDED METHODS + int getTrailSize() const{return trail.size();} + int getTrailVar(int index) const{return var(trail[index]);} + bool getTrailSign(int index) const{return sign(trail[index]);} + + // Mode of operation: + // + double var_decay; // Inverse of the variable activity decay factor. (default 1 / 0.95) + double clause_decay; // Inverse of the clause activity decay factor. (1 / 0.999) + double random_var_freq; // The frequency with which the decision heuristic tries to choose a random variable. (default 0.02) + int restart_first; // The initial restart limit. (default 100) + double restart_inc; // The factor with which the restart limit is multiplied in each restart. (default 1.5) + double learntsize_factor; // The intitial limit for learnt clauses is a factor of the original clauses. (default 1 / 3) + double learntsize_inc; // The limit for learnt clauses is multiplied with this factor each restart. (default 1.1) + bool expensive_ccmin; // Controls conflict clause minimization. (default TRUE) + int polarity_mode; // Controls which polarity the decision heuristic chooses. See enum below for allowed modes. (default polarity_false) + int verbosity; // Verbosity level. 0=silent, 1=some progress report (default 0) + + enum { polarity_true = 0, polarity_false = 1, polarity_user = 2, polarity_rnd = 3 }; + + // Statistics: (read-only member variable) + // + uint64_t starts, decisions, rnd_decisions, propagations, conflicts; + uint64_t clauses_literals, learnts_literals, max_literals, tot_literals; + +protected: + + // Helper structures: + // + struct VarOrderLt { + const vec<double>& activity; + bool operator () (Var x, Var y) const { return activity[x] > activity[y]; } + VarOrderLt(const vec<double>& act) : activity(act) { } + }; + + friend class VarFilter; + struct VarFilter { + const Solver& s; + VarFilter(const Solver& _s) : s(_s) {} + bool operator()(Var v) const { return toLbool(s.assigns[v]) == l_Undef && s.decision_var[v]; } + }; + + // Solver state: + // + bool ok; // If FALSE, the constraints are already unsatisfiable. No part of the solver state may be used! + vec<Clause*> clauses; // List of problem clauses. + vec<Clause*> learnts; // List of learnt clauses. + double cla_inc; // Amount to bump next clause with. + vec<double> activity; // A heuristic measurement of the activity of a variable. + double var_inc; // Amount to bump next variable with. + vec<vec<Clause*> > watches; // 'watches[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true). + vec<char> assigns; // The current assignments (lbool:s stored as char:s). + vec<char> polarity; // The preferred polarity of each variable. + vec<char> decision_var; // Declares if a variable is eligible for selection in the decision heuristic. + vec<Lit> trail; // Assignment stack; stores all assigments made in the order they were made. + vec<int> trail_lim; // Separator indices for different decision levels in 'trail'. + vec<Clause*> reason; // 'reason[var]' is the clause that implied the variables current value, or 'NULL' if none. + vec<int> level; // 'level[var]' contains the level at which the assignment was made. + int qhead; // Head of queue (as index into the trail -- no more explicit propagation queue in MiniSat). + int simpDB_assigns; // Number of top-level assignments since last execution of 'simplify()'. + int64_t simpDB_props; // Remaining number of propagations that must be made before next execution of 'simplify()'. + vec<Lit> assumptions; // Current set of assumptions provided to solve by the user. + Heap<VarOrderLt> order_heap; // A priority queue of variables ordered with respect to the variable activity. + double random_seed; // Used by the random variable selection. + double progress_estimate;// Set by 'search()'. + bool remove_satisfied; // Indicates whether possibly inefficient linear scan for satisfied clauses should be performed in 'simplify'. + + // Temporaries (to reduce allocation overhead). Each variable is prefixed by the method in which it is + // used, exept 'seen' wich is used in several places. + // + vec<char> seen; + vec<Lit> analyze_stack; + vec<Lit> analyze_toclear; + vec<Lit> add_tmp; + + // Main internal methods: + // + void insertVarOrder (Var x); // Insert a variable in the decision order priority queue. + Lit pickBranchLit (int polarity_mode, double random_var_freq); // Return the next decision variable. + void newDecisionLevel (); // Begins a new decision level. + void uncheckedEnqueue (Lit p, Clause* from = NULL); // Enqueue a literal. Assumes value of literal is undefined. + bool enqueue (Lit p, Clause* from = NULL); // Test if fact 'p' contradicts current state, enqueue otherwise. + Clause* propagate (); // Perform unit propagation. Returns possibly conflicting clause. + void cancelUntil (int level); // Backtrack until a certain level. + void analyze (Clause* confl, vec<Lit>& out_learnt, int& out_btlevel); // (bt = backtrack) + void analyzeFinal (Lit p, vec<Lit>& out_conflict); // COULD THIS BE IMPLEMENTED BY THE ORDINARIY "analyze" BY SOME REASONABLE GENERALIZATION? + bool litRedundant (Lit p, uint32_t abstract_levels); // (helper method for 'analyze()') + lbool search (int nof_conflicts, int nof_learnts); // Search for a given number of conflicts. + void reduceDB (); // Reduce the set of learnt clauses. + void removeSatisfied (vec<Clause*>& cs); // Shrink 'cs' to contain only non-satisfied clauses. + + // Maintaining Variable/Clause activity: + // + void varDecayActivity (); // Decay all variables with the specified factor. Implemented by increasing the 'bump' value instead. + void varBumpActivity (Var v); // Increase a variable with the current 'bump' value. + void claDecayActivity (); // Decay all clauses with the specified factor. Implemented by increasing the 'bump' value instead. + void claBumpActivity (Clause& c); // Increase a clause with the current 'bump' value. + + // Operations on clauses: + // + void attachClause (Clause& c); // Attach a clause to watcher lists. + void detachClause (Clause& c); // Detach a clause to watcher lists. + void removeClause (Clause& c); // Detach and free a clause. + bool locked (const Clause& c) const; // Returns TRUE if a clause is a reason for some implication in the current state. + bool satisfied (const Clause& c) const; // Returns TRUE if a clause is satisfied in the current state. + + // Misc: + // + int decisionLevel () const; // Gives the current decisionlevel. + uint32_t abstractLevel (Var x) const; // Used to represent an abstraction of sets of decision levels. + double progressEstimate () const; // DELETE THIS ?? IT'S NOT VERY USEFUL ... + + // Debug: + void printLit (Lit l); + template<class C> + void printClause (const C& c); + void verifyModel (); + void checkLiteralCount(); + + // Static helpers: + // + + // Returns a random float 0 <= x < 1. Seed must never be 0. + static inline double drand(double& seed) { + seed *= 1389796; + int q = (int)(seed / 2147483647); + seed -= (double)q * 2147483647; + return seed / 2147483647; } + + // Returns a random integer 0 <= x < size. Seed must never be 0. + static inline int irand(double& seed, int size) { + return (int)(drand(seed) * size); } +}; + + +//================================================================================================= +// Implementation of inline methods: + + +inline void Solver::insertVarOrder(Var x) { + if (!order_heap.inHeap(x) && decision_var[x]) order_heap.insert(x); } + +inline void Solver::varDecayActivity() { var_inc *= var_decay; } +inline void Solver::varBumpActivity(Var v) { + if ( (activity[v] += var_inc) > 1e100 ) { + // Rescale: + for (int i = 0; i < nVars(); i++) + activity[i] *= 1e-100; + var_inc *= 1e-100; } + + // Update order_heap with respect to new activity: + if (order_heap.inHeap(v)) + order_heap.decrease(v); } + +inline void Solver::claDecayActivity() { cla_inc *= clause_decay; } +inline void Solver::claBumpActivity (Clause& c) { + if ( (c.activity() += cla_inc) > 1e20 ) { + // Rescale: + for (int i = 0; i < learnts.size(); i++) + learnts[i]->activity() *= 1e-20; + cla_inc *= 1e-20; } } + +inline bool Solver::enqueue (Lit p, Clause* from) { return value(p) != l_Undef ? value(p) != l_False : (uncheckedEnqueue(p, from), true); } +inline bool Solver::locked (const Clause& c) const { return reason[var(c[0])] == &c && value(c[0]) == l_True; } +inline void Solver::newDecisionLevel() { trail_lim.push(trail.size()); } + +inline int Solver::decisionLevel () const { return trail_lim.size(); } +inline uint32_t Solver::abstractLevel (Var x) const { return 1 << (level[x] & 31); } +inline lbool Solver::value (Var x) const { return toLbool(assigns[x]); } +inline lbool Solver::value (Lit p) const { return toLbool(assigns[var(p)]) ^ sign(p); } +inline lbool Solver::modelValue (Lit p) const { return model[var(p)] ^ sign(p); } +inline int Solver::nAssigns () const { return trail.size(); } +inline int Solver::nClauses () const { return clauses.size(); } +inline int Solver::nLearnts () const { return learnts.size(); } +inline int Solver::nVars () const { return assigns.size(); } +inline void Solver::setPolarity (Var v, bool b) { polarity [v] = (char)b; } +inline void Solver::setDecisionVar(Var v, bool b) { decision_var[v] = (char)b; if (b) { insertVarOrder(v); } } +inline bool Solver::solve () { vec<Lit> tmp; return solve(tmp); } +inline bool Solver::okay () const { return ok; } + + + +//================================================================================================= +// Debug + etc: + + +#define reportf(format, args...) ( fflush(stdout), fprintf(stderr, format, ## args), fflush(stderr) ) + +static inline void logLit(FILE* f, Lit l) +{ + fprintf(f, "%sx%d", sign(l) ? "~" : "", var(l)+1); +} + +static inline void logLits(FILE* f, const vec<Lit>& ls) +{ + fprintf(f, "[ "); + if (ls.size() > 0){ + logLit(f, ls[0]); + for (int i = 1; i < ls.size(); i++){ + fprintf(f, ", "); + logLit(f, ls[i]); + } + } + fprintf(f, "] "); +} + +static inline const char* showBool(bool b) { return b ? "true" : "false"; } + + +// Just like 'assert()' but expression will be evaluated in the release version as well. +static inline void check(bool expr) { assert(expr); } + + +inline void Solver::printLit(Lit l) +{ + reportf("%s%d:%c", sign(l) ? "-" : "", var(l)+1, value(l) == l_True ? '1' : (value(l) == l_False ? '0' : 'X')); +} + + +template<class C> +inline void Solver::printClause(const C& c) +{ + for (int i = 0; i < c.size(); i++){ + printLit(c[i]); + fprintf(stderr, " "); + } +} + + +//================================================================================================= +#endif diff --git a/minisat/solver/SolverTypes.H b/minisat/solver/SolverTypes.H new file mode 100644 index 0000000..f590f8e --- /dev/null +++ b/minisat/solver/SolverTypes.H @@ -0,0 +1,201 @@ +/***********************************************************************************[SolverTypes.h] +MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson + +Permission is hereby granted, free of charge, to any person obtaining a copy of this software and +associated documentation files (the "Software"), to deal in the Software without restriction, +including without limitation the rights to use, copy, modify, merge, publish, distribute, +sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all copies or +substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT +NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, +DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT +OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +**************************************************************************************************/ + + +#ifndef SolverTypes_h +#define SolverTypes_h + +#include <cassert> +#include <stdint.h> + +//================================================================================================= +// Variables, literals, lifted booleans, clauses: + + +// NOTE! Variables are just integers. No abstraction here. They should be chosen from 0..N, +// so that they can be used as array indices. + +typedef int Var; +#define var_Undef (-1) + + +class Lit { + int x; + public: + Lit() : x(2*var_Undef) { } // (lit_Undef) + explicit Lit(Var var, bool sign = false) : x((var+var) + (int)sign) { } + + // Don't use these for constructing/deconstructing literals. Use the normal constructors instead. + friend int toInt (Lit p); // Guarantees small, positive integers suitable for array indexing. + friend Lit toLit (int i); // Inverse of 'toInt()' + friend Lit operator ~(Lit p); + friend bool sign (Lit p); + friend int var (Lit p); + friend Lit unsign (Lit p); + friend Lit id (Lit p, bool sgn); + + bool operator == (Lit p) const { return x == p.x; } + bool operator != (Lit p) const { return x != p.x; } + bool operator < (Lit p) const { return x < p.x; } // '<' guarantees that p, ~p are adjacent in the ordering. +}; + +inline int toInt (Lit p) { return p.x; } +inline Lit toLit (int i) { Lit p; p.x = i; return p; } +inline Lit operator ~(Lit p) { Lit q; q.x = p.x ^ 1; return q; } +inline bool sign (Lit p) { return p.x & 1; } +inline int var (Lit p) { return p.x >> 1; } +inline Lit unsign (Lit p) { Lit q; q.x = p.x & ~1; return q; } +inline Lit id (Lit p, bool sgn) { Lit q; q.x = p.x ^ (int)sgn; return q; } + +const Lit lit_Undef(var_Undef, false); // }- Useful special constants. +const Lit lit_Error(var_Undef, true ); // } + + +//================================================================================================= +// Lifted booleans: + + +class lbool { + char value; + explicit lbool(int v) : value(v) { } + +public: + lbool() : value(0) { } + lbool(bool x) : value((int)x*2-1) { } + int toInt(void) const { return value; } + + bool operator == (lbool b) const { return value == b.value; } + bool operator != (lbool b) const { return value != b.value; } + lbool operator ^ (bool b) const { return b ? lbool(-value) : lbool(value); } + + friend int toInt (lbool l); + friend lbool toLbool(int v); +}; +inline int toInt (lbool l) { return l.toInt(); } +inline lbool toLbool(int v) { return lbool(v); } + +const lbool l_True = toLbool( 1); +const lbool l_False = toLbool(-1); +const lbool l_Undef = toLbool( 0); + +//================================================================================================= +// Clause -- a simple class for representing a clause: + +class Clause; + +template<class V> +Clause* Clause_new(const V& ps, bool learnt = false); + +class Clause { + uint32_t size_etc; + union { float act; uint32_t abst; } extra; + Lit data[0]; + +public: + void calcAbstraction() { + uint32_t abstraction = 0; + for (int i = 0; i < size(); i++) + abstraction |= 1 << (var(data[i]) & 31); + extra.abst = abstraction; } + + // NOTE: This constructor cannot be used directly (doesn't allocate enough memory). + template<class V> + Clause(const V& ps, bool learnt) { + size_etc = (ps.size() << 3) | (uint32_t)learnt; + for (int i = 0; i < ps.size(); i++) data[i] = ps[i]; + if (learnt) extra.act = 0; else calcAbstraction(); } + + // -- use this function instead: + template<class V> + friend Clause* Clause_new(const V& ps, bool learnt) { + assert(sizeof(Lit) == sizeof(uint32_t)); + assert(sizeof(float) == sizeof(uint32_t)); + void* mem = malloc(sizeof(Clause) + sizeof(uint32_t)*(ps.size())); + return new (mem) Clause(ps, learnt); } + + int size () const { return size_etc >> 3; } + void shrink (int i) { assert(i <= size()); size_etc = (((size_etc >> 3) - i) << 3) | (size_etc & 7); } + void pop () { shrink(1); } + bool learnt () const { return size_etc & 1; } + uint32_t mark () const { return (size_etc >> 1) & 3; } + void mark (uint32_t m) { size_etc = (size_etc & ~6) | ((m & 3) << 1); } + const Lit& last () const { return data[size()-1]; } + + // NOTE: somewhat unsafe to change the clause in-place! Must manually call 'calcAbstraction' afterwards for + // subsumption operations to behave correctly. + Lit& operator [] (int i) { return data[i]; } + Lit operator [] (int i) const { return data[i]; } + operator const Lit* (void) const { return data; } + + float& activity () { return extra.act; } + uint32_t abstraction () const { return extra.abst; } + + Lit subsumes (const Clause& other) const; + void strengthen (Lit p); +}; + + +/*_________________________________________________________________________________________________ +| +| subsumes : (other : const Clause&) -> Lit +| +| Description: +| Checks if clause subsumes 'other', and at the same time, if it can be used to simplify 'other' +| by subsumption resolution. +| +| Result: +| lit_Error - No subsumption or simplification +| lit_Undef - Clause subsumes 'other' +| p - The literal p can be deleted from 'other' +|________________________________________________________________________________________________@*/ +inline Lit Clause::subsumes(const Clause& other) const +{ + if (other.size() < size() || (extra.abst & ~other.extra.abst) != 0) + return lit_Error; + + Lit ret = lit_Undef; + const Lit* c = (const Lit*)(*this); + const Lit* d = (const Lit*)other; + + for (int i = 0; i < size(); i++) { + // search for c[i] or ~c[i] + for (int j = 0; j < other.size(); j++) + if (c[i] == d[j]) + goto ok; + else if (ret == lit_Undef && c[i] == ~d[j]){ + ret = c[i]; + goto ok; + } + + // did not find it + return lit_Error; + ok:; + } + + return ret; +} + + +inline void Clause::strengthen(Lit p) +{ + remove(*this, p); + calcAbstraction(); +} + +#endif |