diff --git a/Data/Unit.hs b/Data/Unit.hs new file mode 100644 --- /dev/null +++ b/Data/Unit.hs @@ -0,0 +1,29 @@ +{- | This module is used to express the fact that any tuple which is composed + only from empty tuples holds the same amount of information as an empty + tuple. -} +module Data.Unit where + +{- | The unit class expresses the fact that all tuples composed from only empty + tuples hold the same amount of information as the empty tuple and can thus + all be constructed by a call to 'unit'. -} +class Unit t where + -- | Constructs a unit type + unit :: t + +instance Unit () where + unit = () + +instance (Unit a,Unit b) => Unit (a,b) where + unit = (unit,unit) + +instance (Unit a,Unit b,Unit c) => Unit (a,b,c) where + unit = (unit,unit,unit) + +instance (Unit a,Unit b,Unit c,Unit d) => Unit (a,b,c,d) where + unit = (unit,unit,unit,unit) + +instance (Unit a,Unit b,Unit c,Unit d,Unit e) => Unit (a,b,c,d,e) where + unit = (unit,unit,unit,unit,unit) + +instance (Unit a,Unit b,Unit c,Unit d,Unit e,Unit f) => Unit (a,b,c,d,e,f) where + unit = (unit,unit,unit,unit,unit,unit) diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,674 @@ + GNU GENERAL PUBLIC LICENSE + Version 3, 29 June 2007 + + Copyright (C) 2007 Free Software Foundation, Inc. + 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. + + + Copyright (C) + + 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 . + +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: + + Copyright (C) + 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 +. + + 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 +. diff --git a/Language/SMTLib2.hs b/Language/SMTLib2.hs new file mode 100644 --- /dev/null +++ b/Language/SMTLib2.hs @@ -0,0 +1,116 @@ +{-# LANGUAGE OverloadedStrings,GADTs,FlexibleInstances,MultiParamTypeClasses,CPP #-} +{- | Example usage: This program tries to find two numbers greater than zero which sum up to 5. + + @ +import Language.SMTLib2 +import Language.SMTLib2.Solver + +program :: SMT (Integer,Integer) +program = do + x <- var + y <- var + assert $ (plus [x,y]) .==. (constant 5) + assert $ x .>. (constant 0) + assert $ y .>. (constant 0) + checkSat + vx <- getValue x + vy <- getValue y + return (vx,vy) + +main = withZ3 program >>= print + @ -} +module Language.SMTLib2 + (-- * Data types + SMT'(),SMT, + SMTBackend(),AnyBackend(..), + SMTType, + SMTAnnotation, + SMTValue, + SMTArith, + SMTOrd(..), + SMTExpr, + SMTFunction, + SMTOption(..), + SMTArray, + Constructor, + Field, + Args(..),LiftArgs(..), + -- * Environment + withSMTBackend,withSMTBackendExitCleanly, + setOption,getInfo,setLogic, + SMTInfo(..), + assert,push,pop,stack, + checkSat,checkSat',checkSatUsing,apply, + CheckSatResult(..), + CheckSatLimits(..),noLimits, + getValue,getValues,getModel, + comment, + getProof, + simplify, + -- ** Unsatisfiable Core + ClauseId(), + assertId, + getUnsatCore, + -- ** Interpolation + InterpolationGroup(), + interpolationGroup, + assertInterp, + getInterpolant, + -- * Expressions + var,varNamed,varNamedAnn,varAnn,argVars,argVarsAnn,argVarsAnnNamed, + untypedVar,untypedNamedVar, + constant,constantAnn, + extractAnnotation, + let',lets,letAnn, + named,named', + optimizeExpr,optimizeExpr', + foldExpr,foldExprM, + foldArgs,foldArgsM, + -- ** Basic logic + (.==.),argEq, + distinct, + ite, + (.&&.),(.||.),and',or',xor,not',not'',(.=>.), + forAll,exists, + forAllAnn,existsAnn, + forAllList,existsList, + -- ** Arithmetic + plus,minus,mult,div',mod',rem',neg,divide,toReal,toInt, + -- ** Arrays + select,store,arrayEquals,unmangleArray,asArray,constArray, + -- ** Bitvectors + bvand,bvor,bvxor,bvnot,bvneg, + bvadd,bvsub,bvmul,bvurem,bvsrem,bvudiv,bvsdiv, + bvule,bvult,bvuge,bvugt, + bvsle,bvslt,bvsge,bvsgt, + bvshl,bvlshr,bvashr, + BitVector(..), +#ifdef SMTLIB2_WITH_DATAKINDS + BVKind(..), +#else + BVTyped,BVUntyped, +#endif + BV8,BV16,BV32,BV64, + N0,N1,N2,N3,N4,N5,N6,N7,N8,N9,N10,N11,N12,N13,N14,N15,N16,N17,N18,N19,N20,N21,N22,N23,N24,N25,N26,N27,N28,N29,N30,N31,N32,N33,N34,N35,N36,N37,N38,N39,N40,N41,N42,N43,N44,N45,N46,N47,N48,N49,N50,N51,N52,N53,N54,N55,N56,N57,N58,N59,N60,N61,N62,N63,N64, + bvconcat,--bvextract,bvextractUnsafe, + bvsplitu16to8, + bvsplitu32to16,bvsplitu32to8, + bvsplitu64to32,bvsplitu64to16,bvsplitu64to8, + bvextract,bvextract', + -- ** Functions + funAnn,funAnnNamed,funAnnRet,fun,app,defFun,defConst,defConstNamed,defFunAnn,defFunAnnNamed,map', + -- ** Data types + is,(.#), + -- ** Lists + head',tail',insert',isNil,isInsert, + -- * Untyped expressions + Untyped,UntypedValue, + entype,entypeValue, + castUntypedExpr,castUntypedExprValue + ) + where + +import Language.SMTLib2.Internals +import Language.SMTLib2.Internals.Instances +import Language.SMTLib2.Internals.Optimize +import Language.SMTLib2.Internals.Interface diff --git a/Language/SMTLib2/Connection.hs b/Language/SMTLib2/Connection.hs new file mode 100644 --- /dev/null +++ b/Language/SMTLib2/Connection.hs @@ -0,0 +1,70 @@ +{- | This module can be used if the simple 'Language.SMTLib2.withSMTSolver'-interface isn't + sufficient, e.g. if you don't want to wrap your whole program into one big + 'Language.SMTLib2.MonadSMT' or you want to run multiple solvers side by side. -} +module Language.SMTLib2.Connection + (SMTConnection() + ,open + ,close + ,withConnection + ,performSMT + ,performSMTExitCleanly + ) where + +import Language.SMTLib2.Internals +import Control.Concurrent.MVar +import Control.Monad.State (runStateT) +import Control.Monad.Reader (runReaderT) +import Control.Monad.Trans (MonadIO,liftIO) +import Control.Exception +import Prelude (($),IO,return) + +-- | Represents a connection to an SMT solver. +-- The SMT solver runs in a seperate thread and communication is handled via handles. +data SMTConnection b = SMTConnection { backend :: b + , status :: MVar SMTState + } + +-- | Create a new connection to a SMT solver by spawning a shell command. +-- The solver must be able to read from stdin and write to stdout. +open :: (MonadIO m,SMTBackend b m) => b -- ^ The backend for the SMT solver. + -> m (SMTConnection b) +open solver = do + st <- liftIO $ newMVar emptySMTState + return (SMTConnection { backend = solver + , status = st + }) + +-- | Closes an open SMT connection. Do not use the connection afterwards. +close :: (MonadIO m,SMTBackend b m) => SMTConnection b -> m () +close conn = do + st <- liftIO $ takeMVar (status conn) + smtHandle (backend conn) st SMTExit + return () + +withConnection :: MonadIO m => SMTConnection b -> (b -> SMTState -> m (a,SMTState)) -> m a +withConnection conn f = do + st <- liftIO $ takeMVar (status conn) + (res,nst) <- f (backend conn) st + liftIO $ putMVar (status conn) nst + return res + +-- | Perform an action in the SMT solver associated with this connection and return the result. +performSMT :: (MonadIO m,SMTBackend b m) + => SMTConnection b -- ^ The connection to the SMT solver to use + -> SMT' m a -- ^ The action to perform + -> m a +performSMT conn act = withConnection conn (\b st -> runStateT (runReaderT (runSMT act) (AnyBackend b)) st) + +performSMTExitCleanly :: SMTBackend b IO + => SMTConnection b + -> SMT' IO a + -> IO a +performSMTExitCleanly conn act = do + st <- takeMVar (status conn) + catch (do + (res,nst) <- runStateT (runReaderT (runSMT act) (AnyBackend $ backend conn)) st + putMVar (status conn) nst + return res) + (\e -> do + smtHandle (backend conn) st SMTExit + throw (e :: SomeException)) diff --git a/Language/SMTLib2/Internals.hs b/Language/SMTLib2/Internals.hs new file mode 100644 --- /dev/null +++ b/Language/SMTLib2/Internals.hs @@ -0,0 +1,1167 @@ +{-# LANGUAGE OverloadedStrings,GADTs,FlexibleInstances,MultiParamTypeClasses,RankNTypes,DeriveDataTypeable,TypeSynonymInstances,TypeFamilies,FlexibleContexts,CPP,ScopedTypeVariables,GeneralizedNewtypeDeriving #-} +module Language.SMTLib2.Internals where + +import Language.SMTLib2.Internals.Operators +import Language.SMTLib2.Strategy + +import Control.Monad.Reader hiding (mapM,mapM_) +import Control.Monad.State hiding (mapM,mapM_) +import Data.Typeable +import Data.Map as Map hiding (assocs,foldl) +import Data.Ratio +import Data.Proxy +#ifdef SMTLIB2_WITH_CONSTRAINTS +import Data.Constraint +#endif +#ifdef SMTLIB2_WITH_DATAKINDS +import Data.Tagged +import Data.List as List (genericReplicate) +#endif +import Data.Fix +import Prelude hiding (mapM,mapM_,foldl,all,maximum) +import Data.Foldable +import Data.Traversable +import Control.Exception +import Data.Functor.Identity +import Data.Char (isDigit) + +-- Monad stuff +import Control.Applicative (Applicative(..)) +import Control.Monad.State.Lazy as Lazy (StateT) + +data SMTRequest response where + SMTSetLogic :: String -> SMTRequest () + SMTGetInfo :: SMTInfo i -> SMTRequest i + SMTSetOption :: SMTOption -> SMTRequest () + SMTAssert :: SMTExpr Bool -> Maybe InterpolationGroup -> Maybe ClauseId -> SMTRequest () + SMTCheckSat :: Maybe Tactic -> CheckSatLimits -> SMTRequest CheckSatResult + SMTDeclareDataTypes :: TypeCollection -> SMTRequest () + SMTDeclareSort :: String -> Integer -> SMTRequest () + SMTPush :: SMTRequest () + SMTPop :: SMTRequest () + SMTDefineFun :: SMTType res => FunInfo -> [FunInfo] -> SMTExpr res -> SMTRequest () + SMTDeclareFun :: FunInfo -> SMTRequest () + SMTGetValue :: SMTValue t => SMTExpr t -> SMTRequest t + SMTGetModel :: SMTRequest SMTModel + SMTGetProof :: SMTRequest (SMTExpr Bool) + SMTGetUnsatCore :: SMTRequest [ClauseId] + SMTSimplify :: SMTType t => SMTExpr t -> SMTRequest (SMTExpr t) + SMTGetInterpolant :: [InterpolationGroup] -> SMTRequest (SMTExpr Bool) + SMTComment :: String -> SMTRequest () + SMTExit :: SMTRequest () + SMTApply :: Tactic -> SMTRequest [SMTExpr Bool] + deriving Typeable + +data SMTModel = SMTModel { modelFunctions :: Map Integer (Integer,[ProxyArg],SMTExpr Untyped) + } deriving (Show,Typeable) + +-- | Describe limits on the ressources that an SMT-solver can use +data CheckSatLimits = CheckSatLimits { limitTime :: Maybe Integer -- ^ A limit on the amount of time the solver can spend on the problem (in milliseconds) + , limitMemory :: Maybe Integer -- ^ A limit on the amount of memory the solver can use (in megabytes) + } deriving (Show,Eq,Ord,Typeable) + +-- | The result of a check-sat query +data CheckSatResult + = Sat -- ^ The formula is satisfiable + | Unsat -- ^ The formula is unsatisfiable + | Unknown -- ^ The solver cannot determine the satisfiability of a formula + deriving (Show,Eq,Ord,Typeable) + +class Monad m => SMTBackend a m where + smtHandle :: Typeable response => a -> SMTState -> SMTRequest response -> m response + +-- | Haskell types which can be represented in SMT +class (Ord t,Typeable t, + Ord (SMTAnnotation t),Typeable (SMTAnnotation t),Show (SMTAnnotation t)) + => SMTType t where + type SMTAnnotation t + getSort :: t -> SMTAnnotation t -> Sort + asDataType :: t -> SMTAnnotation t -> Maybe (String,TypeCollection) + asDataType _ _ = Nothing + asValueType :: t -> SMTAnnotation t -> (forall v. SMTValue v => v -> SMTAnnotation v -> r) -> Maybe r + getProxyArgs :: t -> SMTAnnotation t -> [ProxyArg] + getProxyArgs _ _ = [] + additionalConstraints :: t -> SMTAnnotation t -> Maybe (SMTExpr t -> [SMTExpr Bool]) + additionalConstraints _ _ = Nothing + annotationFromSort :: t -> Sort -> SMTAnnotation t + defaultExpr :: SMTAnnotation t -> SMTExpr t + +data ArgumentSort' a = ArgumentSort Integer + | NormalSort (Sort' a) + +type ArgumentSort = Fix ArgumentSort' + +data Unmangling a = PrimitiveUnmangling (Value -> SMTAnnotation a -> Maybe a) + | ComplexUnmangling (forall m. Monad m => (forall b. SMTValue b => SMTExpr b -> SMTAnnotation b -> m b) -> SMTExpr a -> SMTAnnotation a -> m (Maybe a)) + +data Mangling a = PrimitiveMangling (a -> SMTAnnotation a -> Value) + | ComplexMangling (a -> SMTAnnotation a -> SMTExpr a) + +-- | Haskell values which can be represented as SMT constants +class (SMTType t,Show t) => SMTValue t where + unmangle :: Unmangling t + mangle :: Mangling t + +-- | A type class for all types which support arithmetic operations in SMT +class (SMTValue t,Num t) => SMTArith t + +-- | Lifts the 'Ord' class into SMT +class (SMTType t) => SMTOrd t where + (.<.) :: SMTExpr t -> SMTExpr t -> SMTExpr Bool + (.>=.) :: SMTExpr t -> SMTExpr t -> SMTExpr Bool + (.>.) :: SMTExpr t -> SMTExpr t -> SMTExpr Bool + (.<=.) :: SMTExpr t -> SMTExpr t -> SMTExpr Bool + +infix 4 .<., .<=., .>=., .>. + +-- | An array which maps indices of type /i/ to elements of type /v/. +data SMTArray (i :: *) (v :: *) = SMTArray deriving (Eq,Ord,Typeable) + +data FunInfo = forall arg r. (Args arg,SMTType r) => FunInfo { funInfoId :: Integer + , funInfoProxy :: Proxy (arg,r) + , funInfoArgAnn :: ArgAnnotation arg + , funInfoResAnn :: SMTAnnotation r + , funInfoName :: Maybe (String,Integer) + } + +data SMTState = SMTState { nextVar :: Integer + , nextInterpolationGroup :: Integer + , nextClauseId :: Integer + , allVars :: Map Integer FunInfo + , namedVars :: Map (String,Integer) Integer + , nameCount :: Map String Integer + , declaredDataTypes :: DataTypeInfo } + +data AnyBackend m = forall b. SMTBackend b m => AnyBackend b + +-- | The SMT monad used for communating with the SMT solver +data SMT' m a = SMT { runSMT :: ReaderT (AnyBackend m) (Lazy.StateT SMTState m) a } + +type SMT = SMT' IO + +instance Functor m => Functor (SMT' m) where + fmap f = SMT . fmap f . runSMT + +instance Monad m => Monad (SMT' m) where + return = SMT . return + m >>= f = SMT $ (runSMT m) >>= runSMT . f + +instance MonadIO m => MonadIO (SMT' m) where + liftIO = SMT . liftIO + +instance MonadFix m => MonadFix (SMT' m) where + mfix f = SMT $ mfix (runSMT . f) + +instance (Monad m,Functor m) => Applicative (SMT' m) where + pure = return + (<*>) = ap + +--askSMT :: Monad m => SMT' b m b +--askSMT = SMT ask + +smtBackend :: Monad m => (forall b. SMTBackend b m => b -> SMT' m a) -> SMT' m a +smtBackend f = SMT $ do + AnyBackend backend <- ask + runSMT $ f backend + +getSMT :: Monad m => SMT' m SMTState +getSMT = SMT get + +putSMT :: Monad m => SMTState -> SMT' m () +putSMT = SMT . put + +modifySMT :: Monad m => (SMTState -> SMTState) -> SMT' m () +modifySMT f = SMT $ modify f + +instance MonadTrans SMT' where + lift = SMT . lift . lift + +data Untyped = forall t. SMTType t => Untyped t deriving Typeable + +data UntypedValue = forall t. SMTValue t => UntypedValue t deriving Typeable + +instance Eq Untyped where + (Untyped x) == (Untyped y) = case cast y of + Just y' -> x==y' + Nothing -> False + +instance Ord Untyped where + compare (Untyped x) (Untyped y) = case compare (typeOf x) (typeOf y) of + EQ -> case cast y of + Just y' -> compare x y' + r -> r + +instance Eq UntypedValue where + (UntypedValue x) == (UntypedValue y) = case cast y of + Just y' -> x==y' + Nothing -> False + +instance Ord UntypedValue where + compare (UntypedValue x) (UntypedValue y) = case compare (typeOf x) (typeOf y) of + EQ -> case cast y of + Just y' -> compare x y' + r -> r + +instance Show UntypedValue where + showsPrec p (UntypedValue x) = showsPrec p x + +-- | An abstract SMT expression +data SMTExpr t where + Var :: SMTType t => Integer -> SMTAnnotation t -> SMTExpr t + QVar :: SMTType t => Integer -> Integer -> SMTAnnotation t -> SMTExpr t + Const :: SMTValue t => t -> SMTAnnotation t -> SMTExpr t + AsArray :: (Args arg,SMTType res) => SMTFunction arg res -> ArgAnnotation arg + -> SMTExpr (SMTArray arg res) + Forall :: Integer -> [ProxyArg] -> SMTExpr Bool -> SMTExpr Bool + Exists :: Integer -> [ProxyArg] -> SMTExpr Bool -> SMTExpr Bool + Let :: Integer -> [SMTExpr Untyped] -> SMTExpr b -> SMTExpr b + App :: (Args arg,SMTType res) => SMTFunction arg res -> arg -> SMTExpr res + Named :: SMTExpr a -> String -> Integer -> SMTExpr a + InternalObj :: (SMTType t,Typeable a,Ord a,Show a) => a -> SMTAnnotation t -> SMTExpr t + UntypedExpr :: SMTType t => SMTExpr t -> SMTExpr Untyped + UntypedExprValue :: SMTValue t => SMTExpr t -> SMTExpr UntypedValue + deriving Typeable + +data Sort' a = BoolSort + | IntSort + | RealSort + | BVSort { bvSortWidth :: Integer + , bvSortUntyped :: Bool } + | ArraySort [a] a + | NamedSort String [a] + deriving (Eq,Show,Functor,Foldable,Traversable) + +type Sort = Fix Sort' + +data Value = BoolValue Bool + | IntValue Integer + | RealValue (Ratio Integer) + | BVValue { bvValueWidth :: Integer + , bvValueValue :: Integer } + | ConstrValue String [Value] (Maybe (String,[Sort])) + deriving (Eq,Show) + +data SMTFunction arg res where + SMTEq :: SMTType a => SMTFunction [SMTExpr a] Bool + SMTMap :: (Liftable arg,SMTType res,Args i) => SMTFunction arg res -> SMTFunction (Lifted arg i) (SMTArray i res) + SMTFun :: (Args arg,SMTType res) => Integer -> SMTAnnotation res -> SMTFunction arg res + SMTBuiltIn :: (Liftable arg,SMTType res) => String -> SMTAnnotation res -> SMTFunction arg res + SMTOrd :: (SMTType a) => SMTOrdOp -> SMTFunction (SMTExpr a,SMTExpr a) Bool + SMTArith :: (SMTType a,Num a) => SMTArithOp -> SMTFunction [SMTExpr a] a + SMTMinus :: (SMTType a,Num a) => SMTFunction (SMTExpr a,SMTExpr a) a + SMTIntArith :: SMTIntArithOp -> SMTFunction (SMTExpr Integer,SMTExpr Integer) Integer + SMTDivide :: SMTFunction (SMTExpr Rational,SMTExpr Rational) Rational + SMTNeg :: (SMTType a,Num a) => SMTFunction (SMTExpr a) a + SMTAbs :: (SMTType a,Num a) => SMTFunction (SMTExpr a) a + SMTNot :: SMTFunction (SMTExpr Bool) Bool + SMTLogic :: SMTLogicOp -> SMTFunction [SMTExpr Bool] Bool + SMTDistinct :: SMTType a => SMTFunction [SMTExpr a] Bool + SMTToReal :: SMTFunction (SMTExpr Integer) Rational + SMTToInt :: SMTFunction (SMTExpr Rational) Integer + SMTITE :: SMTType a => SMTFunction (SMTExpr Bool,SMTExpr a,SMTExpr a) a + SMTBVComp :: IsBitVector a => SMTBVCompOp -> SMTFunction (SMTExpr (BitVector a),SMTExpr (BitVector a)) Bool + SMTBVBin :: IsBitVector a => SMTBVBinOp -> SMTFunction (SMTExpr (BitVector a),SMTExpr (BitVector a)) (BitVector a) + SMTBVUn :: IsBitVector a => SMTBVUnOp -> SMTFunction (SMTExpr (BitVector a)) (BitVector a) + SMTSelect :: (Liftable i,SMTType v) => SMTFunction (SMTExpr (SMTArray i v),i) v + SMTStore :: (Liftable i,SMTType v) => SMTFunction (SMTExpr (SMTArray i v),i,SMTExpr v) (SMTArray i v) + SMTConstArray :: (Args i,SMTType v) => ArgAnnotation i -> SMTFunction (SMTExpr v) (SMTArray i v) + SMTConcat :: (Concatable a b) => SMTFunction (SMTExpr (BitVector a),SMTExpr (BitVector b)) (BitVector (ConcatResult a b)) + SMTExtract :: (TypeableNat start,TypeableNat len, + Extractable from len') + => Proxy start -> Proxy len -> SMTFunction (SMTExpr (BitVector from)) (BitVector len') + SMTConstructor :: (Args arg,SMTType dt) => Constructor arg dt -> SMTFunction arg dt + SMTConTest :: (Args arg,SMTType dt) => Constructor arg dt -> SMTFunction (SMTExpr dt) Bool + SMTFieldSel :: (SMTType a,SMTType f) => Field a f -> SMTFunction (SMTExpr a) f + SMTDivisible :: Integer -> SMTFunction (SMTExpr Integer) Bool + deriving (Typeable) + +class (SMTValue (BitVector a)) => IsBitVector a where + getBVSize :: Proxy a -> SMTAnnotation (BitVector a) -> Integer + +class (IsBitVector a,IsBitVector b,IsBitVector (ConcatResult a b)) + => Concatable a b where + type ConcatResult a b + concatAnnotation :: a -> b + -> SMTAnnotation (BitVector a) + -> SMTAnnotation (BitVector b) + -> SMTAnnotation (BitVector (ConcatResult a b)) + +class (IsBitVector a,IsBitVector b) => Extractable a b where + extractAnn :: a -> b -> Integer -> SMTAnnotation (BitVector a) -> SMTAnnotation (BitVector b) + getExtractLen :: a -> b -> SMTAnnotation (BitVector b) -> Integer + +-- | Represents a constructor of a datatype /a/ +-- Can be obtained by using the template haskell extension module +data Constructor arg res = Constructor [ProxyArg] DataType Constr deriving (Typeable) + +-- | Represents a field of the datatype /a/ of the type /f/ +data Field a f = Field [ProxyArg] DataType Constr DataField deriving (Typeable) + +newtype InterpolationGroup = InterpolationGroup Integer deriving (Typeable,Eq,Ord,Show) + +-- | Identifies a clause in an unsatisfiable core +newtype ClauseId = ClauseId Integer deriving (Typeable,Eq,Ord,Show) + +-- | Options controling the behaviour of the SMT solver +data SMTOption + = PrintSuccess Bool -- ^ Whether or not to print \"success\" after each operation + | ProduceModels Bool -- ^ Produce a satisfying assignment after each successful checkSat + | ProduceProofs Bool -- ^ Produce a proof of unsatisfiability after each failed checkSat + | ProduceUnsatCores Bool -- ^ Enable the querying of unsatisfiable cores after a failed checkSat + | ProduceInterpolants Bool -- ^ Enable the generation of craig interpolants + deriving (Show,Eq,Ord) + +data SMTInfo i where + SMTSolverName :: SMTInfo String + SMTSolverVersion :: SMTInfo String + +-- | Instances of this class may be used as arguments for constructed functions and quantifiers. +class (Ord a,Typeable a,Show a, + Ord (ArgAnnotation a),Typeable (ArgAnnotation a),Show (ArgAnnotation a)) + => Args a where + type ArgAnnotation a + foldExprs :: Monad m => (forall t. SMTType t => s -> SMTExpr t -> SMTAnnotation t -> m (s,SMTExpr t)) + -> s -> a -> ArgAnnotation a -> m (s,a) + foldExprs f s x ann = do + (s',_,r) <- foldsExprs (\cs [(expr,_)] ann' -> do + (cs',cr) <- f cs expr ann' + return (cs',[cr],cr) + ) s [(x,())] ann + return (s',r) + foldsExprs :: Monad m => (forall t. SMTType t => s -> [(SMTExpr t,b)] -> SMTAnnotation t -> m (s,[SMTExpr t],SMTExpr t)) + -> s -> [(a,b)] -> ArgAnnotation a -> m (s,[a],a) + extractArgAnnotation :: a -> ArgAnnotation a + toArgs :: ArgAnnotation a -> [SMTExpr Untyped] -> Maybe (a,[SMTExpr Untyped]) + + fromArgs :: a -> [SMTExpr Untyped] + fromArgs arg = fst $ foldExprsId (\lst expr ann -> (lst++[UntypedExpr expr],expr) + ) [] arg (extractArgAnnotation arg) + getTypes :: a -> ArgAnnotation a -> [ProxyArg] + getArgAnnotation :: a -> [Sort] -> (ArgAnnotation a,[Sort]) + +getSorts :: Args a => a -> ArgAnnotation a -> [Sort] +getSorts u ann = fmap (\prx -> withProxyArg prx getSort) (getTypes u ann) + +instance Args () where + type ArgAnnotation () = () + foldExprs _ s _ _ = return (s,()) + foldsExprs _ s args _ = return (s,fmap (const ()) args,()) + extractArgAnnotation _ = () + toArgs _ x = Just ((),x) + fromArgs _ = [] + getTypes _ _ = [] + getArgAnnotation _ xs = ((),xs) + +foldExprsId :: Args a => (forall t. SMTType t => s -> SMTExpr t -> SMTAnnotation t -> (s,SMTExpr t)) + -> s -> a -> ArgAnnotation a -> (s,a) +foldExprsId f st arg ann = runIdentity $ foldExprs (\st' expr ann' -> return $ f st' expr ann') st arg ann + +foldsExprsId :: Args a => (forall t. SMTType t => s -> [(SMTExpr t,b)] -> SMTAnnotation t -> (s,[SMTExpr t],SMTExpr t)) + -> s -> [(a,b)] -> ArgAnnotation a -> (s,[a],a) +foldsExprsId f st exprs anns = runIdentity $ foldsExprs (\st' exprs' anns' -> return $ f st' exprs' anns' + ) st exprs anns + +class (Args a) => Liftable a where + type Lifted a i + getLiftedArgumentAnn :: a -> i -> ArgAnnotation a -> ArgAnnotation i -> ArgAnnotation (Lifted a i) + inferLiftedAnnotation :: a -> i -> ArgAnnotation (Lifted a i) -> (ArgAnnotation i,ArgAnnotation a) +#ifdef SMTLIB2_WITH_CONSTRAINTS + getConstraint :: Args i => p (a,i) -> Dict (Liftable (Lifted a i)) +#endif + +argSorts :: Args a => a -> ArgAnnotation a -> [Sort] +argSorts arg ann = Prelude.reverse res + where + (res,_) = foldExprsId (\tps e ann' -> ((getSort (getUndef e) ann'):tps,e)) [] arg ann + +unpackArgs :: Args a => (forall t. SMTType t => SMTExpr t -> SMTAnnotation t -> s -> (c,s)) -> a -> ArgAnnotation a -> s -> ([c],s) +unpackArgs f x ann i = fst $ foldExprsId (\(res,ci) e ann' -> let (p,ni) = f e ann' ci + in ((res++[p],ni),e) + ) ([],i) x ann + +-- | An extension of the `Args` class: Instances of this class can be represented as native haskell data types. +class Args a => LiftArgs a where + type Unpacked a + -- | Converts a haskell value into its SMT representation. + liftArgs :: Unpacked a -> ArgAnnotation a -> a + -- | Converts a SMT representation back into a haskell value. + unliftArgs :: Monad m => a -> (forall t. SMTValue t => SMTExpr t -> m t) -> m (Unpacked a) + +firstJust :: [Maybe a] -> Maybe a +firstJust [] = Nothing +firstJust ((Just x):_) = Just x +firstJust (Nothing:xs) = firstJust xs + +getUndef :: SMTExpr t -> t +getUndef _ = error "Don't evaluate the result of 'getUndef'" + +getFunUndef :: SMTFunction arg res -> (arg,res) +getFunUndef _ = (error "Don't evaluate the first result of 'getFunUndef'", + error "Don't evaluate the second result of 'getFunUndef'") + +getArrayUndef :: Args i => SMTExpr (SMTArray i v) -> (i,Unpacked i,v) +getArrayUndef _ = (undefined,undefined,undefined) + +withSMTBackendExitCleanly :: SMTBackend b IO => b -> SMT a -> IO a +withSMTBackendExitCleanly backend act + = bracket + (return backend) + (\backend -> smtHandle backend emptySMTState SMTExit) + (\backend -> withSMTBackend' (AnyBackend backend) False act) + +withSMTBackend :: SMTBackend b m => b -> SMT' m a -> m a +withSMTBackend backend act = withSMTBackend' (AnyBackend backend) True act + +emptySMTState :: SMTState +emptySMTState = SMTState { nextVar = 0 + , nextInterpolationGroup = 0 + , nextClauseId = 0 + , allVars = Map.empty + , namedVars = Map.empty + , nameCount = Map.empty + , declaredDataTypes = emptyDataTypeInfo + } + +withSMTBackend' :: AnyBackend m -> Bool -> SMT' m a -> m a +withSMTBackend' backend@(AnyBackend b) mustExit f = do + (res,st) <- runStateT (runReaderT (runSMT f) backend) emptySMTState + when mustExit (smtHandle b st SMTExit) + return res + +funInfoSort :: FunInfo -> Sort +funInfoSort (FunInfo { funInfoProxy = _::Proxy (a,t) + , funInfoResAnn = ann}) + = getSort (undefined::t) ann + +funInfoArgSorts :: FunInfo -> [Sort] +funInfoArgSorts (FunInfo { funInfoProxy = _::Proxy (a,t) + , funInfoArgAnn = ann }) + = getSorts (undefined::a) ann + +newVariableId :: (Monad m) => Maybe String -> (Integer -> Maybe Integer -> (r,FunInfo)) -> SMT' m r +newVariableId name f = do + st <- getSMT + let idx = nextVar st + (nc,st') = case name of + Nothing -> (Nothing,st) + Just name' -> let nc = Map.findWithDefault 0 name' (nameCount st) + in (Just nc,st { namedVars = Map.insert (name',nc) idx (namedVars st) + , nameCount = Map.insert name' (nc+1) (nameCount st) }) + (res,info) = f idx nc + putSMT $ st' { nextVar = succ idx + , allVars = Map.insert idx info (allVars st') } + return res + +newVariable :: (Monad m,SMTType t) => Maybe String -> SMTAnnotation t -> SMT' m (SMTExpr t,FunInfo) +newVariable name (ann::SMTAnnotation t) + = newVariableId name + (\idx nc -> let info = FunInfo { funInfoId = idx + , funInfoProxy = Proxy :: Proxy ((),t) + , funInfoArgAnn = () + , funInfoResAnn = ann + , funInfoName = case (name,nc) of + (Nothing,Nothing) -> Nothing + (Just name',Just nc') -> Just (name',nc') } + in ((Var idx ann::SMTExpr t,info),info)) + +newFunction :: (Monad m,Args arg,SMTType r) => Maybe String -> ArgAnnotation arg -> SMTAnnotation r -> SMT' m (SMTFunction arg r,FunInfo) +newFunction name (ann_arg::ArgAnnotation arg) (ann_res::SMTAnnotation r) + = newVariableId name + (\idx nc -> let info = FunInfo { funInfoId = idx + , funInfoProxy = Proxy :: Proxy (arg,r) + , funInfoArgAnn = ann_arg + , funInfoResAnn = ann_res + , funInfoName = case (name,nc) of + (Nothing,Nothing) -> Nothing + (Just name',Just nc') -> Just (name',nc') } + in ((SMTFun idx ann_res::SMTFunction arg r,info),info)) + +createArgs :: Args a => ArgAnnotation a -> Integer -> Map Integer FunInfo -> (a,[FunInfo],Integer,Map Integer FunInfo) +createArgs ann i mp + = let ((tps,ni,nmp),res) + = foldExprsId (\(tps',ci,mp') (_::SMTExpr t) ann' + -> let info = FunInfo { funInfoId = ci + , funInfoProxy = Proxy :: Proxy ((),t) + , funInfoArgAnn = () + , funInfoResAnn = ann' + , funInfoName = Nothing } + in ((tps'++[info],ci+1,Map.insert ci info mp'),Var ci ann') + ) ([],i,mp) (error "Evaluated the argument to createArgs") ann + in (res,tps,ni,nmp) + +createArgs' :: (Args a,Monad m) => ArgAnnotation a -> SMT' m (a,[FunInfo]) +createArgs' ann = do + (tps,res) <- foldExprs (\tps' (_::SMTExpr t) ann' -> do + (expr',info) <- newVariable Nothing ann' + return (tps'++[info],expr') + ) [] (error "Evaluated the argument to createArgs") ann + return (res,tps) + +nameVariable :: Monad m => Integer -> String -> SMT' m () +nameVariable var name = do + st <- getSMT + let c = Map.findWithDefault 0 name (nameCount st) + putSMT $ st { nameCount = Map.insert name (c+1) (nameCount st) } + +argsSignature :: Args a => a -> ArgAnnotation a -> [Sort] +argsSignature arg ann + = reverse $ fst $ + foldExprsId (\sigs e ann' -> ((getSort (getUndef e) ann'):sigs,e)) + [] arg ann + +{- +functionGetSignature :: (SMTFunction f) + => f + -> ArgAnnotation (SMTFunArg f) + -> SMTAnnotation (SMTFunRes f) + -> ([Sort],Sort) +functionGetSignature fun arg_ann res_ann + = let ~(uarg,ures) = getFunUndef fun + in (argsSignature uarg arg_ann,getSort ures res_ann)-} + +{- +getSortParser :: Monad m => SMT' m SortParser +getSortParser = do + st <- getSMT + return $ mconcat $ fmap (withDeclaredType (\u _ -> fromSort u)) (Map.elems $ declaredTyCons st) +-} + +argumentSortToSort :: Monad m => (Integer -> m Sort) -> ArgumentSort -> m Sort +argumentSortToSort f (Fix (ArgumentSort i)) = f i +argumentSortToSort f (Fix (NormalSort s)) = do + res <- mapM (argumentSortToSort f) s + return (Fix res) + +sortToArgumentSort :: Sort -> ArgumentSort +sortToArgumentSort (Fix s) = Fix (NormalSort (fmap sortToArgumentSort s)) + +declareType :: (Monad m,SMTType t) => t -> SMTAnnotation t -> SMT' m () +declareType (_::t) ann = do + st <- getSMT + let (colls,ndts) = getNewTypeCollections (Proxy::Proxy t) ann + (declaredDataTypes st) + nst = st { declaredDataTypes = ndts } + putSMT nst + smtBackend $ \backend -> mapM_ (\coll -> lift $ smtHandle backend nst (SMTDeclareDataTypes coll)) colls + +-- Data type info + +data DataTypeInfo = DataTypeInfo { structures :: [TypeCollection] + , datatypes :: Map String (DataType,TypeCollection) + , constructors :: Map String (Constr,DataType,TypeCollection) + , fields :: Map String (DataField,Constr,DataType,TypeCollection) } + +data TypeCollection = TypeCollection { argCount :: Integer + , dataTypes :: [DataType] + } + +data ProxyArg = forall t. SMTType t => ProxyArg t (SMTAnnotation t) deriving Typeable + +data ProxyArgValue = forall t. SMTValue t => ProxyArgValue t (SMTAnnotation t) deriving Typeable + +withProxyArg :: ProxyArg -> (forall t. SMTType t => t -> SMTAnnotation t -> a) -> a +withProxyArg (ProxyArg x ann) f = f x ann + +withProxyArgValue :: ProxyArgValue -> (forall t. SMTValue t => t -> SMTAnnotation t -> a) -> a +withProxyArgValue (ProxyArgValue x ann) f = f x ann + +instance Show ProxyArg where + showsPrec p (ProxyArg u ann) = showParen (p>10) $ + showString "ProxyArg " . + showsPrec 11 (typeOf u) . + showChar ' ' . + showsPrec 11 ann + +instance Eq ProxyArg where + (ProxyArg (u1::t) ann1) == (ProxyArg u2 ann2) = case cast (u2,ann2) of + Just (_::t,ann2') -> ann1==ann2' + Nothing -> False + +instance Ord ProxyArg where + compare (ProxyArg u1 ann1) (ProxyArg u2 ann2) = case compare (typeOf u1) (typeOf u2) of + EQ -> case cast ann2 of + Just ann2' -> compare ann1 ann2' + x -> x + +instance Show ProxyArgValue where + showsPrec p (ProxyArgValue u ann) = showParen (p>10) $ + showString "ProxyArg " . + showsPrec 11 (typeOf u) . + showChar ' ' . + showsPrec 11 ann + +instance Eq ProxyArgValue where + (ProxyArgValue (u1::t) ann1) == (ProxyArgValue u2 ann2) = case cast (u2,ann2) of + Just (_::t,ann2') -> ann1==ann2' + Nothing -> False + +instance Ord ProxyArgValue where + compare (ProxyArgValue u1 ann1) (ProxyArgValue u2 ann2) = case compare (typeOf u1) (typeOf u2) of + EQ -> case cast ann2 of + Just ann2' -> compare ann1 ann2' + x -> x + +data AnyValue = forall t. SMTType t => AnyValue [ProxyArg] t (SMTAnnotation t) + +withAnyValue :: AnyValue -> (forall t. SMTType t => [ProxyArg] -> t -> SMTAnnotation t -> a) -> a +withAnyValue (AnyValue p x ann) f = f p x ann + +castAnyValue :: SMTType t => AnyValue -> Maybe (t,SMTAnnotation t) +castAnyValue (AnyValue _ x ann) = cast (x,ann) + +data DataType = DataType { dataTypeName :: String + , dataTypeConstructors :: [Constr] + , dataTypeGetUndefined + :: forall r. [ProxyArg] + -> (forall t. SMTType t => t -> SMTAnnotation t -> r) + -> r + } + +data Constr = Constr { conName :: String + , conFields :: [DataField] + , construct :: forall r. [Maybe ProxyArg] -> [AnyValue] + -> (forall t. SMTType t => [ProxyArg] -> t -> SMTAnnotation t -> r) + -> r + , conTest :: forall t. SMTType t => [ProxyArg] -> t -> Bool + } + +data DataField = DataField { fieldName :: String + , fieldSort :: ArgumentSort + , fieldGet :: forall r t. SMTType t => [ProxyArg] -> t + -> (forall f. SMTType f => f -> SMTAnnotation f -> r) + -> r + } + +emptyDataTypeInfo :: DataTypeInfo +emptyDataTypeInfo = DataTypeInfo { structures = [] + , datatypes = Map.empty + , constructors = Map.empty + , fields = Map.empty } + +containsTypeCollection :: TypeCollection -> DataTypeInfo -> Bool +containsTypeCollection struct dts = case dataTypes struct of + dt:_ -> Map.member (dataTypeName dt) (datatypes dts) + [] -> False + +addDataTypeStructure :: TypeCollection -> DataTypeInfo -> DataTypeInfo +addDataTypeStructure struct dts + = foldl (\cdts dt + -> foldl (\cdts con + -> foldl (\cdts field + -> cdts { fields = Map.insert (fieldName field) (field,con,dt,struct) (fields cdts) } + ) (cdts { constructors = Map.insert (conName con) (con,dt,struct) (constructors cdts) }) + (conFields con) + ) (cdts { datatypes = Map.insert (dataTypeName dt) (dt,struct) (datatypes cdts) }) + (dataTypeConstructors dt) + ) (dts { structures = struct:(structures dts) }) (dataTypes struct) + +-- | Get all the type collections which are not yet declared from a type. +getNewTypeCollections :: SMTType t => Proxy t -> SMTAnnotation t -> DataTypeInfo + -> ([TypeCollection],DataTypeInfo) +getNewTypeCollections (_::Proxy t) ann dts + = case asDataType (undefined::t) ann of + Nothing -> ([],dts) -- This is no declarable data type + Just (name,coll) + -> let isKnown = Map.member name (datatypes dts) -- Is the datatype already known? + proxies = getProxyArgs (undefined::t) ann + (tps1,dts1) = if isKnown + then ([],dts) + else ([coll],addDataTypeStructure coll dts) + (tps2,dts2) = foldl (\(tps,dts) prx -- Check all the data type parameters + -> withProxyArg prx $ + \(_::a) ann' + -> let (ntps,ndts) = getNewTypeCollections + (Proxy::Proxy a) + ann' dts + in (ntps++tps,ndts) + ) ([],dts1) proxies + (tps3,dts3) = if isKnown + then ([],dts2) + else foldl + (\cur dt + -> dataTypeGetUndefined dt proxies $ + \dtUndef dtAnn + -> foldl + (\cur con + -> foldl + (\(tps,dts) field + -> fieldGet field proxies dtUndef $ + \(_::f) fAnn + -> let (ntps,ndts) = getNewTypeCollections + (Proxy::Proxy f) + fAnn dts + in (ntps++tps,ndts) + ) cur (conFields con) + ) cur (dataTypeConstructors dt) + ) ([],dts2) (dataTypes coll) -- Declare all field types + in (tps2++tps3++tps1,dts3) + +asNamedSort :: Sort -> Maybe (String,[Sort]) +asNamedSort (Fix (NamedSort name args)) = Just (name,args) +asNamedSort _ = Nothing + +escapeName :: Either (String,Integer) Integer -> String +escapeName (Right i) = "var"++(if i==0 + then "" + else "_"++show i) +escapeName (Left (c:cs,nc)) + = (if isDigit c + then "num"++escapeName' (c:cs) + else escapeName' (c:cs))++(if nc==0 + then "" + else "_"++show nc) +escapeName (Left ([],0)) = "no_name" +escapeName (Left ([],n)) = "no_name"++show n + +escapeName' :: String -> String +escapeName' [] = [] +escapeName' ('_':xs) = '_':'_':escapeName' xs +escapeName' (x:xs) = x:escapeName' xs + +unescapeName :: String -> Maybe (Either (String,Integer) Integer) +unescapeName "var" = Just (Right 0) +unescapeName ('v':'a':'r':'_':rest) = if all isDigit rest + then Just (Right (read rest)) + else Nothing +unescapeName xs = do + res <- unescapeName' xs + return $ Left res + +unescapeName' :: String -> Maybe (String,Integer) +unescapeName' ('n':'o':'_':'n':'a':'m':'e':rest) = case rest of + [] -> Just ("",0) + xs -> if all isDigit xs + then Just ("",read xs) + else Nothing +unescapeName' ('_':'_':rest) = do + (name,nc) <- unescapeName' rest + return ('_':name,nc) +unescapeName' ('_':rest) = if all isDigit rest + then return ("",read rest) + else Nothing +unescapeName' (x:xs) = do + (name,nc) <- unescapeName' xs + return (x:name,nc) +unescapeName' "" = Just ("",0) + +-- BitVectors + +#ifdef SMTLIB2_WITH_DATAKINDS +data Nat = Z | S Nat deriving Typeable + +data BVKind = BVUntyped + | BVTyped Nat + +class TypeableNat n where + typeOfNat :: Proxy n -> TypeRep + typeOfNat p = Prelude.foldl + (\c _ -> mkTyConApp (mkTyCon3 "smtlib2" "Language.SMTLib2.Internals" "'S") [c]) + (mkTyConApp (mkTyCon3 "smtlib2" "Language.SMTLib2.Internals" "'Z") []) + (genericReplicate (reflectNat p 0) ()) + reflectNat :: Proxy n -> Integer -> Integer + +instance TypeableNat Z where + typeOfNat _ = mkTyConApp + (mkTyCon3 "smtlib2" "Language.SMTLib2.Internals" "'Z") + [] + reflectNat _ x = x + +instance TypeableNat n => TypeableNat (S n) where + typeOfNat _ = mkTyConApp + (mkTyCon3 "smtlib2" "Language.SMTLib2.Internals" "'S") + [typeOfNat (Proxy::Proxy n)] + reflectNat _ x = reflectNat (Proxy::Proxy n) (x+1) + +class TypeableBVKind n where + typeOfBVKind :: Proxy n -> TypeRep + +instance TypeableBVKind BVUntyped where + typeOfBVKind _ = mkTyConApp + (mkTyCon3 "smtlib2" "Language.SMTLib2.Internals" "'BVUntyped") + [] + +instance TypeableNat n => TypeableBVKind (BVTyped n) where + typeOfBVKind _ = mkTyConApp + (mkTyCon3 "smtlib2" "Language.SMTLib2.Internals" "'BVTyped") + [typeOfNat (Proxy::Proxy n)] + +type family Add (n1 :: Nat) (n2 :: Nat) :: Nat +type instance Add Z n = n +type instance Add (S n1) n2 = S (Add n1 n2) + +reifySum :: (Num a,Ord a) => a -> a -> (forall n1 n2. (TypeableNat n1,TypeableNat n2,TypeableNat (Add n1 n2)) + => Proxy (n1::Nat) -> Proxy (n2::Nat) -> Proxy (Add n1 n2) -> r) -> r +reifySum n1 n2 f + | n1 < 0 || n2 < 0 = error "smtlib2: Cann only reify numbers >= 0." + | otherwise = reifySum' n1 n2 f + where + reifySum' :: (Num a,Ord a) => a -> a + -> (forall n1 n2. (TypeableNat n1,TypeableNat n2,TypeableNat (Add n1 n2)) + => Proxy (n1::Nat) -> Proxy (n2::Nat) -> Proxy (Add n1 n2) -> r) -> r + reifySum' 0 n2 f = reifyNat n2 $ \(_::Proxy i) -> f (Proxy::Proxy Z) (Proxy::Proxy i) (Proxy::Proxy i) + reifySum' n1 n2 f = reifySum' (n1-1) n2 $ \(_::Proxy i1) (_::Proxy i2) (_::Proxy i3) + -> f (Proxy::Proxy (S i1)) (Proxy::Proxy i2) (Proxy::Proxy (S i3)) + +reifyExtract :: (Num a,Ord a) => a -> a -> a + -> (forall n1 n2 n3 n4. (TypeableNat n1,TypeableNat n2,TypeableNat n3,TypeableNat n4,Add n4 n2 ~ S n3) + => Proxy (n1::Nat) -> Proxy (n2::Nat) -> Proxy (n3::Nat) -> Proxy (n4::Nat) -> r) -> r +reifyExtract t l u f + | t <= u || l > u || l < 0 = error "smtlib2: Invalid extract parameters." + | otherwise = reifyExtract' t l u (u - l + 1) f + where + reifyExtract' :: (Num a,Ord a) => a -> a -> a -> a + -> (forall n1 n2 n3 n4. (TypeableNat n1,TypeableNat n2,TypeableNat n3,TypeableNat n4,Add n4 n2 ~ S n3) + => Proxy (n1::Nat) -> Proxy (n2::Nat) -> Proxy (n3::Nat) -> Proxy (n4::Nat) -> r) -> r + reifyExtract' t 0 0 1 f + = reifyNat t $ + \(_::Proxy n1) -> f (Proxy::Proxy n1) (Proxy::Proxy Z) (Proxy::Proxy Z) (Proxy::Proxy (S Z)) + reifyExtract' t l u 0 f + = reifyNat t $ + \(_::Proxy n1) + -> reifyNat u $ + \(_::Proxy n3) + -> f (Proxy::Proxy n1) (Proxy::Proxy (S n3)) (Proxy::Proxy n3) (Proxy::Proxy Z) + reifyExtract' t l u r f = reifyExtract' t l (u-1) (r-1) $ + \(_::Proxy n1) (_::Proxy n2) (_::Proxy n3) (_::Proxy n4) + -> f (Proxy::Proxy n1) (Proxy::Proxy n2) (Proxy::Proxy (S n3)) (Proxy::Proxy (S n4)) + + +reifyNat :: (Num a,Ord a) => a -> (forall n. TypeableNat n => Proxy (n::Nat) -> r) -> r +reifyNat x f + | x < 0 = error "smtlib2: Can only reify numbers >= 0." + | otherwise = reifyNat' x f + where + reifyNat' :: (Num a,Ord a) => a -> (forall n. TypeableNat n => Proxy (n::Nat) -> r) -> r + reifyNat' 0 f = f (Proxy :: Proxy Z) + reifyNat' n f = reifyNat' (n-1) (\(_::Proxy n) -> f (Proxy::Proxy (S n))) + +data BitVector (b :: BVKind) = BitVector Integer deriving (Eq,Ord) + +instance TypeableBVKind k => Typeable (BitVector k) where + typeOf _ = mkTyConApp + (mkTyCon3 "smtlib2" "Language.SMTLib2.Internals" "BitVector") + [typeOfBVKind (Proxy::Proxy k)] +#else +data Z = Z deriving (Typeable) +data S a = S deriving (Typeable) + +class Typeable a => TypeableNat a where + reflectNat :: Proxy a -> Integer -> Integer + +instance TypeableNat Z where + reflectNat _ = id + +instance TypeableNat n => TypeableNat (S n) where + reflectNat _ x = reflectNat (Proxy::Proxy n) (x+1) + +type family Add n1 n2 +type instance Add Z n = n +type instance Add (S n1) n2 = S (Add n1 n2) + +data BVUntyped = BVUntyped deriving (Eq,Ord,Show,Typeable) +data BVTyped n = BVTyped deriving (Eq,Ord,Show,Typeable) + +reifyNat :: (Num a,Ord a) => a -> (forall n. TypeableNat n => Proxy n -> r) -> r +reifyNat n f + | n < 0 = error "smtlib2: Can only reify numbers >= 0." + | otherwise = reifyNat' n f + where + reifyNat' :: (Num a,Eq a) => a -> (forall n. TypeableNat n => Proxy n -> r) -> r + reifyNat' 0 f' = f' (Proxy::Proxy Z) + reifyNat' n' f' = reifyNat' (n'-1) (f'.g) + + g :: Proxy n -> Proxy (S n) + g _ = Proxy + +reifySum :: (Num a,Ord a) => a -> a -> (forall n1 n2. (TypeableNat n1,TypeableNat n2,TypeableNat (Add n1 n2)) + => Proxy n1 -> Proxy n2 -> Proxy (Add n1 n2) -> r) -> r +reifySum n1 n2 f + | n1 < 0 || n2 < 0 = error "smtlib2: Cann only reify numbers >= 0." + | otherwise = reifySum' n1 n2 f + where + reifySum' :: (Num a,Ord a) => a -> a + -> (forall n1 n2. (TypeableNat n1,TypeableNat n2,TypeableNat (Add n1 n2)) + => Proxy n1 -> Proxy n2 -> Proxy (Add n1 n2) -> r) -> r + reifySum' 0 n2' f' = reifyNat n2' $ \(_::Proxy i) -> f' (Proxy::Proxy Z) (Proxy::Proxy i) (Proxy::Proxy i) + reifySum' n1' n2' f' = reifySum' (n1'-1) n2' $ \(_::Proxy i1) (_::Proxy i2) (_::Proxy i3) + -> f' (Proxy::Proxy (S i1)) (Proxy::Proxy i2) (Proxy::Proxy (S i3)) + +reifyExtract :: (Num a,Ord a) => a -> a -> a + -> (forall n1 n2 n3 n4. (TypeableNat n1,TypeableNat n2,TypeableNat n3,TypeableNat n4,Add n4 n2 ~ S n3) + => Proxy n1 -> Proxy n2 -> Proxy n3 -> Proxy n4 -> r) -> r +reifyExtract t l u f + | t <= u || l > u || l < 0 = error "smtlib2: Invalid extract parameters." + | otherwise = reifyExtract' t l u (u - l + 1) f + where + reifyExtract' :: (Num a,Ord a) => a -> a -> a -> a + -> (forall n1 n2 n3 n4. (TypeableNat n1,TypeableNat n2,TypeableNat n3,TypeableNat n4,Add n4 n2 ~ S n3) + => Proxy n1 -> Proxy n2 -> Proxy n3 -> Proxy n4 -> r) -> r + reifyExtract' t' 0 0 1 f' + = reifyNat t' $ + \(_::Proxy n1) -> f' (Proxy::Proxy n1) (Proxy::Proxy Z) (Proxy::Proxy Z) (Proxy::Proxy (S Z)) + reifyExtract' t' _ u' 0 f' = reifyNat t' $ + \(_::Proxy n1) + -> reifyNat u' $ + \(_::Proxy n3) + -> f' (Proxy::Proxy n1) (Proxy::Proxy (S n3)) (Proxy::Proxy n3) (Proxy::Proxy Z) + reifyExtract' t' l' u' r' f' = reifyExtract' t' l' (u'-1) (r'-1) $ + \(_::Proxy n1) (_::Proxy n2) (_::Proxy n3) (_::Proxy n4) + -> f' (Proxy::Proxy n1) (Proxy::Proxy n2) (Proxy::Proxy (S n3)) (Proxy::Proxy (S n4)) + +data BitVector (b :: *) = BitVector Integer deriving (Eq,Ord,Typeable) +#endif + +instance Show (BitVector a) where + show (BitVector x) = show x + +instance Enum (BitVector a) where + succ (BitVector x) = BitVector (succ x) + pred (BitVector x) = BitVector (pred x) + toEnum x = BitVector (toEnum x) + fromEnum (BitVector x) = fromEnum x + enumFrom (BitVector x) = [ BitVector y | y <- enumFrom x ] + enumFromThen (BitVector x) (BitVector y) + = [ BitVector z | z <- enumFromThen x y ] + enumFromTo (BitVector x) (BitVector y) + = [ BitVector z | z <- enumFromTo x y ] + enumFromThenTo (BitVector x) (BitVector y) (BitVector z) + = [ BitVector p | p <- enumFromThenTo x y z ] + +type N0 = Z +type N1 = S N0 +type N2 = S N1 +type N3 = S N2 +type N4 = S N3 +type N5 = S N4 +type N6 = S N5 +type N7 = S N6 +type N8 = S N7 +type N9 = S N8 +type N10 = S N9 +type N11 = S N10 +type N12 = S N11 +type N13 = S N12 +type N14 = S N13 +type N15 = S N14 +type N16 = S N15 +type N17 = S N16 +type N18 = S N17 +type N19 = S N18 +type N20 = S N19 +type N21 = S N20 +type N22 = S N21 +type N23 = S N22 +type N24 = S N23 +type N25 = S N24 +type N26 = S N25 +type N27 = S N26 +type N28 = S N27 +type N29 = S N28 +type N30 = S N29 +type N31 = S N30 +type N32 = S N31 +type N33 = S N32 +type N34 = S N33 +type N35 = S N34 +type N36 = S N35 +type N37 = S N36 +type N38 = S N37 +type N39 = S N38 +type N40 = S N39 +type N41 = S N40 +type N42 = S N41 +type N43 = S N42 +type N44 = S N43 +type N45 = S N44 +type N46 = S N45 +type N47 = S N46 +type N48 = S N47 +type N49 = S N48 +type N50 = S N49 +type N51 = S N50 +type N52 = S N51 +type N53 = S N52 +type N54 = S N53 +type N55 = S N54 +type N56 = S N55 +type N57 = S N56 +type N58 = S N57 +type N59 = S N58 +type N60 = S N59 +type N61 = S N60 +type N62 = S N61 +type N63 = S N62 +type N64 = S N63 + +type BV8 = BitVector (BVTyped N8) +type BV16 = BitVector (BVTyped N16) +type BV32 = BitVector (BVTyped N32) +type BV64 = BitVector (BVTyped N64) + +instance Monad m => SMTBackend (AnyBackend m) m where + smtHandle (AnyBackend b) = smtHandle b + +instance Show (SMTExpr t) where + showsPrec = showExpr + +newtype Bound = Bound Integer deriving (Typeable,Eq,Ord,Show) + +showExpr :: Int -> SMTExpr t -> ShowS +showExpr p (Var v ann) = showParen (p>10) (showString "Var " . + showsPrec 11 v . + showChar ' ' . + showsPrec 11 ann) +showExpr p (QVar lvl v ann) = showParen (p>10) (showString "QVar " . + showsPrec 11 lvl . + showChar ' ' . + showsPrec 11 v . + showChar ' ' . + showsPrec 11 ann) +showExpr p (Const c ann) = showParen (p>10) (showString "Const " . + showsPrec 11 c . + showChar ' ' . + showsPrec 11 ann) +showExpr p (AsArray fun ann) = showParen (p>10) (showString "AsArray " . + showsPrec 11 fun . + showChar ' ' . + showsPrec 11 ann) +showExpr p (Forall lvl args f) = showParen (p>10) (showString "Forall " . + showsPrec 11 lvl . + showChar ' ' . + showsPrec 11 args . + showString " ~> " . + showsPrec 11 f) +showExpr p (Exists lvl args f) = showParen (p>10) (showString "Exists " . + showsPrec 11 lvl . + showChar ' ' . + showsPrec 11 args . + showString " ~> " . + showsPrec 11 f) +showExpr p (Let lvl arg f) = showParen (p>10) (showString "Let " . + showsPrec 11 lvl . + showChar ' ' . + showsPrec 11 arg . + showChar ' ' . + showsPrec 11 f) +showExpr p (App fun arg) = let strArgs = showsPrec 11 arg + in showParen (p>10) (showString "App " . + showsPrec 11 fun . + showChar ' ' . + strArgs) +showExpr p (Named expr name nc) = let strExpr = showExpr 11 expr + in showParen (p>10) (showString "Named " . + strExpr . + showChar ' ' . + showsPrec 11 name . + showChar ' ' . + showsPrec 11 nc) +showExpr p (InternalObj obj ann) = showParen (p>10) (showString "InternalObj " . + showsPrec 11 obj . + showChar ' ' . + showsPrec 11 ann) +showExpr p (UntypedExpr e) = showExpr p e +showExpr p (UntypedExprValue e) = showExpr p e + +instance Show (SMTFunction arg res) where + showsPrec _ SMTEq = showString "SMTEq" + showsPrec p (SMTMap fun) = showParen (p>10) (showString "SMTMap " . + showsPrec 11 fun) + showsPrec p (SMTFun i ann) = showParen (p>10) (showString "SMTFun " . + showsPrec 11 i . + showChar ' ' . + showsPrec 11 ann) + showsPrec p (SMTBuiltIn name ann) = showParen (p>10) (showString "SMTBuiltIn " . + showsPrec 11 name . + showChar ' ' . + showsPrec 11 ann) + showsPrec p (SMTOrd op) = showParen (p>10) (showString "SMTOrd " . + showsPrec 11 op) + showsPrec p (SMTArith op) = showParen (p>10) (showString "SMTArith " . + showsPrec 11 op) + showsPrec p SMTMinus = showString "SMTMinus" + showsPrec p (SMTIntArith op) = showParen (p>10) (showString "SMTIntArith " . + showsPrec 11 op) + showsPrec p SMTDivide = showString "SMTDivide" + showsPrec p SMTNeg = showString "SMTNeg" + showsPrec p SMTAbs = showString "SMTAbs" + showsPrec p SMTNot = showString "SMTNot" + showsPrec p (SMTLogic op) = showParen (p>10) (showString "SMTLogic " . + showsPrec 11 op) + showsPrec p SMTDistinct = showString "SMTDistinct" + showsPrec p SMTToReal = showString "SMTToReal" + showsPrec p SMTToInt = showString "SMTToInt" + showsPrec p SMTITE = showString "SMTITE" + showsPrec p (SMTBVComp op) = showParen (p>10) (showString "SMTBVComp " . + showsPrec 11 op) + showsPrec p (SMTBVBin op) = showParen (p>10) (showString "SMTBVBin " . + showsPrec 11 op) + showsPrec p (SMTBVUn op) = showParen (p>10) (showString "SMTBVUn " . + showsPrec 11 op) + showsPrec p SMTSelect = showString "SMTSelect" + showsPrec p SMTStore = showString "SMTStore" + showsPrec p (SMTConstArray ann) = showParen (p>10) (showString "SMTConstArray " . + showsPrec 11 ann) + showsPrec p SMTConcat = showString "SMTConcat" + showsPrec p (SMTExtract start len) = showParen (p>10) (showString "SMTExtract " . + showsPrec 11 (reflectNat start 0) . + showChar ' ' . + showsPrec 11 (reflectNat len 0)) + showsPrec p (SMTConstructor con) = showParen (p>10) (showString "SMTConstructor " . + showsPrec 11 con) + showsPrec p (SMTConTest con) = showParen (p>10) (showString "SMTConTest " . + showsPrec 11 con) + showsPrec p (SMTFieldSel field) = showParen (p>10) (showString "SMTFieldSel " . + showsPrec 11 field) + showsPrec p (SMTDivisible i) = showParen (p>10) (showString "SMTDivisible " . + showsPrec 11 i) + +instance Show (Field a f) where + showsPrec p (Field _ _ _ f) = showParen (p>10) + (showString "Field " . + showsPrec 11 (fieldName f)) + +instance Show (Constructor arg res) where + showsPrec p (Constructor _ _ con) = showParen (p>10) + (showString "Constructor " . + showsPrec 11 (conName con)) + +noLimits :: CheckSatLimits +noLimits = CheckSatLimits { limitTime = Nothing + , limitMemory = Nothing } + +newtype Quantified = Quantified Integer deriving (Typeable,Show,Eq,Ord) + +quantificationLevel :: SMTExpr t -> Integer +quantificationLevel (QVar lvl _ _) = lvl+1 +quantificationLevel (Forall lvl _ _) = lvl+1 +quantificationLevel (Exists lvl _ _) = lvl+1 +quantificationLevel (Let lvl _ _) = lvl+1 +quantificationLevel (App _ arg) = maximum $ fmap quantificationLevel $ fromArgs arg +quantificationLevel (Named expr _ _) = quantificationLevel expr +quantificationLevel (UntypedExpr e) = quantificationLevel e +quantificationLevel (UntypedExprValue e) = quantificationLevel e +quantificationLevel _ = 0 + +inferSorts :: ArgumentSort -> Sort -> Map Integer Sort -> Map Integer Sort +inferSorts (Fix (ArgumentSort i)) s mp = Map.insert i s mp +inferSorts (Fix (NormalSort (ArraySort xs x))) (Fix (ArraySort ys y)) mp + = foldl (\cmp (x,y) -> inferSorts x y cmp + ) (inferSorts x y mp) (zip xs ys) +inferSorts (Fix (NormalSort (NamedSort n1 xs))) (Fix (NamedSort n2 ys)) mp + | n1==n2 = foldl (\cmp (x,y) -> inferSorts x y cmp + ) mp (zip xs ys) +inferSorts _ _ mp = mp + +valueSort :: DataTypeInfo -> Value -> Sort +valueSort _ (BoolValue _) = Fix BoolSort +valueSort _ (IntValue _) = Fix IntSort +valueSort _ (RealValue _) = Fix RealSort +valueSort _ (BVValue w _) = Fix (BVSort w False) +valueSort dts (ConstrValue _ _ (Just (sname,sargs))) = Fix $ NamedSort sname sargs +valueSort dts (ConstrValue name args Nothing) = case Map.lookup name (constructors dts) of + Just (con,dt,tc) -> Fix $ NamedSort (dataTypeName dt) (fmap snd $ Map.toAscList infMp) + where + argTps = fmap (valueSort dts) args + conTps = fmap fieldSort (conFields con) + infMp = foldl (\cinf (tp,argTp) -> inferSorts tp argTp cinf + ) Map.empty (zip conTps argTps) diff --git a/Language/SMTLib2/Internals/Instances.hs b/Language/SMTLib2/Internals/Instances.hs new file mode 100644 --- /dev/null +++ b/Language/SMTLib2/Internals/Instances.hs @@ -0,0 +1,1639 @@ +{- | Implements various instance declarations for 'Language.SMTLib2.SMTType', + 'Language.SMTLib2.SMTValue', etc. -} +{-# LANGUAGE FlexibleInstances,OverloadedStrings,MultiParamTypeClasses,RankNTypes,TypeFamilies,GeneralizedNewtypeDeriving,DeriveDataTypeable,GADTs,FlexibleContexts,CPP,ScopedTypeVariables,TypeOperators #-} +module Language.SMTLib2.Internals.Instances where + +import Language.SMTLib2.Internals +import Language.SMTLib2.Internals.Operators +import Data.Ratio +import Data.Typeable +import Data.List (genericReplicate,zip4,zip5,zip6,genericIndex) +#ifdef SMTLIB2_WITH_CONSTRAINTS +import Data.Constraint +import Data.Proxy +#endif +import Data.Fix +import Data.Map (Map) +import qualified Data.Map as Map +import Data.Maybe (fromJust) +import Data.Traversable (mapM) +import Data.Foldable (foldlM) +import Text.Show +import Data.Functor.Identity +import Prelude hiding (mapM) + +valueToHaskell :: DataTypeInfo + -> (forall t. SMTType t => [ProxyArg] -> t -> SMTAnnotation t -> r) + -> Maybe Sort + -> Value + -> r +valueToHaskell _ f _ (BoolValue v) = f [] v () +valueToHaskell _ f _ (IntValue v) = f [] v () +valueToHaskell _ f _ (RealValue v) = f [] v () +valueToHaskell _ f (Just (Fix (BVSort { bvSortUntyped = True }))) (BVValue { bvValueWidth = w + , bvValueValue = v }) + = f [] (BitVector v::BitVector BVUntyped) w +valueToHaskell _ f _ (BVValue { bvValueWidth = w + , bvValueValue = v }) + = reifyNat w (\(_::Proxy tp) -> f [] (BitVector v::BitVector (BVTyped tp)) ()) +valueToHaskell dtInfo f sort (ConstrValue name args sort') + = case Map.lookup name (constructors dtInfo) of + Just (con,dt,struct) + -> let sort'' = case sort of + Just (Fix (NamedSort name args)) -> Just (name,args) + Nothing -> sort' + argPrx = case sort'' of + Just (_,sort''') -> fmap (\s -> Just $ withSort dtInfo s ProxyArg) sort''' + Nothing -> genericReplicate (argCount struct) Nothing + sorts' = fmap (\field -> argumentSortToSort + (\i -> case sort'' of + Nothing -> Nothing + Just (_,sort''') -> Just $ sort''' `genericIndex` i) + (fieldSort field) + ) (conFields con) + rargs :: [AnyValue] + rargs = fmap (\(val,s) -> valueToHaskell dtInfo AnyValue s val) (zip args sorts') + in construct con argPrx rargs f + +-- | Reconstruct the type annotation for a given SMT expression. +extractAnnotation :: SMTExpr a -> SMTAnnotation a +extractAnnotation (Var _ ann) = ann +extractAnnotation (QVar _ _ ann) = ann +extractAnnotation (Const _ ann) = ann +extractAnnotation (AsArray f arg) = (arg,inferResAnnotation f arg) +extractAnnotation (Forall _ _ _) = () +extractAnnotation (Exists _ _ _) = () +extractAnnotation (Let _ _ f) = extractAnnotation f +extractAnnotation (Named x _ _) = extractAnnotation x +extractAnnotation (App f arg) = inferResAnnotation f (extractArgAnnotation arg) +extractAnnotation (InternalObj _ ann) = ann +extractAnnotation (UntypedExpr (expr::SMTExpr t)) = ProxyArg (undefined::t) (extractAnnotation expr) +extractAnnotation (UntypedExprValue (expr::SMTExpr t)) = ProxyArgValue (undefined::t) (extractAnnotation expr) + +inferResAnnotation :: SMTFunction arg res -> ArgAnnotation arg -> SMTAnnotation res +inferResAnnotation SMTEq _ = () +inferResAnnotation x@(SMTMap f) ann + = withUndef f x (\ua ui -> let (i_ann,a_ann) = inferLiftedAnnotation ua ui ann + in (i_ann,inferResAnnotation f a_ann)) + where + withUndef :: SMTFunction arg res -> SMTFunction (Lifted arg i) (SMTArray i res) -> (arg -> i -> b) -> b + withUndef _ _ f' = f' undefined undefined +inferResAnnotation (SMTFun _ ann) _ = ann +inferResAnnotation (SMTBuiltIn _ ann) _ = ann +inferResAnnotation (SMTOrd _) _ = () +inferResAnnotation (SMTArith _) ~(ann:_) = ann +inferResAnnotation SMTMinus ~(ann,_) = ann +inferResAnnotation (SMTIntArith _) ~(ann,_) = ann +inferResAnnotation SMTDivide ~(ann,_) = ann +inferResAnnotation SMTNeg ann = ann +inferResAnnotation SMTAbs ann = ann +inferResAnnotation SMTNot _ = () +inferResAnnotation (SMTLogic _) _ = () +inferResAnnotation SMTDistinct _ = () +inferResAnnotation SMTToReal _ = () +inferResAnnotation SMTToInt _ = () +inferResAnnotation SMTITE ~(_,ann,_) = ann +inferResAnnotation (SMTBVComp _) _ = () +inferResAnnotation (SMTBVBin _) ~(ann,_) = ann +inferResAnnotation (SMTBVUn _) ann = ann +inferResAnnotation SMTSelect ~(~(_,ann),_) = ann +inferResAnnotation SMTStore ~(ann,_,_) = ann +inferResAnnotation (SMTConstArray i_ann) v_ann = (i_ann,v_ann) +inferResAnnotation x@SMTConcat ~(ann1,ann2) + = withUndef x $ \u1 u2 -> concatAnnotation u1 u2 ann1 ann2 + where + withUndef :: SMTFunction (SMTExpr (BitVector a),SMTExpr (BitVector b)) res + -> (a -> b -> c) -> c + withUndef _ f = f undefined undefined +inferResAnnotation x@(SMTExtract _ prLen) ann + = withUndef x $ \u1 u2 -> extractAnn u1 u2 (reflectNat prLen 0) ann + where + withUndef :: SMTFunction (SMTExpr (BitVector a)) (BitVector res) + -> (a -> res -> c) -> c + withUndef _ f = f undefined undefined +inferResAnnotation (SMTConstructor (Constructor prx dt con)) _ + = case dataTypeGetUndefined dt prx (\_ ann' -> cast ann') of + Just ann' -> ann' +inferResAnnotation (SMTConTest _) _ = () +inferResAnnotation (SMTFieldSel (Field prx dt _ f)) _ + = dataTypeGetUndefined dt prx (\u _ -> case fieldGet f prx u (\_ ann -> cast ann) of + Just ann' -> ann') +inferResAnnotation (SMTDivisible _) _ = () + +-- Untyped + +entype :: (forall a. SMTType a => SMTExpr a -> b) -> SMTExpr Untyped -> b +entype f (Var i (ProxyArg (_::t) ann)) + = f (Var i ann::SMTExpr t) +entype f (QVar lvl i (ProxyArg (_::t) ann)) + = f (QVar lvl i ann::SMTExpr t) +entype f (UntypedExpr x) = f x +entype f (InternalObj obj (ProxyArg (_::t) ann)) + = f (InternalObj obj ann :: SMTExpr t) +entype f expr = error $ "Can't entype expression "++show expr + +entypeValue :: (forall a. SMTValue a => SMTExpr a -> b) -> SMTExpr UntypedValue -> b +entypeValue f (Var i (ProxyArgValue (_::t) ann)) + = f (Var i ann::SMTExpr t) +entypeValue f (QVar lvl i (ProxyArgValue (_::t) ann)) + = f (QVar lvl i ann::SMTExpr t) +entypeValue f (Const (UntypedValue v) (ProxyArgValue (_::t) ann)) + = case cast v of + Just rv -> f (Const (rv::t) ann) +entypeValue f (UntypedExprValue x) = f x +entypeValue f (InternalObj obj (ProxyArgValue (_::t) ann)) + = f (InternalObj obj ann :: SMTExpr t) +entypeValue f expr = error $ "Can't entype expression "++show expr + +{- +entypeValueFunction :: (forall a. SMTValue a => SMTFunction arg a -> b) + -> SMTFunction arg UntypedValue + -> b +entypeValueFunction f (SMTFun i (ProxyArgValue (_::t) ann)) + = f (SMTFun i ann::SMTFunction arg t)-} + +castUntypedExpr :: SMTType t => SMTExpr Untyped -> SMTExpr t +castUntypedExpr = entype (\expr -> case cast expr of + Just r -> r + Nothing -> error $ "smtlib2: castUntypedExpr failed.") + +castUntypedExprValue :: SMTType t => SMTExpr UntypedValue -> SMTExpr t +castUntypedExprValue + = entypeValue (\expr -> case cast expr of + Just r -> r + Nothing -> error $ "smtlib2: castUntypedExprValue failed.") + +instance SMTType Untyped where + type SMTAnnotation Untyped = ProxyArg + getSort _ (ProxyArg u ann) = getSort u ann + asDataType _ (ProxyArg u ann) = asDataType u ann + asValueType _ (ProxyArg u ann) f = asValueType u ann f + getProxyArgs _ (ProxyArg u ann) = getProxyArgs u ann + additionalConstraints _ (ProxyArg u ann) = do + constr <- additionalConstraints u ann + return $ \(UntypedExpr x) -> case cast x of + Just x' -> constr x' + annotationFromSort _ sort = withSort emptyDataTypeInfo sort ProxyArg + defaultExpr (ProxyArg (_::t) ann) = UntypedExpr (defaultExpr ann :: SMTExpr t) + +instance SMTType UntypedValue where + type SMTAnnotation UntypedValue = ProxyArgValue + getSort _ (ProxyArgValue u ann) = getSort u ann + asDataType _ (ProxyArgValue u ann) = asDataType u ann + asValueType _ (ProxyArgValue u ann) f = asValueType u ann f + getProxyArgs _ (ProxyArgValue u ann) = getProxyArgs u ann + additionalConstraints _ (ProxyArgValue u ann) = do + constr <- additionalConstraints u ann + return $ \(UntypedExprValue x) -> case cast x of + Just x' -> constr x' + annotationFromSort _ sort + = withSort emptyDataTypeInfo sort + (\u ann -> case asValueType u ann ProxyArgValue of + Just r -> r + Nothing -> error $ "annotationFromSort for non-value type "++show (typeOf u)++" used.") + defaultExpr (ProxyArgValue (_::t) ann) + = UntypedExprValue (defaultExpr ann :: SMTExpr t) + +instance SMTValue UntypedValue where + unmangle = ComplexUnmangling $ + \f val (ProxyArgValue _ ann) + -> entypeValue + (\(expr'::SMTExpr t) -> case cast ann of + Just ann' -> do + res <- f expr' ann' + return $ Just $ UntypedValue res + ) val + mangle = ComplexMangling (\(UntypedValue x) (ProxyArgValue (_::t) ann) + -> case cast x of + Just x' -> UntypedExprValue $ Const (x'::t) ann) + +-- Bool + +instance SMTType Bool where + type SMTAnnotation Bool = () + getSort _ _ = Fix BoolSort + annotationFromSort _ _ = () + asValueType x ann f = Just $ f x ann + defaultExpr _ = Const False () + +instance SMTValue Bool where + unmangle = PrimitiveUnmangling (\val _ -> case val of + BoolValue v -> Just v + _ -> Nothing) + mangle = PrimitiveMangling (\v _ -> BoolValue v) + +-- Integer + +instance SMTType Integer where + type SMTAnnotation Integer = () + getSort _ _ = Fix IntSort + annotationFromSort _ _ = () + asValueType x ann f = Just $ f x ann + defaultExpr _ = Const 0 () + +instance SMTValue Integer where + unmangle = PrimitiveUnmangling (\val _ -> case val of + IntValue v -> Just v + _ -> Nothing) + mangle = PrimitiveMangling (\v _ -> IntValue v) + +instance SMTArith Integer + +instance Num (SMTExpr Integer) where + fromInteger x = Const x () + (+) x y = App (SMTArith Plus) [x,y] + (-) x y = App SMTMinus (x,y) + (*) x y = App (SMTArith Mult) [x,y] + negate x = App SMTNeg x + abs x = App SMTAbs x + signum x = App SMTITE (App (SMTOrd Ge) (x,Const 0 ()),Const 1 (),Const (-1) ()) + +instance SMTOrd Integer where + (.<.) x y = App (SMTOrd Lt) (x,y) + (.<=.) x y = App (SMTOrd Le) (x,y) + (.>.) x y = App (SMTOrd Gt) (x,y) + (.>=.) x y = App (SMTOrd Ge) (x,y) + +instance Enum (SMTExpr Integer) where + succ x = x + 1 + pred x = x - 1 + toEnum x = Const (fromIntegral x) () + fromEnum (Const x _) = fromIntegral x + fromEnum _ = error $ "smtlib2: Can't use fromEnum on non-constant SMTExpr (use getValue to extract values from the solver)" + enumFrom x = case x of + Const x' _ -> fmap (\i -> Const i ()) (enumFrom x') + _ -> x:[ x+(Const n ()) | n <- [1..] ] + enumFromThen x inc = case inc of + Const inc' _ -> case x of + Const x' _ -> fmap (\i -> Const i ()) (enumFromThen x' inc') + _ -> x:[ x + (Const (n*inc') ()) | n <- [1..]] + _ -> [ Prelude.foldl (+) x (genericReplicate n inc) | n <- [(0::Integer)..]] + enumFromThenTo (Const x _) (Const inc _) (Const lim _) + = fmap (\i -> Const i ()) (enumFromThenTo x inc lim) + enumFromThenTo _ _ _ = error $ "smtlib2: Can't use enumFromThenTo on non-constant SMTExprs" + +-- Real + +instance SMTType (Ratio Integer) where + type SMTAnnotation (Ratio Integer) = () + getSort _ _ = Fix RealSort + annotationFromSort _ _ = () + asValueType x ann f = Just $ f x ann + defaultExpr _ = Const 0 () + +instance SMTValue (Ratio Integer) where + unmangle = PrimitiveUnmangling (\val _ -> case val of + RealValue v -> Just v + _ -> Nothing) + mangle = PrimitiveMangling (\v _ -> RealValue v) + +instance SMTArith (Ratio Integer) + +instance Num (SMTExpr (Ratio Integer)) where + fromInteger x = Const (fromInteger x) () + (+) x y = App (SMTArith Plus) [x,y] + (-) x y = App SMTMinus (x,y) + (*) x y = App (SMTArith Mult) [x,y] + negate = App SMTNeg + abs x = App SMTITE (App (SMTOrd Ge) (x,Const 0 ()),x,App SMTNeg x) + signum x = App SMTITE (App (SMTOrd Ge) (x,Const 0 ()),Const 1 (),Const (-1) ()) + +instance Fractional (SMTExpr (Ratio Integer)) where + (/) x y = App SMTDivide (x,y) + fromRational x = Const x () + +instance SMTOrd (Ratio Integer) where + (.<.) x y = App (SMTOrd Lt) (x,y) + (.<=.) x y = App (SMTOrd Le) (x,y) + (.>.) x y = App (SMTOrd Gt) (x,y) + (.>=.) x y = App (SMTOrd Ge) (x,y) + +-- Arrays + +instance (Args idx,SMTType val) => SMTType (SMTArray idx val) where + type SMTAnnotation (SMTArray idx val) = (ArgAnnotation idx,SMTAnnotation val) + getSort u (anni,annv) = Fix $ ArraySort (argSorts (getIdx u) anni) (getSort (getVal u) annv) + where + getIdx :: SMTArray i v -> i + getIdx _ = undefined + getVal :: SMTArray i v -> v + getVal _ = undefined + annotationFromSort u (Fix (ArraySort argSorts valSort)) = (argAnn,annotationFromSort (getVal u) valSort) + where + (argAnn,[]) = getArgAnnotation (getIdx u) argSorts + getIdx :: SMTArray i v -> i + getIdx _ = undefined + getVal :: SMTArray i v -> v + getVal _ = undefined + asValueType _ _ _ = Nothing + defaultExpr ~(anni,annv) = App (SMTConstArray anni) (defaultExpr annv) + +instance (SMTType a) => Liftable (SMTExpr a) where + type Lifted (SMTExpr a) i = SMTExpr (SMTArray i a) + getLiftedArgumentAnn _ _ a_ann i_ann = (i_ann,a_ann) + inferLiftedAnnotation _ _ ~(i,a) = (i,a) +#ifdef SMTLIB2_WITH_CONSTRAINTS + getConstraint _ = Dict +#endif + +instance (SMTType a) => Liftable [SMTExpr a] where + type Lifted [SMTExpr a] i = [SMTExpr (SMTArray i a)] + getLiftedArgumentAnn _ _ a_anns i_ann = fmap (\a_ann -> (i_ann,a_ann)) a_anns + inferLiftedAnnotation _ _ ~(~(i,x):xs) = (i,x:(fmap snd xs)) +#ifdef SMTLIB2_WITH_CONSTRAINTS + getConstraint _ = Dict +#endif + +instance (Liftable a,Liftable b) + => Liftable (a,b) where + type Lifted (a,b) i = (Lifted a i,Lifted b i) + getLiftedArgumentAnn ~(x,y) i (a_ann,b_ann) i_ann = (getLiftedArgumentAnn x i a_ann i_ann, + getLiftedArgumentAnn y i b_ann i_ann) + inferLiftedAnnotation ~(x,y) i ~(a_ann,b_ann) = let (ann_i,ann_a) = inferLiftedAnnotation x i a_ann + (_,ann_b) = inferLiftedAnnotation y i b_ann + in (ann_i,(ann_a,ann_b)) +#ifdef SMTLIB2_WITH_CONSTRAINTS + getConstraint (_ :: p ((a,b),i)) = case getConstraint (Proxy :: Proxy (a,i)) of + Dict -> case getConstraint (Proxy :: Proxy (b,i)) of + Dict -> Dict +#endif + +instance (Liftable a,Liftable b,Liftable c) + => Liftable (a,b,c) where + type Lifted (a,b,c) i = (Lifted a i,Lifted b i,Lifted c i) + getLiftedArgumentAnn ~(x1,x2,x3) i (ann1,ann2,ann3) i_ann + = (getLiftedArgumentAnn x1 i ann1 i_ann, + getLiftedArgumentAnn x2 i ann2 i_ann, + getLiftedArgumentAnn x3 i ann3 i_ann) + inferLiftedAnnotation ~(x1,x2,x3) i ~(ann1,ann2,ann3) + = let (i_ann,ann1') = inferLiftedAnnotation x1 i ann1 + (_,ann2') = inferLiftedAnnotation x2 i ann2 + (_,ann3') = inferLiftedAnnotation x3 i ann3 + in (i_ann,(ann1',ann2',ann3')) +#ifdef SMTLIB2_WITH_CONSTRAINTS + getConstraint (_ :: p ((a,b,c),i)) = case getConstraint (Proxy :: Proxy (a,i)) of + Dict -> case getConstraint (Proxy :: Proxy (b,i)) of + Dict -> case getConstraint (Proxy :: Proxy (c,i)) of + Dict -> Dict +#endif + +instance (Liftable a,Liftable b,Liftable c,Liftable d) + => Liftable (a,b,c,d) where + type Lifted (a,b,c,d) i = (Lifted a i,Lifted b i,Lifted c i,Lifted d i) + getLiftedArgumentAnn ~(x1,x2,x3,x4) i (ann1,ann2,ann3,ann4) i_ann + = (getLiftedArgumentAnn x1 i ann1 i_ann, + getLiftedArgumentAnn x2 i ann2 i_ann, + getLiftedArgumentAnn x3 i ann3 i_ann, + getLiftedArgumentAnn x4 i ann4 i_ann) + inferLiftedAnnotation ~(x1,x2,x3,x4) i ~(ann1,ann2,ann3,ann4) + = let (i_ann,ann1') = inferLiftedAnnotation x1 i ann1 + (_,ann2') = inferLiftedAnnotation x2 i ann2 + (_,ann3') = inferLiftedAnnotation x3 i ann3 + (_,ann4') = inferLiftedAnnotation x4 i ann4 + in (i_ann,(ann1',ann2',ann3',ann4')) +#ifdef SMTLIB2_WITH_CONSTRAINTS + getConstraint (_ :: p ((a,b,c,d),i)) = case getConstraint (Proxy :: Proxy (a,i)) of + Dict -> case getConstraint (Proxy :: Proxy (b,i)) of + Dict -> case getConstraint (Proxy :: Proxy (c,i)) of + Dict -> case getConstraint (Proxy :: Proxy (d,i)) of + Dict -> Dict +#endif + +instance (Liftable a,Liftable b,Liftable c,Liftable d,Liftable e) + => Liftable (a,b,c,d,e) where + type Lifted (a,b,c,d,e) i = (Lifted a i,Lifted b i,Lifted c i,Lifted d i,Lifted e i) + getLiftedArgumentAnn ~(x1,x2,x3,x4,x5) i (ann1,ann2,ann3,ann4,ann5) i_ann + = (getLiftedArgumentAnn x1 i ann1 i_ann, + getLiftedArgumentAnn x2 i ann2 i_ann, + getLiftedArgumentAnn x3 i ann3 i_ann, + getLiftedArgumentAnn x4 i ann4 i_ann, + getLiftedArgumentAnn x5 i ann5 i_ann) + inferLiftedAnnotation ~(x1,x2,x3,x4,x5) i ~(ann1,ann2,ann3,ann4,ann5) + = let (i_ann,ann1') = inferLiftedAnnotation x1 i ann1 + (_,ann2') = inferLiftedAnnotation x2 i ann2 + (_,ann3') = inferLiftedAnnotation x3 i ann3 + (_,ann4') = inferLiftedAnnotation x4 i ann4 + (_,ann5') = inferLiftedAnnotation x5 i ann5 + in (i_ann,(ann1',ann2',ann3',ann4',ann5')) +#ifdef SMTLIB2_WITH_CONSTRAINTS + getConstraint (_ :: p ((a,b,c,d,e),i)) = case getConstraint (Proxy :: Proxy (a,i)) of + Dict -> case getConstraint (Proxy :: Proxy (b,i)) of + Dict -> case getConstraint (Proxy :: Proxy (c,i)) of + Dict -> case getConstraint (Proxy :: Proxy (d,i)) of + Dict -> case getConstraint (Proxy :: Proxy (e,i)) of + Dict -> Dict +#endif + +instance (Liftable a,Liftable b,Liftable c,Liftable d,Liftable e,Liftable f) + => Liftable (a,b,c,d,e,f) where + type Lifted (a,b,c,d,e,f) i = (Lifted a i,Lifted b i,Lifted c i,Lifted d i,Lifted e i,Lifted f i) + getLiftedArgumentAnn ~(x1,x2,x3,x4,x5,x6) i (ann1,ann2,ann3,ann4,ann5,ann6) i_ann + = (getLiftedArgumentAnn x1 i ann1 i_ann, + getLiftedArgumentAnn x2 i ann2 i_ann, + getLiftedArgumentAnn x3 i ann3 i_ann, + getLiftedArgumentAnn x4 i ann4 i_ann, + getLiftedArgumentAnn x5 i ann5 i_ann, + getLiftedArgumentAnn x6 i ann6 i_ann) + inferLiftedAnnotation ~(x1,x2,x3,x4,x5,x6) i ~(ann1,ann2,ann3,ann4,ann5,ann6) + = let (i_ann,ann1') = inferLiftedAnnotation x1 i ann1 + (_,ann2') = inferLiftedAnnotation x2 i ann2 + (_,ann3') = inferLiftedAnnotation x3 i ann3 + (_,ann4') = inferLiftedAnnotation x4 i ann4 + (_,ann5') = inferLiftedAnnotation x5 i ann5 + (_,ann6') = inferLiftedAnnotation x6 i ann6 + in (i_ann,(ann1',ann2',ann3',ann4',ann5',ann6')) +#ifdef SMTLIB2_WITH_CONSTRAINTS + getConstraint (_ :: p ((a,b,c,d,e,f),i)) = case getConstraint (Proxy :: Proxy (a,i)) of + Dict -> case getConstraint (Proxy :: Proxy (b,i)) of + Dict -> case getConstraint (Proxy :: Proxy (c,i)) of + Dict -> case getConstraint (Proxy :: Proxy (d,i)) of + Dict -> case getConstraint (Proxy :: Proxy (e,i)) of + Dict -> case getConstraint (Proxy :: Proxy (f,i)) of + Dict -> Dict +#endif + +instance (TypeableNat n1,TypeableNat n2,TypeableNat (Add n1 n2)) + => Concatable (BVTyped n1) (BVTyped n2) where + type ConcatResult (BVTyped n1) (BVTyped n2) = BVTyped (Add n1 n2) + concatAnnotation _ _ _ _ = () + +instance (TypeableNat n2) => Concatable BVUntyped (BVTyped n2) where + type ConcatResult BVUntyped (BVTyped n2) = BVUntyped + concatAnnotation _ (_::BVTyped n2) ann1 _ + = ann1+(reflectNat (Proxy::Proxy n2) 0) + +instance (TypeableNat n1) => Concatable (BVTyped n1) BVUntyped where + type ConcatResult (BVTyped n1) BVUntyped = BVUntyped + concatAnnotation (_::BVTyped n1) _ _ ann2 + = (reflectNat (Proxy::Proxy n1) 0)+ann2 + +instance Concatable BVUntyped BVUntyped where + type ConcatResult BVUntyped BVUntyped = BVUntyped + concatAnnotation _ _ ann1 ann2 = ann1+ann2 + +-- Arguments + +instance (SMTType a) => Args (SMTExpr a) where + type ArgAnnotation (SMTExpr a) = SMTAnnotation a + foldExprs f = f + foldsExprs f = f + extractArgAnnotation = extractAnnotation + toArgs _ (x:xs) = do + r <- entype gcast x + return (r,xs) + toArgs _ [] = Nothing + fromArgs x = [UntypedExpr x] + getTypes (_::SMTExpr a) ann = [ProxyArg (undefined::a) ann] + getArgAnnotation u (s:rest) = (annotationFromSort (getUndef u) s,rest) + getArgAnnotation _ [] = error "smtlib2: To few sorts provided." + +instance (Args a,Args b) => Args (a,b) where + type ArgAnnotation (a,b) = (ArgAnnotation a,ArgAnnotation b) + foldExprs f s ~(e1,e2) ~(ann1,ann2) = do + ~(s1,e1') <- foldExprs f s e1 ann1 + ~(s2,e2') <- foldExprs f s1 e2 ann2 + return (s2,(e1',e2')) + foldsExprs f s args ~(ann1,ann2) = do + ~(s1,e1,r1) <- foldsExprs f s (fmap (\(~(e1,_),b) -> (e1,b)) args) ann1 + ~(s2,e2,r2) <- foldsExprs f s1 (fmap (\(~(_,e2),b) -> (e2,b)) args) ann2 + return (s2,zip e1 e2,(r1,r2)) + extractArgAnnotation ~(x,y) = (extractArgAnnotation x, + extractArgAnnotation y) + toArgs ~(ann1,ann2) x = do + (r1,x1) <- toArgs ann1 x + (r2,x2) <- toArgs ann2 x1 + return ((r1,r2),x2) + fromArgs (x,y) = fromArgs x ++ fromArgs y + getTypes ~(x1,x2) (ann1,ann2) = getTypes x1 ann1 ++ getTypes x2 ann2 + getArgAnnotation (_::(a1,a2)) sorts + = let (ann1,r1) = getArgAnnotation (undefined::a1) sorts + (ann2,r2) = getArgAnnotation (undefined::a2) r1 + in ((ann1,ann2),r2) + +instance (SMTValue a) => LiftArgs (SMTExpr a) where + type Unpacked (SMTExpr a) = a + liftArgs = Const + unliftArgs expr f = f expr + +instance (LiftArgs a,LiftArgs b) => LiftArgs (a,b) where + type Unpacked (a,b) = (Unpacked a,Unpacked b) + liftArgs (x,y) ~(a1,a2) = (liftArgs x a1,liftArgs y a2) + unliftArgs (x,y) f = do + rx <- unliftArgs x f + ry <- unliftArgs y f + return (rx,ry) + +instance (Args a,Args b,Args c) => Args (a,b,c) where + type ArgAnnotation (a,b,c) = (ArgAnnotation a,ArgAnnotation b,ArgAnnotation c) + foldExprs f s ~(e1,e2,e3) ~(ann1,ann2,ann3) = do + ~(s1,e1') <- foldExprs f s e1 ann1 + ~(s2,e2') <- foldExprs f s1 e2 ann2 + ~(s3,e3') <- foldExprs f s2 e3 ann3 + return (s3,(e1',e2',e3')) + foldsExprs f s args ~(ann1,ann2,ann3) = do + ~(s1,e1,r1) <- foldsExprs f s (fmap (\(~(e1,_,_),b) -> (e1,b)) args) ann1 + ~(s2,e2,r2) <- foldsExprs f s1 (fmap (\(~(_,e2,_),b) -> (e2,b)) args) ann2 + ~(s3,e3,r3) <- foldsExprs f s2 (fmap (\(~(_,_,e3),b) -> (e3,b)) args) ann3 + return (s3,zip3 e1 e2 e3,(r1,r2,r3)) + extractArgAnnotation ~(e1,e2,e3) + = (extractArgAnnotation e1, + extractArgAnnotation e2, + extractArgAnnotation e3) + toArgs ~(ann1,ann2,ann3) x = do + (r1,x1) <- toArgs ann1 x + (r2,x2) <- toArgs ann2 x1 + (r3,x3) <- toArgs ann3 x2 + return ((r1,r2,r3),x3) + fromArgs (x1,x2,x3) = fromArgs x1 ++ + fromArgs x2 ++ + fromArgs x3 + getArgAnnotation (_::(a1,a2,a3)) sorts + = let (ann1,r1) = getArgAnnotation (undefined::a1) sorts + (ann2,r2) = getArgAnnotation (undefined::a2) r1 + (ann3,r3) = getArgAnnotation (undefined::a3) r2 + in ((ann1,ann2,ann3),r3) + getTypes ~(x1,x2,x3) (ann1,ann2,ann3) = getTypes x1 ann1 ++ getTypes x2 ann2 ++ getTypes x3 ann3 + +instance (LiftArgs a,LiftArgs b,LiftArgs c) => LiftArgs (a,b,c) where + type Unpacked (a,b,c) = (Unpacked a,Unpacked b,Unpacked c) + liftArgs (x,y,z) ~(a1,a2,a3) = (liftArgs x a1,liftArgs y a2,liftArgs z a3) + unliftArgs (x,y,z) f = do + rx <- unliftArgs x f + ry <- unliftArgs y f + rz <- unliftArgs z f + return (rx,ry,rz) + +instance (Args a,Args b,Args c,Args d) => Args (a,b,c,d) where + type ArgAnnotation (a,b,c,d) = (ArgAnnotation a,ArgAnnotation b,ArgAnnotation c,ArgAnnotation d) + foldExprs f s ~(e1,e2,e3,e4) ~(ann1,ann2,ann3,ann4) = do + ~(s1,e1') <- foldExprs f s e1 ann1 + ~(s2,e2') <- foldExprs f s1 e2 ann2 + ~(s3,e3') <- foldExprs f s2 e3 ann3 + ~(s4,e4') <- foldExprs f s3 e4 ann4 + return (s4,(e1',e2',e3',e4')) + foldsExprs f s args ~(ann1,ann2,ann3,ann4) = do + ~(s1,e1,r1) <- foldsExprs f s (fmap (\(~(e1,_,_,_),b) -> (e1,b)) args) ann1 + ~(s2,e2,r2) <- foldsExprs f s1 (fmap (\(~(_,e2,_,_),b) -> (e2,b)) args) ann2 + ~(s3,e3,r3) <- foldsExprs f s2 (fmap (\(~(_,_,e3,_),b) -> (e3,b)) args) ann3 + ~(s4,e4,r4) <- foldsExprs f s3 (fmap (\(~(_,_,_,e4),b) -> (e4,b)) args) ann4 + return (s4,zip4 e1 e2 e3 e4,(r1,r2,r3,r4)) + extractArgAnnotation ~(e1,e2,e3,e4) + = (extractArgAnnotation e1, + extractArgAnnotation e2, + extractArgAnnotation e3, + extractArgAnnotation e4) + toArgs ~(ann1,ann2,ann3,ann4) x = do + (r1,x1) <- toArgs ann1 x + (r2,x2) <- toArgs ann2 x1 + (r3,x3) <- toArgs ann3 x2 + (r4,x4) <- toArgs ann4 x3 + return ((r1,r2,r3,r4),x4) + fromArgs (x1,x2,x3,x4) + = fromArgs x1 ++ + fromArgs x2 ++ + fromArgs x3 ++ + fromArgs x4 + getArgAnnotation (_::(a1,a2,a3,a4)) sorts + = let (ann1,r1) = getArgAnnotation (undefined::a1) sorts + (ann2,r2) = getArgAnnotation (undefined::a2) r1 + (ann3,r3) = getArgAnnotation (undefined::a3) r2 + (ann4,r4) = getArgAnnotation (undefined::a4) r3 + in ((ann1,ann2,ann3,ann4),r4) + getTypes ~(x1,x2,x3,x4) (ann1,ann2,ann3,ann4) + = getTypes x1 ann1 ++ + getTypes x2 ann2 ++ + getTypes x3 ann3 ++ + getTypes x4 ann4 + +instance (LiftArgs a,LiftArgs b,LiftArgs c,LiftArgs d) => LiftArgs (a,b,c,d) where + type Unpacked (a,b,c,d) = (Unpacked a,Unpacked b,Unpacked c,Unpacked d) + liftArgs (x1,x2,x3,x4) ~(a1,a2,a3,a4) = (liftArgs x1 a1,liftArgs x2 a2,liftArgs x3 a3,liftArgs x4 a4) + unliftArgs (x1,x2,x3,x4) f = do + r1 <- unliftArgs x1 f + r2 <- unliftArgs x2 f + r3 <- unliftArgs x3 f + r4 <- unliftArgs x4 f + return (r1,r2,r3,r4) + +instance (Args a,Args b,Args c,Args d,Args e) => Args (a,b,c,d,e) where + type ArgAnnotation (a,b,c,d,e) = (ArgAnnotation a,ArgAnnotation b,ArgAnnotation c,ArgAnnotation d,ArgAnnotation e) + foldExprs f s ~(e1,e2,e3,e4,e5) ~(ann1,ann2,ann3,ann4,ann5) = do + ~(s1,e1') <- foldExprs f s e1 ann1 + ~(s2,e2') <- foldExprs f s1 e2 ann2 + ~(s3,e3') <- foldExprs f s2 e3 ann3 + ~(s4,e4') <- foldExprs f s3 e4 ann4 + ~(s5,e5') <- foldExprs f s4 e5 ann5 + return (s5,(e1',e2',e3',e4',e5')) + foldsExprs f s args ~(ann1,ann2,ann3,ann4,ann5) = do + ~(s1,e1,r1) <- foldsExprs f s (fmap (\(~(e1,_,_,_,_),b) -> (e1,b)) args) ann1 + ~(s2,e2,r2) <- foldsExprs f s1 (fmap (\(~(_,e2,_,_,_),b) -> (e2,b)) args) ann2 + ~(s3,e3,r3) <- foldsExprs f s2 (fmap (\(~(_,_,e3,_,_),b) -> (e3,b)) args) ann3 + ~(s4,e4,r4) <- foldsExprs f s3 (fmap (\(~(_,_,_,e4,_),b) -> (e4,b)) args) ann4 + ~(s5,e5,r5) <- foldsExprs f s4 (fmap (\(~(_,_,_,_,e5),b) -> (e5,b)) args) ann5 + return (s5,zip5 e1 e2 e3 e4 e5,(r1,r2,r3,r4,r5)) + extractArgAnnotation ~(e1,e2,e3,e4,e5) + = (extractArgAnnotation e1, + extractArgAnnotation e2, + extractArgAnnotation e3, + extractArgAnnotation e4, + extractArgAnnotation e5) + toArgs ~(ann1,ann2,ann3,ann4,ann5) x = do + (r1,x1) <- toArgs ann1 x + (r2,x2) <- toArgs ann2 x1 + (r3,x3) <- toArgs ann3 x2 + (r4,x4) <- toArgs ann4 x3 + (r5,x5) <- toArgs ann5 x4 + return ((r1,r2,r3,r4,r5),x5) + fromArgs (x1,x2,x3,x4,x5) + = fromArgs x1 ++ + fromArgs x2 ++ + fromArgs x3 ++ + fromArgs x4 ++ + fromArgs x5 + getArgAnnotation (_::(a1,a2,a3,a4,a5)) sorts + = let (ann1,r1) = getArgAnnotation (undefined::a1) sorts + (ann2,r2) = getArgAnnotation (undefined::a2) r1 + (ann3,r3) = getArgAnnotation (undefined::a3) r2 + (ann4,r4) = getArgAnnotation (undefined::a4) r3 + (ann5,r5) = getArgAnnotation (undefined::a5) r4 + in ((ann1,ann2,ann3,ann4,ann5),r5) + getTypes ~(x1,x2,x3,x4,x5) (ann1,ann2,ann3,ann4,ann5) + = getTypes x1 ann1 ++ + getTypes x2 ann2 ++ + getTypes x3 ann3 ++ + getTypes x4 ann4 ++ + getTypes x5 ann5 + +instance (LiftArgs a,LiftArgs b,LiftArgs c,LiftArgs d,LiftArgs e) => LiftArgs (a,b,c,d,e) where + type Unpacked (a,b,c,d,e) = (Unpacked a,Unpacked b,Unpacked c,Unpacked d,Unpacked e) + liftArgs (x1,x2,x3,x4,x5) ~(a1,a2,a3,a4,a5) = (liftArgs x1 a1,liftArgs x2 a2,liftArgs x3 a3,liftArgs x4 a4,liftArgs x5 a5) + unliftArgs (x1,x2,x3,x4,x5) f = do + r1 <- unliftArgs x1 f + r2 <- unliftArgs x2 f + r3 <- unliftArgs x3 f + r4 <- unliftArgs x4 f + r5 <- unliftArgs x5 f + return (r1,r2,r3,r4,r5) + +instance (Args a,Args b,Args c,Args d,Args e,Args f) => Args (a,b,c,d,e,f) where + type ArgAnnotation (a,b,c,d,e,f) = (ArgAnnotation a,ArgAnnotation b,ArgAnnotation c,ArgAnnotation d,ArgAnnotation e,ArgAnnotation f) + foldExprs f s ~(e1,e2,e3,e4,e5,e6) ~(ann1,ann2,ann3,ann4,ann5,ann6) = do + ~(s1,e1') <- foldExprs f s e1 ann1 + ~(s2,e2') <- foldExprs f s1 e2 ann2 + ~(s3,e3') <- foldExprs f s2 e3 ann3 + ~(s4,e4') <- foldExprs f s3 e4 ann4 + ~(s5,e5') <- foldExprs f s4 e5 ann5 + ~(s6,e6') <- foldExprs f s5 e6 ann6 + return (s6,(e1',e2',e3',e4',e5',e6')) + foldsExprs f s args ~(ann1,ann2,ann3,ann4,ann5,ann6) = do + ~(s1,e1,r1) <- foldsExprs f s (fmap (\(~(e1,_,_,_,_,_),b) -> (e1,b)) args) ann1 + ~(s2,e2,r2) <- foldsExprs f s1 (fmap (\(~(_,e2,_,_,_,_),b) -> (e2,b)) args) ann2 + ~(s3,e3,r3) <- foldsExprs f s2 (fmap (\(~(_,_,e3,_,_,_),b) -> (e3,b)) args) ann3 + ~(s4,e4,r4) <- foldsExprs f s3 (fmap (\(~(_,_,_,e4,_,_),b) -> (e4,b)) args) ann4 + ~(s5,e5,r5) <- foldsExprs f s4 (fmap (\(~(_,_,_,_,e5,_),b) -> (e5,b)) args) ann5 + ~(s6,e6,r6) <- foldsExprs f s5 (fmap (\(~(_,_,_,_,_,e6),b) -> (e6,b)) args) ann6 + return (s6,zip6 e1 e2 e3 e4 e5 e6,(r1,r2,r3,r4,r5,r6)) + extractArgAnnotation ~(e1,e2,e3,e4,e5,e6) + = (extractArgAnnotation e1, + extractArgAnnotation e2, + extractArgAnnotation e3, + extractArgAnnotation e4, + extractArgAnnotation e5, + extractArgAnnotation e6) + toArgs ~(ann1,ann2,ann3,ann4,ann5,ann6) x = do + (r1,x1) <- toArgs ann1 x + (r2,x2) <- toArgs ann2 x1 + (r3,x3) <- toArgs ann3 x2 + (r4,x4) <- toArgs ann4 x3 + (r5,x5) <- toArgs ann5 x4 + (r6,x6) <- toArgs ann6 x5 + return ((r1,r2,r3,r4,r5,r6),x6) + fromArgs (x1,x2,x3,x4,x5,x6) + = fromArgs x1 ++ + fromArgs x2 ++ + fromArgs x3 ++ + fromArgs x4 ++ + fromArgs x5 ++ + fromArgs x6 + getArgAnnotation (_::(a1,a2,a3,a4,a5,a6)) sorts + = let (ann1,r1) = getArgAnnotation (undefined::a1) sorts + (ann2,r2) = getArgAnnotation (undefined::a2) r1 + (ann3,r3) = getArgAnnotation (undefined::a3) r2 + (ann4,r4) = getArgAnnotation (undefined::a4) r3 + (ann5,r5) = getArgAnnotation (undefined::a5) r4 + (ann6,r6) = getArgAnnotation (undefined::a6) r5 + in ((ann1,ann2,ann3,ann4,ann5,ann6),r6) + getTypes ~(x1,x2,x3,x4,x5,x6) (ann1,ann2,ann3,ann4,ann5,ann6) + = getTypes x1 ann1 ++ + getTypes x2 ann2 ++ + getTypes x3 ann3 ++ + getTypes x4 ann4 ++ + getTypes x5 ann5 ++ + getTypes x6 ann6 + +instance (LiftArgs a,LiftArgs b,LiftArgs c,LiftArgs d,LiftArgs e,LiftArgs f) => LiftArgs (a,b,c,d,e,f) where + type Unpacked (a,b,c,d,e,f) = (Unpacked a,Unpacked b,Unpacked c,Unpacked d,Unpacked e,Unpacked f) + liftArgs (x1,x2,x3,x4,x5,x6) ~(a1,a2,a3,a4,a5,a6) + = (liftArgs x1 a1,liftArgs x2 a2,liftArgs x3 a3,liftArgs x4 a4,liftArgs x5 a5,liftArgs x6 a6) + unliftArgs (x1,x2,x3,x4,x5,x6) f = do + r1 <- unliftArgs x1 f + r2 <- unliftArgs x2 f + r3 <- unliftArgs x3 f + r4 <- unliftArgs x4 f + r5 <- unliftArgs x5 f + r6 <- unliftArgs x6 f + return (r1,r2,r3,r4,r5,r6) + +instance Args a => Args [a] where + type ArgAnnotation [a] = [ArgAnnotation a] + foldExprs _ s _ [] = return (s,[]) + foldExprs f s ~(x:xs) (ann:anns) = do + (s',x') <- foldExprs f s x ann + (s'',xs') <- foldExprs f s' xs anns + return (s'',x':xs') + foldsExprs f s _ [] = return (s,[],[]) + foldsExprs f s args [ann] = do + let args_heads = fmap (\(xs,b) -> (head xs,b)) args + ~(s1,res_heads,zhead) <- foldsExprs f s args_heads ann + return (s1,fmap (\x -> [x]) res_heads,[zhead]) + foldsExprs f s args (ann:anns) = do + let args_heads = fmap (\(xs,b) -> (head xs,b)) args + args_tails = fmap (\(xs,b) -> (tail xs,b)) args + ~(s1,res_heads,zhead) <- foldsExprs f s args_heads ann + ~(s2,res_tails,ztail) <- foldsExprs f s1 args_tails anns + return (s2,zipWith (:) res_heads res_tails,zhead:ztail) + extractArgAnnotation = fmap extractArgAnnotation + toArgs [] xs = Just ([],xs) + toArgs (ann:anns) x = do + (r,x') <- toArgs ann x + (rs,x'') <- toArgs anns x' + return (r:rs,x'') + fromArgs xs = concat $ fmap fromArgs xs + getArgAnnotation _ [] = ([],[]) + getArgAnnotation (_::[a]) sorts = let (x,r1) = getArgAnnotation (undefined::a) sorts + (xs,r2) = getArgAnnotation (undefined::[a]) r1 + in (x:xs,r2) + getTypes _ [] = [] + getTypes ~(x:xs) (ann:anns) = getTypes x ann ++ getTypes xs anns + +instance (Typeable a,Show a,Args b,Ord a) => Args (Map a b) where + type ArgAnnotation (Map a b) = Map a (ArgAnnotation b) + foldExprs f s mp mp_ann = foldlM (\(s',cmp) (k,ann) -> do + let el = case Map.lookup k mp of + Nothing -> error $ "smtlib2: Map annotation contains key "++ + show k++ + " but it is not in the map. (Map annotation: "++ + show (Map.keys mp_ann)++ + ", map: "++ + show (Map.keys mp) + Just x -> x + (s'',el') <- foldExprs f s' el ann + return (s'',Map.insert k el' cmp) + ) (s,Map.empty) (Map.toList mp_ann) + foldsExprs f s args mp_ann = do + let lst_ann = Map.toAscList mp_ann + lst = fmap (\(mp,extra) -> ([ mp Map.! k | (k,_) <- lst_ann ],extra) + ) args + (ns,lst',lst_merged) <- foldsExprs f s lst (fmap snd lst_ann) + return (ns,fmap (\lst'' -> Map.fromAscList $ zip (fmap fst lst_ann) lst'' + ) lst',Map.fromAscList $ zip (fmap fst lst_ann) lst_merged) + extractArgAnnotation = fmap extractArgAnnotation + toArgs mp_ann exprs = case Map.mapAccum (\cst ann -> case cst of + Nothing -> (Nothing,undefined) + Just rest -> case toArgs ann rest of + Nothing -> (Nothing,undefined) + Just (res,rest') -> (Just rest',res) + ) (Just exprs) mp_ann of + (Nothing,_) -> Nothing + (Just rest,mp) -> Just (mp,rest) + fromArgs exprs = concat $ fmap fromArgs $ Map.elems exprs + getTypes (_::Map a b) anns = concat [ getTypes (undefined::b) ann | (_,ann) <- Map.toAscList anns ] + getArgAnnotation _ sorts = (Map.empty,sorts) + +instance (Args a,Args b) => Args (Either a b) where + type ArgAnnotation (Either a b) = Either (ArgAnnotation a) (ArgAnnotation b) + foldExprs f s ~(Left x) (Left ann) = do + (ns,res) <- foldExprs f s x ann + return (ns,Left res) + foldExprs f s ~(Right x) (Right ann) = do + (ns,res) <- foldExprs f s x ann + return (ns,Right res) + foldsExprs f s lst (Left ann) = do + (ns,ress,res) <- foldsExprs f s (fmap (\(x,p) -> (case x of + Left x' -> x',p)) lst) ann + return (ns,fmap Left ress,Left res) + foldsExprs f s lst (Right ann) = do + (ns,ress,res) <- foldsExprs f s (fmap (\(x,p) -> (case x of + Right x' -> x',p)) lst) ann + return (ns,fmap Right ress,Right res) + extractArgAnnotation (Left x) = Left $ extractArgAnnotation x + extractArgAnnotation (Right x) = Right $ extractArgAnnotation x + toArgs (Left ann) exprs = do + (res,rest) <- toArgs ann exprs + return (Left res,rest) + toArgs (Right ann) exprs = do + (res,rest) <- toArgs ann exprs + return (Right res,rest) + fromArgs (Left xs) = fromArgs xs + fromArgs (Right xs) = fromArgs xs + getTypes (_::Either a b) (Left ann) = getTypes (undefined::a) ann + getTypes (_::Either a b) (Right ann) = getTypes (undefined::b) ann + getArgAnnotation _ _ = error "smtlib2: getArgAnnotation undefined for Either" + +instance Args a => Args (Maybe a) where + type ArgAnnotation (Maybe a) = Maybe (ArgAnnotation a) + foldExprs _ s _ Nothing = return (s,Nothing) + foldExprs f s ~(Just x) (Just ann) = do + (ns,res) <- foldExprs f s x ann + return (ns,Just res) + foldsExprs _ s lst Nothing = return (s,fmap (const Nothing) lst,Nothing) + foldsExprs f s lst (Just ann) = do + (ns,ress,res) <- foldsExprs f s (fmap (\(x,p) -> (case x of + Just x' -> x',p)) lst) ann + return (ns,fmap Just ress,Just res) + extractArgAnnotation = fmap extractArgAnnotation + toArgs Nothing exprs = Just (Nothing,exprs) + toArgs (Just ann) exprs = do + (res,rest) <- toArgs ann exprs + return (Just res,rest) + fromArgs Nothing = [] + fromArgs (Just x) = fromArgs x + getTypes _ Nothing = [] + getTypes (_::Maybe a) (Just ann) = getTypes (undefined::a) ann + getArgAnnotation _ _ = error "smtlib2: getArgAnnotation undefined for Maybe" + +instance LiftArgs a => LiftArgs [a] where + type Unpacked [a] = [Unpacked a] + liftArgs _ [] = [] + liftArgs ~(x:xs) (ann:anns) = liftArgs x ann:liftArgs xs anns + unliftArgs [] _ = return [] + unliftArgs (x:xs) f = do + x' <- unliftArgs x f + xs' <- unliftArgs xs f + return (x':xs') + +instance (Typeable a,Show a,Ord a,LiftArgs b) => LiftArgs (Map a b) where + type Unpacked (Map a b) = Map a (Unpacked b) + liftArgs mp ann = Map.mapWithKey (\k ann' -> liftArgs (mp Map.! k) ann') ann + unliftArgs mp f = mapM (\el -> unliftArgs el f) mp + +instance (LiftArgs a,LiftArgs b) => LiftArgs (Either a b) where + type Unpacked (Either a b) = Either (Unpacked a) (Unpacked b) + liftArgs ~(Left x) (Left ann) = Left (liftArgs x ann) + liftArgs ~(Right x) (Right ann) = Right (liftArgs x ann) + unliftArgs (Left x) f = do + res <- unliftArgs x f + return $ Left res + unliftArgs (Right x) f = do + res <- unliftArgs x f + return $ Right res + +instance LiftArgs a => LiftArgs (Maybe a) where + type Unpacked (Maybe a) = Maybe (Unpacked a) + liftArgs _ Nothing = Nothing + liftArgs ~(Just x) (Just ann) = Just (liftArgs x ann) + unliftArgs Nothing _ = return Nothing + unliftArgs (Just x) f = do + res <- unliftArgs x f + return (Just res) + +instance SMTType a => SMTType (Maybe a) where + type SMTAnnotation (Maybe a) = SMTAnnotation a + getSort u ann = Fix $ NamedSort "Maybe" [getSort (undefArg u) ann] + asDataType _ _ = Just ("Maybe", + TypeCollection { argCount = 1 + , dataTypes = [dtMaybe] + }) + getProxyArgs (_::Maybe t) ann = [ProxyArg (undefined::t) ann] + annotationFromSort u (Fix (NamedSort "Maybe" [argSort])) = annotationFromSort (undefArg u) argSort + asValueType (_::Maybe x) ann f = asValueType (undefined::x) ann $ + \(_::y) ann' -> f (undefined::Maybe y) ann' + defaultExpr ann = withUndef $ + \u -> App (SMTConstructor (nothing' ann)) () + where + withUndef :: (a -> SMTExpr (Maybe a)) -> SMTExpr (Maybe a) + withUndef f = f undefined + +dtMaybe :: DataType +dtMaybe = DataType { dataTypeName = "Maybe" + , dataTypeConstructors = [conNothing, + conJust] + , dataTypeGetUndefined = \sorts f -> case sorts of + [s] -> withProxyArg s $ + \(_::t) ann -> f (undefined::Maybe t) ann + } + +conNothing :: Constr +conNothing + = Constr { conName = "Nothing" + , conFields = [] + , construct = \[Just prx] [] f + -> withProxyArg prx $ + \(_::t) ann -> f [prx] (Nothing::Maybe t) ann + , conTest = \args x -> case args of + [s] -> withProxyArg s $ + \(_::t) _ -> case cast x of + Just (Nothing::Maybe t) -> True + _ -> False + } + +conJust :: Constr +conJust + = Constr { conName = "Just" + , conFields = [fieldFromJust] + , construct = \sort args f + -> case args of + [v] -> withAnyValue v $ + \_ (rv::t) ann + -> f [ProxyArg (undefined::t) ann] (Just rv) ann + , conTest = \args x -> case args of + [s] -> withProxyArg s $ + \(_::t) _ -> case cast x of + Just (Just (_::t)) -> True + _ -> False + } + +nothing' :: SMTType a => SMTAnnotation a -> Constructor () (Maybe a) +nothing' ann = withUndef $ + \u -> Constructor [ProxyArg u ann] dtMaybe conNothing + where + withUndef :: (a -> Constructor () (Maybe a)) -> Constructor () (Maybe a) + withUndef f = f undefined + +just' :: SMTType a => SMTAnnotation a -> Constructor (SMTExpr a) (Maybe a) +just' ann = withUndef $ + \u -> Constructor [ProxyArg u ann] dtMaybe conJust + where + withUndef :: (a -> Constructor (SMTExpr a) (Maybe a)) -> Constructor (SMTExpr a) (Maybe a) + withUndef f = f undefined + +fieldFromJust :: DataField +fieldFromJust = DataField { fieldName = "fromJust" + , fieldSort = Fix $ ArgumentSort 0 + , fieldGet = \args x f + -> case args of + [s] -> withProxyArg s $ + \(_::t) ann + -> f (case cast x of + Just (arg::Maybe t) -> fromJust arg) ann + } + +instance SMTValue a => SMTValue (Maybe a) where + unmangle = case unmangle of + PrimitiveUnmangling p + -> PrimitiveUnmangling (\val ann -> case val of + ConstrValue "Nothing" [] _ -> Just Nothing + ConstrValue "Just" [arg] _ + -> case p arg ann of + Just v -> Just (Just v) + Nothing -> Nothing + _ -> Nothing) + ComplexUnmangling p + -> ComplexUnmangling $ \f (expr::SMTExpr (Maybe t)) ann -> do + isNothing <- f (App (SMTConTest + (Constructor [ProxyArg (undefined::t) (extractAnnotation expr)] + dtMaybe conNothing :: Constructor () (Maybe a))) expr + ) () + if isNothing + then return (Just Nothing) + else do + val <- p f (App (SMTFieldSel (Field [ProxyArg (undefined::t) (extractAnnotation expr)] dtMaybe conJust fieldFromJust)) expr) ann + case val of + Nothing -> return Nothing + Just val' -> return (Just (Just val')) + mangle = case mangle of + PrimitiveMangling p + -> PrimitiveMangling $ + \val ann -> case val of + (Nothing::Maybe t) -> ConstrValue "Nothing" [] (Just ("Maybe",[getSort (undefined::t) ann])) + Just x -> ConstrValue "Just" [p x ann] Nothing + ComplexMangling p + -> ComplexMangling $ + \(val::Maybe t) ann -> case val of + Just x -> App (SMTConstructor + (Constructor [ProxyArg (undefined::t) ann] dtMaybe conJust)) + (p x ann) + Nothing -> App (SMTConstructor + (Constructor [ProxyArg (undefined::t) ann] + dtMaybe conNothing :: Constructor () (Maybe t))) + () + +-- | Get an undefined value of the type argument of a type. +undefArg :: b a -> a +undefArg _ = undefined + +instance (Typeable a,SMTType a) => SMTType [a] where + type SMTAnnotation [a] = SMTAnnotation a + getSort u ann = Fix (NamedSort "List" [getSort (undefArg u) ann]) + asDataType _ _ = Just ("List", + TypeCollection { argCount = 1 + , dataTypes = [dtList] }) + getProxyArgs (_::[t]) ann = [ProxyArg (undefined::t) ann] + annotationFromSort u (Fix (NamedSort "List" [sort])) = annotationFromSort (undefArg u) sort + asValueType (_::[a]) ann f = asValueType (undefined::a) ann $ + \(_::b) ann' -> f (undefined::[b]) ann' + defaultExpr ann = App (SMTConstructor (nil' ann)) () + +dtList :: DataType +dtList = DataType { dataTypeName = "List" + , dataTypeConstructors = [conNil,conInsert] + , dataTypeGetUndefined = \args f -> case args of + [s] -> withProxyArg s (\(_::t) ann -> f (undefined::[t]) ann) + } + +conNil :: Constr +conNil = Constr { conName = "nil" + , conFields = [] + , construct = \[Just sort] args f + -> withProxyArg sort $ + \(_::t) ann -> f [sort] ([]::[t]) ann + , conTest = \args x -> case args of + [s] -> withProxyArg s $ + \(_::t) _ -> case cast x of + Just ([]::[t]) -> True + _ -> False + } + +conInsert :: Constr +conInsert = Constr { conName = "insert" + , conFields = [fieldHead + ,fieldTail] + , construct = \sort args f + -> case args of + [h,t] -> withAnyValue h $ + \_ (v::t) ann + -> case castAnyValue t of + Just (vs,_) -> f [ProxyArg (undefined::t) ann] (v:vs) ann + , conTest = \args x -> case args of + [s] -> withProxyArg s $ + \(_::t) _ -> case cast x of + Just ((_:_)::[t]) -> True + _ -> False + } + +insert' :: SMTType a => SMTAnnotation a -> Constructor (SMTExpr a,SMTExpr [a]) [a] +insert' ann = withUndef $ + \u -> Constructor [ProxyArg u ann] dtList conInsert + where + withUndef :: (a -> Constructor (SMTExpr a,SMTExpr [a]) [a]) -> Constructor (SMTExpr a,SMTExpr [a]) [a] + withUndef f = f undefined + +nil' :: SMTType a => SMTAnnotation a -> Constructor () [a] +nil' ann = withUndef $ + \u -> Constructor [ProxyArg u ann] dtList conNil + where + withUndef :: (a -> Constructor () [a]) -> Constructor () [a] + withUndef f = f undefined + +fieldHead :: DataField +fieldHead = DataField { fieldName = "head" + , fieldSort = Fix (ArgumentSort 0) + , fieldGet = \args x f -> case args of + [s] -> withProxyArg s $ + \(_::t) ann + -> case cast x of + Just (ys::[t]) -> f (head ys) ann + } + +fieldTail :: DataField +fieldTail = DataField { fieldName = "tail" + , fieldSort = Fix (NormalSort (NamedSort "List" [Fix (ArgumentSort 0)])) + , fieldGet = \args x f -> case args of + [s] -> withProxyArg s $ + \(_::t) ann + -> case cast x of + Just (ys::[t]) -> f (tail ys) ann + } + +instance (Typeable a,SMTValue a) => SMTValue [a] where + unmangle = case unmangle of + PrimitiveUnmangling p + -> PrimitiveUnmangling $ pUnmangle p + ComplexUnmangling p + -> ComplexUnmangling $ cUnmangle p + where + pUnmangle _ (ConstrValue "nil" [] _) ann = Just [] + pUnmangle p (ConstrValue "insert" [h,t] _) ann = do + h' <- p h ann + t' <- pUnmangle p t ann + return (h':t') + cUnmangle :: Monad m + => ((forall b. SMTValue b => SMTExpr b -> SMTAnnotation b -> m b) + -> SMTExpr a -> SMTAnnotation a -> m (Maybe a)) + -> (forall b. SMTValue b => SMTExpr b -> SMTAnnotation b -> m b) + -> SMTExpr [a] -> SMTAnnotation a -> m (Maybe [a]) + cUnmangle c f (expr::SMTExpr [t]) ann = do + isNil <- f (App (SMTConTest + (Constructor [ProxyArg (undefined::t) ann] dtList conNil + ::Constructor () [t])) + expr) () + if isNil + then return (Just []) + else do + h <- c f (App (SMTFieldSel (Field [ProxyArg (undefined::t) ann] dtList conInsert fieldHead)) + expr) ann + t <- cUnmangle c f (App (SMTFieldSel (Field [ProxyArg (undefined::t) ann] dtList conInsert fieldTail)) expr) ann + return $ do + h' <- h + t' <- t + return $ h':t' + mangle = case mangle of + PrimitiveMangling p + -> PrimitiveMangling $ pMangle p + ComplexMangling p + -> ComplexMangling $ cMangle p + where + pMangle _ ([]::[t]) ann = ConstrValue "nil" [] (Just ("List",[getSort (undefined::t) ann])) + pMangle p (x:xs) ann = ConstrValue "insert" [p x ann,pMangle p xs ann] Nothing + cMangle :: (a -> SMTAnnotation a -> SMTExpr a) + -> [a] -> SMTAnnotation a -> SMTExpr [a] + cMangle c ([]::[t]) ann + = App (SMTConstructor (Constructor [ProxyArg (undefined::t) ann] dtList conNil)) () + cMangle c ((x::t):xs) ann + = App (SMTConstructor (Constructor [ProxyArg (undefined::t) ann] dtList conInsert)) + (c x ann,cMangle c xs ann) + +-- BitVector implementation + +instance SMTType (BitVector BVUntyped) where + type SMTAnnotation (BitVector BVUntyped) = Integer + getSort _ l = Fix (BVSort l True) + annotationFromSort _ (Fix (BVSort l _)) = l + asValueType x ann f = Just $ f x ann + defaultExpr bw = Const (BitVector 0) bw + +instance IsBitVector BVUntyped where + getBVSize _ = id + +instance SMTValue (BitVector BVUntyped) where + unmangle = PrimitiveUnmangling $ + \val _ -> case val of + BVValue _ v -> Just (BitVector v) + _ -> Nothing + mangle = PrimitiveMangling $ + \(BitVector v) l -> BVValue l v + +instance TypeableNat n => SMTType (BitVector (BVTyped n)) where + type SMTAnnotation (BitVector (BVTyped n)) = () + getSort _ _ = Fix (BVSort (reflectNat (Proxy::Proxy n) 0) False) + annotationFromSort _ _ = () + asValueType x ann f = Just $ f x ann + defaultExpr _ = Const (BitVector 0) () + +instance TypeableNat n => IsBitVector (BVTyped n) where + getBVSize (_::Proxy (BVTyped n)) _ = reflectNat (Proxy::Proxy n) 0 + +instance TypeableNat n => SMTValue (BitVector (BVTyped n)) where + unmangle = PrimitiveUnmangling $ + \val _ -> case val of + BVValue w v + | (reflectNat (Proxy::Proxy n) 0)==w -> Just (BitVector v) + | otherwise -> Nothing + _ -> Nothing + mangle = PrimitiveMangling $ + \(BitVector v) _ -> BVValue (reflectNat (Proxy::Proxy n) 0) v + +bvUnsigned :: IsBitVector a => BitVector a -> SMTAnnotation (BitVector a) -> Integer +bvUnsigned (BitVector x) _ = x + +bvSigned :: IsBitVector a => BitVector a -> SMTAnnotation (BitVector a) -> Integer +bvSigned (BitVector x::BitVector a) ann + = let sz = getBVSize (Proxy::Proxy a) ann + in if x < 2^(sz-1) + then x + else x-2^sz + +bvRestrict :: IsBitVector a => BitVector a -> SMTAnnotation (BitVector a) -> BitVector a +bvRestrict (BitVector x::BitVector a) ann + = let sz = getBVSize (Proxy::Proxy a) ann + in BitVector (x `mod` (2^sz)) + +instance TypeableNat n => Num (BitVector (BVTyped n)) where + (+) (BitVector x) (BitVector y) = BitVector (x+y) + (-) (BitVector x) (BitVector y) = BitVector (x-y) + (*) (BitVector x) (BitVector y) = BitVector (x*y) + negate (BitVector x) = BitVector (negate x) + abs (BitVector x) = BitVector (abs x) + signum (BitVector x) = BitVector (signum x) + fromInteger i = BitVector i + +instance TypeableNat n => Num (SMTExpr (BitVector (BVTyped n))) where + (+) (x::SMTExpr (BitVector (BVTyped n))) y = App (SMTBVBin BVAdd) (x,y) + (-) (x::SMTExpr (BitVector (BVTyped n))) y = App (SMTBVBin BVSub) (x,y) + (*) (x::SMTExpr (BitVector (BVTyped n))) y = App (SMTBVBin BVMul) (x,y) + negate (x::SMTExpr (BitVector (BVTyped n))) = App (SMTBVUn BVNeg) x + abs (x::SMTExpr (BitVector (BVTyped n))) = App SMTITE (App (SMTBVComp BVUGT) (x,Const (BitVector 0) ()),x,App (SMTBVUn BVNeg) x) + signum (x::SMTExpr (BitVector (BVTyped n))) = App SMTITE (App (SMTBVComp BVUGT) (x,Const (BitVector 0) ()),Const (BitVector 1) (),Const (BitVector (-1)) ()) + fromInteger i = Const (BitVector i) () + +instance Extractable BVUntyped BVUntyped where + extractAnn _ _ len _ = len + getExtractLen _ _ len = len + +instance TypeableNat n => Extractable (BVTyped n) BVUntyped where + extractAnn _ _ len _ = len + getExtractLen _ _ len = len + +instance TypeableNat n => Extractable BVUntyped (BVTyped n) where + extractAnn _ _ _ _ = () + getExtractLen _ (_::BVTyped n) _ = reflectNat (Proxy::Proxy n) 0 + +instance (TypeableNat n1,TypeableNat n2) => Extractable (BVTyped n1) (BVTyped n2) where + extractAnn _ _ _ _ = () + getExtractLen _ (_::BVTyped n) _ = reflectNat (Proxy::Proxy n) 0 + +withSort :: DataTypeInfo -> Sort -> (forall t. SMTType t => t -> SMTAnnotation t -> r) -> r +withSort _ (Fix BoolSort) f = f (undefined::Bool) () +withSort _ (Fix IntSort) f = f (undefined::Integer) () +withSort _ (Fix RealSort) f = f (undefined::Rational) () +withSort _ (Fix (BVSort { bvSortWidth = w + , bvSortUntyped = unt })) f + = if unt + then f (undefined::BitVector BVUntyped) w + else reifyNat w (\(_::Proxy tp) -> f (undefined::BitVector (BVTyped tp)) ()) +withSort mp (Fix (ArraySort args res)) f + = withSorts mp args $ \(_::rargs) argAnn + -> withSort mp res $ \(_::rres) resAnn + -> f (undefined::SMTArray rargs rres) (argAnn,resAnn) +withSort mp (Fix (NamedSort name args)) f + = case Map.lookup name (datatypes mp) of + Just (decl,_) -> dataTypeGetUndefined decl + (fmap (\s -> withSort mp s ProxyArg) args) f + Nothing -> error $ "smtlib2: Datatype "++name++" not defined." + +withNumSort :: DataTypeInfo -> Sort -> (forall t. (SMTType t,Num t) => t -> SMTAnnotation t -> r) -> Maybe r +withNumSort _ (Fix IntSort) f = Just $ f (undefined::Integer) () +withNumSort _ (Fix RealSort) f = Just $ f (undefined::Rational) () +withNumSort _ _ _ = Nothing + +withSorts :: DataTypeInfo -> [Sort] -> (forall arg . Liftable arg => arg -> ArgAnnotation arg -> r) -> r +withSorts mp [x] f = withSort mp x $ \(_::t) ann -> f (undefined::SMTExpr t) ann +withSorts mp [x0,x1] f + = withSort mp x0 $ + \(_::r1) ann1 + -> withSort mp x1 $ + \(_::r2) ann2 -> f (undefined::(SMTExpr r1,SMTExpr r2)) (ann1,ann2) +withSorts mp [x0,x1,x2] f + = withSort mp x0 $ + \(_::r1) ann1 + -> withSort mp x1 $ + \(_::r2) ann2 + -> withSort mp x2 $ + \(_::r3) ann3 -> f (undefined::(SMTExpr r1,SMTExpr r2,SMTExpr r3)) (ann1,ann2,ann3) + +withArraySort :: DataTypeInfo -> [Sort] -> Sort -> (forall i v. (Liftable i,SMTType v) => SMTArray i v -> (ArgAnnotation i,SMTAnnotation v) -> a) -> a +withArraySort mp idx v f + = withSorts mp idx $ + \(_::i) anni + -> withSort mp v $ + \(_::vt) annv -> f (undefined::SMTArray i vt) (anni,annv) + +-- | Recursively fold a monadic function over all sub-expressions of this expression +foldExprM :: (SMTType a,Monad m) => (forall t. SMTType t => s -> SMTExpr t -> m (s,[SMTExpr t])) + -> s -> SMTExpr a -> m (s,[SMTExpr a]) +foldExprM f s (Forall lvl args body) = do + (s',exprs1) <- foldExprM f s body + return (s',[ Forall lvl args body' + | body' <- exprs1 ]) +foldExprM f s (Exists lvl args body) = do + (s',exprs1) <- foldExprM f s body + return (s',[ Exists lvl args body' + | body' <- exprs1 ]) +foldExprM f s (Let lvl defs body) = do + (s1,defs') <- foldDefs s defs + (s2,body') <- foldExprM f s1 body + return (s2,[ Let lvl defs body + | defs <- defs' + , body <- body' ]) + where + foldDefs s [] = return (s,[[]]) + foldDefs s (d:ds) = do + (s1,d') <- foldExprM f s d + (s2,ds') <- foldDefs s1 ds + return (s2,[ d:ds + | d <- d' + , ds <- ds' ]) +foldExprM f s (App fun arg) = do + (s',args') <- foldArgsM f s arg + return (s',[ App fun arg' + | arg' <- args' ]) +foldExprM f s (Named expr name i) = do + (s',exprs') <- foldExprM f s expr + return (s',[ Named expr' name i + | expr' <- exprs' ]) +foldExprM f s (UntypedExpr e) = do + (s',exprs') <- foldExprM f s e + return (s',[ UntypedExpr e' + | e' <- exprs' ]) +foldExprM f s (UntypedExprValue e) = do + (s',exprs') <- foldExprM f s e + return (s',[ UntypedExprValue e' + | e' <- exprs' ]) +foldExprM f s expr = f s expr + +-- | Recursively fold a monadic function over all sub-expressions of the argument +foldArgsM :: (Args a,Monad m) => (forall t. SMTType t => s -> SMTExpr t -> m (s,[SMTExpr t])) + -> s -> a -> m (s,[a]) +foldArgsM f s arg = do + (ns,res) <- fold s (fromArgs arg) + let res' = fmap (\x -> let Just (x',[]) = toArgs (extractArgAnnotation arg) x + in x' + ) res + return (ns,res') + where + fold cs [] = return (cs,[[]]) + fold cs ((UntypedExpr expr):exprs) = do + (s1,nexprs) <- foldExprM f cs expr + (s2,rest) <- fold s1 exprs + return (s2,[ (UntypedExpr x):xs + | x <- nexprs + , xs <- rest ]) + +-- | Recursively fold a function over all sub-expressions of this expression. +-- It is implemented as a special case of 'foldExprM'. +foldExpr :: SMTType a => (forall t. SMTType t => s -> SMTExpr t -> (s,SMTExpr t)) + -> s -> SMTExpr a -> (s,SMTExpr a) +foldExpr f s expr = case runIdentity $ foldExprM (\s' expr' -> let (ns,r) = f s' expr' + in return (ns,[r])) s expr of + (ns,[r]) -> (ns,r) + + +foldExprMux :: SMTType a => (forall t. SMTType t => s -> SMTExpr t -> (s,[SMTExpr t])) + -> s -> SMTExpr a -> (s,[SMTExpr a]) +foldExprMux f s expr = runIdentity $ foldExprM (\s' expr' -> return $ f s' expr') s expr + +-- | Recursively fold a function over all sub-expressions of the argument. +-- It is implemented as a special case of 'foldArgsM'. +foldArgs :: Args a => (forall t. SMTType t => s -> SMTExpr t -> (s,SMTExpr t)) + -> s -> a -> (s,a) +foldArgs f s expr = case runIdentity $ foldArgsM (\s' expr' -> let (ns,expr'') = f s' expr' + in return (ns,[expr''])) s expr of + (ns,[r]) -> (ns,r) + + +foldArgsMux :: Args a => (forall t. SMTType t => s -> SMTExpr t -> (s,[SMTExpr t])) + -> s -> a -> (s,[a]) +foldArgsMux f s expr = runIdentity $ foldArgsM (\s' expr' -> return $ f s' expr') s expr + +instance Args arg => Eq (SMTFunction arg res) where + (==) f1 f2 = compareFun f1 f2 == EQ + +instance Args arg => Ord (SMTFunction arg res) where + compare = compareFun + +compareFun :: (Args a1,Args a2) => SMTFunction a1 r1 -> SMTFunction a2 r2 -> Ordering +compareFun SMTEq SMTEq = EQ +compareFun SMTEq _ = LT +compareFun _ SMTEq = GT +compareFun (SMTMap f1) (SMTMap f2) = compareFun f1 f2 +compareFun (SMTMap _) _ = LT +compareFun _ (SMTMap _) = GT +compareFun (SMTFun i _) (SMTFun j _) = compare i j +compareFun (SMTFun _ _) _ = LT +compareFun _ (SMTFun _ _) = GT +compareFun (SMTBuiltIn n1 _) (SMTBuiltIn n2 _) = compare n1 n2 +compareFun (SMTBuiltIn _ _) _ = LT +compareFun _ (SMTBuiltIn _ _) = GT +compareFun (SMTOrd op1) (SMTOrd op2) = compare op1 op2 +compareFun (SMTOrd _) _ = LT +compareFun _ (SMTOrd _) = GT +compareFun (SMTArith op1) (SMTArith op2) = compare op1 op2 +compareFun SMTMinus SMTMinus = EQ +compareFun SMTMinus _ = LT +compareFun _ SMTMinus = GT +compareFun (SMTIntArith op1) (SMTIntArith op2) = compare op1 op2 +compareFun (SMTIntArith _) _ = LT +compareFun _ (SMTIntArith _) = GT +compareFun SMTDivide SMTDivide = EQ +compareFun SMTDivide _ = LT +compareFun _ SMTDivide = GT +compareFun SMTNeg SMTNeg = EQ +compareFun SMTNeg _ = LT +compareFun _ SMTNeg = GT +compareFun SMTAbs SMTAbs = EQ +compareFun SMTAbs _ = LT +compareFun _ SMTAbs = GT +compareFun SMTNot SMTNot = EQ +compareFun SMTNot _ = LT +compareFun _ SMTNot = GT +compareFun (SMTLogic op1) (SMTLogic op2) = compare op1 op2 +compareFun (SMTLogic _) _ = LT +compareFun _ (SMTLogic _) = GT +compareFun SMTDistinct SMTDistinct = EQ +compareFun SMTDistinct _ = LT +compareFun _ SMTDistinct = GT +compareFun SMTToReal SMTToReal = EQ +compareFun SMTToReal _ = LT +compareFun _ SMTToReal = GT +compareFun SMTToInt SMTToInt = EQ +compareFun SMTToInt _ = LT +compareFun _ SMTToInt = GT +compareFun SMTITE SMTITE = EQ +compareFun SMTITE _ = LT +compareFun _ SMTITE = GT +compareFun (SMTBVComp op1) (SMTBVComp op2) = compare op1 op2 +compareFun (SMTBVComp _) _ = LT +compareFun _ (SMTBVComp _) = GT +compareFun (SMTBVBin op1) (SMTBVBin op2) = compare op1 op2 +compareFun (SMTBVBin _) _ = LT +compareFun _ (SMTBVBin _) = GT +compareFun (SMTBVUn op1) (SMTBVUn op2) = compare op1 op2 +compareFun (SMTBVUn _) _ = LT +compareFun _ (SMTBVUn _) = GT +compareFun SMTSelect SMTSelect = EQ +compareFun SMTSelect _ = LT +compareFun _ SMTSelect = GT +compareFun SMTStore SMTStore = EQ +compareFun SMTStore _ = LT +compareFun _ SMTStore = GT +compareFun (SMTConstArray _) (SMTConstArray _) = EQ +compareFun (SMTConstArray _) _ = LT +compareFun _ (SMTConstArray _) = GT +compareFun SMTConcat SMTConcat = EQ +compareFun SMTConcat _ = LT +compareFun _ SMTConcat = GT +compareFun (SMTExtract (_::Proxy start1) (_::Proxy len1)) (SMTExtract (_::Proxy start2) (_::Proxy len2)) + = compare (typeOf (undefined::start1),typeOf (undefined::len1)) + (typeOf (undefined::start2),typeOf (undefined::len2)) +compareFun (SMTExtract _ _) _ = LT +compareFun _ (SMTExtract _ _) = GT +compareFun (SMTConstructor con1) (SMTConstructor con2) + = compareConstructor con1 con2 +compareFun (SMTConstructor _) _ = LT +compareFun _ (SMTConstructor _) = GT +compareFun (SMTConTest con1) (SMTConTest con2) + = compareConstructor con1 con2 +compareFun (SMTConTest _) _ = LT +compareFun _ (SMTConTest _) = GT +compareFun (SMTFieldSel f1) (SMTFieldSel f2) = compareField f1 f2 +compareFun (SMTFieldSel _) _ = LT +compareFun _ (SMTFieldSel _) = GT +compareFun (SMTDivisible x) (SMTDivisible y) = compare x y +compareFun (SMTDivisible _) _ = LT +compareFun _ (SMTDivisible _) = GT + +compareConstructor :: Constructor arg1 res1 -> Constructor arg2 res2 -> Ordering +compareConstructor (Constructor p1 dt1 con1) (Constructor p2 dt2 con2) + = case compare (dataTypeName dt1) (dataTypeName dt2) of + EQ -> case compare p1 p2 of + EQ -> compare (conName con1) (conName con2) + r -> r + r -> r + +compareField :: Field a1 f1 -> Field a2 f2 -> Ordering +compareField (Field p1 dt1 con1 f1) (Field p2 dt2 con2 f2) + = case compare (dataTypeName dt1) (dataTypeName dt2) of + EQ -> case compare p1 p2 of + EQ -> case compare (conName con1) (conName con2) of + EQ -> compare (fieldName f1) (fieldName f2) + r -> r + r -> r + r -> r + +compareArgs :: (Args a1,Args a2) => a1 -> a2 -> Ordering +compareArgs x y = compare (fromArgs x) (fromArgs y) + +compareExprs :: (SMTType t1,SMTType t2) => SMTExpr t1 -> SMTExpr t2 -> Ordering +compareExprs (UntypedExpr e1) e2 = compareExprs e1 e2 +compareExprs e1 (UntypedExpr e2) = compareExprs e1 e2 +compareExprs (UntypedExprValue e1) e2 = compareExprs e1 e2 +compareExprs e1 (UntypedExprValue e2) = compareExprs e1 e2 +compareExprs (Var i _) (Var j _) = compare i j +compareExprs (Var _ _) _ = LT +compareExprs _ (Var _ _) = GT +compareExprs (QVar lvl1 i1 _) (QVar lvl2 i2 _) = case compare lvl1 lvl2 of + EQ -> compare i1 i2 + r -> r +compareExprs (QVar _ _ _) _ = LT +compareExprs _ (QVar _ _ _) = GT +compareExprs (Const i _) (Const j _) = case cast j of + Just j' -> compare i j' + Nothing -> compare (typeOf i) (typeOf j) +compareExprs (Const _ _) _ = LT +compareExprs _ (Const _ _) = GT +compareExprs (AsArray f1 _) (AsArray f2 _) = compareFun f1 f2 +compareExprs (AsArray _ _) _ = LT +compareExprs _ (AsArray _ _) = GT +compareExprs (Forall lvl1 args1 f1) (Forall lvl2 args2 f2) + = case compare lvl1 lvl2 of + EQ -> case compare args1 args2 of + EQ -> compareExprs f1 f2 + r -> r + r -> r +compareExprs (Forall _ _ _) _ = LT +compareExprs _ (Forall _ _ _) = GT +compareExprs (Exists lvl1 args1 f1) (Exists lvl2 args2 f2) + = case compare lvl1 lvl2 of + EQ -> case compare args1 args2 of + EQ -> compareExprs f1 f2 + r -> r + r -> r +compareExprs (Exists _ _ _) _ = LT +compareExprs _ (Exists _ _ _) = GT +compareExprs (Let lvl1 arg1 f1) (Let lvl2 arg2 f2) + = case compare lvl1 lvl2 of + EQ -> case compare arg1 arg2 of + EQ -> compareExprs f1 f2 + r -> r + r -> r +compareExprs (Let _ _ _) _ = LT +compareExprs _ (Let _ _ _) = GT +compareExprs (App f1 arg1) (App f2 arg2) = case compareFun f1 f2 of + EQ -> compareArgs arg1 arg2 + x -> x +compareExprs (App _ _) _ = LT +compareExprs _ (App _ _) = GT +compareExprs (Named _ n1 i1) (Named _ n2 i2) = compare (n1,i1) (n2,i2) +compareExprs (Named _ _ _) _ = LT +compareExprs _ (Named _ _ _) = GT +compareExprs (InternalObj o1 ann1) (InternalObj o2 ann2) = case compare (typeOf o1) (typeOf o2) of + EQ -> case compare (typeOf ann1) (typeOf ann2) of + EQ -> case cast (o2,ann2) of + Just (o2',ann2') -> compare (o1,ann1) (o2',ann2') + r -> r + r -> r +compareExprs (InternalObj _ _) _ = LT +compareExprs _ (InternalObj _ _) = GT + +instance Eq a => Eq (SMTExpr a) where + (==) x y = case eqExpr x y of + Just True -> True + _ -> False + +instance SMTType t => Ord (SMTExpr t) where + compare = compareExprs + +eqExpr :: SMTExpr a -> SMTExpr a -> Maybe Bool +eqExpr lhs rhs = case (lhs,rhs) of + (Var v1 _,Var v2 _) -> if v1 == v2 + then Just True + else Nothing + (QVar l1 v1 _,QVar l2 v2 _) -> if l1==l2 && v1==v2 + then Just True + else Nothing + (Const v1 _,Const v2 _) -> Just $ v1 == v2 + (AsArray f1 arg1,AsArray f2 arg2) -> case cast f2 of + Nothing -> Nothing + Just f2' -> case cast arg2 of + Nothing -> Nothing + Just arg2' -> if f1 == f2' && arg1 == arg2' + then Just True + else Nothing + (Forall l1 a1 f1,Forall l2 a2 f2) -> if l1==l2 && a1==a2 + then eqExpr f1 f2 + else Nothing + (Exists l1 a1 f1,Exists l2 a2 f2) -> if l1==l2 && a1==a2 + then eqExpr f1 f2 + else Nothing + (Let l1 a1 f1,Let l2 a2 f2) -> if l1==l2 && a1==a2 + then eqExpr f1 f2 + else Nothing + (Named e1 n1 nc1,Named e2 n2 nc2) -> if n1==n2 && nc1 == nc2 + then eqExpr e1 e2 + else Nothing + (App f1 arg1,App f2 arg2) -> case cast f2 of + Nothing -> Nothing + Just f2' -> case cast arg2 of + Nothing -> Nothing + Just arg2' -> if f1 == f2' && arg1 == arg2' + then Just True + else Nothing + (InternalObj o1 ann1,InternalObj o2 ann2) -> case cast (o2,ann2) of + Nothing -> Nothing + Just (o2',ann2') -> Just $ (o1 == o2') && (ann1 == ann2') + (UntypedExpr e1,UntypedExpr e2) -> case cast e2 of + Just e2' -> eqExpr e1 e2' + Nothing -> Just False + (_,_) -> Nothing + +instance Eq (Constructor arg res) where + (Constructor p1 dt1 con1) == (Constructor p2 dt2 con2) + = (dataTypeName dt1 == dataTypeName dt2) && + (p1 == p2) && + (conName con1 == conName con2) + +instance Ord (Constructor arg res) where + compare = compareConstructor + +instance Eq (Field a f) where + (Field p1 dt1 con1 f1) == (Field p2 dt2 con2 f2) + = (dataTypeName dt1 == dataTypeName dt2) && + (p1 == p2) && + (conName con1 == conName con2) && + (fieldName f1 == fieldName f2) + +instance Ord (Field a f) where + compare = compareField + +valueToConst :: DataTypeInfo -> Value -> (forall a. SMTType a => [ProxyArg] -> a -> SMTAnnotation a -> b) -> b +valueToConst _ (BoolValue c) app = app [] c () +valueToConst _ (IntValue c) app = app [] c () +valueToConst _ (RealValue c) app = app [] c () +valueToConst _ (BVValue w v) app = reifyNat w (\(_::Proxy n) -> app [] (BitVector v::BitVector (BVTyped n)) ()) +valueToConst dts (ConstrValue name args sort) app = case Map.lookup name (constructors dts) of + Just (con,dt,tc) -> construct con (case sort of + Nothing -> genericReplicate (argCount tc) Nothing + Just (_,pars) -> [ Just $ withSort dts par ProxyArg + | par <- pars ]) + (fmap (\val -> valueToConst dts val AnyValue) args) + app diff --git a/Language/SMTLib2/Internals/Interface.hs b/Language/SMTLib2/Internals/Interface.hs new file mode 100644 --- /dev/null +++ b/Language/SMTLib2/Internals/Interface.hs @@ -0,0 +1,710 @@ +{- | Defines the user-accessible interface of the smtlib2 library -} +{-# LANGUAGE TypeFamilies,OverloadedStrings,FlexibleContexts,ScopedTypeVariables,CPP,ViewPatterns #-} +module Language.SMTLib2.Internals.Interface where + +import Language.SMTLib2.Internals +import Language.SMTLib2.Internals.Instances (extractAnnotation,dtList,conNil,conInsert,withSort) +import Language.SMTLib2.Internals.Optimize +import Language.SMTLib2.Internals.Operators +import Language.SMTLib2.Strategy + +import Data.Typeable +import Data.Array +import Data.Unit +import Data.List (genericReplicate) +import Control.Monad.Trans (lift) +import Data.Proxy + +-- | Check if the model is satisfiable (e.g. if there is a value for each variable so that every assertion holds) +checkSat :: Monad m => SMT' m Bool +checkSat = checkSat' Nothing noLimits >>= return.isSat + +-- | Check if the model is satisfiable using a given tactic. (Works only with Z3) +checkSatUsing :: Monad m => Tactic -> SMT' m Bool +checkSatUsing t = checkSat' (Just t) noLimits >>= return.isSat + +-- | Like 'checkSat', but gives you more options like choosing a tactic (Z3 only) or providing memory/time-limits +checkSat' :: Monad m => Maybe Tactic -> CheckSatLimits -> SMT' m CheckSatResult +checkSat' tactic limits = smtBackend $ \backend -> do + st <- getSMT + lift $ smtHandle backend st (SMTCheckSat tactic limits) + +isSat :: CheckSatResult -> Bool +isSat Sat = True +isSat Unsat = False +isSat Unknown = error "smtlib2: checkSat query return 'unknown' (To catch this, use checkSat' function)" + +-- | Apply the given tactic to the current assertions. (Works only with Z3) +apply :: Monad m => Tactic -> SMT' m [SMTExpr Bool] +apply t = smtBackend $ \backend -> do + st <- getSMT + lift $ smtHandle backend st (SMTApply t) + +-- | Push a new context on the stack +push :: Monad m => SMT' m () +push = smtBackend $ \backend -> do + st <- getSMT + lift $ smtHandle backend st SMTPush + +-- | Pop a new context from the stack +pop :: Monad m => SMT' m () +pop = smtBackend $ \backend -> do + st <- getSMT + lift $ smtHandle backend st SMTPop + +-- | Perform a stacked operation, meaning that every assertion and declaration made in it will be undone after the operation. +stack :: Monad m => SMT' m a -> SMT' m a +stack act = do + push + res <- act + pop + return res + +-- | Insert a comment into the SMTLib2 command stream. +-- If you aren't looking at the command stream for debugging, this will do nothing. +comment :: Monad m => String -> SMT' m () +comment msg = smtBackend $ \backend -> do + st <- getSMT + lift $ smtHandle backend st (SMTComment msg) + +-- | Create a new named variable +varNamed :: (SMTType t,Typeable t,Unit (SMTAnnotation t),Monad m) => String -> SMT' m (SMTExpr t) +varNamed name = varNamedAnn name unit + +-- | Create a named and annotated variable. +varNamedAnn :: (SMTType t,Typeable t,Monad m) => String -> SMTAnnotation t -> SMT' m (SMTExpr t) +varNamedAnn = argVarsAnnNamed + +-- | Create a annotated variable +varAnn :: (SMTType t,Typeable t,Monad m) => SMTAnnotation t -> SMT' m (SMTExpr t) +varAnn ann = argVarsAnn ann + +-- | Create a fresh new variable +var :: (SMTType t,Typeable t,Unit (SMTAnnotation t),Monad m) => SMT' m (SMTExpr t) +var = argVarsAnn unit + +-- | Create a fresh untyped variable with a name +untypedNamedVar :: Monad m => String -> Sort -> SMT' m (SMTExpr Untyped) +untypedNamedVar name sort = do + st <- getSMT + withSort (declaredDataTypes st) sort $ + \(_::t) ann -> do + v <- varNamedAnn name ann + return $ UntypedExpr (v::SMTExpr t) + +-- | Create a fresh untyped variable +untypedVar :: Monad m => Sort -> SMT' m (SMTExpr Untyped) +untypedVar sort = do + st <- getSMT + withSort (declaredDataTypes st) sort $ + \(_::t) ann -> do + v <- varAnn ann + return $ UntypedExpr (v::SMTExpr t) + +-- | Like `argVarsAnnNamed`, but defaults the name to "var" +argVarsAnn :: (Args a,Monad m) => ArgAnnotation a -> SMT' m a +argVarsAnn = argVarsAnnNamed' Nothing + +-- | Create annotated named SMT variables of the `Args` class. +-- If more than one variable is needed, they get a numerical suffix. +argVarsAnnNamed :: (Args a,Monad m) => String -> ArgAnnotation a -> SMT' m a +argVarsAnnNamed name = argVarsAnnNamed' (Just name) + +argVarsAnnNamed' :: (Args a,Monad m) => Maybe String -> ArgAnnotation a -> SMT' m a +argVarsAnnNamed' name ann = do + (_,arg) <- foldExprs (\_ (_::SMTExpr t) ann' -> do + (res,info) <- newVariable name ann' + smtBackend $ \backend -> do + declareType (undefined::t) ann' + st <- getSMT + lift $ smtHandle backend st (SMTDeclareFun info) + case additionalConstraints (undefined::t) ann' of + Nothing -> return () + Just constr -> mapM_ assert $ constr res + return ((),res) + ) () undefined ann + return arg + +-- | Like `argVarsAnn`, but can only be used for unit type annotations. +argVars :: (Args a,Unit (ArgAnnotation a),Monad m) => SMT' m a +argVars = argVarsAnn unit + +-- | A constant expression. +constant :: (SMTValue t,Unit (SMTAnnotation t)) => t -> SMTExpr t +constant x = Const x unit + +-- | An annotated constant expression. +constantAnn :: SMTValue t => t -> SMTAnnotation t -> SMTExpr t +constantAnn x ann = Const x ann + +getValue :: (SMTValue t,Monad m) => SMTExpr t -> SMT' m t +getValue expr = smtBackend $ \backend -> do + st <- getSMT + lift $ smtHandle backend st (SMTGetValue expr) + +getValues :: (LiftArgs arg,Monad m) => arg -> SMT' m (Unpacked arg) +getValues args = unliftArgs args getValue + +-- | Extract all assigned values of the model +getModel :: Monad m => SMT' m SMTModel +getModel = smtBackend $ \backend -> do + st <- getSMT + lift $ smtHandle backend st SMTGetModel + +-- | Extract all values of an array by giving the range of indices. +unmangleArray :: (Liftable i,LiftArgs i,Ix (Unpacked i),SMTValue v, + Unit (ArgAnnotation i),Monad m) + => (Unpacked i,Unpacked i) + -> SMTExpr (SMTArray i v) + -> SMT' m (Array (Unpacked i) v) +unmangleArray b expr = mapM (\i -> do + v <- getValue (App SMTSelect (expr,liftArgs i unit)) + return (i,v) + ) (range b) >>= return.array b + +-- | Define a new function with a body +defFun :: (Args a,SMTType r,Unit (ArgAnnotation a),Monad m) + => (a -> SMTExpr r) -> SMT' m (SMTFunction a r) +defFun = defFunAnn unit + +-- | Define a new constant. +defConst :: (SMTType r,Monad m) => SMTExpr r -> SMT' m (SMTExpr r) +defConst = defConstNamed "constvar" + +-- | Define a new constant with a name +defConstNamed :: (SMTType r,Monad m) => String -> SMTExpr r -> SMT' m (SMTExpr r) +defConstNamed name = defConstNamed' (Just name) + +defConstNamed' :: (SMTType r,Monad m) => Maybe String -> SMTExpr r -> SMT' m (SMTExpr r) +defConstNamed' name e = smtBackend $ \backend -> do + let ann = extractAnnotation e + (fun,info) <- newVariable name ann + st <- getSMT + lift $ smtHandle backend st (SMTDefineFun info [] e) + return fun + +-- | Define a new function with a body and custom type annotations for arguments and result. +defFunAnnNamed :: (Args a,SMTType r,Monad m) + => String -> ArgAnnotation a -> (a -> SMTExpr r) -> SMT' m (SMTFunction a r) +defFunAnnNamed name = defFunAnnNamed' (Just name) + +defFunAnnNamed' :: (Args a,SMTType r,Monad m) + => Maybe String -> ArgAnnotation a -> (a -> SMTExpr r) -> SMT' m (SMTFunction a r) +defFunAnnNamed' name ann_arg f = smtBackend $ \backend -> do + (au,tps) <- createArgs' ann_arg + let body = f au + ann_res = extractAnnotation body + + (fun,info) <- newFunction name ann_arg ann_res + st <- getSMT + lift $ smtHandle backend st (SMTDefineFun info tps body) + return fun + +-- | Like `defFunAnnNamed`, but defaults the function name to "fun". +defFunAnn :: (Args a,SMTType r,Monad m) + => ArgAnnotation a -> (a -> SMTExpr r) -> SMT' m (SMTFunction a r) +defFunAnn = defFunAnnNamed' Nothing + +-- | Boolean conjunction +and' :: SMTFunction [SMTExpr Bool] Bool +and' = SMTLogic And + +(.&&.) :: SMTExpr Bool -> SMTExpr Bool -> SMTExpr Bool +(.&&.) x y = App (SMTLogic And) [x,y] + +-- | Boolean disjunction +or' :: SMTFunction [SMTExpr Bool] Bool +or' = SMTLogic Or + +(.||.) :: SMTExpr Bool -> SMTExpr Bool -> SMTExpr Bool +(.||.) x y = App (SMTLogic Or) [x,y] + +-- | Create a boolean expression that encodes that the array is equal to the supplied constant array. +arrayEquals :: (LiftArgs i,Liftable i,SMTValue v,Ix (Unpacked i),Unit (ArgAnnotation i),Unit (SMTAnnotation v)) + => SMTExpr (SMTArray i v) -> Array (Unpacked i) v -> SMTExpr Bool +arrayEquals expr arr + = case [(select expr (liftArgs i unit)) .==. (constant v) + | (i,v) <- assocs arr ] of + [] -> constant True + xs -> foldl1 (.&&.) xs + +-- | Asserts that a boolean expression is true +assert :: Monad m => SMTExpr Bool -> SMT' m () +assert expr = smtBackend $ \backend -> do + st <- getSMT + lift $ smtHandle backend st (SMTAssert expr Nothing Nothing) + +-- | Create a new interpolation group +interpolationGroup :: Monad m => SMT' m InterpolationGroup +interpolationGroup = do + st <- getSMT + let intgr = nextInterpolationGroup st + putSMT $ st { nextInterpolationGroup = succ intgr } + return (InterpolationGroup intgr) + +-- | Assert a boolean expression and track it for an unsat core call later +assertId :: Monad m => SMTExpr Bool -> SMT' m ClauseId +assertId expr = smtBackend $ \backend -> do + st <- getSMT + let cid = nextClauseId st + putSMT $ st { nextClauseId = succ cid } + lift $ smtHandle backend st (SMTAssert expr Nothing (Just $ ClauseId cid)) + return (ClauseId cid) + +-- | Assert a boolean expression to be true and assign it to an interpolation group +assertInterp :: Monad m => SMTExpr Bool -> InterpolationGroup -> SMT' m () +assertInterp expr interp = smtBackend $ \backend -> do + st <- getSMT + lift $ smtHandle backend st (SMTAssert expr (Just interp) Nothing) + +getInterpolant :: Monad m => [InterpolationGroup] -> SMT' m (SMTExpr Bool) +getInterpolant grps = smtBackend $ \backend -> do + st <- getSMT + lift $ smtHandle backend st (SMTGetInterpolant grps) + +-- | Set an option for the underlying SMT solver +setOption :: Monad m => SMTOption -> SMT' m () +setOption opt = smtBackend $ \backend -> do + st <- getSMT + lift $ smtHandle backend st (SMTSetOption opt) + +-- | Get information about the underlying SMT solver +getInfo :: (Monad m,Typeable i) => SMTInfo i -> SMT' m i +getInfo inf = smtBackend $ \backend -> do + st <- getSMT + lift $ smtHandle backend st (SMTGetInfo inf) + +-- | Create a new uniterpreted function with annotations for +-- the argument and the return type. +funAnn :: (Liftable a,SMTType r,Monad m) => ArgAnnotation a -> SMTAnnotation r -> SMT' m (SMTFunction a r) +funAnn = funAnnNamed' Nothing + +-- | Create a new uninterpreted named function with annotation for +-- the argument and the return type. +funAnnNamed :: (Liftable a, SMTType r,Monad m) => String -> ArgAnnotation a -> SMTAnnotation r -> SMT' m (SMTFunction a r) +funAnnNamed name = funAnnNamed' (Just name) + +funAnnNamed' :: (Liftable a, SMTType r,Monad m) => Maybe String -> ArgAnnotation a -> SMTAnnotation r -> SMT' m (SMTFunction a r) +funAnnNamed' name annArg annRet = smtBackend $ \backend -> do + (fun,info) <- newFunction name annArg annRet + st <- getSMT + lift $ smtHandle backend st (SMTDeclareFun info) + case additionalConstraints (undefined::t) annRet of + Nothing -> return () + Just constr -> assert $ forAllAnn annArg + (\x -> case constr (fun `app` x) of + [] -> constant True + [x] -> x + xs -> and' `app` xs) + return fun + +-- | funAnn with an annotation only for the return type. +funAnnRet :: (Liftable a,SMTType r,Unit (ArgAnnotation a),Monad m) + => SMTAnnotation r -> SMT' m (SMTFunction a r) +funAnnRet = funAnn unit + +-- | Create a new uninterpreted function. +fun :: (Liftable a,SMTType r,SMTAnnotation r ~ (),Unit (ArgAnnotation a),Monad m) + => SMT' m (SMTFunction a r) +fun = funAnn unit unit + +-- | Apply a function to an argument +app :: (Args arg,SMTType res) => SMTFunction arg res -> arg -> SMTExpr res +app = App + +-- | Lift a function to arrays +map' :: (Liftable arg,Args i,SMTType res) + => SMTFunction arg res -> SMTFunction (Lifted arg i) (SMTArray i res) +map' f = SMTMap f + +-- | Two expressions shall be equal +(.==.) :: SMTType a => SMTExpr a -> SMTExpr a -> SMTExpr Bool +(.==.) x y = App SMTEq [x,y] + +infix 4 .==. + +-- | A generalized version of `.==.` +argEq :: Args a => a -> a -> SMTExpr Bool +argEq xs ys = app and' res + where + (res,_,_) = foldsExprsId + (\s [(arg1,_),(arg2,_)] _ -> ((arg1 .==. arg2):s,[arg1,arg2],undefined)) + [] + [(xs,()),(ys,())] (extractArgAnnotation xs) + +-- | Declares all arguments to be distinct +distinct :: SMTType a => [SMTExpr a] -> SMTExpr Bool +distinct = App SMTDistinct + +-- | Calculate the sum of arithmetic expressions +plus :: (SMTArith a) => SMTFunction [SMTExpr a] a +plus = SMTArith Plus + +-- | Calculate the product of arithmetic expressions +mult :: (SMTArith a) => SMTFunction [SMTExpr a] a +mult = SMTArith Mult + +-- | Subtracts two expressions +minus :: (SMTArith a) => SMTFunction (SMTExpr a,SMTExpr a) a +minus = SMTMinus + +-- | Divide an arithmetic expression by another +div' :: SMTExpr Integer -> SMTExpr Integer -> SMTExpr Integer +div' x y = App (SMTIntArith Div) (x,y) + +div'' :: SMTFunction (SMTExpr Integer,SMTExpr Integer) Integer +div'' = SMTIntArith Div + +-- | Perform a modulo operation on an arithmetic expression +mod' :: SMTExpr Integer -> SMTExpr Integer -> SMTExpr Integer +mod' x y = App (SMTIntArith Mod) (x,y) + +mod'' :: SMTFunction (SMTExpr Integer,SMTExpr Integer) Integer +mod'' = SMTIntArith Mod + +-- | Calculate the remainder of the division of two integer expressions +rem' :: SMTExpr Integer -> SMTExpr Integer -> SMTExpr Integer +rem' x y = App (SMTIntArith Rem) (x,y) + +rem'' :: SMTFunction (SMTExpr Integer,SMTExpr Integer) Integer +rem'' = SMTIntArith Rem + +-- | Divide a rational expression by another one +divide :: SMTExpr Rational -> SMTExpr Rational -> SMTExpr Rational +divide x y = App SMTDivide (x,y) + +divide' :: SMTFunction (SMTExpr Rational,SMTExpr Rational) Rational +divide' = SMTDivide + +-- | For an expression @x@, this returns the expression @-x@. +neg :: SMTArith a => SMTFunction (SMTExpr a) a +neg = SMTNeg + +-- | Convert an integer expression to a real expression +toReal :: SMTExpr Integer -> SMTExpr Rational +toReal = App SMTToReal + +-- | Convert a real expression into an integer expression +toInt :: SMTExpr Rational -> SMTExpr Integer +toInt = App SMTToInt + +-- | If-then-else construct +ite :: (SMTType a) => SMTExpr Bool -- ^ If this expression is true + -> SMTExpr a -- ^ Then return this expression + -> SMTExpr a -- ^ Else this one + -> SMTExpr a +ite c l r = App SMTITE (c,l,r) + +-- | Exclusive or: Return true if exactly one argument is true. +xor :: SMTFunction [SMTExpr Bool] Bool +xor = SMTLogic XOr + +-- | Implication +(.=>.) :: SMTExpr Bool -- ^ If this expression is true + -> SMTExpr Bool -- ^ This one must be as well + -> SMTExpr Bool +(.=>.) x y = App (SMTLogic Implies) [x,y] + +-- | Negates a boolean expression +not' :: SMTExpr Bool -> SMTExpr Bool +not' = App SMTNot + +not'' :: SMTFunction (SMTExpr Bool) Bool +not'' = SMTNot + +-- | Extracts an element of an array by its index +select :: (Liftable i,SMTType v) => SMTExpr (SMTArray i v) -> i -> SMTExpr v +select arr i = App SMTSelect (arr,i) + +-- | The expression @store arr i v@ stores the value /v/ in the array /arr/ at position /i/ and returns the resulting new array. +store :: (Liftable i,SMTType v) => SMTExpr (SMTArray i v) -> i -> SMTExpr v -> SMTExpr (SMTArray i v) +store arr i v = App SMTStore (arr,i,v) + +-- | Interpret a function /f/ from /i/ to /v/ as an array with indices /i/ and elements /v/. +-- Such that: @f \`app\` j .==. select (asArray f) j@ for all indices j. +asArray :: (Args arg,Unit (ArgAnnotation arg),SMTType res) + => SMTFunction arg res -> SMTExpr (SMTArray arg res) +asArray f = AsArray f unit + +-- | Create an array where each element is the same. +constArray :: (Args i,SMTType v) => SMTExpr v -- ^ This element will be at every index of the array + -> ArgAnnotation i -- ^ Annotations of the index type + -> SMTExpr (SMTArray i v) +constArray e i_ann = App (SMTConstArray i_ann) e + +-- | Bitvector and +bvand :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr (BitVector t) +bvand e1 e2 = App (SMTBVBin BVAnd) (e1,e2) + +-- | Bitvector or +bvor :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr (BitVector t) +bvor e1 e2 = App (SMTBVBin BVOr) (e1,e2) + +-- | Bitvector or +bvxor :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr (BitVector t) +bvxor e1 e2 = App (SMTBVBin BVXor) (e1,e2) + +-- | Bitvector not +bvnot :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) +bvnot e = App (SMTBVUn BVNot) e + +-- | Bitvector signed negation +bvneg :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) +bvneg e = App (SMTBVUn BVNeg) e + +-- | Bitvector addition +bvadd :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr (BitVector t) +bvadd e1 e2 = App (SMTBVBin BVAdd) (e1,e2) + +-- | Bitvector subtraction +bvsub :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr (BitVector t) +bvsub e1 e2 = App (SMTBVBin BVSub) (e1,e2) + +-- | Bitvector multiplication +bvmul :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr (BitVector t) +bvmul e1 e2 = App (SMTBVBin BVMul) (e1,e2) + +-- | Bitvector unsigned remainder +bvurem :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr (BitVector t) +bvurem e1 e2 = App (SMTBVBin BVURem) (e1,e2) + +-- | Bitvector signed remainder +bvsrem :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr (BitVector t) +bvsrem e1 e2 = App (SMTBVBin BVSRem) (e1,e2) + +-- | Bitvector unsigned division +bvudiv :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr (BitVector t) +bvudiv e1 e2 = App (SMTBVBin BVUDiv) (e1,e2) + +-- | Bitvector signed division +bvsdiv :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr (BitVector t) +bvsdiv e1 e2 = App (SMTBVBin BVSDiv) (e1,e2) + +-- | Bitvector unsigned less-or-equal +bvule :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr Bool +bvule e1 e2 = App (SMTBVComp BVULE) (e1,e2) + +-- | Bitvector unsigned less-than +bvult :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr Bool +bvult e1 e2 = App (SMTBVComp BVULT) (e1,e2) + +-- | Bitvector unsigned greater-or-equal +bvuge :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr Bool +bvuge e1 e2 = App (SMTBVComp BVUGE) (e1,e2) + +-- | Bitvector unsigned greater-than +bvugt :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr Bool +bvugt e1 e2 = App (SMTBVComp BVUGT) (e1,e2) + +-- | Bitvector signed less-or-equal +bvsle :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr Bool +bvsle e1 e2 = App (SMTBVComp BVSLE) (e1,e2) + +-- | Bitvector signed less-than +bvslt :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr Bool +bvslt e1 e2 = App (SMTBVComp BVSLT) (e1,e2) + +-- | Bitvector signed greater-or-equal +bvsge :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr Bool +bvsge e1 e2 = App (SMTBVComp BVSGE) (e1,e2) + +-- | Bitvector signed greater-than +bvsgt :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr Bool +bvsgt e1 e2 = App (SMTBVComp BVSGT) (e1,e2) + +-- | Bitvector shift left +bvshl :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr (BitVector t) +bvshl e1 e2 = App (SMTBVBin BVSHL) (e1,e2) + +-- | Bitvector logical right shift +bvlshr :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr (BitVector t) +bvlshr e1 e2 = App (SMTBVBin BVLSHR) (e1,e2) + +-- | Bitvector arithmetical right shift +bvashr :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr (BitVector t) +bvashr e1 e2 = App (SMTBVBin BVASHR) (e1,e2) + +-- | Concats two bitvectors into one. +bvconcat :: (Concatable t1 t2) => SMTExpr (BitVector t1) -> SMTExpr (BitVector t2) -> SMTExpr (BitVector (ConcatResult t1 t2)) +bvconcat e1 e2 = App SMTConcat (e1,e2) + +-- | Extract a sub-vector out of a given bitvector. +bvextract :: (TypeableNat start,TypeableNat len,Extractable tp len') + => Proxy start -- ^ The start of the extracted region + -> Proxy len + -> SMTExpr (BitVector tp) -- ^ The bitvector to extract from + -> SMTExpr (BitVector len') +bvextract start len (e::SMTExpr (BitVector tp)) + = App (SMTExtract start len) e + +bvextract' :: Integer -> Integer -> SMTExpr (BitVector BVUntyped) -> SMTExpr (BitVector BVUntyped) +bvextract' start len = reifyNat start $ + \start' -> reifyNat len $ \len' -> bvextract start' len' + +-- | Safely split a 16-bit bitvector into two 8-bit bitvectors. +bvsplitu16to8 :: SMTExpr BV16 -> (SMTExpr BV8,SMTExpr BV8) +bvsplitu16to8 e = (App (SMTExtract (Proxy::Proxy N8) (Proxy::Proxy N8)) e, + App (SMTExtract (Proxy::Proxy N0) (Proxy::Proxy N8)) e) + +-- | Safely split a 32-bit bitvector into two 16-bit bitvectors. +bvsplitu32to16 :: SMTExpr BV32 -> (SMTExpr BV16,SMTExpr BV16) +bvsplitu32to16 e = (App (SMTExtract (Proxy::Proxy N16) (Proxy::Proxy N16)) e, + App (SMTExtract (Proxy::Proxy N0) (Proxy::Proxy N16)) e) + +-- | Safely split a 32-bit bitvector into four 8-bit bitvectors. +bvsplitu32to8 :: SMTExpr BV32 -> (SMTExpr BV8,SMTExpr BV8,SMTExpr BV8,SMTExpr BV8) +bvsplitu32to8 e = (App (SMTExtract (Proxy::Proxy N24) (Proxy::Proxy N8)) e, + App (SMTExtract (Proxy::Proxy N16) (Proxy::Proxy N8)) e, + App (SMTExtract (Proxy::Proxy N8) (Proxy::Proxy N8)) e, + App (SMTExtract (Proxy::Proxy N0) (Proxy::Proxy N8)) e) + +-- | Safely split a 64-bit bitvector into two 32-bit bitvectors. +bvsplitu64to32 :: SMTExpr BV64 -> (SMTExpr BV32,SMTExpr BV32) +bvsplitu64to32 e = (App (SMTExtract (Proxy::Proxy N32) (Proxy::Proxy N32)) e, + App (SMTExtract (Proxy::Proxy N0) (Proxy::Proxy N32)) e) + +-- | Safely split a 64-bit bitvector into four 16-bit bitvectors. +bvsplitu64to16 :: SMTExpr BV64 -> (SMTExpr BV16,SMTExpr BV16,SMTExpr BV16,SMTExpr BV16) +bvsplitu64to16 e = (App (SMTExtract (Proxy::Proxy N48) (Proxy::Proxy N16)) e, + App (SMTExtract (Proxy::Proxy N32) (Proxy::Proxy N16)) e, + App (SMTExtract (Proxy::Proxy N16) (Proxy::Proxy N16)) e, + App (SMTExtract (Proxy::Proxy N0) (Proxy::Proxy N16)) e) + +-- | Safely split a 64-bit bitvector into eight 8-bit bitvectors. +bvsplitu64to8 :: SMTExpr BV64 -> (SMTExpr BV8,SMTExpr BV8,SMTExpr BV8,SMTExpr BV8,SMTExpr BV8,SMTExpr BV8,SMTExpr BV8,SMTExpr BV8) +bvsplitu64to8 e = (App (SMTExtract (Proxy::Proxy N56) (Proxy::Proxy N8)) e, + App (SMTExtract (Proxy::Proxy N48) (Proxy::Proxy N8)) e, + App (SMTExtract (Proxy::Proxy N40) (Proxy::Proxy N8)) e, + App (SMTExtract (Proxy::Proxy N32) (Proxy::Proxy N8)) e, + App (SMTExtract (Proxy::Proxy N24) (Proxy::Proxy N8)) e, + App (SMTExtract (Proxy::Proxy N16) (Proxy::Proxy N8)) e, + App (SMTExtract (Proxy::Proxy N8) (Proxy::Proxy N8)) e, + App (SMTExtract (Proxy::Proxy N0) (Proxy::Proxy N8)) e) + +mkQuantified :: (Args a,SMTType b) => (Integer -> [ProxyArg] -> SMTExpr b -> SMTExpr b) + -> ArgAnnotation a -> (a -> SMTExpr b) + -> SMTExpr b +mkQuantified constr ann f = constr lvl sorts body + where + undef :: (a -> SMTExpr b) -> a + undef _ = undefined + sorts = getTypes (undef f) ann + Just (arg0,[]) = toArgs ann [InternalObj () prx + | prx <- sorts ] + body' = f arg0 + lvl = quantificationLevel body' + Just (arg1,[]) = toArgs ann [QVar lvl i prx + | (i,prx) <- Prelude.zip [0..] sorts ] + body = f arg1 + +-- | If the supplied function returns true for all possible values, the forall quantification returns true. +forAll :: (Args a,Unit (ArgAnnotation a)) => (a -> SMTExpr Bool) -> SMTExpr Bool +forAll = forAllAnn unit + +-- | An annotated version of `forAll`. +forAllAnn :: Args a => ArgAnnotation a -> (a -> SMTExpr Bool) -> SMTExpr Bool +forAllAnn = mkQuantified Forall + +-- | If the supplied function returns true for at least one possible value, the exists quantification returns true. +exists :: (Args a,Unit (ArgAnnotation a)) => (a -> SMTExpr Bool) -> SMTExpr Bool +exists = existsAnn unit + +-- | An annotated version of `exists`. +existsAnn :: Args a => ArgAnnotation a -> (a -> SMTExpr Bool) -> SMTExpr Bool +existsAnn = mkQuantified Exists + +-- | Binds an expression to a variable. +-- Can be used to prevent blowups in the command stream if expressions are used multiple times. +-- @let' x f@ is functionally equivalent to @f x@. +let' :: (Args a,Unit (ArgAnnotation a),SMTType b) => a -> (a -> SMTExpr b) -> SMTExpr b +let' = letAnn unit + +-- | Like `let'`, but can be given an additional type annotation for the argument of the function. +letAnn :: (Args a,SMTType b) => ArgAnnotation a -> a -> (a -> SMTExpr b) -> SMTExpr b +letAnn ann arg = mkQuantified (\lvl _ body -> Let lvl args body) ann + where + args = fromArgs arg + +-- | Like 'let'', but can define multiple variables of the same type. +lets :: (Args a,Unit (ArgAnnotation a),SMTType b) => [a] -> ([a] -> SMTExpr b) -> SMTExpr b +lets xs = letAnn (fmap (const unit) xs) xs + +-- | Like 'forAll', but can quantify over more than one variable (of the same type). +forAllList :: (Args a,Unit (ArgAnnotation a)) => Integer -- ^ Number of variables to quantify + -> ([a] -> SMTExpr Bool) -- ^ Function which takes a list of the quantified variables + -> SMTExpr Bool +forAllList l = forAllAnn (genericReplicate l unit) + +-- | Like `exists`, but can quantify over more than one variable (of the same type). +existsList :: (Args a,Unit (ArgAnnotation a)) => Integer -- ^ Number of variables to quantify + -> ([a] -> SMTExpr Bool) -- ^ Function which takes a list of the quantified variables + -> SMTExpr Bool +existsList l = existsAnn (genericReplicate l unit) + +-- | Checks if the expression is formed a specific constructor. +is :: (Args arg,SMTType dt) => SMTExpr dt -> Constructor arg dt -> SMTExpr Bool +is e con = App (SMTConTest con) e + +-- | Access a field of an expression +(.#) :: (SMTType a,SMTType f) => SMTExpr a -> Field a f -> SMTExpr f +(.#) e f = App (SMTFieldSel f) e + +-- | Takes the first element of a list +head' :: (SMTType a,Unit (SMTAnnotation a)) => SMTExpr [a] -> SMTExpr a +head' = App (SMTBuiltIn "head" unit) + +-- | Drops the first element from a list +tail' :: (SMTType a,Unit (SMTAnnotation a)) => SMTExpr [a] -> SMTExpr [a] +tail' = App (SMTBuiltIn "tail" unit) + +-- | Checks if a list is empty. +isNil :: (SMTType a) => SMTExpr [a] -> SMTExpr Bool +isNil (e::SMTExpr [a]) = is e (Constructor [ProxyArg (undefined::[a]) (extractAnnotation e)] dtList conNil:: Constructor () [a]) + +-- | Checks if a list is non-empty. +isInsert :: (SMTType a,Unit (SMTAnnotation a)) => SMTExpr [a] -> SMTExpr Bool +isInsert (e::SMTExpr [a]) = is e (Constructor [ProxyArg (undefined::[a]) (extractAnnotation e)] dtList conInsert :: Constructor (SMTExpr a,SMTExpr [a]) [a]) + +-- | Sets the logic used for the following program (Not needed for many solvers). +setLogic :: Monad m => String -> SMT' m () +setLogic name = smtBackend $ \backend -> do + st <- getSMT + lift $ smtHandle backend st (SMTSetLogic name) + +-- | Given an arbitrary expression, this creates a named version of it and a name to reference it later on. +named :: (SMTType a,SMTAnnotation a ~ (),Monad m) + => String -> SMTExpr a -> SMT' m (SMTExpr a,SMTExpr a) +named name expr = do + (var,info) <- newVariable (Just name) (extractAnnotation expr) + let Just (name,nc) = funInfoName info + return (Named expr name nc,var) + +-- | Like `named`, but defaults the name to "named". +named' :: (SMTType a,SMTAnnotation a ~ (),Monad m) + => SMTExpr a -> SMT' m (SMTExpr a,SMTExpr a) +named' = named "named" + +-- | After an unsuccessful 'checkSat' this method extracts a proof from the SMT solver that the instance is unsatisfiable. +getProof :: Monad m => SMT' m (SMTExpr Bool) +getProof = smtBackend $ \backend -> do + st <- getSMT + lift $ smtHandle backend st SMTGetProof + +-- | Use the SMT solver to simplify a given expression. +-- Currently only works with Z3. +simplify :: (SMTType t,Monad m) => SMTExpr t -> SMT' m (SMTExpr t) +simplify expr = smtBackend $ \backend -> do + st <- getSMT + lift $ smtHandle backend st (SMTSimplify expr) + +-- | After an unsuccessful 'checkSat', return a list of clauses which make the +-- instance unsatisfiable. +getUnsatCore :: Monad m => SMT' m [ClauseId] +getUnsatCore = smtBackend $ \backend -> do + st <- getSMT + lift $ smtHandle backend st SMTGetUnsatCore + +optimizeExpr' :: SMTExpr a -> SMTExpr a +optimizeExpr' e = case optimizeExpr e of + Nothing -> e + Just e' -> e' diff --git a/Language/SMTLib2/Internals/Operators.hs b/Language/SMTLib2/Internals/Operators.hs new file mode 100644 --- /dev/null +++ b/Language/SMTLib2/Internals/Operators.hs @@ -0,0 +1,58 @@ +module Language.SMTLib2.Internals.Operators where + +import Data.Typeable + +data SMTOrdOp + = Ge + | Gt + | Le + | Lt + deriving (Typeable,Eq,Ord,Show) + +data SMTArithOp + = Plus + | Mult + deriving (Typeable,Eq,Ord,Show) + +data SMTIntArithOp = Div + | Mod + | Rem + deriving (Typeable,Eq,Ord,Show) + +data SMTLogicOp = And + | Or + | XOr + | Implies + deriving (Typeable,Eq,Ord,Show) + +data SMTBVCompOp + = BVULE + | BVULT + | BVUGE + | BVUGT + | BVSLE + | BVSLT + | BVSGE + | BVSGT + deriving (Typeable,Eq,Ord,Show) + +data SMTBVBinOp + = BVAdd + | BVSub + | BVMul + | BVURem + | BVSRem + | BVUDiv + | BVSDiv + | BVSHL + | BVLSHR + | BVASHR + | BVXor + | BVAnd + | BVOr + deriving (Typeable,Eq,Ord,Show) + +data SMTBVUnOp + = BVNot + | BVNeg + deriving (Typeable,Eq,Ord,Show) diff --git a/Language/SMTLib2/Internals/Optimize.hs b/Language/SMTLib2/Internals/Optimize.hs new file mode 100644 --- /dev/null +++ b/Language/SMTLib2/Internals/Optimize.hs @@ -0,0 +1,240 @@ +module Language.SMTLib2.Internals.Optimize (optimizeBackend,optimizeExpr) where + +import Language.SMTLib2.Internals +import Language.SMTLib2.Internals.Instances (bvSigned,bvUnsigned,bvRestrict,eqExpr) +import Language.SMTLib2.Internals.Operators +import Data.Proxy +import Data.Bits +import Data.Either (partitionEithers) +import Data.Typeable (cast) + +optimizeBackend :: b -> OptimizeBackend b +optimizeBackend = OptB + +data OptimizeBackend b = OptB b + +instance SMTBackend b m => SMTBackend (OptimizeBackend b) m where + smtHandle (OptB b) st (SMTAssert expr grp cid) + = let nexpr = case optimizeExpr expr of + Just e -> e + Nothing -> expr + in case nexpr of + Const True _ -> return () + _ -> smtHandle b st (SMTAssert nexpr grp cid) + smtHandle (OptB b) st (SMTDefineFun name args body) + = let nbody = case optimizeExpr body of + Just e -> e + Nothing -> body + in smtHandle b st (SMTDefineFun name args nbody) + smtHandle (OptB b) st (SMTGetValue expr) + = let nexpr = case optimizeExpr expr of + Just e -> e + Nothing -> expr + in smtHandle b st (SMTGetValue nexpr) + smtHandle (OptB b) st SMTGetProof = do + res <- smtHandle b st SMTGetProof + case optimizeExpr res of + Just e -> return e + Nothing -> return res + smtHandle (OptB b) st (SMTSimplify expr) = do + let nexpr = case optimizeExpr expr of + Just e -> e + Nothing -> expr + simp <- smtHandle b st (SMTSimplify nexpr) + case optimizeExpr simp of + Nothing -> return simp + Just simp' -> return simp' + smtHandle (OptB b) st (SMTGetInterpolant grps) = do + inter <- smtHandle b st (SMTGetInterpolant grps) + case optimizeExpr inter of + Nothing -> return inter + Just e -> return e + smtHandle (OptB b) st req = smtHandle b st req + +optimizeExpr :: SMTExpr t -> Maybe (SMTExpr t) +optimizeExpr (App fun x) = let (opt,x') = foldExprsId (\opt expr ann -> case optimizeExpr expr of + Nothing -> (opt,expr) + Just expr' -> (True,expr') + ) False x (extractArgAnnotation x) + in case optimizeCall fun x' of + Nothing -> if opt + then Just $ App fun x' + else Nothing + Just res -> Just res + +optimizeExpr _ = Nothing + +optimizeCall :: SMTFunction arg res -> arg -> Maybe (SMTExpr res) +optimizeCall SMTEq [] = Just (Const True ()) +optimizeCall SMTEq [_] = Just (Const True ()) +optimizeCall SMTEq [x,y] = case eqExpr x y of + Nothing -> Nothing + Just res -> Just (Const res ()) +optimizeCall SMTNot (Const x _) = Just $ Const (not x) () +optimizeCall (SMTLogic _) [x] = Just x +optimizeCall (SMTLogic And) xs = case removeConstsOf False xs of + Just _ -> Just $ Const False () + Nothing -> case removeConstsOf True xs of + Nothing -> case xs of + [] -> Just $ Const True () + _ -> Nothing + Just [] -> Just $ Const True () + Just [x] -> Just x + Just xs' -> Just $ App (SMTLogic And) xs' +optimizeCall (SMTLogic Or) xs = case removeConstsOf True xs of + Just _ -> Just $ Const True () + Nothing -> case removeConstsOf False xs of + Nothing -> case xs of + [] -> Just $ Const False () + _ -> Nothing + Just [] -> Just $ Const False () + Just [x] -> Just x + Just xs' -> Just $ App (SMTLogic Or) xs' +optimizeCall (SMTLogic XOr) [] = Just $ Const False () +optimizeCall (SMTLogic Implies) [] = Just $ Const True () +optimizeCall (SMTLogic Implies) xs + = let (args,res) = splitLast xs + in case res of + Const True _ -> Just (Const True ()) + _ -> case removeConstsOf False args of + Just _ -> Just $ Const True () + Nothing -> case removeConstsOf True args of + Nothing -> case args of + [] -> Just res + _ -> Nothing + Just [] -> Just res + Just args' -> Just $ App (SMTLogic Implies) (args'++[res]) +optimizeCall SMTITE (Const True _,ifT,_) = Just ifT +optimizeCall SMTITE (Const False _,_,ifF) = Just ifF +optimizeCall SMTITE (_,ifT,ifF) = case eqExpr ifT ifF of + Just True -> Just ifT + _ -> Nothing +optimizeCall (SMTBVBin op) args = bvBinOpOptimize op args +optimizeCall SMTConcat (Const (BitVector v1::BitVector b1) ann1,Const (BitVector v2::BitVector b2) ann2) + = Just (Const (BitVector $ (v1 `shiftL` (fromInteger $ getBVSize (Proxy::Proxy b2) ann2)) .|. v2) + (concatAnnotation (undefined::b1) (undefined::b2) ann1 ann2)) +optimizeCall (SMTExtract pstart plen) (Const from@(BitVector v) ann) + = let start = reflectNat pstart 0 + undefFrom :: BitVector from -> from + undefFrom _ = undefined + undefLen :: SMTExpr (BitVector len) -> len + undefLen _ = undefined + len = reflectNat plen 0 + res = Const (BitVector $ (v `shiftR` (fromInteger start)) .&. (1 `shiftL` (fromInteger $ reflectNat plen 0) - 1)) + (extractAnn (undefFrom from) (undefLen res) len ann) + in Just res +optimizeCall (SMTBVComp op) args = bvCompOptimize op args +optimizeCall (SMTArith op) args = case cast args of + Just args' -> case cast (intArithOptimize op args') of + Just res -> res + Nothing -> Nothing +optimizeCall SMTMinus args = case cast args of + Just args' -> case cast (intMinusOptimize args') of + Just res -> res + Nothing -> Nothing +optimizeCall (SMTOrd op) args = case cast args of + Just args' -> case cast (intCmpOptimize op args') of + Just res -> res + Nothing -> Nothing +optimizeCall _ _ = Nothing + +removeConstsOf :: Bool -> [SMTExpr Bool] -> Maybe [SMTExpr Bool] +removeConstsOf val = removeItems (\e -> case e of + Const c _ -> c==val + _ -> False) + +removeItems :: (a -> Bool) -> [a] -> Maybe [a] +removeItems f [] = Nothing +removeItems f (x:xs) = if f x + then (case removeItems f xs of + Nothing -> Just xs + Just xs' -> Just xs') + else (case removeItems f xs of + Nothing -> Nothing + Just xs' -> Just (x:xs')) + +splitLast :: [a] -> ([a],a) +splitLast [x] = ([],x) +splitLast (x:xs) = let (xs',last) = splitLast xs + in (x:xs',last) + +bvBinOpOptimize :: IsBitVector a => SMTBVBinOp -> (SMTExpr (BitVector a),SMTExpr (BitVector a)) -> Maybe (SMTExpr (BitVector a)) +bvBinOpOptimize BVAdd (Const (BitVector 0) _,y) = Just y +bvBinOpOptimize BVAdd (x,Const (BitVector 0) _) = Just x +bvBinOpOptimize BVAdd (Const (BitVector x) w,Const (BitVector y) _) = Just (Const (bvRestrict (BitVector $ x+y) w) w) +bvBinOpOptimize BVAnd (Const (BitVector x) w,Const (BitVector y) _) = Just (Const (BitVector $ x .&. y) w) +bvBinOpOptimize BVOr (Const (BitVector x) w,Const (BitVector y) _) = Just (Const (BitVector $ x .|. y) w) +bvBinOpOptimize BVOr (Const (BitVector 0) _,oth) = Just oth +bvBinOpOptimize BVOr (oth,Const (BitVector 0) _) = Just oth +bvBinOpOptimize BVSHL (Const (BitVector x) w,Const (BitVector y) _) + = Just (Const (bvRestrict (BitVector $ x `shiftL` (fromInteger y)) w) w) +bvBinOpOptimize BVSHL (Const (BitVector 0) w,_) = Just (Const (BitVector 0) w) +bvBinOpOptimize BVSHL (oth,Const (BitVector 0) w) = Just oth +bvBinOpOptimize _ _ = Nothing + +bvCompOptimize :: IsBitVector a => SMTBVCompOp -> (SMTExpr (BitVector a),SMTExpr (BitVector a)) -> Maybe (SMTExpr Bool) +bvCompOptimize op (Const b1 ann1,Const b2 ann2) + = Just $ Const (case op of + BVULE -> u1 <= u2 + BVULT -> u1 < u2 + BVUGE -> u1 >= u2 + BVUGT -> u1 > u2 + BVSLE -> s1 <= s2 + BVSLT -> s1 < s2 + BVSGE -> s1 >= s2 + BVSGT -> s1 > s2) () + where + u1 = bvUnsigned b1 ann1 + u2 = bvUnsigned b2 ann2 + s1 = bvSigned b1 ann1 + s2 = bvSigned b2 ann2 +bvCompOptimize _ _ = Nothing + +intArithOptimize :: SMTArithOp -> [SMTExpr Integer] -> Maybe (SMTExpr Integer) +intArithOptimize Plus xs + = let (consts,nonconsts) = partitionEithers $ fmap (\e -> case e of + Const i _ -> Left i + _ -> Right e + ) xs + in case consts of + [] -> Nothing + [x] -> case nonconsts of + [] -> Just (Const x ()) + [y] -> if x==0 + then Just y + else Nothing + _ -> Nothing + _ -> let s = sum consts + in case nonconsts of + [] -> Just (Const s ()) + [x] -> if s==0 + then Just x + else Just (App (SMTArith Plus) [x,Const s ()]) + _ -> Just (App (SMTArith Plus) (nonconsts++(if s==0 + then [] + else [Const s ()]))) +intArithOptimize Mult xs + = let (consts,nonconsts) = partitionEithers $ fmap (\e -> case e of + Const i _ -> Left i + _ -> Right e + ) xs + in case consts of + [] -> Nothing + [_] -> Nothing + _ -> case nonconsts of + [] -> Just (Const (product consts) ()) + _ -> Just (App (SMTArith Mult) (nonconsts++[Const (product consts) ()])) + +intMinusOptimize :: (SMTExpr Integer,SMTExpr Integer) -> Maybe (SMTExpr Integer) +intMinusOptimize (Const x _,Const y _) = Just (Const (x-y) ()) +intMinusOptimize (x,Const 0 _) = Just x +intMinusOptimize _ = Nothing + +intCmpOptimize :: SMTOrdOp -> (SMTExpr Integer,SMTExpr Integer) -> Maybe (SMTExpr Bool) +intCmpOptimize op (Const x _,Const y _) + = Just (Const (case op of + Ge -> x >= y + Gt -> x > y + Le -> x <= y + Lt -> x < y) ()) +intCmpOptimize _ _ = Nothing diff --git a/Language/SMTLib2/Pipe.hs b/Language/SMTLib2/Pipe.hs new file mode 100644 --- /dev/null +++ b/Language/SMTLib2/Pipe.hs @@ -0,0 +1,1678 @@ +{-# LANGUAGE ViewPatterns #-} +module Language.SMTLib2.Pipe + (SMTPipe(), + FunctionParser(), + createSMTPipe, + withPipe, + exprToLisp, + exprToLispWith, + lispToExpr, + sortToLisp,lispToSort, + renderExpr, + renderExpr', + renderSMTRequest, + renderSMTResponse, + commonFunctions, + commonTheorems) where + +import Language.SMTLib2.Internals as SMT +import Language.SMTLib2.Internals.Instances +import Language.SMTLib2.Internals.Operators +import Language.SMTLib2.Strategy as Strat +import Data.Unit + +import Data.Monoid +import qualified Data.AttoLisp as L +import qualified Data.Attoparsec.Number as L +import Data.Attoparsec +import System.Process +import qualified Data.Text as T + +import System.IO as IO +import qualified Data.ByteString as BS hiding (reverse) +import qualified Data.ByteString.Char8 as BS8 +import Blaze.ByteString.Builder +import Data.Typeable +import Data.Map (Map) +import qualified Data.Map as Map +import Data.Fix +import Data.Proxy +#ifdef SMTLIB2_WITH_CONSTRAINTS +import Data.Constraint +#endif +import Data.List (genericLength,genericIndex,find) +import Numeric (readInt,readHex) +import Data.Ratio +import Control.Monad.Trans (MonadIO,liftIO) +import Control.Monad.Identity +import Data.Char (isDigit) + +{- | An SMT backend which uses process pipes to communicate with an SMT solver + process. -} +data SMTPipe = SMTPipe { channelIn :: Handle + , channelOut :: Handle + , processHandle :: ProcessHandle } + +renderExpr :: (SMTType t,Monad m) => SMTExpr t -> SMT' m String +renderExpr expr = do + st <- getSMT + return $ renderExpr' st expr + +renderExpr' :: SMTType t => SMTState -> SMTExpr t -> String +renderExpr' st expr + = let lexpr = exprToLisp expr (allVars st) (declaredDataTypes st) + in show lexpr + +instance MonadIO m => SMTBackend SMTPipe m where + smtHandle pipe st req@(SMTGetValue (expr::SMTExpr t)) + = case unmangle :: Unmangling t of + PrimitiveUnmangling _ -> handleNormal pipe st req + ComplexUnmangling f -> do + res <- f (\expr' ann -> smtHandle pipe st (SMTGetValue expr')) expr (extractAnnotation expr) + case res of + Just x -> return x + Nothing -> error $ "smtlib2: Error while unmangling expression "++show expr++" to type "++show (typeOf (undefined::t)) + smtHandle pipe st req = handleNormal pipe st req + +handleNormal :: (MonadIO m,Typeable a) => SMTPipe -> SMTState -> SMTRequest a -> m a +handleNormal pipe st req = do + case cast req of + Just (_::SMTRequest ()) -> return () + _ -> clearInput pipe + case renderSMTRequest st req of + Left l -> putRequest pipe l + Right msg -> liftIO $ IO.hPutStr (channelIn pipe) $ Prelude.unlines (fmap (';':) (Prelude.lines msg)) + handleRequest pipe st req + +renderSMTRequest :: SMTState -> SMTRequest r -> Either L.Lisp String +renderSMTRequest st (SMTGetInfo SMTSolverName) + = Left $ L.List [L.Symbol "get-info",L.Symbol ":name"] +renderSMTRequest st (SMTGetInfo SMTSolverVersion) + = Left $ L.List [L.Symbol "get-info",L.Symbol ":version"] +renderSMTRequest st (SMTAssert expr interp cid) + = let expr1 = exprToLisp expr (allVars st) (declaredDataTypes st) + expr2 = case interp of + Nothing -> expr1 + Just (InterpolationGroup gr) + -> L.List [L.Symbol "!" + ,expr1 + ,L.Symbol ":interpolation-group" + ,L.Symbol (T.pack $ "i"++show gr)] + expr3 = case cid of + Nothing -> expr2 + Just (ClauseId cid) + -> L.List [L.Symbol "!" + ,expr2 + ,L.Symbol ":named" + ,L.Symbol (T.pack $ "_cid"++show cid)] + in Left $ L.List [L.Symbol "assert",expr3] +renderSMTRequest st (SMTCheckSat tactic limits) + = Left $ L.List (if extendedCheckSat + then [L.Symbol "check-sat-using" + ,case tactic of + Just t -> tacticToLisp t + Nothing -> L.Symbol "smt"]++ + (case limitTime limits of + Just t -> [L.Symbol ":timeout" + ,L.Number (L.I t)] + Nothing -> [])++ + (case limitMemory limits of + Just m -> [L.Symbol ":max-memory" + ,L.Number (L.I m)] + Nothing -> []) + else [L.Symbol "check-sat"]) + where + extendedCheckSat = case tactic of + Just _ -> True + _ -> case limitTime limits of + Just _ -> True + _ -> case limitMemory limits of + Just _ -> True + _ -> False +renderSMTRequest st (SMTDeclareDataTypes dts) + = let param x = L.Symbol $ T.pack $ "arg"++show x + in Left $ + L.List [L.Symbol "declare-datatypes" + ,args [ param i | i <- [0..(argCount dts)-1] ] + ,L.List + [ L.List $ [L.Symbol $ T.pack $ dataTypeName dt] + ++ [ L.List $ [L.Symbol $ T.pack $ conName con] + ++ [ L.List [L.Symbol $ T.pack $ fieldName field + ,case fieldSort field of + Fix (NormalSort (NamedSort fTpName _)) -> case find (\dt -> (dataTypeName dt)==fTpName) (dataTypes dts) of + Nothing -> argumentSortToLisp param (fieldSort field) + Just _ -> L.Symbol (T.pack fTpName) + _ -> argumentSortToLisp param (fieldSort field)] + | field <- conFields con ] + | con <- dataTypeConstructors dt ] + | dt <- dataTypes dts ] + ] +renderSMTRequest st (SMTDeclareSort name arity) + = Left $ L.List [L.Symbol "declare-sort",L.Symbol $ T.pack name,L.toLisp arity] +renderSMTRequest st (SMTDeclareFun name) + = let tps = funInfoArgSorts name + rtp = funInfoSort name + in Left $ L.List [L.Symbol "declare-fun" + ,L.Symbol $ T.pack $ getSMTName name + ,args (fmap sortToLisp tps) + ,sortToLisp rtp + ] +renderSMTRequest st (SMTDefineFun name arg definition) + = let ann = extractAnnotation definition + retSort = getSort (getUndef definition) ann + in Left $ L.List [L.Symbol "define-fun" + ,L.Symbol $ T.pack $ getSMTName name + ,args [ L.List [ L.Symbol $ T.pack $ getSMTName n, sortToLisp $ funInfoSort n ] + | n <- arg ] + ,sortToLisp retSort + ,exprToLisp definition (allVars st) (declaredDataTypes st)] +renderSMTRequest st (SMTComment msg) = Right msg +renderSMTRequest st SMTExit = Left $ L.List [L.Symbol "exit"] +renderSMTRequest st (SMTGetInterpolant grps) + = Left $ L.List [L.Symbol "get-interpolant" + ,L.List [ L.Symbol $ T.pack ("i"++show g) | InterpolationGroup g <- grps ] + ] +renderSMTRequest st (SMTSetOption opt) + = Left $ L.List $ [L.Symbol "set-option"] + ++(case opt of + PrintSuccess v -> [L.Symbol ":print-success" + ,L.Symbol $ if v then "true" else "false"] + ProduceModels v -> [L.Symbol ":produce-models" + ,L.Symbol $ if v then "true" else "false"] + SMT.ProduceProofs v -> [L.Symbol ":produce-proofs" + ,L.Symbol $ if v then "true" else "false"] + SMT.ProduceUnsatCores v -> [L.Symbol ":produce-unsat-cores" + ,L.Symbol $ if v then "true" else "false"] + ProduceInterpolants v -> [L.Symbol ":produce-interpolants" + ,L.Symbol $ if v then "true" else "false"] + ) +renderSMTRequest st (SMTSetLogic name) + = Left $ L.List [L.Symbol "set-logic" + ,L.Symbol $ T.pack name] +renderSMTRequest st SMTGetProof + = Left $ L.List [L.Symbol "get-proof"] +renderSMTRequest st SMTGetUnsatCore + = Left $ L.List [L.Symbol "get-unsat-core"] +renderSMTRequest st (SMTSimplify expr) + = let lexpr = exprToLisp expr (allVars st) (declaredDataTypes st) + in Left $ L.List [L.Symbol "simplify" + ,lexpr] +renderSMTRequest st SMTPush = Left $ L.List [L.Symbol "push",L.toLisp (1::Integer)] +renderSMTRequest st SMTPop = Left $ L.List [L.Symbol "pop",L.toLisp (1::Integer)] +renderSMTRequest st (SMTGetValue expr) + = let lexpr = exprToLisp expr (allVars st) (declaredDataTypes st) + in Left $ L.List [L.Symbol "get-value" + ,L.List [lexpr]] +renderSMTRequest st SMTGetModel = Left $ L.List [L.Symbol "get-model"] +renderSMTRequest st (SMTApply tactic) + = Left $ L.List [L.Symbol "apply" + ,tacticToLisp tactic] + +handleRequest :: MonadIO m => SMTPipe -> SMTState -> SMTRequest response -> m response +handleRequest pipe _ (SMTGetInfo SMTSolverName) = do + res <- parseResponse pipe + case res of + L.List [L.Symbol ":name",L.String name] -> return $ T.unpack name + _ -> error "Invalid solver response to 'get-info' name query" +handleRequest pipe _ (SMTGetInfo SMTSolverVersion) = do + res <- parseResponse pipe + case res of + L.List [L.Symbol ":version",L.String name] -> return $ T.unpack name + _ -> error "Invalid solver response to 'get-info' version query" +handleRequest pipe st (SMTAssert _ _ _) = return () +handleRequest pipe _ (SMTCheckSat tactic limits) = do + res <- liftIO $ BS.hGetLine (channelOut pipe) + case res of + "sat" -> return Sat + "sat\r" -> return Sat + "unsat" -> return Unsat + "unsat\r" -> return Unsat + "unknown" -> return Unknown + "unknown\r" -> return Unknown + _ -> error $ "smtlib2: unknown check-sat response: "++show res +handleRequest pipe _ (SMTDeclareDataTypes dts) = return () +handleRequest pipe _ (SMTDeclareSort name arity) = return () +handleRequest pipe _ (SMTDeclareFun name) = return () +handleRequest _ _ (SMTDefineFun name arg definition) = return () +handleRequest _ _ (SMTComment msg) = return () +handleRequest pipe _ SMTExit = do + liftIO $ hClose (channelIn pipe) + liftIO $ hClose (channelOut pipe) + liftIO $ terminateProcess (processHandle pipe) + _ <- liftIO $ waitForProcess (processHandle pipe) + return () +handleRequest pipe st (SMTGetInterpolant grps) = do + val <- parseResponse pipe + case lispToExpr commonFunctions + (findName st) (declaredDataTypes st) gcast (Just $ Fix BoolSort) 0 val of + Just (Just x) -> return x + _ -> error $ "smtlib2: Failed to parse get-interpolant result: "++show val +handleRequest _ _ (SMTSetOption opt) = return () +handleRequest _ _ (SMTSetLogic name) = return () +handleRequest pipe st SMTGetProof = do + res <- parseResponse pipe + let proof = case res of + L.List items -> case findProof items of + Nothing -> res + Just p -> p + _ -> res + case lispToExpr (commonFunctions `mappend` commonTheorems) + (findName st) + (declaredDataTypes st) gcast (Just $ Fix BoolSort) 0 proof of + Just (Just x) -> return x + _ -> error $ "smtlib2: Couldn't parse proof "++show res + where + findProof [] = Nothing + findProof ((L.List [L.Symbol "proof",proof]):_) = Just proof + findProof (x:xs) = findProof xs +handleRequest pipe _ SMTGetUnsatCore = do + res <- parseResponse pipe + case res of + L.List names -> return $ + fmap (\name -> case name of + L.Symbol s -> case T.unpack s of + '_':'c':'i':'d':cid + | all isDigit cid -> ClauseId (read cid) + str -> error $ "Language.SMTLib2.getUnsatCore: Unknown clause id "++str + _ -> error $ "Language.SMTLib2.getUnsatCore: Unknown expression " + ++show name++" in core list." + ) names + _ -> error $ "Language.SMTLib2.getUnsatCore: Unknown response "++show res++" to query." +handleRequest pipe st (SMTSimplify (expr::SMTExpr t)) = do + val <- parseResponse pipe + case lispToExpr commonFunctions + (findName st) (declaredDataTypes st) gcast (Just $ getSort (undefined::t) (extractAnnotation expr)) 0 val of + Just (Just x) -> return x + _ -> error $ "smtlib2: Failed to parse simplify result: "++show val +handleRequest _ _ SMTPush = return () +handleRequest _ _ SMTPop = return () +handleRequest pipe st (SMTGetValue (expr::SMTExpr t)) = do + let ann = extractAnnotation expr + sort = getSort (undefined::t) ann + PrimitiveUnmangling unm = unmangle :: Unmangling t + val <- parseResponse pipe + case val of + L.List [L.List [_,res]] + -> let res' = removeLets res + in case lispToValue' (declaredDataTypes st) (Just sort) res' of + Just val' -> case unm val' ann of + Just val'' -> return val'' + Nothing -> error $ "smtlib2: Failed to unmangle value "++show val'++" to type "++show (typeOf (undefined::t)) + Nothing -> error $ "smtlib2: Failed to parse value from "++show res + _ -> error $ "smtlib2: Unexpected get-value response: "++show val +handleRequest pipe st SMTGetModel = do + val <- parseResponse pipe + case val of + L.List (L.Symbol "model":mdl) -> return $ foldl parseModel (SMTModel Map.empty) mdl + _ -> error $ "smtlib2: Unexpected get-model response: "++show val + where + parseModel cur (L.List [L.Symbol "define-fun", + L.Symbol fname, + L.List args, + rtp, + fun]) = case mapM (\arg -> case arg of + L.List [L.Symbol argName, + argTp] -> case lispToSort argTp of + Just argTp' -> withSort (declaredDataTypes st) argTp' $ + \u ann -> Just (argName,ProxyArg u ann) + _ -> Nothing + _ -> Nothing + ) args of + Just args' -> case lispToSort rtp of + Just rtp' -> let argMp = Map.fromList [ (name,(i,sort)) + | (i,(name,sort)) <- zip [0..] args' ] + funId = case unescapeName (T.unpack fname) of + Nothing -> Nothing + Just (Right idx) -> Just idx + Just (Left name) -> case Map.lookup name (namedVars st) of + Just idx -> Just idx + Nothing -> Nothing + in case lispToExpr commonFunctions (\n -> do + (i,tp) <- Map.lookup n argMp + return $ QVar 0 i tp) + (declaredDataTypes st) + UntypedExpr + (Just rtp') + 1 + fun of + Just res -> case funId of + Nothing -> error $ "smtlib2: Model defines unknown function "++show fname + Just fid -> cur { modelFunctions = Map.insert fid (0,fmap snd args',res) + (modelFunctions cur) + } + Nothing -> error $ "smtlib2: Failed to parse return type: "++show rtp + Nothing -> error $ "smtlib2: Failed to parse argument specification "++show args + parseModel _ def = error $ "smtlib2: Failed to parse model entry: "++show def +handleRequest pipe st (SMTApply tactic) = do + val <- parseResponse pipe + case val of + L.List (L.Symbol "goals":goals) + -> return $ + fmap (\goal -> case goal of + L.List ((L.Symbol "goal"):expr:_) + -> case lispToExpr (commonFunctions `mappend` commonTheorems) + (findName st) + (declaredDataTypes st) gcast (Just $ Fix BoolSort) 0 expr of + Just (Just x) -> x + _ -> error $ "smtlib2: Couldn't parse goal "++show expr + _ -> error $ "smtlib2: Couldn't parse goal description "++show val + ) goals + +renderSMTResponse :: SMTState -> SMTRequest response -> response -> Maybe String +renderSMTResponse _ (SMTGetInfo SMTSolverName) name + = Just $ show $ L.List [L.Symbol ":name",L.String $ T.pack name] +renderSMTResponse _ (SMTGetInfo SMTSolverVersion) vers + = Just $ show $ L.List [L.Symbol ":version",L.String $ T.pack vers] +renderSMTResponse _ (SMTCheckSat _ _) res = case res of + Sat -> Just "sat" + Unsat -> Just "unsat" + Unknown -> Just "unknown" +renderSMTResponse st (SMTGetInterpolant grps) expr + = Just $ renderExpr' st expr +renderSMTResponse st SMTGetProof proof + = Just $ renderExpr' st proof +renderSMTResponse st (SMTSimplify _) expr + = Just $ renderExpr' st expr +renderSMTResponse _ (SMTGetValue _) v = Just $ show v +renderSMTResponse st (SMTApply _) goals + = Just $ show $ + L.List $ [L.Symbol "goals"]++ + [exprToLisp goal (allVars st) (declaredDataTypes st) + | goal <- goals ] +renderSMTResponse _ SMTGetUnsatCore core = Just (show core) +renderSMTResponse _ SMTGetModel mdl = Just (show mdl) +renderSMTResponse _ _ _ = Nothing + +-- | Spawn a new SMT solver process and create a pipe to communicate with it. +createSMTPipe :: String -- ^ Path to the binary of the SMT solver + -> [String] -- ^ Command line arguments to be passed to the SMT solver + -> IO SMTPipe +createSMTPipe solver args = do + let cmd = CreateProcess { cmdspec = RawCommand solver args + , cwd = Nothing + , env = Nothing + , std_in = CreatePipe + , std_out = CreatePipe + , std_err = Inherit + , close_fds = False + , create_group = True +#if MIN_VERSION_process(1,2,0) + , delegate_ctlc = False +#endif + } + (Just hin,Just hout,_,handle) <- createProcess cmd + return $ SMTPipe { channelIn = hin + , channelOut = hout + , processHandle = handle } + +sortToLisp :: Sort -> L.Lisp +sortToLisp s = sortToLisp' sortToLisp (unFix s) + +argumentSortToLisp :: (Integer -> L.Lisp) -> ArgumentSort -> L.Lisp +argumentSortToLisp f sort = case unFix sort of + ArgumentSort i -> f i + NormalSort s -> sortToLisp' (argumentSortToLisp f) s + +sortToLisp' :: (a -> L.Lisp) -> Sort' a -> L.Lisp +sortToLisp' _ BoolSort = L.Symbol "Bool" +sortToLisp' _ IntSort = L.Symbol "Int" +sortToLisp' _ RealSort = L.Symbol "Real" +sortToLisp' _ (BVSort { bvSortWidth = w }) + = L.List [L.Symbol "_", + L.Symbol "BitVec", + L.toLisp w] +sortToLisp' f (ArraySort args' val) + = L.List ((L.Symbol "Array"):(fmap f args')++[f val]) +sortToLisp' _ (NamedSort name []) = L.Symbol (T.pack name) +sortToLisp' f (NamedSort name args) + = L.List $ (L.Symbol $ T.pack name):fmap f args + +-- | Parse a lisp expression into an SMT sort. +lispToSort :: L.Lisp -> Maybe Sort +lispToSort (L.Symbol "Bool") = Just $ Fix BoolSort +lispToSort (L.Symbol "Int") = Just $ Fix IntSort +lispToSort (L.Symbol "Real") = Just $ Fix RealSort +lispToSort (L.List [L.Symbol "_", + L.Symbol "BitVec", + L.Number (L.I n)]) + = Just $ Fix $ BVSort { bvSortWidth = n + , bvSortUntyped = False } +lispToSort (L.List (L.Symbol "Array":args)) = do + argSorts <- mapM lispToSort args' + resSort <- lispToSort res + return $ Fix $ ArraySort argSorts resSort + where + (args',res) = splitLast args + splitLast [s] = ([],s) + splitLast (x:xs) = let (xs',l) = splitLast xs + in (x:xs',l) +lispToSort (L.Symbol x) = Just $ Fix $ NamedSort (T.unpack x) [] +lispToSort (L.List ((L.Symbol x):args)) = do + argSorts <- mapM lispToSort args + return $ Fix $ NamedSort (T.unpack x) argSorts +lispToSort _ = Nothing + +getSMTName :: FunInfo -> String +getSMTName info = escapeName (case funInfoName info of + Nothing -> Right (funInfoId info) + Just name -> Left name) + +findName :: SMTState -> T.Text -> Maybe (SMTExpr Untyped) +findName st name = case unescapeName (T.unpack name) of + Nothing -> Nothing + Just (Right idx) -> case Map.lookup idx (allVars st) of + Nothing -> Nothing + Just (FunInfo { funInfoProxy = _::Proxy (a,t) + , funInfoResAnn = ann + }) -> let expr :: SMTExpr t + expr = Var idx ann + in Just $ mkUntyped expr + Just (Left name') -> case Map.lookup name' (namedVars st) of + Nothing -> Nothing + Just idx -> case Map.lookup idx (allVars st) of + Nothing -> Nothing + Just (FunInfo { funInfoProxy = _::Proxy (a,t) + , funInfoResAnn = ann + }) -> let expr :: SMTExpr t + expr = Var idx ann + in Just $ mkUntyped expr + +mkUntyped :: SMTType t => SMTExpr t -> SMTExpr Untyped +mkUntyped e = case cast e of + Just e' -> e' + Nothing -> case cast e of + Just e' -> entypeValue UntypedExpr e' + Nothing -> UntypedExpr e + +exprToLisp :: SMTExpr t -> Map Integer FunInfo -> DataTypeInfo -> L.Lisp +exprToLisp + = exprToLispWith + (\obj -> error $ "smtlib2: Can't translate internal object "++ + show obj++" to s-expression.") + +exprToLispWith :: (forall a. (Typeable a,Ord a,Show a) => a -> L.Lisp) -> SMTExpr t -> Map Integer FunInfo -> DataTypeInfo -> L.Lisp +exprToLispWith _ (Var idx _) mp _ = case Map.lookup idx mp of + Just info -> L.Symbol $ T.pack $ + escapeName (case funInfoName info of + Nothing -> Right (funInfoId info) + Just name -> Left name) + Nothing -> L.Symbol $ T.pack $ escapeName (Right idx) +exprToLispWith _ (QVar lvl idx _) _ _ = L.Symbol $ T.pack $ "q_"++show lvl++"_"++show idx +exprToLispWith objs (Const x ann) mp dts = case mangle of + PrimitiveMangling f -> valueToLisp dts $ f x ann + ComplexMangling f -> exprToLispWith objs (f x ann) mp dts +exprToLispWith _ (AsArray f arg) mp _ + = let f' = functionGetSymbol mp f arg + (sargs,sres) = functionSignature f arg + in L.List [L.Symbol "_",L.Symbol "as-array",if isOverloaded f + then L.List [f' + ,L.List $ fmap sortToLisp sargs + ,sortToLisp sres] + else f'] +exprToLispWith objs (Forall lvl tps body) mp dts + = L.List [L.Symbol "forall" + ,L.List [L.List [L.Symbol $ T.pack $ "q_"++show lvl++"_"++show i,sortToLisp sort] + | (i,tp) <- Prelude.zip [0..] tps + , let sort = withProxyArg tp getSort ] + ,exprToLispWith objs body mp dts] +exprToLispWith objs (Exists lvl tps body) mp dts + = L.List [L.Symbol "exists" + ,L.List [L.List [L.Symbol $ T.pack $ "q_"++show lvl++"_"++show i,sortToLisp sort] + | (i,tp) <- Prelude.zip [0..] tps + , let sort = withProxyArg tp getSort ] + ,exprToLispWith objs body mp dts] +exprToLispWith objs (Let lvl args body) mp dts + = L.List [L.Symbol "let" + ,L.List [L.List [L.Symbol $ T.pack $ "q_"++show lvl++"_"++show i, + exprToLispWith objs def mp dts] + | (i,def) <- Prelude.zip [0..] args ] + ,exprToLispWith objs body mp dts] +exprToLispWith objs (App fun x) mp dts + = let arg_ann = extractArgAnnotation x + l = functionGetSymbol mp fun arg_ann + x' = fmap (\e -> exprToLispWith objs e mp dts) (fromArgs x) + in if Prelude.null x' + then l + else L.List $ l:x' +exprToLispWith objs (Named expr name nc) mp dts + = let expr' = exprToLispWith objs expr mp dts + in L.List [L.Symbol "!",expr' + ,L.Symbol ":named" + ,L.Symbol $ T.pack $ escapeName (Left (name,nc))] +exprToLispWith objs (InternalObj obj ann) _ _ = objs obj +exprToLispWith objs (UntypedExpr expr) mp dts + = exprToLispWith objs expr mp dts +exprToLispWith objs (UntypedExprValue expr) mp dts + = exprToLispWith objs expr mp dts + +isOverloaded :: SMTFunction a b -> Bool +isOverloaded SMTEq = True +isOverloaded (SMTMap _) = True +isOverloaded (SMTOrd _) = True +isOverloaded (SMTArith _) = True +isOverloaded SMTMinus = True +isOverloaded SMTNeg = True +isOverloaded SMTAbs = True +isOverloaded SMTDistinct = True +isOverloaded SMTITE = True +isOverloaded (SMTBVComp _) = True +isOverloaded (SMTBVBin _) = True +isOverloaded (SMTBVUn _) = True +isOverloaded SMTSelect = True +isOverloaded SMTStore = True +isOverloaded (SMTConstArray _) = True +isOverloaded SMTConcat = True +isOverloaded (SMTExtract _ _) = True +isOverloaded _ = False + +functionSignature :: (Args a,SMTType b) => SMTFunction a b -> ArgAnnotation a -> ([Sort],Sort) +functionSignature f argAnn = withUndef f $ + \ua ur -> (getSorts ua argAnn, + getSort ur resAnn) + where + resAnn = inferResAnnotation f argAnn + withUndef :: SMTFunction a b -> (a -> b -> r) -> r + withUndef _ f = f undefined undefined + +functionGetSymbol :: Map Integer FunInfo -> SMTFunction a b -> ArgAnnotation a -> L.Lisp +functionGetSymbol _ SMTEq _ = L.Symbol "=" +functionGetSymbol mp fun@(SMTMap f) ann + = L.List [L.Symbol "_", + L.Symbol "map", + sym] + where + getUndefI :: SMTFunction p (SMTArray i res) -> i + getUndefI _ = undefined + getUndefA :: SMTFunction arg res -> arg + getUndefA _ = undefined + ui = getUndefI fun + ua = getUndefA f + (ann_i,ann_v) = inferLiftedAnnotation ua ui ann + sym' = functionGetSymbol mp f ann_v + (sigArg,sigRes) = functionSignature f ann_v + sym = if isOverloaded f + then L.List [sym', + L.List (fmap sortToLisp sigArg), + sortToLisp sigRes] + else sym' +functionGetSymbol mp (SMTFun name _) _ = case Map.lookup name mp of + Just info -> L.Symbol (T.pack $ getSMTName info) +functionGetSymbol _ (SMTBuiltIn name _) _ = L.Symbol $ T.pack name +functionGetSymbol _ (SMTOrd op) _ = L.Symbol $ case op of + Ge -> ">=" + Gt -> ">" + Le -> "<=" + Lt -> "<" +functionGetSymbol _ (SMTArith op) _ = L.Symbol $ case op of + Plus -> "+" + Mult -> "*" +functionGetSymbol _ SMTMinus _ = L.Symbol "-" +functionGetSymbol _ (SMTIntArith op) _ = L.Symbol $ case op of + Div -> "div" + Mod -> "mod" + Rem -> "rem" +functionGetSymbol _ SMTDivide _ = L.Symbol "/" +functionGetSymbol _ SMTNeg _ = L.Symbol "-" +functionGetSymbol _ SMTAbs _ = L.Symbol "abs" +functionGetSymbol _ SMTNot _ = L.Symbol "not" +functionGetSymbol _ (SMTLogic op) _ = case op of + And -> L.Symbol "and" + Or -> L.Symbol "or" + XOr -> L.Symbol "xor" + Implies -> L.Symbol "=>" +functionGetSymbol _ SMTDistinct _ = L.Symbol "distinct" +functionGetSymbol _ SMTToReal _ = L.Symbol "to_real" +functionGetSymbol _ SMTToInt _ = L.Symbol "to_int" +functionGetSymbol _ SMTITE _ = L.Symbol "ite" +functionGetSymbol _ (SMTBVComp op) _ = L.Symbol $ case op of + BVULE -> "bvule" + BVULT -> "bvult" + BVUGE -> "bvuge" + BVUGT -> "bvugt" + BVSLE -> "bvsle" + BVSLT -> "bvslt" + BVSGE -> "bvsge" + BVSGT -> "bvsgt" +functionGetSymbol _ (SMTBVBin op) _ = L.Symbol $ case op of + BVAdd -> "bvadd" + BVSub -> "bvsub" + BVMul -> "bvmul" + BVURem -> "bvurem" + BVSRem -> "bvsrem" + BVUDiv -> "bvudiv" + BVSDiv -> "bvsdiv" + BVSHL -> "bvshl" + BVLSHR -> "bvlshr" + BVASHR -> "bvashr" + BVXor -> "bvxor" + BVAnd -> "bvand" + BVOr -> "bvor" +functionGetSymbol _ (SMTBVUn op) _ = case op of + BVNot -> L.Symbol "bvnot" + BVNeg -> L.Symbol "bvneg" +functionGetSymbol _ SMTSelect _ = L.Symbol "select" +functionGetSymbol _ SMTStore _ = L.Symbol "store" +functionGetSymbol _ f@(SMTConstArray i_ann) v_ann + = withUndef f $ + \u_arr -> L.List [L.Symbol "as" + ,L.Symbol "const" + ,sortToLisp $ getSort u_arr (i_ann,v_ann)] + where + withUndef :: SMTFunction (SMTExpr v) (SMTArray i v) + -> (SMTArray i v -> a) -> a + withUndef _ f' = f' undefined +functionGetSymbol _ SMTConcat _ = L.Symbol "concat" +functionGetSymbol _ f@(SMTExtract prStart prLen) ann + = L.List [L.Symbol "_" + ,L.Symbol "extract" + ,L.Number $ L.I (start+len-1) + ,L.Number $ L.I start] + where + start = reflectNat prStart 0 + len = reflectNat prLen 0 +functionGetSymbol _ (SMTConstructor (Constructor _ _ con)) _ = L.Symbol $ T.pack (conName con) +functionGetSymbol _ (SMTConTest (Constructor _ _ con)) _ = L.Symbol $ T.pack $ "is-"++(conName con) +functionGetSymbol _ (SMTFieldSel (Field _ _ _ f)) _ = L.Symbol $ T.pack (fieldName f) +functionGetSymbol _ (SMTDivisible n) _ = L.List [L.Symbol "_",L.Symbol "divisible",L.Number $ L.I n] + +clearInput :: MonadIO m => SMTPipe -> m () +clearInput pipe = do + r <- liftIO $ hReady (channelOut pipe) + if r + then (do + _ <- liftIO $ BS.hGetSome (channelOut pipe) 1024 + clearInput pipe) + else return () + +putRequest :: MonadIO m => SMTPipe -> L.Lisp -> m () +putRequest pipe expr = do + clearInput pipe + liftIO $ toByteStringIO (BS.hPutStr $ channelIn pipe) (mappend (L.fromLispExpr expr) flush) + liftIO $ BS.hPutStrLn (channelIn pipe) "" + liftIO $ hFlush (channelIn pipe) + +parseResponse :: MonadIO m => SMTPipe -> m L.Lisp +parseResponse pipe = do + str <- liftIO $ BS.hGetLine (channelOut pipe) + let continue (Done _ r) = return r + continue res@(Partial _) = do + line <- liftIO $ BS.hGetLine (channelOut pipe) + continue (feed (feed res line) (BS8.singleton '\n')) + continue (Fail str' ctx msg) = error $ "Error parsing "++show str'++" response in "++show ctx++": "++msg + continue $ parse L.lisp (BS8.snoc str '\n') + +args :: [L.Lisp] -> L.Lisp +args [] = L.Symbol "()" +args xs = L.List xs + +removeLets :: L.Lisp -> L.Lisp +removeLets = removeLets' Map.empty + where + removeLets' mp (L.List [L.Symbol "let",L.List decls,body]) + = let nmp = Map.union mp + (Map.fromList + [ (name,removeLets' nmp expr) + | L.List [L.Symbol name,expr] <- decls ]) + in removeLets' nmp body + removeLets' mp (L.Symbol sym) = case Map.lookup sym mp of + Nothing -> L.Symbol sym + Just r -> r + removeLets' mp (L.List entrs) = L.List $ fmap (removeLets' mp) entrs + removeLets' _ x = x + +newtype FunctionParser = FunctionParser { parseFun :: L.Lisp + -> FunctionParser + -> DataTypeInfo + -> Maybe FunctionParser' } + +instance Monoid FunctionParser where + mempty = FunctionParser $ \_ _ _ -> Nothing + mappend p1 p2 = FunctionParser $ \l fun dts -> case parseFun p1 l fun dts of + Nothing -> parseFun p2 l fun dts + Just r -> Just r + +data FunctionParser' + = OverloadedParser { sortConstraint :: [Sort] -> Bool + , deriveRetSort :: [Sort] -> Maybe Sort + , parseOverloaded :: forall a. [Sort] -> Sort + -> (forall arg res. (Liftable arg,SMTType res) => SMTFunction arg res -> a) + -> Maybe a } + | DefinedParser { definedArgSig :: [Sort] + , definedRetSig :: Sort + , parseDefined :: forall a. (forall arg res. (Liftable arg,SMTType res) => SMTFunction arg res -> a) + -> Maybe a } + +-- | A map which contains signatures for a few common theorems which can be used in the proofs which 'getProof' returns. +commonTheorems :: FunctionParser +commonTheorems = mconcat + [nameParser (L.Symbol "|unit-resolution|") + (OverloadedParser (const True) + (const $ Just $ Fix BoolSort) + $ \_ _ f -> Just $ f (SMTBuiltIn "|unit-resolution|" () :: SMTFunction [SMTExpr Bool] Bool)) + ,simpleParser (SMTBuiltIn "asserted" () :: SMTFunction (SMTExpr Bool) Bool) + ,simpleParser (SMTBuiltIn "hypothesis" () :: SMTFunction (SMTExpr Bool) Bool) + ,simpleParser (SMTBuiltIn "lemma" () :: SMTFunction (SMTExpr Bool) Bool) + ,simpleParser (SMTBuiltIn "monotonicity" () :: SMTFunction (SMTExpr Bool,SMTExpr Bool) Bool) + ,simpleParser (SMTBuiltIn "trans" () :: SMTFunction (SMTExpr Bool,SMTExpr Bool,SMTExpr Bool) Bool) + ,simpleParser (SMTBuiltIn "rewrite" () :: SMTFunction (SMTExpr Bool) Bool) + ,simpleParser (SMTBuiltIn "mp" () :: SMTFunction (SMTExpr Bool,SMTExpr Bool,SMTExpr Bool) Bool)] + +lispToValue :: DataTypeInfo -> Maybe Sort -> L.Lisp -> Maybe Value +lispToValue _ sort (L.Symbol "true") = case sort of + Nothing -> Just $ BoolValue True + Just (Fix BoolSort) -> Just $ BoolValue True + Just _ -> Nothing +lispToValue _ sort (L.Symbol "false") = case sort of + Nothing -> Just $ BoolValue False + Just (Fix BoolSort) -> Just $ BoolValue False + Just _ -> Nothing +lispToValue _ sort (L.Number (L.I x)) = case sort of + Nothing -> Just $ IntValue x + Just (Fix RealSort) -> Just $ RealValue (fromInteger x) + Just (Fix IntSort) -> Just $ IntValue x + Just (Fix (BVSort { bvSortWidth = w })) -> Just $ BVValue { bvValueWidth = w + , bvValueValue = x } + Just _ -> Nothing +lispToValue dts sort (L.List [L.Symbol "-",v]) + = case lispToValue dts sort v of + Just (RealValue x) -> Just $ RealValue (-x) + Just (IntValue x) -> Just $ IntValue (-x) + _ -> Nothing +lispToValue _ sort (L.Number (L.D x)) = case sort of + Nothing -> Just $ RealValue (realToFrac x) + Just (Fix RealSort) -> Just $ RealValue (realToFrac x) + Just _ -> Nothing +lispToValue dts sort (L.List [L.Symbol "/",x,y]) = case sort of + Nothing -> result + Just (Fix RealSort) -> result + Just _ -> Nothing + where + result = do + RealValue x' <- lispToValue dts (Just $ Fix RealSort) x + RealValue y' <- lispToValue dts (Just $ Fix RealSort) y + return $ RealValue $ x' / y' +lispToValue _ sort (L.Symbol s) = case sort of + Nothing -> result + Just (Fix (BVSort {})) -> result + Just _ -> Nothing + where + result = case T.unpack s of + '#':'b':rest -> let len = genericLength rest + in case readInt 2 + (\x -> x=='0' || x=='1') + (\x -> if x=='0' then 0 else 1) + rest of + [(v,_)] -> Just $ BVValue { bvValueWidth = len + , bvValueValue = v } + _ -> Nothing + '#':'x':rest -> let len = (genericLength rest)*4 + in case readHex rest of + [(v,_)] -> Just $ BVValue { bvValueWidth = len + , bvValueValue = v } + _ -> Nothing + _ -> Nothing +lispToValue _ sort (L.List [L.Symbol "_",L.Symbol val,L.Number (L.I bits)]) + = case sort of + Nothing -> result + Just (Fix (BVSort {})) -> result + Just _ -> Nothing + where + result = case T.unpack val of + 'b':'v':num -> Just $ BVValue { bvValueWidth = fromIntegral bits + , bvValueValue = read num } + _ -> Nothing +lispToValue _ _ _ = Nothing + +lispToValue' :: DataTypeInfo -> Maybe Sort -> L.Lisp -> Maybe Value +lispToValue' dts sort l = case lispToValue dts sort l of + Just res -> Just res + Nothing -> case sort of + Just (Fix (NamedSort name argSorts)) -> lispToConstr dts (Just (name,argSorts)) l + +lispToConstr :: DataTypeInfo -> Maybe (String,[Sort]) -> L.Lisp -> Maybe Value +lispToConstr dts sort (L.List [L.Symbol "as", + expr, + dt]) = do + sort' <- lispToSort dt + case sort' of + Fix (NamedSort name args) -> lispToConstr dts (Just (name,args)) expr +lispToConstr dts sort (L.Symbol n) + = let rn = T.unpack n + in case Map.lookup rn (constructors dts) of + Just (constr,dt,coll) + -> Just (ConstrValue rn [] (case sort of + Just s -> Just s + Nothing -> Nothing)) +lispToConstr dts sort (L.List ((L.Symbol name):args)) = do + let (constr,dt,coll) = case Map.lookup (T.unpack name) (constructors dts) of + Just r -> r + Nothing -> error $ "smtlib2: Can't find constructor for "++(T.unpack name) + argSorts = fmap (\field -> getArgSort (fieldSort field) + ) (conFields constr) + args' <- mapM (\(l,s) -> lispToValue' dts s l) (zip args argSorts) + return $ ConstrValue (T.unpack name) args' + (case sort of + Just sort' -> Just sort' + Nothing -> Nothing) + where + getArgSort (Fix (ArgumentSort n)) = case sort of + Just (_,args) -> Just $ args `genericIndex` n + _ -> Nothing + getArgSort (Fix (NormalSort s)) = case s of + BoolSort -> Just $ Fix BoolSort + IntSort -> Just $ Fix IntSort + RealSort -> Just $ Fix RealSort + BVSort w u -> Just $ Fix (BVSort w u) + ArraySort idx v -> do + idx' <- mapM getArgSort idx + v' <- getArgSort v + return $ Fix $ ArraySort idx' v' + NamedSort name args -> do + args' <- mapM getArgSort args + return $ Fix $ NamedSort name args' +lispToConstr _ _ _ = Nothing + +valueToLisp :: DataTypeInfo -> Value -> L.Lisp +valueToLisp _ (BoolValue False) = L.Symbol "false" +valueToLisp _ (BoolValue True) = L.Symbol "true" +valueToLisp _ (IntValue i) = if i<0 + then L.List [L.Symbol "-" + ,L.Number $ L.I (abs i)] + else L.Number $ L.I i +valueToLisp _ (RealValue i) + = let res = L.List [L.Symbol "/" + ,L.Number $ L.I (abs $ numerator i) + ,L.Number $ L.I $ denominator i] + in if i<0 + then L.List [L.Symbol "-" + ,res] + else res +valueToLisp _ (BVValue { bvValueWidth = w + , bvValueValue = v }) + = L.List [L.Symbol "_" + ,L.Symbol $ T.pack $ "bv"++(if v>=0 + then show v + else show (2^w + v)) + ,L.Number $ L.I w] +valueToLisp dts (ConstrValue name vals sort) + = let constr = case sort of + Just (tp,sort') -> L.List [L.Symbol "as" + ,L.Symbol $ T.pack name + ,if null sort' + then L.Symbol $ T.pack tp + else L.List $ [L.Symbol $ T.pack tp]++(fmap sortToLisp sort')] + Nothing -> L.Symbol $ T.pack name + in case vals of + [] -> constr + _ -> L.List (constr:(fmap (valueToLisp dts) vals)) + +-- | Parse a lisp expression into an SMT expression. +-- Since we cannot know what type the expression might have, we pass a +-- general function which may take any SMT expression and produce the desired +-- result. +lispToExpr :: FunctionParser -- ^ The parser to use for function symbols + -> (T.Text -> Maybe (SMTExpr Untyped)) -- ^ How to handle variable names + -> DataTypeInfo -- ^ Information about declared data types + -> (forall a. SMTType a => SMTExpr a -> b) -- ^ A function to apply to the resulting SMT expression + -> Maybe Sort -- ^ If you know the sort of the expression, you can pass it here. + -> Integer -- ^ The current quantification level + -> L.Lisp -- ^ The lisp expression to parse + -> Maybe b +lispToExpr fun bound dts f expected lvl l = case lispToValue dts expected l of + Just val -> valueToHaskell dts + (\_ (val'::t) ann + -> asValueType (undefined::t) ann $ + \(_::tv) ann' -> case cast (val',ann') of + Just (rval::tv,rann::SMTAnnotation tv) -> f $ Const rval rann + ) expected val + Nothing -> case preprocessHack l of + L.Symbol name -> case bound name of + Nothing -> Nothing + Just subst -> entype (\expr -> Just $ f expr) subst + L.List [L.Symbol "forall",L.List args',body] + -> fmap f $ quantToExpr Forall fun bound dts args' lvl body + L.List [L.Symbol "exists",L.List args',body] + -> fmap f $ quantToExpr Exists fun bound dts args' lvl body + L.List [L.Symbol "let",L.List args',body] + -> parseLet fun bound dts f expected args' lvl body + L.List [L.Symbol "_",L.Symbol "as-array",fsym] + -> case parseFun fun fsym fun dts of + Nothing -> Nothing + Just (DefinedParser arg_sort _ parse) + -> parse $ \(rfun :: SMTFunction arg res) -> case getArgAnnotation (undefined::arg) arg_sort of + (ann,[]) -> f (AsArray rfun ann) + (_,_) -> error "smtlib2: Arguments not wholy parsed." + Just _ -> error "smtlib2: as-array can't handle overloaded functions." + L.List (fsym:args') -> case parseFun fun fsym fun dts of + Nothing -> Nothing + Just (OverloadedParser constr derive parse) + -> do + nargs <- lispToExprs constr args' + let arg_tps = fmap (entype $ \(expr::SMTExpr t) + -> getSort (undefined::t) (extractAnnotation expr) + ) nargs + parse arg_tps + (case derive arg_tps of + Nothing -> case expected of + Nothing -> error $ "smtlib2: Couldn't infer return type of "++show l + Just s -> s + Just s -> s) $ + \(rfun :: SMTFunction arg res) + -> case (do + let (ann,[]) = getArgAnnotation (undefined::arg) arg_tps + (rargs,rest) <- toArgs ann nargs + case rest of + [] -> Just $ App rfun rargs + _ -> Nothing) of + Just e -> f e + Nothing -> error $ "smtlib2: Wrong arguments for function "++show fsym++": "++show arg_tps++" ("++show args'++")." + Just (DefinedParser arg_tps _ parse) -> do + nargs <- mapM (\(el,tp) -> lispToExpr fun bound dts mkUntyped (Just tp) lvl el) + (zip args' arg_tps) + parse $ \(rfun :: SMTFunction arg res) + -> case (do + let (ann,[]) = getArgAnnotation (undefined::arg) arg_tps + (rargs,rest) <- toArgs ann nargs + case rest of + [] -> Just $ App rfun rargs + _ -> Nothing) of + Just e -> f e + Nothing -> error $ "smtlib2: Wrong arguments for function "++show fsym + _ -> Nothing + where + lispToExprs constr exprs = do + res <- mapM (\arg -> lispToExpr fun bound dts mkUntyped Nothing lvl arg) exprs + let sorts = fmap (entype exprSort) res + if constr sorts + then return res + else (case generalizeSorts sorts of + Just sorts' -> mapM (\(arg,sort') -> lispToExpr fun bound dts mkUntyped (Just sort') lvl arg) (zip exprs sorts') + Nothing -> return res) + preprocessHack (L.List ((L.Symbol "concat"):args)) = foldl1 (\expr arg -> L.List [L.Symbol "concat",expr,arg]) args + preprocessHack x = x + +generalizeSort :: Sort -> Maybe Sort +generalizeSort (Fix (BVSort i False)) = Just $ Fix $ BVSort i True +generalizeSort (Fix (ArraySort idx cont)) = case generalizeSorts idx of + Just idx' -> case generalizeSort cont of + Just cont' -> Just $ Fix $ ArraySort idx' cont' + Nothing -> Just $ Fix $ ArraySort idx' cont + Nothing -> case generalizeSort cont of + Just cont' -> Just $ Fix $ ArraySort idx cont' + Nothing -> Nothing +generalizeSort (Fix (NamedSort n args)) = case generalizeSorts args of + Nothing -> Nothing + Just args' -> Just $ Fix $ NamedSort n args' +generalizeSort _ = Nothing + +generalizeSorts :: [Sort] -> Maybe [Sort] +generalizeSorts [] = Nothing +generalizeSorts (x:xs) = case generalizeSort x of + Nothing -> case generalizeSorts xs of + Just xs' -> Just $ x:xs' + Nothing -> Nothing + Just x' -> case generalizeSorts xs of + Nothing -> Just $ x':xs + Just xs' -> Just $ x':xs' + +exprSort :: SMTType a => SMTExpr a -> Sort +exprSort (expr::SMTExpr a) = getSort (undefined::a) (extractAnnotation expr) + +quantToExpr :: (Integer -> [ProxyArg] -> SMTExpr Bool -> SMTExpr Bool) + -> FunctionParser + -> (T.Text -> Maybe (SMTExpr Untyped)) + -> DataTypeInfo + -> [L.Lisp] -> Integer -> L.Lisp -> Maybe (SMTExpr Bool) +quantToExpr con fun bound dts args lvl body = do + argLst <- mapM (\el -> case el of + L.List [L.Symbol name,tp] -> do + sort <- lispToSort tp + return (name,withSort dts sort ProxyArg) + _ -> Nothing + ) args + let argMp = Map.fromList [ (name,(i,tp)) + | (i,(name,tp)) <- Prelude.zip [0..] argLst ] + bound' name = case Map.lookup name argMp of + Just (idx,tp) -> Just (QVar lvl idx tp) + Nothing -> bound name + lispToExpr fun bound' dts + (\body' -> case cast body' of + Just body'' -> con lvl (fmap snd argLst) body'' + ) (Just $ Fix BoolSort) (lvl+1) body + +parseLet :: FunctionParser + -> (T.Text -> Maybe (SMTExpr Untyped)) + -> DataTypeInfo + -> (forall a. SMTType a => SMTExpr a -> b) + -> Maybe Sort + -> [L.Lisp] -> Integer -> L.Lisp -> Maybe b +parseLet fun bound dts app expected args lvl body = do + argLst <- mapM (\el -> case el of + L.List [L.Symbol name,expr] -> do + expr' <- lispToExpr fun bound dts UntypedExpr Nothing (lvl+1) expr + return (name,expr') + _ -> Nothing + ) args + let argMp = Map.fromList [ (name,(i,extractAnnotation expr)) + | (i,(name,expr)) <- Prelude.zip [0..] argLst ] + bound' name = case Map.lookup name argMp of + Just (idx,tp) -> Just (QVar lvl idx tp) + Nothing -> bound name + lispToExpr fun bound' dts + (\body' -> app (Let lvl (fmap snd argLst) body') + ) expected (lvl+1) body +{- +data LetStruct where + LetStruct :: SMTType a => SMTAnnotation a -> SMTExpr a -> (SMTExpr a -> LetStruct) -> LetStruct + EndLet :: SMTType a => SMTExpr a -> LetStruct + +parseLetStruct :: FunctionParser + -> (T.Text -> Maybe (SMTExpr Untyped)) + -> DataTypeInfo + -> Maybe Sort + -> [L.Lisp] -> L.Lisp -> LetStruct +parseLetStruct fun bound tps expected (L.List [L.Symbol name,expr]:rest) arg + = case lispToExpr fun bound tps + (\expr' -> LetStruct (extractAnnotation expr') expr' $ + \sym -> parseLetStruct fun + (\txt -> if txt==name + then Just $ mkUntyped sym + else bound txt) tps expected rest arg + ) Nothing expr of + Nothing -> error $ "smtlib2: Failed to parse argument in let-expression "++show expr + Just x -> x +parseLetStruct fun bound tps expected [] arg + = case lispToExpr fun bound tps EndLet expected arg of + Nothing -> error $ "smtlib2: Failed to parse body of let-expression: "++show arg + Just x -> x +parseLetStruct _ _ _ _ (el:_) _ = error $ "smtlib2: Invalid entry "++show el++" in let construct." + +extractType :: (forall a. SMTType a => a -> b) -> LetStruct -> b +extractType f (EndLet x) = f (getUndef x) +extractType f (LetStruct _ expr g) = extractType f (g expr) + +convertLetStructT :: SMTType a => LetStruct -> SMTExpr a +convertLetStructT (EndLet x) = case gcast x of + Just x' -> x' + Nothing -> error "smtlib2: Type error while converting let structure." +convertLetStructT (LetStruct ann x g) = Let ann x (\sym -> convertLetStructT (g sym)) + +convertLetStruct :: (forall a. SMTType a => SMTExpr a -> b) -> LetStruct -> b +convertLetStruct f x + = extractType + (\(_::t) -> f (convertLetStructT x :: SMTExpr t)) x +-} +withFirstArgSort :: DataTypeInfo -> L.Lisp -> [Sort] -> (forall t. SMTType t => t -> SMTAnnotation t -> a) -> a +withFirstArgSort dts _ (s:rest) f = case s of + Fix (BVSort i False) -> if any (\sort -> case sort of + Fix (BVSort _ True) -> True + _ -> False) rest + then withSort dts (Fix $ BVSort i True) f + else withSort dts s f + _ -> withSort dts s f +withFirstArgSort _ sym [] _ = error $ "smtlib2: Function "++show sym++" needs at least one argument." + +nameParser :: L.Lisp -> FunctionParser' -> FunctionParser +nameParser name sub = FunctionParser (\sym _ _ -> if sym==name + then Just sub + else Nothing) + +allEqConstraint :: [Sort] -> Bool +allEqConstraint (x:xs) = all (==x) xs +allEqConstraint [] = True + +simpleParser :: (Liftable arg,SMTType res,Unit (ArgAnnotation arg),Unit (SMTAnnotation res)) + => SMTFunction arg res -> FunctionParser +simpleParser fun + = let fsym = functionGetSymbol (error "smtlib2: Don't lookup names in simpleParser") fun unit + (uargs,ures) = getFunUndef fun + in nameParser fsym (DefinedParser + (getSorts uargs unit) + (getSort ures unit) + $ \f -> Just $ f fun) + +-- | A parser for all available SMT logics. +commonFunctions :: FunctionParser +commonFunctions = mconcat + [fieldParser + ,constructorParser + ,eqParser + ,mapParser + ,ordOpParser + ,arithOpParser + ,minusParser + ,intArithParser + ,divideParser + ,absParser + ,logicParser + ,iteParser + ,distinctParser + ,toRealParser + ,toIntParser + ,bvCompParser + ,bvBinOpParser + ,bvUnOpParser + ,selectParser + ,storeParser + ,constArrayParser + ,concatParser + ,extractParser + ,sigParser + ,divisibleParser] + +eqParser, + mapParser, + ordOpParser, + arithOpParser, + minusParser, + intArithParser, + divideParser, + absParser, + logicParser, + iteParser, + distinctParser, + toRealParser, + toIntParser, + bvCompParser, + bvBinOpParser, + bvUnOpParser, + selectParser, + storeParser, + constArrayParser, + concatParser, + extractParser, + sigParser, + divisibleParser :: FunctionParser +eqParser = FunctionParser v + where + v (L.Symbol "=") rec dts = Just $ OverloadedParser allEqConstraint + (const $ Just $ getSort (undefined::Bool) ()) $ + \sort_arg _ f + -> withFirstArgSort dts "=" sort_arg $ + \(_::t) _ -> Just $ f (SMTEq :: SMTFunction [SMTExpr t] Bool) + v _ _ _ = Nothing + +mapParser = FunctionParser v + where + v (L.List [L.Symbol "_" + ,L.Symbol "map" + ,fun]) rec dts +#ifdef SMTLIB2_WITH_CONSTRAINTS + = case parseFun rec fun rec dts of + Nothing -> Nothing + Just (DefinedParser _ ret_sig parse) + -> Just $ OverloadedParser + { sortConstraint = const True + , deriveRetSort = \arg -> case arg of + Fix (ArraySort i _):_ -> Just (Fix $ ArraySort i ret_sig) + _ -> error "smtlib2: map function must have arrays as arguments." + , parseOverloaded = \_ ret f + -> let idx_sort = case ret of + Fix (ArraySort i _) -> i + _ -> error "smtlib2: map function must have arrays as return type." + in parse $ \(fun' :: SMTFunction arg res) + -> withSorts dts idx_sort $ + \(_::i) _ + -> let res = SMTMap fun' :: SMTFunction (Lifted arg i) (SMTArray i res) + in case getConstraint (Proxy :: Proxy (arg,i)) of + Dict -> f res + } + Just _ -> error "smtlib2: map function can't handle overloaded functions." +#else + = Just $ error "smtlib2: Compile smtlib2 with -fWithConstraints to enable parsing of map functions" +#endif + v _ _ _ = Nothing + +ordOpParser = FunctionParser $ \sym _ dts -> case sym of + L.Symbol ">=" -> p sym Ge dts + L.Symbol ">" -> p sym Gt dts + L.Symbol "<=" -> p sym Le dts + L.Symbol "<" -> p sym Lt dts + _ -> Nothing + where + p :: L.Lisp -> SMTOrdOp -> DataTypeInfo -> Maybe FunctionParser' + p sym op dts = Just $ OverloadedParser allEqConstraint (const $ Just $ getSort (undefined::Bool) ()) $ + \sort_arg _ f -> withFirstArgSort dts sym sort_arg $ + \(_::t) _ + -> Just $ f (SMTOrd op :: SMTFunction (SMTExpr t,SMTExpr t) Bool) + +arithOpParser = FunctionParser $ \sym _ dts -> case sym of + L.Symbol "+" -> Just $ OverloadedParser allEqConstraint (\sorts -> Just (head sorts)) $ + \_ sort_ret f + -> withNumSort dts sort_ret $ + \(_::t) _ + -> f (SMTArith Plus::SMTFunction [SMTExpr t] t) + L.Symbol "*" -> Just $ OverloadedParser allEqConstraint (\sorts -> Just (head sorts)) $ + \_ sort_ret f + -> withNumSort dts sort_ret $ + \(_::t) _ + -> f (SMTArith Mult::SMTFunction [SMTExpr t] t) + _ -> Nothing + +minusParser = FunctionParser $ \sym _ dts -> case sym of + L.Symbol "-" -> Just $ OverloadedParser allEqConstraint (\sorts -> Just (head sorts)) $ + \sort_arg _ f -> case sort_arg of + [] -> error "smtlib2: minus function needs at least one argument" + [s] -> withNumSort dts s $ \(_::t) _ -> f (SMTNeg::SMTFunction (SMTExpr t) t) + (s:_) -> withNumSort dts s $ \(_::t) _ -> f (SMTMinus::SMTFunction (SMTExpr t,SMTExpr t) t) + _ -> Nothing + +intArithParser = mconcat [simpleParser (SMTIntArith Div) + ,simpleParser (SMTIntArith Mod) + ,simpleParser (SMTIntArith Rem)] + +divideParser = simpleParser SMTDivide + +absParser = FunctionParser $ \sym _ dts -> case sym of + L.Symbol "abs" -> Just $ OverloadedParser (const True) (\sorts -> Just $ head sorts) $ + \_ sort_ret f + -> withNumSort dts sort_ret $ \(_::t) _ -> f (SMTAbs::SMTFunction (SMTExpr t) t) + _ -> Nothing + +logicParser = mconcat $ + (simpleParser SMTNot) + :[ nameParser (L.Symbol name) + (OverloadedParser (const True) + (const $ Just $ getSort (undefined::Bool) ()) + $ \_ _ f -> Just $ f (SMTLogic p)) + | (name,p) <- [("and",And),("or",Or),("xor",XOr),("=>",Implies)]] + +distinctParser = FunctionParser $ \sym _ dts -> case sym of + L.Symbol "distinct" -> Just $ OverloadedParser allEqConstraint + (const $ Just $ getSort (undefined::Bool) ()) $ + \sort_arg _ f + -> withFirstArgSort dts "distinct" sort_arg $ + \(_::t) _ -> Just $ f (SMTDistinct::SMTFunction [SMTExpr t] Bool) + _ -> Nothing + +toRealParser = simpleParser SMTToReal +toIntParser = simpleParser SMTToInt + +iteParser = FunctionParser $ \sym _ dts -> case sym of + L.Symbol "ite" -> Just $ OverloadedParser (\sorts -> case sorts of + [_,s1,s2] -> s1==s2 + _ -> False) + (\sorts -> case sorts of + [_,s,_] -> Just s + _ -> error $ "smtlib2: Wrong number of arguments to ite (expected 3, got "++show (length sorts)++".") $ + \_ sort_ret f + -> withSort dts sort_ret $ + \(_::t) _ -> Just $ f (SMTITE :: SMTFunction (SMTExpr Bool,SMTExpr t,SMTExpr t) t) + _ -> Nothing + +bvCompParser = FunctionParser $ \sym _ _ -> case sym of + L.Symbol "bvule" -> p BVULE + L.Symbol "bvult" -> p BVULT + L.Symbol "bvuge" -> p BVUGE + L.Symbol "bvugt" -> p BVSLE + L.Symbol "bvsle" -> p BVSLE + L.Symbol "bvslt" -> p BVSLT + L.Symbol "bvsge" -> p BVSGE + L.Symbol "bvsgt" -> p BVSGT + _ -> Nothing + where + p :: SMTBVCompOp -> Maybe FunctionParser' + p op = Just $ OverloadedParser allEqConstraint (const $ Just $ getSort (undefined::Bool) ()) $ + \sort_arg _ f -> case sort_arg of + (Fix (BVSort i False):_) + -> reifyNat i $ \(_::Proxy n) + -> Just $ f (SMTBVComp op::SMTFunction (SMTExpr (BitVector (BVTyped n)), + SMTExpr (BitVector (BVTyped n))) Bool) + (Fix (BVSort _ True):_) + -> Just $ f (SMTBVComp op::SMTFunction (SMTExpr (BitVector BVUntyped), + SMTExpr (BitVector BVUntyped)) Bool) + _ -> error "smtlib2: Bitvector comparision needs bitvector arguments." + +bvBinOpParser = FunctionParser $ \sym _ _ -> case sym of + L.Symbol "bvadd" -> p BVAdd + L.Symbol "bvsub" -> p BVSub + L.Symbol "bvmul" -> p BVMul + L.Symbol "bvurem" -> p BVURem + L.Symbol "bvsrem" -> p BVSRem + L.Symbol "bvudiv" -> p BVUDiv + L.Symbol "bvsdiv" -> p BVSDiv + L.Symbol "bvshl" -> p BVSHL + L.Symbol "bvlshr" -> p BVLSHR + L.Symbol "bvashr" -> p BVASHR + L.Symbol "bvxor" -> p BVXor + L.Symbol "bvand" -> p BVAnd + L.Symbol "bvor" -> p BVOr + _ -> Nothing + where + p :: SMTBVBinOp -> Maybe FunctionParser' + p op = Just $ OverloadedParser allEqConstraint (Just . head) $ + \_ sort_ret f -> case sort_ret of + Fix (BVSort i False) + -> reifyNat i (\(_::Proxy n) + -> Just $ f (SMTBVBin op::SMTFunction (SMTExpr (BitVector (BVTyped n)), + SMTExpr (BitVector (BVTyped n))) + (BitVector (BVTyped n)))) + Fix (BVSort _ True) + -> Just $ f (SMTBVBin op::SMTFunction (SMTExpr (BitVector BVUntyped), + SMTExpr (BitVector BVUntyped)) + (BitVector BVUntyped)) + _ -> Nothing + +bvUnOpParser = FunctionParser $ \sym _ _ -> case sym of + L.Symbol "bvnot" + -> Just $ OverloadedParser (const True) (Just . head) $ + \_ sort_ret f -> case sort_ret of + Fix (BVSort i False) + -> reifyNat i $ \(_::Proxy n) + -> Just $ f (SMTBVUn BVNot::SMTFunction (SMTExpr (BitVector (BVTyped n))) + (BitVector (BVTyped n))) + Fix (BVSort _ True) -> Just $ f (SMTBVUn BVNot::SMTFunction (SMTExpr (BitVector BVUntyped)) + (BitVector BVUntyped)) + _ -> Nothing + L.Symbol "bvneg" + -> Just $ OverloadedParser (const True) (Just . head) $ + \_ sort_ret f -> case sort_ret of + Fix (BVSort i False) + -> reifyNat i $ \(_::Proxy n) + -> Just $ f (SMTBVUn BVNeg::SMTFunction (SMTExpr (BitVector (BVTyped n))) + (BitVector (BVTyped n))) + Fix (BVSort _ True) -> Just $ f (SMTBVUn BVNeg::SMTFunction (SMTExpr (BitVector BVUntyped)) + (BitVector BVUntyped)) + _ -> Nothing + _ -> Nothing + +selectParser = FunctionParser $ \sym _ dts -> case sym of + L.Symbol "select" + -> Just $ OverloadedParser (const True) + (\sort_arg -> case sort_arg of + (Fix (ArraySort _ vsort):_) -> Just vsort + _ -> error "smtlib2: Wrong arguments for select function.") $ + \sort_arg sort_ret f -> case sort_arg of + (Fix (ArraySort isort1 _):_) + -> withSorts dts isort1 $ + \(_::i) _ -> withSort dts sort_ret $ + \(_::v) _ -> Just $ f (SMTSelect::SMTFunction (SMTExpr (SMTArray i v),i) v) + _ -> error "smtlib2: Wrong arguments for select function." + _ -> Nothing + +storeParser = FunctionParser $ \sym _ dts -> case sym of + L.Symbol "store" + -> Just $ OverloadedParser (\tps -> case tps of + (Fix (ArraySort idx res)):tps' -> checkArraySort idx res tps' + _ -> False) + (\sort_arg -> case sort_arg of + s:_ -> Just s + _ -> error "smtlib2: Wrong arguments for store function.") $ + \_ sort_ret f -> case sort_ret of + Fix (ArraySort idx val) + -> withArraySort dts idx val $ + \(_::SMTArray i v) _ + -> Just $ f (SMTStore::SMTFunction (SMTExpr (SMTArray i v),i,SMTExpr v) (SMTArray i v)) + _ -> error "smtlib2: Wrong return type for store function." + _ -> Nothing + where + checkArraySort [] cont [tp] = cont==tp + checkArraySort (arg:args) cont (tp:tps) = arg==tp && checkArraySort args cont tps + checkArraySort _ _ _ = False + +constArrayParser = FunctionParser g + where + g (L.List [L.Symbol "as" + ,L.Symbol "const" + ,s]) _ dts + = case lispToSort s of + Just rsort@(Fix (ArraySort idx val)) + -> Just $ DefinedParser [val] rsort $ + \f -> withArraySort dts idx val $ + \(_::SMTArray i v) (i_ann,_) + -> Just $ f (SMTConstArray i_ann::SMTFunction (SMTExpr v) (SMTArray i v)) + _ -> Nothing + g _ _ _ = Nothing + +concatParser = nameParser (L.Symbol "concat") + (OverloadedParser (const True) + (\args' -> let lenSum = sum $ fmap (\(Fix (BVSort i _)) -> i) args' + untypedRes = any (\(Fix (BVSort _ isUntyped)) -> isUntyped) args' + in Just $ Fix $ BVSort lenSum untypedRes) + (\sort_arg _ f -> case sort_arg of + [Fix (BVSort i1 False),Fix (BVSort i2 False)] + -> reifySum i1 i2 $ + \(_::Proxy n1) (_::Proxy n2) _ + -> Just $ f (SMTConcat::SMTFunction (SMTExpr (BitVector (BVTyped n1)), + SMTExpr (BitVector (BVTyped n2))) + (BitVector (ConcatResult (BVTyped n1) (BVTyped n2)))) + [Fix (BVSort _ True),Fix (BVSort i2 False)] + -> reifyNat i2 $ + \(_::Proxy n2) + -> Just $ f (SMTConcat::SMTFunction (SMTExpr (BitVector BVUntyped), + SMTExpr (BitVector (BVTyped n2))) + (BitVector BVUntyped)) + [Fix (BVSort i1 False),Fix (BVSort _ True)] + -> reifyNat i1 $ + \(_::Proxy n1) + -> Just $ f (SMTConcat::SMTFunction (SMTExpr (BitVector (BVTyped n1)), + SMTExpr (BitVector BVUntyped)) + (BitVector BVUntyped)) + [Fix (BVSort _ True),Fix (BVSort _ True)] + -> Just $ f (SMTConcat::SMTFunction (SMTExpr (BitVector BVUntyped),SMTExpr (BitVector BVUntyped)) (BitVector BVUntyped)) + _ -> Nothing)) + +extractParser = FunctionParser g + where + g (L.List [L.Symbol "_" + ,L.Symbol "extract" + ,L.Number (L.I u) + ,L.Number (L.I l)]) _ _ + = Just $ OverloadedParser (const True) + (\args' -> case args' of + [Fix (BVSort t untyped)] -> if u < t && l >= 0 && l <= u + then Just $ Fix (BVSort (u-l+1) untyped) + else error "smtlib2: Invalid parameters for extract." + _ -> error "smtlib2: Invalid parameters for extract.") + (\sort_arg sort_ret f -> case sort_arg of + [Fix (BVSort t untA)] -> case sort_ret of + Fix (BVSort r untR) + -> if r+l == u+1 && (untR == untA) + then reifyNat l $ + \(_::Proxy start) + -> reifyNat (u-l+1) $ + \(_::Proxy len) + -> if not untR + then reifyNat t $ + \(_::Proxy tp) + -> Just $ f (SMTExtract (Proxy::Proxy start) (Proxy::Proxy len) + ::SMTFunction (SMTExpr (BitVector (BVTyped tp))) + (BitVector (BVTyped len))) + else Just $ f (SMTExtract (Proxy::Proxy start) (Proxy::Proxy len) + ::SMTFunction (SMTExpr (BitVector BVUntyped)) + (BitVector (BVTyped len))) + else error "smtlib2: Invalid parameters for extract." + _ -> error "smtlib2: Wrong return type for extract." + _ -> error "smtlib2: Wrong argument type for extract.") + g _ _ _ = Nothing + +sigParser = FunctionParser g + where + g (L.List [fsym,L.List sig,ret]) r dts = do + rsig <- mapM lispToSort sig + rret <- lispToSort ret + parser <- parseFun r fsym r dts + return $ DefinedParser rsig rret $ + \f -> case parser of + OverloadedParser _ _ parse -> parse rsig rret f + DefinedParser _ _ parse -> parse f + g _ _ _ = Nothing + +divisibleParser = FunctionParser g + where + g (L.List [L.Symbol "_",L.Symbol "divisible",L.Number (L.I n)]) _ _ + = Just $ DefinedParser { definedArgSig = [Fix IntSort] + , definedRetSig = Fix BoolSort + , parseDefined = \f -> Just $ f (SMTDivisible n) } + g _ _ _ = Nothing + +constructorParser :: FunctionParser +constructorParser + = FunctionParser $ + \sym _ dts -> case sym of + L.Symbol name -> case Map.lookup (T.unpack name) (constructors dts) of + Nothing -> Nothing + Just (con,dt,struc) -> case argCount struc of + 0 -> let argSorts = [ runIdentity $ + argumentSortToSort + (error $ "smtlib2: Internal error: Constructor "++conName con + ++" of data type "++dataTypeName dt + ++" is declared as having no arguments, but it uses them") + (fieldSort field) + | field <- conFields con ] + resSort = Fix $ NamedSort (dataTypeName dt) [] + in Just $ DefinedParser { definedArgSig = argSorts + , definedRetSig = resSort + , parseDefined = \f -> withSort dts resSort + (\(uret::ret) ann_ret + -> withSorts dts argSorts + (\(_::arg) ann + -> Just $ f (SMTConstructor (Constructor (getProxyArgs uret ann_ret) dt con::Constructor arg ret)))) + } + _ -> Just $ OverloadedParser { sortConstraint = \_ -> True + , deriveRetSort = infer + , parseOverloaded = parse + } + where + infer tps = let inf = foldl (\cinf (x,y) -> inferSorts x y cinf) + Map.empty (zip (fmap fieldSort (conFields con)) tps) + in argumentSortToSort (\i -> Map.lookup i inf) + (Fix $ NormalSort (NamedSort (dataTypeName dt) + [Fix $ ArgumentSort i + | i <- [0..(argCount struc)-1]])) + parse :: [Sort] -> Sort + -> (forall arg res. + (Liftable arg,SMTType res) + => SMTFunction arg res -> a) -> Maybe a + parse tps rtp app + = withSorts dts tps $ + \(_::arg') _ + -> withSort dts rtp $ + \(_::res') _ + -> Just $ app (SMTConstructor + (Constructor proxies dt con + ::Constructor arg' res')) + where + proxies = case rtp of + Fix (NamedSort _ tps) -> fmap (\tp -> withSort dts tp ProxyArg) tps + _ -> Nothing + +fieldParser :: FunctionParser +fieldParser + = FunctionParser $ + \sym _ dts -> case sym of + L.Symbol name -> case Map.lookup (T.unpack name) (fields dts) of + Nothing -> Nothing + Just (field,constr,dt,struc) + -> Just $ OverloadedParser { sortConstraint = \_ -> True + , deriveRetSort = infer + , parseOverloaded = parse } + where + infer [Fix (NamedSort _ tps)] + = let mp = Map.fromList (zip [0..] tps) + in argumentSortToSort (\i -> Map.lookup i mp) (fieldSort field) + parse :: [Sort] -> Sort + -> (forall arg res. + (Liftable arg,SMTType res) + => SMTFunction arg res -> a) -> Maybe a + parse [Fix (NamedSort _ tps)] rtp app + = dataTypeGetUndefined dt proxies $ + \(u::t) _ -> withSort dts rtp $ + \(_::f) _ + -> Just $ app (SMTFieldSel + (Field proxies dt constr field + :: Field t f)) + where + proxies = fmap (\tp -> withSort dts tp ProxyArg) tps + _ -> Nothing + +withPipe :: MonadIO m => String -> [String] -> SMT' m a -> m a +withPipe prog args act = do + pipe <- liftIO $ createSMTPipe prog args + withSMTBackend pipe act + +tacticToLisp :: Tactic -> L.Lisp +tacticToLisp Skip = L.Symbol "skip" +tacticToLisp (AndThen ts) = L.List ((L.Symbol "and-then"):fmap tacticToLisp ts) +tacticToLisp (OrElse ts) = L.List ((L.Symbol "or-else"):fmap tacticToLisp ts) +tacticToLisp (ParOr ts) = L.List ((L.Symbol "par-or"):fmap tacticToLisp ts) +tacticToLisp (ParThen t1 t2) = L.List [L.Symbol "par-then" + ,tacticToLisp t1 + ,tacticToLisp t2] +tacticToLisp (TryFor t n) = L.List [L.Symbol "try-for" + ,tacticToLisp t + ,L.Number $ L.I n] +tacticToLisp (If c t1 t2) = L.List [L.Symbol "if" + ,probeToLisp c + ,tacticToLisp t1 + ,tacticToLisp t2] +tacticToLisp (FailIf c) = L.List [L.Symbol "fail-if" + ,probeToLisp c] +tacticToLisp (UsingParams (CustomTactic name) []) = L.Symbol (T.pack name) +tacticToLisp (UsingParams (CustomTactic name) pars) + = L.List ([L.Symbol "using-params" + ,L.Symbol $ T.pack name]++ + concat [ [L.Symbol (T.pack $ ':':pname) + ,case par of + ParBool True -> L.Symbol "true" + ParBool False -> L.Symbol "false" + ParInt i -> L.Number $ L.I i + ParDouble i -> L.Number $ L.D i] + | (pname,par) <- pars ]) + +probeToLisp :: Probe a -> L.Lisp +probeToLisp (ProbeBoolConst b) + = L.Symbol $ if b then "true" else "false" +probeToLisp (ProbeIntConst i) + = L.Number $ L.I i +probeToLisp (ProbeAnd ps) + = L.List ((L.Symbol "and"): + fmap probeToLisp ps) +probeToLisp (ProbeOr ps) + = L.List ((L.Symbol "or"): + fmap probeToLisp ps) +probeToLisp (ProbeNot p) + = L.List [L.Symbol "not" + ,probeToLisp p] +probeToLisp (ProbeEq p1 p2) + = L.List [L.Symbol "=" + ,probeToLisp p1 + ,probeToLisp p2] +probeToLisp (ProbeCompare cmp p1 p2) + = L.List [L.Symbol $ case cmp of + Ge -> ">=" + Gt -> ">" + Le -> "<=" + Lt -> "<" + ,probeToLisp p1 + ,probeToLisp p2] +probeToLisp IsPB = L.Symbol "is-pb" +probeToLisp ArithMaxDeg = L.Symbol "arith-max-deg" +probeToLisp ArithAvgDeg = L.Symbol "arith-avg-deg" +probeToLisp ArithMaxBW = L.Symbol "arith-max-bw" +probeToLisp ArithAvgBW = L.Symbol "arith-avg-bw" +probeToLisp IsQFLIA = L.Symbol "is-qflia" +probeToLisp IsQFLRA = L.Symbol "is-qflra" +probeToLisp IsQFLIRA = L.Symbol "is-qflira" +probeToLisp IsILP = L.Symbol "is-ilp" +probeToLisp IsQFNIA = L.Symbol "is-qfnia" +probeToLisp IsQFNRA = L.Symbol "is-qfnra" +probeToLisp IsNIA = L.Symbol "is-nia" +probeToLisp IsNRA = L.Symbol "is-nra" +probeToLisp IsUnbounded = L.Symbol "is-unbounded" +probeToLisp Memory = L.Symbol "memory" +probeToLisp Depth = L.Symbol "depth" +probeToLisp Size = L.Symbol "size" +probeToLisp NumExprs = L.Symbol "num-exprs" +probeToLisp NumConsts = L.Symbol "num-consts" +probeToLisp NumBoolConsts = L.Symbol "num-bool-consts" +probeToLisp NumArithConsts = L.Symbol "num-arith-consts" +probeToLisp NumBVConsts = L.Symbol "num-bv-consts" +probeToLisp Strat.ProduceProofs = L.Symbol "produce-proofs" +probeToLisp ProduceModel = L.Symbol "produce-model" +probeToLisp Strat.ProduceUnsatCores = L.Symbol "produce-unsat-cores" +probeToLisp HasPatterns = L.Symbol "has-patterns" +probeToLisp IsPropositional = L.Symbol "is-propositional" +probeToLisp IsQFBV = L.Symbol "is-qfbv" +probeToLisp IsQFBVEQ = L.Symbol "is-qfbv-eq" + diff --git a/Language/SMTLib2/Solver.hs b/Language/SMTLib2/Solver.hs new file mode 100644 --- /dev/null +++ b/Language/SMTLib2/Solver.hs @@ -0,0 +1,23 @@ +{- | Gives interfaces to some common SMT solvers. + -} +module Language.SMTLib2.Solver where + +import Language.SMTLib2 +import Language.SMTLib2.Pipe +import Control.Monad.Trans (MonadIO) + +-- | Z3 is a solver by Microsoft . +withZ3 :: MonadIO m => SMT' m a -> m a +withZ3 = withPipe "z3" ["-smt2","-in"] + +-- | MathSAT . +withMathSat :: MonadIO m => SMT' m a -> m a +withMathSat = withPipe "mathsat" [] + +-- | CVC4 is an open-source SMT solver +withCVC4 :: MonadIO m => SMT' m a -> m a +withCVC4 = withPipe "cvc4" ["--lang smt2"] + +-- | SMTInterpol is an experimental interpolating SMT solver +withSMTInterpol :: MonadIO m => SMT' m a -> m a +withSMTInterpol = withPipe "java" ["-jar","/usr/local/share/java/smtinterpol.jar","-q"] diff --git a/Language/SMTLib2/Strategy.hs b/Language/SMTLib2/Strategy.hs new file mode 100644 --- /dev/null +++ b/Language/SMTLib2/Strategy.hs @@ -0,0 +1,146 @@ +module Language.SMTLib2.Strategy where + +import Language.SMTLib2.Internals.Operators + +import Text.Show + +data Tactic + = Skip + | AndThen [Tactic] + | OrElse [Tactic] + | ParOr [Tactic] + | ParThen Tactic Tactic + | TryFor Tactic Integer + | If (Probe Bool) Tactic Tactic + | FailIf (Probe Bool) + | forall p. Show p => UsingParams (BuiltInTactic p) [p] + +data Probe a where + ProbeBoolConst :: Bool -> Probe Bool + ProbeIntConst :: Integer -> Probe Integer + ProbeAnd :: [Probe Bool] -> Probe Bool + ProbeOr :: [Probe Bool] -> Probe Bool + ProbeNot :: Probe Bool -> Probe Bool + ProbeEq :: Show a => Probe a -> Probe a -> Probe Bool + ProbeCompare :: SMTOrdOp -> Probe Integer -> Probe Integer -> Probe Bool + IsPB :: Probe Bool + ArithMaxDeg :: Probe Integer + ArithAvgDeg :: Probe Integer + ArithMaxBW :: Probe Integer + ArithAvgBW :: Probe Integer + IsQFLIA :: Probe Bool + IsQFLRA :: Probe Bool + IsQFLIRA :: Probe Bool + IsILP :: Probe Bool + IsQFNIA :: Probe Bool + IsQFNRA :: Probe Bool + IsNIA :: Probe Bool + IsNRA :: Probe Bool + IsUnbounded :: Probe Bool + Memory :: Probe Integer + Depth :: Probe Integer + Size :: Probe Integer + NumExprs :: Probe Integer + NumConsts :: Probe Integer + NumBoolConsts :: Probe Integer + NumArithConsts :: Probe Integer + NumBVConsts :: Probe Integer + ProduceProofs :: Probe Bool + ProduceModel :: Probe Bool + ProduceUnsatCores :: Probe Bool + HasPatterns :: Probe Bool + IsPropositional :: Probe Bool + IsQFBV :: Probe Bool + IsQFBVEQ :: Probe Bool + +data AnyPar = ParBool Bool + | ParInt Integer + | ParDouble Double + deriving Show + +data BuiltInTactic p where + QFLRATactic :: BuiltInTactic QFLRATacticP + CustomTactic :: String -> BuiltInTactic (String,AnyPar) + +data QFLRATacticP + = ArithBranchCutRatio Integer + deriving Show + +instance Show Tactic where + showsPrec _ Skip = showString "Skip" + showsPrec p (AndThen ts) = showParen (p>10) (showString "AndThen " . + showsPrec 0 ts) + showsPrec p (OrElse ts) = showParen (p>10) (showString "OrElse " . + showsPrec 0 ts) + showsPrec p (ParOr ts) = showParen (p>10) (showString "ParOr " . + showsPrec 0 ts) + showsPrec p (ParThen t1 t2) = showParen (p>10) (showString "ParThen " . + showsPrec 11 t1 . + showChar ' ' . + showsPrec 11 t2) + showsPrec p (TryFor t n) = showParen (p>10) (showString "TryFor " . + showsPrec 11 t . + showChar ' ' . + showsPrec 11 n) + showsPrec p (If c t1 t2) = showParen (p>10) (showString "If " . + showsPrec 11 c . + showChar ' ' . + showsPrec 11 t1 . + showChar ' ' . + showsPrec 11 t2) + showsPrec p (FailIf c) = showParen (p>10) (showString "FailIf " . + showsPrec 11 c) + showsPrec p (UsingParams t []) = showsPrec p t + showsPrec p (UsingParams t pars) = showParen (p>10) (showString "UsingParams " . + showsPrec 11 t . + showChar ' ' . + showsPrec 11 pars) + +instance Show (BuiltInTactic p) where + showsPrec _ QFLRATactic = showString "QFLRATactic" + showsPrec _ (CustomTactic name) = showString name + +instance Show a => Show (Probe a) where + showsPrec p (ProbeBoolConst c) = showParen (p>10) (showString "ProbeBoolConst " . + showsPrec 11 c) + showsPrec p (ProbeIntConst c) = showParen (p>10) (showString "ProbeIntConst " . + showsPrec 11 c) + showsPrec p (ProbeAnd ps) = showParen (p>10) (showString "ProbeAnd " . + showsPrec 11 ps) + showsPrec p (ProbeOr ps) = showParen (p>10) (showString "ProbeOr " . + showsPrec 11 ps) + showsPrec p (ProbeNot c) = showParen (p>10) (showString "ProbeNot " . + showsPrec 11 c) + showsPrec p (ProbeEq p1 p2) = showParen (p>10) (showString "ProbeEq " . + showsPrec 11 p1 . + showChar ' ' . + showsPrec 11 p2) + showsPrec _ IsPB = showString "IsPB" + showsPrec _ ArithMaxDeg = showString "ArithMaxDeg" + showsPrec _ ArithAvgDeg = showString "ArithAvgDeg" + showsPrec _ ArithMaxBW = showString "ArithMaxBW" + showsPrec _ ArithAvgBW = showString "ArithAvgBW" + showsPrec _ IsQFLIA = showString "IsQFLIA" + showsPrec _ IsQFLRA = showString "IsQFLRA" + showsPrec _ IsQFLIRA = showString "IsQFLIRA" + showsPrec _ IsILP = showString "IsILP" + showsPrec _ IsQFNIA = showString "IsQFNIA" + showsPrec _ IsQFNRA = showString "IsQFNRA" + showsPrec _ IsNIA = showString "IsNIA" + showsPrec _ IsNRA = showString "IsNRA" + showsPrec _ IsUnbounded = showString "IsUnbounded" + showsPrec _ Memory = showString "Memory" + showsPrec _ Depth = showString "Depth" + showsPrec _ Size = showString "Size" + showsPrec _ NumExprs = showString "NumExprs" + showsPrec _ NumConsts = showString "NumConsts" + showsPrec _ NumBoolConsts = showString "NumBoolConsts" + showsPrec _ NumArithConsts = showString "NumArithConsts" + showsPrec _ NumBVConsts = showString "NumBVConsts" + showsPrec _ ProduceProofs = showString "ProduceProofs" + showsPrec _ ProduceModel = showString "ProduceModel" + showsPrec _ ProduceUnsatCores = showString "ProduceUnsatCores" + showsPrec _ HasPatterns = showString "HasPatterns" + showsPrec _ IsPropositional = showString "IsPropositional" + showsPrec _ IsQFBV = showString "IsQFBV" + showsPrec _ IsQFBVEQ = showString "IsQFBVEQ" diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/smtlib2.cabal b/smtlib2.cabal new file mode 100644 --- /dev/null +++ b/smtlib2.cabal @@ -0,0 +1,51 @@ +Name: smtlib2 +Version: 0.1 +Author: Henning Günther +Maintainer: guenther@forsyte.at +Synopsis: A type-safe interface to communicate with an SMT solver. +Stability: provisional +Category: SMT, Formal Methods, Theorem Provers, Symbolic Computation +License: GPL-3 +License-File: LICENSE +Build-Type: Simple +Cabal-Version: >=1.6 + +Source-Repository head + Type: git + Location: https://github.com/hguenther/smtlib2.git + +Flag WithConstraints + Description: Enables the use of the constraint-kind extension which is needed to parse 'map'-expressions. + Default: True +Flag WithDataKinds + Description: Enables the use of the data-kinds extension which is needed for typed bitvectors. + Default: False + +Library + Build-Depends: base >= 4 && < 5,text,mtl,process,blaze-builder,bytestring, + attoparsec,atto-lisp >= 0.2,array, + containers, transformers, data-fix, tagged + Extensions: GADTs,RankNTypes,CPP,ScopedTypeVariables, + MultiParamTypeClasses,FlexibleContexts,OverloadedStrings, + DeriveFunctor,FlexibleInstances,DeriveTraversable,DeriveFoldable, + DeriveDataTypeable + if flag(WithConstraints) + Build-Depends: constraints + CPP-Options: -DSMTLIB2_WITH_CONSTRAINTS + if flag(WithDataKinds) + Extensions: DataKinds,PolyKinds + CPP-Options: -DSMTLIB2_WITH_DATAKINDS + + GHC-Options: -fwarn-unused-imports + Exposed-Modules: + Language.SMTLib2 + Language.SMTLib2.Solver + Language.SMTLib2.Connection + Language.SMTLib2.Internals + Language.SMTLib2.Internals.Instances + Language.SMTLib2.Internals.Interface + Language.SMTLib2.Internals.Optimize + Language.SMTLib2.Internals.Operators + Language.SMTLib2.Pipe + Language.SMTLib2.Strategy + Data.Unit