smtlib2 (empty) → 0.1
raw patch · 14 files changed
+6603/−0 lines, 14 filesdep +arraydep +atto-lispdep +attoparsecsetup-changed
Dependencies added: array, atto-lisp, attoparsec, base, blaze-builder, bytestring, constraints, containers, data-fix, mtl, process, tagged, text, transformers
Files
- Data/Unit.hs +29/−0
- LICENSE +674/−0
- Language/SMTLib2.hs +116/−0
- Language/SMTLib2/Connection.hs +70/−0
- Language/SMTLib2/Internals.hs +1167/−0
- Language/SMTLib2/Internals/Instances.hs +1639/−0
- Language/SMTLib2/Internals/Interface.hs +710/−0
- Language/SMTLib2/Internals/Operators.hs +58/−0
- Language/SMTLib2/Internals/Optimize.hs +240/−0
- Language/SMTLib2/Pipe.hs +1678/−0
- Language/SMTLib2/Solver.hs +23/−0
- Language/SMTLib2/Strategy.hs +146/−0
- Setup.hs +2/−0
- smtlib2.cabal +51/−0
+ Data/Unit.hs view
@@ -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)
+ LICENSE view
@@ -0,0 +1,674 @@+ GNU GENERAL PUBLIC LICENSE+ Version 3, 29 June 2007++ Copyright (C) 2007 Free Software Foundation, Inc. <http://fsf.org/>+ Everyone is permitted to copy and distribute verbatim copies+ of this license document, but changing it is not allowed.++ Preamble++ The GNU General Public License is a free, copyleft license for+software and other kinds of works.++ The licenses for most software and other practical works are designed+to take away your freedom to share and change the works. By contrast,+the GNU General Public License is intended to guarantee your freedom to+share and change all versions of a program--to make sure it remains free+software for all its users. We, the Free Software Foundation, use the+GNU General Public License for most of our software; it applies also to+any other work released this way by its authors. You can apply it to+your programs, too.++ When we speak of free software, we are referring to freedom, not+price. Our General Public Licenses are designed to make sure that you+have the freedom to distribute copies of free software (and charge for+them if you wish), that you receive source code or can get it if you+want it, that you can change the software or use pieces of it in new+free programs, and that you know you can do these things.++ To protect your rights, we need to prevent others from denying you+these rights or asking you to surrender the rights. Therefore, you have+certain responsibilities if you distribute copies of the software, or if+you modify it: responsibilities to respect the freedom of others.++ For example, if you distribute copies of such a program, whether+gratis or for a fee, you must pass on to the recipients the same+freedoms that you received. You must make sure that they, too, receive+or can get the source code. And you must show them these terms so they+know their rights.++ Developers that use the GNU GPL protect your rights with two steps:+(1) assert copyright on the software, and (2) offer you this License+giving you legal permission to copy, distribute and/or modify it.++ For the developers' and authors' protection, the GPL clearly explains+that there is no warranty for this free software. For both users' and+authors' sake, the GPL requires that modified versions be marked as+changed, so that their problems will not be attributed erroneously to+authors of previous versions.++ Some devices are designed to deny users access to install or run+modified versions of the software inside them, although the manufacturer+can do so. This is fundamentally incompatible with the aim of+protecting users' freedom to change the software. The systematic+pattern of such abuse occurs in the area of products for individuals to+use, which is precisely where it is most unacceptable. Therefore, we+have designed this version of the GPL to prohibit the practice for those+products. If such problems arise substantially in other domains, we+stand ready to extend this provision to those domains in future versions+of the GPL, as needed to protect the freedom of users.++ Finally, every program is threatened constantly by software patents.+States should not allow patents to restrict development and use of+software on general-purpose computers, but in those that do, we wish to+avoid the special danger that patents applied to a free program could+make it effectively proprietary. To prevent this, the GPL assures that+patents cannot be used to render the program non-free.++ The precise terms and conditions for copying, distribution and+modification follow.++ TERMS AND CONDITIONS++ 0. Definitions.++ "This License" refers to version 3 of the GNU General Public License.++ "Copyright" also means copyright-like laws that apply to other kinds of+works, such as semiconductor masks.++ "The Program" refers to any copyrightable work licensed under this+License. Each licensee is addressed as "you". "Licensees" and+"recipients" may be individuals or organizations.++ To "modify" a work means to copy from or adapt all or part of the work+in a fashion requiring copyright permission, other than the making of an+exact copy. The resulting work is called a "modified version" of the+earlier work or a work "based on" the earlier work.++ A "covered work" means either the unmodified Program or a work based+on the Program.++ To "propagate" a work means to do anything with it that, without+permission, would make you directly or secondarily liable for+infringement under applicable copyright law, except executing it on a+computer or modifying a private copy. Propagation includes copying,+distribution (with or without modification), making available to the+public, and in some countries other activities as well.++ To "convey" a work means any kind of propagation that enables other+parties to make or receive copies. Mere interaction with a user through+a computer network, with no transfer of a copy, is not conveying.++ An interactive user interface displays "Appropriate Legal Notices"+to the extent that it includes a convenient and prominently visible+feature that (1) displays an appropriate copyright notice, and (2)+tells the user that there is no warranty for the work (except to the+extent that warranties are provided), that licensees may convey the+work under this License, and how to view a copy of this License. If+the interface presents a list of user commands or options, such as a+menu, a prominent item in the list meets this criterion.++ 1. Source Code.++ The "source code" for a work means the preferred form of the work+for making modifications to it. "Object code" means any non-source+form of a work.++ A "Standard Interface" means an interface that either is an official+standard defined by a recognized standards body, or, in the case of+interfaces specified for a particular programming language, one that+is widely used among developers working in that language.++ The "System Libraries" of an executable work include anything, other+than the work as a whole, that (a) is included in the normal form of+packaging a Major Component, but which is not part of that Major+Component, and (b) serves only to enable use of the work with that+Major Component, or to implement a Standard Interface for which an+implementation is available to the public in source code form. A+"Major Component", in this context, means a major essential component+(kernel, window system, and so on) of the specific operating system+(if any) on which the executable work runs, or a compiler used to+produce the work, or an object code interpreter used to run it.++ The "Corresponding Source" for a work in object code form means all+the source code needed to generate, install, and (for an executable+work) run the object code and to modify the work, including scripts to+control those activities. However, it does not include the work's+System Libraries, or general-purpose tools or generally available free+programs which are used unmodified in performing those activities but+which are not part of the work. For example, Corresponding Source+includes interface definition files associated with source files for+the work, and the source code for shared libraries and dynamically+linked subprograms that the work is specifically designed to require,+such as by intimate data communication or control flow between those+subprograms and other parts of the work.++ The Corresponding Source need not include anything that users+can regenerate automatically from other parts of the Corresponding+Source.++ The Corresponding Source for a work in source code form is that+same work.++ 2. Basic Permissions.++ All rights granted under this License are granted for the term of+copyright on the Program, and are irrevocable provided the stated+conditions are met. This License explicitly affirms your unlimited+permission to run the unmodified Program. The output from running a+covered work is covered by this License only if the output, given its+content, constitutes a covered work. This License acknowledges your+rights of fair use or other equivalent, as provided by copyright law.++ You may make, run and propagate covered works that you do not+convey, without conditions so long as your license otherwise remains+in force. You may convey covered works to others for the sole purpose+of having them make modifications exclusively for you, or provide you+with facilities for running those works, provided that you comply with+the terms of this License in conveying all material for which you do+not control copyright. Those thus making or running the covered works+for you must do so exclusively on your behalf, under your direction+and control, on terms that prohibit them from making any copies of+your copyrighted material outside their relationship with you.++ Conveying under any other circumstances is permitted solely under+the conditions stated below. Sublicensing is not allowed; section 10+makes it unnecessary.++ 3. Protecting Users' Legal Rights From Anti-Circumvention Law.++ No covered work shall be deemed part of an effective technological+measure under any applicable law fulfilling obligations under article+11 of the WIPO copyright treaty adopted on 20 December 1996, or+similar laws prohibiting or restricting circumvention of such+measures.++ When you convey a covered work, you waive any legal power to forbid+circumvention of technological measures to the extent such circumvention+is effected by exercising rights under this License with respect to+the covered work, and you disclaim any intention to limit operation or+modification of the work as a means of enforcing, against the work's+users, your or third parties' legal rights to forbid circumvention of+technological measures.++ 4. Conveying Verbatim Copies.++ You may convey verbatim copies of the Program's source code as you+receive it, in any medium, provided that you conspicuously and+appropriately publish on each copy an appropriate copyright notice;+keep intact all notices stating that this License and any+non-permissive terms added in accord with section 7 apply to the code;+keep intact all notices of the absence of any warranty; and give all+recipients a copy of this License along with the Program.++ You may charge any price or no price for each copy that you convey,+and you may offer support or warranty protection for a fee.++ 5. Conveying Modified Source Versions.++ You may convey a work based on the Program, or the modifications to+produce it from the Program, in the form of source code under the+terms of section 4, provided that you also meet all of these conditions:++ a) The work must carry prominent notices stating that you modified+ it, and giving a relevant date.++ b) The work must carry prominent notices stating that it is+ released under this License and any conditions added under section+ 7. This requirement modifies the requirement in section 4 to+ "keep intact all notices".++ c) You must license the entire work, as a whole, under this+ License to anyone who comes into possession of a copy. This+ License will therefore apply, along with any applicable section 7+ additional terms, to the whole of the work, and all its parts,+ regardless of how they are packaged. This License gives no+ permission to license the work in any other way, but it does not+ invalidate such permission if you have separately received it.++ d) If the work has interactive user interfaces, each must display+ Appropriate Legal Notices; however, if the Program has interactive+ interfaces that do not display Appropriate Legal Notices, your+ work need not make them do so.++ A compilation of a covered work with other separate and independent+works, which are not by their nature extensions of the covered work,+and which are not combined with it such as to form a larger program,+in or on a volume of a storage or distribution medium, is called an+"aggregate" if the compilation and its resulting copyright are not+used to limit the access or legal rights of the compilation's users+beyond what the individual works permit. Inclusion of a covered work+in an aggregate does not cause this License to apply to the other+parts of the aggregate.++ 6. Conveying Non-Source Forms.++ You may convey a covered work in object code form under the terms+of sections 4 and 5, provided that you also convey the+machine-readable Corresponding Source under the terms of this License,+in one of these ways:++ a) Convey the object code in, or embodied in, a physical product+ (including a physical distribution medium), accompanied by the+ Corresponding Source fixed on a durable physical medium+ customarily used for software interchange.++ b) Convey the object code in, or embodied in, a physical product+ (including a physical distribution medium), accompanied by a+ written offer, valid for at least three years and valid for as+ long as you offer spare parts or customer support for that product+ model, to give anyone who possesses the object code either (1) a+ copy of the Corresponding Source for all the software in the+ product that is covered by this License, on a durable physical+ medium customarily used for software interchange, for a price no+ more than your reasonable cost of physically performing this+ conveying of source, or (2) access to copy the+ Corresponding Source from a network server at no charge.++ c) Convey individual copies of the object code with a copy of the+ written offer to provide the Corresponding Source. This+ alternative is allowed only occasionally and noncommercially, and+ only if you received the object code with such an offer, in accord+ with subsection 6b.++ d) Convey the object code by offering access from a designated+ place (gratis or for a charge), and offer equivalent access to the+ Corresponding Source in the same way through the same place at no+ further charge. You need not require recipients to copy the+ Corresponding Source along with the object code. If the place to+ copy the object code is a network server, the Corresponding Source+ may be on a different server (operated by you or a third party)+ that supports equivalent copying facilities, provided you maintain+ clear directions next to the object code saying where to find the+ Corresponding Source. Regardless of what server hosts the+ Corresponding Source, you remain obligated to ensure that it is+ available for as long as needed to satisfy these requirements.++ e) Convey the object code using peer-to-peer transmission, provided+ you inform other peers where the object code and Corresponding+ Source of the work are being offered to the general public at no+ charge under subsection 6d.++ A separable portion of the object code, whose source code is excluded+from the Corresponding Source as a System Library, need not be+included in conveying the object code work.++ A "User Product" is either (1) a "consumer product", which means any+tangible personal property which is normally used for personal, family,+or household purposes, or (2) anything designed or sold for incorporation+into a dwelling. In determining whether a product is a consumer product,+doubtful cases shall be resolved in favor of coverage. For a particular+product received by a particular user, "normally used" refers to a+typical or common use of that class of product, regardless of the status+of the particular user or of the way in which the particular user+actually uses, or expects or is expected to use, the product. A product+is a consumer product regardless of whether the product has substantial+commercial, industrial or non-consumer uses, unless such uses represent+the only significant mode of use of the product.++ "Installation Information" for a User Product means any methods,+procedures, authorization keys, or other information required to install+and execute modified versions of a covered work in that User Product from+a modified version of its Corresponding Source. The information must+suffice to ensure that the continued functioning of the modified object+code is in no case prevented or interfered with solely because+modification has been made.++ If you convey an object code work under this section in, or with, or+specifically for use in, a User Product, and the conveying occurs as+part of a transaction in which the right of possession and use of the+User Product is transferred to the recipient in perpetuity or for a+fixed term (regardless of how the transaction is characterized), the+Corresponding Source conveyed under this section must be accompanied+by the Installation Information. But this requirement does not apply+if neither you nor any third party retains the ability to install+modified object code on the User Product (for example, the work has+been installed in ROM).++ The requirement to provide Installation Information does not include a+requirement to continue to provide support service, warranty, or updates+for a work that has been modified or installed by the recipient, or for+the User Product in which it has been modified or installed. Access to a+network may be denied when the modification itself materially and+adversely affects the operation of the network or violates the rules and+protocols for communication across the network.++ Corresponding Source conveyed, and Installation Information provided,+in accord with this section must be in a format that is publicly+documented (and with an implementation available to the public in+source code form), and must require no special password or key for+unpacking, reading or copying.++ 7. Additional Terms.++ "Additional permissions" are terms that supplement the terms of this+License by making exceptions from one or more of its conditions.+Additional permissions that are applicable to the entire Program shall+be treated as though they were included in this License, to the extent+that they are valid under applicable law. If additional permissions+apply only to part of the Program, that part may be used separately+under those permissions, but the entire Program remains governed by+this License without regard to the additional permissions.++ When you convey a copy of a covered work, you may at your option+remove any additional permissions from that copy, or from any part of+it. (Additional permissions may be written to require their own+removal in certain cases when you modify the work.) You may place+additional permissions on material, added by you to a covered work,+for which you have or can give appropriate copyright permission.++ Notwithstanding any other provision of this License, for material you+add to a covered work, you may (if authorized by the copyright holders of+that material) supplement the terms of this License with terms:++ a) Disclaiming warranty or limiting liability differently from the+ terms of sections 15 and 16 of this License; or++ b) Requiring preservation of specified reasonable legal notices or+ author attributions in that material or in the Appropriate Legal+ Notices displayed by works containing it; or++ c) Prohibiting misrepresentation of the origin of that material, or+ requiring that modified versions of such material be marked in+ reasonable ways as different from the original version; or++ d) Limiting the use for publicity purposes of names of licensors or+ authors of the material; or++ e) Declining to grant rights under trademark law for use of some+ trade names, trademarks, or service marks; or++ f) Requiring indemnification of licensors and authors of that+ material by anyone who conveys the material (or modified versions of+ it) with contractual assumptions of liability to the recipient, for+ any liability that these contractual assumptions directly impose on+ those licensors and authors.++ All other non-permissive additional terms are considered "further+restrictions" within the meaning of section 10. If the Program as you+received it, or any part of it, contains a notice stating that it is+governed by this License along with a term that is a further+restriction, you may remove that term. If a license document contains+a further restriction but permits relicensing or conveying under this+License, you may add to a covered work material governed by the terms+of that license document, provided that the further restriction does+not survive such relicensing or conveying.++ If you add terms to a covered work in accord with this section, you+must place, in the relevant source files, a statement of the+additional terms that apply to those files, or a notice indicating+where to find the applicable terms.++ Additional terms, permissive or non-permissive, may be stated in the+form of a separately written license, or stated as exceptions;+the above requirements apply either way.++ 8. Termination.++ You may not propagate or modify a covered work except as expressly+provided under this License. Any attempt otherwise to propagate or+modify it is void, and will automatically terminate your rights under+this License (including any patent licenses granted under the third+paragraph of section 11).++ However, if you cease all violation of this License, then your+license from a particular copyright holder is reinstated (a)+provisionally, unless and until the copyright holder explicitly and+finally terminates your license, and (b) permanently, if the copyright+holder fails to notify you of the violation by some reasonable means+prior to 60 days after the cessation.++ Moreover, your license from a particular copyright holder is+reinstated permanently if the copyright holder notifies you of the+violation by some reasonable means, this is the first time you have+received notice of violation of this License (for any work) from that+copyright holder, and you cure the violation prior to 30 days after+your receipt of the notice.++ Termination of your rights under this section does not terminate the+licenses of parties who have received copies or rights from you under+this License. If your rights have been terminated and not permanently+reinstated, you do not qualify to receive new licenses for the same+material under section 10.++ 9. Acceptance Not Required for Having Copies.++ You are not required to accept this License in order to receive or+run a copy of the Program. Ancillary propagation of a covered work+occurring solely as a consequence of using peer-to-peer transmission+to receive a copy likewise does not require acceptance. However,+nothing other than this License grants you permission to propagate or+modify any covered work. These actions infringe copyright if you do+not accept this License. Therefore, by modifying or propagating a+covered work, you indicate your acceptance of this License to do so.++ 10. Automatic Licensing of Downstream Recipients.++ Each time you convey a covered work, the recipient automatically+receives a license from the original licensors, to run, modify and+propagate that work, subject to this License. You are not responsible+for enforcing compliance by third parties with this License.++ An "entity transaction" is a transaction transferring control of an+organization, or substantially all assets of one, or subdividing an+organization, or merging organizations. If propagation of a covered+work results from an entity transaction, each party to that+transaction who receives a copy of the work also receives whatever+licenses to the work the party's predecessor in interest had or could+give under the previous paragraph, plus a right to possession of the+Corresponding Source of the work from the predecessor in interest, if+the predecessor has it or can get it with reasonable efforts.++ You may not impose any further restrictions on the exercise of the+rights granted or affirmed under this License. For example, you may+not impose a license fee, royalty, or other charge for exercise of+rights granted under this License, and you may not initiate litigation+(including a cross-claim or counterclaim in a lawsuit) alleging that+any patent claim is infringed by making, using, selling, offering for+sale, or importing the Program or any portion of it.++ 11. Patents.++ A "contributor" is a copyright holder who authorizes use under this+License of the Program or a work on which the Program is based. The+work thus licensed is called the contributor's "contributor version".++ A contributor's "essential patent claims" are all patent claims+owned or controlled by the contributor, whether already acquired or+hereafter acquired, that would be infringed by some manner, permitted+by this License, of making, using, or selling its contributor version,+but do not include claims that would be infringed only as a+consequence of further modification of the contributor version. For+purposes of this definition, "control" includes the right to grant+patent sublicenses in a manner consistent with the requirements of+this License.++ Each contributor grants you a non-exclusive, worldwide, royalty-free+patent license under the contributor's essential patent claims, to+make, use, sell, offer for sale, import and otherwise run, modify and+propagate the contents of its contributor version.++ In the following three paragraphs, a "patent license" is any express+agreement or commitment, however denominated, not to enforce a patent+(such as an express permission to practice a patent or covenant not to+sue for patent infringement). To "grant" such a patent license to a+party means to make such an agreement or commitment not to enforce a+patent against the party.++ If you convey a covered work, knowingly relying on a patent license,+and the Corresponding Source of the work is not available for anyone+to copy, free of charge and under the terms of this License, through a+publicly available network server or other readily accessible means,+then you must either (1) cause the Corresponding Source to be so+available, or (2) arrange to deprive yourself of the benefit of the+patent license for this particular work, or (3) arrange, in a manner+consistent with the requirements of this License, to extend the patent+license to downstream recipients. "Knowingly relying" means you have+actual knowledge that, but for the patent license, your conveying the+covered work in a country, or your recipient's use of the covered work+in a country, would infringe one or more identifiable patents in that+country that you have reason to believe are valid.++ If, pursuant to or in connection with a single transaction or+arrangement, you convey, or propagate by procuring conveyance of, a+covered work, and grant a patent license to some of the parties+receiving the covered work authorizing them to use, propagate, modify+or convey a specific copy of the covered work, then the patent license+you grant is automatically extended to all recipients of the covered+work and works based on it.++ A patent license is "discriminatory" if it does not include within+the scope of its coverage, prohibits the exercise of, or is+conditioned on the non-exercise of one or more of the rights that are+specifically granted under this License. You may not convey a covered+work if you are a party to an arrangement with a third party that is+in the business of distributing software, under which you make payment+to the third party based on the extent of your activity of conveying+the work, and under which the third party grants, to any of the+parties who would receive the covered work from you, a discriminatory+patent license (a) in connection with copies of the covered work+conveyed by you (or copies made from those copies), or (b) primarily+for and in connection with specific products or compilations that+contain the covered work, unless you entered into that arrangement,+or that patent license was granted, prior to 28 March 2007.++ Nothing in this License shall be construed as excluding or limiting+any implied license or other defenses to infringement that may+otherwise be available to you under applicable patent law.++ 12. No Surrender of Others' Freedom.++ If conditions are imposed on you (whether by court order, agreement or+otherwise) that contradict the conditions of this License, they do not+excuse you from the conditions of this License. If you cannot convey a+covered work so as to satisfy simultaneously your obligations under this+License and any other pertinent obligations, then as a consequence you may+not convey it at all. For example, if you agree to terms that obligate you+to collect a royalty for further conveying from those to whom you convey+the Program, the only way you could satisfy both those terms and this+License would be to refrain entirely from conveying the Program.++ 13. Use with the GNU Affero General Public License.++ Notwithstanding any other provision of this License, you have+permission to link or combine any covered work with a work licensed+under version 3 of the GNU Affero General Public License into a single+combined work, and to convey the resulting work. The terms of this+License will continue to apply to the part which is the covered work,+but the special requirements of the GNU Affero General Public License,+section 13, concerning interaction through a network will apply to the+combination as such.++ 14. Revised Versions of this License.++ The Free Software Foundation may publish revised and/or new versions of+the GNU General Public License from time to time. Such new versions will+be similar in spirit to the present version, but may differ in detail to+address new problems or concerns.++ Each version is given a distinguishing version number. If the+Program specifies that a certain numbered version of the GNU General+Public License "or any later version" applies to it, you have the+option of following the terms and conditions either of that numbered+version or of any later version published by the Free Software+Foundation. If the Program does not specify a version number of the+GNU General Public License, you may choose any version ever published+by the Free Software Foundation.++ If the Program specifies that a proxy can decide which future+versions of the GNU General Public License can be used, that proxy's+public statement of acceptance of a version permanently authorizes you+to choose that version for the Program.++ Later license versions may give you additional or different+permissions. However, no additional obligations are imposed on any+author or copyright holder as a result of your choosing to follow a+later version.++ 15. Disclaimer of Warranty.++ THERE IS NO WARRANTY FOR THE PROGRAM, TO THE EXTENT PERMITTED BY+APPLICABLE LAW. EXCEPT WHEN OTHERWISE STATED IN WRITING THE COPYRIGHT+HOLDERS AND/OR OTHER PARTIES PROVIDE THE PROGRAM "AS IS" WITHOUT WARRANTY+OF ANY KIND, EITHER EXPRESSED OR IMPLIED, INCLUDING, BUT NOT LIMITED TO,+THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR+PURPOSE. THE ENTIRE RISK AS TO THE QUALITY AND PERFORMANCE OF THE PROGRAM+IS WITH YOU. SHOULD THE PROGRAM PROVE DEFECTIVE, YOU ASSUME THE COST OF+ALL NECESSARY SERVICING, REPAIR OR CORRECTION.++ 16. Limitation of Liability.++ IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGREED TO IN WRITING+WILL ANY COPYRIGHT HOLDER, OR ANY OTHER PARTY WHO MODIFIES AND/OR CONVEYS+THE PROGRAM AS PERMITTED ABOVE, BE LIABLE TO YOU FOR DAMAGES, INCLUDING ANY+GENERAL, SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE+USE OR INABILITY TO USE THE PROGRAM (INCLUDING BUT NOT LIMITED TO LOSS OF+DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED BY YOU OR THIRD+PARTIES OR A FAILURE OF THE PROGRAM TO OPERATE WITH ANY OTHER PROGRAMS),+EVEN IF SUCH HOLDER OR OTHER PARTY HAS BEEN ADVISED OF THE POSSIBILITY OF+SUCH DAMAGES.++ 17. Interpretation of Sections 15 and 16.++ If the disclaimer of warranty and limitation of liability provided+above cannot be given local legal effect according to their terms,+reviewing courts shall apply local law that most closely approximates+an absolute waiver of all civil liability in connection with the+Program, unless a warranty or assumption of liability accompanies a+copy of the Program in return for a fee.++ END OF TERMS AND CONDITIONS++ How to Apply These Terms to Your New Programs++ If you develop a new program, and you want it to be of the greatest+possible use to the public, the best way to achieve this is to make it+free software which everyone can redistribute and change under these terms.++ To do so, attach the following notices to the program. It is safest+to attach them to the start of each source file to most effectively+state the exclusion of warranty; and each file should have at least+the "copyright" line and a pointer to where the full notice is found.++ <one line to give the program's name and a brief idea of what it does.>+ Copyright (C) <year> <name of author>++ This program is free software: you can redistribute it and/or modify+ it under the terms of the GNU General Public License as published by+ the Free Software Foundation, either version 3 of the License, or+ (at your option) any later version.++ This program is distributed in the hope that it will be useful,+ but WITHOUT ANY WARRANTY; without even the implied warranty of+ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the+ GNU General Public License for more details.++ You should have received a copy of the GNU General Public License+ along with this program. If not, see <http://www.gnu.org/licenses/>.++Also add information on how to contact you by electronic and paper mail.++ If the program does terminal interaction, make it output a short+notice like this when it starts in an interactive mode:++ <program> Copyright (C) <year> <name of author>+ This program comes with ABSOLUTELY NO WARRANTY; for details type `show w'.+ This is free software, and you are welcome to redistribute it+ under certain conditions; type `show c' for details.++The hypothetical commands `show w' and `show c' should show the appropriate+parts of the General Public License. Of course, your program's commands+might be different; for a GUI interface, you would use an "about box".++ You should also get your employer (if you work as a programmer) or school,+if any, to sign a "copyright disclaimer" for the program, if necessary.+For more information on this, and how to apply and follow the GNU GPL, see+<http://www.gnu.org/licenses/>.++ The GNU General Public License does not permit incorporating your program+into proprietary programs. If your program is a subroutine library, you+may consider it more useful to permit linking proprietary applications with+the library. If this is what you want to do, use the GNU Lesser General+Public License instead of this License. But first, please read+<http://www.gnu.org/philosophy/why-not-lgpl.html>.
+ Language/SMTLib2.hs view
@@ -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
+ Language/SMTLib2/Connection.hs view
@@ -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))
+ Language/SMTLib2/Internals.hs view
@@ -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)
+ Language/SMTLib2/Internals/Instances.hs view
@@ -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
+ Language/SMTLib2/Internals/Interface.hs view
@@ -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'
+ Language/SMTLib2/Internals/Operators.hs view
@@ -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)
+ Language/SMTLib2/Internals/Optimize.hs view
@@ -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
+ Language/SMTLib2/Pipe.hs view
@@ -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"+
+ Language/SMTLib2/Solver.hs view
@@ -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 <http://research.microsoft.com/en-us/um/redmond/projects/z3>.+withZ3 :: MonadIO m => SMT' m a -> m a+withZ3 = withPipe "z3" ["-smt2","-in"]++-- | MathSAT <http://mathsat.fbk.eu>.+withMathSat :: MonadIO m => SMT' m a -> m a+withMathSat = withPipe "mathsat" []++-- | CVC4 is an open-source SMT solver <http://cs.nyu.edu/acsys/cvc4>+withCVC4 :: MonadIO m => SMT' m a -> m a+withCVC4 = withPipe "cvc4" ["--lang smt2"]++-- | SMTInterpol is an experimental interpolating SMT solver <http://ultimate.informatik.uni-freiburg.de/smtinterpol>+withSMTInterpol :: MonadIO m => SMT' m a -> m a+withSMTInterpol = withPipe "java" ["-jar","/usr/local/share/java/smtinterpol.jar","-q"]
+ Language/SMTLib2/Strategy.hs view
@@ -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"
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ smtlib2.cabal view
@@ -0,0 +1,51 @@+Name: smtlib2+Version: 0.1+Author: Henning Günther <guenther@forsyte.at>+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