diff --git a/COPYING b/COPYING deleted file mode 100644 --- a/COPYING +++ /dev/null @@ -1,340 +0,0 @@ - GNU GENERAL PUBLIC LICENSE - Version 2, June 1991 - - Copyright (C) 1989, 1991 Free Software Foundation, Inc. - 59 Temple Place - Suite 330, Boston, MA - 02111-1307, USA. - Everyone is permitted to copy and distribute verbatim copies - of this license document, but changing it is not allowed. - - Preamble - - The licenses for most software are designed to take away your -freedom to share and change it. By contrast, the GNU General Public -License is intended to guarantee your freedom to share and change free -software--to make sure the software is free for all its users. This -General Public License applies to most of the Free Software -Foundation's software and to any other program whose authors commit to -using it. (Some other Free Software Foundation software is covered by -the GNU Library General Public License instead.) You can apply it to -your programs, too. - - When we speak of free software, we are referring to freedom, not -price. Our General Public Licenses are designed to make sure that you -have the freedom to distribute copies of free software (and charge for -this service if you wish), that you receive source code or can get it -if you want it, that you can change the software or use pieces of it -in new free programs; and that you know you can do these things. - - To protect your rights, we need to make restrictions that forbid -anyone to deny you these rights or to ask you to surrender the rights. -These restrictions translate to certain responsibilities for you if you -distribute copies of the software, or if you modify it. - - For example, if you distribute copies of such a program, whether -gratis or for a fee, you must give the recipients all the rights that -you have. You must make sure that they, too, receive or can get the -source code. And you must show them these terms so they know their -rights. - - We protect your rights with two steps: (1) copyright the software, and -(2) offer you this license which gives you legal permission to copy, -distribute and/or modify the software. - - Also, for each author's protection and ours, we want to make certain -that everyone understands that there is no warranty for this free -software. If the software is modified by someone else and passed on, we -want its recipients to know that what they have is not the original, so -that any problems introduced by others will not reflect on the original -authors' reputations. - - Finally, any free program is threatened constantly by software -patents. We wish to avoid the danger that redistributors of a free -program will individually obtain patent licenses, in effect making the -program proprietary. To prevent this, we have made it clear that any -patent must be licensed for everyone's free use or not licensed at all. - - The precise terms and conditions for copying, distribution and -modification follow. - - GNU GENERAL PUBLIC LICENSE - TERMS AND CONDITIONS FOR COPYING, DISTRIBUTION AND MODIFICATION - - 0. This License applies to any program or other work which contains -a notice placed by the copyright holder saying it may be distributed -under the terms of this General Public License. The "Program", below, -refers to any such program or work, and a "work based on the Program" -means either the Program or any derivative work under copyright law: -that is to say, a work containing the Program or a portion of it, -either verbatim or with modifications and/or translated into another -language. (Hereinafter, translation is included without limitation in -the term "modification".) Each licensee is addressed as "you". - -Activities other than copying, distribution and modification are not -covered by this License; they are outside its scope. The act of -running the Program is not restricted, and the output from the Program -is covered only if its contents constitute a work based on the -Program (independent of having been made by running the Program). -Whether that is true depends on what the Program does. - - 1. You may copy and distribute verbatim copies of the Program's -source code as you receive it, in any medium, provided that you -conspicuously and appropriately publish on each copy an appropriate -copyright notice and disclaimer of warranty; keep intact all the -notices that refer to this License and to the absence of any warranty; -and give any other recipients of the Program a copy of this License -along with the Program. - -You may charge a fee for the physical act of transferring a copy, and -you may at your option offer warranty protection in exchange for a fee. - - 2. You may modify your copy or copies of the Program or any portion -of it, thus forming a work based on the Program, and copy and -distribute such modifications or work under the terms of Section 1 -above, provided that you also meet all of these conditions: - - a) You must cause the modified files to carry prominent notices - stating that you changed the files and the date of any change. - - b) You must cause any work that you distribute or publish, that in - whole or in part contains or is derived from the Program or any - part thereof, to be licensed as a whole at no charge to all third - parties under the terms of this License. - - c) If the modified program normally reads commands interactively - when run, you must cause it, when started running for such - interactive use in the most ordinary way, to print or display an - announcement including an appropriate copyright notice and a - notice that there is no warranty (or else, saying that you provide - a warranty) and that users may redistribute the program under - these conditions, and telling the user how to view a copy of this - License. (Exception: if the Program itself is interactive but - does not normally print such an announcement, your work based on - the Program is not required to print an announcement.) - -These requirements apply to the modified work as a whole. If -identifiable sections of that work are not derived from the Program, -and can be reasonably considered independent and separate works in -themselves, then this License, and its terms, do not apply to those -sections when you distribute them as separate works. But when you -distribute the same sections as part of a whole which is a work based -on the Program, the distribution of the whole must be on the terms of -this License, whose permissions for other licensees extend to the -entire whole, and thus to each and every part regardless of who wrote it. - -Thus, it is not the intent of this section to claim rights or contest -your rights to work written entirely by you; rather, the intent is to -exercise the right to control the distribution of derivative or -collective works based on the Program. - -In addition, mere aggregation of another work not based on the Program -with the Program (or with a work based on the Program) on a volume of -a storage or distribution medium does not bring the other work under -the scope of this License. - - 3. You may copy and distribute the Program (or a work based on it, -under Section 2) in object code or executable form under the terms of -Sections 1 and 2 above provided that you also do one of the following: - - a) Accompany it with the complete corresponding machine-readable - source code, which must be distributed under the terms of Sections - 1 and 2 above on a medium customarily used for software interchange; or, - - b) Accompany it with a written offer, valid for at least three - years, to give any third party, for a charge no more than your - cost of physically performing source distribution, a complete - machine-readable copy of the corresponding source code, to be - distributed under the terms of Sections 1 and 2 above on a medium - customarily used for software interchange; or, - - c) Accompany it with the information you received as to the offer - to distribute corresponding source code. (This alternative is - allowed only for noncommercial distribution and only if you - received the program in object code or executable form with such - an offer, in accord with Subsection b above.) - -The source code for a work means the preferred form of the work for -making modifications to it. For an executable work, complete source -code means all the source code for all modules it contains, plus any -associated interface definition files, plus the scripts used to -control compilation and installation of the executable. However, as a -special exception, the source code distributed need not include -anything that is normally distributed (in either source or binary -form) with the major components (compiler, kernel, and so on) of the -operating system on which the executable runs, unless that component -itself accompanies the executable. - -If distribution of executable or object code is made by offering -access to copy from a designated place, then offering equivalent -access to copy the source code from the same place counts as -distribution of the source code, even though third parties are not -compelled to copy the source along with the object code. - - 4. You may not copy, modify, sublicense, or distribute the Program -except as expressly provided under this License. Any attempt -otherwise to copy, modify, sublicense or distribute the Program is -void, and will automatically terminate your rights under this License. -However, parties who have received copies, or rights, from you under -this License will not have their licenses terminated so long as such -parties remain in full compliance. - - 5. You are not required to accept this License, since you have not -signed it. However, nothing else grants you permission to modify or -distribute the Program or its derivative works. These actions are -prohibited by law if you do not accept this License. Therefore, by -modifying or distributing the Program (or any work based on the -Program), you indicate your acceptance of this License to do so, and -all its terms and conditions for copying, distributing or modifying -the Program or works based on it. - - 6. Each time you redistribute the Program (or any work based on the -Program), the recipient automatically receives a license from the -original licensor to copy, distribute or modify the Program subject to -these terms and conditions. You may not impose any further -restrictions on the recipients' exercise of the rights granted herein. -You are not responsible for enforcing compliance by third parties to -this License. - - 7. If, as a consequence of a court judgment or allegation of patent -infringement or for any other reason (not limited to patent issues), -conditions are imposed on you (whether by court order, agreement or -otherwise) that contradict the conditions of this License, they do not -excuse you from the conditions of this License. If you cannot -distribute so as to satisfy simultaneously your obligations under this -License and any other pertinent obligations, then as a consequence you -may not distribute the Program at all. For example, if a patent -license would not permit royalty-free redistribution of the Program by -all those who receive copies directly or indirectly through you, then -the only way you could satisfy both it and this License would be to -refrain entirely from distribution of the Program. - -If any portion of this section is held invalid or unenforceable under -any particular circumstance, the balance of the section is intended to -apply and the section as a whole is intended to apply in other -circumstances. - -It is not the purpose of this section to induce you to infringe any -patents or other property right claims or to contest validity of any -such claims; this section has the sole purpose of protecting the -integrity of the free software distribution system, which is -implemented by public license practices. Many people have made -generous contributions to the wide range of software distributed -through that system in reliance on consistent application of that -system; it is up to the author/donor to decide if he or she is willing -to distribute software through any other system and a licensee cannot -impose that choice. - -This section is intended to make thoroughly clear what is believed to -be a consequence of the rest of this License. - - 8. If the distribution and/or use of the Program is restricted in -certain countries either by patents or by copyrighted interfaces, the -original copyright holder who places the Program under this License -may add an explicit geographical distribution limitation excluding -those countries, so that distribution is permitted only in or among -countries not thus excluded. In such case, this License incorporates -the limitation as if written in the body of this License. - - 9. The Free Software Foundation may publish revised and/or new versions -of the General Public License from time to time. Such new versions will -be similar in spirit to the present version, but may differ in detail to -address new problems or concerns. - -Each version is given a distinguishing version number. If the Program -specifies a version number of this License which applies to it and "any -later version", you have the option of following the terms and conditions -either of that version or of any later version published by the Free -Software Foundation. If the Program does not specify a version number of -this License, you may choose any version ever published by the Free Software -Foundation. - - 10. If you wish to incorporate parts of the Program into other free -programs whose distribution conditions are different, write to the author -to ask for permission. For software which is copyrighted by the Free -Software Foundation, write to the Free Software Foundation; we sometimes -make exceptions for this. Our decision will be guided by the two goals -of preserving the free status of all derivatives of our free software and -of promoting the sharing and reuse of software generally. - - NO WARRANTY - - 11. BECAUSE THE PROGRAM IS LICENSED FREE OF CHARGE, THERE IS NO WARRANTY -FOR THE PROGRAM, TO THE EXTENT PERMITTED BY APPLICABLE LAW. EXCEPT WHEN -OTHERWISE STATED IN WRITING THE COPYRIGHT HOLDERS AND/OR OTHER PARTIES -PROVIDE THE PROGRAM "AS IS" WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESSED -OR IMPLIED, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF -MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE. THE ENTIRE RISK AS -TO THE QUALITY AND PERFORMANCE OF THE PROGRAM IS WITH YOU. SHOULD THE -PROGRAM PROVE DEFECTIVE, YOU ASSUME THE COST OF ALL NECESSARY SERVICING, -REPAIR OR CORRECTION. - - 12. IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGREED TO IN WRITING -WILL ANY COPYRIGHT HOLDER, OR ANY OTHER PARTY WHO MAY MODIFY AND/OR -REDISTRIBUTE THE PROGRAM AS PERMITTED ABOVE, BE LIABLE TO YOU FOR DAMAGES, -INCLUDING ANY GENERAL, SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES ARISING -OUT OF THE USE OR INABILITY TO USE THE PROGRAM (INCLUDING BUT NOT LIMITED -TO LOSS OF DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED BY -YOU OR THIRD PARTIES OR A FAILURE OF THE PROGRAM TO OPERATE WITH ANY OTHER -PROGRAMS), EVEN IF SUCH HOLDER OR OTHER PARTY HAS BEEN ADVISED OF THE -POSSIBILITY OF SUCH DAMAGES. - - END OF TERMS AND CONDITIONS - - Appendix: How to Apply These Terms to Your New Programs - - If you develop a new program, and you want it to be of the greatest -possible use to the public, the best way to achieve this is to make it -free software which everyone can redistribute and change under these terms. - - To do so, attach the following notices to the program. It is safest -to attach them to the start of each source file to most effectively -convey the exclusion of warranty; and each file should have at least -the "copyright" line and a pointer to where the full notice is found. - - - Copyright (C) 19yy - - This program is free software; you can redistribute it and/or modify - it under the terms of the GNU General Public License as published by - the Free Software Foundation; either version 2 of the License, or - (at your option) any later version. - - This program is distributed in the hope that it will be useful, - but WITHOUT ANY WARRANTY; without even the implied warranty of - MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - GNU General Public License for more details. - - You should have received a copy of the GNU General Public License - along with this program; if not, write to the Free Software - Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA. - -Also add information on how to contact you by electronic and paper mail. - -If the program is interactive, make it output a short notice like this -when it starts in an interactive mode: - - Gnomovision version 69, Copyright (C) 19yy name of author - Gnomovision comes with ABSOLUTELY NO WARRANTY; for details type `show w'. - This is free software, and you are welcome to redistribute it - under certain conditions; type `show c' for details. - -The hypothetical commands `show w' and `show c' should show the appropriate -parts of the General Public License. Of course, the commands you use may -be called something other than `show w' and `show c'; they could even be -mouse-clicks or menu items--whatever suits your program. - -You should also get your employer (if you work as a programmer) or your -school, if any, to sign a "copyright disclaimer" for the program, if -necessary. Here is a sample; alter the names: - - Yoyodyne, Inc., hereby disclaims all copyright interest in the program - `Gnomovision' (which makes passes at compilers) written by James Hacker. - - , 1 April 1989 - Ty Coon, President of Vice - -This General Public License does not permit incorporating your program into -proprietary programs. If your program is a subroutine library, you may -consider it more useful to permit linking proprietary applications with the -library. If this is what you want to do, use the GNU Library General -Public License instead of this License. diff --git a/HTab.cabal b/HTab.cabal --- a/HTab.cabal +++ b/HTab.cabal @@ -1,15 +1,15 @@ +cabal-version: 2.4 Name: HTab -Version: 1.6.3 +Version: 1.7.2 Synopsis: Tableau based theorem prover for hybrid logics Description: Tableau based theorem prover for hybrid logics -Homepage: http://www.glyc.dc.uba.ar/intohylo/htab.php -Bug-reports: http://code.google.com/p/intohylo/ +Homepage: http://hub.darcs.net/gh/htab +Bug-reports: http://hub.darcs.net/gh/htab/issues Category: Theorem provers -License: GPL -License-file: COPYING +License: BSD-3-Clause +License-file: LICENSE Author: Guillaume Hoffmann, Carlos Areces, Daniel Gorín, Juan Heguiabehere Maintainer: guillaumh@gmail.com -Cabal-version: >= 1.6.0 Build-type: Simple Extra-source-files: tests/test-example-formulas.hs tests/coverage.sh @@ -17,15 +17,13 @@ examples/*.sh examples/sat/*.frm examples/unsat/*.frm + rc/*.frm source-repository head type: darcs - location: http://www.glyc.dc.uba.ar/intohylo/repos/htab/ - -Flag static - Description: Build a static binary - Default: False + location: http://hub.darcs.net/gh/htab Executable htab + Default-language: Haskell2010 Main-is: htab.hs Other-modules: HTab.Branch HTab.CommandLine @@ -34,27 +32,25 @@ HTab.Formula HTab.Literals HTab.Main + HTab.Memory HTab.ModelGen HTab.Relations HTab.RuleId HTab.Rules HTab.Statistics HTab.Tableau - Build-Depends: base >= 4, base < 5, + Build-Depends: base >= 4.10, base < 5, mtl >= 2, mtl < 3, containers, deepseq, strict, - cmdargs >= 0.10.1, - hylolib == 1.4.* - Extensions: GADTs + random, + cmdargs >= 0.10.10, + hylolib >= 1.5.1 + Default-extensions: GADTs DeriveDataTypeable FlexibleContexts Rank2Types ScopedTypeVariables Hs-Source-Dirs: src ghc-options: -O2 -Wall - ghc-prof-options: -auto-all - - if flag(static) - ghc-options: -static -optl-static -optl-pthread diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,30 @@ +Copyright (c) 2019, Guillaume Hoffmann + +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are met: + + * Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + + * Redistributions in binary form must reproduce the above + copyright notice, this list of conditions and the following + disclaimer in the documentation and/or other materials provided + with the distribution. + + * Neither the name of Guillaume Hoffmann nor the names of other + contributors may be used to endorse or promote products derived + from this software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT +OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, +SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT +LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, +DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY +THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT +(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE +OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/NEWS b/NEWS --- a/NEWS +++ b/NEWS @@ -1,3 +1,8 @@ +* 2019.04.25 : 1.7.2 + o --memory flag to run memory logic testsuite + o compile with GHC 8.6 +* 2016.06.03 : 1.7.0 + o --translation to support relation-changing modal logics * 2011.12.02 : 1.6.0 o pattern based blocking by default o lazy branching on all nodes except with chain blocking diff --git a/rc/br_infinite.frm b/rc/br_infinite.frm new file mode 100644 --- /dev/null +++ b/rc/br_infinite.frm @@ -0,0 +1,18 @@ +signature { +propositions { s } +nominals { } +relations { br, gbr } +} + +theory + +{ + s; + [] false; + [br](s --> [br]!s); + [br](!s --> [] !s); +

true; + [br]<> true; + [br][br](s --> [](!s --> [][]!s)); + [br][][][br](s --> <>( !s & <><>s )); +} diff --git a/rc/br_no_tree.frm b/rc/br_no_tree.frm new file mode 100644 --- /dev/null +++ b/rc/br_no_tree.frm @@ -0,0 +1,12 @@ +signature { +propositions { p } +nominals { } +relations { br } +} + +theory + +{ + [] false; +
[] false; +} diff --git a/rc/br_unsat_bad_infinite.frm b/rc/br_unsat_bad_infinite.frm new file mode 100644 --- /dev/null +++ b/rc/br_unsat_bad_infinite.frm @@ -0,0 +1,14 @@ +signature { +propositions { s } +nominals { } +relations { br, gbr } +} + +theory + +{ + s; + [] false; + [br](s --> [br]!s); + [br][]!s; +} diff --git a/rc/gbr_no_tree.frm b/rc/gbr_no_tree.frm new file mode 100644 --- /dev/null +++ b/rc/gbr_no_tree.frm @@ -0,0 +1,12 @@ +signature { +propositions { p } +nominals { } +relations { sw } +} + +theory + +{ + [] false; + [] false; +} diff --git a/rc/gsab_confluence.frm b/rc/gsab_confluence.frm new file mode 100644 --- /dev/null +++ b/rc/gsab_confluence.frm @@ -0,0 +1,14 @@ +signature { +propositions { a, b, c } +nominals { } +relations { gsb } +} + +theory + +{ + <>(a & !b & <><>a ); + <>(b & !a & <><>b ); + [][](c & []!c); + [][][] false; +} diff --git a/rc/gsab_count.frm b/rc/gsab_count.frm new file mode 100644 --- /dev/null +++ b/rc/gsab_count.frm @@ -0,0 +1,13 @@ +signature { +propositions { } +nominals { } +relations { gsb } +} + +theory + +{ + true; + [gsb][gsb][gsb][gsb]false; +} + diff --git a/rc/gsab_infinite.frm b/rc/gsab_infinite.frm new file mode 100644 --- /dev/null +++ b/rc/gsab_infinite.frm @@ -0,0 +1,20 @@ +signature { +propositions { s } +nominals { } +relations { sb, gsb } +} + +theory + +{ + s; + []!s; + <> true; + []( <>s & !<>s ); + []<>!s; + [][]( !s --> ( <>s & !<>s) ); + [gsb]( (<>(<>s & <>(!s & !<>s)) ) --> <>!<>s); + [gsb][]( (!<>s) --> []<>s ); + [gsb](!<>( (!<>s) & <><>( !s & (<>s) & <>!<>s))); + [gsb][gsb]( (<>((!<>s) & <><>(!s & !<>s))) --> <>(!<>s & <>!<>s)); +} diff --git a/rc/gsab_no_tree.frm b/rc/gsab_no_tree.frm new file mode 100644 --- /dev/null +++ b/rc/gsab_no_tree.frm @@ -0,0 +1,12 @@ +signature { +propositions { } +nominals { } +relations { gsb } +} + +theory + +{ + <><> true; + [gsb][] false; +} diff --git a/rc/gswap_infinite.frm b/rc/gswap_infinite.frm new file mode 100644 --- /dev/null +++ b/rc/gswap_infinite.frm @@ -0,0 +1,25 @@ +signature { +propositions { s } +nominals { } +relations { gsw } +} + +theory + +{ + s; + []!s; + [][]!s; + [][][]!s; + [][][][]!s; + [][][][][]!s; + [][][][][][]!s; + [][][][][][][]!s; + [][][][][][][][]!s; + [][][][][][][][][]!s; + <> true; + []<> true; + [][][gsw][gsw][][](s --> <><><>s); + [][gsw](<>s -> [][]!s); + [][][][gsw][gsw][gsw]((<><><>s) --> <><><>(!s & <><><>s)); +} diff --git a/rc/gswap_no_tree.frm b/rc/gswap_no_tree.frm new file mode 100644 --- /dev/null +++ b/rc/gswap_no_tree.frm @@ -0,0 +1,12 @@ +signature { +propositions { } +nominals { } +relations { gsw } +} + +theory + +{ + []false; + <> true; +} diff --git a/rc/mem_br_struct.frm b/rc/mem_br_struct.frm new file mode 100644 --- /dev/null +++ b/rc/mem_br_struct.frm @@ -0,0 +1,22 @@ +signature { +propositions { s, t, a, b, c, d } +nominals { } +relations { br } +} + +theory + +{ + s; + []false; + [br](s --> [br]!s); + [br](!s --> []!s); + +
(!s & t &
( !s & !t & + a & !b & !c & !d & + <>(!s & !a & b & !c & !d & + <>(!s & !a & !b & c & !d & + <>(!s & !a & !b & !c & d + ))))); + +} diff --git a/rc/mem_br_struct_refl.frm b/rc/mem_br_struct_refl.frm new file mode 100644 --- /dev/null +++ b/rc/mem_br_struct_refl.frm @@ -0,0 +1,18 @@ +signature { +propositions { s, t } +nominals { } +relations { br } +} + +theory + +{ + s; + []false; + [br](s --> [br]!s); + [br](!s --> []!s); + +
(!s & t &
( !s & !t & +
(s &
( (<>s) & <>(!s & <>s))) + )); +} diff --git a/rc/mem_sab_struct.frm b/rc/mem_sab_struct.frm new file mode 100644 --- /dev/null +++ b/rc/mem_sab_struct.frm @@ -0,0 +1,25 @@ +signature { +propositions { s, a, b, c } +nominals { } +relations { sb } +} + +theory + +{ + s; + []!s; + + []<>s; + [sb][sb](s --> []<>s); + [][sb](s --> <>[]!s); + + [][](!s --> <>s); + [][][](s --> []<>s); + [][][sb]( s --> <>[]!s); + + [][sb](s --> [sb]( ([]!s) --> [][](s --> []<>s))); + [][sb](s --> [](([]!s) --> [][](s --> <>[]!s))); + + <>(a & !b & !c & <>(!s & !a & b & !c & <>(!s & !a & !b & c ))); +} diff --git a/rc/mem_sab_struct2.frm b/rc/mem_sab_struct2.frm new file mode 100644 --- /dev/null +++ b/rc/mem_sab_struct2.frm @@ -0,0 +1,25 @@ +signature { +propositions { s, a, b, c, d } +nominals { } +relations { sb } +} + +theory + +{ + s; + []!s; + + []<>s; + [sb][sb](s --> []<>s); + [][sb](s --> <>[]!s); + + [][](!s --> <>s); + [][][](s --> []<>s); + [][][sb]( s --> <>[]!s); + + [][sb](s --> [sb]( ([]!s) --> [][](s --> []<>s))); + [][sb](s --> [](([]!s) --> [][](s --> <>[]!s))); + + <>(a & !b & !c & !d & <>(!s & !a & b & !c & !d & <>(!s & !a & !b & c & !d & <> (!s & !a & !b & !c & d)))); +} diff --git a/rc/mem_sab_struct3.frm b/rc/mem_sab_struct3.frm new file mode 100644 --- /dev/null +++ b/rc/mem_sab_struct3.frm @@ -0,0 +1,25 @@ +signature { +propositions { s, a, b, c, d, e } +nominals { } +relations { sb } +} + +theory + +{ + s; + []!s; + + []<>s; + [sb][sb](s --> []<>s); + [][sb](s --> <>[]!s); + + [][](!s --> <>s); + [][][](s --> []<>s); + [][][sb]( s --> <>[]!s); + + [][sb](s --> [sb]( ([]!s) --> [][](s --> []<>s))); + [][sb](s --> [](([]!s) --> [][](s --> <>[]!s))); + + <>(a & !b & !c & !d & !e & <>(!s & !a & b & !c & !d & !e & <>(!s & !a & !b & c & !d & !e & <> (!s & !a & !b & !c & d & !e & <> (!s & !a & !b & !c & !d & e) )))); +} diff --git a/rc/mem_sab_struct_refl.frm b/rc/mem_sab_struct_refl.frm new file mode 100644 --- /dev/null +++ b/rc/mem_sab_struct_refl.frm @@ -0,0 +1,26 @@ +signature { +propositions { s, a, b, c } +nominals { } +relations { sb } +} + +theory + +{ + s; + []!s; + + []<>s; + [sb][sb](s --> []<>s); + [][sb](s --> <>[]!s); + + [][](!s --> <>s); + [][][](s --> []<>s); + [][][sb]( s --> <>[]!s); + + [][sb](s --> [sb]( ([]!s) --> [][](s --> []<>s))); + [][sb](s --> [](([]!s) --> [][](s --> <>[]!s))); + + + <>( (s & ( (!<>s) & <>( (!<>s ) ) ) ) ); +} diff --git a/rc/mem_sw_struct.frm b/rc/mem_sw_struct.frm new file mode 100644 --- /dev/null +++ b/rc/mem_sw_struct.frm @@ -0,0 +1,28 @@ +signature { +propositions { s, a, b, c, d } +nominals { } +relations { sw } +} + +theory + +{ + s; + []!s; + [](!s --> ((<>(s & []false)) & [sw](s --> []!<>s))); + [][](!s --> ((<>(s & []false)) & [sw](s --> []!<>s))); + [][][](!s --> ((<>(s & []false)) & [sw](s --> []!<>s))); + + [][sw](s --> [][][](s --> [] false)); + [][][sw](s --> [][][](s --> [] false)); + + + [sw][sw](!s --> (s & <><>(s & <>!<>s))); + + + <>(!s & a & !b & !c & !d & + <>(!s & !a & b & !c & !d & + <>(!s & !a & !b & c & !d & + <>(!s & !a & !b & !c & d + )))); +} diff --git a/rc/mem_sw_struct_refl.frm b/rc/mem_sw_struct_refl.frm new file mode 100644 --- /dev/null +++ b/rc/mem_sw_struct_refl.frm @@ -0,0 +1,24 @@ +signature { +propositions { s, a, b, c, d } +nominals { } +relations { sw } +} + +theory + +{ + s; + []!s; + [](!s --> ((<>(s & []false)) & [sw](s --> []!<>s))); + [][](!s --> ((<>(s & []false)) & [sw](s --> []!<>s))); + [][][](!s --> ((<>(s & []false)) & [sw](s --> []!<>s))); + + [][sw](s --> [][][](s --> [] false)); + [][][sw](s --> [][][](s --> [] false)); + + + [sw][sw](!s --> (s & <><>(s & <>!<>s))); + + + <>( a & (s & <><>(!s & !<>s))); +} diff --git a/rc/sab_loop.frm b/rc/sab_loop.frm new file mode 100644 --- /dev/null +++ b/rc/sab_loop.frm @@ -0,0 +1,14 @@ +signature { +propositions { a, b } +nominals { } +relations { sb } +} + +theory + +{ + <>(a & !b & <><>a); + <>(b & !a & <><>b); + [sb](a --> [][]!a); + [sb](b --> [][]!b); +} diff --git a/rc/sab_loop_diamond.frm b/rc/sab_loop_diamond.frm new file mode 100644 --- /dev/null +++ b/rc/sab_loop_diamond.frm @@ -0,0 +1,17 @@ +signature { +propositions { a, b } +nominals { } +relations { sb } +} + +theory + +{ + <>(a & !b & <><><>a); + <>(b & !a & <><><>b); + [sb](a --> [][][]!a); + [sb](b --> [][][]!b); + + [][][sb][][][] false; + [][][][][]<> true; +} diff --git a/rc/sab_no_tree.frm b/rc/sab_no_tree.frm new file mode 100644 --- /dev/null +++ b/rc/sab_no_tree.frm @@ -0,0 +1,12 @@ +signature { +propositions { } +nominals { } +relations { sb, gsb } +} + +theory + +{ + <><>true; + [sb][]false; +} diff --git a/rc/sab_sat_01.frm b/rc/sab_sat_01.frm new file mode 100644 --- /dev/null +++ b/rc/sab_sat_01.frm @@ -0,0 +1,13 @@ +signature { +propositions { p, q } +nominals { } +relations { sb, gsb } +} + +theory + +{ + p; + q; + ( <><> true) ; +} diff --git a/rc/swap_diamond.frm b/rc/swap_diamond.frm new file mode 100644 --- /dev/null +++ b/rc/swap_diamond.frm @@ -0,0 +1,15 @@ +signature { +propositions { a, b } +nominals { } +relations { sw } +} + +theory + +{ + <>(a & !b & <>a); + <>(b & !a & <>b); + [sw][][sw][][] false; + [][sw][][] false; + <><><><><> true; +} diff --git a/rc/swap_infinite.frm b/rc/swap_infinite.frm new file mode 100644 --- /dev/null +++ b/rc/swap_infinite.frm @@ -0,0 +1,25 @@ +signature { +propositions { s } +nominals { } +relations { sw } +} + +theory + +{ + s; + []!s; + [][]!s; + [][][]!s; + [][][][]!s; + [][][][][]!s; + [][][][][][]!s; + [][][][][][][]!s; + [][][][][][][][]!s; + [][][][][][][][][]!s; + <> true; + []<> true; + [sw][sw](!s --> <><><><><>s); + [sw][][]!s; + [sw][sw][sw](([]!s) --> <><><>(!s & <><><>s)); +} diff --git a/rc/swap_no_tree.frm b/rc/swap_no_tree.frm new file mode 100644 --- /dev/null +++ b/rc/swap_no_tree.frm @@ -0,0 +1,15 @@ +signature { +propositions { p } +nominals { } +relations { sw } +} + +theory + +{ + p; + []!p; + [][]!p; + [][][]!p; + <><>p; +} diff --git a/src/HTab/Branch.hs b/src/HTab/Branch.hs --- a/src/HTab/Branch.hs +++ b/src/HTab/Branch.hs @@ -13,11 +13,11 @@ diaAlreadyDone, downAlreadyDone, ReducedDisjunct(..), patternOf, findByPattern, -prefixes, isInTheModel, +prefixes, isNominalUrfather, isInTheModel, +positiveNomOf, isTransitive ) where -import Control.Applicative ( (<$>) ) import Data.Maybe( mapMaybe ) import Data.Map ( Map ) @@ -30,17 +30,18 @@ import qualified HTab.DMap as D import qualified HTab.DisjSet as DS import HTab.CommandLine(Params(..)) -import HTab.Formula +import HTab.Formula hiding ( list ) import HTab.Relations ( OutRels, emptyRels, insertRelation, mergePrefixes, successors, linksFromTo, showRels ) import HTab.Literals ( UpdateResult(..), Literals, SlotUpdateResult(..), LiteralSlot, - updateMap, lsUnions, lsAddDeps, lsQuery) + updateMap, lsUnions, lsAddDeps, lsQuery, + positiveNom) data BranchInfo = BranchOK Branch | BranchClash Branch Prefix DependencySet Formula -type BoxConstraints = IntMap {- Prefix -} (Map Rel [(Formula,Depth,DependencySet)]) +type BoxConstraints = IntMap {- Prefix -} (Map Rel [(Formula,DependencySet)]) type BranchingWitnesses = IntMap {- Prefix -} (Map Literal [PrFormula]) type EquivClasses = DS.DisjSet DS.Pointer @@ -51,7 +52,7 @@ accStr :: OutRels, -- local and global constraints boxFwd :: BoxConstraints, - univCons :: [(DependencySet,Formula,Depth)], + univCons :: [(DependencySet,Formula)], -- pending formulas / todo lists todoList :: TodoList, -- saturation of rules @@ -73,8 +74,7 @@ -- information about language of input formula and blocking mode inputLanguage :: LanguageInfo, blockedDias :: IntMap {- Prefix -} [PrFormula], - relInfo :: RelInfo, - generators :: [Generator]} + relInfo :: RelInfo} -- @@ -84,7 +84,7 @@ "\nLiterals:", showIMap (\v -> "(" ++ showMap_lits v ++ ")") "\n " (literals br), "\nRelations: ", showRels (accStr br), "\nBoxes: ", showIMap (\v -> "(" ++ showMap_rel v ++ ")") "\n " (boxFwd br), - "\n", show (todoList br), + "\n", showTodo (todoList br), "\nWitnesses: ", showIMap (\v -> "(" ++ showMap_lits2 v ++ ")") "\n " (brWitnesses br), "\nDia rule chart: ", show (diaRlCh br), @@ -97,13 +97,12 @@ "\nPrefix-Nominal classes : ", showMap ", " (nomPrefClasses br), "\nlastPref : ", show (lastPref br), " nextnom : ", show (nextNom br), - "\ngenerators :", show (generators br), "\nRel info:", show (relInfo br), "\n" ] where showIMap :: (a -> String) -> String -> IntMap a -> String showIMap vShow sep im - = I.foldWithKey (\k v -> (++ sep ++ show k ++ " -> " ++ vShow v )) "" im + = I.foldrWithKey (\k v -> (++ sep ++ show k ++ " -> " ++ vShow v )) "" im showMap sep = Map.foldrWithKey (\k v -> (++ sep ++ show k ++ " -> " ++ show v )) "" showMap_lits ml = Map.foldrWithKey (\l d -> (++ show l ++ " " ++ dsShow d ++ ", ")) "" ml showMap_lits2 = Map.foldrWithKey (\l fs -> (++ show l ++ " :" ++ show fs ++ ", ")) "" @@ -117,8 +116,18 @@ downTodo :: Set PrFormula, mergeTodo :: Set (DependencySet, Prefix, Nom), roleIncTodo :: Set (DependencySet, Prefix, Prefix, [Rel]) } - deriving Show +showTodo :: TodoList -> String +showTodo t = unlines + [ "DisjTodo " ++ show (disjTodo t) + , "DiaTodo " ++ show (diaTodo t) + , "ExistTodo " ++ show (existTodo t) + , "AtTodo " ++ show (atTodo t) + , "DownTodo " ++ show (downTodo t) + , "MergeTodo " ++ show (mergeTodo t) + , "RoleITodo " ++ show (roleIncTodo t) + ] + emptyTodoList :: TodoList emptyTodoList = TodoList { disjTodo = Set.empty, @@ -146,16 +155,16 @@ $ bookKeepFormula p pf br bookKeepFormula :: Params -> PrFormula -> Branch -> Branch -bookKeepFormula p pf_@(PrFormula pr ds md f) br +bookKeepFormula p pf_@(PrFormula pr ds f) br = rescheduleLazyBranching p pf $ rescheduleBlockedDias ur br where (ur,ds2,_) = getUrfatherAndDeps br (DS.Prefix pr) pf = if ur == pr then pf_ - else PrFormula ur (dsUnion ds ds2) md f + else PrFormula ur (dsUnion ds ds2) f rescheduleLazyBranching :: Params -> PrFormula -> Branch -> Branch -rescheduleLazyBranching p (PrFormula pr ds _ (Lit l)) br -- pr already urfather +rescheduleLazyBranching p (PrFormula pr ds (Lit l)) br -- pr already urfather | lazyBranching p && isProp l = let (Just innerMap) = I.lookup pr (brWitnesses br) @@ -183,13 +192,13 @@ putAwayFormula :: Params -> PrFormula -> Branch -> BranchInfo -putAwayFormula p pf@(PrFormula pr ds md f2) br = +putAwayFormula p pf@(PrFormula pr ds f2) br = case f2 of - Con fs -> addFormulas p (prefix pr ds md fs) br + Con fs -> addFormulas p (prefix pr ds fs) br Dis _ -> putAwayDisjunction p pf br Dia _ _ -> BranchOK $ addToTodo pf br - Box r f -> addBoxConstraint pr r md f ds p br - A f -> addUnivConstraint md f ds p br + Box r f -> addBoxConstraint pr r f ds p br + A f -> addUnivConstraint f ds p br E _ -> BranchOK $ addToTodo pf br At _ _ -> BranchOK $ addToTodo pf br Down _ _ -> BranchOK $ addToTodo pf br @@ -197,13 +206,13 @@ Lit l -> addToLiterals pr ds l br putAwayDisjunction :: Params -> PrFormula -> Branch -> BranchInfo -putAwayDisjunction p pf@(PrFormula pr ds md f@(Dis fs)) br +putAwayDisjunction p pf@(PrFormula pr ds f@(Dis fs)) br | lazyBranching p = case reduceDisjunctionProposeLazy br pr fs of Contradiction dsClash -> BranchClash br pr (dsUnion ds dsClash) f Triviality -> BranchOK br Reduced new_ds disjuncts mProposed - -> let fNew = PrFormula pr (dsUnion ds new_ds) md (Dis disjuncts) + -> let fNew = PrFormula pr (dsUnion ds new_ds) (Dis disjuncts) -- TODO if there was no reduction, leave ds in case mProposed of @@ -241,7 +250,7 @@ {- todo list functions -} addToTodo :: PrFormula -> Branch -> Branch -addToTodo pf@(PrFormula p ds _ f2) br = +addToTodo pf@(PrFormula p ds f2) br = if alreadyDone then br else brWithSaturation{todoList = newTodoList} @@ -283,7 +292,7 @@ br2 = br{blockedDias = I.delete pr $ blockedDias br} addToBlockedDias :: PrFormula -> Branch -> BranchInfo -addToBlockedDias f@(PrFormula pr _ _ _) br +addToBlockedDias f@(PrFormula pr _ _) br = BranchOK br{blockedDias = I.insertWith (++) ur [f] (blockedDias br)} where ur = getUrfather br (DS.Prefix pr) @@ -321,7 +330,7 @@ newLiterals = I.delete oldUr $ I.insert newUr slot $ literals br -- structures that merge - newBoxFwd = D.moveInnerPlusDeps3 fDs (boxFwd br) oldUr newUr + newBoxFwd = D.moveInnerPlusDeps fDs (boxFwd br) oldUr newUr newAccStr = mergePrefixes (accStr br) oldUr newUr fDs newDiaRlCh = moveInMap (diaRlCh br) oldUr newUr Set.union newBlockedDias = moveInMap (blockedDias br) oldUr newUr (++) @@ -385,13 +394,13 @@ -- to a branch as several prefixed formulas with different branching dependencies. -- This functions takes a list of prefixed formulas, looks which inner formulas -- are the same and merge their branching dependencies. -nubAndMergeDeps prfs = namd prfs (Map.empty::Map (Prefix,Formula,Depth) DependencySet) +nubAndMergeDeps prfs = namd prfs (Map.empty::Map (Prefix,Formula) DependencySet) -namd :: [PrFormula] -> Map (Prefix,Formula,Depth) DependencySet -> [PrFormula] -namd ((PrFormula p ds md f):prfs) theMap = - namd prfs (Map.insertWith dsUnion (p,f,md) ds theMap) +namd :: [PrFormula] -> Map (Prefix,Formula) DependencySet -> [PrFormula] +namd ((PrFormula p ds f):prfs) theMap = + namd prfs (Map.insertWith dsUnion (p,f) ds theMap) -namd [] theMap = map (\((p,f,md),ds) -> PrFormula p ds md f) (Map.assocs theMap) +namd [] theMap = map (\((p,f),ds) -> PrFormula p ds f) (Map.assocs theMap) {- handling nominal urfathers, equivalence classes and dependencies -} @@ -434,51 +443,51 @@ {- box-related constraints -} boxRule :: DependencySet - -> (Map Rel [(Formula,Depth,DependencySet)], + -> (Map Rel [(Formula,DependencySet)], Map Rel [(Prefix,DependencySet)] ) -> [PrFormula] boxRule deps (mapBox, mapAcc) - = [PrFormula p (dsUnions [deps,ds1,ds2]) md f | + = [PrFormula p (dsUnions [deps,ds1,ds2]) f | r1 <- Map.keys mapBox, r2 <- Map.keys mapAcc, r1 == r2, - (f,md,ds1) <- (Map.!) mapBox r1, + (f,ds1) <- (Map.!) mapBox r1, (p,ds2) <- (Map.!) mapAcc r2 ] -addBoxConstraint :: Prefix -> Rel -> Depth -> Formula -> DependencySet -> Params -> Branch +addBoxConstraint :: Prefix -> Rel -> Formula -> DependencySet -> Params -> Branch -> BranchInfo -addBoxConstraint pr_ r md f ds p br +addBoxConstraint pr_ r f ds p br | boxAlreadyDone br pr (r,f) = BranchOK br | otherwise - = let newBr = br{boxFwd = updateBoxConstr pr r (md+1) f ds (boxFwd br)} + = let newBr = br{boxFwd = updateBoxConstr pr r f ds (boxFwd br)} succs = get [] r $ successors (accStr br) pr toAdd = fromTrans ++ fromBox fromTrans = if isTransitive (relInfo br) r - then map (\(pr2,ds2) -> PrFormula pr2 (dsUnion ds ds2) md (Box r f)) succs + then map (\(pr2,ds2) -> PrFormula pr2 (dsUnion ds ds2) (Box r f)) succs else [] - fromBox = map (\(pr2,ds2) -> PrFormula pr2 (dsUnion ds ds2) (md+1) f) succs + fromBox = map (\(pr2,ds2) -> PrFormula pr2 (dsUnion ds ds2) f) succs -- todo check again with new pattern, create successor if new pattern not realized in addFormulas p toAdd newBr where pr = getUrfather br (DS.Prefix pr_) -updateBoxConstr :: Prefix -> Rel -> Depth -> Formula -> DependencySet -> BoxConstraints +updateBoxConstr :: Prefix -> Rel -> Formula -> DependencySet -> BoxConstraints -> BoxConstraints -updateBoxConstr p1_ r_ md_ f_ ds_ boxConstr_ = +updateBoxConstr p1_ r_ f_ ds_ boxConstr_ = case I.lookup p1_ boxConstr_ of - Nothing -> I.insert p1_ (Map.singleton r_ [(f_,md_,ds_)]) boxConstr_ + Nothing -> I.insert p1_ (Map.singleton r_ [(f_,ds_)]) boxConstr_ Just innerMap -> case Map.lookup r_ innerMap of Nothing - -> I.insert p1_ (Map.insert r_ [(f_,md_,ds_)] innerMap) boxConstr_ + -> I.insert p1_ (Map.insert r_ [(f_,ds_)] innerMap) boxConstr_ Just innerInnerList - -> I.insert p1_ (Map.insert r_ ((f_,md_,ds_):innerInnerList) innerMap) boxConstr_ + -> I.insert p1_ (Map.insert r_ ((f_,ds_):innerInnerList) innerMap) boxConstr_ boxAlreadyDone :: Branch -> Prefix -> (Rel,Formula) -> Bool boxAlreadyDone br ur (r,f) = case ( do inner <- I.lookup ur (boxFwd br) - boxes <- map (\(e,_,_) -> e) <$> Map.lookup r inner + boxes <- map (\(e,_) -> e) <$> Map.lookup r inner return (f `elem` boxes) ) of Just True -> True _ -> False @@ -492,9 +501,9 @@ toAdd = transApplications ++ boxApplications transApplications = if isTransitive (relInfo br) r - then map (\(f,md,ds2) -> PrFormula p2 (dsUnion ds ds2) (md+1) (Box r f)) toSendFwd + then map (\(f,ds2) -> PrFormula p2 (dsUnion ds ds2) (Box r f)) toSendFwd else [] - boxApplications = map (\(f,md,ds2) -> PrFormula p2 (dsUnion ds ds2) md f) toSendFwd + boxApplications = map (\(f,ds2) -> PrFormula p2 (dsUnion ds ds2) f) toSendFwd p1 = getUrfather br (DS.Prefix p1_) p2 = getUrfather br (DS.Prefix p2_) toSendFwd = get [] r $ iget Map.empty p1 (boxFwd br) @@ -540,7 +549,7 @@ -- { f } U { f' | p:[r]f' in branch } -- r has to be forward patternOf :: Branch -> PrFormula -> Set Formula -patternOf br (PrFormula pr _ _ (Dia r f)) +patternOf br (PrFormula pr _ (Dia r f)) = Set.insert f boxes where ur = getUrfather br (DS.Prefix pr) boxes = if isTransitive (relInfo br) r @@ -552,7 +561,7 @@ boxesOf :: Branch -> Prefix -> Rel -> Set Formula boxesOf br p r - = set $ map (\(e,_,_) -> e) $ get [] r $ iget Map.empty p (boxFwd br) + = set $ map (\(e,_) -> e) $ get [] r $ iget Map.empty p (boxFwd br) findByPattern :: Branch -> Set Formula -> Prefix findByPattern br pattern = @@ -567,13 +576,13 @@ addDiaRuleCheck :: Prefix -> (Rel,Formula) -> Prefix -> Branch -> BranchInfo addDiaRuleCheck pr (r,f) newPr br = BranchOK br2 - where pattern = patternOf br (PrFormula ur dsEmpty 0 (Dia r f)) + where pattern = patternOf br (PrFormula ur dsEmpty (Dia r f)) br1 = br{patterns = I.insert newPr pattern (patterns br)} br2 = br1{diaRlCh=I.insertWith Set.union ur (Set.singleton (r,f)) (diaRlCh br1)} ur = getUrfather br (DS.Prefix pr) diaAlreadyDone :: Branch -> PrFormula -> Bool -diaAlreadyDone b (PrFormula p _ _ (Dia r f)) = +diaAlreadyDone b (PrFormula p _ (Dia r f)) = case I.lookup ur (diaRlCh b) of Nothing -> False Just fset -> Set.member (r,f) fset @@ -588,7 +597,7 @@ where ur = getUrfather br (DS.Prefix pr) downAlreadyDone :: Branch -> PrFormula -> Bool -downAlreadyDone b (PrFormula p _ _ f@(Down _ _)) = +downAlreadyDone b (PrFormula p _ f@(Down _ _)) = case I.lookup ur (downRlCh b) of Nothing -> False Just fset -> Set.member f fset @@ -596,17 +605,22 @@ downAlreadyDone _ _ = error "down already done : wrong formula kind" -addUnivConstraint :: Depth -> Formula -> DependencySet -> Params -> Branch -> BranchInfo -addUnivConstraint md f ds p br - = addFormulas p [PrFormula pr ds (md+1) f | pr <- urfathers] newBr - where newBr = br{univCons = (ds,f,md+1):(univCons br)} +-- | return some nominal that holds at a given prefix +positiveNomOf :: Branch -> Prefix -> Maybe String +positiveNomOf b p = positiveNom (literals b) ur + where ur = getUrfather b (DS.Prefix p) + +addUnivConstraint :: Formula -> DependencySet -> Params -> Branch -> BranchInfo +addUnivConstraint f ds p br + = addFormulas p [PrFormula pr ds f | pr <- urfathers] newBr + where newBr = br{univCons = (ds,f):(univCons br)} prefs = [0..(lastPref br)] urfathers = filter (isNominalUrfather br) prefs createNewNode :: Params -> Branch -> BranchInfo createNewNode p br = addFormulas p - ( map (\(ds,f,md) -> PrFormula newPr ds md f) univConstraints ) + ( map (\(ds,f) -> PrFormula newPr ds f) univConstraints ) newBrWithRefl where newPr = lastPref br + 1 newBr = br{lastPref = newPr} @@ -627,9 +641,9 @@ -- - add a nominal formula at a fresh prefix for each nominal of the input language -- (even if the nominal was filtered out during lexical normalisation) -- - add reflexive links for prefixes 0 and nominal witnesses -initialBranch :: Params -> LanguageInfo -> RelInfo -> [Generator] -> Formula +initialBranch :: Params -> LanguageInfo -> RelInfo -> Formula -> BranchInfo -initialBranch p fLang relInfo_ gs f +initialBranch p fLang relInfo_ f = addFormulas p [pf] br where pf = firstPrefixedFormula f @@ -661,8 +675,7 @@ nomPrefClasses = initClasses, inputLanguage = fLang, blockedDias = I.empty, - relInfo = relInfo_, - generators = gs + relInfo = relInfo_ } addToLiterals :: Prefix -> DependencySet -> Literal -> Branch -> BranchInfo @@ -750,5 +763,4 @@ get :: (Ord k) => a -> k -> Map k a -> a get = Map.findWithDefault - diff --git a/src/HTab/CommandLine.hs b/src/HTab/CommandLine.hs --- a/src/HTab/CommandLine.hs +++ b/src/HTab/CommandLine.hs @@ -10,7 +10,6 @@ data Params = Params { filename :: FilePath, - symfile :: Maybe FilePath, genModel :: Maybe FilePath, dotModel :: Bool, timeout :: Int, @@ -23,15 +22,19 @@ showFormula :: Bool, allTransitive :: Bool, allReflexive :: Bool + , translate :: Bool + , minimal :: Bool + , random :: Bool + , seed :: Maybe String + , test_translations :: Bool } deriving (Show, Data, Typeable) -data UnitProp = Eager | UPYes | UPNo deriving (Data, Typeable, Eq, Show) +data UnitProp = UPYes | Eager | UPNo deriving (Data, Typeable, Eq, Show) defaultParams :: Annotate Ann defaultParams = record Params{} [ filename := "" += name "f" += typFile += help "input file", - symfile := Nothing += name "s" += typFile += help "input symmetries file (not used yet)", genModel := Nothing += name "m" += typFile += help "output model file", dotModel := False += help "output model in dot format (otherwise: hylolib format)", timeout := 0 += name "t" += help "timeout (in seconds, default=none)", @@ -40,12 +43,17 @@ semBranch := True += help "enable semantic branching (default)", backjumping := True += help "enable backjumping (default)", lazyBranching := True += help "enable lazy branching (default)" , - unitProp `enum_` [atom Eager += explicit += name "eager" += help "unit propagation: eager (default)", - atom UPYes += explicit += name "unit-prop" += help "unit propagation: enabled", - atom UPNo += explicit += name "no-unit-prop" += help "unit propagation: disabled"] , + unitProp `enum_` [atom UPYes += explicit += name "unit-prop" += help "unit propagation on selected disjunction (default)", + atom Eager += explicit += name "eager" += help "unit propagation on all disjunctions", + atom UPNo += explicit += name "no-unit-prop" += help "unit propagation disabled"] , showFormula := False += help "display formula", allTransitive := False += help "make all relations transitive", - allReflexive := False += help "make all relations reflexive" + allReflexive := False += help "make all relations reflexive", + translate := False += help "translate relation-changing formulas to hybrid", + minimal := False += help "look for minimal model (slow)", + random := False += help "randomly select next disjunctive formula, also randomize disjuncts", + seed := Nothing += help "set random seed (integer)", + test_translations := False += help "run the memory-to-relation-changing test suite" ] += verbosity strategyVal :: String @@ -62,12 +70,15 @@ " b = down-arrow binder | = or", " r = role inclusion", "", - "The default is `" ++ strategyVal ++ "'", - "The rules conjunction, box, universal modality and converse difference", - "modality are immediate, thus do not belong to the strategy."] + "The default is \"" ++ strategyVal ++ "\"", + "The rules conjunction, box, and universal modality", + "are applied immediately, thus do not belong to the strategy."] return False - | null (filename p) = + | null (filename p) && not (test_translations p)= do putStrLn $ unlines ["ERROR: No input specified.","Run with --help for usage options"] + return False + | translate p && (allTransitive p || allReflexive p) = + do putStrLn $ unlines ["ERROR: --translate incompatible with --all-transitive or --all-reflexive."] return False | otherwise = return True where notPermutationOf l1 l2 = sort l1 /= sort l2 diff --git a/src/HTab/DMap.hs b/src/HTab/DMap.hs --- a/src/HTab/DMap.hs +++ b/src/HTab/DMap.hs @@ -2,7 +2,7 @@ (DMap, empty, flatten, delete, insert, insertWith, (!), insert1, lookup, lookup1, lookupInter, - moveInnerPlusDeps, moveInnerPlusDeps3 ) + moveInnerPlusDeps ) where @@ -77,21 +77,6 @@ -> let origInnerMapPlusDeps = M.map (addDeps newDeps) origInnerMap prunedM = I.delete origKey m addDeps newBps = map (\(el,oldBps) -> (el,dsUnion newBps oldBps)) - in case I.lookup destKey m of - Nothing -> I.insert destKey origInnerMapPlusDeps prunedM - Just destInnerMap - -> let mergedInnerMap = M.unionWith (++) origInnerMapPlusDeps destInnerMap - in I.insert destKey mergedInnerMap prunedM - -moveInnerPlusDeps3 :: DependencySet -> DMap [(c1,c2,DependencySet)] -> Int -> Int - -> DMap [(c1,c2,DependencySet)] -moveInnerPlusDeps3 newDeps m origKey destKey - = case I.lookup origKey m of - Nothing -> m - Just origInnerMap - -> let origInnerMapPlusDeps = M.map (addDeps newDeps) origInnerMap - prunedM = I.delete origKey m - addDeps newBps = map (\(el1,el2,oldBps) -> (el1,el2,dsUnion newBps oldBps)) in case I.lookup destKey m of Nothing -> I.insert destKey origInnerMapPlusDeps prunedM Just destInnerMap diff --git a/src/HTab/Formula.hs b/src/HTab/Formula.hs --- a/src/HTab/Formula.hs +++ b/src/HTab/Formula.hs @@ -1,7 +1,7 @@ module HTab.Formula (Nom, Prop, Rel, Prefix, Formula(..), Literal(..), Atom(..), -DependencySet, Dependency, Depth, +DependencySet, Dependency, dsUnion, dsUnions, dsInsert, dsMember, dsEmpty, dsMin, dsShow, addDeps, PrFormula(..),showLess, @@ -14,18 +14,17 @@ showRelInfo, negLit, encodeValidityTest, encodeSatTest, encodeRetrieveTask, HyLoFormula, RelProperty(..), -isPositiveNom, isPositiveProp, isProp -,parseGenerators,Generator,applyGenerators +isPositiveNom, isPositiveProp, isProp, list, imp, +trSab, trSwap, trBri, emptyset ) where -import Debug.Trace import qualified Data.Set as Set import Data.Set ( Set ) import qualified Data.Map as Map import Data.Map ( Map ) import qualified Data.IntSet as IntSet -import Data.List ( delete, nub, intercalate, isPrefixOf ) +import Data.List ( delete, nub, intercalate ) import Data.Char ( toUpper ) @@ -86,8 +85,8 @@ show (At n f) = n ++ ":(" ++ show f ++ ")" show (Box r f) = "[" ++ r ++ "]" ++ show f show (Dia r f) = "<" ++ r ++ ">" ++ show f - show (A f) = "A" ++ show f - show (E f) = "E" ++ show f + show (A f) = "A " ++ show f + show (E f) = "E " ++ show f show (Down n f) = "down " ++ n ++ "." ++ show f -- parsing of the input file @@ -107,13 +106,19 @@ showRelInfo :: RelInfo -> String showRelInfo = Map.foldrWithKey (\r v -> (++ " " ++ show r ++ " -> " ++ show v )) "" +data RelationChanging = Sabotage | Bridge | Swap + parse :: Params -> String -> (Theory,RelInfo,LanguageInfo,[Task]) parse p s = (theory, relInfo, fLang, tasks) where parseOutput = InputFile.myparse s -- direct parse from hylolib pRelInfo = P.relations parseOutput - relInfo = forceProperties p parseOutput $ convertToOurType pRelInfo - theory = convert relInfo $ P.theory parseOutput + relInfo = if translate p + then monomodal $ convertToOurType pRelInfo + else forceProperties p parseOutput $ convertToOurType pRelInfo + theory = if translate p + then doTranslate (detectRCLogic pRelInfo) $ P.theory parseOutput + else convert relInfo $ P.theory parseOutput tasks = P.tasks parseOutput fLang = langInfo parseOutput @@ -131,7 +136,25 @@ (allReflexive p, Reflexive )] theory = P.theory po +-- assume input formula is relation-changing +-- then it is monomodal, only relation is R +monomodal :: RelInfo -> RelInfo +monomodal _ = Map.fromList [("R", [])] + -- TODO check parameter and fail if relation other than R used in input file + +detectRCLogic :: PRelInfo -> RelationChanging +detectRCLogic prelI + | "sb" `elem` rels = Sabotage + | "gsb" `elem` rels = Sabotage + | "sw" `elem` rels = Swap + | "gsw" `elem` rels = Swap + | "br" `elem` rels = Bridge + | "gbr" `elem` rels = Bridge + | otherwise = error "does not seem like a relation-changing formula!" + where rels = map fst prelI + + convertToOurType :: PRelInfo -> RelInfo -- and add for each relation in the formula, the relevant key convertToOurType prelI = foldr insertRelProp Map.empty (concatMap convertOne prelI) @@ -157,6 +180,7 @@ in (t,r,i) where removeBeginEnd = unwords . delete "begin" . delete "end" . words +-- convert from hylolib format to htab's convert :: RelInfo -> [F.Formula S.NomSymbol S.PropSymbol S.RelSymbol] -> Formula convert relI = conv_ relI . foldr (F.:&:) F.Top @@ -195,6 +219,153 @@ | otherwise = relational r where props = Map.findWithDefault [] r relI + +-- COMMON STRUCTURES FOR ALL RELATION-CHANGING TRANSLATIONS -- +type S = ( [(String, String)] , Int) -- Int = next nominal number to use +emptyset :: S -- directly nominal strings (uppercase) +emptyset = ([],0) +-- generate unused nominal and update S +next :: S -> (String,S) +next (ss,n) = ("N" ++ show n, (ss, n + 1)) + +-- SABOTAGE TRANSLATION -- +-- not exactly a union but we're mimicking the article +union :: S -> (String, String) -> S +union (ss,n) nm = (ss ++ [nm], n) +-- macro for translation +belongs :: String -> S -> Formula +belongs n (ss,_) = foldr disj (neg taut) $ set [ (n' y) `conj` At n (n' x) | (x,y) <- ss ] + where n' = Lit . PosLit . N + +-- SWAP TRANSLATION -- +inverse :: S -> S +inverse (ss,n) = (map (\(a,b) -> (b,a)) ss, n) +-- | slightly different from paper: phi must be already translated +isSat :: S -> Formula -> Formula +isSat (ss,_) phi = foldr disj (neg taut) [ n x `conj` At y phi | (x,y) <- ss ] + where n = Lit . PosLit . N + +-- | swap again some pair in S +again :: S -> (String, String) -> S +again (ss,n) xy@(x,y) + | xy `elem` ss = ( (y,x):(delete xy ss), n) + | otherwise = error "trying to swap again something that is not here" + +doTranslate :: RelationChanging -> [F.Formula S.NomSymbol S.PropSymbol S.RelSymbol] -> Formula +doTranslate rc input = -- TODO detect if sabotage, if bridge, if swap + case rc of + Sabotage -> trSab emptyset bigAnd + Swap -> trSwap emptyset bigAnd + Bridge -> trBri emptyset bigAnd + where bigAnd = convert Map.empty input + +trSab :: S -> Formula -> Formula +trSab _ l@(Lit _) = l +trSab s (Con fs) = Con (Set.map (trSab s) fs) +trSab s (Dis fs) = Dis (Set.map (trSab s) fs) +trSab s (At n f) = At n (trSab s f) +trSab s (Down v f) = Down v (trSab s f) +trSab s (A f) = A (trSab s f) +trSab s (E f) = E (trSab s f) +trSab s (Box r f) = neg $ trSab s (Dia r (neg f)) +trSab s (Dia r f) + | up r `elem` ["R","R1"] = + case s of + ([],_) -> Dia "R" (trSab s1 f) + _ -> Down newNom1 ( Dia "R" ( (neg $ belongs newNom1 s1) `conj` (trSab s1 f))) + | up r == "SB" = + Down newNom1 (Dia "R" ( (neg $ belongs newNom1 s2) `conj` (Down newNom2 (trSab s2u12 f)))) + | up r == "GSB" = + Down newNom1 $ E $ Down newNom2 + $ (Dia "R" ( (neg $ belongs newNom2 s2) `conj` (Down newNom3 $ At newNom1 (trSab s4u23 f)))) + | otherwise = error ("Relation is not r, r1, sb or gsb: " ++ r) + where (newNom1,s1) = next s + (newNom2,s2) = next s1 + s2u12 = s2 `union` (newNom1,newNom2) + (newNom3,s3) = next s2 + s4u23 = s3 `union` (newNom2,newNom3) + +trBri :: S -> Formula -> Formula +trBri _ l@(Lit _) = l +trBri s (Con fs) = Con (Set.map (trBri s) fs) +trBri s (Dis fs) = Dis (Set.map (trBri s) fs) +trBri s (At n f) = At n (trBri s f) +trBri s (Down v f) = Down v (trBri s f) +trBri s (A f) = A (trBri s f) +trBri s (E f) = E (trBri s f) +trBri s (Box r f) = neg $ trBri s (Dia r (neg f)) +trBri s (Dia r f) + | up r `elem` ["R","R1"] = + case s of + ([],_) -> Dia "R" (trBri s1 f) + _ -> Down newNom1 $ E $ Down newNom2 + ( (( At newNom1 (Dia "R" (n newNom2))) `disj` (belongs newNom1 s1)) + `conj` (trBri s2 f) + ) + | up r == "BR" = + Down newNom1 $ E $ Down newNom2 + ( ( neg $ At newNom1 (Dia "R" (n newNom2))) + `conj` (neg $ belongs newNom1 s1) + `conj` (trBri s2u12 f) + ) + | up r == "GBR" = + Down newNom1 $ E $ Down newNom2 $ E $ Down newNom3 + ( ( neg $ At newNom2 (Dia "R" (n newNom3))) + `conj` (neg $ belongs newNom2 s1) + `conj` At newNom1 (trBri s4u23 f) + ) + | otherwise = error ("Relation is not r, r1, br or gbr: " ++ r) + where (newNom1,s1) = next s + (newNom2,s2) = next s1 + s2u12 = s2 `union` (newNom1,newNom2) + (newNom3,s3) = next s2 + s4u23 = s3 `union` (newNom2,newNom3) + n = Lit . PosLit . N + +trSwap :: S -> Formula -> Formula +trSwap _ l@(Lit _) = l +trSwap s (Con fs) = Con (Set.map (trSwap s) fs) +trSwap s (Dis fs) = Dis (Set.map (trSwap s) fs) +trSwap s (At n f) = At n (trSwap s f) +trSwap s (Down v f) = Down v (trSwap s f) +trSwap s (A f) = A (trSwap s f) +trSwap s (E f) = E (trSwap s f) +trSwap s (Box r f) = neg $ trSwap s (Dia r (neg f)) +trSwap s@(ss,_) (Dia r f) + | up r `elem` ["R","R1"] = + case s of + ([],_) -> Dia "R" (trSwap s1 f) + _ -> (Down newNom1 ( Dia "R" ( (neg $ belongs newNom1 s1) `conj` (trSwap s1 f)))) + `disj` + (isSat (inverse s) (trSwap s f)) + | up r == "SW" = + ( Down newNom1 (Dia "R" (n newNom1)) `conj` trSwap s f ) + `disj` + ( Down newNom1 $ Dia "R" + $ neg (n newNom1) + `conj` neg (belongs newNom1 s) + `conj` neg (belongs newNom1 (inverse s)) + `conj` (Down newNom2 $ trSwap s2u12 f)) + `disj` + foldr disj (neg taut) [ n y `conj` At x (trSwap (again s (x,y)) f) | (x,y) <- ss ] + | up r == "GSW" = + ( (E $ Down newNom1 $ Dia "R" $ n newNom1) `conj` trSwap s f ) + `disj` + ( Down newNom1 $ E $ Down newNom2 $ Dia "R" + $ neg (n newNom2) + `conj` neg (belongs newNom2 s) + `conj` neg (belongs newNom2 (inverse s)) + `conj` (Down newNom3 $ At newNom1 $ trSwap s4u23 f)) + `disj` + foldr disj (neg taut) [ trSwap (again s (x,y)) f | (x,y) <- ss ] + | otherwise = error ("Relation is not r, r1, sw or gsw: " ++ r) + where (newNom1,s1) = next s + (newNom2,s2) = next s1 + s2u12 = s2 `union` (newNom1,newNom2) + (newNom3,s3) = next s2 + s4u23 = s3 `union` (newNom2,newNom3) + n = Lit . PosLit . N + type HyLoFormula = F.Formula S.NomSymbol S.PropSymbol S.RelSymbol encodeValidityTest :: RelInfo -> Formula -> [HyLoFormula] -> Formula @@ -309,25 +480,23 @@ -- prefixed formula -type Depth = Int -- modal depth of current formula wrt input formula - -data PrFormula = PrFormula Prefix DependencySet Depth Formula +data PrFormula = PrFormula Prefix DependencySet Formula deriving Eq instance Show PrFormula where - show (PrFormula pr ds md f) = show pr ++ ":" ++ dsShow ds ++ ":" ++ show md ++ ":" ++ show f + show (PrFormula pr ds f) = show pr ++ ":" ++ dsShow ds ++ ":" ++ show f showLess :: PrFormula -> String -showLess (PrFormula pr _ md f) = show pr ++ ":" ++ show (md,f) +showLess (PrFormula pr _ f) = show pr ++ ":" ++ show f -prefix :: Prefix -> DependencySet -> Depth -> Set Formula -> [PrFormula] -prefix p bps md fs = [PrFormula p bps md formula|formula <- list fs] +prefix :: Prefix -> DependencySet -> Set Formula -> [PrFormula] +prefix p bps fs = [PrFormula p bps formula|formula <- list fs] firstPrefixedFormula :: Formula -> PrFormula -firstPrefixedFormula = PrFormula 0 dsEmpty 0 +firstPrefixedFormula = PrFormula 0 dsEmpty negPr :: PrFormula -> PrFormula -negPr (PrFormula p ds md f) = PrFormula p ds md (neg f) +negPr (PrFormula p ds f) = PrFormula p ds (neg f) -- formula language @@ -352,7 +521,7 @@ composeMap baseCase g e = case e of Con fs -> Con $ Set.map g fs Dis fs -> Dis $ Set.map g fs - Dia r f -> Dia r (g f) + Dia r f -> Dia r (g f) Box r f -> Box r (g f) At i f -> At i (g f) A f -> A (g f) @@ -374,12 +543,20 @@ type Dependency = Int type DependencySet = IntSet.IntSet + +-- the ordering of prformula's is used in selecting the next formula in the todo list +-- here we select the one that's most promising for backjumping instance Ord PrFormula where - compare (PrFormula pr1 ds1 _ f1) (PrFormula pr2 ds2 _ f2) = - case dsMin ds1 `compare` dsMin ds2 of + compare (PrFormula pr1 ds1 f1) (PrFormula pr2 ds2 f2) = +-- This one seems more performant in many cases: + +-- case dsMin ds1 `compare` dsMin ds2 of + +-- But this one seems 'fairer' and helps termination on some complicated formulas + case IntSet.size ds1 `compare` IntSet.size ds2 of LT -> LT GT -> GT - EQ -> compare (pr1,f1) (pr2,f2) + EQ -> compare (pr1,f1,ds1) (pr2,f2,ds2) dsUnion :: DependencySet -> DependencySet -> DependencySet dsUnion = IntSet.union @@ -403,7 +580,7 @@ dsShow = show . IntSet.toList addDeps :: DependencySet -> PrFormula -> PrFormula -addDeps ds1 (PrFormula p ds2 md f) = PrFormula p (dsUnion ds1 ds2) md f +addDeps ds1 (PrFormula p ds2 f) = PrFormula p (dsUnion ds1 ds2) f list :: Ord a => Set.Set a -> [a] list = Set.toList @@ -411,68 +588,6 @@ set :: Ord a => [a] -> Set.Set a set = Set.fromList --- symmetries --- substitution of literals inside of formulas - -type Generator = [(Depth,Literal,Literal)] - -applyGenerators :: [Generator] -> PrFormula -> [PrFormula] -applyGenerators gens f - = if null res - then res - else trace ("SYM on " ++ showLess f ++ ":" ++ intercalate "," (map showLess res)) - res - where res = delete f $ nub $ map (\gen -> subst gen f) gens - -subst :: Generator -> PrFormula -> PrFormula -subst gen (PrFormula pr ds md f) = PrFormula pr ds md $ substNorm (normGen gen md) f - -normGen :: Generator -> Depth -> Generator -normGen g md = [(md1-md,a1,a2) | (md1,a1,a2) <- g, md1 - md >= 0] - -substNorm :: Generator -> Formula -> Formula --- act as if we were at modal depth 0 and generator has been adjusted -substNorm gen (Lit a) = Lit $ genOnLit gen a -substNorm gen (At n f) = At n $ substNorm (normGen gen 1) f -substNorm gen (Box r f) = Box r $ substNorm (normGen gen 1) f -substNorm gen (Dia r f) = Dia r $ substNorm (normGen gen 1) f -substNorm gen (Down n f) = Down n $ substNorm (normGen gen 1) f -substNorm gen (A f) = A $ substNorm (normGen gen 1) f -substNorm gen (E f) = E $ substNorm (normGen gen 1) f -substNorm gen f = composeMap id (substNorm gen) f - -genOnLit :: Generator -> Literal -> Literal -genOnLit [] l = l -genOnLit ((d,x,y):g) l - | d == 0 && x == l = y - | d == 0 && x == negLit l = negLit y - | d == 0 && y == l = x - | d == 0 && y == negLit l = negLit x - | otherwise = genOnLit g l - -parseGenerators :: String -> [Generator] -parseGenerators genString - = [lineToGen l [] | l <- lines genString, - not ("%" `isPrefixOf` l), - not (null l) ] - --- turn such a line into a generator: --- 4 -2 5, 5 3 5, 0 -6 -3 -lineToGen :: String -> Generator -> Generator -lineToGen "" g = g -lineToGen (',':l) g = lineToGen l g -lineToGen l g = let triple = takeWhile (/= ',') l - remainder = dropWhile (/= ',') l - [md,l1,l2] = map read $ words triple - -- we read X for PX or -Y for -PY, - -- now we need to convert it in atom - a1 = if l1 < 0 - then NegLit $ P $ "P" ++ show (negate l1) - else PosLit $ P $ "P" ++ show l1 - a2 = if l2 < 0 - then NegLit $ P $ "P" ++ show (negate l2) - else PosLit $ P $ "P" ++ show l2 - in lineToGen remainder (g ++ [(md,a1,a2)]) - up :: String -> String up = map toUpper + diff --git a/src/HTab/Literals.hs b/src/HTab/Literals.hs --- a/src/HTab/Literals.hs +++ b/src/HTab/Literals.hs @@ -1,7 +1,8 @@ module HTab.Literals ( UpdateResult(..), Literals, SlotUpdateResult(..), LiteralSlot, -updateMap, lsUnions, lsAddDeps, lsQuery +updateMap, lsUnions, lsAddDeps, lsQuery, +positiveNom ) where import Data.IntMap ( IntMap) @@ -112,4 +113,10 @@ where dlookup pr_ l_ lits_ = do slot <- I.lookup pr_ lits_ M.lookup l_ slot + +positiveNom :: Literals -> Prefix -> Maybe String +positiveNom lits pr = do slot <- I.lookup pr lits + case filter isPositiveNom (M.keys slot) of + (PosLit (N n):_) -> Just n + _ -> Nothing diff --git a/src/HTab/Main.hs b/src/HTab/Main.hs --- a/src/HTab/Main.hs +++ b/src/HTab/Main.hs @@ -3,27 +3,29 @@ ( runWithParams, TaskRunFlag(..)) where -import Control.Applicative ( (<$>) ) -import Control.Monad ( when ) +import Control.Monad ( when, forM_ ) import Control.Monad.State( runStateT ) +import Data.List ( intersperse ) +import qualified Data.Map as Map import System.Console.CmdArgs ( whenNormal, whenLoud ) - import System.CPUTime( getCPUTime ) import qualified System.Timeout as T +import System.Random (StdGen, getStdGen) import System.IO.Strict ( readFile ) import Prelude hiding ( readFile ) import HyLo.InputFile.Parser ( QueryType(..) ) -import HTab.CommandLine( filename, symfile, +import HTab.CommandLine( filename, random, seed, test_translations, timeout, Params, genModel, dotModel, showFormula ) import HTab.Branch( BranchInfo(..), initialBranch) import HTab.Statistics( Statistics, initialStatisticsStateFor, printOutMetricsFinal ) import HTab.Tableau( OpenFlag(..), tableauStart ) -import HTab.Formula( Theory, RelInfo, LanguageInfo, Task, - Formula, encodeValidityTest, encodeSatTest, encodeRetrieveTask, - showRelInfo, parseGenerators ) +import HTab.Formula( Theory, RelInfo, LanguageInfo(..), Task, + Formula(Con), encodeValidityTest, encodeSatTest, encodeRetrieveTask, + showRelInfo, list ) +import HTab.Memory (unsats, sats) import qualified HTab.Formula as F import qualified HyLo.Signature.String as S import HTab.ModelGen ( Model, toDot ) @@ -31,8 +33,41 @@ data TaskRunFlag = SUCCESS | FAILURE runWithParams :: Params -> IO (Maybe TaskRunFlag) +runWithParams p | test_translations p = + do putStrLn "Running memory logic to relation-changing logics test suite." + g <- case seed p of + Nothing -> getStdGen + Just s -> do putStrLn "Using given random seed." + return (read s) + putStrLn "=== UNSAT formulas ===" + forM_ (zip [1::Int ..] unsats) $ \(i,(mf,rc,h,name)) -> + do myPutStrLn (show i ++ " " ++ show mf ++ " via " ++ name) + r <- inTimeout (timeout p) $ + do (result,_) <- tableauInit p g $ initialBranch p (LanguageInfo []) Map.empty h + return result + case r of + Nothing -> myPutStrLn "Timeout" + Just (CLOSED _) -> myPutStrLn "OK" + Just (OPEN _) -> myPutStrLn ("ERROR: formula is sat\n" ++ show rc) + putStrLn "=== SAT formulas ===" + forM_ (zip [(length unsats + 1)::Int ..] sats) $ \(i,(mf,rc,h,name)) -> + do myPutStrLn (show i ++ " " ++ show mf ++ " via " ++ name) + r <- inTimeout (timeout p) $ + do (result,_) <- tableauInit p g $ initialBranch p (LanguageInfo []) Map.empty h + return result + case r of + Nothing -> myPutStrLn "Timeout" + Just (OPEN _) -> myPutStrLn "OK" + Just (CLOSED _) -> myPutStrLn ("ERROR: formula is unsat\n" ++ show rc) + return (Just SUCCESS) + runWithParams p = time "Total time: " $ do + g <- case seed p of + Nothing -> getStdGen + Just s -> do putStrLn "Using given random seed." + return (read s) + when (random p) $ putStrLn ( unlines ["Will use random seed:",show g]) i <- readFile (filename p) if head (words i) == "begin" then do @@ -44,11 +79,9 @@ "End of input", "Relations properties :" ++ showRelInfo relInfo ] -- - gs <- parseGenerators <$> maybe (return "") readFile (symfile p) -- read symmetries - -- tResult <- inTimeout (timeout p) $ - do (result,s) <- tableauInit p $ - initialBranch p fLang relInfo gs f + do (result,s) <- tableauInit p g $ + initialBranch p fLang relInfo f whenNormal $ printOutMetricsFinal s return result -- @@ -61,7 +94,7 @@ return (Just FAILURE) else do let allTasks = F.parse p i - result <- inTimeout (timeout p) (runTasks allTasks p) + result <- inTimeout (timeout p) (runTasks allTasks p g) -- case result of Nothing -> myPutStrLn "\nTimeout.\n" @@ -76,42 +109,42 @@ -- -runTasks :: (Theory,RelInfo,LanguageInfo,[Task]) -> Params -> IO TaskRunFlag -runTasks allTasks@(theory,relInfo,fLang,tasks) p = +runTasks :: (Theory,RelInfo,LanguageInfo,[Task]) -> Params -> StdGen -> IO TaskRunFlag +runTasks allTasks@(theory,relInfo,fLang,tasks) p g = do myPutStrLn "== Checking theory satisfiability ==" res <- time "Task time:" $ - runTask (Satisfiable, genModel p, []) relInfo fLang theory p + runTask (Satisfiable, genModel p, []) relInfo fLang theory p g case res of SUCCESS | null tasks -> return SUCCESS | otherwise -> do myPutStrLn "\n== Starting tasks ==" - res2 <- runTasks2 allTasks p + res2 <- runTasks2 allTasks p g myPutStrLn "\n== End of tasks ==" return res2 FAILURE -> return FAILURE -- -runTasks2 :: (Theory,RelInfo,LanguageInfo,[Task]) -> Params -> IO TaskRunFlag -runTasks2 (_,_,_,[]) _ = error "runTasks2 empty list error" -runTasks2 (theory,relInfo,fLang,(hd:tl)) p = - do res <- time "Task time:" $ runTask hd relInfo fLang theory p +runTasks2 :: (Theory,RelInfo,LanguageInfo,[Task]) -> Params -> StdGen -> IO TaskRunFlag +runTasks2 (_,_,_,[]) _ _ = error "runTasks2 empty list error" +runTasks2 (theory,relInfo,fLang,(hd:tl)) p g = + do res <- time "Task time:" $ runTask hd relInfo fLang theory p g case res of SUCCESS | null tl -> return SUCCESS - | otherwise -> runTasks2 (theory,relInfo,fLang,tl) p - FAILURE -> do _ <- runTasks2 (theory,relInfo,fLang,tl) p + | otherwise -> runTasks2 (theory,relInfo,fLang,tl) p g + FAILURE -> do _ <- runTasks2 (theory,relInfo,fLang,tl) p g return FAILURE -- -runTask :: Task -> RelInfo -> LanguageInfo -> Formula -> Params -> IO TaskRunFlag -runTask (Retrieve,mOutFile,fs) relInfo fLang theory p = +runTask :: Task -> RelInfo -> LanguageInfo -> Formula -> Params -> StdGen -> IO TaskRunFlag +runTask (Retrieve,mOutFile,fs) relInfo fLang theory p g = do myPutStrLn "\n* Instance retrieval task" let (noms,encfs) = encodeRetrieveTask relInfo fLang theory fs -- myPutStrLn $ "Instances making true: " ++ show fs -- - results <- mapM (tableauInit p . initialBranch p fLang relInfo []) encfs + results <- mapM (tableauInit p g . initialBranch p fLang relInfo) encfs -- NOTE: we reuse the same random generator let goods = [ S.NomSymbol n | (n,(CLOSED _ ,_)) <- zip noms results] myPutStrLn $ show goods let doWrite f = do writeFile f (show goods ++ "\n") @@ -119,17 +152,20 @@ maybe (return ()) doWrite mOutFile return SUCCESS -runTask (Satisfiable,mOutFile,fs) relInfo fLang theory p = +runTask (Satisfiable,mOutFile,fs) relInfo fLang theory p g = do myPutStrLn "\n* Satisfiability task" let f = encodeSatTest relInfo theory fs -- + let f_lines = case f of + Con cs -> list cs + _ -> [f] when (showFormula p) $ - myPutStrLn $ unlines ["Input for SAT test:", - "{ " ++ show f ++ " }", - "End of input", + myPutStrLn $ unlines $ ["Input for SAT test:", + "{"] ++ intersperse "" (map show f_lines) ++ + ["}", "End of input", "Relations properties :" ++ showRelInfo relInfo ] -- - (result,stats) <- tableauInit p $ initialBranch p fLang relInfo [] f + (result,stats) <- tableauInit p g $ initialBranch p fLang relInfo f -- whenNormal $ printOutMetricsFinal stats -- @@ -140,7 +176,7 @@ CLOSED _ -> do myPutStrLn "The formula is unsatisfiable." return FAILURE -runTask (Valid,mOutFile,fs) relInfo fLang theory p = +runTask (Valid,mOutFile,fs) relInfo fLang theory p g = do myPutStrLn "\n* Validity task" let f = encodeValidityTest relInfo theory fs -- @@ -150,7 +186,7 @@ "End of input", "Relations properties :" ++ showRelInfo relInfo ] -- - (result,stats) <- tableauInit p $ initialBranch p fLang relInfo [] f + (result,stats) <- tableauInit p g $ initialBranch p fLang relInfo f -- whenNormal $ printOutMetricsFinal stats -- @@ -161,7 +197,7 @@ CLOSED _ -> do myPutStrLn "The formula is valid." return SUCCESS -runTask (Counting,_,_) _ _ _ _ = +runTask (Counting,_,_) _ _ _ _ _ = do myPutStrLn "\n* Counting task is NOT supported" return FAILURE @@ -174,11 +210,11 @@ output | dotModel p = toDot m | otherwise = show m -tableauInit :: Params -> BranchInfo -> IO (OpenFlag,Statistics) -tableauInit p bi = +tableauInit :: Params -> StdGen -> BranchInfo -> IO (OpenFlag,Statistics) +tableauInit p g bi = do whenLoud $ putStrLn ">> Starting rules application" initStatsState $ tableauStart p bi - where initStatsState = initialStatisticsStateFor runStateT + where initStatsState = initialStatisticsStateFor runStateT g -- diff --git a/src/HTab/Memory.hs b/src/HTab/Memory.hs new file mode 100644 --- /dev/null +++ b/src/HTab/Memory.hs @@ -0,0 +1,232 @@ +module HTab.Memory ( sats, unsats ) +where + +import qualified Data.Set as Set +import HTab.Formula + +data MemFormula + = MLit Literal + | MCon MemFormula MemFormula + | MDis MemFormula MemFormula + | MBox MemFormula + | MDia MemFormula + | MNeg MemFormula + | Re MemFormula -- ^ Remember + | Kn -- ^ Known + deriving (Eq, Ord ) + +instance Show MemFormula where + show (MLit a) = show a + show (MCon f1 f2) = "(" ++ show f1 ++ " & " ++ show f2 ++ ")" + show (MDis f1 f2) = "(" ++ show f1 ++ " v " ++ show f2 ++ ")" + show (MBox f) = "[](" ++ show f ++ ")" + show (MDia f) = "<>(" ++ show f ++ ")" + show (MNeg f) = "¬(" ++ show f ++ ")" + show (Re f) = "Re(" ++ show f ++ ")" + show Kn = "Kn" + +mtop, mbot :: MemFormula +mtop = MLit $ PosLit Taut +mbot = MLit $ NegLit Taut + +-- unsat memory logic formulas +kn, re1, re2, re3 :: MemFormula +kn = Kn +re1 = (MLit (PosLit (P "P"))) `MCon` (Re (MLit (NegLit (P "P")))) +re2 = (MBox mbot) `MCon` (Re (MDia mtop)) +re3 = (MDia mbot) `MCon` (Re (MBox mtop)) +-- bury these unsat formulas in sufficiently deep diamonds +unsats_mem :: [MemFormula] +unsats_mem = concat [ nested f | f <- [kn, re1, re2, re3] ] + +-- (interesting) SAT memory logic formulas +rekn1, rekn2, rekn3, rekn4, chain4 :: MemFormula +rekn1 = Re (MDia Kn `MCon` MBox Kn) -- (r)( <>(k) & [](k) ) +rekn2 = MNeg Kn -- !(k) +rekn3 = Re ( MDia (MNeg Kn)) -- (r)<>!(k) +rekn4 = Re (MDia Kn `MCon` MDia (MNeg Kn)) -- (r)( <>(k) & <>!(k) ) +chain4 = c [ p "a", q "b", q "c", q "d", MDia + (c [ q "a", p "b", q "c", q "d", MDia + (c [ q "a", q "b", p "c", q "d", MDia + (c [ q "a", q "b", q "c", p "d"])])])] + where p = MLit . PosLit . P + q = MLit . NegLit . P + c = foldr1 MCon + +sats_mem :: [MemFormula] +sats_mem = chain4 : concat [ nested f | f <- [rekn1, rekn2, rekn3, rekn4]] + +nested :: MemFormula -> [MemFormula] +nested f = [f, MDia f, MDia $ MDia f, MDia $ MDia $ MDia f] + +-- test suite for translations Memory Logic -> Relation-Changing logics +unsats, sats :: [(MemFormula, Formula,Formula,String)] +unsats = concatMap memToHybrid unsats_mem -- all of them should be found UNSAT +sats = concatMap memToHybrid sats_mem -- all of them should be found SAT + +-- given a memory logic formula, translate it to the 6 relation-changing logics + translate again to hybrid logic +memToHybrid :: MemFormula -> [(MemFormula,Formula,Formula,String)] +memToHybrid f = map (\(rcTr, hTr,name) -> (f, rcTr f, hTr (rcTr f), name)) + [ (memGSb, trSab emptyset, "Global Sabotage") + , (memGSw, trSwap emptyset, "Global Swap") + , (memGBr, trBri emptyset, "Global Bridge") + , (memLBr, trBri emptyset, "Local Bridge") + , (memLSw, trSwap emptyset, "Local Swap") + , (memLSb, trSab emptyset, "Local Sabotage") ] + +-- ^ translate a memory logic formula into a global sabotage +-- formula where modalities are R and GSB +memGSb :: MemFormula -> Formula +memGSb f_ = struct (mmd f_) `conj` go f_ + where + struct n = foldr conj neg_s [ nestBox i (neg_s `imp` Dia "R" s) | i <- [0..n]] + + go (Kn) = neg (Dia "R" s) + go (Re f) = Dia "GSB" ( (neg (Dia "R" s)) `conj` go f) + go (MDia f) = Dia "R" (neg_s `conj` go f) + go (MBox f) = Box "R" (neg_s `imp` go f) + go (MCon f g) = (go f) `conj` (go g) + go (MDis f g) = (go f) `disj` (go g) + go (MLit l) = Lit l + go (MNeg f) = neg (go f) + +memGSw :: MemFormula -> Formula +memGSw f_ = struct (mmd f_) `conj` go f_ + where + struct n = foldr conj neg_s [ nestBox i (neg_s `imp` Dia "R" s) | i <- [0..n]] + + go (Kn) = neg (Dia "R" s) + go (Re f) = Dia "GSW" ( (neg (Dia "R" s)) `conj` go f) + go (MDia f) = Dia "R" (neg_s `conj` go f) + go (MBox f) = Box "R" (neg_s `imp` go f) + go (MCon f g) = (go f) `conj` (go g) + go (MDis f g) = (go f) `disj` (go g) + go (MLit l) = Lit l + go (MNeg f) = neg (go f) + +memGBr :: MemFormula -> Formula +memGBr f_ = struct (mmd f_) `conj` go f_ + where + struct n = foldr conj taut [ nestBox i neg_s | i <- [0..(n+1)]] + + go (Kn) = Dia "R" s + go (Re f) = Dia "GBR" ( (Dia "R" s) `conj` go f) + go (MDia f) = Dia "R" (neg_s `conj` go f) + go (MBox f) = Box "R" (neg_s `imp` go f) + go (MCon f g) = (go f) `conj` (go g) + go (MDis f g) = (go f) `disj` (go g) + go (MLit l) = Lit l + go (MNeg f) = neg (go f) + +memLSw :: MemFormula -> Formula +memLSw f_ = struct `conj` d (go f_) + where + struct = Con $ set + [ s + , b neg_s + , b (neg_s `imp` uniq) + , b $ b (neg_s `imp` uniq) + , b $ b $ b (neg_s `imp` uniq) + , b $ bsw (s `imp` (b $ b $ b (s `imp` b (neg taut)))) + , b $ b $ bsw (s `imp` (b $ b $ b (s `imp` b (neg taut)))) + , bsw $ bsw ( neg_s `imp` dsw ( s `conj` (d (b neg_s `imp` (d $ d (s `conj` d(b(neg_s)))))))) + ] + + go (MDia f) = Dia "R" (neg_s `conj` go f) + go (MBox f) = Box "R" (neg_s `imp` go f) + go (MCon f g) = (go f) `conj` (go g) + go (MDis f g) = (go f) `disj` (go g) + go (MLit l) = Lit l + go (MNeg f) = neg (go f) + go (Kn) = neg (d s) + go (Re f) = dsw (s `conj` d (go f)) + + uniq = (d (s `conj` (b (neg taut)))) + `conj` bsw (s `imp` b (b neg_s)) + bsw = Box "SW" + dsw = Dia "SW" + +memLBr :: MemFormula -> Formula +memLBr f_ = struct `conj` dbr(neg_s `conj` t `conj` dbr(neg_s `conj` neg_t `conj` go f_)) + where + struct = Con $ set + [ s + , b (neg taut) + , bbr (s `imp` bbr neg_s) + , bbr (neg_s `imp` b neg_s) + ] + + go (MDia f) = Dia "R" (neg_s_and_neg_t `conj` go f) + go (MBox f) = Box "R" (neg_s_and_neg_t `imp` go f) + go (MCon f g) = (go f) `conj` (go g) + go (MDis f g) = (go f) `disj` (go g) + go (MLit l) = Lit l + go (MNeg f) = neg (go f) + go (Kn) = d s + go (Re f) = dbr( s `conj` dbr ( neg_s `conj` (d s) `conj` (go f))) + + t = Lit (PosLit (P "T")) + neg_t = Lit (NegLit (P "T")) + neg_s_and_neg_t = neg_s `conj` neg_t + dbr = Dia "BR" + bbr = Box "BR" + +memLSb :: MemFormula -> Formula +memLSb f_ = struct `conj` d (go f_) + where + struct = Con $ set + [ s + , b neg_s + , b $ d s + , bsb ( bsb ( s `imp` b (d s))) + , b ( bsb ( s `imp` d (b neg_s ))) + , b ( b ( neg_s `imp` d s)) + + + , b ( bsb ( s `imp` ( bsb ( (b neg_s) `imp` (b ( b ( s `imp` b (d s)))))))) + , b ( bsb ( s `imp` ( b ( (b neg_s) `imp` (b ( b ( s `imp` d (b neg_s)))))))) + , b ( b ( neg_s `imp`( s `imp` d ( b neg_s)))) + + ] + + go (MDia f) = Dia "R" (neg_s `conj` go f) + go (MBox f) = Box "R" (neg_s `imp` go f) + go (MCon f g) = (go f) `conj` (go g) + go (MDis f g) = (go f) `disj` (go g) + go (MLit l) = Lit l + go (MNeg f) = neg (go f) + go (Kn) = neg (d s) + go (Re f) = dsb( s `conj` dsb ( neg (d s) `conj` go f)) + + dsb = Dia "SB" + bsb = Box "SB" + + +-- helper functions + +-- ^ Modal depth of a memory logic formula +mmd :: MemFormula -> Int +mmd Kn = 0 +mmd (MLit _ ) = 0 +mmd (MBox f) = 1 + mmd f +mmd (MDia f) = 1 + mmd f +mmd (MDis f g) = max (mmd f) (mmd g) +mmd (MCon f g) = max (mmd f) (mmd g) +mmd (MNeg f) = mmd f +mmd (Re f) = mmd f + +nestBox :: Int -> Formula -> Formula +nestBox 0 f = f +nestBox n f = nestBox (n-1) (Box "R" f) + +s, neg_s :: Formula +neg_s = Lit (NegLit (P "S")) +s = Lit (PosLit (P "S")) + +set :: Ord a => [a] -> Set.Set a +set = Set.fromList + +d, b :: Formula -> Formula +d = Dia "R" +b = Box "R" + diff --git a/src/HTab/ModelGen.hs b/src/HTab/ModelGen.hs --- a/src/HTab/ModelGen.hs +++ b/src/HTab/ModelGen.hs @@ -43,7 +43,7 @@ [ (pr, r, pr2) | pr <- prefixes br, isInTheModel br pr, - blockedDia@(PrFormula _ _ _ (Dia r _)) <- get [] pr (blockedDias br), + blockedDia@(PrFormula _ _ (Dia r _)) <- get [] pr (blockedDias br), let pat = patternOf br blockedDia, let pr2 = findByPattern br pat ] rels = (allRels $ accStr br) ++ pbBlocked diff --git a/src/HTab/Rules.hs b/src/HTab/Rules.hs --- a/src/HTab/Rules.hs +++ b/src/HTab/Rules.hs @@ -4,6 +4,10 @@ applicableRule, applyRule, ruleToId ) where +import System.Random + +import qualified Data.Map as Map + import qualified Data.Set as Set import Data.Maybe ( mapMaybe ) @@ -20,6 +24,7 @@ addDownRuleCheck, doLazyBranching, getUrfatherAndDeps, merge, + isNominalUrfather, positiveNomOf, -- for choosing rule in todo list patternBlocked, diaAlreadyDone, downAlreadyDone, @@ -29,19 +34,20 @@ ) import HTab.CommandLine(Params, UnitProp(..), lazyBranching, semBranch, unitProp, - strategy) + strategy, minimal) +import qualified HTab.CommandLine as CL ( random ) import HTab.RuleId(RuleId(..)) import qualified HTab.DisjSet as DS -- rule constructors contain the data needed to modify a branch -data Rule = DiaRule PrFormula -- creates a prefix +data Rule = DiaRule PrFormula Dependency -- creates a prefix + | ExistRule PrFormula Dependency -- creates a prefix | DisjRule PrFormula [PrFormula] | SemBrRule PrFormula [PrFormula] | LazyBrRule PrFormula Prefix Literal [PrFormula] | AtRule PrFormula | DownRule PrFormula - | ExistRule PrFormula -- creates a prefix | DiscardDownRule PrFormula | DiscardDiaDoneRule PrFormula | DiscardDiaBlockedRule PrFormula @@ -53,12 +59,12 @@ instance Show Rule where show (MergeRule pr n _) = "merge: " ++ show (pr, show n) - show (DiaRule todelete) = "diamond: " ++ showLess todelete + show (DiaRule todelete _ ) = "diamond: " ++ showLess todelete show (DisjRule todelete _ ) = "disjunction: " ++ showLess todelete show (SemBrRule todelete _ ) = "semantic branching: " ++ showLess todelete show (AtRule todelete ) = "at: " ++ showLess todelete show (DownRule todelete ) = "down: " ++ showLess todelete - show (ExistRule todelete ) = "E: " ++ showLess todelete + show (ExistRule todelete _ ) = "E: " ++ showLess todelete show (DiscardDownRule todelete) = "Discard: " ++ showLess todelete show (DiscardDiaDoneRule todelete) = "Discard done: " ++ showLess todelete @@ -73,12 +79,12 @@ ruleToId :: Rule -> RuleId ruleToId r = case r of (MergeRule _ _ _) -> R_Merge - (DiaRule _ ) -> R_Dia + (DiaRule _ _) -> R_Dia (DisjRule _ _) -> R_Disj (SemBrRule _ _) -> R_SemBr (AtRule _ ) -> R_At (DownRule _) -> R_Down - (ExistRule _) -> R_Exist + (ExistRule _ _) -> R_Exist (DiscardDownRule _) -> R_DiscardDown (DiscardDiaDoneRule _) -> R_DiscardDiaDone (DiscardDiaBlockedRule _) -> R_DiscardDiaBlocked @@ -89,14 +95,14 @@ -- the rules application strategy is defined here: -- the first rule is the one that will be applied at the next tableau step -applicableRule :: Branch -> Params -> Dependency -> Maybe (Rule,Branch) -applicableRule br p d = - case mapMaybe (ruleByChar br p d) (strategy p) of +applicableRule :: Branch -> Params -> Dependency -> StdGen -> Maybe (Rule,Branch, StdGen) +applicableRule br p d g = + case mapMaybe (ruleByChar br p d g) (strategy p) of -- TODO weird to use the same g, but right after we only take the first rule [] -> Nothing - ((rule,newtodo):_) -> Just (rule,br{todoList = newtodo}) + ((rule,newtodo,g'):_) -> Just (rule, br{todoList = newtodo}, g') -ruleByChar :: Branch -> Params -> Dependency -> Char -> Maybe (Rule,TodoList) -ruleByChar br p d char = +ruleByChar :: Branch -> Params -> Dependency -> StdGen -> Char -> Maybe (Rule,TodoList, StdGen) +ruleByChar br p d g char = case char of 'n' -> applicableMergeRule '|' -> applicableDisjRule @@ -112,51 +118,62 @@ applicableDiaRule = do (f,new) <- Set.minView $ diaTodo todos if diaAlreadyDone br f - then return ( DiscardDiaDoneRule f, todos{diaTodo = new}) + then return ( DiscardDiaDoneRule f, todos{diaTodo = new}, g) else if patternBlocked br f - then return ( DiscardDiaBlockedRule f, todos{diaTodo = new}) - else return ( DiaRule f, todos{diaTodo = new}) + then return ( DiscardDiaBlockedRule f, todos{diaTodo = new}, g) + else return ( DiaRule f d, todos{diaTodo = new}, g) applicableAtRule = do (f,new) <- Set.minView $ atTodo todos - return (AtRule f, todos{atTodo = new}) + return (AtRule f, todos{atTodo = new}, g) + applicableDownRule = do (f,new) <- Set.minView $ downTodo todos if downAlreadyDone br f - then return (DiscardDownRule f, todos{downTodo = new}) - else return (DownRule f, todos{downTodo = new}) + then return (DiscardDownRule f, todos{downTodo = new}, g) + else return (DownRule f, todos{downTodo = new}, g) + applicableExistRule = do (f,new) <- Set.minView $ existTodo todos - return (ExistRule f, todos{existTodo = new}) + return (ExistRule f d, todos{existTodo = new}, g) applicableRoleIncRule = do ((ds, p1, p2, rs),new) <- Set.minView $ roleIncTodo todos - return (RoleIncRule p1 rs p2 (dsInsert d ds), todos{roleIncTodo = new}) + return (RoleIncRule p1 rs p2 (dsInsert d ds), todos{roleIncTodo = new}, g) + applicableMergeRule = do ((ds,pr,n),new) <- Set.minView $ mergeTodo todos - return (MergeRule pr n ds, todos{mergeTodo = new}) + return (MergeRule pr n ds, todos{mergeTodo = new}, g) applicableDisjRule = case unitProp p of Eager -> {- scan all disjuncts until one can be discarded, reduced to one disjunct or clashes -} case mapMaybe (makeInteresting p br d) $ Set.toList $ disjTodo todos of - ((r,pf):_) -> return (r, todos{disjTodo = Set.delete pf $ disjTodo todos}) + ((r,pf):_) -> return (r, todos{disjTodo = Set.delete pf $ disjTodo todos}, g) [] -> regularApplicableDisjRule -- todo: update counter (CurCount, MaxCount) step 10 -- to space out unit propagation lookup _ -> regularApplicableDisjRule regularApplicableDisjRule - = do (f,new) <- Set.minView $ disjTodo todos - return (disjRule p f br d, todos{disjTodo = new}) + | not (CL.random p) + = do (f,new) <- Set.minView $ disjTodo todos + return (disjRule p f br d, todos{disjTodo = new}, g) + | otherwise + = if Set.null s then Nothing + else let (n, g') = randomR (0, Set.size s - 1) g + f = Set.elemAt n s -- pick formula + new = Set.deleteAt n s -- remove from Set + in Just (disjRule p f br d, todos{disjTodo = new}, g') + where s = disjTodo todos makeInteresting :: Params -> Branch -> Dependency -> PrFormula -> Maybe (Rule,PrFormula) -makeInteresting p br d df@(PrFormula pr ds md (Dis fs)) +makeInteresting p br d df@(PrFormula pr ds (Dis fs)) = case reduceDisjunctionProposeLazy br pr fs of Triviality -> Just (DiscardDisjTrivialRule df,df) Contradiction ds_clash -> Just (ClashDisjRule (dsUnion ds ds_clash) df,df) Reduced new_ds disjuncts mProposed | Set.size disjuncts == 1 - -> Just (DisjRule df ( prefix ur newDeps md disjuncts ), df) + -> Just (DisjRule df ( prefix ur newDeps disjuncts ), df) | lazyBranching p -> case mProposed of Nothing -> Nothing Just lit - -> Just (LazyBrRule df ur lit [PrFormula ur newDeps md (Dis disjuncts)], + -> Just (LazyBrRule df ur lit [PrFormula ur newDeps (Dis disjuncts)], df) | otherwise -> Nothing where newDeps = dsInsert d $ dsUnion ds new_ds @@ -172,60 +189,106 @@ clash@(BranchClash _ _ _ _) >>? _ = clash (BranchOK br) >>? f = f br -applyRule :: Params -> Rule -> Branch -> [BranchInfo] -applyRule p rule br +applyRule :: Params -> Rule -> Branch -> StdGen -> ([BranchInfo], StdGen) +applyRule p rule br g = case rule of - DiaRule (PrFormula pr ds md (Dia r f)) - -> [ createNewNode p br >>? - addAccFormula p (dsUnion ds ds2, r, ur, newPr) >>? - addFormulas p [PrFormula newPr ds (md+1) f] >>? - addDiaRuleCheck pr (r,f) newPr ] - where newPr = lastPref br + 1 + DiaRule (PrFormula pr ds (Dia r f)) d -- here, if minimal, branch on all prefixes + | minimal p -> if CL.random p then shuffle g choices else (choices, g) + | otherwise -> (properNewBranch, g) + where + tryAllPrefixes = map reusePrefix $ filter (isNominalUrfather br) [0..lastPref br] + reusePrefix pr' = + addAccFormula p (dsInsert d (dsUnion ds ds2), r, ur, pr') br >>? + addFormulas p [PrFormula pr' (dsInsert d ds) f] >>? + addDiaRuleCheck pr (r,f) pr' + properNewBranch = + [ createNewNode p br >>? + addAccFormula p (deps, r, ur, newPr) >>? + addFormulas p [PrFormula newPr ds f] >>? + addDiaRuleCheck pr (r,f) newPr + ] + deps = if CL.random p && minimal p then dsInsert d (dsUnion ds ds2) else dsUnion ds ds2 + choices = tryAllPrefixes ++ properNewBranch + newPr = lastPref br + 1 (ur,ds2,_) = getUrfatherAndDeps br (DS.Prefix pr) - DisjRule _ prFormulas -> - [ addFormulas p [toadd] br | toadd <- prFormulas ] - SemBrRule _ prFormulas -> - [ addFormulas p toadds br | toadds <- go prFormulas [] ] + ExistRule (PrFormula _ ds (E f2)) d -- here, if minimal, branch on all prefixes + | minimal p -> if CL.random p then shuffle g choices else (choices, g) + | otherwise -> (properNewBranch, g) + where + tryAllPrefixes = map reusePrefix $ filter (isNominalUrfather br) [0..lastPref br] + reusePrefix pr' = addFormulas p [PrFormula pr' (dsInsert d ds) f2] br + properNewBranch = [createNewNode p br >>? addFormulas p [PrFormula newPr deps f2]] + deps = if CL.random p && minimal p then dsInsert d ds else ds + choices = tryAllPrefixes ++ properNewBranch + newPr = lastPref br + 1 + + DisjRule _ prFormulas + | CL.random p -> shuffle g choices + | otherwise -> (choices, g) + where choices = [ addFormulas p [toadd] br | toadd <- prFormulas ] + SemBrRule _ prFormulas + | CL.random p -> shuffle g choices + | otherwise -> (choices, g) where + choices = [ addFormulas p toadds br | toadds <- go prFormulas [] ] go (hd:tl) negs = (hd:negs):(go tl (negPr hd:negs)) go [] _ = [] LazyBrRule _ pr lit prFormulas -> - [ doLazyBranching pr lit prFormulas br ] - AtRule (PrFormula _ ds md (At n f)) -> - [ addFormulas p [toadd] br{ nomPrefClasses = equiv }] + ([ doLazyBranching pr lit prFormulas br ], g) + AtRule (PrFormula _ ds (At n f)) -> + ([ addFormulas p [toadd] br{ nomPrefClasses = equiv }], g) where (ur,ds2,equiv) = getUrfatherAndDeps br (DS.Nominal n) - toadd = PrFormula ur (dsUnion ds ds2) (md+1) f - DownRule (PrFormula pr ds md f@(Down v f2)) -> - [ createNewNom br >>? - addFormulas p [toadd1, toadd2] >>? - addDownRuleCheck pr f ] - where toadd1 = PrFormula pr ds (md+1) (replaceVar v newNom f2) - toadd2 = PrFormula pr ds (md+1) $ Lit $ PosLit $ N newNom - newNom = '_':(show $ nextNom br) - ExistRule (PrFormula _ ds md (E f2)) -> - [createNewNode p br >>? addFormulas p [toadd]] - where toadd = PrFormula newPr ds (md+1) f2 - newPr = lastPref br + 1 - DiscardDownRule _ -> [BranchOK br] - DiscardDiaDoneRule _ -> [BranchOK br] - DiscardDisjTrivialRule _ -> [BranchOK br] - DiscardDiaBlockedRule f -> [addToBlockedDias f br] + toadd = PrFormula ur (dsUnion ds ds2) f + DownRule (PrFormula pr ds f@(Down v f2)) -> + case positiveNomOf br pr of -- reuse positive nominal if we can + Nothing -> ( [ createNewNom br >>? + addFormulas p [toadd1, toadd2] >>? + addDownRuleCheck pr f ], g) + where toadd1 = PrFormula pr ds (replaceVar v newNom f2) + toadd2 = PrFormula pr ds $ Lit $ PosLit $ N newNom + newNom = '_':(show $ nextNom br) + Just n' -> + ( [ addFormulas p [PrFormula pr ds (replaceVar v n' f2)] br >>? + addDownRuleCheck pr f ], g) + DiscardDownRule _ -> ([BranchOK br], g) + DiscardDiaDoneRule _ -> ([BranchOK br], g) + DiscardDisjTrivialRule _ -> ([BranchOK br], g) + DiscardDiaBlockedRule f -> ([addToBlockedDias f br], g) - ClashDisjRule ds (PrFormula pr ds2 _ f) -> [BranchClash br pr (dsUnion ds ds2) f] - MergeRule pr n ds -> [merge p pr ds n br] + ClashDisjRule ds (PrFormula pr ds2 f) -> ([BranchClash br pr (dsUnion ds ds2) f], g) + MergeRule pr n ds -> ([merge p pr ds n br], g) RoleIncRule p1 rs p2 ds -> - [addAccFormula p (ds, r, p1, p2) br | r <- rs] + ([addAccFormula p (ds, r, p1, p2) br | r <- rs], g) _ -> error $ "applyRule with bad argument: " ++ show rule disjRule :: Params -> PrFormula -> Branch -> Dependency -> Rule -disjRule p df@(PrFormula pr ds md (Dis fs)) br d +disjRule p df@(PrFormula pr ds (Dis fs)) br d = if unitProp p == UPNo - then rule df $ prefix pr (dsInsert d ds) md fs + then rule df $ prefix pr (dsInsert d ds) fs else case reduceDisjunctionProposeLazy br pr fs of Triviality -> DiscardDisjTrivialRule df Contradiction ds_clash -> ClashDisjRule (dsUnion ds ds_clash) df Reduced new_ds disjuncts _ - -> rule df (prefix pr (dsInsert d $ dsUnion ds new_ds) md disjuncts) + -> rule df (prefix pr (dsInsert d $ dsUnion ds new_ds) disjuncts) where rule = if semBranch p then SemBrRule else DisjRule -- todo: if only one conjunct remaining, do not add d , but still create a DisjRule disjRule _ _ _ _ = error "disjRule" + + +-- list shuffler +-- http://okmij.org/ftp/Haskell/perfect-shuffle.txt + +fisherYatesStep :: RandomGen g => (Map.Map Int a, g) -> (Int, a) -> (Map.Map Int a, g) +fisherYatesStep (m, gen) (i, x) = ((Map.insert j x . Map.insert i (m Map.! j)) m, gen') + where + (j, gen') = randomR (0, i) gen + +shuffle :: RandomGen g => g -> [a] -> ([a], g) +shuffle gen [] = ([], gen) +shuffle gen l = + toElems $ foldl fisherYatesStep (initial (head l) gen) (numerate (tail l)) + where + toElems (x, y) = (Map.elems x, y) + numerate = zip [1..] + initial x gen' = (Map.singleton 0 x, gen') + diff --git a/src/HTab/Statistics.hs b/src/HTab/Statistics.hs --- a/src/HTab/Statistics.hs +++ b/src/HTab/Statistics.hs @@ -21,7 +21,7 @@ -} module HTab.Statistics -( Statistics, StatisticsState, StatisticsStateIO, +( Statistics(..), StatisticsState, StatisticsStateIO, recordFiredRule, recordClosedBranch, printOutMetricsFinal, printOutMetrics, @@ -39,6 +39,8 @@ import qualified Control.Monad.State as State(liftIO) import Control.DeepSeq ( NFData, rnf ) +import System.Random + import Data.Map(Map) import qualified Data.Map as Map(insertWith, toList, empty) import Data.List ( intercalate ) @@ -47,10 +49,11 @@ data Statistics = Stat{metrics::[Metric], count::Int, - step::Int} + step::Int, + rGen::StdGen} instance NFData Statistics where - rnf (Stat sM sC sS) = rnf sM `seq` rnf sC `seq` rnf sS + rnf (Stat sM sC sS _) = rnf sM `seq` rnf sC `seq` rnf sS type StatisticsState a = forall m. (MonadState Statistics m) => m a type StatisticsStateIO a = forall m. (MonadState Statistics m, MonadIO m) => m a @@ -61,23 +64,23 @@ rnf s `seq` s updateStep :: Statistics -> Statistics -updateStep s@(Stat _ _ 0) = s +updateStep s@(Stat _ _ 0 _) = s updateStep stat = stat{count = count stat + 1} needsToPrintOut :: Statistics -> Bool -needsToPrintOut (Stat _ _ 0) = False -needsToPrintOut (Stat _ iter toi) = iter > 0 && iter `mod` toi == 0 +needsToPrintOut (Stat _ _ 0 _) = False +needsToPrintOut (Stat _ iter toi _) = iter > 0 && iter `mod` toi == 0 -defaultStats :: Statistics -defaultStats = Stat{metrics=[closedBranches, ruleApplicationCount], - count=0, step=0} +defaultStats :: StdGen -> Statistics +defaultStats g = Stat{metrics=[closedBranches, ruleApplicationCount], + count=0, step=0, rGen=g} ---------- Monadic Statistics functions follow ------------- -initialStatisticsStateFor :: (MonadState Statistics m) => (m a -> Statistics -> b) +initialStatisticsStateFor :: (MonadState Statistics m) => (m a -> Statistics -> b) -> StdGen -> m a -> b -initialStatisticsStateFor f = flip f defaultStats +initialStatisticsStateFor f g = flip f (defaultStats g) setPrintOutInterval :: Int -> StatisticsState () setPrintOutInterval i = modify $ \s -> s{step = i} @@ -87,7 +90,6 @@ recordClosedBranch :: StatisticsState () recordClosedBranch = modify (updateMetrics recordClosedBranchM) - printOutMetricsFinal :: Statistics -> IO () printOutMetricsFinal stats = diff --git a/src/HTab/Tableau.hs b/src/HTab/Tableau.hs --- a/src/HTab/Tableau.hs +++ b/src/HTab/Tableau.hs @@ -4,8 +4,8 @@ import System.Console.CmdArgs ( whenLoud ) -import Control.Monad.State(StateT,lift,modify) -import HTab.Statistics(Statistics,updateStep,printOutMetrics, +import Control.Monad.State(StateT,lift,modify, gets, modify) +import HTab.Statistics(Statistics(rGen),updateStep,printOutMetrics, recordClosedBranch,recordFiredRule) import HTab.Branch(BranchInfo(..)) import HTab.CommandLine(backjumping,Params,configureStats) @@ -33,16 +33,19 @@ return $ CLOSED bprs BranchOK br -> do verbose (show br) - case applicableRule br p (depth + 1) of + g <- gets rGen + case applicableRule br p (depth + 1) g of -- generate new number Nothing -> do verbose ">> Saturated open branch" return $ OPEN $ buildModel br - Just (rule,newBranch) -> + Just (rule,newBranch, g') -> do verbose $ ">> Rule : " ++ show rule recordFiredRule $ ruleToId rule - case applyRule p rule newBranch of + let (bis,g'') = applyRule p rule newBranch g' + modify $ \s -> s{rGen = g''} + case bis of -- need to shuffle disjunction order [newBi] -> tableauDown p (depth + 1) newBi - bis -> tableauRight p (depth + 1) bis dsEmpty + _ -> tableauRight p (depth + 1) bis dsEmpty tableauRight :: Params -> Depth -> [BranchInfo] -> DependencySet -> TableauMonad OpenFlag tableauRight p depth (hd:tl) currentDepSet = diff --git a/src/htab.hs b/src/htab.hs --- a/src/htab.hs +++ b/src/htab.hs @@ -3,7 +3,6 @@ where import Control.Monad ( unless ) -import Control.Applicative ( (<$>) ) import System.Console.CmdArgs @@ -46,9 +45,9 @@ else return Nothing header :: String -header = unlines ["HTab 1.6.0", - "G. Hoffmann, C. Areces, D.Gorin and J. Heguiabehere. (c) 2002-2011.", - "http://code.google.com/p/intohylo/"] +header = unlines ["HTab 1.7.0", + "G. Hoffmann, C. Areces, D.Gorin and J. Heguiabehere. (c) 2002-2016.", + "http://hub.darcs.net/gh/htab/"] gplTag :: [String] gplTag = [