mios (empty) → 1.2.1
raw patch · 24 files changed
+4495/−0 lines, 24 filesdep +basedep +bytestringdep +containerssetup-changed
Dependencies added: base, bytestring, containers, ghc-prim, primitive, vector
Files
- LICENSE +675/−0
- SAT/Solver/Mios.hs +298/−0
- SAT/Solver/Mios/Clause.hs +144/−0
- SAT/Solver/Mios/ClauseManager.hs +324/−0
- SAT/Solver/Mios/Data/Singleton.hs +196/−0
- SAT/Solver/Mios/Data/Stack.hs +93/−0
- SAT/Solver/Mios/Data/Vec.hs +86/−0
- SAT/Solver/Mios/Data/VecBool.hs +55/−0
- SAT/Solver/Mios/Data/VecDouble.hs +53/−0
- SAT/Solver/Mios/Glucose.hs +72/−0
- SAT/Solver/Mios/Internal.hs +34/−0
- SAT/Solver/Mios/M114.hs +816/−0
- SAT/Solver/Mios/OptionParser.hs +132/−0
- SAT/Solver/Mios/Solver.hs +554/−0
- SAT/Solver/Mios/Types.hs +269/−0
- SAT/Solver/Mios/Validator.hs +47/−0
- SAT/Util/BoolExp.hs +244/−0
- SAT/Util/CNFIO.hs +31/−0
- SAT/Util/CNFIO/MinisatReader.hs +73/−0
- SAT/Util/CNFIO/Reader.hs +130/−0
- SAT/Util/CNFIO/Writer.hs +58/−0
- Setup.hs +2/−0
- app/mios.hs +20/−0
- mios.cabal +89/−0
+ LICENSE view
@@ -0,0 +1,675 @@+ 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>.+
+ SAT/Solver/Mios.hs view
@@ -0,0 +1,298 @@+-- | Minisat-based Implementation and Optimization Study on SAT solver+{-# LANGUAGE ViewPatterns #-}+{-# LANGUAGE Trustworthy #-}++module SAT.Solver.Mios+ (+ -- * Interface to the core of solver+ versionId+ , CNFDescription (..)+ , module SAT.Solver.Mios.OptionParser+ , runSolver+ , solveSAT+ , solveSATWithConfiguration+ , solve+ , getModel+ -- * Assignment Validator+ , validateAssignment+ , validate+ -- * For standalone programs+ , executeSolverOn+ , executeSolver+ , executeValidatorOn+ , executeValidator+ -- * File IO+ , dumpAssigmentAsCNF+ )+ where++import Control.Monad ((<=<), unless, void, when)+import Data.Char+import qualified Data.ByteString.Char8 as B+import Data.List+import qualified Data.Vector.Unboxed as U+import Numeric (showFFloat)+import System.CPUTime+import System.Exit+import System.IO++import SAT.Solver.Mios.Types+import SAT.Solver.Mios.Internal+import SAT.Solver.Mios.Solver+import SAT.Solver.Mios.M114+import SAT.Solver.Mios.OptionParser+import SAT.Solver.Mios.Validator++reportElapsedTime :: Bool -> String -> Integer -> IO Integer+reportElapsedTime False _ _ = return 0+reportElapsedTime _ _ 0 = getCPUTime+reportElapsedTime _ mes t = do+ now <- getCPUTime+ let toSecond = 1000000000000 :: Double+ hPutStr stderr mes+ hPutStrLn stderr $ showFFloat (Just 3) ((fromIntegral (now - t)) / toSecond) " sec"+ return now++-- | executes a solver on the given CNF file+-- This is the simplest entry to standalone programs; not for Haskell programs+executeSolverOn :: FilePath -> IO ()+executeSolverOn path = executeSolver (miosDefaultOption { _targetFile = Just path })++-- | executes a solver on the given 'arg :: MiosConfiguration'+-- | This is another entry point for standalone programs.+executeSolver :: MiosProgramOption -> IO ()+executeSolver opts@(_targetFile -> target@(Just cnfFile)) = do+ t0 <- reportElapsedTime (_confTimeProbe opts) "" 0+ (desc, cls) <- parseHeader target <$> B.readFile cnfFile+ when (_numberOfVariables desc == 0) $ error $ "couldn't load " ++ show cnfFile+ s <- newSolver (toMiosConf opts) desc+ parseClauses s desc cls+ t1 <- reportElapsedTime (_confTimeProbe opts) ("## [" ++ showPath cnfFile ++ "] Parse: ") t0+ when (_confVerbose opts) $ do+ nc <- nClauses s+ hPutStrLn stderr $ cnfFile ++ " was loaded: #v = " ++ show (nVars s, _numberOfVariables desc) ++ " #c = " ++ show (nc, _numberOfClauses desc)+ res <- simplifyDB s+ -- when (_confVerbose opts) $ hPutStrLn stderr $ "`simplifyDB`: " ++ show res+ result <- solve s []+ case result of+ True | _confNoAnswer opts -> when (_confVerbose opts) $ hPutStrLn stderr "SATISFIABLE"+ False | _confNoAnswer opts -> when (_confVerbose opts) $ hPutStrLn stderr "UNSATISFIABLE"+ True -> print =<< getModel s+ False -> do -- contradiction+ -- FIXMEin future+ when (_confVerbose opts) $ hPutStrLn stderr "UNSAT"+ -- print =<< map lit2int <$> asList (conflict s)+ putStrLn "[]"+ case _outputFile opts of+ Just fname -> dumpAssigmentAsCNF fname result =<< getModel s+ Nothing -> return ()+ t2 <- reportElapsedTime (_confTimeProbe opts) ("## [" ++ showPath cnfFile ++ "] Solve: ") t1+ when (result && _confCheckAnswer opts) $ do+ asg <- getModel s+ s' <- newSolver (toMiosConf opts) desc+ parseClauses s' desc cls+ good <- validate s' asg+ if _confVerbose opts+ then hPutStrLn stderr $ if good then "A vaild answer" else "Internal error: mios returns a wrong answer"+ else unless good $ hPutStrLn stderr "Internal error: mios returns a wrong answer"+ void $ reportElapsedTime (_confTimeProbe opts) ("## [" ++ showPath cnfFile ++ "] Validate: ") t2+ void $ reportElapsedTime (_confTimeProbe opts) ("## [" ++ showPath cnfFile ++ "] Total: ") t0+ when (_confStatProbe opts) $ do+ hPutStr stderr $ "## [" ++ showPath cnfFile ++ "] "+ hPutStrLn stderr . intercalate ", " . map (\(k, v) -> show k ++ ": " ++ show v) =<< getStats s++executeSolver _ = return ()++-- | new top-level interface that returns+--+-- * conflicting literal set :: Left [Int]+-- * satisfiable assignment :: Right [Int]+--+runSolver :: Traversable t => MiosConfiguration -> CNFDescription -> t [Int] -> IO (Either [Int] [Int])+runSolver m d c = do+ s <- newSolver m d+ mapM_ ((s `addClause`) <=< (newSizedVecIntFromList . map int2lit)) c+ noConf <- simplifyDB s+ if noConf+ then do+ x <- solve s []+ if x+ then Right <$> getModel s+ else Left . map lit2int <$> asList (conflict s)+ else return $ Left []+++-- | the easiest interface for Haskell programs+-- This returns the result @::[[Int]]@ for a given @(CNFDescription, [[Int]])@+-- The first argument @target@ can be build by @Just target <- cnfFromFile targetfile@.+-- The second part of the first argument is a list of vector, which 0th element is the number of its real elements+solveSAT :: Traversable m => CNFDescription -> m [Int] -> IO [Int]+solveSAT = solveSATWithConfiguration defaultConfiguration++-- | solves the problem (2rd arg) under the configuration (1st arg)+-- and returns an assignment as list of literals :: Int+solveSATWithConfiguration :: Traversable m => MiosConfiguration -> CNFDescription -> m [Int] -> IO [Int]+solveSATWithConfiguration conf desc cls = do+ s <- newSolver conf desc+ -- mapM_ (const (newVar s)) [0 .. _numberOfVariables desc - 1]+ mapM_ ((s `addClause`) <=< (newSizedVecIntFromList . map int2lit)) cls+ noConf <- simplifyDB s+ if noConf+ then do+ result <- solve s []+ if result+ then getModel s+ else return []+ else return []++-- | validates a given assignment from STDIN for the CNF file (2nd arg)+-- this is the entry point for standalone programs+executeValidatorOn :: FilePath -> IO ()+executeValidatorOn path = executeValidator (miosDefaultOption { _targetFile = Just path })++-- | validates a given assignment for the problem (2nd arg)+-- this is another entry point for standalone programs; see app/mios.hs+executeValidator :: MiosProgramOption -> IO ()+executeValidator opts@(_targetFile -> target@(Just cnfFile)) = do+ (desc, cls) <- parseHeader target <$> B.readFile cnfFile+ when (_numberOfVariables desc == 0) . error $ "couldn't load " ++ show cnfFile+ s <- newSolver (toMiosConf opts) desc+ parseClauses s desc cls+ when (_confVerbose opts) $+ hPutStrLn stderr $ cnfFile ++ " was loaded: #v = " ++ show (_numberOfVariables desc) ++ " #c = " ++ show (_numberOfClauses desc)+ when (_confVerbose opts) $ do+ nc <- nClauses s+ nl <- nLearnts s+ hPutStrLn stderr $ "(nv, nc, nl) = " ++ show (nVars s, nc, nl)+ asg <- read <$> getContents+ unless (_confNoAnswer opts) $ print asg+ result <- s `validate` (asg :: [Int])+ if result+ then putStrLn ("It's a valid assignment for " ++ cnfFile ++ ".") >> exitSuccess+ else putStrLn ("It's an invalid assignment for " ++ cnfFile ++ ".") >> exitFailure++executeValidator _ = return ()++-- | returns True if a given assignment (2nd arg) satisfies the problem (1st arg)+-- if you want to check the @answer@ which a @slover@ returned, run @solver `validate` answer@,+-- where 'validate' @ :: Traversable t => Solver -> t Lit -> IO Bool@+validateAssignment :: (Traversable m, Traversable n) => CNFDescription -> m [Int] -> n Int -> IO Bool+validateAssignment desc cls asg = do+ s <- newSolver defaultConfiguration desc+ mapM_ ((s `addClause`) <=< (newSizedVecIntFromList . map int2lit)) cls+ s `validate` asg++-- | dumps an assigment to file.+-- 2nd arg is+--+-- * @True@ if the assigment is satisfiable assigment+--+-- * @False@ if not+--+-- >>> do y <- solve s ... ; dumpAssigmentAsCNF "result.cnf" y <$> model s+--+dumpAssigmentAsCNF :: FilePath -> Bool -> [Int] -> IO ()+dumpAssigmentAsCNF fname False _ = do+ withFile fname WriteMode $ \h -> do+ hPutStrLn h "UNSAT"++dumpAssigmentAsCNF fname True l = do+ withFile fname WriteMode $ \h -> do+ hPutStrLn h "SAT"+ hPutStrLn h . unwords $ map show l++--------------------------------------------------------------------------------+-- DIMACS CNF Reader+--------------------------------------------------------------------------------++parseHeader :: Maybe FilePath -> B.ByteString -> (CNFDescription, B.ByteString)+parseHeader target bs = if B.head bs == 'p' then (parseP l, B.tail bs') else parseHeader target (B.tail bs')+ where+ (l, bs') = B.span ('\n' /=) bs+ -- format: p cnf n m, length "p cnf" == 5+ parseP line = case B.readInt $ B.dropWhile (`elem` " \t") (B.drop 5 line) of+ Just (x, second) -> case B.readInt (B.dropWhile (`elem` " \t") second) of+ Just (y, _) -> CNFDescription x y target+ _ -> CNFDescription 0 0 target+ _ -> CNFDescription 0 0 target++parseClauses :: Solver -> CNFDescription -> B.ByteString -> IO ()+parseClauses s (CNFDescription nv nc _) bs = do+ let maxLit = int2lit $ negate nv+ buffer <- newVec $ maxLit + 1+ polvec <- newVecBool (maxLit + 1) False+ let+ loop :: Int -> B.ByteString -> IO ()+ loop ((< nc) -> False) _ = return ()+ loop i b = loop (i + 1) =<< readClause s buffer polvec b+ loop 0 bs+ -- static polarity+ let+ asg = assigns s+ checkPolarity :: Int -> IO ()+ checkPolarity ((< nv) -> False) = return ()+ checkPolarity v = do+ p <- getNthBool polvec $ var2lit v True+ n <- getNthBool polvec $ var2lit v False+ when (p == False || n == False) $ setNth asg v $ if p then lTrue else lFalse+ checkPolarity $ v + 1+ checkPolarity 1++skipWhitespace :: B.ByteString -> B.ByteString+skipWhitespace s+ | elem c " \t\n" = skipWhitespace $ B.tail s+ | otherwise = s+ where+ c = B.head s++-- | skip comment lines+-- __Pre-condition:__ we are on the benngining of a line+skipComments :: B.ByteString -> B.ByteString+skipComments s+ | c == 'c' = skipComments . B.tail . B.dropWhile (/= '\n') $ s+ | otherwise = s+ where+ c = B.head s++parseInt :: B.ByteString -> (Int, B.ByteString)+parseInt st = do+ let+ zero = ord '0'+ loop :: B.ByteString -> Int -> (Int, B.ByteString)+ loop s val = case B.head s of+ c | '0' <= c && c <= '9' -> loop (B.tail s) (val * 10 + ord c - zero)+ _ -> (val, B.tail s)+ case B.head st of+ '-' -> let (k, x) = loop (B.tail st) 0 in (negate k, x)+ '+' -> loop st (0 :: Int)+ c | '0' <= c && c <= '9' -> loop st 0+ _ -> error "PARSE ERROR! Unexpected char"++readClause :: Solver -> Vec -> VecBool -> B.ByteString -> IO B.ByteString+readClause s buffer pvec stream = do+ let+ loop :: Int -> B.ByteString -> IO B.ByteString+ loop i b = do+ let (k, b') = parseInt $ skipWhitespace b+ if k == 0+ then do+ -- putStrLn . ("clause: " ++) . show . map lit2int =<< asList stack+ setNth buffer 0 $ i - 1+ addClause s buffer+ return b'+ else do+ let l = int2lit k+ setNth buffer i l+ setNthBool pvec l True+ loop (i + 1) b'+ loop 1 . skipComments . skipWhitespace $ stream+++showPath :: FilePath -> String+showPath str+ | elem '/' str = take (len - length basename) (repeat ' ') ++ basename+ | otherwise = take (len - length basename') (repeat ' ') ++ basename'+ where+ len = 50+ basename = reverse . takeWhile (/= '/') . reverse $ str+ basename' = take len str
+ SAT/Solver/Mios/Clause.hs view
@@ -0,0 +1,144 @@+-- | Clause, a data supporting pointer-based equality+{-# LANGUAGE+ BangPatterns+ , FlexibleInstances+ , MagicHash+ , MultiParamTypeClasses+ , RecordWildCards+ , ViewPatterns+ #-}+{-# LANGUAGE Trustworthy #-}++module SAT.Solver.Mios.Clause+ (+ Clause (..)+-- , isLit+-- , getLit+ , shrinkClause+ , newClauseFromVec+ , sizeOfClause+ -- * Vector of Clause+ , ClauseVector+ , newClauseVector+ , getNthClause+ , setNthClause+ , swapClauses+ )+ where++import Control.Monad (forM_)+import GHC.Prim (tagToEnum#, reallyUnsafePtrEquality#)+import qualified Data.Vector as V+import qualified Data.Vector.Mutable as MV+import qualified Data.Vector.Unboxed.Mutable as UV+import Data.List (intercalate)+import SAT.Solver.Mios.Types++-- | __Fig. 7.(p.11)__+-- clause, null, binary clause.+-- This matches both of @Clause@ and @GClause@ in MiniSat+-- TODO: GADTs is better?+data Clause = Clause+ {+ learnt :: !Bool -- ^ whether this is a learnt clause+ , activity :: !DoubleSingleton -- ^ activity of this clause+ , protected :: !BoolSingleton -- ^ protected from reduce+ , lbd :: !IntSingleton -- ^ storing the LBD; values are computed in Solver+ , lits :: !Vec -- ^ which this clause consists of+ }+-- | BinaryClause Lit -- binary clause consists of only a propagating literal+ | NullClause -- as null pointer++-- | The equality on 'Clause' is defined with 'reallyUnsafePtrEquality'.+instance Eq Clause where+ {-# SPECIALIZE INLINE (==) :: Clause -> Clause -> Bool #-}+ (==) x y = x `seq` y `seq` tagToEnum# (reallyUnsafePtrEquality# x y)++instance Show Clause where+ show NullClause = "NullClause"+ show _ = "a clause"++-- | supports a restricted set of 'VectorFamily' methods+instance VectorFamily Clause Lit where+ dump mes NullClause = return $ mes ++ "Null"+ dump mes Clause{..} = do+ a <- show <$> getDouble activity+ (len:ls) <- asList lits+ return $ mes ++ "C" ++ show len ++ "{" ++ intercalate "," [show learnt, a, show . map lit2int . take len $ ls] ++ "}"+ {-# SPECIALIZE INLINE asVec :: Clause -> Vec #-}+ asVec Clause{..} = UV.unsafeTail lits+ {-# SPECIALIZE INLINE asList :: Clause -> IO [Int] #-}+ asList NullClause = return []+ asList Clause{..} = do+ (n : ls) <- asList lits+ return $ take n ls++-- returns True if it is a 'BinaryClause'+-- FIXME: this might be discarded in minisat 2.2+-- isLit :: Clause -> Bool+-- isLit (BinaryClause _) = True+-- isLit _ = False++-- returns the literal in a BinaryClause+-- FIXME: this might be discarded in minisat 2.2+-- getLit :: Clause -> Lit+-- getLit (BinaryClause x) = x++-- coverts a binary clause to normal clause in order to reuse map-on-literals-in-a-clause codes+-- liftToClause :: Clause -> Clause+-- liftToClause (BinaryClause _) = error "So far I use generic function approach instead of lifting"++-- | drop the last /N/ literals in a 'Clause' to eliminate unsatisfied literals+{-# INLINABLE shrinkClause #-}+shrinkClause :: Int -> Clause -> IO ()+shrinkClause !n Clause{..} = setNth lits 0 . subtract n =<< getNth lits 0++-- | copies /vec/ and return a new 'Clause'+-- Since 1.0.100 DIMACS reader should use a scratch buffer allocated statically.+{-# INLINE newClauseFromVec #-}+newClauseFromVec :: Bool -> Vec -> IO Clause+newClauseFromVec l vec = do+ n <- getNth vec 0+ v <- newVec $ n + 1+ forM_ [0 .. n] $ \i -> setNth v i =<< getNth vec i+ Clause l <$> newDouble 0 <*> newBool False <*> newInt n <*> return v++-- | returns the number of literals in a clause, even if the given clause is a binary clause+{-# INLINE sizeOfClause #-}+sizeOfClause :: Clause -> IO Int+-- sizeOfClause (BinaryClause _) = return 1+sizeOfClause !c = getNth (lits c) 0++--------------------------------------------------------------------------------++-- | Mutable 'Clause' Vector+type ClauseVector = MV.IOVector Clause++instance VectorFamily ClauseVector Clause where+ asList cv = V.toList <$> V.freeze cv+ dump mes cv = do+ l <- asList cv+ sts <- mapM (dump ",") (l :: [Clause])+ return $ mes ++ tail (concat sts)++-- | returns a new 'ClauseVector'+newClauseVector :: Int -> IO ClauseVector+newClauseVector n = do+ v <- MV.new (max 4 n)+ MV.set v NullClause+ return v++-- | returns the nth 'Clause'+{-# INLINE getNthClause #-}+getNthClause :: ClauseVector -> Int -> IO Clause+getNthClause = MV.unsafeRead++-- | sets the nth 'Clause'+{-# INLINE setNthClause #-}+setNthClause :: ClauseVector -> Int -> Clause -> IO ()+setNthClause = MV.unsafeWrite++-- | swaps the two 'Clause's+{-# INLINE swapClauses #-}+swapClauses :: ClauseVector -> Int -> Int -> IO ()+swapClauses = MV.unsafeSwap
+ SAT/Solver/Mios/ClauseManager.hs view
@@ -0,0 +1,324 @@+-- | A shrinkable 'VectorFamily' of 'C.Clause'+{-# LANGUAGE+ BangPatterns+ , DuplicateRecordFields+ , FlexibleInstances+ , MultiParamTypeClasses+ , RecordWildCards+ , ViewPatterns+ #-}+{-# LANGUAGE Trustworthy #-}++module SAT.Solver.Mios.ClauseManager+ (+ -- * higher level interface for ClauseVector+ ClauseManager (..)+-- -- * vector of clauses+-- , SimpleManager+ -- * Manager with an extra Int (used as sort key or blocking literal)+ , ClauseExtManager+ , pushClauseWithKey+ , getKeyVector+ , markClause+-- , purifyManager+ -- * WatcherList+ , WatcherList+ , newWatcherList+ , getNthWatcher+ , garbageCollect+-- , numberOfRegisteredClauses+ )+ where++import Control.Monad (forM, unless, when)+import qualified Data.IORef as IORef+import qualified Data.List as L+import qualified Data.Vector as V+import qualified Data.Vector.Mutable as MV+import SAT.Solver.Mios.Types+import qualified SAT.Solver.Mios.Clause as C++-- | resizable clause vector+class ClauseManager a where+ newManager :: Int -> IO a+ numberOfClauses :: a -> IO Int+ clearManager :: a -> IO ()+ shrinkManager :: a -> Int -> IO ()+ getClauseVector :: a -> IO C.ClauseVector+ pushClause :: a -> C.Clause -> IO ()+-- removeClause :: a -> C.Clause -> IO ()+-- removeNthClause :: a -> Int -> IO ()++{-+-- | The Clause Container+data SimpleManager = SimpleManager+ {+ _nActives :: IntSingleton -- number of active clause+ , _clauseVector :: IORef.IORef C.ClauseVector -- clause list+ }++instance ClauseManager SimpleManager where+ {-# SPECIALIZE INLINE newManager :: Int -> IO SimpleManager #-}+ newManager initialSize = do+ i <- newInt 0+ v <- C.newClauseVector initialSize+ SimpleManager i <$> IORef.newIORef v+ {-# SPECIALIZE INLINE numberOfClauses :: SimpleManager -> IO Int #-}+ numberOfClauses SimpleManager{..} = getInt _nActives+ {-# SPECIALIZE INLINE clearManager :: SimpleManager -> IO () #-}+ clearManager SimpleManager{..} = setInt _nActives 0+ {-# SPECIALIZE INLINE shrinkManager :: SimpleManager -> Int -> IO () #-}+ shrinkManager SimpleManager{..} k = modifyInt _nActives (subtract k)+ {-# SPECIALIZE INLINE getClauseVector :: SimpleManager -> IO C.ClauseVector #-}+ getClauseVector SimpleManager{..} = IORef.readIORef _clauseVector+ -- | O(1) inserter+ {-# SPECIALIZE INLINE pushClause :: SimpleManager -> C.Clause -> IO () #-}+ pushClause !SimpleManager{..} !c = do+ !n <- getInt _nActives+ !v <- IORef.readIORef _clauseVector+ if MV.length v - 1 <= n+ then do+ v' <- MV.unsafeGrow v (max 8 (MV.length v))+ -- forM_ [n .. MV.length v' - 1] $ \i -> MV.unsafeWrite v' i C.NullClause+ MV.unsafeWrite v' n c+ IORef.writeIORef _clauseVector v'+ else MV.unsafeWrite v n c+ modifyInt _nActives (1 +)+ -- | O(1) remove-and-compact function+ {-# SPECIALIZE INLINE removeNthClause :: SimpleManager -> Int -> IO () #-}+ removeNthClause SimpleManager{..} i = do+ !n <- subtract 1 <$> getInt _nActives+ !v <- IORef.readIORef _clauseVector+ MV.unsafeWrite v i =<< MV.unsafeRead v n+ setInt _nActives n+ -- | O(n) but lightweight remove-and-compact function+ -- __Pre-conditions:__ the clause manager is empty or the clause is stored in it.+ {-# SPECIALIZE INLINE removeClause :: SimpleManager -> C.Clause -> IO () #-}+ removeClause SimpleManager{..} c = do+ -- putStrLn =<< dump "@removeClause| remove " c+ -- putStrLn =<< dump "@removeClause| from " m+ !n <- subtract 1 <$> getInt _nActives+ -- unless (0 <= n) $ error $ "removeClause catches " ++ show n+ !v <- IORef.readIORef _clauseVector+ let+ seekIndex :: Int -> IO Int+ seekIndex k = do+ c' <- MV.unsafeRead v k+ if c' == c then return k else seekIndex $ k + 1+ unless (n == -1) $ do+ !i <- seekIndex 0+ MV.unsafeWrite v i =<< MV.unsafeRead v n+ setInt _nActives n++instance VectorFamily SimpleManager C.Clause where+ dump mes SimpleManager{..} = do+ n <- getInt _nActives+ if n == 0+ then return $ mes ++ "empty clausemanager"+ else do+ l <- take n <$> (asList =<< IORef.readIORef _clauseVector)+ sts <- mapM (dump ",") (l :: [C.Clause])+ return $ mes ++ "[" ++ show n ++ "]" ++ tail (concat sts)+-}++--------------------------------------------------------------------------------++-- | Clause + Blocking Literal+data ClauseExtManager = ClauseExtManager+ {+ _nActives :: IntSingleton -- number of active clause+ , _purged :: BoolSingleton -- whether it needs gc+ , _clauseVector :: IORef.IORef C.ClauseVector -- clause list+ , _keyVector :: IORef.IORef Vec -- Int list+ }++instance ClauseManager ClauseExtManager where+ {-# SPECIALIZE INLINE newManager :: Int -> IO ClauseExtManager #-}+ newManager initialSize = do+ i <- newInt 0+ v <- C.newClauseVector initialSize+ b <- newVec (MV.length v)+ ClauseExtManager i <$> newBool False <*> IORef.newIORef v <*> IORef.newIORef b+ {-# SPECIALIZE INLINE numberOfClauses :: ClauseExtManager -> IO Int #-}+ numberOfClauses ClauseExtManager{..} = getInt _nActives+ {-# SPECIALIZE INLINE clearManager :: ClauseExtManager -> IO () #-}+ clearManager ClauseExtManager{..} = setInt _nActives 0+ {-# SPECIALIZE INLINE shrinkManager :: ClauseExtManager -> Int -> IO () #-}+ shrinkManager ClauseExtManager{..} k = modifyInt _nActives (subtract k)+ {-# SPECIALIZE INLINE getClauseVector :: ClauseExtManager -> IO C.ClauseVector #-}+ getClauseVector ClauseExtManager{..} = IORef.readIORef _clauseVector+ -- | O(1) insertion function+ {-# SPECIALIZE INLINE pushClause :: ClauseExtManager -> C.Clause -> IO () #-}+ pushClause !ClauseExtManager{..} !c = do+ -- checkConsistency m c+ !n <- getInt _nActives+ !v <- IORef.readIORef _clauseVector+ !b <- IORef.readIORef _keyVector+ if MV.length v - 1 <= n+ then do+ let len = max 8 $ MV.length v+ v' <- MV.unsafeGrow v len+ b' <- vecGrow b len+ MV.unsafeWrite v' n c+ setNth b' n 0+ IORef.writeIORef _clauseVector v'+ IORef.writeIORef _keyVector b'+ else MV.unsafeWrite v n c >> setNth b n 0+ modifyInt _nActives (1 +)+{-+ -- | O(n) but lightweight remove-and-compact function+ -- __Pre-conditions:__ the clause manager is empty or the clause is stored in it.+ {-# SPECIALIZE INLINE removeClause :: ClauseExtManager -> C.Clause -> IO () #-}+ removeClause ClauseExtManager{..} c = do+ !n <- subtract 1 <$> getInt _nActives+ !v <- IORef.readIORef _clauseVector+ !b <- IORef.readIORef _keyVector+ let+ seekIndex :: Int -> IO Int+ seekIndex k = do+ c' <- MV.unsafeRead v k+ if c' == c then return k else seekIndex $ k + 1+ unless (n == -1) $ do+ !i <- seekIndex 0+ MV.unsafeWrite v i =<< MV.unsafeRead v n+ setNth b i =<< getNth b n+ setInt _nActives n+ removeNthClause = error "removeNthClause is not implemented on ClauseExtManager"+-}++-- | sets the expire flag to a clause+{-# INLINE markClause #-}+markClause :: ClauseExtManager -> C.Clause -> IO ()+markClause ClauseExtManager{..} c = do+ !n <- getInt _nActives+ !v <- IORef.readIORef _clauseVector+ let+ seekIndex :: Int -> IO ()+ seekIndex k = do+ c' <- MV.unsafeRead v k+ if c' == c then MV.unsafeWrite v k C.NullClause else seekIndex $ k + 1+ unless (n == 0) $ do+ seekIndex 0+ setBool _purged True++{-# INLINE purifyManager #-}+purifyManager :: ClauseExtManager -> IO ()+purifyManager ClauseExtManager{..} = do+ diry <- getBool _purged+ when diry $ do+ n <- getInt _nActives+ vec <- IORef.readIORef _clauseVector+ keys <- IORef.readIORef _keyVector+ let+ loop :: Int -> Int -> IO Int+ loop ((< n) -> False) n' = return n'+ loop i j = do+ c <- C.getNthClause vec i+ if c /= C.NullClause+ then do+ unless (i == j) $ do+ C.setNthClause vec j c+ setNth keys j =<< getNth keys i+ loop (i + 1) (j + 1)+ else loop (i + 1) j+ setInt _nActives =<< loop 0 0+ setBool _purged False++-- | returns the associated Int vector+{-# INLINE getKeyVector #-}+getKeyVector :: ClauseExtManager -> IO Vec+getKeyVector ClauseExtManager{..} = IORef.readIORef _keyVector++-- | O(1) inserter+{-# INLINE pushClauseWithKey #-}+pushClauseWithKey :: ClauseExtManager -> C.Clause -> Lit -> IO ()+pushClauseWithKey !ClauseExtManager{..} !c k = do+ -- checkConsistency m c+ !n <- getInt _nActives+ !v <- IORef.readIORef _clauseVector+ !b <- IORef.readIORef _keyVector+ if MV.length v - 1 <= n+ then do+ let len = max 8 $ MV.length v+ v' <- MV.unsafeGrow v len+ b' <- vecGrow b len+ MV.unsafeWrite v' n c+ setNth b' n k+ IORef.writeIORef _clauseVector v'+ IORef.writeIORef _keyVector b'+ else MV.unsafeWrite v n c >> setNth b n k+ modifyInt _nActives (1 +)++instance VectorFamily ClauseExtManager C.Clause where+ dump mes ClauseExtManager{..} = do+ n <- getInt _nActives+ if n == 0+ then return $ mes ++ "empty ClauseExtManager"+ else do+ l <- take n <$> (asList =<< IORef.readIORef _clauseVector)+ sts <- mapM (dump ",") (l :: [C.Clause])+ return $ mes ++ "[" ++ show n ++ "]" ++ tail (concat sts)++-------------------------------------------------------------------------------- WatcherList++-- | Vector of 'ClauseExtManager'+type WatcherList = V.Vector ClauseExtManager++-- | /n/ is the number of 'Var', /m/ is default size of each watcher list+-- | For /n/ vars, we need [0 .. 2 + 2 * n - 1] slots, namely /2 * (n + 1)/-length vector+newWatcherList :: Int -> Int -> IO WatcherList+newWatcherList n m = V.fromList <$> forM [0 .. int2lit (negate n) + 1] (\_ -> newManager m)++-- | returns the watcher List :: "ClauseManager" for "Literal" /l/+{-# INLINE getNthWatcher #-}+getNthWatcher :: WatcherList -> Lit-> ClauseExtManager+getNthWatcher = V.unsafeIndex++instance VectorFamily WatcherList C.Clause where+ dump mes wl = (mes ++) . L.concat <$> forM [1 .. V.length wl - 1] (\i -> dump ("\n" ++ show (lit2int i) ++ "' watchers:") (getNthWatcher wl i))++-- | purges all expirable clauses in 'WatcherList'+{-# INLINE garbageCollect #-}+garbageCollect :: WatcherList -> IO ()+garbageCollect wm = V.mapM_ purifyManager wm++numberOfRegisteredClauses :: WatcherList -> IO Int+numberOfRegisteredClauses ws = sum <$> V.mapM numberOfClauses ws++{-+-------------------------------------------------------------------------------- debugging stuff++checkConsistency :: ClauseManager a => a -> C.Clause -> IO ()+checkConsistency manager c = do+ nc <- numberOfClauses manager+ vec <- getClauseVector manager+ let+ loop :: Int -> IO ()+ loop i = do+ when (i < nc) $ do+ c' <- MV.unsafeRead vec i+ when (c' == c) $ error "insert a clause to a ClauseMananger twice"+ loop $ i + 1+ loop 0++checkClauseOrder :: ClauseManager a => a -> IO ()+checkClauseOrder manager = do+ putStr "checking..."+ nc <- numberOfClauses manager+ vec <- getClauseVector manager+ let+ nthActivity :: Int -> IO Double+ nthActivity i = getDouble . C.activity =<< MV.unsafeRead vec i+ report :: Int -> Int -> IO ()+ report i j = (putStr . (++ ", ") . show =<< nthActivity i) >> when (i < j) (report (i + 1) j)+ loop :: Int -> Double -> IO ()+ loop i v = do+ when (i < nc) $ do+ c <- MV.unsafeRead vec i+ a <- getDouble (C.activity c)+ when (c == C.NullClause) $ error "null is included"+ when (v < a) $ report 0 i >> error ("unsorted clause vector: " ++ show (nc, i))+ loop (i + 1) a+ loop 0 =<< nthActivity 0+ putStrLn "done"+-}
+ SAT/Solver/Mios/Data/Singleton.hs view
@@ -0,0 +1,196 @@+-- | A fast(est) mutable data+{-# LANGUAGE+ BangPatterns+ #-}+{-# LANGUAGE Trustworthy #-}++module SAT.Solver.Mios.Data.Singleton+ (+ -- * Bool+ BoolSingleton+ , newBool+ , getBool+ , setBool+ , modifyBool+ -- * Int+ , IntSingleton+ , newInt+ , getInt+ , setInt+ , modifyInt+ -- * Double+ , DoubleSingleton+ , newDouble+ , getDouble+ , setDouble+ , modifyDouble+ )+ where+{-+----------------------------------------+-- Implementation 1. :: IORef+----------------------------------------++import Data.IORef++type BoolSingleton = IORef Bool++newBool :: Bool -> IO BoolSingleton+newBool = newIORef++{-# INLINE getBool #-}+getBool :: BoolSingleton -> IO Bool+getBool = readIORef++{-# INLINE setBool #-}+setBool :: BoolSingleton -> Bool -> IO ()+setBool = writeIORef++{-# INLINE modifyBool #-}+modifyBool :: BoolSingleton -> (Bool -> Bool) -> IO ()+modifyBool = modifyIORef'++type IntSingleton = IORef Int++newInt :: Int -> IO IntSingleton+newInt = newIORef++{-# INLINE getInt #-}+getInt :: IntSingleton -> IO Int+getInt = readIORef++{-# INLINE setInt #-}+setInt :: IntSingleton -> Int -> IO ()+setInt = writeIORef++{-# INLINE modifyInt #-}+modifyInt :: IntSingleton -> (Int -> Int) -> IO ()+modifyInt = modifyIORef'++type DoubleSingleton = IORef Double++newDouble :: Double -> IO DoubleSingleton+newDouble = newIORef++{-# INLINE getDouble #-}+getDouble :: DoubleSingleton -> IO Double+getDouble = readIORef++{-# INLINE setDouble #-}+setDouble :: DoubleSingleton -> Double -> IO ()+setDouble = writeIORef++{-# INLINE modifyDouble #-}+modifyDouble :: DoubleSingleton -> (Double -> Double) -> IO ()+modifyDouble = modifyIORef'+-}+{-+----------------------------------------+-- Implementation 2. :: Data.Mutable.IOURef+----------------------------------------++import qualified Data.Mutable as M++newtype IntSingleton = IntSingleton+ {+ mutableInt :: M.IOURef Int+ }++newInt :: IO IntSingleton+newInt = IntSingleton <$> M.newRef 0++{-# INLINE getInt #-}+getInt :: IntSingleton -> IO Int+getInt !(IntSingleton val) = M.readRef val++{-# INLINE setInt #-}+setInt :: IntSingleton -> Int -> IO ()+setInt !(IntSingleton val) !x = M.writeRef val x++{-# INLINE modifyInt #-}+modifyInt :: IntSingleton -> (Int -> Int) -> IO ()+modifyInt !(IntSingleton val) !f = M.modifyRef' val f+-}++-- {-+----------------------------------------+-- Implementation 3. :: Data.Vector.Unboxed.Mutable+----------------------------------------++import qualified Data.Vector.Unboxed.Mutable as UV++-- | mutable Int+type IntSingleton = UV.IOVector Int++-- | returns a new 'IntSingleton'+newInt :: Int -> IO IntSingleton+newInt k = do+ s <- UV.new 1+ UV.unsafeWrite s 0 k+ return s++-- | returns the value+{-# INLINE getInt #-}+getInt :: IntSingleton -> IO Int+getInt val = UV.unsafeRead val 0++-- | sets the value+{-# INLINE setInt #-}+setInt :: IntSingleton -> Int -> IO ()+setInt val !x = UV.unsafeWrite val 0 x++-- | modifies the value+{-# INLINE modifyInt #-}+modifyInt :: IntSingleton -> (Int -> Int) -> IO ()+modifyInt val !f = UV.unsafeModify val f 0++-- | mutable Bool+type BoolSingleton = UV.IOVector Bool++-- | returns a new 'BoolSingleton'+newBool :: Bool -> IO BoolSingleton+newBool b = do+ s <- UV.new 1+ UV.unsafeWrite s 0 b+ return s++-- | returns the value+{-# INLINE getBool #-}+getBool :: BoolSingleton -> IO Bool+getBool val = UV.unsafeRead val 0++-- | sets the value+{-# INLINE setBool #-}+setBool :: BoolSingleton -> Bool -> IO ()+setBool val !x = UV.unsafeWrite val 0 x++-- | modifies the value+{-# INLINE modifyBool #-}+modifyBool :: BoolSingleton -> (Bool -> Bool) -> IO ()+modifyBool val !f = UV.unsafeModify val f 0++-- | mutable Double+type DoubleSingleton = UV.IOVector Double++-- | returns a new 'DoubleSingleton'+newDouble :: Double -> IO DoubleSingleton+newDouble d = do+ s <- UV.new 1+ UV.unsafeWrite s 0 d+ return s++-- | returns the value+{-# INLINE getDouble #-}+getDouble :: DoubleSingleton -> IO Double+getDouble val = UV.unsafeRead val 0++-- | sets the value+{-# INLINE setDouble #-}+setDouble :: DoubleSingleton -> Double -> IO ()+setDouble val !x = UV.unsafeWrite val 0 x++-- | modifies the value+{-# INLINE modifyDouble #-}+modifyDouble :: DoubleSingleton -> (Double -> Double) -> IO ()+modifyDouble val !f = UV.unsafeModify val f 0+-- -}
+ SAT/Solver/Mios/Data/Stack.hs view
@@ -0,0 +1,93 @@+-- | stack of Int, by adding the length field as the zero-th element to a 'Vec'+{-# LANGUAGE+ BangPatterns+ , FlexibleInstances+ , MultiParamTypeClasses+ #-}+{-# LANGUAGE Trustworthy #-}++module SAT.Solver.Mios.Data.Stack+ (+ Stack+ , newStack+ , clearStack+ , sizeOfStack+ , pushToStack+ , popFromStack+ , lastOfStack+ , shrinkStack+ , asSizedVec+ , isoVec+ )+ where++import qualified Data.Vector.Unboxed.Mutable as UV+import SAT.Solver.Mios.Types++-- | Unboxed mutable stack for Int.+newtype Stack = Stack+ {+ ivec :: UV.IOVector Int+ }++instance VectorFamily Stack Int where+ dump str v = (str ++) . show <$> asList v+ {-# SPECIALIZE INLINE asVec :: Stack -> Vec #-}+ asVec (Stack v) = UV.unsafeTail v+ asList (Stack v) = do+ (n : l) <- asList v+ return $ take n l++-- | returns the number of elements+{-# INLINE sizeOfStack #-}+sizeOfStack :: Stack -> IO Int+sizeOfStack (Stack v) = UV.unsafeRead v 0++-- | clear stack+{-# INLINE clearStack #-}+clearStack :: Stack -> IO ()+clearStack (Stack v) = UV.unsafeWrite v 0 0++-- | returns a new stack which size is @size@+{-# INLINABLE newStack #-}+newStack :: Int -> IO Stack+newStack n = do+ v <- UV.new $ n + 1+ UV.set v 0+ return $ Stack v++-- | pushs an int to 'Stack'+{-# INLINE pushToStack #-}+pushToStack :: Stack -> Int -> IO ()+pushToStack (Stack v) !x = do+ !i <- (+ 1) <$> UV.unsafeRead v 0+ UV.unsafeWrite v i x+ UV.unsafeWrite v 0 i++-- | drops the first element from 'Stack'+{-# INLINE popFromStack #-}+popFromStack :: Stack -> IO ()+popFromStack (Stack v) = UV.unsafeModify v (subtract 1) 0++-- | peeks the last element in 'Stack'+{-# INLINE lastOfStack #-}+lastOfStack :: Stack -> IO Int+lastOfStack (Stack v) = UV.unsafeRead v =<< UV.unsafeRead v 0++-- | Shrink the stack. The given arg means the number of discards.+-- therefore, shrink s n == for [1 .. n] $ \_ -> pop s+{-# INLINE shrinkStack #-}+shrinkStack :: Stack -> Int -> IO ()+shrinkStack (Stack v) k = UV.unsafeModify v (subtract k) 0++-- | converts Stack to sized Vec; this is the method to get the internal vector+{-# INLINE asSizedVec #-}+asSizedVec :: Stack -> Vec+asSizedVec (Stack v) = v++-- | isomorphic conversion to 'Vec'+--+-- Note: 'asVec' drops the 1st element and no copy (unsafe operation); 'isoVec' really copies the real elements+{-# INLINE isoVec #-}+isoVec :: Stack -> IO Vec+isoVec (Stack v) = UV.clone . flip UV.take v . (1 +) =<< UV.unsafeRead v 0
+ SAT/Solver/Mios/Data/Vec.hs view
@@ -0,0 +1,86 @@+-- | The fundamental data structure: Fixed Mutable Unboxed Int Vector+{-# LANGUAGE+ BangPatterns+ #-}+{-# LANGUAGE Trustworthy #-}++module SAT.Solver.Mios.Data.Vec+ (+ Vec+ , sizeOfVector+ , getNth+ , setNth+ , swapBetween+ , modifyNth+ , setAll+ , newVec+ , newVecWith+ , newSizedVecIntFromList+ , newSizedVecIntFromUVector+ , vecGrow+ )+ where++import qualified Data.Vector.Unboxed as U+import qualified Data.Vector.Unboxed.Mutable as UV++-- | Costs of all operations are /O/(/1/)+type Vec = UV.IOVector Int++-- | returns the size of 'Vec'+{-# INLINE sizeOfVector #-}+sizeOfVector :: Vec -> IO Int+sizeOfVector v = return $! UV.length v++-- | returns a new 'Vec'+{-# INLINE newVec #-}+newVec :: Int -> IO Vec+newVec = UV.new++-- | returns a new 'Vec' filled with an Int+{-# INLINE newVecWith #-}+newVecWith :: Int -> Int -> IO Vec+newVecWith n x = do+ v <- UV.new n+ UV.set v x+ return v++-- | gets the nth value+{-# INLINE getNth #-}+getNth :: Vec -> Int -> IO Int+getNth = UV.unsafeRead++-- | sets the nth value+{-# INLINE setNth #-}+setNth :: Vec -> Int -> Int -> IO ()+setNth = UV.unsafeWrite++-- | modify the nth value+{-# INLINE modifyNth #-}+modifyNth :: Vec -> (Int -> Int) -> Int -> IO ()+modifyNth = UV.unsafeModify++-- | sets all elements+{-# INLINE setAll #-}+setAll :: Vec -> Int -> IO ()+setAll = UV.set++-- | swaps two elements+{-# INLINE swapBetween #-}+swapBetween:: Vec -> Int -> Int -> IO ()+swapBetween = UV.unsafeSwap++-- | returns a new 'Vec' from a @[Int]@+{-# INLINE newSizedVecIntFromList #-}+newSizedVecIntFromList :: [Int] -> IO Vec+newSizedVecIntFromList !l = U.unsafeThaw $ U.fromList (length l : l)++-- | returns a new 'Vec' from a Unboxed Int Vector+{-# INLINE newSizedVecIntFromUVector #-}+newSizedVecIntFromUVector :: U.Vector Int -> IO Vec+newSizedVecIntFromUVector = U.unsafeThaw++-- | calls @unasfeGrow@+{-# INLINE vecGrow #-}+vecGrow :: Vec -> Int -> IO Vec+vecGrow = UV.unsafeGrow
+ SAT/Solver/Mios/Data/VecBool.hs view
@@ -0,0 +1,55 @@+-- | Mutable Unboxed Boolean Vector+--+-- * __VecBool@::UV.IOVector Bool@ -- data type that contains a mutable list of elements+--+{-# LANGUAGE+ BangPatterns+ , FlexibleInstances+ , MultiParamTypeClasses+ #-}+{-# LANGUAGE Trustworthy #-}++module SAT.Solver.Mios.Data.VecBool+ (+ VecBool+ , newVecBool+ , getNthBool+ , setNthBool+ , modifyNthBool+ )+ where++import Control.Monad (forM)+import qualified Data.Vector.Unboxed.Mutable as UV+import SAT.Solver.Mios.Types (VectorFamily(..))++-- | Mutable unboxed Bool Vector+type VecBool = UV.IOVector Bool++-- | provides 'clear' and 'size'+instance VectorFamily VecBool Bool where+ clear _ = error "VecBool.clear"+ asList v = forM [0 .. UV.length v - 1] $ UV.unsafeRead v+ dump str v = (str ++) . show <$> asList v++-- | returns a new 'VecBool'+newVecBool :: Int -> Bool -> IO VecBool+newVecBool n x = do+ v <- UV.new n+ UV.set v x+ return v++-- | returns the nth value in 'VecBool'+{-# INLINE getNthBool #-}+getNthBool :: VecBool -> Int -> IO Bool+getNthBool = UV.unsafeRead++-- | sets the nth value+{-# INLINE setNthBool #-}+setNthBool :: VecBool -> Int -> Bool -> IO ()+setNthBool = UV.unsafeWrite++-- | sets the nth value+{-# INLINE modifyNthBool #-}+modifyNthBool :: VecBool -> (Bool -> Bool) -> Int -> IO ()+modifyNthBool = UV.unsafeModify
+ SAT/Solver/Mios/Data/VecDouble.hs view
@@ -0,0 +1,53 @@+-- | Mutable Unboxed Double Vector+{-# LANGUAGE+ BangPatterns+ , FlexibleInstances+ , MultiParamTypeClasses+ #-}+{-# LANGUAGE Trustworthy #-}++module SAT.Solver.Mios.Data.VecDouble+ (+ VecDouble+ , newVecDouble+ , getNthDouble+ , setNthDouble+ , modifyNthDouble+ )+ where++import Control.Monad (forM)+import Data.List ()+import qualified Data.Vector.Unboxed.Mutable as UV+import SAT.Solver.Mios.Types (VectorFamily(..))++-- | Mutable unboxed Double Vector+type VecDouble = UV.IOVector Double++instance VectorFamily VecDouble Double where+ clear _ = error "VecDouble.clear"+ asList v = forM [0 .. UV.length v - 1] $ UV.unsafeRead v+ dump str v = (str ++) . show <$> asList v++-- | returns a new 'VecDouble'+newVecDouble :: Int -> Double -> IO VecDouble+newVecDouble n 0 = UV.new n+newVecDouble n x = do+ v <- UV.new n+ UV.set v x+ return v++-- | returns the nth value in 'VecDouble'+{-# INLINE getNthDouble #-}+getNthDouble :: Int -> VecDouble -> IO Double+getNthDouble !n v = UV.unsafeRead v n++-- | sets the nth value+{-# INLINE setNthDouble #-}+setNthDouble :: Int -> VecDouble -> Double -> IO ()+setNthDouble !n v !x = UV.unsafeWrite v n x++-- | updates the nth value+{-# INLINE modifyNthDouble #-}+modifyNthDouble :: Int -> VecDouble -> (Double -> Double) -> IO ()+modifyNthDouble !n v !f = UV.unsafeModify v f n
+ SAT/Solver/Mios/Glucose.hs view
@@ -0,0 +1,72 @@+-- | This is a part of MIOS+{-# LANGUAGE+ BangPatterns+ , RecordWildCards+ , ScopedTypeVariables+ , ViewPatterns+ #-}+{-# LANGUAGE Safe #-}++module SAT.Solver.Mios.Glucose+ (+ computeLBD+ , lbdOf+ , setLBD+ , updateLBD+ , nextReduction+ )+ where++import Control.Monad (when)+import SAT.Solver.Mios.Types+import SAT.Solver.Mios.Clause+import SAT.Solver.Mios.Solver++-- | returns the LBD vaule for 'Vec[1 ..]'+computeLBD :: Solver -> Vec -> IO Int+computeLBD Solver{..} vec = do+ key <- (1 +) <$> getInt lbd'key+ setInt lbd'key key+ nv <- getNth vec 0+ let+ loop :: Int -> Int -> IO Int+ loop ((<= nv) -> False) n = return n+ loop !i !n = do+ l <- getNth level . lit2var =<< getNth vec i+ seen <- if l == 0 then return True else (key ==) <$> getNth lbd'seen l+ if seen+ then loop (i + 1) n+ else setNth lbd'seen l key >> loop (i + 1) (n + 1)+ loop 1 0++-- | returns the LBD value of 'Clause'+{-# INLINE lbdOf #-}+lbdOf :: Solver -> Clause -> IO Int+lbdOf s (lits -> v) = computeLBD s v++-- | update the LBD field in 'Clause'+{-# INLINE setLBD #-}+setLBD :: Solver -> Clause -> IO ()+setLBD s c = setInt (lbd c) =<< lbdOf s c++-- | update the lbd field of /c/+{-# INLINE updateLBD #-}+updateLBD :: Solver -> Clause -> IO ()+updateLBD _ NullClause = error "LBD71"+updateLBD _ (learnt -> False) = return ()+updateLBD s c@Clause{..} = setInt lbd =<< lbdOf s c++-- | 0 based+--+-- >>> nextReduction 0+-- 20000+-- >>> nextReduction 1+-- 40000 + 200 = 20000 + 20000 + 200+-- >>> nextReduction 2+-- 6000 + 600 = 20000 + 20200 + 20000 + 400+-- >>> nextReduction 3+-- 80000 + 1200 = 20000 + 20200 + 20400 + 20000 + 600+--+nextReduction :: Int -> Int -> Int+-- nextReduction _ n = 30000 + 10000 * n+nextReduction b n = b + 300 * n
+ SAT/Solver/Mios/Internal.hs view
@@ -0,0 +1,34 @@+-- | Internal Settings+module SAT.Solver.Mios.Internal+ (+ versionId+ , MiosConfiguration (..)+ , defaultConfiguration+ , module Plumbing+ )+ where+import SAT.Solver.Mios.Data.VecBool as Plumbing+import SAT.Solver.Mios.Data.VecDouble as Plumbing+import SAT.Solver.Mios.Data.Stack as Plumbing++-- | version name+versionId :: String+versionId = "mios 1.2 <https://github.com/shnarazk/mios/>" -- blocking literal + lbd + phase-saving++-- | solver's parameters; random decision rate was dropped.+data MiosConfiguration = MiosConfiguration+ {+ variableDecayRate :: Double -- ^ decay rate for variable activity+ , clauseDecayRate :: Double -- ^ decay rate for clause activity+ , collectStats :: Bool -- ^ whether collect and report statistics+ }++-- | dafault configuration+--+-- * Minisat-1.14 uses @(0.95, 0.999, 0.2 = 20 / 1000)@.+-- * Minisat-2.20 uses @(0.95, 0.999, 0)@.+-- * Gulcose-4.0 uses @(0.8 , 0.999, 0)@.+-- * Mios-1.2 uses @(0.95, 0.999, 0)@.+--+defaultConfiguration :: MiosConfiguration+defaultConfiguration = MiosConfiguration 0.95 0.999 {- 0 -} False
+ SAT/Solver/Mios/M114.hs view
@@ -0,0 +1,816 @@+-- | This is a part of MIOS+{-# LANGUAGE+ BangPatterns+ , RecordWildCards+ , ScopedTypeVariables+ , ViewPatterns+ #-}+{-# LANGUAGE Safe #-}++module SAT.Solver.Mios.M114+ (+ simplifyDB+ , solve+ )+ where++import Control.Monad (forM_, unless, void, when)+import Data.Bits+import Data.Foldable (foldrM)+import SAT.Solver.Mios.Types+import SAT.Solver.Mios.Internal+import SAT.Solver.Mios.Clause+import SAT.Solver.Mios.ClauseManager+import SAT.Solver.Mios.Solver+import SAT.Solver.Mios.Glucose++-- | #114: __RemoveWatch__+{-# INLINABLE removeWatch #-}+removeWatch :: Solver -> Clause -> IO ()+removeWatch Solver{..} c = do+ let lvec = asVec c+ l1 <- negateLit <$> getNth lvec 0+ markClause (getNthWatcher watches l1) c+ l2 <- negateLit <$> getNth lvec 1+ markClause (getNthWatcher watches l2) c++--------------------------------------------------------------------------------+-- Operations on 'Clause'+--------------------------------------------------------------------------------++-- | __Fig. 8. (p.12)__ create a new LEARNT clause and adds it to watcher lists+-- This is a strippped-down version of 'newClause' in Solver+{-# INLINABLE newLearntClause #-}+newLearntClause :: Solver -> Vec -> IO ()+newLearntClause s@Solver{..} ps = do+ good <- getBool ok+ when good $ do+ -- ps is a 'SizedVectorInt'; ps[0] is the number of active literals+ -- Since this solver must generate only healthy learnt clauses, we need not to run misc check in 'newClause'+ k <- getNth ps 0+ case k of+ 1 -> do+ l <- getNth ps 1+ unsafeEnqueue s l NullClause+ _ -> do+ -- allocate clause:+ c <- newClauseFromVec True ps+ let vec = asVec c+ -- Pick a second literal to watch:+ let+ findMax :: Int -> Int -> Int -> IO Int+ findMax ((< k) -> False) j _ = return j+ findMax i j val = do+ v' <- lit2var <$> getNth vec i+ a <- getNth assigns v'+ b <- getNth level v'+ if (a /= lBottom) && (val < b)+ then findMax (i + 1) i b+ else findMax (i + 1) j val+ swapBetween vec 1 =<< findMax 0 0 0 -- Let @max_i@ be the index of the literal with highest decision level+ -- Bump, enqueue, store clause:+ claBumpActivity s c -- newly learnt clauses should be considered active+ -- Add clause to all managers+ pushClause learnts c+ l <- getNth vec 0+ pushClauseWithKey (getNthWatcher watches (negateLit l)) c 0+ l1 <- negateLit <$> getNth vec 1+ pushClauseWithKey (getNthWatcher watches l1) c 0+ -- update the solver state by @l@+ unsafeEnqueue s l c+ -- Since unsafeEnqueue updates the 1st literal's level, setLBD should be called after unsafeEnqueue+ setLBD s c++-- | __Simplify.__ At the top-level, a constraint may be given the opportunity to+-- simplify its representation (returns @False@) or state that the constraint is+-- satisfied under the current assignment and can be removed (returns @True@).+-- A constraint must /not/ be simplifiable to produce unit information or to be+-- conflicting; in that case the propagation has not been correctly defined.+--+-- MIOS NOTE: the original doesn't update watchers; only checks its satisfiabiliy.+{-# INLINABLE simplify #-}+simplify :: Solver -> Clause -> IO Bool+simplify s c = do+ n <- sizeOfClause c+ let+ lvec = asVec c+ loop ::Int -> IO Bool+ loop ((< n) -> False) = return False+ loop i = do+ v <- valueLit s =<< getNth lvec i+ if v == 1 then return True else loop (i + 1)+ loop 0++--------------------------------------------------------------------------------+-- MIOS NOTE on Minor methods:+--+-- * no (meaningful) 'newVar' in mios+-- * 'assume' is defined in 'Solver'+-- * `cancelUntil` is defined in 'Solver'++--------------------------------------------------------------------------------+-- Major methods++-- | M114: __Fig. 10. (p.15)__+--+-- analyze : (confl : Clause*) (out_learnt : vec<Lit>&) (out_btlevel :: int&) -> [void]+--+-- __Description:_-+-- Analzye confilct and produce a reason clause.+--+-- __Pre-conditions:__+-- * 'out_learnt' is assumed to be cleared.+-- * Corrent decision level must be greater than root level.+--+-- __Post-conditions:__+-- * 'out_learnt[0]' is the asserting literal at level 'out_btlevel'.+-- * If out_learnt.size() > 1 then 'out_learnt[1]' has the greatest decision level of the+-- rest of literals. There may be others from the same level though.+--+-- @analyze@ is invoked from @search@+-- {-# INLINEABLE analyze #-}+analyze :: Solver -> Clause -> IO Int+analyze s@Solver{..} confl = do+ -- litvec+ clearStack litsLearnt+ pushToStack litsLearnt 0 -- reserve the first place for the unassigned literal+ dl <- decisionLevel s+ let+ litsVec = asVec litsLearnt+ trailVec = asVec trail+ loopOnClauseChain :: Clause -> Lit -> Int -> Int -> Int -> IO Int+ loopOnClauseChain c p ti bl pathC = do -- p : literal, ti = trail index, bl = backtrack level+ when (learnt c) $ do+ claBumpActivity s c+ -- update LBD like #Glucose4.0+ d <- getInt (lbd c)+ when (2 < d) $ do+ nblevels <- lbdOf s c+ when (nblevels + 1 < d) $ do -- improve the LBD+ when (d <= 30) $ setBool (protected c) True -- 30 is `lbLBDFrozenClause`+ -- seems to be interesting: keep it fro the next round+ setInt (lbd c) nblevels -- Update it+ sc <- sizeOfClause c+ let+ lvec = asVec c+ loopOnLiterals :: Int -> Int -> Int -> IO (Int, Int)+ loopOnLiterals ((< sc) -> False) b pc = return (b, pc) -- b = btLevel, pc = pathC+ loopOnLiterals j b pc = do+ (q :: Lit) <- getNth lvec j+ let v = lit2var q+ sn <- getNth an'seen v+ l <- getNth level v+ if sn == 0 && 0 < l+ then do+ varBumpActivity s v+ setNth an'seen v 1+ if dl <= l -- cancelUntil doesn't clear level of cancelled literals+ then do+ -- glucose heuristics+ r <- getNthClause reason v+ when (r /= NullClause && learnt r) $ pushToStack lastDL q+ -- end of glucose heuristics+ loopOnLiterals (j + 1) b (pc + 1)+ else pushToStack litsLearnt q >> loopOnLiterals (j + 1) (max b l) pc+ else loopOnLiterals (j + 1) b pc+ (b', pathC') <- loopOnLiterals (if p == bottomLit then 0 else 1) bl pathC+ let+ -- select next clause to look at+ nextPickedUpLit :: Int -> IO Int+ nextPickedUpLit i = do+ x <- getNth an'seen . lit2var =<< getNth trailVec i+ if x == 0 then nextPickedUpLit $ i - 1 else return i+ ti' <- nextPickedUpLit ti+ nextP <- getNth trailVec ti'+ let nextV = lit2var nextP+ confl' <- getNthClause reason nextV+ setNth an'seen nextV 0+ if 1 < pathC'+ then loopOnClauseChain confl' nextP (ti' - 1) b' (pathC' - 1)+ else setNth litsVec 0 (negateLit nextP) >> return b'+ ti <- subtract 1 <$> sizeOfStack trail+ levelToReturn <- loopOnClauseChain confl bottomLit ti 0 0+ -- Simplify phase (implemented only @expensive_ccmin@ path)+ n <- sizeOfStack litsLearnt+ clearStack an'stack -- analyze_stack.clear();+ clearStack an'toClear -- out_learnt.copyTo(analyze_toclear);+ pushToStack an'toClear =<< getNth litsVec 0+ let+ merger :: Int -> Int -> IO Int+ merger ((< n) -> False) b = return b+ merger i b = do+ l <- getNth litsVec i+ pushToStack an'toClear l+ -- restrict the search depth (range) to 32+ merger (i + 1) . setBit b . (31 .&.) =<< getNth level (lit2var l)+ levels <- merger 1 0+ let+ loopOnLits :: Int -> Int -> IO ()+ loopOnLits ((< n) -> False) n' = shrinkStack litsLearnt $ n - n'+ loopOnLits i j = do+ l <- getNth litsVec i+ c1 <- (NullClause ==) <$> getNthClause reason (lit2var l)+ if c1+ then setNth litsVec j l >> loopOnLits (i + 1) (j + 1)+ else do+ c2 <- not <$> analyzeRemovable s l levels+ if c2+ then setNth litsVec j l >> loopOnLits (i + 1) (j + 1)+ else loopOnLits (i + 1) j+ loopOnLits 1 1 -- the first literal is specail+ -- glucose heuristics+ nld <- sizeOfStack lastDL+ lbd' <- computeLBD s $ asSizedVec litsLearnt -- this is not the right value+ let+ vec = asVec lastDL+ loopOnLastDL :: Int -> IO ()+ loopOnLastDL ((< nld) -> False) = return ()+ loopOnLastDL i = do+ v <- lit2var <$> getNth vec i+ d' <- getInt . lbd =<< getNthClause reason v+ when (lbd' < d') $ varBumpActivity s v+ loopOnLastDL $ i + 1+ loopOnLastDL 0+ clearStack lastDL+ -- Clear seen+ k <- sizeOfStack an'toClear+ let+ vec' = asVec an'toClear+ cleaner :: Int -> IO ()+ cleaner ((< k) -> False) = return ()+ cleaner i = do+ v <- lit2var <$> getNth vec' i+ setNth an'seen v 0+ cleaner $ i + 1+ cleaner 0+ return levelToReturn++-- | #M114+-- 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.+--+-- Implementation memo:+--+-- * @an'toClear@ is initialized by @ps@ in @analyze@ (a copy of 'learnt').+-- This is used only in this function and @analyze@.+--+{-# INLINEABLE analyzeRemovable #-}+analyzeRemovable :: Solver -> Lit -> Int -> IO Bool+analyzeRemovable Solver{..} p minLevel = do+ -- assert (reason[var(p)]!= NullCaulse);+ clearStack an'stack -- analyze_stack.clear()+ pushToStack an'stack p -- analyze_stack.push(p);+ top <- sizeOfStack an'toClear+ let+ loopOnStack :: IO Bool+ loopOnStack = do+ k <- sizeOfStack an'stack -- int top = analyze_toclear.size();+ if 0 == k+ then return True+ else do -- assert(reason[var(analyze_stack.last())] != GClause_NULL);+ sl <- lastOfStack an'stack+ popFromStack an'stack -- analyze_stack.pop();+ c <- getNthClause reason (lit2var sl) -- getRoot sl+ nl <- sizeOfClause c+ let+ cvec = asVec c+ loopOnLit :: Int -> IO Bool -- loopOnLit (int i = 1; i < c.size(); i++){+ loopOnLit ((< nl) -> False) = loopOnStack+ loopOnLit i = do+ p' <- getNth cvec i -- valid range is [0 .. nl - 1]+ let v' = lit2var p'+ l' <- getNth level v'+ c1 <- (1 /=) <$> getNth an'seen v'+ if c1 && (0 /= l') -- if (!analyze_seen[var(p)] && level[var(p)] != 0){+ then do+ c3 <- (NullClause /=) <$> getNthClause reason v'+ if c3 && testBit minLevel (l' .&. 31) -- if (reason[var(p)] != GClause_NULL && ((1 << (level[var(p)] & 31)) & min_level) != 0){+ then do+ setNth an'seen v' 1 -- analyze_seen[var(p)] = 1;+ pushToStack an'stack p' -- analyze_stack.push(p);+ pushToStack an'toClear p' -- analyze_toclear.push(p);+ loopOnLit $ i + 1+ else do+ -- loopOnLit (int j = top; j < analyze_toclear.size(); j++) analyze_seen[var(analyze_toclear[j])] = 0;+ top' <- sizeOfStack an'toClear+ let vec = asVec an'toClear+ forM_ [top .. top' - 1] $ \j -> do x <- getNth vec j; setNth an'seen (lit2var x) 0+ -- analyze_toclear.shrink(analyze_toclear.size() - top); note: shrink n == repeat n pop+ shrinkStack an'toClear $ top' - top+ return False+ else loopOnLit $ i + 1+ loopOnLit 1+ loopOnStack++-- | #114+-- analyzeFinal : (confl : Clause *) (skip_first : boot) -> [void]+--+-- __Description:__+-- Specialized analysis proceduce to express the final conflict in terms of assumptions.+-- 'root_level' is allowed to point beyond end of trace (useful if called after conflict while+-- making assumptions). If 'skip_first' is TRUE, the first literal of 'confl' is ignored (needed+-- if conflict arose before search even started).+--+analyzeFinal :: Solver -> Clause -> Bool -> IO ()+analyzeFinal Solver{..} confl skipFirst = do+ clearStack conflict+ rl <- getInt rootLevel+ unless (rl == 0) $ do+ n <- sizeOfClause confl+ let+ lvec = asVec confl+ loopOnConfl :: Int -> IO ()+ loopOnConfl ((< n) -> False) = return ()+ loopOnConfl i = do+ (x :: Var) <- lit2var <$> getNth lvec i+ lvl <- getNth level x+ when (0 < lvl) $ setNth an'seen x 1+ loopOnConfl $ i + 1+ loopOnConfl $ if skipFirst then 1 else 0+ tls <- sizeOfStack trailLim+ trs <- sizeOfStack trail+ tlz <- getNth (asVec trailLim) 0+ let+ trailVec = asVec trail+ loopOnTrail :: Int -> IO ()+ loopOnTrail ((tlz <=) -> False) = return ()+ loopOnTrail i = do+ (l :: Lit) <- getNth trailVec i+ let (x :: Var) = lit2var l+ saw <- getNth an'seen x+ when (saw == 1) $ do+ (r :: Clause) <- getNthClause reason x+ if r == NullClause+ then pushToStack conflict (negateLit l)+ else do+ k <- sizeOfClause r+ let+ cvec = asVec r+ loopOnLits :: Int -> IO ()+ loopOnLits ((< k) -> False) = return ()+ loopOnLits j = do+ (v :: Var) <- lit2var <$> getNth cvec j+ lv <- getNth level v+ when (0 < lv) $ setNth an'seen v 1+ loopOnLits $ i + 1+ loopOnLits 1+ setNth an'seen x 0+ loopOnTrail $ i - 1+ loopOnTrail =<< if tls <= rl then return (trs - 1) else getNth (asVec trailLim) rl++-- | M114:+-- propagate : [void] -> [Clause+]+--+-- __Description:__+-- Porpagates all enqueued facts. If a conflict arises, the cornflicting clause is returned.+-- otherwise CRef_undef.+--+-- __Post-conditions:__+-- * the propagation queue is empty, even if there was a conflict.+--+-- memo: @propagate@ is invoked by @search@,`simpleDB` and `solve`+{-# INLINABLE propagate #-}+propagate :: Solver -> IO Clause+propagate s@Solver{..} = do+ -- myVal <- getNth stats (fromEnum NumOfBackjump)+ let+{-+ myVal = 0+ bumpAllVar :: IO () -- not in use+ bumpAllVar = do+ let+ loop :: Int -> IO ()+ loop ((<= nVars) -> False) = return ()+ loop i = do+ c <- getNth pr'seen i+ when (c == myVal) $ varBumpActivity s i+ loop $ i + 1+ loop 1+-}+ trailVec = asVec trail+ while :: Clause -> Bool -> IO Clause+ while confl False = {- bumpAllVar >> -} return confl+ while confl True = do+ (p :: Lit) <- getNth trailVec =<< getInt qHead+ modifyInt qHead (+ 1)+ let (ws :: ClauseExtManager) = getNthWatcher watches p+ end <- numberOfClauses ws+ cvec <- getClauseVector ws+ bvec <- getKeyVector ws+-- rc <- getNthClause reason $ lit2var p+-- byGlue <- if (rc /= NullClause) && learnt rc then (== 2) <$> getInt (lbd rc) else return False+ let+{-+ checkAllLiteralsIn :: Clause -> IO () -- not in use+ checkAllLiteralsIn c = do+ nc <- sizeOfClause c+ let+ vec = asVec c+ loop :: Int -> IO ()+ loop((< nc) -> False) = return ()+ loop i = do+ (v :: Var) <- lit2var <$> getNth vec i+ setNth pr'seen v myVal+ loop $ i + 1+ loop 0+-}+ forClause :: Clause -> Int -> Int -> IO Clause+ forClause confl i@((< end) -> False) j = do+ shrinkManager ws (i - j)+ while confl =<< ((<) <$> getInt qHead <*> sizeOfStack trail)+ forClause confl i j = do+ (l :: Lit) <- getNth bvec i+ bv <- if l == 0 then return lFalse else valueLit s l+ if bv == lTrue+ then do+ unless (i == j) $ do -- NOTE: if i == j, the path doesn't require accesses to cvec!+ (c :: Clause) <- getNthClause cvec i+ setNthClause cvec j c+ setNth bvec j l+ forClause confl (i + 1) (j + 1)+ else do+ -- checkAllLiteralsIn c+ (c :: Clause) <- getNthClause cvec i+ let+ lits = asVec c+ falseLit = negateLit p+ -- Make sure the false literal is data[1]+ ((falseLit ==) <$> getNth lits 0) >>= (`when` swapBetween lits 0 1)+ -- if 0th watch is true, then clause is already satisfied.+ (first :: Lit) <- getNth lits 0+ val <- valueLit s first+ if val == lTrue+ then setNthClause cvec j c >> setNth bvec j first >> forClause confl (i + 1) (j + 1)+ else do+ -- Look for new watch+ cs <- sizeOfClause c+ let+ forLit :: Int -> IO Clause+ forLit ((< cs) -> False) = do+ -- Did not find watch; clause is unit under assignment:+ setNthClause cvec j c+ setNth bvec j 0+ result <- enqueue s first c+ if not result+ then do+ ((== 0) <$> decisionLevel s) >>= (`when` setBool ok False)+ setInt qHead =<< sizeOfStack trail+ -- Copy the remaining watches:+ let+ copy i'@((< end) -> False) j' = forClause c i' j'+ copy i' j' = do+ setNthClause cvec j' =<< getNthClause cvec i'+ setNth bvec j' =<< getNth bvec i'+ copy (i' + 1) (j' + 1)+ copy (i + 1) (j + 1)+ else forClause confl (i + 1) (j + 1)+ forLit k = do+ (l :: Lit) <- getNth lits k+ lv <- valueLit s l+ if lv /= lFalse+ then do+ swapBetween lits 1 k+ pushClauseWithKey (getNthWatcher watches (negateLit l)) c l+ forClause confl (i + 1) j+ else forLit $ k + 1+ forLit 2+ forClause confl 0 0+ while NullClause =<< ((<) <$> getInt qHead <*> sizeOfStack trail)++-- | #M22+-- reduceDB: () -> [void]+--+-- __Description:__+-- Remove half of the learnt clauses, minus the clauses locked by the current assigmnent. Locked+-- clauses are clauses that are reason to some assignment. Binary clauses are never removed.+{-# INLINABLE reduceDB #-}+reduceDB :: Solver -> IO ()+reduceDB s@Solver{..} = do+ n <- nLearnts s+ vec <- getClauseVector learnts+ let+ loop :: Int -> IO ()+ loop ((< n) -> False) = return ()+ loop i = (removeWatch s =<< getNthClause vec i) >> loop (i + 1)+ k <- sortClauses s learnts (div n 2) -- k is the number of clauses not to be purged+ loop k -- CAVEAT: `vec` is a zero-based vector+ garbageCollect watches+ shrinkManager learnts (n - k)++-- | (Good to Bad) Quick sort the key vector based on their activities and returns number of privileged clauses.+-- this function uses the same metrix as reduceDB_lt in glucose 4.0:+-- 1. binary clause+-- 2. smaller lbd+-- 3. larger activity defined in MiniSat+-- , where smaller value is better.+--+-- they are coded into an Int as the following layout:+--+-- * 14 bit: LBD or 0 for preserved clauses+-- * 19 bit: converted activity+-- * remain: clauseVector index+--+(lbdWidth :: Int, activityWidth :: Int, indexWidth :: Int) = (l, a, w - (l + a + 1))+ where+ w = finiteBitSize (0:: Int)+ (l, a) = case () of+ _ | 64 <= w -> (16, 19) -- 28 bit => 256M clauses+ _ | 60 <= w -> (14, 19) -- 26 bit => 32M clauses+ _ | 32 <= w -> ( 7, 6) -- 18 bit => 256K clauses+ _ | 29 <= w -> ( 6, 5) -- 17 bit => 128K clauses+ _ -> error "Int on your CPU doesn't have sufficient bit width."++{-# INLINABLE sortClauses #-}+sortClauses :: Solver -> ClauseExtManager -> Int -> IO Int+sortClauses s cm nneeds = do+ -- constants+ let+ lbdMax :: Int+ lbdMax = 2 ^ lbdWidth - 1+ activityMax :: Int+ activityMax = 2 ^ activityWidth - 1+ activityScale :: Double+ activityScale = fromIntegral activityMax+ indexMax :: Int+ indexMax = (2 ^ indexWidth - 1) -- 67,108,863 for 26+ n <- numberOfClauses cm+ when (indexMax < n) $ error $ "## The number of learnt clauses " ++ show n ++ " exceeds mios's " ++ show indexWidth ++" bit manage capacity"+ vec <- getClauseVector cm+ keys <- getKeyVector cm+ -- 1: assign keys+ let+ assignKey :: Int -> Int -> IO Int+ assignKey ((< n) -> False) m = return m+ assignKey i m = do+ c <- getNthClause vec i+ k <- (\k -> if k == 2 then return k else fromEnum <$> getBool (protected c)) =<< sizeOfClause c+ case k of+ 1 -> setBool (protected c) False >> setNth keys i (shiftL 2 indexWidth + i) >> assignKey (i + 1) (m + 1)+ 2 -> setNth keys i (shiftL 1 indexWidth + i) >> assignKey (i + 1) (m + 1)+ _ -> do+ l <- locked s c -- this is expensive+ if l+ then setNth keys i (shiftL 1 indexWidth + i) >> assignKey (i + 1) (m + 1)+ else do+ d <- getInt $ lbd c+ b <- floor . (activityScale *) . (1 -) . logBase 1e100 . max 1 <$> getDouble (activity c)+ setNth keys i $ shiftL (min lbdMax d) (activityWidth + indexWidth) + shiftL b indexWidth + i+ assignKey (i + 1) m+ limit <- min n . (+ nneeds) <$> assignKey 0 0+ -- 2: sort keyVector+ let+ sortOnRange :: Int -> Int -> IO ()+ sortOnRange left right+ | limit < left = return ()+ | left >= right = return ()+ | left + 1 == right = do+ a <- getNth keys left+ b <- getNth keys right+ unless (a < b) $ swapBetween keys left right+ | otherwise = do+ let p = div (left + right) 2+ pivot <- getNth keys p+ swapBetween keys p left -- set a sentinel for r'+ let+ nextL :: Int -> IO Int+ nextL i@((<= right) -> False) = return i+ nextL i = do v <- getNth keys i; if v < pivot then nextL (i + 1) else return i+ nextR :: Int -> IO Int+ -- nextR i@((left <=) -> False) = return i+ nextR i = do v <- getNth keys i; if pivot < v then nextR (i - 1) else return i+ divide :: Int -> Int -> IO Int+ divide l r = do+ l' <- nextL l+ r' <- nextR r+ if l' < r' then swapBetween keys l' r' >> divide (l' + 1) (r' - 1) else return r'+ m <- divide (left + 1) right+ swapBetween keys left m+ sortOnRange left (m - 1)+ sortOnRange (m + 1) right+ sortOnRange 0 (n - 1)+ -- 3: place clauses+ let+ seek :: Int -> IO ()+ seek ((< limit) -> False) = return ()+ seek i = do+ bits <- getNth keys i+ when (indexMax < bits) $ do+ c <- getNthClause vec i+ let+ sweep k = do+ k' <- (indexMax .&.) <$> getNth keys k+ setNth keys k k+ if k' == i+ then setNthClause vec k c+ else getNthClause vec k' >>= setNthClause vec k >> sweep k'+ sweep i+ seek $ i + 1+ seek 0+ return limit++-- | #M22+--+-- 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.+--+{-# INLINABLE simplifyDB #-}+simplifyDB :: Solver -> IO Bool+simplifyDB s@Solver{..} = do+ good <- getBool ok+ if good+ then do+ p <- propagate s+ if p /= NullClause+ then setBool ok False >> return False+ else do+ -- Clear watcher lists:+ n <- sizeOfStack trail+ let+ vec = asVec trail+ loopOnLit ((< n) -> False) = return ()+ loopOnLit i = do+ l <- getNth vec i+ clearManager . getNthWatcher watches $ l+ clearManager . getNthWatcher watches $ negateLit l+ loopOnLit $ i + 1+ loopOnLit 0+ -- Remove satisfied clauses:+ let+ for :: Int -> IO Bool+ for ((< 2) -> False) = return True+ for t = do+ let ptr = if t == 0 then learnts else clauses+ vec' <- getClauseVector ptr+ n' <- numberOfClauses ptr+ let+ loopOnVector :: Int -> Int -> IO Bool+ loopOnVector ((< n') -> False) j = shrinkManager ptr (n' - j) >> return True+ loopOnVector i j = do+ c <- getNthClause vec' i+ l <- locked s c+ r <- simplify s c+ if not l && r+ then removeWatch s c >> loopOnVector (i + 1) j+ else setNthClause vec' j c >> loopOnVector (i + 1) (j + 1)+ loopOnVector 0 0+ ret <- for 0+ garbageCollect watches+ return ret+ else return False++-- | #M22+--+-- search : (nof_conflicts : int) (params : const SearchParams&) -> [lbool]+--+-- __Description:__+-- Search for a model the specified number of conflicts.+-- NOTE: Use negative value for 'nof_conflicts' indicate infinity.+--+-- __Output:__+-- 'l_True' if a partial assigment that is consistent with respect to the clause set is found. If+-- all variables are decision variables, that 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.+{-# INLINABLE search #-}+search :: Solver -> Int -> Int -> IO LiftedBool+search s@Solver{..} nOfConflicts nOfLearnts = do+ -- clear model+ let+ loop :: Int -> IO LiftedBool+ loop conflictC = do+ !confl <- propagate s+ d <- decisionLevel s+ if confl /= NullClause+ then do+ -- CONFLICT+ incrementStat s NumOfBackjump 1+ r <- getInt rootLevel+ if d == r+ then do+ -- Contradiction found:+ analyzeFinal s confl False+ return LFalse+ else do+-- u <- (== 0) . (flip mod 5000) <$> getNth stats (fromEnum NumOfBackjump)+-- when u $ do+-- d <- getDouble varDecay+-- when (d < 0.95) $ modifyDouble varDecay (+ 0.01)+ backtrackLevel <- analyze s confl -- 'analyze' resets litsLearnt by itself+ (s `cancelUntil`) . max backtrackLevel =<< getInt rootLevel+ newLearntClause s $ asSizedVec litsLearnt+ k <- sizeOfStack litsLearnt+ when (k == 1) $ do+ (v :: Var) <- lit2var <$> getNth (asVec litsLearnt) 0+ setNth level v 0+ varDecayActivity s+ claDecayActivity s+ loop $ conflictC + 1+ else do -- NO CONFLICT+ -- Simplify the set of problem clauses:+ when (d == 0) . void $ simplifyDB s -- our simplifier cannot return @False@ here+ k1 <- numberOfClauses learnts+ k2 <- nAssigns s+ when (k1 - k2 >= nOfLearnts) $ reduceDB s -- Reduce the set of learnt clauses+ case () of+ _ | k2 == nVars -> do+ -- Model found:+ forM_ [0 .. nVars - 1] $ \i -> setNthBool model i . (lTrue ==) =<< getNth assigns (i + 1)+ return LTrue+ _ | conflictC >= nOfConflicts -> do+ -- Reached bound on number of conflicts+ (s `cancelUntil`) =<< getInt rootLevel -- force a restart+ incrementStat s NumOfRestart 1+ return Bottom+ _ -> do+ -- New variable decision:+ v <- select s -- many have heuristic for polarity here+ -- << #phasesaving+ oldVal <- getNth phases v+ unsafeAssume s $ var2lit v (0 < oldVal) -- cannot return @False@+ -- >> #phasesaving+ loop conflictC+ good <- getBool ok+ if good then loop 0 else return LFalse++-- | __Fig. 16. (p.20)__+-- Main solve method.+--+-- __Pre-condition:__ If assumptions are used, 'simplifyDB' must be+-- called right before using this method. If not, a top-level conflict (resulting in a+-- non-usable internal state) cannot be distinguished from a conflict under assumptions.+solve :: (Foldable t) => Solver -> t Lit -> IO Bool+solve s@Solver{..} assumps = do+ -- PUSH INCREMENTAL ASSUMPTIONS:+ let+ injector :: Lit -> Bool -> IO Bool+ injector _ False = return False+ injector a True = do+ b <- assume s a+ if not b+ then do -- conflict analyze+ (confl :: Clause) <- getNthClause reason (lit2var a)+ analyzeFinal s confl True+ pushToStack conflict (negateLit a)+ cancelUntil s 0+ return False+ else do+ confl <- propagate s+ if confl /= NullClause+ then do+ analyzeFinal s confl True+ cancelUntil s 0+ return False+ else return True+ good <- simplifyDB s+ x <- if good then foldrM injector True assumps else return False+ if not x+ then return False+ else do+ setInt rootLevel =<< decisionLevel s+ -- SOLVE:+ nc <- fromIntegral <$> nClauses s+ let+ while :: Double -> Double -> IO Bool+ while nOfConflicts nOfLearnts = do+ status <- search s (floor nOfConflicts) (floor nOfLearnts)+ if status == Bottom+ then while (1.5 * nOfConflicts) (1.1 * nOfLearnts)+ else cancelUntil s 0 >> return (status == LTrue)+ while 100 (nc / 3.0)+++--+-- 'enqueue' is defined in 'Solver'; functions in M114 use 'unsafeEnqueue'+--+{-# INLINABLE unsafeEnqueue #-}+unsafeEnqueue :: Solver -> Lit -> Clause -> IO ()+unsafeEnqueue s@Solver{..} p from = do+ let v = lit2var p+ setNth assigns v $! if positiveLit p then lTrue else lFalse+ setNth level v =<< decisionLevel s+ setNthClause reason v from -- NOTE: @from@ might be NULL!+ pushToStack trail p++-- __Pre-condition:__ propagation queue is empty+{-# INLINE unsafeAssume #-}+unsafeAssume :: Solver -> Lit -> IO ()+unsafeAssume s@Solver{..} p = do+ pushToStack trailLim =<< sizeOfStack trail+ unsafeEnqueue s p NullClause++{-+-- | for debug+fromAssigns :: Vec -> IO [Int]+fromAssigns as = zipWith f [1 .. ] . tail <$> asList as+ where+ f n x+ | x == lTrue = n+ | x == lFalse = negate n+ | otherwise = 0++-- | for debug+dumpAssignment :: String -> Vec -> IO String+dumpAssignment mes v = (mes ++) . show <$> fromAssigns v+-}
+ SAT/Solver/Mios/OptionParser.hs view
@@ -0,0 +1,132 @@+{-# LANGUAGE Safe #-}+-- | command line option parser for mios+module SAT.Solver.Mios.OptionParser+ (+ MiosConfiguration (..)+ , defaultConfiguration+ , MiosProgramOption (..)+ , miosDefaultOption+ , miosOptions+ , miosUsage+ , miosParseOptions+ , miosParseOptionsFromArgs+ , toMiosConf+ )+ where++import System.Console.GetOpt (ArgDescr(..), ArgOrder(..), getOpt, OptDescr(..), usageInfo)+import System.Environment (getArgs)+import SAT.Solver.Mios.Internal (MiosConfiguration (..), defaultConfiguration)++-- | configuration swithces+data MiosProgramOption = MiosProgramOption+ {+ _targetFile :: Maybe String+ , _outputFile :: Maybe String+ , _confVariableDecayRate :: Double+ , _confClauseDecayRate :: Double+-- , _confRandomDecisionRate :: Int+ , _confCheckAnswer :: Bool+ , _confVerbose :: Bool+ , _confTimeProbe :: Bool+ , _confStatProbe :: Bool+ , _confNoAnswer :: Bool+ , _validateAssignment :: Bool+ , _displayHelp :: Bool+ , _displayVersion :: Bool+ }++-- | default option settings+miosDefaultOption :: MiosProgramOption+miosDefaultOption = MiosProgramOption+ {+ _targetFile = Just ""+ , _outputFile = Nothing+ , _confVariableDecayRate = variableDecayRate defaultConfiguration+ , _confClauseDecayRate = clauseDecayRate defaultConfiguration+-- , _confRandomDecisionRate = randomDecisionRate defaultConfiguration+ , _confCheckAnswer = False+ , _confVerbose = False+ , _confTimeProbe = False+ , _confStatProbe = collectStats defaultConfiguration+ , _confNoAnswer = False+ , _validateAssignment = False+ , _displayHelp = False+ , _displayVersion = False+ }++-- | definition of mios option+miosOptions :: [OptDescr (MiosProgramOption -> MiosProgramOption)]+miosOptions =+ [+ Option ['d'] ["variable-decay-rate"]+ (ReqArg (\v c -> c { _confVariableDecayRate = read v }) (show (_confVariableDecayRate miosDefaultOption)))+ "[solver] variable activity decay rate (0.0 - 1.0)"+ , Option ['c'] ["clause-decay-rate"]+ (ReqArg (\v c -> c { _confClauseDecayRate = read v }) (show (_confClauseDecayRate miosDefaultOption)))+ "[solver] clause activity decay rate (0.0 - 1.0)"+-- , Option ['r'] ["random-decision-rate"]+-- (ReqArg (\v c -> c { _confRandomDecisionRate = read v }) (show (_confRandomDecisionRate miosDefaultOption)))+-- "[solver] random selection rate (0 - 1000)"+ , Option [':'] ["validate-assignment"]+ (NoArg (\c -> c { _validateAssignment = True }))+ "[solver] read an assignment from STDIN and validate it"+ , Option [] ["validate"]+ (NoArg (\c -> c { _confCheckAnswer = True }))+ "[solver] self-check the (satisfied) answer"+ , Option ['o'] ["output"]+ (ReqArg (\v c -> c { _outputFile = Just v })"file")+ "[option] filename to store the result"+{-+ , Option [] ["stdin"]+ (NoArg (\c -> c { _targetFile = Nothing }))+ "[option] read a CNF from STDIN instead of a file"+-}+ , Option ['v'] ["verbose"]+ (NoArg (\c -> c { _confVerbose = True }))+ "[option] display misc information"+ , Option ['X'] ["hide-solution"]+ (NoArg (\c -> c { _confNoAnswer = True }))+ "[option] hide the solution"+ , Option [] ["time"]+ (NoArg (\c -> c { _confTimeProbe = True }))+ "[option] display execution time"+ , Option [] ["stat"]+ (NoArg (\c -> c { _confStatProbe = True }))+ "[option] display statistics information"+ , Option ['h'] ["help"]+ (NoArg (\c -> c { _displayHelp = True }))+ "[misc] display this help message"+ , Option [] ["version"]+ (NoArg (\c -> c { _displayVersion = True }))+ "[misc] display program ID"+ ]++-- | generates help message+miosUsage :: String -> String+miosUsage mes = usageInfo mes miosOptions++-- | builds "MiosProgramOption" from string given as command option+miosParseOptions :: String -> [String] -> IO MiosProgramOption+miosParseOptions mes argv =+ case getOpt Permute miosOptions argv of+ (o, [], []) -> do+ return $ foldl (flip id) miosDefaultOption o+ (o, (n:_), []) -> do+ let conf = foldl (flip id) miosDefaultOption o+ return $ conf { _targetFile = Just n }+ (_, _, errs) -> ioError (userError (concat errs ++ miosUsage mes))++-- | builds "MiosProgramOption" from a String+miosParseOptionsFromArgs :: String -> IO MiosProgramOption+miosParseOptionsFromArgs mes = miosParseOptions mes =<< getArgs++-- | converts "MiosProgramOption" into "SIHConfiguration"+toMiosConf :: MiosProgramOption -> MiosConfiguration+toMiosConf opts = MiosConfiguration+ {+ variableDecayRate = _confVariableDecayRate opts+ , clauseDecayRate = _confClauseDecayRate opts+-- , randomDecisionRate = _confRandomDecisionRate opts+ , collectStats = _confStatProbe opts+ }
+ SAT/Solver/Mios/Solver.hs view
@@ -0,0 +1,554 @@+-- | This is a part of MIOS+{-# LANGUAGE+ BangPatterns+ , RecordWildCards+ , ScopedTypeVariables+ , TupleSections+ , ViewPatterns+ #-}+{-# LANGUAGE Safe #-}++module SAT.Solver.Mios.Solver+ (+ -- * Solver+ Solver (..)+ , newSolver+ -- * Misc Accessors+ , nAssigns+ , nClauses+ , nLearnts+ , decisionLevel+ , valueVar+ , valueLit+ , locked+ , VarHeap+ -- * State Modifiers+ , addClause+ , enqueue+ , assume+ , cancelUntil+ , getModel+ -- * Activities+ , claBumpActivity+ , claDecayActivity+ , varBumpActivity+ , varDecayActivity+ -- * Stats+ , StatIndex (..)+ , incrementStat+ , getStats+ )+ where++import Control.Monad ((<=<), forM_, unless, when)+import SAT.Solver.Mios.Types+import SAT.Solver.Mios.Internal+import SAT.Solver.Mios.Clause+import SAT.Solver.Mios.ClauseManager++-- | __Fig. 2.(p.9)__ Internal State of the solver+data Solver = Solver+ {+ -- Public Interface+ model :: !VecBool -- ^ If found, this vector has the model+ , conflict :: !Stack -- ^ set of literals in the case of conflicts+ -- Clause Database+ , clauses :: !ClauseExtManager -- ^ List of problem constraints.+ , learnts :: !ClauseExtManager -- ^ List of learnt clauses.+ , watches :: !WatcherList -- ^ a list of constraint wathing 'p', literal-indexed+ -- Assignment Management+ , assigns :: !Vec -- ^ The current assignments indexed on variables; var-indexed+ , phases :: !Vec -- ^ The last assignments indexed on variables; var-indexed+ , trail :: !Stack -- ^ List of assignments in chronological order; var-indexed+ , trailLim :: !Stack -- ^ Separator indices for different decision levels in 'trail'.+ , qHead :: !IntSingleton -- ^ 'trail' is divided at qHead; assignments and queue+ , reason :: !ClauseVector -- ^ For each variable, the constraint that implied its value; var-indexed+ , level :: !Vec -- ^ For each variable, the decision level it was assigned; var-indexed+ -- Variable Order+ , activities :: !VecDouble -- ^ Heuristic measurement of the activity of a variable; var-indexed+ , order :: !VarHeap -- ^ Keeps track of the dynamic variable order.+ -- Configuration+ , config :: !MiosConfiguration -- ^ search paramerters+ , nVars :: !Int -- ^ number of variables+ , claInc :: !DoubleSingleton -- ^ Clause activity increment amount to bump with.+-- , varDecay :: !DoubleSingleton -- ^ used to set 'varInc'+ , varInc :: !DoubleSingleton -- ^ Variable activity increment amount to bump with.+ , rootLevel :: !IntSingleton -- ^ Separates incremental and search assumptions.+ -- Working Memory+ , ok :: !BoolSingleton -- ^ return value holder+ , an'seen :: !Vec -- ^ scratch var for 'analyze'; var-indexed+ , an'toClear :: !Stack -- ^ ditto+ , an'stack :: !Stack -- ^ ditto+ , pr'seen :: !Vec -- ^ used in propagate+ , lbd'seen :: !Vec -- ^ used in lbd computation+ , lbd'key :: !IntSingleton -- ^ used in lbd computation+ , litsLearnt :: !Stack -- ^ used to create a learnt clause+ , lastDL :: !Stack -- ^ last decision level used in analyze+ , stats :: !Vec -- ^ statistics information holder+ }++-- | returns an everything-is-initialized solver from the arguments+newSolver :: MiosConfiguration -> CNFDescription -> IO Solver+newSolver conf (CNFDescription nv nc _) = do+ Solver+ -- Public Interface+ <$> newVecBool nv False -- model+ <*> newStack nv -- coflict+ -- Clause Database+ <*> newManager nc -- clauses+ <*> newManager nc -- learnts+ <*> newWatcherList nv 2 -- watches+ -- Assignment Management+ <*> newVecWith (nv + 1) lBottom -- assigns+ <*> newVecWith (nv + 1) lBottom -- phases+ <*> newStack nv -- trail+ <*> newStack nv -- trailLim+ <*> newInt 0 -- qHead+ <*> newClauseVector (nv + 1) -- reason+ <*> newVecWith (nv + 1) (-1) -- level+ -- Variable Order+ <*> newVecDouble (nv + 1) 0 -- activities+ <*> newVarHeap nv -- order+ -- Configuration+ <*> return conf -- config+ <*> return nv -- nVars+ <*> newDouble 1.0 -- claInc+-- <*> newDouble (variableDecayRate conf) -- varDecay+ <*> newDouble 1.0 -- varInc+ <*> newInt 0 -- rootLevel+ -- Working Memory+ <*> newBool True -- ok+ <*> newVec (nv + 1) -- an'seen+ <*> newStack nv -- an'toClear+ <*> newStack nv -- an'stack+ <*> newVecWith (nv + 1) (-1) -- pr'seen+ <*> newVec nv -- lbd'seen+ <*> newInt 0 -- lbd'key+ <*> newStack nv -- litsLearnt+ <*> newStack nv -- lastDL+ <*> newVec (1 + fromEnum (maxBound :: StatIndex)) -- stats++--------------------------------------------------------------------------------+-- Accessors++-- | returns the number of current assigments+{-# INLINE nAssigns #-}+nAssigns :: Solver -> IO Int+nAssigns = sizeOfStack . trail++-- | returns the number of constraints (clauses)+{-# INLINE nClauses #-}+nClauses :: Solver -> IO Int+nClauses = numberOfClauses . clauses++-- | returns the number of learnt clauses+{-# INLINE nLearnts #-}+nLearnts :: Solver -> IO Int+nLearnts = numberOfClauses . learnts++-- | return the model as a list of literal+getModel :: Solver -> IO [Int]+getModel s = zipWith (\n b -> if b then n else negate n) [1 .. ] <$> asList (model s)++-- | returns the current decision level+{-# INLINE decisionLevel #-}+decisionLevel :: Solver -> IO Int+decisionLevel Solver{..} = sizeOfStack trailLim++-- | returns the assignment (:: 'LiftedBool' = @[-1, 0, -1]@) from 'Var'+{-# INLINE valueVar #-}+valueVar :: Solver -> Var -> IO Int+valueVar s !x = getNth (assigns s) x++-- | returns the assignment (:: 'LiftedBool' = @[-1, 0, -1]@) from 'Lit'+{-# INLINE valueLit #-}+valueLit :: Solver -> Lit -> IO Int -- FIXME: LiftedBool+valueLit Solver{..} !p = if positiveLit p then getNth assigns (lit2var p) else negate <$> getNth assigns (lit2var p)++-- | __Fig. 7. (p.11)__+-- returns @True@ if the clause is locked (used as a reason). __Learnt clauses only__+{-# INLINE locked #-}+locked :: Solver -> Clause -> IO Bool+locked Solver{..} c@Clause{..} = (c ==) <$> (getNthClause reason . lit2var =<< getNth lits 1)++-- | stats+data StatIndex =+ NumOfBackjump+ | NumOfRestart+ deriving (Bounded, Enum, Eq, Ord, Read, Show)++-- | increments a stat data corresponding to 'StatIndex'+incrementStat :: Solver -> StatIndex -> Int -> IO ()+incrementStat (config -> collectStats -> False) _ _ = return ()+incrementStat (stats -> v) (fromEnum -> i) k = modifyNth v (+ k) i++-- | returns the statistics as list+getStats :: Solver -> IO [(StatIndex, Int)]+getStats (config -> collectStats -> False) = return []+getStats (stats -> v) = mapM (\i -> (i, ) <$> getNth v (fromEnum i)) [minBound .. maxBound :: StatIndex]++-------------------------------------------------------------------------------- State Modifiers++-- | returns @False@ if a conflict has occured.+-- This function is called only before the solving phase to register the given clauses.+{-# INLINABLE addClause #-}+addClause :: Solver -> Vec -> IO Bool+addClause s@Solver{..} vecLits = do+ result <- clauseNew s vecLits False+ case result of+ (False, _) -> return False -- Conflict occured+ (True, c) -> do+ unless (c == NullClause) $ pushClause clauses c+ return True -- No conflict++-- | __Fig. 8. (p.12)__ create a new clause and adds it to watcher lists+-- Constructor function for clauses. Returns @False@ if top-level conflict is determined.+-- @outClause@ may be set to Null if the new clause is already satisfied under the current+-- top-level assignment.+--+-- __Post-condition:__ @ps@ is cleared. For learnt clauses, all+-- literals will be false except @lits[0]@ (this by design of the 'analyze' method).+-- For the propagation to work, the second watch must be put on the literal which will+-- first be unbound by backtracking. (Note that none of the learnt-clause specific things+-- needs to done for a user defined contraint type.)+{-# INLINABLE clauseNew #-}+clauseNew :: Solver -> Vec -> Bool -> IO (Bool, Clause)+clauseNew s@Solver{..} ps isLearnt = do+ -- now ps[0] is the number of living literals+ exit <- do+ let+ handle :: Int -> Int -> Int -> IO Bool+ handle j l n -- removes duplicates, but returns @True@ if this clause is satisfied+ | j > n = return False+ | otherwise = do+ y <- getNth ps j+ case () of+ _ | y == l -> do -- finds a duplicate+ swapBetween ps j n+ modifyNth ps (subtract 1) 0+ handle j l (n - 1)+ _ | - y == l -> setNth ps 0 0 >> return True -- p and negateLit p occurs in ps+ _ -> handle (j + 1) l n+ loopForLearnt :: Int -> IO Bool+ loopForLearnt i = do+ n <- getNth ps 0+ if n < i+ then return False+ else do+ l <- getNth ps i+ sat <- handle (i + 1) l n+ if sat+ then return True+ else loopForLearnt $ i + 1+ loop :: Int -> IO Bool+ loop i = do+ n <- getNth ps 0+ if n < i+ then return False+ else do+ l <- getNth ps i -- check the i-th literal's satisfiability+ sat <- valueLit s l -- any literal in ps is true+ case sat of+ 1 -> setNth ps 0 0 >> return True+ -1 -> do+ swapBetween ps i n+ modifyNth ps (subtract 1) 0+ loop i+ _ -> do+ sat' <- handle (i + 1) l n+ if sat'+ then return True+ else loop $ i + 1+ if isLearnt then loopForLearnt 1 else loop 1+ k <- getNth ps 0+ case k of+ 0 -> return (exit, NullClause)+ 1 -> do+ l <- getNth ps 1+ (, NullClause) <$> enqueue s l NullClause+ _ -> do+ -- allocate clause:+ c <- newClauseFromVec isLearnt ps+ let vec = asVec c+ when isLearnt $ do+ -- Pick a second literal to watch:+ let+ findMax :: Int -> Int -> Int -> IO Int+ findMax ((< k) -> False) j _ = return j+ findMax i j val = do+ v' <- lit2var <$> getNth vec i+ a <- getNth assigns v'+ b <- getNth level v'+ if (a /= lBottom) && (val < b)+ then findMax (i + 1) i b+ else findMax (i + 1) j val+ -- Let @max_i@ be the index of the literal with highest decision level+ max_i <- findMax 0 0 0+ swapBetween vec 1 max_i+ -- check literals occurences+ -- x <- asList c+ -- unless (length x == length (nub x)) $ error "new clause contains a element doubly"+ -- Bumping:+ claBumpActivity s c -- newly learnt clauses should be considered active+ forM_ [0 .. k -1] $ varBumpActivity s . lit2var <=< getNth vec -- variables in conflict clauses are bumped+ -- Add clause to watcher lists:+ l0 <- negateLit <$> getNth vec 0+ pushClauseWithKey (getNthWatcher watches l0) c 0+ l1 <- negateLit <$> getNth vec 1+ pushClauseWithKey (getNthWatcher watches l1) c 0+ return (True, c)++-- | __Fig. 9 (p.14)__+-- Puts a new fact on the propagation queue, as well as immediately updating the variable's value+-- in the assignment vector. If a conflict arises, @False@ is returned and the propagation queue is+-- cleared. The parameter 'from' contains a reference to the constraint from which 'p' was+-- propagated (defaults to @Nothing@ if omitted).+{-# INLINABLE enqueue #-}+enqueue :: Solver -> Lit -> Clause -> IO Bool+enqueue s@Solver{..} p from = do+ -- putStrLn . ("ssigns " ++) . show . map lit2int =<< asList trail+ -- putStrLn =<< dump ("enqueue " ++ show (lit2int p) ++ " ") from+ let signumP = if positiveLit p then lTrue else lFalse+ let v = lit2var p+ val <- valueVar s v+ if val /= lBottom+ then do -- Existing consistent assignment -- don't enqueue+ return $ val == signumP+ else do+ -- New fact, store it+ setNth assigns v $! signumP+ setNth level v =<< decisionLevel s+ setNthClause reason v from -- NOTE: @from@ might be NULL!+ pushToStack trail p+ return True++-- | __Fig. 12 (p.17)__+-- returns @False@ if immediate conflict.+--+-- __Pre-condition:__ propagation queue is empty+{-# INLINE assume #-}+assume :: Solver -> Lit -> IO Bool+assume s@Solver{..} p = do+ pushToStack trailLim =<< sizeOfStack trail+ enqueue s p NullClause++-- | #M22: Revert to the states at given level (keeping all assignment at 'level' but not beyond).+{-# INLINABLE cancelUntil #-}+cancelUntil :: Solver -> Int -> IO ()+cancelUntil s@Solver{..} lvl = do+ dl <- decisionLevel s+ when (lvl < dl) $ do+ let tr = asVec trail+ let tl = asVec trailLim+ lim <- getNth tl lvl+ ts <- sizeOfStack trail+ ls <- sizeOfStack trailLim+ let+ loopOnTrail :: Int -> IO ()+ loopOnTrail ((lim <=) -> False) = return ()+ loopOnTrail c = do+ x <- lit2var <$> getNth tr c+ setNth phases x =<< getNth assigns x+ setNth assigns x lBottom+ -- #reason to set reason Null+ -- if we don't clear @reason[x] :: Clause@ here, @reason[x]@ remains as locked.+ -- This means we can't reduce it from clause DB and affects the performance.+ setNthClause reason x NullClause -- 'analyze` uses reason without checking assigns+ -- FIXME: #polarity https://github.com/shnarazk/minisat/blosb/master/core/Solver.cc#L212+ undo s x+ -- insertHeap s x -- insertVerOrder+ loopOnTrail $ c - 1+ loopOnTrail $ ts - 1+ shrinkStack trail (ts - lim)+ shrinkStack trailLim (ls - lvl)+ setInt qHead =<< sizeOfStack trail++-------------------------------------------------------------------------------- VarOrder++-- | Interfate to select a decision var based on variable activity.+instance VarOrder Solver where+ -- | __Fig. 6. (p.10)__+ -- Creates a new SAT variable in the solver.+ newVar _ = return 0+ -- i <- nVars s+ -- Version 0.4:: push watches =<< newVec -- push'+ -- Version 0.4:: push watches =<< newVec -- push'+ -- push undos =<< newVec -- push'+ -- push reason NullClause -- push'+ -- push assigns lBottom+ -- push level (-1)+ -- push activities (0.0 :: Double)+ -- newVar order+ -- growQueueSized (i + 1) propQ+ -- return i+ {-# SPECIALIZE INLINE update :: Solver -> Var -> IO () #-}+ update = increaseHeap+ {-# SPECIALIZE INLINE undo :: Solver -> Var -> IO () #-}+ undo s v = inHeap s v >>= (`unless` insertHeap s v)+ {-# SPECIALIZE INLINE select :: Solver -> IO Var #-}+ select s = do+ let+ asg = assigns s+ -- | returns the most active var (heap-based implementation)+ loop :: IO Var+ loop = do+ n <- numElementsInHeap s+ if n == 0+ then return 0+ else do+ v <- getHeapRoot s+ x <- getNth asg v+ if x == lBottom then return v else loop+ loop++-------------------------------------------------------------------------------- Activities++-- | __Fig. 14 (p.19)__ Bumping of clause activity+{-# INLINE varBumpActivity #-}+varBumpActivity :: Solver -> Var -> IO ()+varBumpActivity s@Solver{..} !x = do+ !a <- (+) <$> getNthDouble x activities <*> getDouble varInc+ if 1e100 < a+ then varRescaleActivity s+ else setNthDouble x activities a+ update s x++-- | __Fig. 14 (p.19)__+{-# INLINE varDecayActivity #-}+varDecayActivity :: Solver -> IO ()+varDecayActivity Solver{..} = modifyDouble varInc (/ variableDecayRate config)+-- varDecayActivity Solver{..} = modifyDouble varInc . (flip (/)) =<< getDouble varDecay++-- | __Fig. 14 (p.19)__+{-# INLINE varRescaleActivity #-}+varRescaleActivity :: Solver -> IO ()+varRescaleActivity Solver{..} = do+ forM_ [1 .. nVars] $ \i -> modifyNthDouble i activities (* 1e-100)+ modifyDouble varInc (* 1e-100)++-- | __Fig. 14 (p.19)__+{-# INLINE claBumpActivity #-}+claBumpActivity :: Solver -> Clause -> IO ()+claBumpActivity s@Solver{..} Clause{..} = do+ a <- (+) <$> getDouble activity <*> getDouble claInc+ if 1e100 < a+ then claRescaleActivity s+ else setDouble activity a++-- | __Fig. 14 (p.19)__+{-# INLINE claDecayActivity #-}+claDecayActivity :: Solver -> IO ()+claDecayActivity Solver{..} = modifyDouble claInc (/ clauseDecayRate config)++-- | __Fig. 14 (p.19)__+{-# INLINE claRescaleActivity #-}+claRescaleActivity :: Solver -> IO ()+claRescaleActivity Solver{..} = do+ vec <- getClauseVector learnts+ n <- numberOfClauses learnts+ let+ loopOnVector :: Int -> IO ()+ loopOnVector ((< n) -> False) = return ()+ loopOnVector i = do+ c <- getNthClause vec i+ modifyDouble (activity c) (* 1e-20) -- not 1e-100+ loopOnVector $ i + 1+ loopOnVector 0+ modifyDouble claInc (* 1e-20) -- not 1e-100++-------------------------------------------------------------------------------- VarHeap++-- | 'VarHeap' is a heap tree built from two 'Vec'+-- This implementation is identical wtih that in Minisat-1.14+-- Note: the zero-th element of @heap@ is used for holding the number of elements+-- Note: VarHeap itself is not a @VarOrder@, because it requires a pointer to solver+data VarHeap = VarHeap+ {+ heap :: Vec -- order to var+ , idxs :: Vec -- var to order (index)+ }++newVarHeap :: Int -> IO VarHeap+newVarHeap n = VarHeap <$> newSizedVecIntFromList lst <*> newSizedVecIntFromList lst+ where+ lst = [1 .. n]++{-# INLINE numElementsInHeap #-}+numElementsInHeap :: Solver -> IO Int+numElementsInHeap (order -> heap -> h) = getNth h 0++{-# INLINE inHeap #-}+inHeap :: Solver -> Var -> IO Bool+inHeap (order -> idxs -> at) n = (/= 0) <$> getNth at n++{-# INLINE increaseHeap #-}+increaseHeap :: Solver -> Int -> IO ()+increaseHeap s@(order -> idxs -> at) n = inHeap s n >>= (`when` (percolateUp s =<< getNth at n))++{-# INLINABLE percolateUp #-}+percolateUp :: Solver -> Int -> IO ()+percolateUp Solver{..} start = do+ let VarHeap to at = order+ v <- getNth to start+ ac <- getNthDouble v activities+ let+ loop :: Int -> IO ()+ loop i = do+ let iP = div i 2 -- parent+ if iP == 0+ then setNth to i v >> setNth at v i -- end+ else do+ v' <- getNth to iP+ acP <- getNthDouble v' activities+ if ac > acP+ then setNth to i v' >> setNth at v' i >> loop iP -- loop+ else setNth to i v >> setNth at v i -- end+ loop start++{-# INLINABLE percolateDown #-}+percolateDown :: Solver -> Int -> IO ()+percolateDown Solver{..} start = do+ let (VarHeap to at) = order+ n <- getNth to 0+ v <- getNth to start+ ac <- getNthDouble v activities+ let+ loop :: Int -> IO ()+ loop i = do+ let iL = 2 * i -- left+ if iL <= n+ then do+ let iR = iL + 1 -- right+ l <- getNth to iL+ r <- getNth to iR+ acL <- getNthDouble l activities+ acR <- getNthDouble r activities+ let (ci, child, ac') = if iR <= n && acL < acR then (iR, r, acR) else (iL, l, acL)+ if ac' > ac+ then setNth to i child >> setNth at child i >> loop ci+ else setNth to i v >> setNth at v i -- end+ else setNth to i v >> setNth at v i -- end+ loop start++{-# INLINE insertHeap #-}+insertHeap :: Solver -> Var -> IO ()+insertHeap s@(order -> VarHeap to at) v = do+ n <- (1 +) <$> getNth to 0+ setNth at v n+ setNth to n v+ setNth to 0 n+ percolateUp s n++-- | renamed from 'getmin'+{-# INLINE getHeapRoot #-}+getHeapRoot :: Solver -> IO Int+getHeapRoot s@(order -> VarHeap to at) = do+ r <- getNth to 1+ l <- getNth to =<< getNth to 0 -- the last element's value+ setNth to 1 l+ setNth at l 1+ setNth at r 0+ modifyNth to (subtract 1) 0 -- pop+ n <- getNth to 0+ when (1 < n) $ percolateDown s 1+ return r
+ SAT/Solver/Mios/Types.hs view
@@ -0,0 +1,269 @@+-- | Basic data types used throughout mios.+{-# LANGUAGE+ BangPatterns+ , FlexibleContexts+ , FlexibleInstances+ , FunctionalDependencies+ , MultiParamTypeClasses+ #-}+{-# LANGUAGE Trustworthy #-}++module SAT.Solver.Mios.Types+ (+ -- Singleton+ module SAT.Solver.Mios.Data.Singleton+ -- Fixed Unboxed Mutable Int Vector+ , module SAT.Solver.Mios.Data.Vec+ -- Abstract interfaces+ , VectorFamily (..)+ -- * Variable+ , Var+ , bottomVar+ , int2var+ -- * Internal encoded Literal+ , Lit+ , lit2int+ , int2lit+ , bottomLit+ , newLit+ , positiveLit+ , lit2var+ , var2lit+ , negateLit+ -- * Assignment+ , LiftedBool (..)+ , lbool+ , lFalse+ , lTrue+ , lBottom+ , VarOrder (..)+ -- * CNF+ , CNFDescription (..)+ )+ where++import Control.Monad (forM)+import Data.Bits+import qualified Data.Vector.Unboxed.Mutable as UV+import SAT.Solver.Mios.Data.Singleton+import SAT.Solver.Mios.Data.Vec++-- | Public interface as /Container/+class VectorFamily s t | s -> t where+ -- * Size operations+ -- | erases all elements in it+ clear :: s -> IO ()+ clear = error "no default method for clear"+ -- * Debug+ -- | dump the contents+ dump :: Show t => String -> s -> IO String+ dump msg _ = error $ msg ++ ": no defalut method for dump"+ -- | get a raw data+ asVec :: s -> UV.IOVector Int+ asVec = error "asVector undefined"+ -- | converts into a list+ asList :: s -> IO [t]+ asList = error "asList undefined"+ {-# MINIMAL dump #-}++-- | provides 'clear' and 'size'+instance VectorFamily Vec Int where+ clear = error "Vec.clear"+ {-# SPECIALIZE INLINE asList :: Vec -> IO [Int] #-}+ asList v = forM [0 .. UV.length v - 1] $ UV.unsafeRead v+ dump str v = (str ++) . show <$> asList v+ {-# SPECIALIZE INLINE asVec :: Vec -> Vec #-}+ asVec = id++-- | represents "Var"+type Var = Int++-- | Special constant in 'Var' (p.7)+bottomVar :: Var+bottomVar = 0++-- | converts a usual Int as literal to an internal 'Var' presentation+--+-- >>> int2var 1+-- 1 -- the first literal is the first variable+-- >>> int2var 2+-- 2 -- literal @2@ is variable 2+-- >>> int2var (-2)+-- 2 -- literal @-2@ is corresponding to variable 2+--+{-# INLINE int2var #-}+int2var = abs++-- | The literal data has an 'index' method which converts the literal to+-- a "small" integer suitable for array indexing. The 'var' method returns+-- the underlying variable of the literal, and the 'sign' method if the literal+-- is signed (False for /x/ and True for /-x/).+type Lit = Int++-- | Special constant in 'Lit' (p.7)+bottomLit :: Lit+bottomLit = 0++-- | converts "Var" into 'Lit'+newLit :: Var -> Lit+newLit = error "newLit undefined"++-- | returns @True@ if the literal is positive+{-# INLINE positiveLit #-}+positiveLit :: Lit -> Bool+positiveLit = even++-- | negates literal+--+-- >>> negateLit 2+-- 3+-- >>> negateLit 3+-- 2+-- >>> negateLit 4+-- 5+-- >>> negateLit 5+-- 4+{-# INLINE negateLit #-}+negateLit :: Lit -> Lit+negateLit !l = complementBit l 0 -- if even l then l + 1 else l - 1++----------------------------------------+----------------- Var+----------------------------------------++-- | converts 'Lit' into 'Var'+--+-- >>> lit2var 2+-- 1+-- >>> lit2var 3+-- 1+-- >>> lit2var 4+-- 2+-- >>> lit2var 5+-- 2+{-# INLINE lit2var #-}+lit2var :: Lit -> Var+lit2var !n = shiftR n 1++-- | converts a 'Var' to the corresponing literal+--+-- >>> var2lit 1 True+-- 2+-- >>> var2lit 1 False+-- 3+-- >>> var2lit 2 True+-- 4+-- >>> var2lit 2 False+-- 5+{-# INLINE var2lit #-}+var2lit :: Var -> Bool -> Lit+var2lit !v True = shiftL v 1+var2lit !v _ = shiftL v 1 + 1++----------------------------------------+----------------- Int+----------------------------------------++-- | converts 'Int' into 'Lit' as @lit2int . int2lit == id@+--+-- >>> int2lit 1+-- 2+-- >>> int2lit (-1)+-- 3+-- >>> int2lit 2+-- 4+-- >>> int2lit (-2)+-- 5+--+{-# INLINE int2lit #-}+int2lit :: Int -> Lit+int2lit n+ | 0 < n = 2 * n+ | otherwise = -2 * n + 1++-- | converts `Lit' into 'Int' as @int2lit . lit2int == id@+--+-- >>> lit2int 2+-- 1+-- >>> lit2int 3+-- -1+-- >>> lit2int 4+-- 2+-- >>> lit2int 5+-- -2+{-# INLINE lit2int #-}+lit2int :: Lit -> Int+lit2int l = case divMod l 2 of+ (i, 0) -> i+ (i, _) -> - i++-- | Lifted Boolean domain (p.7) that extends 'Bool' with "⊥" means /undefined/+-- design note: _|_ should be null = 0; True literals are coded to even numbers. So it should be 2.+data LiftedBool = Bottom | LFalse | LTrue+ deriving (Bounded, Eq, Ord, Read, Show)++instance Enum LiftedBool where+ {-# SPECIALIZE INLINE toEnum :: Int -> LiftedBool #-}+ toEnum 1 = LTrue+ toEnum (-1) = LFalse+ toEnum _ = Bottom+ {-# SPECIALIZE INLINE fromEnum :: LiftedBool -> Int #-}+ fromEnum Bottom = 0+ fromEnum LFalse = 1+ fromEnum LTrue = 2++-- | converts 'Bool' into 'LBool'+{-# INLINE lbool #-}+lbool :: Bool -> LiftedBool+lbool True = LTrue+lbool False = LFalse++-- | A contant representing False+lFalse:: Int+lFalse = -1++-- | A constant representing True+lTrue :: Int+lTrue = 1++-- | A constant for "undefined"+lBottom :: Int+lBottom = 0++-- | Assisting ADT for the dynamic variable ordering of the solver.+-- The constructor takes references to the assignment vector and the activity+-- vector of the solver. The method 'select' will return the unassigned variable+-- with the highest activity.+class VarOrder o where+ -- | constructor+ newVarOrder :: (VectorFamily v1 Bool, VectorFamily v2 Double) => v1 -> v2 -> IO o+ newVarOrder _ _ = error "newVarOrder undefined"++ -- | Called when a new variable is created.+ newVar :: o -> IO Var+ newVar = error "newVar undefined"++ -- | Called when variable has increased in activity.+ update :: o -> Var -> IO ()+ update _ = error "update undefined"++ -- | Called when all variables have been assigned new activities.+ updateAll :: o -> IO ()+ updateAll = error "updateAll undefined"++ -- | Called when variable is unbound (may be selected again).+ undo :: o -> Var -> IO ()+ undo _ _ = error "undo undefined"++ -- | Called to select a new, unassigned variable.+ select :: o -> IO Var+ select = error "select undefined"++-- | misc information on CNF+data CNFDescription = CNFDescription+ {+ _numberOfVariables :: !Int -- ^ number of variables+ , _numberOfClauses :: !Int -- ^ number of clauses+ , _pathname :: Maybe FilePath -- ^ given filename+ }+ deriving (Eq, Ord, Show)
+ SAT/Solver/Mios/Validator.hs view
@@ -0,0 +1,47 @@+-- | validate an assignment+{-# LANGUAGE+ ViewPatterns+ #-}+{-# LANGUAGE Safe #-}+module SAT.Solver.Mios.Validator+ (+ validate+ )+ where++import Data.Foldable (toList)+import SAT.Solver.Mios.Types+import SAT.Solver.Mios.Clause+import SAT.Solver.Mios.ClauseManager+import SAT.Solver.Mios.Solver++-- | validates the assignment even if the implementation of 'Solver' is wrong; we re-implement some functions here.+validate :: Traversable t => Solver -> t Int -> IO Bool+validate s (toList -> map int2lit -> lst) = do+ assignment <- newVec $ 1 + nVars s+ vec <- getClauseVector (clauses s)+ nc <- numberOfClauses (clauses s)+ let+ inject :: Lit -> IO ()+ inject l = setNth assignment (lit2var l) $ if positiveLit l then lTrue else lFalse+ -- return True if the literal is satisfied under the assignment+ satisfied :: Lit -> IO Bool+ satisfied l+ | positiveLit l = (lTrue ==) <$> getNth assignment (lit2var l)+ | otherwise = (lFalse ==) <$> getNth assignment (lit2var l)+ -- return True is any literal in the given list+ satAny :: [Lit] -> IO Bool+ satAny [] = return False+ satAny (l:ls) = do+ sat' <- satisfied l+ if sat' then return True else satAny ls+ -- traverse all clauses in 'clauses'+ loopOnVector :: Int -> IO Bool+ loopOnVector ((< nc) -> False) = return True+ loopOnVector i = do+ c <- getNthClause vec i+ sat' <- satAny =<< asList c+ if sat' then loopOnVector (i + 1) else return False+ if null lst+ then error "validator got an empty assignment."+ else mapM_ inject lst >> loopOnVector 0
+ SAT/Util/BoolExp.hs view
@@ -0,0 +1,244 @@+{-# LANGUAGE BangPatterns, FlexibleInstances, ViewPatterns, UndecidableInstances #-}+{-# LANGUAGE Safe #-}++-- | Boolean Expression module to build CNF from arbitrary expressions+-- Tseitin translation: http://en.wikipedia.org/wiki/Tseitin_transformation+module SAT.Util.BoolExp+ (+ -- * Class & Type+ BoolComponent (..)+ , BoolForm (..)+ -- * Expression contructors+ , (-|-)+ , (-&-)+ , (-=-)+ , (-!-)+ , (->-)+ , neg+ -- * List Operation+ , disjunctionOf+ , (-|||-)+ , conjunctionOf+ , (-&&&-)+ -- * Convert function+ , asList+ , asList_+ , asLatex+ , asLatex_+ , numberOfVariables+ , numberOfClauses+ , tseitinBase+ )+ where++import Data.List (foldl', intercalate)++-- | the start index for the generated variables by Tseitin encoding+tseitinBase :: Int+tseitinBase = 1600000++data L = L Int++-- | class of objects that can be interpeted as a bool expression+class BoolComponent a where+ toBF :: a -> BoolForm -- lift to BoolForm++-- | CNF expression+data BoolForm = Cnf (Int, Int) [[Int]]+ deriving (Eq, Show)++instance BoolComponent Int where+ toBF a = Cnf (abs a, max tseitinBase (abs a)) [[a]]++instance BoolComponent L where+ toBF (L a) = Cnf (abs a, max tseitinBase (abs a)) [[a]]++instance BoolComponent [Char] where+ toBF (read -> a) = Cnf (abs a, max tseitinBase (abs a)) [[a]]++instance BoolComponent BoolForm where+ toBF = id++-- | returns the number of variables in the 'BoolForm'+numberOfVariables :: BoolForm -> Int+numberOfVariables (Cnf (a, b) _) = a + b - tseitinBase++-- | returns the number of clauses in the 'BoolForm'+numberOfClauses :: BoolForm -> Int+numberOfClauses (Cnf _ l) = length l++boolFormTrue = Cnf (-1, 1) []+boolFormFalse = Cnf (-1, -1) []++instance BoolComponent Bool where+ toBF True = boolFormTrue+ toBF False = boolFormFalse++isTrue :: BoolForm -> Bool+isTrue = (== boolFormTrue)++isFalse :: BoolForm -> Bool+isFalse = (== boolFormFalse)++-- | return a 'clause' list only if it contains some real clause (not a literal)+clausesOf :: BoolForm -> [[Int]]+clausesOf cnf@(Cnf _ [[]]) = []+clausesOf cnf@(Cnf _ [[x]]) = []+clausesOf cnf@(Cnf _ l) = l++maxRank :: BoolForm -> Int+maxRank (Cnf (n, _) _) = n++-- | returns the number of valiable used as the output of this expression.+-- and returns itself it the expression is a literal.+-- Otherwise the number is a integer larger than 'tseitinBase'.+-- Therefore @1 + max tseitinBase the-returned-value@ is the next literal variable for future.+tseitinNumber :: BoolForm -> Int+tseitinNumber (Cnf (m, n) [[x]]) = x+tseitinNumber (Cnf (_, n) _) = n++renumber :: Int -> BoolForm -> (BoolForm, Int)+renumber base (Cnf (m, n) l)+ | l == [] = (Cnf (m, n) l, 0)+ | tseitinBase < base = (Cnf (m, n') l', n')+ | otherwise = (Cnf (n', tseitinBase) l', n')+ where+ l' = map (map f) l+ n' = maximum $ map maximum l'+ offset = base - tseitinBase - 1+ f x = if abs x < tseitinBase then x else signum x * (abs x + offset)++instance Ord BoolForm where+ compare (Cnf _ a) (Cnf _ b) = compare a b++-- | disjunction constructor+--+-- >>> asList $ "3" -|- "4"+-- [[3,4,-5],[-3,5],[-4,5]]+--+-- >>> asList (("3" -|- "4") -|- "-1")+-- [[3,4,-5],[-3,5],[-4,5],[5,-1,-6],[-5,6],[1,6]]+--+(-|-) :: (BoolComponent a, BoolComponent b) => a -> b -> BoolForm+(toBF -> e1) -|- (toBF -> e2')+ | isTrue e1 || isTrue e2' = boolFormTrue+ | isFalse e1 && isFalse e2' = boolFormFalse+ | isFalse e1 = e2'+ | isFalse e2' = e1+ | otherwise = Cnf (m, c) $ clausesOf e1 ++ clausesOf e2 ++ [[a, b, - c], [- a, c], [- b, c]]+ where+ a = tseitinNumber e1+ (e2, b) = renumber (1 + max tseitinBase a) e2'+ m = max (maxRank e1) (maxRank e2)+ c = 1 + max tseitinBase (max a b)++-- | conjunction constructor+--+-- >>> asList $ "3" -&- "-2"+-- [[-3,2,4],[3,-4],[-2,-4]]+--+-- >>> asList $ "3" -|- ("1" -&- "2")+-- [[-1,-2,4],[1,-4],[2,-4],[3,4,-5],[-3,5],[-4,5]]+--+(-&-) :: (BoolComponent a, BoolComponent b) => a -> b -> BoolForm+(toBF -> e1) -&- (toBF -> e2')+ | isTrue e1 && isTrue e2' = boolFormTrue+ | isFalse e1 || isFalse e2' = boolFormFalse+ | isTrue e1 = e2'+ | isTrue e2' = e1+ | otherwise = Cnf (m, c) $ clausesOf e1 ++ clausesOf e2 ++ [[- a, - b, c], [a, - c], [b, - c]]+ where+ a = tseitinNumber e1+ (e2, b) = renumber (1 + max tseitinBase a) e2'+ m = max (maxRank e1) (maxRank e2)+ c = 1 + max tseitinBase (max a b)++-- | negate a form+--+-- >>> asList $ neg ("1" -|- "2")+-- [[1,2,-3],[-1,3],[-2,3],[-3,-4],[3,4]]+neg :: (BoolComponent a) => a -> BoolForm+neg (toBF -> e) =+ Cnf (m, c) $ clausesOf e ++ [[- a, - c], [a, c]]+ where+ a = tseitinNumber e+ m = maxRank e+ c = 1 + max tseitinBase a++-- | equal on BoolForm+(-=-) :: (BoolComponent a, BoolComponent b) => a -> b -> BoolForm+(toBF -> e1) -=- (toBF -> e2) = (e1 -&- e2) -|- (neg e1 -&- neg e2)++-- | negation on BoolForm+(-!-) :: (BoolComponent a, BoolComponent b) => a -> b -> BoolForm+(toBF -> e1) -!- (toBF -> e2) = (neg e1 -&- e2) -|- (e1 -&- neg e2)++-- | implication as a short cut+--+-- >>> asList ("1" ->- "2")+-- [[-1,-3],[1,3],[3,2,-4],[-3,4],[-2,4]]+(->-) :: (BoolComponent a, BoolComponent b) => a -> b -> BoolForm+(toBF -> a) ->- (toBF -> b) = (neg a) -|- b++-- | merge [BoolForm] by '(-|-)'+disjunctionOf :: [BoolForm] -> BoolForm+disjunctionOf [] = boolFormFalse+disjunctionOf (x:l) = foldl' (-|-) x l++-- | an alias of 'disjunctionOf'+(-|||-) = disjunctionOf++-- | merge [BoolForm] by '(-&-)'+conjunctionOf :: [BoolForm] -> BoolForm+conjunctionOf [] = boolFormTrue+conjunctionOf (x:l) = foldl' (-&-) x l++-- | an alias of 'conjunctionOf'+(-&&&-) = conjunctionOf++-- | converts a BoolForm to "[[Int]]"+asList_ :: BoolForm -> [[Int]]+asList_ cnf@(Cnf (m,_) _)+ | isTrue cnf = []+ | isFalse cnf = [[]]+ | otherwise = l'+ where+ (Cnf _ l', _) = renumber (m + 1) cnf++-- | converts a *satisfied* BoolForm to "[[Int]]"+asList :: BoolForm -> [[Int]]+asList cnf@(Cnf (m,n) l)+ | isTrue cnf = []+ | isFalse cnf = [[]]+ | n <= tseitinBase = l+ | otherwise = [m'] : l'+ where+ (Cnf (m', _) l', _) = renumber (m + 1) cnf++-- | make latex string from CNF, using 'asList_'+--+-- >>> asLatex $ "3" -|- "4"+-- "\\begin{displaymath}\n( x_{3} \\vee x_{4} )\n\\end{displaymath}\n"+--+asLatex_ :: BoolForm -> String+asLatex_ b = beg ++ s ++ end+ where+ beg = "\\begin{displaymath}\n"+ end = "\n\\end{displaymath}\n"+ s = intercalate " \\wedge " [ makeClause c | c <- asList_ b]+ makeClause c = "(" ++ intercalate "\\vee" [makeLiteral l | l <- c] ++ ")"+ makeLiteral l+ | 0 < l = " x_{" ++ show l ++ "} "+ | otherwise = " \\neg " ++ "x_{" ++ show (negate l) ++ "} "++-- | make latex string from CNF, using 'asList'+asLatex :: BoolForm -> String+asLatex b = beg ++ s ++ end+ where+ beg = "\\begin{displaymath}\n"+ end = "\n\\end{displaymath}\n"+ s = intercalate " \\wedge " [ makeClause c | c <- asList b]+ makeClause c = "(" ++ intercalate "\\vee" [makeLiteral l | l <- c] ++ ")"+ makeLiteral l+ | 0 < l = " x_{" ++ show l ++ "} "+ | otherwise = " \\neg " ++ "x_{" ++ show (negate l) ++ "} "
+ SAT/Util/CNFIO.hs view
@@ -0,0 +1,31 @@+{-# LANGUAGE Safe #-}++-- | Read/Write a CNF file only with ghc standard libraries+module SAT.Util.CNFIO+ (+ -- * Input+ fromFile+ , clauseListFromFile+ , fromMinisatOutput+ , clauseListFromMinisatOutput+ -- * Output+ , toFile+ , toCNFString+ , asCNFString+ , asCNFString_+ -- * Bool Operation+ , module SAT.Util.BoolExp+ )+ where+import SAT.Util.CNFIO.Reader+import SAT.Util.CNFIO.Writer+import SAT.Util.CNFIO.MinisatReader+import SAT.Util.BoolExp++-- | String from BoolFrom+asCNFString :: BoolForm -> String+asCNFString = toCNFString . asList++-- | String from BoolFrom+asCNFString_ :: BoolForm -> String+asCNFString_ = toCNFString . asList_
+ SAT/Util/CNFIO/MinisatReader.hs view
@@ -0,0 +1,73 @@+{-# LANGUAGE Safe #-}++-- | Read an output file of minisat+module SAT.Util.CNFIO.MinisatReader+ (+ -- * Interface+ fromMinisatOutput+ , clauseListFromMinisatOutput+ )+ where+-- import Control.Applicative ((<$>), (<*>), (<*), (*>))+import Data.Char+import Text.ParserCombinators.ReadP++-- parser+-- |parse a non-signed integer+{-# INLINE pint #-}+pint = do+ n <- munch isDigit+ return (read n :: Int)++{-# INLINE mint #-}+mint = do+ char '-'+ n <- munch isDigit+ return (- (read n::Int))++-- |parse a (signed) integer+{-# INLINE int #-}+int = mint <++ pint++-- |return integer list that terminates at zero+{-# INLINE seqNums #-}+seqNums = do+ skipSpaces+ x <- int+ skipSpaces+ if (x == 0) then return [] else (x :) <$> seqNums++-- |top level interface for parsing CNF+{-# INLINE parseMinisatOutput #-}+parseMinisatOutput :: ReadP ((Int, Int), [Int])+parseMinisatOutput = do+ string "SAT"+ skipSpaces+ l <- seqNums+ return ((length l,0), l)++-- |read a minisat output:+-- ((numbefOfVariables, 0), [Literal])+--+-- >>> fromFile "result"+-- ((3, 0), [1, -2, 3])+--+{-# INLINE fromMinisatOutput #-}+fromMinisatOutput :: FilePath -> IO (Maybe ((Int, Int), [Int]))+fromMinisatOutput f = do+ c <- readFile f+ case readP_to_S parseMinisatOutput c of+ [(a, _)] -> return $ Just a+ _ -> return Nothing++-- | return clauses as [[Int]] from 'file'+--+-- >>> clauseListFromMinisatOutput "result"+-- [1,-2,3]+--+clauseListFromMinisatOutput :: FilePath -> IO [Int]+clauseListFromMinisatOutput l = do+ res <- fromMinisatOutput l+ case res of+ Just p -> return (snd p)+ _ -> return []
+ SAT/Util/CNFIO/Reader.hs view
@@ -0,0 +1,130 @@+{-# LANGUAGE Safe #-}++-- | Read a CNF file without haskell-platform+module SAT.Util.CNFIO.Reader+ (+ -- * Interface+ fromFile+ , clauseListFromFile+ )+ where+import Control.Applicative ((<$>), (<*>), (<*), (*>))+import Data.Char+import Text.ParserCombinators.ReadP++-- parser+{-# INLINE newline #-}+newline = char '\n'++{-# INLINE digit #-}+digit = satisfy isDigit++{-# INLINE spaces #-}+spaces = munch (`elem` " \t")++{-# INLINE noneOf #-}+noneOf s = satisfy (`notElem` s)++-- |parse a non-signed integer+{-# INLINE pint #-}+pint = do+ n <- munch isDigit+ return (read n :: Int)++{-# INLINE mint #-}+mint = do+ char '-'+ n <- munch isDigit+ return (- (read n::Int))++-- |parse a (signed) integer+{-# INLINE int #-}+int = mint <++ pint++-- |Parse something like: p FORMAT VARIABLES CLAUSES+{-# INLINE problemLine #-}+problemLine = do+ char 'p'+ skipSpaces+ (string "cnf" <++ string "CNF")+ skipSpaces+ vars <- pint+ skipSpaces+ clas <- pint+ spaces+ newline+ return (vars, clas)++-- |Parse something like: c This in an example of a comment line.+{-# INLINE commentLines #-}+commentLines = do+ l <- look+ if (head l) == 'c'+ then do+ munch ('\n' /=)+ newline+ commentLines+ else return ()++_commentLines = do+ char 'c'+ munch ('\n' /=)+ newline+ l <- look+ if (head l) == 'c' then commentLines else return ()++-- |Parse the preamble part+{-# INLINE preambleCNF #-}+preambleCNF = do+ commentLines+ problemLine++-- |return integer list that terminates at zero+{-# INLINE seqNums #-}+seqNums = do+ skipSpaces+ x <- int+ skipSpaces+ if (x == 0) then return [] else (x :) <$> seqNums++-- |Parse something like: 1 -2 0 4 0 -3 0+{-# INLINE parseClauses #-}+parseClauses :: Int -> ReadP [[Int]]+parseClauses n = count n seqNums++-- |top level interface for parsing CNF+{-# INLINE parseCNF #-}+parseCNF :: ReadP ((Int, Int), [[Int]])+parseCNF = do+ a <- preambleCNF+ b <- parseClauses (snd a)+ return (a, b)++-- |driver:: String -> Either ParseError Int+driver input = readP_to_S (parseClauses 1) input++-- |read a CNF file and return:+-- ((numbefOfVariables, numberOfClauses), [Literal])+--+-- >>> fromFile "acnf"+-- ((3, 4), [[1, 2], [-2, 3], [-1, 2, -3], [3]]+--+{-# INLINE fromFile #-}+fromFile :: FilePath -> IO (Maybe ((Int, Int), [[Int]]))+fromFile f = do+ c <- readFile f+ case readP_to_S parseCNF c of+ [(a, _)] -> return $ Just a+ _ -> return Nothing++-- | return clauses as [[Int]] from 'file'+--+-- >>> clauseListFromFile "a.cnf"+-- [[1, 2], [-2, 3], [-1, 2, -3], [3]]+--+clauseListFromFile :: FilePath -> IO [[Int]]+clauseListFromFile l = do+ res <- fromFile l+ case res of+ Just (_, l) -> return l+ _ -> return []
+ SAT/Util/CNFIO/Writer.hs view
@@ -0,0 +1,58 @@+{-# LANGUAGE Safe #-}++-- | Write SAT data to CNF file+module SAT.Util.CNFIO.Writer+ (+ -- * Interface+ toFile+ , toCNFString+ , toString+ , toLatexString+ )+ where+import Data.List (intercalate, nub, sort)+import System.IO++-- | Write the CNF to file 'f', using 'toCNFString'+toFile :: FilePath -> [[Int]] -> IO ()+toFile f l = writeFile f $ toCNFString l++-- | Convert [Clause] to String, where Clause is [Int]+--+-- >>> toCNFString []+-- "p cnf 0 0\n"+--+-- >>> toCNFString [[-1, 2], [-3, -4]]+-- "p cnf 4 2\n-1 2 0\n-3 -4 0\n"+--+-- >>> toCNFString [[1], [-2], [-3, -4], [1,2,3,4]]+-- "p cnf 4 4\n1 0\n-2 0\n-3 -4 0\n1 2 3 4 0\n"+--+toCNFString :: [[Int]] -> String+toCNFString l = hdr ++ str+ where+ hdr = "p cnf " ++ show numV ++ " " ++ show numC ++ "\n"+ numC = length l+ numV = last $ nub $ sort $ map abs $ concat l+ str = concat [intercalate " " (map show c) ++ " 0\n" | c <- l]++-- | converts @[[Int]]@ to a String+toString :: [[Int]] -> String -> String -> String+toString l and' or' = intercalate a ["(" ++ intercalate o [ lit x | x <- c] ++ ")" | c <- l]+ where+ lit x+ | 0 <= x = "X" ++ show x+ | otherwise = "-X" ++ show (abs x)+ a = pad and'+ o = pad or'+ pad s = " " ++ s ++ " "++-- | converts @[[Int]]@ to a LaTeX expression+toLatexString :: [[Int]] -> String+toLatexString l = "\\begin{eqnarray*}\n" ++ intercalate a ["(" ++ intercalate o [ lit x | x <- c] ++ ")" | c <- l] ++ "\n\\end{eqnarray*}"+ where+ lit x+ | 0 <= x = "X_{" ++ show x ++ "}"+ | otherwise = "\\overline{X_{" ++ show (abs x) ++ "}}"+ a = " \n\\wedge "+ o = " \\vee "
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ app/mios.hs view
@@ -0,0 +1,20 @@+-- | Executable of 'Minisat Implementation and Optimization Study'+module Main+ (+ main+ )+ where++import SAT.Solver.Mios++-- | main+main :: IO ()+main = do+ opts <- miosParseOptionsFromArgs versionId+ case () of+ _ | _displayVersion opts -> putStrLn versionId+ _ | _displayHelp opts -> putStrLn $ miosUsage $ versionId ++ "\nUsage: mios [OPTIONS] target.cnf"+ _ | _targetFile opts == Just "" -> putStrLn $ miosUsage $ versionId ++ "\nUsage: mios [OPTIONS] target.cnf"+ _ | _validateAssignment opts -> executeValidator opts+ _ | otherwise -> executeSolver opts+
+ mios.cabal view
@@ -0,0 +1,89 @@+-- Initial mios.cabal generated by cabal init. For further documentation,+-- see http://haskell.org/cabal/users-guide/++name: mios+version: 1.2.1+synopsis: A Minisat-based SAT solver in Haskell+description:++ A modern and fast SAT solver written in Haskell, based on Minisat-1.14 and 2.2.+ By using CDCL, watch literals, VSIDS, restart, blocking-literals, LBD and so on,+ the current version is only 1.8 time slower than Minisat-1.14.+ "Mios" is an abbreviation of /Minisat-based Implementation and Optimization Study on SAT solver/.+ .++homepage: https://github.com/shnarazk/mios+license: GPL-3+license-file: LICENSE+author: Shuji Narazaki <narazaki@nagasaki-u.ac.jp>+maintainer: Shuji Narazaki <narazaki@nagasaki-u.ac.jp>+category: Artificial Intelligence, Constraint Solver+build-type: Simple+cabal-version: >=1.16++Flag llvm+ Description: Compile with llvm+ Default: False++library+ buildable: True+ default-language: Haskell2010+ default-extensions: Strict+ exposed-modules:+ SAT.Solver.Mios+ SAT.Solver.Mios.Clause+ SAT.Solver.Mios.ClauseManager+ SAT.Solver.Mios.Data.VecBool+ SAT.Solver.Mios.Data.VecDouble+ SAT.Solver.Mios.Data.Vec+ SAT.Solver.Mios.Data.Singleton+ SAT.Solver.Mios.Data.Stack+ SAT.Solver.Mios.Internal+ SAT.Solver.Mios.Glucose+ SAT.Solver.Mios.M114+ SAT.Solver.Mios.OptionParser+ SAT.Solver.Mios.Solver+ SAT.Solver.Mios.Types+ SAT.Solver.Mios.Validator+ SAT.Util.CNFIO+ SAT.Util.CNFIO.MinisatReader+ SAT.Util.CNFIO.Reader+ SAT.Util.CNFIO.Writer+ SAT.Util.BoolExp+ build-depends: base ==4.9.*, vector >=0.11, containers >=0.5, ghc-prim >=0.5, bytestring >=0.10, primitive >=0.6+ if flag(llvm)+ ghc-options: -ignore-asserts -funbox-strict-fields -fllvm -optlo-O3+ else+ ghc-options: -ignore-asserts -funbox-strict-fields -msse4.2++executable mios+ main-is: app/mios.hs+ buildable: True+ default-language: Haskell2010+ default-extensions: Strict+ build-depends: base ==4.9.*, vector >=0.11, containers >=0.5, ghc-prim >=0.5, bytestring >=0.10, primitive >=0.6+ if flag(llvm)+ ghc-options: -ignore-asserts -funbox-strict-fields -fllvm -optlo-O3+ else+ ghc-options: -ignore-asserts -funbox-strict-fields -msse4.2+ other-modules:+ SAT.Solver.Mios+ SAT.Solver.Mios.Clause+ SAT.Solver.Mios.ClauseManager+ SAT.Solver.Mios.Data.VecBool+ SAT.Solver.Mios.Data.VecDouble+ SAT.Solver.Mios.Data.Vec+ SAT.Solver.Mios.Data.Singleton+ SAT.Solver.Mios.Data.Stack+ SAT.Solver.Mios.Internal+ SAT.Solver.Mios.Glucose+ SAT.Solver.Mios.M114+ SAT.Solver.Mios.OptionParser+ SAT.Solver.Mios.Solver+ SAT.Solver.Mios.Types+ SAT.Solver.Mios.Validator+ SAT.Util.CNFIO+ SAT.Util.CNFIO.MinisatReader+ SAT.Util.CNFIO.Reader+ SAT.Util.CNFIO.Writer+ SAT.Util.BoolExp