HTab 1.6.3 → 1.7.2
raw patch · 41 files changed
+1269/−657 lines, 41 filesdep +randomdep ~basedep ~cmdargsdep ~hylolib
Dependencies added: random
Dependency ranges changed: base, cmdargs, hylolib
Files
- COPYING +0/−340
- HTab.cabal +15/−19
- LICENSE +30/−0
- NEWS +5/−0
- rc/br_infinite.frm +18/−0
- rc/br_no_tree.frm +12/−0
- rc/br_unsat_bad_infinite.frm +14/−0
- rc/gbr_no_tree.frm +12/−0
- rc/gsab_confluence.frm +14/−0
- rc/gsab_count.frm +13/−0
- rc/gsab_infinite.frm +20/−0
- rc/gsab_no_tree.frm +12/−0
- rc/gswap_infinite.frm +25/−0
- rc/gswap_no_tree.frm +12/−0
- rc/mem_br_struct.frm +22/−0
- rc/mem_br_struct_refl.frm +18/−0
- rc/mem_sab_struct.frm +25/−0
- rc/mem_sab_struct2.frm +25/−0
- rc/mem_sab_struct3.frm +25/−0
- rc/mem_sab_struct_refl.frm +26/−0
- rc/mem_sw_struct.frm +28/−0
- rc/mem_sw_struct_refl.frm +24/−0
- rc/sab_loop.frm +14/−0
- rc/sab_loop_diamond.frm +17/−0
- rc/sab_no_tree.frm +12/−0
- rc/sab_sat_01.frm +13/−0
- rc/swap_diamond.frm +15/−0
- rc/swap_infinite.frm +25/−0
- rc/swap_no_tree.frm +15/−0
- src/HTab/Branch.hs +72/−60
- src/HTab/CommandLine.hs +22/−11
- src/HTab/DMap.hs +1/−16
- src/HTab/Formula.hs +201/−86
- src/HTab/Literals.hs +8/−1
- src/HTab/Main.hs +72/−36
- src/HTab/Memory.hs +232/−0
- src/HTab/ModelGen.hs +1/−1
- src/HTab/Rules.hs +128/−65
- src/HTab/Statistics.hs +14/−12
- src/HTab/Tableau.hs +9/−6
- src/htab.hs +3/−4
− COPYING
@@ -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.-- <one line to give the program's name and a brief idea of what it does.>- Copyright (C) 19yy <name of author>-- This program is free software; you can redistribute it and/or modify- it under the terms of the GNU General Public License as published by- the Free Software Foundation; either version 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.-- <signature of Ty Coon>, 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.
HTab.cabal view
@@ -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
+ LICENSE view
@@ -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.
NEWS view
@@ -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
+ rc/br_infinite.frm view
@@ -0,0 +1,18 @@+signature {+propositions { s }+nominals { }+relations { br, gbr }+}++theory++{+ s;+ [] false;+ [br](s --> [br]!s);+ [br](!s --> [] !s);+ <br><br> true;+ [br]<> true;+ [br][br](s --> [](!s --> [][]!s));+ [br][][][br](s --> <>( !s & <><>s ));+}
+ rc/br_no_tree.frm view
@@ -0,0 +1,12 @@+signature {+propositions { p }+nominals { }+relations { br }+}++theory++{+ [] false;+ <br>[] false;+}
+ rc/br_unsat_bad_infinite.frm view
@@ -0,0 +1,14 @@+signature {+propositions { s }+nominals { }+relations { br, gbr }+}++theory++{+ s;+ [] false;+ [br](s --> [br]!s);+ [br][]!s;+}
+ rc/gbr_no_tree.frm view
@@ -0,0 +1,12 @@+signature {+propositions { p }+nominals { }+relations { sw }+}++theory++{+ [] false;+ <gbr>[] false;+}
+ rc/gsab_confluence.frm view
@@ -0,0 +1,14 @@+signature {+propositions { a, b, c }+nominals { }+relations { gsb }+}++theory++{+ <>(a & !b & <><>a );+ <>(b & !a & <><>b );+ [][](c & []!c);+ <gsb>[][][] false;+}
+ rc/gsab_count.frm view
@@ -0,0 +1,13 @@+signature {+propositions { }+nominals { }+relations { gsb }+}++theory++{+ <gsb><gsb><gsb> true;+ [gsb][gsb][gsb][gsb]false;+}+
+ rc/gsab_infinite.frm view
@@ -0,0 +1,20 @@+signature {+propositions { s }+nominals { }+relations { sb, gsb }+}++theory++{+ s;+ []!s;+ <> true;+ []( <>s & <gsb>!<>s );+ []<>!s;+ [][]( !s --> ( <>s & <gsb>!<>s) );+ [gsb]( (<>(<>s & <>(!s & !<>s)) ) --> <>!<>s);+ [gsb][]( (!<>s) --> []<>s );+ [gsb](!<>( (!<>s) & <><>( !s & (<>s) & <>!<>s)));+ [gsb][gsb]( (<>((!<>s) & <><>(!s & !<>s))) --> <>(!<>s & <>!<>s));+}
+ rc/gsab_no_tree.frm view
@@ -0,0 +1,12 @@+signature {+propositions { }+nominals { }+relations { gsb }+}++theory++{+ <><> true;+ [gsb][] false;+}
+ rc/gswap_infinite.frm view
@@ -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));+}
+ rc/gswap_no_tree.frm view
@@ -0,0 +1,12 @@+signature {+propositions { }+nominals { }+relations { gsw }+}++theory++{+ []false;+ <gsw><> true;+}
+ rc/mem_br_struct.frm view
@@ -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);++ <br>(!s & t & <br>( !s & !t &+ a & !b & !c & !d &+ <>(!s & !a & b & !c & !d &+ <>(!s & !a & !b & c & !d &+ <>(!s & !a & !b & !c & d+ )))));++}
+ rc/mem_br_struct_refl.frm view
@@ -0,0 +1,18 @@+signature {+propositions { s, t }+nominals { }+relations { br }+}++theory++{+ s;+ []false;+ [br](s --> [br]!s);+ [br](!s --> []!s);++ <br>(!s & t & <br>( !s & !t &+ <br>(s & <br>( (<>s) & <>(!s & <>s)))+ ));+}
+ rc/mem_sab_struct.frm view
@@ -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 )));+}
+ rc/mem_sab_struct2.frm view
@@ -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))));+}
+ rc/mem_sab_struct3.frm view
@@ -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) ))));+}
+ rc/mem_sab_struct_refl.frm view
@@ -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)));+++ <>( <sb>(s & <sb>( (!<>s) & <>( (!<>s ) ) ) ) );+}
+ rc/mem_sw_struct.frm view
@@ -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 --> <sw>(s & <><><sw>(s & <>!<>s)));+++ <>(!s & a & !b & !c & !d &+ <>(!s & !a & b & !c & !d &+ <>(!s & !a & !b & c & !d &+ <>(!s & !a & !b & !c & d+ ))));+}
+ rc/mem_sw_struct_refl.frm view
@@ -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 --> <sw>(s & <><><sw>(s & <>!<>s)));+++ <>( a & <sw>(s & <><>(!s & !<>s)));+}
+ rc/sab_loop.frm view
@@ -0,0 +1,14 @@+signature {+propositions { a, b }+nominals { }+relations { sb }+}++theory++{+ <>(a & !b & <><>a);+ <>(b & !a & <><>b);+ [sb](a --> [][]!a);+ [sb](b --> [][]!b);+}
+ rc/sab_loop_diamond.frm view
@@ -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;+}
+ rc/sab_no_tree.frm view
@@ -0,0 +1,12 @@+signature {+propositions { }+nominals { }+relations { sb, gsb }+}++theory++{+ <><>true;+ [sb][]false;+}
+ rc/sab_sat_01.frm view
@@ -0,0 +1,13 @@+signature {+propositions { p, q }+nominals { }+relations { sb, gsb }+}++theory++{+ <sb>p;+ <sb>q;+ <gsb>( <><> true) ;+}
+ rc/swap_diamond.frm view
@@ -0,0 +1,15 @@+signature {+propositions { a, b }+nominals { }+relations { sw }+}++theory++{+ <>(a & !b & <>a);+ <>(b & !a & <>b);+ [sw][][sw][][] false;+ [][sw][][] false;+ <sw><sw><><><><><> true;+}
+ rc/swap_infinite.frm view
@@ -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));+}
+ rc/swap_no_tree.frm view
@@ -0,0 +1,15 @@+signature {+propositions { p }+nominals { }+relations { sw }+}++theory++{+ p;+ []!p;+ [][]!p;+ [][][]!p;+ <sw><><>p;+}
src/HTab/Branch.hs view
@@ -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-
src/HTab/CommandLine.hs view
@@ -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
src/HTab/DMap.hs view
@@ -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
src/HTab/Formula.hs view
@@ -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+
src/HTab/Literals.hs view
@@ -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
src/HTab/Main.hs view
@@ -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 --
+ src/HTab/Memory.hs view
@@ -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"+
src/HTab/ModelGen.hs view
@@ -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
src/HTab/Rules.hs view
@@ -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')+
src/HTab/Statistics.hs view
@@ -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 =
src/HTab/Tableau.hs view
@@ -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 =
src/htab.hs view
@@ -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 = [