diff --git a/COPYING b/COPYING new file mode 100644 --- /dev/null +++ b/COPYING @@ -0,0 +1,340 @@ + GNU GENERAL PUBLIC LICENSE + Version 2, June 1991 + + Copyright (C) 1989, 1991 Free Software Foundation, Inc. + 59 Temple Place - Suite 330, Boston, MA + 02111-1307, USA. + Everyone is permitted to copy and distribute verbatim copies + of this license document, but changing it is not allowed. + + Preamble + + The licenses for most software are designed to take away your +freedom to share and change it. By contrast, the GNU General Public +License is intended to guarantee your freedom to share and change free +software--to make sure the software is free for all its users. This +General Public License applies to most of the Free Software +Foundation's software and to any other program whose authors commit to +using it. (Some other Free Software Foundation software is covered by +the GNU Library General Public License instead.) You can apply it to +your programs, too. + + When we speak of free software, we are referring to freedom, not +price. Our General Public Licenses are designed to make sure that you +have the freedom to distribute copies of free software (and charge for +this service if you wish), that you receive source code or can get it +if you want it, that you can change the software or use pieces of it +in new free programs; and that you know you can do these things. + + To protect your rights, we need to make restrictions that forbid +anyone to deny you these rights or to ask you to surrender the rights. +These restrictions translate to certain responsibilities for you if you +distribute copies of the software, or if you modify it. + + For example, if you distribute copies of such a program, whether +gratis or for a fee, you must give the recipients all the rights that +you have. You must make sure that they, too, receive or can get the +source code. And you must show them these terms so they know their +rights. + + We protect your rights with two steps: (1) copyright the software, and +(2) offer you this license which gives you legal permission to copy, +distribute and/or modify the software. + + Also, for each author's protection and ours, we want to make certain +that everyone understands that there is no warranty for this free +software. If the software is modified by someone else and passed on, we +want its recipients to know that what they have is not the original, so +that any problems introduced by others will not reflect on the original +authors' reputations. + + Finally, any free program is threatened constantly by software +patents. We wish to avoid the danger that redistributors of a free +program will individually obtain patent licenses, in effect making the +program proprietary. To prevent this, we have made it clear that any +patent must be licensed for everyone's free use or not licensed at all. + + The precise terms and conditions for copying, distribution and +modification follow. + + GNU GENERAL PUBLIC LICENSE + TERMS AND CONDITIONS FOR COPYING, DISTRIBUTION AND MODIFICATION + + 0. This License applies to any program or other work which contains +a notice placed by the copyright holder saying it may be distributed +under the terms of this General Public License. The "Program", below, +refers to any such program or work, and a "work based on the Program" +means either the Program or any derivative work under copyright law: +that is to say, a work containing the Program or a portion of it, +either verbatim or with modifications and/or translated into another +language. (Hereinafter, translation is included without limitation in +the term "modification".) Each licensee is addressed as "you". + +Activities other than copying, distribution and modification are not +covered by this License; they are outside its scope. The act of +running the Program is not restricted, and the output from the Program +is covered only if its contents constitute a work based on the +Program (independent of having been made by running the Program). +Whether that is true depends on what the Program does. + + 1. You may copy and distribute verbatim copies of the Program's +source code as you receive it, in any medium, provided that you +conspicuously and appropriately publish on each copy an appropriate +copyright notice and disclaimer of warranty; keep intact all the +notices that refer to this License and to the absence of any warranty; +and give any other recipients of the Program a copy of this License +along with the Program. + +You may charge a fee for the physical act of transferring a copy, and +you may at your option offer warranty protection in exchange for a fee. + + 2. You may modify your copy or copies of the Program or any portion +of it, thus forming a work based on the Program, and copy and +distribute such modifications or work under the terms of Section 1 +above, provided that you also meet all of these conditions: + + a) You must cause the modified files to carry prominent notices + stating that you changed the files and the date of any change. + + b) You must cause any work that you distribute or publish, that in + whole or in part contains or is derived from the Program or any + part thereof, to be licensed as a whole at no charge to all third + parties under the terms of this License. + + c) If the modified program normally reads commands interactively + when run, you must cause it, when started running for such + interactive use in the most ordinary way, to print or display an + announcement including an appropriate copyright notice and a + notice that there is no warranty (or else, saying that you provide + a warranty) and that users may redistribute the program under + these conditions, and telling the user how to view a copy of this + License. (Exception: if the Program itself is interactive but + does not normally print such an announcement, your work based on + the Program is not required to print an announcement.) + +These requirements apply to the modified work as a whole. If +identifiable sections of that work are not derived from the Program, +and can be reasonably considered independent and separate works in +themselves, then this License, and its terms, do not apply to those +sections when you distribute them as separate works. But when you +distribute the same sections as part of a whole which is a work based +on the Program, the distribution of the whole must be on the terms of +this License, whose permissions for other licensees extend to the +entire whole, and thus to each and every part regardless of who wrote it. + +Thus, it is not the intent of this section to claim rights or contest +your rights to work written entirely by you; rather, the intent is to +exercise the right to control the distribution of derivative or +collective works based on the Program. + +In addition, mere aggregation of another work not based on the Program +with the Program (or with a work based on the Program) on a volume of +a storage or distribution medium does not bring the other work under +the scope of this License. + + 3. You may copy and distribute the Program (or a work based on it, +under Section 2) in object code or executable form under the terms of +Sections 1 and 2 above provided that you also do one of the following: + + a) Accompany it with the complete corresponding machine-readable + source code, which must be distributed under the terms of Sections + 1 and 2 above on a medium customarily used for software interchange; or, + + b) Accompany it with a written offer, valid for at least three + years, to give any third party, for a charge no more than your + cost of physically performing source distribution, a complete + machine-readable copy of the corresponding source code, to be + distributed under the terms of Sections 1 and 2 above on a medium + customarily used for software interchange; or, + + c) Accompany it with the information you received as to the offer + to distribute corresponding source code. (This alternative is + allowed only for noncommercial distribution and only if you + received the program in object code or executable form with such + an offer, in accord with Subsection b above.) + +The source code for a work means the preferred form of the work for +making modifications to it. For an executable work, complete source +code means all the source code for all modules it contains, plus any +associated interface definition files, plus the scripts used to +control compilation and installation of the executable. However, as a +special exception, the source code distributed need not include +anything that is normally distributed (in either source or binary +form) with the major components (compiler, kernel, and so on) of the +operating system on which the executable runs, unless that component +itself accompanies the executable. + +If distribution of executable or object code is made by offering +access to copy from a designated place, then offering equivalent +access to copy the source code from the same place counts as +distribution of the source code, even though third parties are not +compelled to copy the source along with the object code. + + 4. You may not copy, modify, sublicense, or distribute the Program +except as expressly provided under this License. Any attempt +otherwise to copy, modify, sublicense or distribute the Program is +void, and will automatically terminate your rights under this License. +However, parties who have received copies, or rights, from you under +this License will not have their licenses terminated so long as such +parties remain in full compliance. + + 5. You are not required to accept this License, since you have not +signed it. However, nothing else grants you permission to modify or +distribute the Program or its derivative works. These actions are +prohibited by law if you do not accept this License. Therefore, by +modifying or distributing the Program (or any work based on the +Program), you indicate your acceptance of this License to do so, and +all its terms and conditions for copying, distributing or modifying +the Program or works based on it. + + 6. Each time you redistribute the Program (or any work based on the +Program), the recipient automatically receives a license from the +original licensor to copy, distribute or modify the Program subject to +these terms and conditions. You may not impose any further +restrictions on the recipients' exercise of the rights granted herein. +You are not responsible for enforcing compliance by third parties to +this License. + + 7. If, as a consequence of a court judgment or allegation of patent +infringement or for any other reason (not limited to patent issues), +conditions are imposed on you (whether by court order, agreement or +otherwise) that contradict the conditions of this License, they do not +excuse you from the conditions of this License. If you cannot +distribute so as to satisfy simultaneously your obligations under this +License and any other pertinent obligations, then as a consequence you +may not distribute the Program at all. For example, if a patent +license would not permit royalty-free redistribution of the Program by +all those who receive copies directly or indirectly through you, then +the only way you could satisfy both it and this License would be to +refrain entirely from distribution of the Program. + +If any portion of this section is held invalid or unenforceable under +any particular circumstance, the balance of the section is intended to +apply and the section as a whole is intended to apply in other +circumstances. + +It is not the purpose of this section to induce you to infringe any +patents or other property right claims or to contest validity of any +such claims; this section has the sole purpose of protecting the +integrity of the free software distribution system, which is +implemented by public license practices. Many people have made +generous contributions to the wide range of software distributed +through that system in reliance on consistent application of that +system; it is up to the author/donor to decide if he or she is willing +to distribute software through any other system and a licensee cannot +impose that choice. + +This section is intended to make thoroughly clear what is believed to +be a consequence of the rest of this License. + + 8. If the distribution and/or use of the Program is restricted in +certain countries either by patents or by copyrighted interfaces, the +original copyright holder who places the Program under this License +may add an explicit geographical distribution limitation excluding +those countries, so that distribution is permitted only in or among +countries not thus excluded. In such case, this License incorporates +the limitation as if written in the body of this License. + + 9. The Free Software Foundation may publish revised and/or new versions +of the General Public License from time to time. Such new versions will +be similar in spirit to the present version, but may differ in detail to +address new problems or concerns. + +Each version is given a distinguishing version number. If the Program +specifies a version number of this License which applies to it and "any +later version", you have the option of following the terms and conditions +either of that version or of any later version published by the Free +Software Foundation. If the Program does not specify a version number of +this License, you may choose any version ever published by the Free Software +Foundation. + + 10. If you wish to incorporate parts of the Program into other free +programs whose distribution conditions are different, write to the author +to ask for permission. For software which is copyrighted by the Free +Software Foundation, write to the Free Software Foundation; we sometimes +make exceptions for this. Our decision will be guided by the two goals +of preserving the free status of all derivatives of our free software and +of promoting the sharing and reuse of software generally. + + NO WARRANTY + + 11. BECAUSE THE PROGRAM IS LICENSED FREE OF CHARGE, THERE IS NO WARRANTY +FOR THE PROGRAM, TO THE EXTENT PERMITTED BY APPLICABLE LAW. EXCEPT WHEN +OTHERWISE STATED IN WRITING THE COPYRIGHT HOLDERS AND/OR OTHER PARTIES +PROVIDE THE PROGRAM "AS IS" WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESSED +OR IMPLIED, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF +MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE. THE ENTIRE RISK AS +TO THE QUALITY AND PERFORMANCE OF THE PROGRAM IS WITH YOU. SHOULD THE +PROGRAM PROVE DEFECTIVE, YOU ASSUME THE COST OF ALL NECESSARY SERVICING, +REPAIR OR CORRECTION. + + 12. IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGREED TO IN WRITING +WILL ANY COPYRIGHT HOLDER, OR ANY OTHER PARTY WHO MAY MODIFY AND/OR +REDISTRIBUTE THE PROGRAM AS PERMITTED ABOVE, BE LIABLE TO YOU FOR DAMAGES, +INCLUDING ANY GENERAL, SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES ARISING +OUT OF THE USE OR INABILITY TO USE THE PROGRAM (INCLUDING BUT NOT LIMITED +TO LOSS OF DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED BY +YOU OR THIRD PARTIES OR A FAILURE OF THE PROGRAM TO OPERATE WITH ANY OTHER +PROGRAMS), EVEN IF SUCH HOLDER OR OTHER PARTY HAS BEEN ADVISED OF THE +POSSIBILITY OF SUCH DAMAGES. + + END OF TERMS AND CONDITIONS + + Appendix: How to Apply These Terms to Your New Programs + + If you develop a new program, and you want it to be of the greatest +possible use to the public, the best way to achieve this is to make it +free software which everyone can redistribute and change under these terms. + + To do so, attach the following notices to the program. It is safest +to attach them to the start of each source file to most effectively +convey the exclusion of warranty; and each file should have at least +the "copyright" line and a pointer to where the full notice is found. + + + Copyright (C) 19yy + + This program is free software; you can redistribute it and/or modify + it under the terms of the GNU General Public License as published by + the Free Software Foundation; either version 2 of the License, or + (at your option) any later version. + + This program is distributed in the hope that it will be useful, + but WITHOUT ANY WARRANTY; without even the implied warranty of + MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + GNU General Public License for more details. + + You should have received a copy of the GNU General Public License + along with this program; if not, write to the Free Software + Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA. + +Also add information on how to contact you by electronic and paper mail. + +If the program is interactive, make it output a short notice like this +when it starts in an interactive mode: + + Gnomovision version 69, Copyright (C) 19yy name of author + Gnomovision comes with ABSOLUTELY NO WARRANTY; for details type `show w'. + This is free software, and you are welcome to redistribute it + under certain conditions; type `show c' for details. + +The hypothetical commands `show w' and `show c' should show the appropriate +parts of the General Public License. Of course, the commands you use may +be called something other than `show w' and `show c'; they could even be +mouse-clicks or menu items--whatever suits your program. + +You should also get your employer (if you work as a programmer) or your +school, if any, to sign a "copyright disclaimer" for the program, if +necessary. Here is a sample; alter the names: + + Yoyodyne, Inc., hereby disclaims all copyright interest in the program + `Gnomovision' (which makes passes at compilers) written by James Hacker. + + , 1 April 1989 + Ty Coon, President of Vice + +This General Public License does not permit incorporating your program into +proprietary programs. If your program is a subroutine library, you may +consider it more useful to permit linking proprietary applications with the +library. If this is what you want to do, use the GNU Library General +Public License instead of this License. diff --git a/HTab.cabal b/HTab.cabal new file mode 100644 --- /dev/null +++ b/HTab.cabal @@ -0,0 +1,62 @@ +Name: HTab +Version: 1.5.4 +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/ +Category: Theorem provers +License: GPL +License-file: COPYING +Author: Guillaume Hoffmann, Carlos Areces, Daniel Gorín, Juan Heguiabehere +Maintainer: guillaume.hoffmann@loria.fr +Cabal-version: >= 1.6.0 +Build-type: Simple + +Data-files: NEWS + examples/*.sh + examples/sat/*.frm + examples/sat_no_mod/*.frm + examples/unsat/*.frm + +Extra-source-files: tests/test-example-formulas.hs + tests/coverage.sh + +Flag static + Description: Build a static binary + Default: False + +Executable htab + Main-is: htab.hs + Other-modules: HTab.Base + HTab.Branch + HTab.CommandLine + HTab.DisjSet + HTab.DMap + HTab.Formula + HTab.Main + HTab.ModelGen + HTab.Relations + HTab.RuleId + HTab.Rules + HTab.Statistics + HTab.Tableau + Build-Depends: base >= 4, base < 5, + mtl >= 1, mtl < 2, + containers < 1, + filepath > 1, filepath <= 2, + directory > 1, directory <= 2, + deepseq >= 1, deepseq <2, + strict < 1, + cmdargs == 0.5, + hylolib >= 1.3, hylolib < 1.4 + Extensions: GADTs + DeriveDataTypeable + FlexibleContexts + Rank2Types + ScopedTypeVariables + Hs-Source-Dirs: src + ghc-options: -O2 -Wall + ghc-prof-options: -auto-all + + if flag(static) + ghc-options: -static -optl-static -optl-pthread diff --git a/NEWS b/NEWS new file mode 100644 --- /dev/null +++ b/NEWS @@ -0,0 +1,63 @@ +* 2010.09.27 : 1.5.4 + o lazy branching by default + o fix memory leak + o flag changes (see --help) +* 2010.05.13 : 1.5.3 + o eager unit propagation by default + o remove unsat caching + o functional and injective modalities support broken for now (non terminating) + o some flag changes (see --help) +* 2009.11.10 : 1.5.2 + o fix bug that made 1.5.1 nearly unusable + o instance retrieval handling (return all nominals making true a given formula) + o add example formulas for all supported languages + o add a --no-loop-check switch (to use with -U -F) + o no longer need --simple if the first word of the input is "begin" +* 2009.10.29 : 1.5.1 + o role inclusion and role equality support of the form + r subsetof {s,t,u} + r equals {s,t,u} + where { } = union of + o MERGE rule no longer immediate (m in the strategy string) + o AND rule now immediate + o internal changes +* 2009.10.03 : 1.5.0 + o new input format with multiple queries support + o converse modalities support + o reflexive, symmetric and transitive modalities support + o experimental support for injective and functional modalities + o experimental support for the transitive closure modality + o fair strategy, strategy order and unrestricted blocking options + o caching for H(@,A) +* 2009.03.02 : 1.4.0 + o down-arrow binder support + o compilable with GHC 6.10 + o removed full clash and latex output + o bugfixes +* 2008.10.30 : 1.3.5 + o unit propagation optimisation + o chain-based blocking for H(@,E) (global blocking still available as an option) +* 2008.04.24 : 1.3.4 + o difference modality support + o no longer depends on happy + o bugfixes and optimisations + o last version compilable with GHC 6.6.X +* 2008.02.11 : 1.3.3 + o universal modality support + o equivalence classes handled with disjoint-set forest + o less duplications of formulas + o more efficient box rule +* 2007.12.05 : 1.2.2 + o backjumping performance improved + o changed command line parameters and configuration file handling + o reads input form standard input when no input file is provided + o added quiet mode + o use HyLoLib's lexer for compatibility +* 2007.10.29 : 1.1 + o backjumping + o more efficient structures for the box rule + o save config file in $HOME +* 2007.09.28 : 1.0 + o semantic branching + o full clash + o model building diff --git a/Setup.lhs b/Setup.lhs new file mode 100644 --- /dev/null +++ b/Setup.lhs @@ -0,0 +1,4 @@ +#! /usr/bin/env runhaskell + +> import Distribution.Simple +> main = defaultMain diff --git a/examples/runsat.sh b/examples/runsat.sh new file mode 100644 --- /dev/null +++ b/examples/runsat.sh @@ -0,0 +1,10 @@ +#!/bin/bash + +HTABPATH="../dist/build/htab/htab" # path to HTab +UNSATPATH="sat" # directory where examples are + +for file in `ls ${UNSATPATH}/*.frm`; +do echo $file;${HTABPATH} -f $file $1 $2 $3 $4; +done + + diff --git a/examples/rununsat.sh b/examples/rununsat.sh new file mode 100644 --- /dev/null +++ b/examples/rununsat.sh @@ -0,0 +1,9 @@ +#!/bin/bash + +HTABPATH="../dist/build/htab/htab" # path to HTab +UNSATPATH="unsat" # directory where examples are + +for file in `ls ${UNSATPATH}/*.frm`; +do echo $file;${HTABPATH} -f $file $1 $2 $3 $4; +done + diff --git a/examples/sat/d_sat1.frm b/examples/sat/d_sat1.frm new file mode 100644 --- /dev/null +++ b/examples/sat/d_sat1.frm @@ -0,0 +1,4 @@ +signature { automatic } theory +{ +A (D (P1)) +} diff --git a/examples/sat/d_sat2.frm b/examples/sat/d_sat2.frm new file mode 100644 --- /dev/null +++ b/examples/sat/d_sat2.frm @@ -0,0 +1,4 @@ +signature { automatic } theory +{ +B N1 +} diff --git a/examples/sat/d_sat3.frm b/examples/sat/d_sat3.frm new file mode 100644 --- /dev/null +++ b/examples/sat/d_sat3.frm @@ -0,0 +1,4 @@ +signature { automatic } theory +{ +A B N1 +} diff --git a/examples/sat/d_sat4.frm b/examples/sat/d_sat4.frm new file mode 100644 --- /dev/null +++ b/examples/sat/d_sat4.frm @@ -0,0 +1,4 @@ +signature { automatic } theory +{ +B !N1 +} diff --git a/examples/sat/d_sat5.frm b/examples/sat/d_sat5.frm new file mode 100644 --- /dev/null +++ b/examples/sat/d_sat5.frm @@ -0,0 +1,4 @@ +signature { automatic } theory +{ +n1 & B <>n1 +} diff --git a/examples/sat/d_sat6.frm b/examples/sat/d_sat6.frm new file mode 100644 --- /dev/null +++ b/examples/sat/d_sat6.frm @@ -0,0 +1,5 @@ +signature { automatic } theory +{ +n1:!n2; +n1 & B D!n1 +} diff --git a/examples/sat/d_sat7.frm b/examples/sat/d_sat7.frm new file mode 100644 --- /dev/null +++ b/examples/sat/d_sat7.frm @@ -0,0 +1,12 @@ +% SAT +% caused a loop when the saturation for the difference modality was not exhaustive, +% ie when we did not check if the "second different word" was already created + +signature { automatic } theory +{ +!N1; !P3; +D N1; +P3 v ( E(N1 v N1:P2) & A(N1 v E P3)); +E(!P2 & B(!P3)); +N1 v A(P2 v D(P3 v <>(P3 & N1))) +} diff --git a/examples/sat/down01.frm b/examples/sat/down01.frm new file mode 100644 --- /dev/null +++ b/examples/sat/down01.frm @@ -0,0 +1,4 @@ +signature { automatic } theory +{ +N2 & <>( down N3 . ( N1:(N2 & !N3))) +} diff --git a/examples/sat/spy.frm b/examples/sat/spy.frm new file mode 100644 --- /dev/null +++ b/examples/sat/spy.frm @@ -0,0 +1,6 @@ +signature { automatic } theory +{ +down (N1 []([]( down( N2 (N1:<>(N2)))))); +[]<>true; +[] (down (N1 (!<>N1))) +} diff --git a/examples/sat/test01.frm b/examples/sat/test01.frm new file mode 100644 --- /dev/null +++ b/examples/sat/test01.frm @@ -0,0 +1,5 @@ +signature { automatic } theory + +{ + !(P1 & P1) +} diff --git a/examples/sat/test02.frm b/examples/sat/test02.frm new file mode 100644 --- /dev/null +++ b/examples/sat/test02.frm @@ -0,0 +1,6 @@ +signature { automatic } theory + +{ + !(P1 & P1); + P2 | P1 +} diff --git a/examples/sat/test03.frm b/examples/sat/test03.frm new file mode 100644 --- /dev/null +++ b/examples/sat/test03.frm @@ -0,0 +1,6 @@ +signature { automatic } theory + +{ + !(P1 & P1) & (P3 -> P2); + !(!P5 ->(P3 | !!P4)) +} diff --git a/examples/sat/test04.frm b/examples/sat/test04.frm new file mode 100644 --- /dev/null +++ b/examples/sat/test04.frm @@ -0,0 +1,7 @@ +signature { automatic } theory + +{ + (P1 & P1 & P1 ) -> (P3 | P4); + (P3 -> (!P2 | (P5 -> P6))); + P6 | P7 | !P8 +} diff --git a/examples/sat/test05.frm b/examples/sat/test05.frm new file mode 100644 --- /dev/null +++ b/examples/sat/test05.frm @@ -0,0 +1,8 @@ +signature { automatic } theory + +{ + !(P1 & P2) <--> P7 | P3; + P5 & P3 -> (P8 | !(P10 -> P9)); + (P3 | P6) -> (P4 | !P16); + (P7 | !P8) +} diff --git a/examples/sat/test06.frm b/examples/sat/test06.frm new file mode 100644 --- /dev/null +++ b/examples/sat/test06.frm @@ -0,0 +1,5 @@ +signature { automatic } theory + +{ + (N1:P1) & (N2:!P1) +} diff --git a/examples/sat/test07.frm b/examples/sat/test07.frm new file mode 100644 --- /dev/null +++ b/examples/sat/test07.frm @@ -0,0 +1,7 @@ +signature { automatic } theory + +{ + !(P1 & P1) & (P3 -> P2); + N1 : !(!P5 ->(P3 | !!P4)); + N2 : (N3 : P3) +} diff --git a/examples/sat/test08.frm b/examples/sat/test08.frm new file mode 100644 --- /dev/null +++ b/examples/sat/test08.frm @@ -0,0 +1,7 @@ +signature { automatic } theory + +{ + (<>(<>(<>(P1 <--> P2)))); + ([]P3); + ([](P3 -> (P5 | P2))) +} diff --git a/examples/sat/test09.frm b/examples/sat/test09.frm new file mode 100644 --- /dev/null +++ b/examples/sat/test09.frm @@ -0,0 +1,4 @@ +signature { automatic } theory +{ +(P1 & (P1 & (P1 & P1))) & (P3 & (P2 & P1) & (P1 & (P2 & P3))) +} diff --git a/examples/sat/test10.frm b/examples/sat/test10.frm new file mode 100644 --- /dev/null +++ b/examples/sat/test10.frm @@ -0,0 +1,23 @@ +signature { automatic } theory +{ + !(P1 & P1); + !(P1 & P1); + P2 | P1; + !(P1 & P1) & (P3 -> P2); + !(!P5 -->(P3 | !!P4)); + (P1 & P1 & P1 ) --> (P3 | P4); + (P3 --> (!P2 | (P5 --> P6))); + P6 | P7 | !P8; + !(P1 & P2) <--> P7 | P3; + P5 & P3 --> (P8 | !(P10 -> P9)); + (P3 | P6) --> (P4 | !P16); + (P7 | !P8); + (N1:P1) & (N2:!P1); + !(P1 & P1) & (P3 --> P2); + N1 : !(!P5 -->(P3 | !!P4)); + N2 : (N3 : P3); + <><><>(P1 <--> P2); + ([]P3); + ([](P3 --> (P5 | P2))); + (P10 & (P10 & (P10 & P10))) & (P30 & (P20 & P10) & (P10 & (P20 & P30))) +} diff --git a/examples/sat/test11.frm b/examples/sat/test11.frm new file mode 100644 --- /dev/null +++ b/examples/sat/test11.frm @@ -0,0 +1,5 @@ +signature { automatic } theory +{ +<>p1 & <><>!p1 & <><><>p1 & <><><><>!p1 & <><><><><>p1 & <><><><><><>!p1; +[](p1 & [](!p1 & [](p1 & [](!p1 & [](p1 & []!p1))))) +} diff --git a/examples/sat/test12.frm b/examples/sat/test12.frm new file mode 100644 --- /dev/null +++ b/examples/sat/test12.frm @@ -0,0 +1,7 @@ +signature { automatic } theory +{ +n1:[](n2 <--> n3 v n5); +[](n1: (n2 <--> p1)); +[][]<>(p1 <--> []p3) <--> <><>p4; +<><><>(p2 v n2:p3) <--> (<>[]p3 v <>[]p2) +} diff --git a/examples/sat/test13.frm b/examples/sat/test13.frm new file mode 100644 --- /dev/null +++ b/examples/sat/test13.frm @@ -0,0 +1,8 @@ +signature { automatic } + +theory +{ +[R1](p1 v p3) <--> [R3](p3 --> !p3); +[R2](p1 --> (p1 <--> (p3 v p4 v !p5))); +[R1][R2][R3](p1 v !p3 v !p5) +} diff --git a/examples/sat/test14.frm b/examples/sat/test14.frm new file mode 100644 --- /dev/null +++ b/examples/sat/test14.frm @@ -0,0 +1,8 @@ +signature { automatic } theory +{ +<>p1 & <>(p1 & <>p1) & [](p1 & <>p1 & <>(<>!p1 & []p2)); +[]!p2 & (p1 <--> p3) & [](p1 <--> p3); +p11 v p12 v p13 v p14 v p15; +!p11 v !p12 v !p13; +[][][](p11 <--> p12) +} diff --git a/examples/sat/test15.frm b/examples/sat/test15.frm new file mode 100644 --- /dev/null +++ b/examples/sat/test15.frm @@ -0,0 +1,7 @@ +signature { automatic } theory +{ +[](n1 <--> [](n2 <--> [](n3 <--> []n4))); +<>[]<>(p1 <--> p2); +[](p3 -> n1:!p1); +(n1:n2) +} diff --git a/examples/sat/test16.frm b/examples/sat/test16.frm new file mode 100644 --- /dev/null +++ b/examples/sat/test16.frm @@ -0,0 +1,12 @@ +signature { automatic } theory +{ +n1:(p1 --> p2); +n2:(p2 --> p3); +n3:(p3 --> p4); +p4 --> (n1: n2); +p2 --> (n1: n3); +[][][]false; +<><>(p1 v false --> p3); +<><>(p2 --> false v [](p1 <--> n3)); +<>(<>p1 v []p3) <--> <>(<>p3 v <>p2) +} diff --git a/examples/sat/test17.frm b/examples/sat/test17.frm new file mode 100644 --- /dev/null +++ b/examples/sat/test17.frm @@ -0,0 +1,6 @@ +signature { automatic } theory +{ +[R1]([R1]p3 --> n1 --> n2:n1 --> n3:n3:n4); +n1 --> ([R1] p3 v [R2] (p2 v [R1]p4)); +(n1:n3) v (n3:n1) <--> [R1]((n1 --> n3 )) +} diff --git a/examples/sat/test18.frm b/examples/sat/test18.frm new file mode 100644 --- /dev/null +++ b/examples/sat/test18.frm @@ -0,0 +1,6 @@ +signature { automatic } theory +{ +([R1] p1 )<--> ([R3]p1 <--> [R1]!p3); +n1: [R2]p1 <--> p2 --> p3; +false --> (false <--> n1:n3) +} diff --git a/examples/sat/test19.frm b/examples/sat/test19.frm new file mode 100644 --- /dev/null +++ b/examples/sat/test19.frm @@ -0,0 +1,10 @@ +signature { automatic } theory +{ +p1 --> (false --> [R2]p3); +[R2](p1 <--> [R2](p1 v p2 v p3)); +[R1][R1][R2](p1 --> [R1](p2 <--> p1)); +(!p1 v !p3) --> (n1:n2); +!p1 v !p3; +(!p1 v !p3) <--> (!p1 v !p3); +[R2][R1](n1:!p1 v !p3) +} diff --git a/examples/sat/test20.frm b/examples/sat/test20.frm new file mode 100644 --- /dev/null +++ b/examples/sat/test20.frm @@ -0,0 +1,7 @@ +signature { automatic } theory +{ +(n1: p1 v n2) & (n2: p2 v n3) & (n3: p3 v n4); +[][][](n1 <--> p3 & <>(n3 -> !p3)); +<>[](n1 <--> n4); +(n4: (p3 <-->[]p3)) <--> (n3: (p4 <-->[]p4)) +} diff --git a/examples/sat/test21.frm b/examples/sat/test21.frm new file mode 100644 --- /dev/null +++ b/examples/sat/test21.frm @@ -0,0 +1,10 @@ +signature { automatic } theory +{ +n1:(n3:p3 v (n4 --> p3)); +[R1](n3:[R3] (p1 v p2 v p3) <--> n4:n2); +n1:n2 v n2:n1; +[R2](p1 <--> p4); +([R1] (p2 v !p4)) v [R3](p3 --> (!p2)); +((P32 v P31) & (!P32 v !P31)) <--> p32 +} + diff --git a/examples/sat/test22.frm b/examples/sat/test22.frm new file mode 100644 --- /dev/null +++ b/examples/sat/test22.frm @@ -0,0 +1,8 @@ +signature { automatic } theory +{ +<>[](p1 v p2) & []<>(p2 v p1) & <><>p1 & <><>p2; +[](!p1 v !p2) & [](p3 <-->p4); +[](p1 <--> p5 & [](p2 <--> p5)); +n1: (p1 <--> p5) & n2: (p1 <--> p5); +n1: !n2 +} diff --git a/examples/sat/test23.frm b/examples/sat/test23.frm new file mode 100644 --- /dev/null +++ b/examples/sat/test23.frm @@ -0,0 +1,6 @@ +signature { automatic } theory +{ +<>(n1 & <>(n2 & <>(n3 & <>(n4 & <>(n5 & <>(n6)))))); +(n1:!n2 & n2:!n3 & n3:!n4 & n4:!n5 & n5:!n6 & n6:!n1); +[](p1 -> [](p2 -> [](p3 -> [](p4 -> [](p5 -> [](p6)))))) +} diff --git a/examples/sat/test24.frm b/examples/sat/test24.frm new file mode 100644 --- /dev/null +++ b/examples/sat/test24.frm @@ -0,0 +1,9 @@ +signature { automatic } theory +{ +(p1 <--> p2) & (p3 <--> p4) v (p5 <--> p6) v (p6<-->p7); +[](!p1 & !p2 & !p3 & !p4 & !p5 & !p6 & !p7); +<>(n1:p1) & <>(n2:p2) & <>(n3:p3) & <>(n4:p4) & <>(n5:p5) & <>(n6:p6) & <>(n7:p7); +<><>(n1:p1) & <><>(n2:p2) & <><>(n3:p3) & <><>(n4:p4) & <><>(n5:p5) & <><>(n6:p6) & +<><>(n7:p7); +n1:n2 & n2:n3 & n3:n4 & n4:n5 & n5:n6 & n6:n7 +} diff --git a/examples/sat/test25.frm b/examples/sat/test25.frm new file mode 100644 --- /dev/null +++ b/examples/sat/test25.frm @@ -0,0 +1,5 @@ +signature { automatic } theory +{ +n1:p1 v n2:p2 v n3:p3 v n4:p4; +[]!p1 & []!p2 & []!p3 & []!p4 +} diff --git a/examples/sat/test26.frm b/examples/sat/test26.frm new file mode 100644 --- /dev/null +++ b/examples/sat/test26.frm @@ -0,0 +1,5 @@ +signature { automatic } theory +{ +(n1: <>[]!p1) | (n1: []<>p2) | (n2: p3); +(n1: <>n3) | (n2: p1) +} diff --git a/examples/sat/test27.frm b/examples/sat/test27.frm new file mode 100644 --- /dev/null +++ b/examples/sat/test27.frm @@ -0,0 +1,4 @@ +signature { automatic } theory +{ +A (p1 ^ []!p1) +} diff --git a/examples/sat/test28.frm b/examples/sat/test28.frm new file mode 100644 --- /dev/null +++ b/examples/sat/test28.frm @@ -0,0 +1,5 @@ +signature { automatic } theory +{ +A []p1; +!p1 +} diff --git a/examples/sat/test29.frm b/examples/sat/test29.frm new file mode 100644 --- /dev/null +++ b/examples/sat/test29.frm @@ -0,0 +1,5 @@ +signature { automatic } theory +{ +A[](([]!p1) v (<>p1)); +n1:<><>p1 +} diff --git a/examples/sat/test30.frm b/examples/sat/test30.frm new file mode 100644 --- /dev/null +++ b/examples/sat/test30.frm @@ -0,0 +1,4 @@ +signature { automatic } theory +{ +A(!N0 v !N1) +} diff --git a/examples/sat/test31.frm b/examples/sat/test31.frm new file mode 100644 --- /dev/null +++ b/examples/sat/test31.frm @@ -0,0 +1,4 @@ +signature { automatic } theory +{ +A(N0 : true) +} diff --git a/examples/sat/test32.frm b/examples/sat/test32.frm new file mode 100644 --- /dev/null +++ b/examples/sat/test32.frm @@ -0,0 +1,4 @@ +signature { automatic } theory +{ +A(N0 & E true) +} diff --git a/examples/sat/test33.frm b/examples/sat/test33.frm new file mode 100644 --- /dev/null +++ b/examples/sat/test33.frm @@ -0,0 +1,12 @@ +% satisfiable +% found unsatisfiable if the branching dependencies are not copied +% to the right structures when there is an equivalence class merge + +signature { automatic } theory + +{ + +n1:[]false; +n2:<>true; +(<><>true ) v (n2 & n1) +} diff --git a/examples/sat/test34.frm b/examples/sat/test34.frm new file mode 100644 --- /dev/null +++ b/examples/sat/test34.frm @@ -0,0 +1,10 @@ +% caused a problem of in the interaction between backjumping and equivalence classes + +signature { automatic } theory +{ +P1 v !N1:(!N1 v !P1); +N1 v !N1:(!N1 v P1); +P1 v N1:(!P1 v !N1); +!P1 v ![R1](!N1 v P1); +P1 v [R1](P1 v N1) +} diff --git a/examples/sat/test35.frm b/examples/sat/test35.frm new file mode 100644 --- /dev/null +++ b/examples/sat/test35.frm @@ -0,0 +1,9 @@ +% caused a problem of in the interaction between backjumping and equivalence classes +signature { automatic } theory +{ +!N1 v !A(!N1 v !P1); +N1 v !N1:(!P1 v !N1); +P1 v [R1](N1 v P1); +!P1 v [R1](!P1 v !N1); +!N1 v A(!P1 v !N1) +} diff --git a/examples/sat/test36.frm b/examples/sat/test36.frm new file mode 100644 --- /dev/null +++ b/examples/sat/test36.frm @@ -0,0 +1,7 @@ +signature { automatic } theory +{ +N1; +<>true; +[]<>true; +[]N1 +} diff --git a/examples/sat/test37.frm b/examples/sat/test37.frm new file mode 100644 --- /dev/null +++ b/examples/sat/test37.frm @@ -0,0 +1,13 @@ +% sat +% may be found unsatisfiable if the dependencies are not +% correctly propagated when [] constraints and accessibility +% formulas meet, after an equivalence class merge + +signature { automatic } theory + +{ +N1; +<><>(N2 & P1); +E false v [](N1 v E true); +[](!P1 v N2:(N1 & !P1)) +} diff --git a/examples/sat/test38.frm b/examples/sat/test38.frm new file mode 100644 --- /dev/null +++ b/examples/sat/test38.frm @@ -0,0 +1,8 @@ +% had bad model building at some point with chain blocking + +signature { automatic } theory + +{ +A<><>!N1; +[](P1 v N1) & []!P1 +} diff --git a/examples/sat/test39.frm b/examples/sat/test39.frm new file mode 100644 --- /dev/null +++ b/examples/sat/test39.frm @@ -0,0 +1,7 @@ +signature { automatic } theory +{ +P1 v N2:N1; +!N2 v (!N2 & B false); +!P1 v <>false; +N1 v []true +} diff --git a/examples/sat/test40.frm b/examples/sat/test40.frm new file mode 100644 --- /dev/null +++ b/examples/sat/test40.frm @@ -0,0 +1,4 @@ +begin +N0; +<>( N0 & ((<>true) & ([] <>N0:[]N0))) +end diff --git a/examples/sat/trclos1.frm b/examples/sat/trclos1.frm new file mode 100644 --- /dev/null +++ b/examples/sat/trclos1.frm @@ -0,0 +1,18 @@ +signature { + +propositions { P1, P2, P3, P4 } +nominals { N1, N2 } +relations { R1 , RX : {trclosureof R1} } + +} + +theory { + +!P4 v [R1](!P2 v ![R1](N2 v [RX](P2 v !N1:(!N2 v ![R1](!N2 v N1))))); +!N1 v [RX](!P4 v ![RX](!N2 v [RX](P4 v [RX](!P4 v !N1:(!P4 v P3))))); +P2 v N2:(!P1 v [R1](N1 v [RX](!N1 v !N1:(N2 v ![RX](!N1 v P1))))); +N1 v [R1](P3 v !N2:(!P4 v N2:(N1 v ![R1](N1 v [RX](N1 v !N2))))); +!N1 v [RX](!P3 v !N2:(N1 v !N1:(!N2 v ![R1](!P3 v [RX](N2 v !N1))))); +!N1 v ![R1](!P4 v ![RX](!N2 v N1:(N2 v [RX](P3 v [R1](!N1 v P2))))) + +} diff --git a/examples/sat_no_mod/all1.frm b/examples/sat_no_mod/all1.frm new file mode 100644 --- /dev/null +++ b/examples/sat_no_mod/all1.frm @@ -0,0 +1,52 @@ +% Input file in the format of hylolib 1.3 + +signature +{ + +propositions { tall, strong, pretty, naive } +nominals { alice, bob, jean, marie, unknown } +relations { love, + lovedBy : {inverseof love}, + canManipulate : {trclosureof lovedBy}, + know : {reflexive}, + touches : {symmetric}, + U : {universal}, + fatherOf, + motherOf, + parentOf : {equals {fatherOf,motherOf}}, + childOf : {inverseof parentOf}, + youngerThan : {transitive, subsetof childOf} + } + +} + +theory { + [U]((tall & strong) --> pretty); + + alice: ( strong & !tall & !naive); + bob: ( tall & !strong ) ; + + (alice:bob) v jean:marie; + + bob:[lovedBy]naive; + + alice:marie; + marie:bob; + bob:jean; + + unknown:alice + +} + +query (satisfiable? , "out1") { + alice:jean +} + +query (satisfiable? , "out2") { + unknown:jean +} + +query (retrieve , "retrieve1") { + jean +} + diff --git a/examples/unsat/d_unsat1.frm b/examples/unsat/d_unsat1.frm new file mode 100644 --- /dev/null +++ b/examples/unsat/d_unsat1.frm @@ -0,0 +1,4 @@ +signature { automatic } theory +{ +A D N1 +} diff --git a/examples/unsat/d_unsat2.frm b/examples/unsat/d_unsat2.frm new file mode 100644 --- /dev/null +++ b/examples/unsat/d_unsat2.frm @@ -0,0 +1,6 @@ +signature { automatic } theory +{ +N1 & B N1; +E P1; +E !P1 +} diff --git a/examples/unsat/d_unsat3.frm b/examples/unsat/d_unsat3.frm new file mode 100644 --- /dev/null +++ b/examples/unsat/d_unsat3.frm @@ -0,0 +1,5 @@ +signature { automatic } theory +{ +N1:!N2; +E B !(N1 v N2) +} diff --git a/examples/unsat/d_unsat4.frm b/examples/unsat/d_unsat4.frm new file mode 100644 --- /dev/null +++ b/examples/unsat/d_unsat4.frm @@ -0,0 +1,8 @@ +signature { automatic } theory +{ +N1:!N2; N1:!N3; N1:!N4; +N2:!N3; N2:!N4; N3:!N4; +N1:P1; N2:P1; +N3:!P1; N4:!P1; +(E B P1) v (E B !P1) +} diff --git a/examples/unsat/d_unsat5.frm b/examples/unsat/d_unsat5.frm new file mode 100644 --- /dev/null +++ b/examples/unsat/d_unsat5.frm @@ -0,0 +1,16 @@ +signature { automatic } theory +{ +!P1 v ![R1](!N1 v !D(!P2 v N1:(N1 v P3))); +!N1 v !D(P1 v !A(!N1 v !N1:(!N1 v !P1))); +P3 v A(!P3 v [R1](!N1 v D(!P2 v P3))); +P1 v [R1](P3 v A(N1 v N1:(!P3 v !N1))); +!N1 v !A(N1 v !D(P2 v ![R1](P1 v N1))); +!P1 v !A(P3 v !D(N1 v N1:(!N1 v !P2))); +N1 v !A(P1 v !N1:(!N1 v [R1](P1 v P3))); +!P1 v !D(!P1 v !A(N1 v !N1:(P1 v !P3))); +!N1 v !A(!N1 v !D(N1 v N1:(P2 v N1))); +N1 v ![R1](P1 v [R1](!P2 v D(!P1 v P3))); +N1 v A(!P2 v D(!P1 v ![R1](!P3 v !N1))); +!P2 v N1:(N1 v [R1](!P2 v !A(P3 v N1))); +N1 v [R1](N1 v !N1:(P3 v !N1:(!P2 v N1))) +} diff --git a/examples/unsat/d_unsat6.frm b/examples/unsat/d_unsat6.frm new file mode 100644 --- /dev/null +++ b/examples/unsat/d_unsat6.frm @@ -0,0 +1,4 @@ +signature { automatic } theory +{ +<>([]!N0 ^ B false) +} diff --git a/examples/unsat/fun_inj1.frm b/examples/unsat/fun_inj1.frm new file mode 100644 --- /dev/null +++ b/examples/unsat/fun_inj1.frm @@ -0,0 +1,13 @@ +signature { +propositions { p } +nominals { n,m } +relations { r : { functional } } +} + +theory + +{ + n:p; + m:!p; + n:m +} diff --git a/examples/unsat/fun_inj2.frm b/examples/unsat/fun_inj2.frm new file mode 100644 --- /dev/null +++ b/examples/unsat/fun_inj2.frm @@ -0,0 +1,14 @@ +signature { +propositions { p } +nominals { n,a,b } +relations { r, + s : { inverseof r, functional } } +} + +theory + +{ + a:n; + b:n; + a:!b +} diff --git a/examples/unsat/interpol.frm b/examples/unsat/interpol.frm new file mode 100644 --- /dev/null +++ b/examples/unsat/interpol.frm @@ -0,0 +1,6 @@ +% Interpolation formula + +signature { automatic } theory +{ +!((<>p1 & <>!p1) --> (([](p2 --> N1) --> <>!p2))) +} diff --git a/examples/unsat/role_equality1.frm b/examples/unsat/role_equality1.frm new file mode 100644 --- /dev/null +++ b/examples/unsat/role_equality1.frm @@ -0,0 +1,15 @@ +signature { +propositions { p } +nominals { } +relations { student, + course, + tag : { equals {student, course}} } +} + +theory + +{ + p; + [student]!p; + [course]!p +} diff --git a/examples/unsat/role_inclusion1.frm b/examples/unsat/role_inclusion1.frm new file mode 100644 --- /dev/null +++ b/examples/unsat/role_inclusion1.frm @@ -0,0 +1,13 @@ +signature { +propositions { p } +nominals { } +relations { s, t, r : { reflexive, subsetof {s,t}} } +} + +theory + +{ + p; + [s]!p; + [t]!p +} diff --git a/examples/unsat/symmetry1.frm b/examples/unsat/symmetry1.frm new file mode 100644 --- /dev/null +++ b/examples/unsat/symmetry1.frm @@ -0,0 +1,14 @@ +signature { +propositions { p } +nominals { n,m } +relations { s : {symmetric}, t : {trclosureof s} } +} + +theory + +{ + n:m; + n:p; + m:[t]!p + +} diff --git a/examples/unsat/test01.frm b/examples/unsat/test01.frm new file mode 100644 --- /dev/null +++ b/examples/unsat/test01.frm @@ -0,0 +1,5 @@ +signature { automatic } theory + +{ + P1 & !P1 +} diff --git a/examples/unsat/test02.frm b/examples/unsat/test02.frm new file mode 100644 --- /dev/null +++ b/examples/unsat/test02.frm @@ -0,0 +1,7 @@ +signature { automatic } theory + +{ + P1 | P2 | P3 | P4; + !P1 | !P2; + !(P1 --> ((P3 <--> P4) --> P1)) +} diff --git a/examples/unsat/test03.frm b/examples/unsat/test03.frm new file mode 100644 --- /dev/null +++ b/examples/unsat/test03.frm @@ -0,0 +1,7 @@ +signature { automatic } theory +{ + +P1 | P2 ; +P1 | !P2; +!P1 +} diff --git a/examples/unsat/test04.frm b/examples/unsat/test04.frm new file mode 100644 --- /dev/null +++ b/examples/unsat/test04.frm @@ -0,0 +1,6 @@ +signature { automatic } theory + +{ +!(((P3 | (!P4 & P5)) <--> (P7 | (P4 --> P2))) <--> (((P3 | (!P4 & P5)) --> (P7 | +(P4 --> P2))) & ((P7 | (P4 --> P2)) --> (P3 | (!P4 & P5))))) +} diff --git a/examples/unsat/test05.frm b/examples/unsat/test05.frm new file mode 100644 --- /dev/null +++ b/examples/unsat/test05.frm @@ -0,0 +1,7 @@ +signature { automatic } theory + +{ + !((P1 & P2) -> ( ((P4 <--> !P7) | !P9) --> ((P1 & P2) | (P2 | !P2)) )); + P1 | P2; + P4 <--> ! P5 +} diff --git a/examples/unsat/test06.frm b/examples/unsat/test06.frm new file mode 100644 --- /dev/null +++ b/examples/unsat/test06.frm @@ -0,0 +1,7 @@ +signature { automatic } theory + +{ + N1 : ( N2); + N2 : P1; + N1 : [R1] !P1 +} diff --git a/examples/unsat/test07.frm b/examples/unsat/test07.frm new file mode 100644 --- /dev/null +++ b/examples/unsat/test07.frm @@ -0,0 +1,5 @@ +signature { automatic } theory + +{ + !(([R1](P1 --> P2)) --> (([R1] P1) --> ([R1] P2))) +} diff --git a/examples/unsat/test08.frm b/examples/unsat/test08.frm new file mode 100644 --- /dev/null +++ b/examples/unsat/test08.frm @@ -0,0 +1,5 @@ +signature { automatic } theory + +{ + !([R1](P1 | !P1)) +} diff --git a/examples/unsat/test09.frm b/examples/unsat/test09.frm new file mode 100644 --- /dev/null +++ b/examples/unsat/test09.frm @@ -0,0 +1,5 @@ +signature { automatic } theory + +{ + !(([R1](P1 & P2)) -> (([R1]P1) & ([R1]P2))) +} diff --git a/examples/unsat/test10.frm b/examples/unsat/test10.frm new file mode 100644 --- /dev/null +++ b/examples/unsat/test10.frm @@ -0,0 +1,5 @@ +signature { automatic } theory + +{ + !(((P1) | (P2)) --> ((P1 | P2))) +} diff --git a/examples/unsat/test11.frm b/examples/unsat/test11.frm new file mode 100644 --- /dev/null +++ b/examples/unsat/test11.frm @@ -0,0 +1,4 @@ +signature { automatic } theory +{ +!(N1 : N1) +} diff --git a/examples/unsat/test12.frm b/examples/unsat/test12.frm new file mode 100644 --- /dev/null +++ b/examples/unsat/test12.frm @@ -0,0 +1,6 @@ +signature { automatic } theory +{ +N1: N2; +N1: [R1] P1; +N2: !P1 +} diff --git a/examples/unsat/test13.frm b/examples/unsat/test13.frm new file mode 100644 --- /dev/null +++ b/examples/unsat/test13.frm @@ -0,0 +1,4 @@ +signature { automatic } theory +{ +!([R1](P1 --> P2) --> [R1]P1 --> [R1]P2) +} diff --git a/examples/unsat/test14.frm b/examples/unsat/test14.frm new file mode 100644 --- /dev/null +++ b/examples/unsat/test14.frm @@ -0,0 +1,6 @@ +signature { automatic } theory +{ +!((!<>(n1:n3 v <>(p1 <--> []p3)) & <>(n3:<>p1 --> [](p3 v <>(p4 <--> +<>p2)))) --> <>(!(n1:n3 v <>(p1 <--> []p3) & (n3:<>p1 --> [](p3 v <>(p4 <--> +<>p2)))))) +} diff --git a/examples/unsat/test15.frm b/examples/unsat/test15.frm new file mode 100644 --- /dev/null +++ b/examples/unsat/test15.frm @@ -0,0 +1,4 @@ +signature { automatic } theory +{ +!(<>(n1 & <><><><><>(n1:n2) & (<>(p1 --> [](p3 <--> <>p1))) & <><><><><>(n2:n3)) & <>(n3 & p2) --> <>((<>(p1 --> [](p3 <--> <>p1))) & p2)) +} diff --git a/examples/unsat/test16.frm b/examples/unsat/test16.frm new file mode 100644 --- /dev/null +++ b/examples/unsat/test16.frm @@ -0,0 +1,5 @@ +signature { automatic } theory +{ +!(((<><><><>(n1:n2)) & n1:(([]<>(p1 v n2:(p1 <--> <>p3))) --> (<>p1 <--> []<>(false v n2:(n3 & P4))))) --> (n2:([]<>(p1 v n2:(p1 <--> <>p3))) --> n1:(<>p1 <--> []<>(false v n2:(n3 & P4))))) +} + diff --git a/examples/unsat/test17.frm b/examples/unsat/test17.frm new file mode 100644 --- /dev/null +++ b/examples/unsat/test17.frm @@ -0,0 +1,5 @@ +signature { automatic } theory +{ +!(n1:(n1 & n2:(n2 & ([](p1 -->((!(p1 -> (p2 --> p1))) v p2)) --> ([]p1 --> []p2))))) +} + diff --git a/examples/unsat/test18.frm b/examples/unsat/test18.frm new file mode 100644 --- /dev/null +++ b/examples/unsat/test18.frm @@ -0,0 +1,6 @@ +signature { automatic } theory +{ +n1:<>(n1 v (p1 ^ !p1)); +n1:((<>true v (p1 --> (p2 --> p1)) v []false) --> p1); +!(n1:<>p1) +} diff --git a/examples/unsat/test19.frm b/examples/unsat/test19.frm new file mode 100644 --- /dev/null +++ b/examples/unsat/test19.frm @@ -0,0 +1,10 @@ +signature { automatic } theory +{ +<>((p1 v p2) & (n1:p3)); +[](p1 --> p3); +[](p2 --> p3); +n1:(p3 --> !p1); +n1:<>n2; +n2:((n1:!p1) --> p5); +!(<>p3 v n1:<>p5) +} diff --git a/examples/unsat/test20.frm b/examples/unsat/test20.frm new file mode 100644 --- /dev/null +++ b/examples/unsat/test20.frm @@ -0,0 +1,12 @@ +signature { automatic } theory +{ +n1:(p1 -> <>p2); +n2:(p2 -> []p3); +n1:!n2; +n3:<>n1; +n3:<>n2; +n1:<>n2; +n2:<>n1; +n1:!p3; +n3:<>(n2 & p2) +} diff --git a/examples/unsat/test21.frm b/examples/unsat/test21.frm new file mode 100644 --- /dev/null +++ b/examples/unsat/test21.frm @@ -0,0 +1,12 @@ +signature { automatic } theory +{ +n1:(p1 --> <>([](<>p1 <--> []<>(p1 v false)))); +n2:(([](<>p1 <--> []<>(p1 v false))) --> []p3); +n1:!n2; +n3:<>n1; +n3:<>n2; +n1:<>n2; +n2:<>n1; +n1:!p3; +n3:<>(n2 & ([](<>p1 <--> []<>(p1 v false)))) +} diff --git a/examples/unsat/test22.frm b/examples/unsat/test22.frm new file mode 100644 --- /dev/null +++ b/examples/unsat/test22.frm @@ -0,0 +1,11 @@ +signature { automatic } theory +{ +n1:<>(!((<>(n1 & p1) & <>(n1 & p2))-> <>(p1 & p2))); +<>(p1 v <>(p1 v <>(p1 v <>(p1 v <>(p1 v <>(p1 v <>(n2:n1))))))); +[]!p1; +[][]!p1; +[][][]!p1; +[][][][]!p1; +[][][][][]!p1; +n2:<>true +} diff --git a/examples/unsat/test23.frm b/examples/unsat/test23.frm new file mode 100644 --- /dev/null +++ b/examples/unsat/test23.frm @@ -0,0 +1,12 @@ +signature { automatic } theory +{ +n1:<>(!((<>(n1 & p1) & <>(n1 & p2))-> <>(p1 & p2))); +<>((p1 <--> [](p3 <--> <>false)) v <>((p1 <--> [](p3 <--> <>false)) v <>((p1 <--> [](p3 <--> <>false)) v <>((p1 <--> [](p3 <--> <>false)) v <>((p1 <--> [](p3 <--> <>false)) v <>((p1 <--> [](p3 <--> <>false)) v <>(n2:n1))))))); +[](!(p1 <--> [](p3 <--> <>false))); +[][](!(p1 <--> [](p3 <--> <>false))); +[][][](!(p1 <--> [](p3 <--> <>false))); +[][][][](!(p1 <--> [](p3 <--> <>false))); +[][][][][](!(p1 <--> [](p3 <--> <>false))); +n2:<>true +} + diff --git a/examples/unsat/test24.frm b/examples/unsat/test24.frm new file mode 100644 --- /dev/null +++ b/examples/unsat/test24.frm @@ -0,0 +1,14 @@ +signature { automatic } theory +{ +n1:(p1 --> <>([](<>p1 <--> []<>(p1 v false)))); +n2:(([](<>p1 <--> []<>(p1 v false))) -> [](([](p1 <--> (n2:n1 v []<>p2))))); +n1:!n2; +n3:<>n1; +n3:<>n2; +n1:<>n2; +n2:<>n1; +n1:!(([](p1 <--> (n2:n1 v []<>p2)))); +n3:<>(n2 & ([](<>p1 <--> []<>(p1 v false)))) +} + + diff --git a/examples/unsat/test25.frm b/examples/unsat/test25.frm new file mode 100644 --- /dev/null +++ b/examples/unsat/test25.frm @@ -0,0 +1,6 @@ +signature { automatic } theory +{ +!(<>(n1 & <><><><><>(n1:n2) & (<>(p1 --> [](p3 <--> <>p1))) & <><><><><>(n2:n3)) & <>(n3 & (p1 v (p3 <--> <>[]p1))) --> <>((<>(p1 --> [](p3 <--> <>p1))) & (p1 v (p3 <--> <>[]p1)))) +} + + diff --git a/examples/unsat/test28.frm b/examples/unsat/test28.frm new file mode 100644 --- /dev/null +++ b/examples/unsat/test28.frm @@ -0,0 +1,6 @@ +signature { automatic } theory +{ +n1:<>(n1 v (p1 & !p1)); +n1:(<>true --> p1); +!(n1:<>p1) +} diff --git a/examples/unsat/test29.frm b/examples/unsat/test29.frm new file mode 100644 --- /dev/null +++ b/examples/unsat/test29.frm @@ -0,0 +1,10 @@ +signature { automatic } theory +{ +(n1 v !([R1](n3 v (n3:(!n4 v !(n2:(p8 v ([R1](p6 v ([R1](!p3 v !(n4:(n2 v (n2:(n1 v (n4:(n3 v p1))))))))))))))))) & +(!n4 v !(n3:(!n1 v (n2:(!n3 v !([R1](n3 v (n4:(n2 v ([R1](p7 v !(n3:(p6 v !(n4:(n1 v !([R1](n1 v !p5))))))))))))))))) & +(p4 v !([R1](n4 v ([R1](!n4 v (n1:(n3 v !([R1](!n1 v ([R1](!n3 v (n4:(!p6 v !(n2:(!p3 v !(n4:(!n3 v n1))))))))))))))))) & +(n4 v !([R1](!p2 v (n3:(!n2 v (n4:(!n1 v !([R1](!p7 v !(n2:(!n4 v ([R1](!p2 v !(n3:(!p6 v (n2:(!n1 v p6))))))))))))))))) & +(n2 v ([R1](n3 v !(n2:(!n3 v (n3:(!n4 v (n3:(!p2 v ([R1](!p2 v (n3:(!p3 v !([R1](!p3 v ([R1](n2 v !n1))))))))))))))))) & +(!n2 v (n4:(!p4 v !([R1](n1 v (n4:(p4 v (n4:(p4 v !(n3:(p2 v ([R1](!p1 v ([R1](p1 v ([R1](n2 v !n1))))))))))))))))) & +(n4 v !(n1:(!n3 v (n1:(!p2 v ([R1](n1 v !(n4:(!p3 v !([R1](n2 v ([R1](!n2 v (n1:(!p4 v ([R1](n4 v !n3))))))))))))))))) +} diff --git a/examples/unsat/test32.frm b/examples/unsat/test32.frm new file mode 100644 --- /dev/null +++ b/examples/unsat/test32.frm @@ -0,0 +1,8 @@ +signature { automatic } theory +{ +n2:n1; +n1 v (n1:(n2 & !p1)); +(n1:p1); +!n2 +} + diff --git a/examples/unsat/test33.frm b/examples/unsat/test33.frm new file mode 100644 --- /dev/null +++ b/examples/unsat/test33.frm @@ -0,0 +1,4 @@ +signature { automatic } theory +{ +A (p1 ^ <>!p1) +} diff --git a/examples/unsat/test34.frm b/examples/unsat/test34.frm new file mode 100644 --- /dev/null +++ b/examples/unsat/test34.frm @@ -0,0 +1,5 @@ +signature { automatic } theory +{ +A(P1 v P2); +N1:(!P1 & !P2) +} diff --git a/examples/unsat/test35.frm b/examples/unsat/test35.frm new file mode 100644 --- /dev/null +++ b/examples/unsat/test35.frm @@ -0,0 +1,5 @@ +signature { automatic } theory +{ +down(N1 !N1) +} + diff --git a/examples/unsat/test36.frm b/examples/unsat/test36.frm new file mode 100644 --- /dev/null +++ b/examples/unsat/test36.frm @@ -0,0 +1,4 @@ +signature { automatic } theory +{ +!((down (N1 dia (N1 ^ p1) )) --> p1) +} diff --git a/examples/unsat/test37.frm b/examples/unsat/test37.frm new file mode 100644 --- /dev/null +++ b/examples/unsat/test37.frm @@ -0,0 +1,10 @@ +signature { automatic } theory +{ +n3:[R3](down (N1 [R1]([R1]( down( N2 (N1:N2)))))) ; +n3:n1; +n3:n2; +n3:n3; +n1:n2; +n2:n3; +n1:!n3 +} diff --git a/examples/unsat/test38.frm b/examples/unsat/test38.frm new file mode 100644 --- /dev/null +++ b/examples/unsat/test38.frm @@ -0,0 +1,5 @@ +signature { automatic } theory +{ +p1 v <><><><>p1 v down(N1 <>(N1:[]p1)); +A !p1 +} diff --git a/examples/unsat/test39.frm b/examples/unsat/test39.frm new file mode 100644 --- /dev/null +++ b/examples/unsat/test39.frm @@ -0,0 +1,15 @@ +signature { + +propositions { p } +nominals { n} +relations { r : {functional}, + s : {inverseof r} } + +} + +theory +{ + +E (p & n) & E (!p & n) + +} diff --git a/examples/unsat/test40.frm b/examples/unsat/test40.frm new file mode 100644 --- /dev/null +++ b/examples/unsat/test40.frm @@ -0,0 +1,14 @@ +signature { + +propositions { p } +nominals { n} +relations { r : {functional} } + +} + +theory +{ + +n:( p & n:!p) + +} diff --git a/src/HTab/Base.hs b/src/HTab/Base.hs new file mode 100644 --- /dev/null +++ b/src/HTab/Base.hs @@ -0,0 +1,75 @@ +---------------------------------------------------- +-- -- +-- Base.hs -- +-- General use functions -- +-- -- +---------------------------------------------------- + +{- +Copyright (C) HyLoRes 2002-2005 +Carlos Areces - areces@loria.fr - http://www.loria.fr/~areces +Daniel Gorin - dgorin@dc.uba.ar +Juan Heguiabehere - juanh@inf.unibz.it - http://www.inf.unibz.it/~juanh/ + +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. +-} + +module HTab.Base + +where +import qualified Data.Map as Map +import Data.IntMap ( IntMap ) +import qualified Data.IntMap as IntMap +import Data.List ( sort ) +import qualified Data.Set as Set + +almostCartesianProduct :: [a] -> [b] -> [(a,b)] +-- example: +-- acp [a1,a2,a3] [b1,b2,b3] = [(a1,b2),(a1,b3),(a2,b1),(a2,b3),(a3,b1),(a3,b2)] +-- +-- require : as and bs must be of the same size +almostCartesianProduct [] _ = error "almostCartesianProduct: first list empty" +almostCartesianProduct _ [] = error "almostCartesianProduct: second list empty" +almostCartesianProduct as bs = [(a,b) | (idxA,a) <- zip [(0::Int)..] as, + (idxB,b) <- zip [(0::Int)..] bs, + idxA /= idxB] + + +moveInMap :: IntMap b -> Int -> Int -> (b -> b -> b) -> IntMap b +moveInMap m origKey destKey mergeF + = result + where mOrigValue = IntMap.lookup origKey m + prunedM = IntMap.delete origKey m + result = case mOrigValue of + Nothing -> m + Just origValue -> IntMap.insertWith mergeF destKey origValue prunedM + +doMemoize :: Ord a => (a -> b) -> a -> Map.Map a b -> (b, Map.Map a b) +doMemoize f e m = case Map.lookup e m of + Nothing -> let result = f e in (result, Map.insert e result m) + Just result -> (result, m) + +permutationOf :: Ord a => [a] -> [a] -> Bool +permutationOf l1 l2 = sort l1 == sort l2 + +set :: Ord a => [a] -> Set.Set a +set = Set.fromList + +list :: Ord a => Set.Set a -> [a] +list = Set.toList + +invertMap :: (Ord a, Ord b) => Map.Map a b -> Map.Map b a +invertMap = Map.fromList . map (\(a,b) -> (b,a)) . Map.assocs diff --git a/src/HTab/Branch.hs b/src/HTab/Branch.hs new file mode 100644 --- /dev/null +++ b/src/HTab/Branch.hs @@ -0,0 +1,1158 @@ +{-# OPTIONS_GHC -fglasgow-exts #-} + +---------------------------------------------------- +-- -- +-- Branch.hs -- +-- -- +---------------------------------------------------- + + +module HTab.Branch +( +Branch(..), BranchMonad, createNewProp, createNewPref, createNewNomTestRelevance, BranchInfo(..), +addFormulas, addFormula, addAccFormula, +addDiaRuleCheck, addDiaXRuleCheck, addDownRuleCheck, addDiffRuleCheck, +addParentPrefix, addFirstFormulas, +ScheduledRule(..), TodoList(..), +BranchData(..), +emptyBranch,initialBranchStateFor,prefixes, +reduceDisjunctionProposeLazy, doLazyBranching, +merge, +getUrfather, getUrfatherAndDeps, isInTheModel, relationIsInTheModel, +getModelRepresentative, isNotBlocked, +BlockingMode(..), diaAlreadyDone, diaXAlreadyDone, +downAlreadyDone, +unfulfilledEventualities, ReducedDisjunct(..), +isSymmetric, isTransitive, +deleteUEV, insertUEV_addFormula +) where + +import Control.Monad.Reader(ReaderT, MonadReader) +import Control.Monad.State(StateT) +import Data.List(minimumBy) +import Data.Maybe( mapMaybe ) +import Data.Ord ( comparing ) + +import Data.Map ( Map ) +import qualified Data.Map as Map +import Data.Set ( Set ) +import qualified Data.Set as Set +import Data.IntMap ( IntMap) +import qualified Data.IntMap as IntMap + +import qualified HTab.DisjSet as DS + +import HTab.Statistics(Statistics) +import HTab.CommandLine(CmdLineParams(..)) + +import HTab.Formula + +import HTab.DMap ( DMap(..), toMap ) +import qualified HTab.DMap as DMap +import HTab.Base(moveInMap, almostCartesianProduct, doMemoize, set, list) + +import HTab.Relations ( Relations(..), emptyRels, insertRelation, mergePrefixes, + successors, predecessors, linksFromTo ) +import qualified HTab.Relations as Relations + +data BranchInfo = BranchOK Branch | + BranchClash Branch Prefix DependencySet Formula + +type Clashable_info = DMap {- Prefix Literal -} DependencySet +type Box_constraints = DMap {- Prefix Rel -} [(Formula,DependencySet)] +type Branching_witnesses = DMap {- Prefix Literal -} [PrFormula] +type EquivClasses = DS.DisjSet DS.Pointer +data BlockingMode = AnywhereBlocking | ChainTwinBlocking deriving (Eq,Show) + +data Branch = + Branch {clashStr :: Clashable_info, + -- pending formulas / todo lists + todoList :: TodoList, + -- immediate rules constraints + boxConstrFwd :: Box_constraints, + boxConstrBwd :: Box_constraints, + univCons :: [(DependencySet,Formula)], + -- saturation of rules + diaRlCh :: IntMap {- Prefix -} (Set (Rel,Formula)), + diaXRlCh :: IntMap {- Prefix -} (Set (Rel,Formula)), + boxRlCh :: IntMap {- Prefix -} (Set (Rel,Formula)), + boxXRlCh :: IntMap {- Prefix -} (Set (Rel,Formula)), + downRlCh :: IntMap {- Prefix -} (Set Formula), + atRlCh :: Set Formula, + existRlCh :: Set Formula, + dDiaRlCh :: Map Formula (Maybe Prop), + -- formulas true in an equivalence class + prefToForms :: IntMap {- Prefix -} (Set Formula), + -- backjumping data attached to equivalence classes + prToDepSet :: IntMap {- Prefix -} DependencySet, + -- other data + accStr :: Relations, + -- equivalence classes + nomPrefClasses :: EquivClasses, + -- book keeping + lastPref :: Prefix, + nextNom :: Nom, + nextProp :: Prop, + eventualities :: IntMap DependencySet, + -- lazy branching + brWitnesses :: Branching_witnesses, + -- caching / memoisation data + downVarRelevantCh :: Map Formula Bool, + -- information about language of input formula and blocking mode + inputLanguage :: LanguageInfo, + blockMode :: BlockingMode, + unblockedPrefsLim :: Prefix, + blockedDias :: IntMap {- Prefix -} [PrFormula], + prefParent :: IntMap {- Prefix -} Prefix, + relevantNominals :: Set Nom, + relInfo :: RelInfo, + encoding :: Encoding} + +-- + +emptyBranch :: CmdLineParams -> LanguageInfo -> RelInfo -> Encoding -> Branch +emptyBranch clp fLang relInfo_ encoding_ = + Branch + { clashStr = DMap.empty, + todoList = emptyTodoList clp, + accStr = emptyRels, + boxConstrBwd = DMap.empty, + boxConstrFwd = DMap.empty, + diaRlCh = IntMap.empty, + diaXRlCh = IntMap.empty, + boxRlCh = IntMap.empty, + boxXRlCh = IntMap.empty, + downRlCh = IntMap.empty, + atRlCh = Set.empty, + existRlCh = Set.empty, + dDiaRlCh = Map.empty, + downVarRelevantCh = Map.empty, + univCons = [], + lastPref = 0, + nextNom = maxNom encoding_ + 4, + nextProp = maxProp encoding_ + 4, + prefToForms = IntMap.empty, + prToDepSet = IntMap.empty, + eventualities = IntMap.empty, + brWitnesses = DMap.empty, + nomPrefClasses = DS.mkDSet, + inputLanguage = fLang, + blockMode = blockingMode, + unblockedPrefsLim = 0, + blockedDias = IntMap.empty, + prefParent = IntMap.empty, + relevantNominals = set $ relevantNoms fLang, + relInfo = relInfo_, + encoding = encoding_ + } + where blockingMode = + if languagePast fLang + || languageTrans fLang + || relInfo_ `oneIs` Symmetric + || relInfo_ `oneIs` Functional + || relInfo_ `oneIs` Injective + then ChainTwinBlocking + else AnywhereBlocking + +instance Show Branch where + show br + = concat [ "Input language: ", show (inputLanguage br), + "\nClashable formulas:", showIMap (\v -> "(" ++ showMap_lits v ++ ")") "\n " (toMap $ clashStr br), + "\n", show (todoList br), + showl "\nRelations: " (accStr br), + ifNotEmpty (boxConstrFwd br) + (\c -> "\nBox fwd: " ++ showIMap (\v -> "(" ++ showMap_rel v ++ ")") "\n " (toMap c)), + ifNotEmpty (boxConstrBwd br) + (\c -> "\nBox bwd: " ++ showIMap (\v -> "(" ++ showMap_rel v ++ ")") "\n " (toMap c)), + ifNotEmpty (brWitnesses br) + (\c -> "\nWitnesses: " ++ showIMap (\v -> "(" ++ showMap_lits2 v ++ ")") "\n " (toMap c)), + showl "\nDia rule chart: " (diaRlCh br), + showl "\nDown rule chart: " (downRlCh br), + showl "\n@ rule chart: " (list $ atRlCh br), + showl "\nExist rule chart: " (list $ existRlCh br), + showl "\nDiff dia rule chart: " (dDiaRlCh br), + showl "\nDown var relevant chart: " (downVarRelevantCh br), + showl "\nUniv constraints: " (univCons br), + ifNotEmpty (prToDepSet br) (\m -> "\nPrefix to dependency set:" ++ showIMap dsShow "\n " m), + ifNotEmpty (prefToForms br) (\m -> "\nPrefix to formulas:" ++ showIMap (show . Set.toList) "\n " m), + showl "\nEventualities: " (eventualities br), + showl "\nParent: " (prefParent br), + "\nBlocking mode: ", show (blockMode br), + "\nPrefix-Nominal classes : ", showMap show ", " (nomPrefClasses br), + "\nModel-relevant nominals : " ++ (unwords $ map showLit $ list $ relevantNominals br), + "\nlastPref : " ++ show (lastPref br) ++ + " nextnom : " ++ showLit (nextNom br) ++ + " nextprop : " ++ showLit (nextProp br) + ] + where + ifNotEmpty b f = if empty b then "" else f b + showl intro b = if empty b then "" else intro ++ show b + + showIMap vShow sep = IntMap.foldWithKey (\k v -> (++ sep ++ show k ++ " -> " ++ vShow v )) "" + showMap vShow sep = Map.foldWithKey (\k v -> (++ sep ++ show k ++ " -> " ++ vShow v )) "" + showMap_lits = IntMap.foldWithKey (\l d -> (++ showLit l ++ " " ++ dsShow d ++ ", ")) "" + showMap_lits2 = IntMap.foldWithKey (\l fs -> (++ showLit l ++ " " ++ ":" ++ show fs ++ ", ")) "" + showMap_rel = IntMap.foldWithKey (\r dxs -> (++ "-" ++ showRel r ++ "-> " ++ show dxs ++ ", ")) "" + +class Emptyable a where + empty :: a -> Bool + +instance Emptyable [a] where + empty [] = True + empty _ = False + +instance Emptyable (Map a b) where + empty = Map.null + +instance Emptyable (IntMap b) where + empty = IntMap.null + +instance Emptyable (DMap c) where + empty (DMap m) = IntMap.null m + +instance Emptyable Relations where + empty = Relations.null + +instance Emptyable (Set a) where + empty = Set.null + + +data TodoList = Unfair{disjTodo :: Set PrFormula, + diaTodo :: Set PrFormula, + diaXTodo :: Set PrFormula, + existTodo :: Set PrFormula, + atTodo :: Set PrFormula, + downTodo :: Set PrFormula, + diffTodo :: Set PrFormula, + mergeTodo :: Set (DependencySet, Prefix, DS.Pointer), + roleIncTodo :: Set (DependencySet, Prefix, Prefix, [Rel]) } + | Fair [ScheduledRule] + +instance Show TodoList where + show (Fair srs) = "Todo list: " ++ show srs + show (Unfair disjs dias diaxs es ars downs diffs merges rolein) + = "Todo lists:" ++ concatMap (\el -> "\n" ++ show (list el)) [disjs, dias, diaxs, es, ars, downs, diffs] + ++ "\n" ++ show (list merges) + ++ "\n" ++ show (list rolein) + +data ScheduledRule = SR_Formula PrFormula + | SR_Merge Prefix DS.Pointer DependencySet + | SR_Inclusion Prefix [Rel] Prefix DependencySet + +instance Show ScheduledRule where + show (SR_Formula pf) = show pf + show (SR_Merge pr po _) = "Merge " ++ show (pr,po) + show (SR_Inclusion p1 ss p2 _) = "Role inclusion " ++ show p1 ++ "<" ++ show ss ++ ">" ++ show p2 + +emptyTodoList :: CmdLineParams -> TodoList +emptyTodoList clp = + if fairStrategy clp + then Fair [] + else Unfair { disjTodo = Set.empty, + diaTodo = Set.empty, + diaXTodo = Set.empty, + existTodo = Set.empty, + atTodo = Set.empty, + downTodo = Set.empty, + diffTodo = Set.empty, + mergeTodo = Set.empty, + roleIncTodo = Set.empty + } + +{- + "add formula" functions, that handle + prefixes and nominals +-} + +addFormulas :: CmdLineParams -> Branch -> [PrFormula] -> BranchInfo +addFormulas clp br fs = + foldr (\f bi -> + case bi of + BranchOK br2 -> addFormula clp br2 f + clash -> clash + ) + (BranchOK br) + fs + +addFormula :: CmdLineParams -> Branch -> PrFormula -> BranchInfo +addFormula clp br pf + = putAwayFormula clp pf + $ bookKeepFormula clp pf br + +bookKeepFormula :: CmdLineParams -> PrFormula -> Branch -> Branch +bookKeepFormula clp pf_ br + = addToPrefToForms pf + $ rescheduleLazyBranching clp pf + $ rescheduleBlockedDias ur br + where + (ur,pf) = toUrfather br pf_ + +rescheduleLazyBranching :: CmdLineParams -> PrFormula -> Branch -> Branch +rescheduleLazyBranching clp (PrFormula pr ds (Lit l)) br -- pr already urfather + | lazyBranching clp && isProp l + = + let (Just innerMap) = DMap.lookup1 pr (brWitnesses br) + in + + case DMap.lookup pr l (brWitnesses br) of + Just _ + -> let innerMap2 = IntMap.delete l innerMap + newBrW = DMap.insert1 pr innerMap2 (brWitnesses br) + newBr = br{brWitnesses = newBrW} + in + newBr -- forget the disjunctions, they are really satisfied + Nothing + -> case DMap.lookup pr (negLit l) (brWitnesses br) of + Just fs + -> let innerMap2 = IntMap.delete (negLit l) innerMap + newBrW = DMap.insert1 pr innerMap2 (brWitnesses br) + newBr = br{brWitnesses = newBrW} + in + foldr addToTodo newBr (map (addDeps ds) fs) --reschedule + Nothing + -> br -- do nothing + +rescheduleLazyBranching _ _ br = br + + +putAwayFormula :: CmdLineParams -> PrFormula -> Branch -> BranchInfo +putAwayFormula clp pf@(PrFormula pr ds f2) br = + case f2 of + Con fs -> addFormulas clp br (prefix pr ds fs) + Dis _ -> putAwayDisjunction clp pf br + Dia _ _ -> BranchOK $ addToTodo pf br + DiaX _ _ _ -> BranchOK $ addToTodo pf br + Box r f -> addBoxConstraint pr r f ds clp br + BoxX r f -> addBoxXConstraint pr r f ds clp br + A f -> addUnivConstraint f ds clp br + B f -> b_rule pr f ds clp br + E _ -> BranchOK $ addToTodo pf br + D _ -> BranchOK $ addToTodo pf br + At _ _ -> BranchOK $ addToTodo pf br + Down _ _ -> BranchOK $ addToTodo pf br + Lit l | isPositiveNom l -> addToClashable pr ds l $ addToTodo pf br + Lit l -> addToClashable pr ds l br + +putAwayDisjunction :: CmdLineParams -> PrFormula -> Branch -> BranchInfo +putAwayDisjunction clp pf@(PrFormula pr ds f@(Dis fs)) br + | lazyBranching clp && ur <= unblockedPrefsLim br + = 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) (Dis disjuncts) --todo if there was no reduction, leave ds + in + case mProposed of + Nothing -> BranchOK $ addToTodo fNew br + Just lit -- add pr, lit, ((++) disjuncts) aux witnesses + -> BranchOK $ doLazyBranching ur lit [fNew] br + | otherwise + = BranchOK $ addToTodo pf br + where ur = getUrfather br (DS.Prefix pr) + +putAwayDisjunction _ pf _ = error ("putAwayDisjunction " ++ show pf) + +doLazyBranching :: Prefix -> Literal -> [PrFormula] -> Branch -> Branch +doLazyBranching pr lit pfs br -- assume the tests have been done beforehand + = case DMap.lookup1 pr (brWitnesses br) of + Nothing -> let newBrW = DMap.insert pr lit pfs (brWitnesses br) + in br{brWitnesses = newBrW} + Just innerMap + -> case IntMap.lookup lit innerMap of -- assume this is the only place where l or (negLit l) occur + Nothing -> let newInner = IntMap.insert lit pfs innerMap + newBrW = DMap.insert1 pr newInner (brWitnesses br) + in br{brWitnesses = newBrW} + Just fs -- assume the test was already done + -> let newInner = IntMap.insert lit (pfs++fs) innerMap + newBrW = DMap.insert1 pr newInner (brWitnesses br) + in br{brWitnesses = newBrW} + + +-- TODO +-- when doing a merge, do all the witness checks! +-- when formula is sat and doing model building, add all witnesses! + +{- todo list functions -} + +addToTodo :: PrFormula -> Branch -> Branch +addToTodo pf@(PrFormula p ds f2) br = + if alreadyDone + then br + else brWithSaturation{todoList = newTodoList} + where + newTodoList = + case todoList br of + Fair srs -> case f2 of + Lit l | isPositiveNom l + -> Fair ( srs ++ [SR_Merge p (DS.Nominal l) ds] ) + _ -> Fair ( srs ++ [SR_Formula pf]) + utodo -> + case f2 of + Dis _ -> utodo{ disjTodo = Set.insert pf ( disjTodo utodo)} + Dia _ _ -> utodo{ diaTodo = Set.insert pf ( diaTodo utodo)} + DiaX _ _ _ -> utodo{ diaXTodo = Set.insert pf ( diaXTodo utodo)} + E _ -> utodo{existTodo = Set.insert pf (existTodo utodo)} + D _ -> utodo{ diffTodo = Set.insert pf ( diffTodo utodo)} + At _ _ -> utodo{ atTodo = Set.insert pf ( atTodo utodo)} + Down _ _ -> utodo{ downTodo = Set.insert pf ( downTodo utodo)} + Lit l + | isPositiveNom l -> utodo{mergeTodo = Set.insert (ds,p,DS.Nominal l) (mergeTodo utodo)} + _ -> error $ "addToTodo: " ++ show f2 + alreadyDone = + case f2 of + E _ -> existAlreadyDone br f2 + D _ -> False + At _ _ -> atAlreadyDone br f2 + Down _ _ -> downAlreadyDone br pf + Dia _ _ -> False -- the test happens later, when the todo list is processed + DiaX _ r ev -> diaXAlreadyDone br p (r,ev) + Dis _ -> False -- the test happens later, when the todo list is processed + Lit l + | isPositiveNom l -> inSameClass br p l + _ -> error $ "alreadyDone: " ++ show f2 + brWithSaturation = + case f2 of + E _ -> br{existRlCh = Set.insert f2 (existRlCh br)} + At _ _ -> br{atRlCh = Set.insert f2 (atRlCh br)} + _ -> br + +rescheduleBlockedDias :: Prefix -> Branch -> Branch +rescheduleBlockedDias pr br + = foldr addToTodo br2 toAdd + where toAdd = IntMap.findWithDefault [] pr (blockedDias br) + br2 = br{blockedDias = IntMap.delete pr $ blockedDias br} + +{- helper functions for equivalence class merge -} + +merge :: CmdLineParams -> Branch -> Prefix -> DependencySet -> DS.Pointer -> BranchInfo +merge clp br pr fDs pointer -- pointer is a nominal or a prefix + = let + (DS.Prefix ur1,classes1) = DS.find (DS.Prefix pr) (nomPrefClasses br) + (poAncestor ,classes2) = DS.find pointer classes1 + classes3 = DS.union (DS.Prefix pr) pointer classes2 + in + case poAncestor of + DS.Nominal _ -> BranchOK $ addClassDeps ur1 fDs $ br { nomPrefClasses = classes3 } + -- nominal not yet in the equivalence classes + DS.Prefix ur2 + | ur1 == ur2 -> BranchOK $ addClassDeps ur1 fDs br + | otherwise + -> + let + oldUr = max ur1 ur2 + newUr = min ur1 ur2 + clashableInfoSlots = mapMaybe (\ur -> DMap.lookup1 ur (clashStr br)) [ur1,ur2] + currentDeps = dsUnions $ fDs:(map (findDeps br) [ur1,ur2]) + newPrToDepSet = IntMap.insert newUr currentDeps (prToDepSet br) + newClashableSlotUrfather = cisAddDeps currentDeps $ cisUnions clashableInfoSlots + in + case newClashableSlotUrfather of + Slot_UpdateFailure clashingDeps -> + let newBr = br{nomPrefClasses = classes3} in + BranchClash newBr pr (dsUnion clashingDeps currentDeps) (neg taut) + + Slot_UpdateSuccess urfatherSlot -> + let newClashStr = DMap $ IntMap.delete oldUr $ IntMap.insert newUr urfatherSlot (toMap $ clashStr br) + + -- structures that merge + newPrefToForms = moveInMap (prefToForms br) oldUr newUr Set.union + newBoxConstrFwd = DMap.moveInnerDataDMapPlusDeps fDs (boxConstrFwd br) oldUr newUr + newBoxConstrBwd = DMap.moveInnerDataDMapPlusDeps fDs (boxConstrBwd br) oldUr newUr + newAccStr = mergePrefixes (accStr br) oldUr newUr fDs + newDiaRlCh = moveInMap (diaRlCh br) oldUr newUr Set.union + newDiaXRlCh = moveInMap (diaXRlCh br) oldUr newUr Set.union + newBoxRlCh = moveInMap (boxRlCh br) oldUr newUr Set.union + newBoxXRlCh = moveInMap (boxXRlCh br) oldUr newUr Set.union + newBlockedDias = moveInMap (blockedDias br) oldUr newUr (++) + (newBrWitnesses,unwitnessedToAdd) = mergeWitnesses oldUr newUr urfatherSlot (brWitnesses br) + + -- structures that combine + mapBoxFwd = map (\idx -> IntMap.findWithDefault IntMap.empty idx (toMap $ boxConstrFwd br) ) [ur1,ur2] + mapAccFwd = map (successors (accStr br)) [ur1,ur2] + formulasToSend1 = concatMap (boxRule currentDeps) $ almostCartesianProduct mapBoxFwd mapAccFwd + + mapBoxBwd = map (\idx -> IntMap.findWithDefault IntMap.empty idx (toMap $ boxConstrBwd br) ) [ur1,ur2] + mapAccBwd = map (predecessors (accStr br)) [ur1,ur2] + formulasToSend2 = concatMap (boxRule currentDeps) $ almostCartesianProduct mapBoxBwd mapAccBwd + + formulasToAdd = nubAndMergeDeps $ formulasToSend1 + ++ formulasToSend2 + ++ unwitnessedToAdd + + newBr = br{nomPrefClasses = classes3, + boxConstrFwd = newBoxConstrFwd, + boxConstrBwd = newBoxConstrBwd, + accStr = newAccStr, + prToDepSet = newPrToDepSet, + prefToForms = newPrefToForms, + diaRlCh = newDiaRlCh, + diaXRlCh = newDiaXRlCh, + boxRlCh = newBoxRlCh, + boxXRlCh = newBoxXRlCh, + blockedDias = newBlockedDias, + clashStr = newClashStr, + brWitnesses = newBrWitnesses} + in + addFormulas clp newBr formulasToAdd + +mergeWitnesses :: Prefix -> Prefix -> Clashable_info_slot -> Branching_witnesses -> (Branching_witnesses, [PrFormula]) +mergeWitnesses oldUr newUr urfatherSlot dbrWits@(DMap brWits) + =( DMap.insert1 newUr newDest2 ( DMap.delete oldUr dbrWits ), toAdd1 ++ toAdd2 ) + where + srcInnerMap = maybe IntMap.empty id (IntMap.lookup oldUr brWits) + destInnerMap = maybe IntMap.empty id (IntMap.lookup newUr brWits) + (newDest1,toAdd1) = mergeWitnesses_WitnessesMap srcInnerMap destInnerMap + (newDest2,toAdd2) = mergeWitnesses_AgainstClashable newDest1 urfatherSlot + +mergeWitnesses_WitnessesMap :: IntMap [PrFormula] -> IntMap [PrFormula] -> (IntMap [PrFormula], [PrFormula]) +mergeWitnesses_WitnessesMap srcWitMap destWitMap + = foldr go (destWitMap,[]) $ IntMap.assocs srcWitMap + where + go (l,fs) (destMap,toAddAgain) + = case IntMap.lookup l destMap of + Just fs2 -> (IntMap.insert l (fs2++fs) destMap, toAddAgain) + Nothing + -> case IntMap.lookup (negLit l) destMap of -- (negLit l) is just one bit away from l in the map, but we don't use it + Just fs2 -> (IntMap.delete (negLit l) destMap, fs++fs2++toAddAgain) + Nothing -> (IntMap.insert l fs destMap, toAddAgain) + +mergeWitnesses_AgainstClashable :: IntMap [PrFormula] -> Clashable_info_slot -> (IntMap [PrFormula],[PrFormula]) +mergeWitnesses_AgainstClashable witMap cis + = foldr go (witMap,[]) $ IntMap.assocs witMap + where + go (lit,fs) (destMap,toAddAgain) + | lit `IntMap.member` cis = (IntMap.delete lit destMap,toAddAgain) + | negLit lit `IntMap.member` cis = (IntMap.delete lit destMap,fs++toAddAgain) -- same remark as above + | otherwise = (destMap,toAddAgain) + +nubAndMergeDeps :: [PrFormula] -> [PrFormula] +-- Rationale : because of the equivalence classes, a same formula can be added to a branch +-- as several prefixed formulas with different branching dependencies. This functions takes +-- a list of prefixes formulas, looks which inner formulas are the same and merge their +-- branching dependencies. +nubAndMergeDeps prfs = namd prfs (Map.empty::Map (Prefix,Formula) DependencySet) + +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),ds) -> PrFormula p ds f) (Map.assocs theMap) + +{- + Functions related to nom, prefixes and nominals ... +-} + +toUrfather :: Branch -> PrFormula -> (Prefix,PrFormula) +toUrfather br f@(PrFormula pr ds f2) + = (urfather, newF) + where + (urfather,ds2,_) = getUrfatherAndDeps br (DS.Prefix pr) + newF = if urfather == pr + then f else PrFormula urfather (dsUnion ds ds2) f2 + +addToPrefToForms :: PrFormula -> Branch -> Branch +addToPrefToForms (PrFormula pr _ f) br | forInclusion br f = + br{prefToForms = newMap} + where currentPtf = prefToForms br + newMap = IntMap.insertWith Set.union pr (Set.singleton f) currentPtf +addToPrefToForms _ br = br + +{- handling nominal urfathers, equivalence classes and dependencies -} + +isNominalUrfather :: Branch -> Prefix -> Bool +isNominalUrfather b p = DS.isRoot (DS.Prefix p) classes + where classes = nomPrefClasses b + + +-- May look redundant with getUrfatherAndDeps, but it is important not +-- to make the test isRoot for performance +getUrfather :: Branch -> DS.Pointer -> Prefix +getUrfather br p = + ur + where + (DS.Prefix ur) = DS.onlyFind p (nomPrefClasses br) + +getUrfatherAndDeps :: Branch -> DS.Pointer -> (Prefix,DependencySet,EquivClasses) +getUrfatherAndDeps br p = + if DS.isRoot p classes then defaultAnswer + else (ur,deps,newClasses) + where classes = nomPrefClasses br + (urfather, newClasses) = DS.find p classes + (DS.Prefix ur) = urfather + DS.Prefix unboxedP = p + defaultAnswer = (unboxedP,dsEmpty,classes) + deps = findDeps br ur + +findDeps :: Branch -> Prefix -> DependencySet +findDeps br pr = IntMap.findWithDefault dsEmpty pr (prToDepSet br) + +addClassDeps :: Prefix -> DependencySet -> Branch -> Branch +addClassDeps pr ds br = br { prToDepSet = IntMap.insertWith dsUnion pr ds (prToDepSet br) } + +inSameClass :: Branch -> Prefix -> Int -> Bool +inSameClass br p n + = case fst $ DS.find (DS.Nominal (atom n)) (nomPrefClasses br) of + DS.Nominal _ -> False + DS.Prefix p2 -> getUrfather br (DS.Prefix p) == p2 + +-- <*>-related functions + +deleteUEV :: Branch -> Int -> Branch +deleteUEV br idx = br{eventualities = IntMap.delete idx (eventualities br)} + +insertUEV_addFormula :: Branch -> CmdLineParams -> Maybe Int -> DependencySet -> (Int -> PrFormula) -> BranchInfo +insertUEV_addFormula br clp mi ds ff + = addFormula clp br2 f + where idxToUse = case mi of + Nothing -> case IntMap.maxViewWithKey $ eventualities br of + Nothing -> 0 + Just ((i,_),_) -> i+1 + Just idx -> idx + newEvs = IntMap.insertWith dsUnion idxToUse ds $ eventualities br + br2 = br{eventualities= newEvs} + f = ff idxToUse + +{- box-related constraints -} + +boxRule :: DependencySet -> (IntMap {- Rel -} [(Formula,DependencySet)], IntMap {- Rel -} [(Prefix,DependencySet)]) -> [PrFormula] +boxRule deps (mapBox, mapAcc) + = [PrFormula p (dsUnions [deps,ds1,ds2]) f | + r1 <- IntMap.keys mapBox, + r2 <- IntMap.keys mapAcc, + r1 == r2, + (f,ds1) <- (IntMap.!) mapBox r1, + (p,ds2) <- (IntMap.!) mapAcc r2 ] + +addBoxConstraint :: Prefix -> Rel -> Formula -> DependencySet -> CmdLineParams -> Branch -> BranchInfo +addBoxConstraint pr_ r f ds clp br_ + | boxAlreadyDone br_ pr (r,f) = BranchOK br_ + | isForward r + = let newBr = br{boxConstrFwd = updateBoxConstr pr r f ds (boxConstrFwd br)} + accessiblePrDs = IntMap.findWithDefault [] r $ successors (accStr br) pr + toAdd = symApplications ++ transApplications ++ boxApplications + transApplications = if isTransitive (relInfo br) r + then map (\(p,ds2) -> PrFormula p (dsUnion ds ds2) (Box r f)) accessiblePrDs + else [] + symApplications = [PrFormula pr ds $ Box (invRel r) f | isSymmetric (relInfo br) r] + boxApplications = map (\(p,ds2) -> PrFormula p (dsUnion ds ds2) f) accessiblePrDs + in + addFormulas clp newBr toAdd + + | otherwise + = let newBr = br{boxConstrBwd = updateBoxConstr pr (atom r) f ds (boxConstrBwd br)} + accessiblePrDs = IntMap.findWithDefault [] (atom r) $ predecessors (accStr br) pr + toAdd = transApplications ++ boxApplications -- no symApplications cause inv rewritten as forward during parsing + transApplications = if isTransitive (relInfo br) (atom r) + then map (\(p,ds2) -> PrFormula p (dsUnion ds ds2) (Box r f)) accessiblePrDs + else [] + boxApplications = map (\(p,ds2) -> PrFormula p (dsUnion ds ds2) f) accessiblePrDs + in + addFormulas clp newBr toAdd + where pr = getUrfather br_ (DS.Prefix pr_) + br = addBoxRuleCheck br_ pr (r,f) + +updateBoxConstr :: Prefix -> Rel -> Formula -> DependencySet -> Box_constraints -> Box_constraints +updateBoxConstr p1_ r_ f_ ds_ (DMap boxConstr_) = + case IntMap.lookup p1_ boxConstr_ of + Nothing -> DMap $ IntMap.insert p1_ (IntMap.singleton r_ [(f_,ds_)]) boxConstr_ + Just innerMap -> + case IntMap.lookup r_ innerMap of + Nothing -> DMap $ IntMap.insert p1_ (IntMap.insert r_ [(f_,ds_)] innerMap) boxConstr_ + Just innerInnerList -> DMap $ IntMap.insert p1_ (IntMap.insert r_ ((f_,ds_):innerInnerList) innerMap) boxConstr_ + +addBoxRuleCheck :: Branch -> Prefix -> (Rel,Formula) -> Branch +addBoxRuleCheck br ur (r,f) = + br{boxRlCh=IntMap.insertWith Set.union ur (Set.singleton (r,f)) (boxRlCh br)} + +boxAlreadyDone :: Branch -> Prefix -> (Rel,Formula) -> Bool +boxAlreadyDone b ur (r,f) = + case IntMap.lookup ur (boxRlCh b) of + Nothing -> False + Just fset -> Set.member (r,f) fset + +-- [*]phi --> phi & [][*]phi +-- need not to do all that addBoxConstraint does +addBoxXConstraint :: Prefix -> Rel -> Formula -> DependencySet -> CmdLineParams -> Branch -> BranchInfo +addBoxXConstraint pr r f ds clp br + | boxXAlreadyDone br ur (r,f) = BranchOK br + | otherwise = addFormulas clp br2 [PrFormula pr ds f, PrFormula pr ds (Box r (BoxX r f))] + where ur = getUrfather br (DS.Prefix pr) + br2 = addBoxXRuleCheck br ur (r,f) + +addBoxXRuleCheck :: Branch -> Prefix -> (Rel,Formula) -> Branch +addBoxXRuleCheck br ur (r,f) = + br{boxXRlCh=IntMap.insertWith Set.union ur (Set.singleton (r,f)) (boxXRlCh br)} + +boxXAlreadyDone :: Branch -> Prefix -> (Rel,Formula) -> Bool +boxXAlreadyDone b ur (r,f) = + case IntMap.lookup ur (boxXRlCh b) of + Nothing -> False + Just fset -> Set.member (r,f) fset + +addAccFormula :: CmdLineParams -> Branch -> AccFormula -> BranchInfo +addAccFormula clp br (AccFormula ds r p1_ p2_) + | isBackwards r = addAccFormula clp br (AccFormula ds (invRel r) p2_ p1_) + | otherwise -- forward + = addFormulas clp newBr toAdd + where toAdd = transApplications ++ boxApplications + transApplications = if isTransitive (relInfo br) r + then + ( ( map (\(f,ds2) -> PrFormula p2 (dsUnion ds ds2) (Box r f)) toSendFwd ) + ++ ( map (\(f,ds2) -> PrFormula p1 (dsUnion ds ds2) (Box r f)) toSendBwd ) ) + else [] + boxApplications = ( ( map (\(f,ds2) -> PrFormula p2 (dsUnion ds ds2) f) toSendFwd ) + ++ ( map (\(f,ds2) -> PrFormula p1 (dsUnion ds ds2) f) toSendBwd ) ) + p1 = getUrfather br (DS.Prefix p1_) + p2 = getUrfather br (DS.Prefix p2_) + toSendFwd = IntMap.findWithDefault [] r $ IntMap.findWithDefault IntMap.empty p1 (toMap $ boxConstrFwd br) + toSendBwd = IntMap.findWithDefault [] r $ IntMap.findWithDefault IntMap.empty p2 (toMap $ boxConstrBwd br) + newBr = scheduleInclusionRule p1 p2 r ds $ insertRelationBranch br p1 r p2 ds + + +scheduleInclusionRule :: Prefix -> Prefix -> Rel -> DependencySet -> Branch -> Branch +scheduleInclusionRule p1 p2 r ds br -- todo get all included + = if null toschedule + then br + else br{todoList = newTodoList} + where parentss = case Map.lookup r (relInfo br) of + Nothing -> [] + Just props -> [ rs | SubsetOf rs <- props] + toschedule = map (\parents -> (ds,p1,p2,parents)) $ filter (not . alreadyDone) parentss + alreadyDone = any (`elem` linksFromTo (accStr br) p1 p2) + newTodoList = + case todoList br of + Fair srs -> Fair (srs ++ map (\(ds_,p1_,p2_,parents_) -> SR_Inclusion p1_ parents_ p2_ ds_) toschedule ) + utodo -> utodo{roleIncTodo = Set.union (Set.fromList toschedule) (roleIncTodo utodo)} + +insertRelationBranch :: Branch -> Prefix -> Rel -> Prefix -> DependencySet -> Branch +insertRelationBranch br p1 r p2 ds + = br{accStr = insertRelation (accStr br) p1 r p2 ds} + + +{- blocking conditions -} + +isNotBlocked :: Branch -> Prefix -> Bool +isNotBlocked br pr + | pr <= unblockedPrefsLim br = True + | otherwise = + case blockMode br of + AnywhereBlocking -> null $ filter isSubsumer labels + where ur = getUrfather br (DS.Prefix pr) + fs = formulasOf br ur + isSubsumer fs_ = fs `Set.isSubsetOf` fs_ + labels = map snd $ takeWhile ((< ur).fst) $ ascPrefToForm br + ChainTwinBlocking -> isNotChainTwinBlocked br pr + +isNotChainTwinBlocked :: Branch -> Prefix -> Bool +isNotChainTwinBlocked br pr = not $ test2equal $ map (formulasOf br) (getAllParents br pr) + +getAllParents :: Branch -> Prefix -> [Prefix] +-- getAllParents up to one that has an input nominal +getAllParents br pr = (getUrfather br (DS.Prefix pr)):rest + where rest = case IntMap.lookup pr (prefParent br) of + Nothing -> [] + Just parent -> if isNominalUrfather br parent + then getAllParents br parent + else [getUrfather br (DS.Prefix parent)] + + +test2equal :: (Ord a) => [Set a] -> Bool -- inefficient +test2equal (s:sets) = any (s ==) sets || test2equal sets +test2equal [] = False + + +{- model building -} + +isInTheModel :: Branch -> Prefix -> Bool +isInTheModel br pr | isNominalUrfather br pr + = case blockMode br of + AnywhereBlocking -> getModelRepresentative br pr == pr + ChainTwinBlocking -> case findModelRepresentativeChainTwinBlocking br pr of + Nothing -> False + Just repr -> repr == pr +isInTheModel _ _ = False + +relationIsInTheModel :: Branch -> (Prefix,Rel,Prefix) -> Bool +relationIsInTheModel br (p1,_,p2) + = case blockMode br of + ChainTwinBlocking -> hasIdentityUrfather br p1 && hasIdentityUrfather br p2 + AnywhereBlocking -> isInTheModel br p1 + where hasIdentityUrfather br_ pr_ + = case findModelRepresentativeChainTwinBlocking br_ pr_ of {Nothing -> False ; _ -> True } + +getModelRepresentative :: Branch -> Prefix -> Prefix -- which is also an inclusion representative +getModelRepresentative br pr + = case blockMode br of + AnywhereBlocking-> case map fst $ filter (Set.isSubsetOf fs . snd) $ ascPrefToForm br of + [] -> pr + (hd:_) -> hd + where ur = getUrfather br (DS.Prefix pr) + fs = formulasOf br ur + ChainTwinBlocking -> case findModelRepresentativeChainTwinBlocking br pr of + Nothing -> error ("found an interesting counter example " ++ show pr) + Just repr -> repr + + +findModelRepresentativeChainTwinBlocking :: Branch -> Prefix -> Maybe Prefix +findModelRepresentativeChainTwinBlocking br pr + = go br pr 0 + where + go :: Branch -> Prefix -> Prefix -> Maybe Prefix + go br_ initial current = + let urCurrent = getUrfather br (DS.Prefix current) in + if urCurrent == initial + then if isNotChainTwinBlocked br initial then Just initial else Nothing + else if areTwins br_ initial urCurrent && isNotChainTwinBlocked br urCurrent + then Just urCurrent + else go br_ initial (current+1) + +areTwins :: Branch -> Prefix -> Prefix -> Bool +areTwins br p1 p2 = formulasOf br p1 == formulasOf br p2 + + +ascPrefToForm :: Branch -> [(Prefix,Set Formula)] +ascPrefToForm br = [ (pr,formulasOf br pr) | pr <- prefixes br ] + +-- maybe should get the urfather of given prefix, so that the caller functions won't have to do it +formulasOf :: Branch -> Prefix -> Set Formula +formulasOf br p = IntMap.findWithDefault Set.empty p (prefToForms br) + +-- is the formula useful to calculate inclusion urfathers ? +forInclusion :: Branch -> Formula -> Bool +forInclusion br (Lit l) + | isProp l = True + | isNominal l = Set.member (atom l) (relevantNominals br) + | otherwise = False -- top, bottom +forInclusion _ (Con _) = False +forInclusion _ (Dis _) = False +forInclusion _ (At _ _) = False +forInclusion _ (Down _ _) = False +forInclusion _ (Box _ _) = True +forInclusion _ (Dia _ _) = True +forInclusion _ (BoxX _ _) = False +forInclusion _ (DiaX _ _ _) = False +forInclusion _ (A _) = False +forInclusion _ (E _) = False +forInclusion _ (D _) = False +forInclusion _ (B _) = False + +addParentPrefix :: Branch -> Prefix -> Prefix -> Branch +addParentPrefix br son father = br{prefParent = IntMap.insert son father (prefParent br)} + +{- modifications done by rule application -} + +addDiaRuleCheck :: Branch -> Prefix -> (Rel,Formula) -> Branch +addDiaRuleCheck br pr (r,f) = + br{diaRlCh=IntMap.insertWith Set.union ur (Set.singleton (r,f)) (diaRlCh br)} + where ur = getUrfather br (DS.Prefix pr) + +diaAlreadyDone :: Branch -> PrFormula -> Bool +diaAlreadyDone b (PrFormula p _ (Dia r f)) = + case IntMap.lookup ur (diaRlCh b) of + Nothing -> False + Just fset -> Set.member (r,f) fset + where ur = getUrfather b (DS.Prefix p) + +diaAlreadyDone _ _ = error "dia already done : wrong formula kind" +-- + +addDiaXRuleCheck :: Branch -> Prefix -> (Rel, Formula) -> Branch +addDiaXRuleCheck br pr f = + br{diaXRlCh=IntMap.insertWith Set.union ur (Set.singleton f) (diaXRlCh br)} + where ur = getUrfather br (DS.Prefix pr) + +diaXAlreadyDone :: Branch -> Prefix -> (Rel,Formula) -> Bool +diaXAlreadyDone b p f = + case IntMap.lookup ur (diaXRlCh b) of + Nothing -> False + Just fset -> Set.member f fset + where ur = getUrfather b (DS.Prefix p) + + + +unfulfilledEventualities :: Branch -> Maybe DependencySet +unfulfilledEventualities br + = if IntMap.null $ eventualities br + then Nothing + else Just $ dsUnions $ IntMap.elems $ eventualities br + +-- + +addDownRuleCheck :: Branch -> Prefix -> Formula -> Branch +addDownRuleCheck br pr f = + br{downRlCh=IntMap.insertWith Set.union ur (Set.singleton f) (downRlCh br)} + where ur = getUrfather br (DS.Prefix pr) + +downAlreadyDone :: Branch -> PrFormula -> Bool +downAlreadyDone b (PrFormula p _ f@(Down _ _)) = + case IntMap.lookup ur (downRlCh b) of + Nothing -> False + Just fset -> Set.member f fset + where ur = getUrfather b (DS.Prefix p) + +downAlreadyDone _ _ = error "down already done : wrong formula kind" + +-- + +existAlreadyDone :: Branch -> Formula -> Bool +existAlreadyDone b f@(E _) = Set.member f (existRlCh b) +existAlreadyDone _ _ = error "exist already done : wrong formula kind" + +-- + +atAlreadyDone :: Branch -> Formula -> Bool +atAlreadyDone b f@(At _ _) = Set.member f (atRlCh b) +atAlreadyDone _ _ = error "at already done : wrong formula kind" + +-- + +addUnivConstraint :: Formula -> DependencySet -> CmdLineParams -> Branch -> BranchInfo +addUnivConstraint f ds clp br + = addFormulas clp newBr + ( map (\p -> PrFormula p ds f) urfathers ) + where newBr = br{univCons = (ds,f):(univCons br)} + prefs = [0..(lastPref br)] + urfathers = filter (isNominalUrfather br) prefs + +-- + +b_rule :: Prefix -> Formula -> DependencySet -> CmdLineParams -> Branch -> BranchInfo +b_rule pr f ds clp br + = addFormula clp br2 (PrFormula pr ds $ Down newNom $ A (Lit newNom `disj` f)) + where newNom = nextNom br + br2 = br{nextNom = nextNom br + 4} +-- + +addDiffRuleCheck :: Branch -> Formula -> Maybe Prop -> Branch +addDiffRuleCheck br f mp = br{dDiaRlCh=Map.insert f mp (dDiaRlCh br)} + +-- + +createNewPref :: CmdLineParams -> Branch -> BranchInfo +createNewPref clp br + = addFormulas clp newBrWithRefl + ( map (\(ds,f) -> PrFormula newPr ds f) univConstraints ) + where newPr = lastPref br + 1 + newBr = br{lastPref = newPr} + univConstraints = univCons br + newBrWithRefl = addReflexiveLinks newPr newBr + +addReflexiveLinks :: Prefix -> Branch -> Branch +addReflexiveLinks pr br + = foldr (\rel_ br_ -> insertRelationBranch br_ pr rel_ pr dsEmpty) br reflRels + where reflRels = Map.keys $ Map.filter (elem Reflexive) (relInfo br) + + +-- + +createNewProp :: Branch -> Branch +createNewProp br = br{nextProp = nextProp br + 4} + +createNewNomTestRelevance :: Branch -> Formula -> Branch +createNewNomTestRelevance br f + = br{nextNom = nextNom br + 4, + relevantNominals = if relevant then Set.insert newNom (relevantNominals br) else relevantNominals br, + downVarRelevantCh = newDVRC + } + where (relevant, newDVRC) = doMemoize checkIfVariableNegatedOnce f (downVarRelevantCh br) + newNom = nextNom br + +-- + +-- preparation of the branch at the beginning of the calculus: +-- - add the input formula at prefix 0 +-- - 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) -- <= TODO currently not the case. Get the nominals from the encoding +-- - add reflexive links for prefixes 0 and nominal witnesses +-- - add functionality and injectivitty down-arrow formulas +addFirstFormulas :: CmdLineParams -> Branch -> LanguageInfo -> Formula -> BranchInfo +addFirstFormulas clp br_ fLang f + = addFormulas clp br5 ([pf]++funUniv++injUniv) + where ns = languageNoms fLang + nbNs = length ns + nomWitnesses = [1..nbNs] + br = foldr addReflexiveLinks ( br_{lastPref = nbNs} ) (0:nomWitnesses) + pf = firstPrefixedFormula f + newClasses = foldr (\(pr,n) -> DS.union (DS.Prefix pr) (DS.Nominal n)) + (nomPrefClasses br) + (zip [1..] ns) + newClashStr = foldr (\(pr,n) -> DMap.insert pr n dsEmpty) + DMap.empty + (zip [1..] ns) + br2 = br{nomPrefClasses = newClasses, + clashStr = newClashStr} + br3 = foldr (\(pr,n) -> bookKeepFormula clp (PrFormula pr dsEmpty (Lit n))) + br2 + (zip [1..] ns) + funUniv = map (\r -> PrFormula 0 dsEmpty + $ A $ Down newNom $ Box (inv r (relInfo br)) $ Box r (Lit newNom)) funRels + where funRels = Map.keys $ Map.filter (elem Functional) (relInfo br) + injUniv = map (\r -> PrFormula 0 dsEmpty + $ A $ Down newNom $ Box r $ Box (inv r (relInfo br)) (Lit newNom)) injRels + where injRels = Map.keys $ Map.filter (elem Injective) (relInfo br) + newNom = nextNom br3 + br4 = br3{nextNom = nextNom br3 + 4} + br5 = br4{unblockedPrefsLim = nbNs} + +{- functions to handle the "clashable information", ie literals associated to prefixes -} + +data UpdateResult = UpdateSuccess Clashable_info | UpdateFailure DependencySet + +addToClashable :: Prefix -> DependencySet -> Literal -> Branch -> BranchInfo +addToClashable pr_ ds1 l br + = case updateMap (clashStr br) pr ds l of + UpdateSuccess cs -> BranchOK br{clashStr = cs} + UpdateFailure dsf -> BranchClash br pr dsf (Lit l) + where (pr,ds2,_) = getUrfatherAndDeps br (DS.Prefix pr_) + ds = ds1 `dsUnion` ds2 + + +-- Insert a piece of clashable information into all the clashable information of a branch + +updateMap :: Clashable_info -> Prefix -> DependencySet -> Literal -> UpdateResult +updateMap cs _ ds l | isTop l = UpdateSuccess cs + | isBottom l = UpdateFailure ds +updateMap (DMap cs) pre ds l + = case IntMap.lookup pre cs of + Nothing -> UpdateSuccess $ DMap $ IntMap.insert pre (IntMap.singleton l ds) cs + Just slot -> case cisUpdate slot l ds of + Slot_UpdateSuccess updatedSlot -> UpdateSuccess $ DMap $ IntMap.insert pre updatedSlot cs + Slot_UpdateFailure failureDeps -> UpdateFailure failureDeps + + +type Clashable_info_slot = IntMap {- Literal -} DependencySet +data Slot_UpdateResult = Slot_UpdateSuccess Clashable_info_slot + | Slot_UpdateFailure DependencySet + + +-- Union a list of clashable info slots +cisUnions :: [Clashable_info_slot] -> Slot_UpdateResult +cisUnions [] = Slot_UpdateSuccess IntMap.empty +cisUnions [cis] = Slot_UpdateSuccess cis +cisUnions (cis1:cis2:tl) + = case cisUnion cis1 cis2 of + failure@(Slot_UpdateFailure _) -> failure + Slot_UpdateSuccess newCis -> cisUnions (newCis:tl) + +-- Union two clashable info slots + +-- if there is a clash, the result reports the set of dependencies whose earliest dependency is the earliest +-- among all dependencies sets that caused the clash +cisUnion :: Clashable_info_slot -> Clashable_info_slot -> Slot_UpdateResult +cisUnion cis1 cis2 + = ucis_helper cis1 (IntMap.assocs cis2) + where ucis_helper :: Clashable_info_slot -> [(Literal,DependencySet)] -> Slot_UpdateResult + ucis_helper cis l_ds_s = + let (updateStatus,clashing_ds_s) + = foldr (\(l,ds) (upResult,clashingBps_s) + -> case upResult of + Slot_UpdateSuccess cis_ -> (cisUpdate cis_ l ds, clashingBps_s) + Slot_UpdateFailure ds_s -> (cisUpdate cis l ds, ds_s:clashingBps_s) + -- we reuse the input Clashabe Info Slot + ) + (Slot_UpdateSuccess cis,[]) l_ds_s + result = case clashing_ds_s of + [] -> updateStatus -- is 'success' + ds_s -> Slot_UpdateFailure $ findEarliestSet ds_s + where findEarliestSet = minimumBy compareBPSets + compareBPSets ds1 ds2 = comparing dsMin ds1 ds2 + in + result + + +-- Insert a piece of information in a clashable info slot + +cisUpdate :: Clashable_info_slot -> Literal -> DependencySet -> Slot_UpdateResult +cisUpdate cis l ds | isTop l = Slot_UpdateSuccess cis + | isBottom l = Slot_UpdateFailure ds +cisUpdate cis l ds -- nominals, propositional symbols + = case IntMap.lookup (negLit l) cis of + Just ds2 -> Slot_UpdateFailure $ dsUnion ds ds2 + Nothing -> Slot_UpdateSuccess $ IntMap.insertWith mergeDeps l ds cis + where mergeDeps d1 d2 = if dsMin d1 < dsMin d2 then d1 else d2 + -- if the same information is caused by an earlier + -- branching, only keep the information of the earliest set of dependencies + +-- Other functions related to clashable information + +cisAddDeps :: DependencySet -> Slot_UpdateResult -> Slot_UpdateResult +cisAddDeps ds res_cis = + case res_cis of + Slot_UpdateSuccess cis -> Slot_UpdateSuccess $ IntMap.map (dsUnion ds) cis + failure -> failure + + + +cisQuery :: Branch -> Prefix -> Literal -> Maybe (Bool,DependencySet) +-- Output : Nothing = nevermind ; Just True = already there ; Just False = contrary there +cisQuery _ _ l | isTop l = Just (True,dsEmpty) + | isBottom l = Just (False,dsEmpty) +cisQuery br pr l + = case DMap.lookup pr l (clashStr br) of + Just ds -> Just (True,ds) + Nothing -> case DMap.lookup pr (negLit l) (clashStr br) of + Just ds -> Just (False,ds) + Nothing -> Nothing + +{- function used for unit propagation -} + + +data ReducedDisjunct + = Triviality + | Contradiction DependencySet + | Reduced DependencySet (Set Formula) (Maybe Prop) -- proposable witness for lazy branching + deriving Show + +reduceDisjunctionProposeLazy :: Branch -> Prefix -> Set Formula -> ReducedDisjunct +reduceDisjunctionProposeLazy br pr fs + = case Set.fold go (Just ( Set.empty , dsEmpty, Nothing )) fs of + Nothing -> Triviality + Just (disjuncts,ds,proposed) + | Set.null disjuncts -> Contradiction ds + | otherwise -> Reduced ds disjuncts proposed -- what if not reduced ? and no proposed witness ? + where + ur = getUrfather br (DS.Prefix pr) + go _ Nothing = Nothing + go l@(Lit current) (Just (disjuncts,ds_,proposed)) + = case (cisQuery br ur current, proposed) of + (Just (True,_) ,_) -> Nothing + (Just (False,ds2) ,_) -> Just (disjuncts,dsUnion ds_ ds2, proposed) + (Nothing, Nothing) + -> if isPositiveNom current + then Just (Set.insert l disjuncts,ds_,Nothing) -- no lazy branching with positive nominals + else case DMap.lookup ur (negLit current) (brWitnesses br) of + -- if current is a negated nominal, we know the "just" case is impossible + Just _ -> Just (Set.insert l disjuncts,ds_,Nothing) -- there's an opposed witness + Nothing -> Just (Set.insert l disjuncts,ds_, Just current) -- propose for witness + _ {- already a proposed witness -} + -> Just (Set.insert l disjuncts,ds_,proposed) + go f (Just (disjuncts,ds_,proposed)) = Just (Set.insert f disjuncts, ds_,proposed) + + +{- other functions -} +prefixes :: Branch -> [Prefix] +prefixes br = [0..(lastPref br)] + +oneIs :: RelInfo -> RelProperty -> Bool +oneIs relI p = any ( elem p . snd) $ Map.toList relI + +hasProperty :: RelProperty -> RelInfo -> Rel -> Bool +hasProperty p relI r = case Map.lookup r relI of + Nothing -> False + Just properties -> p `elem` properties + +isSymmetric :: RelInfo -> Rel -> Bool +isSymmetric = hasProperty Symmetric + +isTransitive :: RelInfo -> Rel -> Bool +isTransitive = hasProperty Transitive + +{- Monad related stuff -} + +data BranchData = BranchData { branch_clp :: CmdLineParams } + +type BranchMonad a = ReaderT BranchData (StateT Statistics IO) a + +initialBranchStateFor :: (MonadReader BranchData m) => (m a -> BranchData -> b) -> BranchData -> m a -> b +initialBranchStateFor f bd = flip f bd + diff --git a/src/HTab/CommandLine.hs b/src/HTab/CommandLine.hs new file mode 100644 --- /dev/null +++ b/src/HTab/CommandLine.hs @@ -0,0 +1,87 @@ +---------------------------------------------------- +-- -- +-- CommandLine.hs: -- +-- Functions that handle command line processing -- +-- and presentation +-- -- +---------------------------------------------------- + +module HTab.CommandLine ( + CmdLineParams(..), UnitProp(..), + defaultParams, configureStats, checkParams +) where + +import System.Console.CmdArgs + +import HTab.Base( permutationOf ) +import HTab.Statistics( StatisticsState, setPrintOutInterval ) + +data CmdLineParams = CLP { + filename :: Maybe FilePath, + genModel :: Maybe FilePath, + timeout :: Int, + stats :: Int, + strategy :: String, + fairStrategy :: Bool, + semBranch :: Bool, + backjumping :: Bool, + lazyBranching :: Bool, + unitProp :: UnitProp, + noLoopCheck :: Bool, + showFormula :: Bool, + allTransitive :: Bool, + allReflexive :: Bool, + allSymmetric :: Bool, + allFunctional :: Bool, + allInjective :: Bool + } deriving (Show, Data, Typeable) + +data UnitProp = Eager | UPYes | UPNo deriving (Data, Typeable, Eq, Show) + +defaultParams :: CmdLineParams +defaultParams + = CLP{ + filename = Nothing &= name "f" &= typFile &= help "input file", + genModel = Nothing &= name "m" &= typFile &= help "output model file", + timeout = 0 &= name "t" &= help "timeout (in seconds, default=none)", + stats = 0 &= help "display statistics every n steps (default=none)", + strategy = strategyVal &= help "specify rule order", + fairStrategy = False &= help "enable fair strategy", + semBranch = True &= help "enable semantic branching (default)", + backjumping = True &= help "enable backjumping (default)", + lazyBranching = True &= help "enable lazy branching (default)" , + unitProp = enum [Eager &= explicit &= name "eager" &= help "unit propagation: eager (default)", + UPYes &= explicit &= name "unit-prop" &= help "unit propagation: enabled", + UPNo &= explicit &= name "no-unit-prop" &= help "unit propagation: disabled"] , + noLoopCheck = False &= help "disable all loop check", + showFormula = False &= help "display formula", + allTransitive = False &= help "make all relations transitive", + allReflexive = False &= help "make all relations reflexive", + allSymmetric = False &= help "make all relations symmetric", + allFunctional = False &= help "make all relations functional", + allInjective = False &= help "make all relations injective" + } &= verbosity + +strategyVal :: String +strategyVal = "n@E IO Bool +checkParams clp + = if (strategy clp) `permutationOf` strategyVal + then return True + else do putStrLn + $ unlines ["ERROR", + "strategy should contain all of the following characters: ", + " n = nominals @ = satisfaction operator", + " E = existential modality < = diamond", + " D = difference modality b = down-arrow binder", + " | = or * = transitive closure diamond", + " 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."] + return False + +configureStats :: CmdLineParams -> StatisticsState () +configureStats clp = setPrintOutInterval $ stats clp diff --git a/src/HTab/DMap.hs b/src/HTab/DMap.hs new file mode 100644 --- /dev/null +++ b/src/HTab/DMap.hs @@ -0,0 +1,94 @@ +module HTab.DMap +(DMap(..), empty, toMap, flatten, + delete, insert, insertWith, (!), + insert1, lookup, lookup1, lookupInter, + moveInnerDataDMapPlusDeps ) + +where + +-- import Test.QuickCheck ( Arbitrary(..), Gen, Property, +-- forAll, oneof, variant, sized, resize ) +-- import HyLo.Test ( UnitTest, runTest ) +-- import Control.Monad ( liftM ) + +import Data.IntMap ( IntMap ) +import qualified Data.IntMap as IM + +import HTab.Formula(DependencySet, dsUnion) + +import Prelude hiding ( lookup ) + +{- a DMap , or double map, is a nesting of two Maps -} + +data DMap c = DMap (IntMap (IntMap c)) + +instance (Show c) => Show (DMap c) where + show (DMap m) = show m + +toMap :: DMap c -> IntMap (IntMap c) +toMap (DMap m) = m + +empty :: DMap c +empty = DMap IM.empty + +insert1 :: Int -> IntMap c -> DMap c -> DMap c +insert1 k1 v (DMap m) = DMap $ IM.insert k1 v m + +insert :: Int -> Int -> c -> DMap c -> DMap c +insert k1 k2 v (DMap m) + = case IM.lookup k1 m of + Nothing -> DMap $ IM.insert k1 (IM.singleton k2 v) m + Just innerM -> DMap $ IM.insert k1 (IM.insert k2 v innerM) m + + +insertWith :: (c -> c -> c) -> Int -> Int -> c -> DMap c -> DMap c +insertWith f k1 k2 v (DMap m) + = case IM.lookup k1 m of + Nothing -> DMap $ IM.insert k1 (IM.singleton k2 v) m + Just innerM -> DMap $ IM.insert k1 (IM.insertWith f k2 v innerM) m + +flatten :: DMap c -> [((Int,Int),c)] +flatten (DMap m) + = let ambcs = IM.assocs m in -- [(a,IntMap c)] + concatMap (\(a_,innerM_) -> map (\(b_,c_) -> ((a_,b_),c_)) (IM.assocs innerM_ )) ambcs + +infixl 9 ! + +(!) :: DMap c -> Int -> Int -> c +(!) (DMap m) k1 k2 = (IM.!) ( (IM.!) m k1 ) k2 + + +lookup :: Int -> Int -> DMap c -> Maybe c +lookup k1 k2 (DMap m) = do innerMap <- IM.lookup k1 m + IM.lookup k2 innerMap + +lookup1 :: Int -> DMap c -> Maybe (IntMap c) +lookup1 k1 (DMap m) = IM.lookup k1 m + +delete :: Int -> DMap c -> DMap c +delete k1 (DMap m) = DMap $ IM.delete k1 m + +lookupInter :: Int -> DMap c -> [Int] +lookupInter k1 (DMap m) = case IM.lookup k1 m of + Nothing -> [] + Just innerMap -> IM.keys innerMap + +-- provided two keys of the DMap and a merge function, merge the inner maps of +-- both keys using the merge function when needed for inner values +-- delete the first inner map +-- and add the given dependencies +moveInnerDataDMapPlusDeps :: DependencySet -> DMap [(c,DependencySet)] -> Int -> Int -> DMap [(c,DependencySet)] +moveInnerDataDMapPlusDeps newDeps (DMap m) origKey destKey + = DMap + $ case IM.lookup origKey m of + Nothing -> m + Just origInnerMap + -> let origInnerMapPlusDeps = IM.map (addDeps newDeps) origInnerMap + prunedM = IM.delete origKey m + addDeps newBps = map (\(el,oldBps) -> (el,dsUnion newBps oldBps)) + in case IM.lookup destKey m of + Nothing -> IM.insert destKey origInnerMapPlusDeps prunedM + Just destInnerMap + -> let mergedInnerMap = IM.unionWith (++) origInnerMapPlusDeps destInnerMap + in IM.insert destKey mergedInnerMap prunedM + diff --git a/src/HTab/DisjSet.hs b/src/HTab/DisjSet.hs new file mode 100644 --- /dev/null +++ b/src/HTab/DisjSet.hs @@ -0,0 +1,71 @@ +module HTab.DisjSet +( DisjSet, Pointer(..), mkDSet, find, union, isRoot, onlyFind ) +where + +import qualified Data.Map as Map +import HTab.Formula ( showLit, Nom ) + +-- a disjoint-set forest +type DisjSet x = Map.Map x x +-- meaning: if an element is *not* in DisjSet, +-- then it is a root of a class + +-- invariant: there is no N such that (N,N) is in DisjSet +-- (it would provoke a look in the find function) + + + +-- find the root of the tree in which a given element belongs to +-- at each call to "find", we optimise the DisjSet to link to the root +find :: Ord x => x -> DisjSet x -> (x,DisjSet x) +find n s = case Map.lookup n s of + Nothing -> (n,s) + Just parent -> let (ancestor, modifiedDisjSet) = find parent s + in + (ancestor, Map.insert n ancestor modifiedDisjSet) + + +onlyFind :: Ord x => x -> DisjSet x -> x +onlyFind n s + = case Map.lookup n s of + Nothing -> n + Just parent -> onlyFind parent s + +-- union the sets in which a and b belong to +-- ensure : root of the merged set is the smallest root (min a b) +union :: Ord x => x -> x -> DisjSet x -> DisjSet x +union a b s = case compare rootA rootB of + EQ -> modifiedDisjSet2 + GT -> Map.insert rootA rootB modifiedDisjSet2 + LT -> Map.insert rootB rootA modifiedDisjSet2 + where (rootA,modifiedDisjSet1) = find a s + (rootB,modifiedDisjSet2) = find b modifiedDisjSet1 + +isRoot :: Ord x => x -> DisjSet x -> Bool +isRoot n s = Map.notMember n s + +-- constructor of an empty disjoint-set forest +mkDSet :: Ord x => DisjSet x +mkDSet = Map.empty::DisjSet x + +-- this should be outside of the module +data Pointer = Prefix Int | Nominal Nom + deriving (Eq) + +instance Show Pointer where + show (Prefix p) = 'P' : show p + show (Nominal n) = showLit n + +instance Ord Pointer where + compare (Prefix i1) (Prefix i2) = compare i1 i2 + compare (Nominal i1) (Nominal i2) = compare i1 i2 + compare (Nominal _) (Prefix _) = GT + compare (Prefix _) (Nominal _) = LT + +-- We have this order (p: prefix , n: nominal): +-- p0 < p1 < ... < pn < n0 < n1 < ... < nm + +-- The representative of a set is the smallest (by this order) element of the set. +-- Good news : a set always contains a prefix, so the reprensentative +-- is always the earliest prefix of the set. + diff --git a/src/HTab/Formula.hs b/src/HTab/Formula.hs new file mode 100644 --- /dev/null +++ b/src/HTab/Formula.hs @@ -0,0 +1,770 @@ +---------------------------------------------------- +-- -- +-- Formula.hs: -- +-- Formula data type, normal -- +-- form and show functions. -- +-- -- +---------------------------------------------------- + + +module HTab.Formula + +(Atom, Prop, Nom, Literal, +Rel, Prefix, Formula(..), +DependencySet, Dependency, +dsUnion, dsUnions, dsInsert, dsMember, +dsEmpty, dsMin, dsShow, addDeps, +PrFormula(..),showLess, AccFormula(..), +LanguageInfo(..), neg, +conj, disj, taut, +prop, nom, formulaLanguageInfo, prefix, +checkIfVariableNegatedOnce, replaceVar, +firstPrefixedFormula, +parse, simpleParse, Theory, RelInfo, Task, +showRelInfo, showRel, showLit, negLit, isForward, isBackwards, +encodeValidityTest, encodeSatTest, encodeRetrieveTask, +HyLoFormula, RelProperty(..), Encoding(..), maxNom, maxProp, toPropSymbol, toNomSymbol, toRelSymbol, +isTop, isBottom, isPositiveNom, isPositiveProp, isPositive, isNegative, isNominal, isProp, atom, +inv, invRel, int +) + + where + +import Data.Bits (complementBit, testBit, clearBit, (.|.) ) +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, sort ) + +import qualified HyLo.Signature.String as S + +import HyLo.Signature( HasSignature(..), relSymbols, nomSymbols, propSymbols ) + +import qualified HyLo.InputFile as InputFile +import qualified HyLo.InputFile.Parser as P +import HTab.Base (set, list, invertMap) +import qualified HyLo.Formula as F +import HTab.CommandLine ( CmdLineParams(..) ) + +type Prefix = Int + +type Rel = Int + +showRel :: Int -> String +showRel x = sign ++ name + where sign = if testBit x 0 then "-" else "" + name = show $ x `div` 2 + + +isBackwards, isForward :: Int -> Bool +isBackwards x = testBit x 0 +isForward = not . isBackwards + +data Formula + = Lit Atom + | Con (Set Formula) + | Dis (Set Formula) + | At Nom Formula + | Box Rel Formula + | Dia Rel Formula + | Down Nom Formula + | BoxX Rel Formula + | DiaX (Maybe Int) Rel Formula + | A Formula + | E Formula + | D Formula + | B Formula + deriving (Eq, Ord) + +-- convention : bit0 = OFF -> positive literal, negative otherwise +-- O : top +-- 1 : bottom + +-- 2 : p0 +-- 3 : !p0 +-- 4 : n0 +-- 5 : !n0 + +-- 6 : p1 +-- 7 : !p1 +-- 8 : n1 +-- 9 : !n1 +-- ... + +type Atom = Int +type Prop = Int +type Nom = Int +type Literal = Int + +isTop, isBottom, isPositiveNom, isNegativeNom, isNominal, isPositiveProp, isProp, isNegative, isPositive :: Int -> Bool +isTop = (==0) +isBottom = (==1) +isPositiveNom a = ((a `mod` 4) == 0) && (a > 1) +isNegativeNom a = ((a `mod` 4) == 1) && (a > 1) +isNominal a = ((a `mod` 4) < 2) && (a > 1) +isPositiveProp a = (a `mod` 4) == 2 +isProp a = (a `mod` 4) >= 2 +isNegative a = testBit a 0 +isPositive = not . isNegative + +atom :: Int -> Int +atom x = clearBit x 0 + +negLit :: Int -> Int +negLit x = complementBit x 0 + +invRel :: Int -> Int +invRel = negLit + +showLit :: Int -> String +showLit n + | isTop n = "True" + | isBottom n = "False" + | otherwise = case n `mod` 4 of + 0 -> "N" ++ show ((n `div` 4) - 1) + 1 -> "!N" ++ show ((n `div` 4) - 1) + 2 -> "P" ++ show (n `div` 4) + 3 -> "!P" ++ show (n `div` 4) + _ -> error "Impossible" + +instance Show Formula where + show (Lit a) = showLit a + show (Con fs) = "^" ++ show (list fs) + show (Dis fs) = "v" ++ show (list fs) + show (At n f) = showLit n ++ ":(" ++ show f ++ ")" + show (Box r f) = "[" ++ showRel r ++ "]" ++ show f + show (Dia r f) = "<" ++ showRel r ++ ">" ++ show f + show (BoxX r f) = "[" ++ showRel r ++ "*]" ++ show f + show (DiaX i r f) = "<" ++ showRel r ++ "*>(" ++ show i ++ ")" ++ show f + show (A f) = "A" ++ show f + show (E f) = "E" ++ show f + show (D f) = "D" ++ show f + show (B f) = "B" ++ show f + show (Down n f) = "down " ++ showLit n ++ "." ++ show f + +-- parsing of the input file + +type Theory = Formula +type Task = P.InferenceTask +type PRelInfo = [P.RelInfo] + +type RelInfo = Map Rel [RelProperty] +data RelProperty = Reflexive + | Symmetric + | Transitive + | Functional + | Injective + | Universal + | Difference + -- + | InverseOf Rel + | TRClosureOf Rel + | SubsetOf [Rel] + deriving (Eq, Show, Ord) + +showRelInfo :: RelInfo -> String +showRelInfo = Map.foldWithKey (\r v -> (++ " " ++ showRel r ++ " -> " ++ show v )) "" + +parse :: CmdLineParams -> String -> (Theory,RelInfo,Encoding,[Task]) +parse clp s + = (theory, relInfo, encoding, tasks) + where parseOutput = InputFile.myparse s -- direct parse from hylolib + encoding = getEncoding parseOutput + pRelInfo = P.relations parseOutput + relInfo = handleFunInj $ saturate $ forceProperties clp encoding $ convertToOurType pRelInfo encoding -- TODO + theory = convert relInfo encoding $ P.theory parseOutput + tasks = P.tasks parseOutput + + +data Encoding = Encoding { nomMap :: Map String Int, + propMap :: Map String Int, + relMap :: Map String Int } + deriving Show + +maxNom, maxProp :: Encoding -> Int +maxNom e = case Map.elems $ nomMap e of + [] -> 0 -- hackish + els -> maximum els + +maxProp e = case Map.elems $ propMap e of + [] -> -2 -- hackish + els -> maximum els + +toPropSymbol :: Encoding -> Int -> S.PropSymbol +toPropSymbol e i = S.PropSymbol $ case Map.lookup (atom i) (invertMap $ propMap e) of + Nothing -> {- new prop symbol -} "new_prop_" ++ show i + Just x -> x + +toNomSymbol :: Encoding -> Int -> S.NomSymbol +toNomSymbol e i = S.NomSymbol $ case Map.lookup (atom i) (invertMap $ nomMap e) of + Nothing -> error $ show e ++ " nom symbol " ++ show i + Just x -> x + +toRelSymbol :: Encoding -> Int -> S.RelSymbol +toRelSymbol e i = case Map.lookup (atom i) (invertMap $ relMap e) of + Nothing -> error $ show e ++ " rel symbol " ++ show i + Just x -> if isForward i then S.RelSymbol x else S.InvRelSymbol x + + +getEncoding :: P.ParseOutput -> Encoding +getEncoding parseOutput = + Encoding { nomMap = Map.fromList $ zip noms $ map (\n -> 4 + n*4) [0..], + propMap = Map.fromList $ zip props $ map (\p -> 2 + p*4) [0..], + relMap = Map.fromList $ zip rels $ map (\r -> r*2) [0..] } + where + theory = P.theory parseOutput + noms = map (\(S.NomSymbol n) -> n) $ Set.toList $ Set.unions $ map (nomSymbols . getSignature) theory + props = map (\(S.PropSymbol p) -> p) $ Set.toList $ Set.unions $ map (propSymbols . getSignature) theory + rels1 = map fst $ P.relations parseOutput + rels2 = map (\(S.RelSymbol r) -> r) $ Set.toList $ Set.unions $ map (relSymbols . getSignature) theory + rels = nub $ rels1 ++ rels2 + +nomsOfEncoding :: Encoding -> [Nom] +nomsOfEncoding e = Map.elems (nomMap e) + +-- add properties specified by the --all-PROP parameters +-- in order to work in case of automatic signature, requires +-- the list of RelSymbol present in the formula + +forceProperties :: CmdLineParams -> Encoding -> RelInfo -> RelInfo +forceProperties clp encoding relI + = foldr addToAll relI rels + where rels = Map.elems $ relMap encoding + addToAll r = Map.insertWith (\c1 c2 -> nub $ c1 ++ c2) r conds + conds = map snd $ + filter fst $ [(allTransitive clp, Transitive), + (allReflexive clp, Reflexive ), + (allSymmetric clp, Symmetric ), + (allFunctional clp, Functional), + (allInjective clp, Injective )] + +convertToOurType :: PRelInfo -> Encoding -> RelInfo -- and add for each relation in the formula, the relevant key +convertToOurType prelI e = foldr insertRelProp Map.empty (concatMap convertOne prelI) + where insertRelProp (rs,pr) = Map.insertWith (++) rs [pr] + convertOne (r,props) = concatMap (c r) props + c r P.Reflexive = [(int e r,Reflexive )] + c r P.Symmetric = [(int e r,Symmetric )] + c r P.Transitive = [(int e r,Transitive )] + c r P.Functional = [(int e r,Functional )] + c r P.Universal = [(int e r,Universal )] + c r P.Difference = [(int e r,Difference )] + c r (P.InverseOf s) = [(int e r,InverseOf (int e s))] + c r (P.TRClosureOf s) = [(int e r,TRClosureOf (int e s))] + c r (P.SubsetOf ss) = [(int e r,SubsetOf [ int e s | s <- ss])] + c r (P.Equals ss) = [(int e r,SubsetOf [ int e s | s <- ss])] ++ [(int e s,SubsetOf [int e r]) | s <- ss] + c _ (P.TClosureOf _) = error "TClosureOf not handled" + +simpleParse :: CmdLineParams -> String -> (Theory,RelInfo,Encoding,[Task]) +simpleParse clp s = parse clp $ "signature { automatic } theory { " ++ removeBeginEnd s ++ "}" + where removeBeginEnd = unwords . delete "begin" . delete "end" . words + +convert :: RelInfo -> Encoding -> [F.Formula S.NomSymbol S.PropSymbol S.RelSymbol] -> Formula +convert relI e = conv_ relI e . foldr (F.:&:) F.Top + +conv_ :: RelInfo -> Encoding -> F.Formula S.NomSymbol S.PropSymbol S.RelSymbol -> Formula +conv_ _ _ F.Top = taut +conv_ _ _ F.Bot = neg taut +conv_ _ e (F.Prop p) = prop e p +conv_ _ e (F.Nom n) = nom e n +conv_ relI e (F.Neg f) = neg $ conv_ relI e f +conv_ relI e (f1 F.:&: f2) = conv_ relI e f1 `conj` conv_ relI e f2 +conv_ relI e (f1 F.:|: f2) = conv_ relI e f1 `disj` conv_ relI e f2 +conv_ relI e (f1 F.:-->: f2) = conv_ relI e f1 `imp` conv_ relI e f2 +conv_ relI e (f1 F.:<-->: f2) = conv_ relI e f1 `dimp` conv_ relI e f2 +conv_ relI e (F.Diam r f) = specialiseDia r relI e (conv_ relI e f) +conv_ relI e (F.Box r f) = specialiseBox r relI e (conv_ relI e f) +conv_ relI e (F.At n f) = at e n (conv_ relI e f) +conv_ relI e (F.Down v f) = downArrow e v (conv_ relI e f) +conv_ relI e (F.A f) = univMod (conv_ relI e f) +conv_ relI e (F.E f) = existMod (conv_ relI e f) +conv_ relI e (F.D f) = dExistMod (conv_ relI e f) +conv_ relI e (F.B f) = dUnivMod (conv_ relI e f) + +type Connector = Formula -> Formula + +specialiseDia :: S.RelSymbol -> RelInfo -> Encoding -> Connector +specialiseDia r relI e = specialise r relI (diamond e, diamondX e, dExistMod, existMod) e + +specialiseBox :: S.RelSymbol -> RelInfo -> Encoding -> Connector +specialiseBox r relI e = specialise r relI (box e, boxX e, dUnivMod, univMod) e + +specialise :: S.RelSymbol -> RelInfo -> (S.RelSymbol -> Connector, S.RelSymbol -> Connector, Connector, Connector) -> Encoding -> Connector +specialise (S.InvRelSymbol r) _ (relational, _ , _ , _) _ -- happens only with simple input + = relational $ S.InvRelSymbol r + +specialise (S.RelSymbol r) relI (relational, rtclosure, difference, global) e + = case filter interesting props of + (Difference:_) -> difference + (Universal:_) -> global + [] -> relational $ S.RelSymbol r + _ -> case specialise2 (int e r) relI of + Just_ r2 -> relational $ toRelSymbol e r2 + Inverse r2 -> relational $ invRS $ toRelSymbol e r2 + RTClosure r2 -> rtclosure $ toRelSymbol e r2 + RTClosureInv r2 -> rtclosure $ invRS $ toRelSymbol e r2 + where + interesting Difference = True + interesting Universal = True + interesting (InverseOf _) = True + interesting (TRClosureOf _) = True + interesting _ = False + props = Map.findWithDefault [] (int e r) relI + invRS (S.RelSymbol s) = S.InvRelSymbol s + invRS (S.InvRelSymbol s) = S.RelSymbol s + +data ModType = Just_ Rel | Inverse Rel | RTClosure Rel | RTClosureInv Rel + +specialise2 :: Rel -> RelInfo -> ModType +specialise2 r_ relI + = go (Just_ r_) + where + go j@(Just_ r) = + case filter interesting (propsOf r) of + (InverseOf r2:_) -> go (Inverse r2) + (TRClosureOf r2:_) -> go (RTClosure r2) + _ -> j + + go io@(Inverse r) = + case filter interesting (propsOf r) of + (InverseOf r2:_) -> go (Just_ r2) + (TRClosureOf r2:_) -> RTClosureInv r2 + _ -> io + + go rtc@(RTClosure r) = + case filter interesting (propsOf r) of + (InverseOf r2:_) -> RTClosureInv r2 + (TRClosureOf r2:_) -> go (RTClosure r2) + _ -> rtc + + go rtci@(RTClosureInv r) = + case filter interesting (propsOf r) of + (InverseOf r2:_) -> RTClosure r2 + _ -> rtci + + interesting (InverseOf _) = True + interesting (TRClosureOf _) = True + interesting _ = False + propsOf r__ = Map.findWithDefault [] r__ relI + + +inv :: Rel -> RelInfo -> Rel +inv r relI + = case Map.lookup r relI of + Nothing -> r + Just properties -> if Symmetric `elem` properties then r else invRel r + +type HyLoFormula = F.Formula S.NomSymbol S.PropSymbol S.RelSymbol + +-- saturate RelInfo with hierarchy information : Reflexive, Symmetric, Transitive, Universal, Difference + +saturate :: RelInfo -> RelInfo +saturate relI = Map.mapWithKey saturateOne relI + where saturateOne r props = let ancestorProps = concatMap (getProperties relI) $ getAncestors r relI + newProps = list $ Set.union (set ancestorProps) (set props) + in + newProps + +getProperties :: RelInfo -> Rel -> [RelProperty] +getProperties ri r + = getOnlyProps $ filter isProp_ props + where props = Map.findWithDefault [] r ri + getOnlyProps = filter isProp_ + isProp_ Reflexive = True + isProp_ Symmetric = True + isProp_ Transitive = True + isProp_ Universal = True + isProp_ Difference = True + isProp_ _ = False + +getAncestors :: Rel -> RelInfo -> [Rel] +getAncestors r_ relI = + list $ go (Set.singleton r_) r_ + where + go seen r = + let props = Map.findWithDefault [] r relI + parents = concatMap extractParent props + extractParent (InverseOf rp) = [rp] + extractParent (TRClosureOf rp) = [rp] + extractParent _ = [ ] + todo = list ( (set parents) Set.\\ seen ) + newSeen = Set.union seen $ set parents + in + case todo of + [] -> Set.singleton r + _ -> Set.insert r $ Set.unions $ map (go newSeen) todo + +-- ========================================================================== +-- +-- saturate relInfo with the properties Functional and Injective +-- rationale : being able to enforce Injectivity even though the +-- input format does not have an Injective label. +-- the solution to do so is: +-- R_injective , Inv_R { inverseof R_injective, Functional } +-- +-- ========================================================================== + +data FunInj = Not | Fun | Inj | FunInj + +handleFunInj :: RelInfo -> RelInfo +handleFunInj relI = +-- explore the hierarchy of relations starting by the leaves and ending at the top +-- taking into account the alternations "inverseof" to enforce functionality and/or injectivity + Map.foldWithKey startFromLeaf relI relI + where startFromLeaf rs props currentRelI = follow rs props currentRelI Not + + follow rs props currentRelI currentStatus + = case parentsWithInv props status of + Just (parent,newStatus) -> let parentProps = Map.findWithDefault [] parent currentRelI in + follow parent parentProps currentRelI newStatus + Nothing + -> case currentStatus of + Not -> currentRelI + _ -> Map.insertWith (++) rs (toProps status) currentRelI + where + status = if Functional `elem` props + then case currentStatus of + FunInj -> FunInj + Inj -> FunInj + Fun -> Fun + Not -> Fun + else currentStatus + toProps Not = [] + toProps FunInj = [Functional, Injective] + toProps Fun = [Functional] + toProps Inj = [Injective] + + parentsWithInv props status + = case concatZip $ map extractParent props of + ([],[]) -> Nothing + ((par:_),_) -> Just (par, invert status) + where invert Not = Not + invert FunInj = FunInj + invert Fun = Inj + invert Inj = Fun + (_,(par:_)) -> Just (par, status) + where extractParent (InverseOf rp) = ([rp],[]) + extractParent (TRClosureOf rp) = ([] ,[rp]) + extractParent _ = ([] ,[]) + + +concatZip :: [([a],[b])] -> ([a],[b]) +concatZip [] = ([],[]) +concatZip ((as,bs):tl) = (as++as2,bs++bs2) where (as2,bs2) = concatZip tl + +-- ========================================================================== + +encodeValidityTest :: RelInfo -> Encoding -> Formula -> [HyLoFormula] -> Formula +encodeValidityTest relI e th fs + = neg $ conj th (convert relI e fs) + +encodeSatTest :: RelInfo -> Encoding -> Formula -> [HyLoFormula] -> Formula +encodeSatTest relI e th fs + = conj th (convert relI e fs) + +encodeRetrieveTask :: RelInfo -> Encoding -> LanguageInfo -> Formula -> [HyLoFormula] -> ([Int],[Formula]) +encodeRetrieveTask relI e fLang theory fs + = (noms , map (\n -> conj theory (At n (neg $ convert relI e fs))) noms) + where noms = languageNoms fLang + +-- CONSTRUCTORS + +{- Atoms -} +taut :: Formula +nom :: Encoding -> S.NomSymbol -> Formula +prop :: Encoding -> S.PropSymbol -> Formula + +taut = Lit 0 +nom e (S.NomSymbol n) = Lit ( nomMap e Map.! n ) +prop e (S.PropSymbol p) = Lit ( propMap e Map.! p ) + +{- Modalities -} +box, diamond, boxX, diamondX :: Encoding -> S.RelSymbol -> Formula -> Formula +univMod, existMod, dUnivMod, dExistMod :: Formula -> Formula +box e (S.RelSymbol r) = Box $ int e r +box e (S.InvRelSymbol r) = Box $ invRel $ int e r +diamond e (S.RelSymbol r) = Dia $ int e r +diamond e (S.InvRelSymbol r) = Dia $ invRel $ int e r +boxX e (S.RelSymbol r) = BoxX $ int e r +boxX e (S.InvRelSymbol r) = BoxX $ invRel $ int e r +diamondX e (S.RelSymbol r) = DiaX Nothing $ int e r +diamondX e (S.InvRelSymbol r) = DiaX Nothing $ invRel $ int e r +univMod = A +existMod = E +dUnivMod = B +dExistMod = D + +int :: Encoding -> String -> Int +int e s = (relMap e) Map.! s + +{- binder -} +downArrow :: Encoding -> S.NomSymbol -> Formula -> Formula +downArrow e (S.NomSymbol n) = Down ((nomMap e) Map.! n) + +{- Hybrid operators -} +at :: Encoding -> S.NomSymbol -> Formula -> Formula +at e (S.NomSymbol n) = At ((nomMap e) Map.! n) + +{- Conjunction and disjunction -} + +conj, disj :: Formula -> Formula -> Formula + +conj (Con xs) (Con ys) = Con (Set.union xs ys) +conj f c@(Con _) = conj c f +conj c@(Con xs) f + | isTrue f = c + | isFalse f = neg taut + | otherwise = Con (Set.insert f xs) +conj f f' + | isTrue f = f' + | isFalse f = neg taut + | isTrue f' = f + | isFalse f' = neg taut + | otherwise = skipSingleton Con (set [f,f']) + +disj (Dis xs) (Dis ys) = Dis (Set.union xs ys) +disj f c@(Dis _) = disj c f +disj c@(Dis xs) f + | isTrue f = taut + | isFalse f = c + | otherwise = Dis (Set.insert f xs) +disj f f' + | isTrue f = taut + | isFalse f = f' + | isTrue f' = taut + | isFalse f' = f + | otherwise = skipSingleton Dis (set [f,f']) + +dimp :: Formula -> Formula -> Formula +dimp f1 f2 = (neg f1 `disj` f2) `conj` (f1 `disj` neg f2) +-- this form is preferred so as to enhance lazy branching + +-- TODO +-- ala Spartacus: +-- when there is no literal in the double implication, +-- use the following form: +--dimp f1 f2 = (f1 `conj` f2) `disj` (neg f1 `conj` neg f2) + +imp :: Formula -> Formula -> Formula +imp f1 f2 = neg f1 `disj` f2 + +skipSingleton :: (Set Formula -> Formula) -> Set Formula -> Formula +skipSingleton c xs + | Set.size xs == 1 = Set.findMin xs + | otherwise = c xs + +isTrue, isFalse :: Formula -> Bool +isTrue (Lit 0) = True +isTrue _ = False +isFalse (Lit 1) = True +isFalse _ = False + +-- invariant : neg is only called on literals during +-- the run of the algorithm +neg :: Formula -> Formula +neg (Con l) = Dis (Set.map neg l) +neg (Dis l) = Con (Set.map neg l) +neg (At n f) = At n (neg f) +neg (Down v f) = Down v (neg f) +neg (Box r f) = Dia r (neg f) +neg (Dia r f) = Box r (neg f) +neg (BoxX r f) = DiaX Nothing r (neg f) +neg (DiaX _ r f) = BoxX r (neg f) +neg (A f) = E (neg f) +neg (E f) = A (neg f) +neg (D f) = B (neg f) +neg (B f) = D (neg f) +neg (Lit n) = Lit $ negLit n + + +-- prefixed formula + +data PrFormula = PrFormula Prefix DependencySet Formula + deriving Eq + +instance Show PrFormula where + show (PrFormula pr ds f) = show pr ++ ":" ++ (dsShow ds) ++ ":" ++ show f + +showLess :: PrFormula -> String +showLess (PrFormula pr _ f) = show pr ++ ":" ++ show f + +prefix :: Prefix -> DependencySet -> Set Formula -> [PrFormula] +prefix p bps fs = [PrFormula p bps formula|formula <- Set.toList fs] + +firstPrefixedFormula :: Formula -> PrFormula +firstPrefixedFormula = PrFormula 0 dsEmpty + +-- accessibility Formulas + +data AccFormula = AccFormula DependencySet Rel Prefix Prefix + deriving (Eq, Ord) + +instance Show AccFormula where + show (AccFormula bprs r p1 p2) = show bprs ++ ":" ++ show p1 ++ "<" ++ showRel r ++ ">" ++ show p2 + +-- formula language + +data LanguageInfo = LanguageInfo { languageNoms :: [Int], -- ascending list + relevantNoms :: [Int], + languageUniv :: Bool, + languagePast :: Bool, + languageDiff :: Bool, + languageTrans :: Bool, + languageDown :: Bool } + +instance Show LanguageInfo where + show li = "Input Language:" + ++ "\n|" ++ yesnol "Noms" ( languageNoms li ) + ++ "\n|" ++ yesnol "Relevant Noms" ( relevantNoms li ) ++ "\n" + ++ yesno "Univ, " ( languageUniv li ) + ++ yesno "Past, " ( languagePast li ) + ++ yesno "Trans, " ( languageTrans li) + ++ yesno "Down." ( languageDown li ) + where yesno :: String -> Bool -> String + yesno s b = ( if b then "" else "no " ) ++ s + yesnol s l | null l = "no " ++ s + yesnol s l = s ++ concatMap (\l_ -> ", " ++ showLit l_) l + +formulaLanguageInfo :: Formula -> Encoding -> LanguageInfo +formulaLanguageInfo f e + = LanguageInfo { languageNoms = noms, + relevantNoms = relNoms, + languageUniv = hasUnivModality f, + languagePast = hasPast f, + languageDiff = hasDiffModality f, + languageTrans = hasTransClosure f, + languageDown = hasDownArrow f } + + where allNoms_ = nomsOfEncoding e + relNoms_ = extractRelevantNominals f + noms = sort allNoms_ + relNoms = Set.toAscList relNoms_ + +-- composeXX functions follow the idea from +-- "A pattern for almost compositional functions", Bringert and Ranta. +composeFold :: b + -> (b -> b -> b) + -> (Formula -> b) + -> (Formula -> b) +composeFold zero combine g e = case e of + Con fs -> foldr1 combine $ map g $ list fs + Dis fs -> foldr1 combine $ map g $ list fs + Dia _ f -> g f + Box _ f -> g f + DiaX _ _ f -> g f + BoxX _ f -> g f + At _ f -> g f + Down _ f -> g f + A f -> g f + E f -> g f + D f -> g f + B f -> g f + _ -> zero + +composeMap :: (Formula -> Formula) + -> (Formula -> Formula) + -> (Formula -> Formula) +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) + Box r f -> Box r (g f) + DiaX i r f -> DiaX i r (g f) + BoxX r f -> BoxX r (g f) + At i f -> At i (g f) + A f -> A (g f) + E f -> E (g f) + D f -> D (g f) + B f -> B (g f) + Down x f -> Down x (g f) + f -> baseCase f + + +extractRelevantNominals :: Formula -> Set Nom +extractRelevantNominals (Lit n)| isNegativeNom n = Set.singleton (atom n) +extractRelevantNominals (At _ f) = extractRelevantNominals f +extractRelevantNominals f = composeFold Set.empty Set.union extractRelevantNominals f + +hasUnivModality :: Formula -> Bool +hasUnivModality (A _) = True +hasUnivModality f = composeFold False (||) hasUnivModality f + +hasPast :: Formula -> Bool +hasPast (Dia r _) = testBit r 0 +hasPast (Box r _) = testBit r 0 +hasPast (BoxX r _) = testBit r 0 +hasPast (DiaX _ r _) = testBit r 0 +hasPast f = composeFold False (||) hasPast f + +hasDiffModality :: Formula -> Bool +hasDiffModality (B _) = True +hasDiffModality f = composeFold False (||) hasDiffModality f + +hasTransClosure :: Formula -> Bool +hasTransClosure (BoxX _ _) = True +hasTransClosure (DiaX _ _ _) = True +hasTransClosure f = composeFold False (||) hasTransClosure f + +hasDownArrow :: Formula -> Bool +hasDownArrow (Down _ _ ) = True +hasDownArrow f = composeFold False (||) hasDownArrow f + +replaceVar :: Int -> Int -> Formula -> Formula +replaceVar v n a@(Lit v2) + | isNominal v2 = if atom v /= atom v2 then a + else Lit $ atom n .|. sign v2 + where sign x = if isNegative x then 1 else 0 + +replaceVar v n a@(Down v2 f) = if v == v2 then a -- variable capture + else Down v2 (replaceVar v n f) +replaceVar v n (At v2 f) = if v == v2 then At n (replaceVar v n f) + else At v2 (replaceVar v n f) +replaceVar v n f = composeMap id (replaceVar v n) f + +checkIfVariableNegatedOnce :: Formula -> Bool +checkIfVariableNegatedOnce (Down v_ f_) + = go v_ f_ + where go :: Int -> Formula -> Bool + go v (Down v2 f) = if v == v2 then False {- variable capture -} else go v f + go v (Lit v2) = (atom v == atom v2) && isNegative v2 + go v f = composeFold False (||) (go v) f + +checkIfVariableNegatedOnce _ = error "checkIfVariableNegatedOnce : only down-arrow formulas" + + +-- backjumping + +type Dependency = Int +type DependencySet = IntSet.IntSet + +instance Ord PrFormula where + compare (PrFormula pr1 ds1 f1) (PrFormula pr2 ds2 f2) = + case dsMin ds1 `compare` dsMin ds2 of + LT -> LT + GT -> GT + EQ -> compare (pr1,f1) (pr2,f2) + +dsUnion :: DependencySet -> DependencySet -> DependencySet +dsUnion = IntSet.union + +dsUnions :: [DependencySet] -> DependencySet +dsUnions = IntSet.unions + +dsInsert :: Dependency -> DependencySet -> DependencySet +dsInsert = IntSet.insert + +dsMember :: Dependency -> DependencySet -> Bool +dsMember = IntSet.member + +dsEmpty :: DependencySet +dsEmpty = IntSet.empty + +dsMin :: DependencySet -> Int +dsMin ds = maybe 0 fst $ IntSet.minView ds + +dsShow :: DependencySet -> String +dsShow = show . IntSet.toList + +addDeps :: DependencySet -> PrFormula -> PrFormula +addDeps ds1 (PrFormula p ds2 f) = PrFormula p (dsUnion ds1 ds2) f diff --git a/src/HTab/Main.hs b/src/HTab/Main.hs new file mode 100644 --- /dev/null +++ b/src/HTab/Main.hs @@ -0,0 +1,189 @@ +module HTab.Main + +( runWithParams, TaskRunFlag(..)) + +where +import Control.Applicative ( (<$>) ) +import Control.Monad ( when ) +import Control.Monad.State( runStateT ) +import Control.Monad.Reader( runReaderT ) + +import System.Console.CmdArgs ( whenNormal, whenLoud ) + +import System.IO ( hSetBuffering, stdin, BufferMode(LineBuffering)) +import System.CPUTime( getCPUTime ) +import qualified System.Timeout as T +import System.IO.Strict ( readFile ) +import Prelude hiding ( readFile ) + +import HyLo.InputFile.Parser ( QueryType(..) ) + +import HTab.CommandLine( filename, timeout, CmdLineParams, genModel, backjumping, + showFormula ) +import HTab.Branch( BranchInfo(..),initialBranchStateFor, BranchData(..), + emptyBranch, addFirstFormulas) +import HTab.Statistics( Statistics, initialStatisticsStateFor, printOutMetricsFinal ) +import HTab.Tableau( OpenFlag(..), tableauStart ) +import HTab.Formula( formulaLanguageInfo, languageTrans, Theory, RelInfo, Encoding, Task, + Formula, encodeValidityTest, encodeSatTest, encodeRetrieveTask, + toNomSymbol, showRelInfo ) +import qualified HTab.Formula as F +import HTab.ModelGen ( Model ) + +data TaskRunFlag = SUCCESS | FAILURE + +runWithParams :: CmdLineParams -> IO (Maybe TaskRunFlag) +runWithParams clp = + time "Total time: " + $ do + let fromStdIn = do myPutStrLn $ "Reading from stdin (run again with" ++ + "`--help' for usage options)" + hSetBuffering stdin LineBuffering + getContents + + let parse = \i -> if head (words i) == "begin" + then F.simpleParse clp i else F.parse clp i + allTasks <- parse <$> maybe fromStdIn readFile (filename clp) + -- + result <- if timeout clp == 0 + then Just <$> runTasks allTasks clp + else T.timeout (timeout clp * (10::Int)^(6::Int)) + (runTasks allTasks clp) + -- + case result of + Nothing -> myPutStrLn "\nTimeout.\n" + Just SUCCESS -> myPutStrLn "\nAll tasks successful.\n" + Just FAILURE -> myPutStrLn "\nOne task failed.\n" + -- + return result + +-- + +runTasks :: (Theory,RelInfo,Encoding,[Task]) -> CmdLineParams -> IO TaskRunFlag +runTasks allTasks@(theory,relInfo,encoding,tasks) clp = + do + myPutStrLn "== Checking theory satisfiability ==" + res <- runOneTask (Satisfiable, genModel clp,[]) relInfo encoding theory clp + case res of + SUCCESS | null tasks -> return SUCCESS + | otherwise -> do myPutStrLn "\n== Starting tasks ==" + res2 <- runTasks2 allTasks clp + myPutStrLn "\n== End of tasks ==" + return res2 + FAILURE -> return FAILURE + +-- + +runTasks2 :: (Theory,RelInfo,Encoding,[Task]) -> CmdLineParams -> IO TaskRunFlag +runTasks2 (_,_,_,[]) _ = error "runTasks2 empty list error" +runTasks2 (theory,relInfo,encoding,(hd:tl)) clp = + do res <- runOneTask hd relInfo encoding theory clp + case res of + SUCCESS | null tl -> return SUCCESS + | otherwise -> runTasks2 (theory,relInfo,encoding,tl) clp + FAILURE -> do _ <- runTasks2 (theory,relInfo,encoding,tl) clp + return FAILURE + +-- + +runOneTask :: Task -> RelInfo -> Encoding -> Formula -> CmdLineParams -> IO TaskRunFlag +runOneTask (query,mOutFile,fs) relInfo encoding theory clp = + time "Task time:" + $ do + myPutStrLn $ "\n* " ++ case query of {Valid -> "Validity task"; + Satisfiable -> "Satisfiability task"; + Retrieve -> "Instance retrieval task"} + -- + result <- + case query of + Retrieve + -> + do let fLang = formulaLanguageInfo theory encoding + let initialBranch = emptyBranch clp fLang relInfo encoding + let (noms,encfs) = encodeRetrieveTask relInfo encoding fLang theory fs + -- + myPutStrLn $ "Instances making true: " ++ show fs + -- + results <- mapM (tableauInit clp . addFirstFormulas clp initialBranch fLang) encfs + let goodnoms = [ toNomSymbol encoding n | (n,(CLOSED _ ,_)) <- zip noms results] + myPutStrLn $ show goodnoms + let doWrite f = do writeFile f (show goodnoms ++ "\n") + myPutStrLn ("Nominals saved as " ++ f) + maybe (return ()) doWrite mOutFile + return SUCCESS + + valOrSat + -> + do let f = case valOrSat of + Valid -> encodeValidityTest relInfo encoding theory fs + Satisfiable -> encodeSatTest relInfo encoding theory fs + _ -> error "never happens" + -- + when (showFormula clp) + $ myPutStrLn + $ unlines ["Input for SAT test:", + "{ " ++ show f ++ " }", + "End of input", + "Relations properties :" ++ showRelInfo relInfo ] + -- + let fLang = formulaLanguageInfo f encoding + let initialBranch = emptyBranch clp fLang relInfo encoding + let branchInfo = addFirstFormulas clp initialBranch fLang f + let clp2 = if languageTrans fLang then clp{backjumping=False} else clp + -- + result <- tableauInit clp2 branchInfo + -- + case result of + (OPEN m, stats) -> do myPutStrLn $ + case query of + Valid -> "The formula is not valid." + Satisfiable -> "The formula is satisfiable." + _ -> error "never happens" + saveGenModel mOutFile m + whenNormal $ printOutMetricsFinal stats + return SUCCESS + (CLOSED _, stats) -> do myPutStrLn $ + case query of + Valid -> "The formula is valid." + Satisfiable -> "The formula is unsatisfiable." + _ -> error "never happens" + whenNormal $ printOutMetricsFinal stats + return FAILURE + -- + return $ case (query, result) of + (Satisfiable, SUCCESS ) -> SUCCESS + (Satisfiable, FAILURE ) -> FAILURE + (Valid , SUCCESS ) -> FAILURE + (Valid , FAILURE ) -> SUCCESS + (Retrieve , _ ) -> SUCCESS + +-- + +saveGenModel :: Maybe FilePath -> Model -> IO () +saveGenModel mOutFile m = maybe (return ()) doWrite mOutFile + where doWrite f = do writeFile f (show m) + myPutStrLn ("Model saved as " ++ f) + +tableauInit :: CmdLineParams -> BranchInfo -> IO (OpenFlag,Statistics) +tableauInit clp bi = + do whenLoud $ putStrLn ">> Starting rules application" + initStatsState $ initBranchState bd $ tableauStart clp bi + where initStatsState = initialStatisticsStateFor runStateT + initBranchState = initialBranchStateFor runReaderT + bd = BranchData { branch_clp = clp } + +-- + +time :: String -> IO a -> IO a +time message action = + do start <- getCPUTime + result <- action + end <- getCPUTime + let elapsedTime = fromInteger (end - start) / 1000000000000.0 + myPutStrLn $ message ++ show (elapsedTime :: Double) + return result + + +myPutStrLn :: String -> IO () +myPutStrLn str = do whenNormal $ putStrLn str + diff --git a/src/HTab/ModelGen.hs b/src/HTab/ModelGen.hs new file mode 100644 --- /dev/null +++ b/src/HTab/ModelGen.hs @@ -0,0 +1,93 @@ +module HTab.ModelGen (Model, buildModel ) + +where + +import qualified Data.Set as Set +import Data.Set (Set) +import qualified Data.IntMap as IntMap +import HyLo.Model.Herbrand ( inducedModel ) +import qualified HyLo.Model.Herbrand as H +import qualified HyLo.Model as M + +import qualified HyLo.Signature.String as S + +import HTab.Formula( Prefix, Rel, LanguageInfo(..), Encoding, int, + RelInfo, toPropSymbol, toNomSymbol, toRelSymbol, isPositiveProp ) +import HTab.Branch( Branch(..), prefixes, getUrfather, + isInTheModel, relationIsInTheModel, getModelRepresentative, + isTransitive, isSymmetric ) +import qualified HTab.DisjSet as DS +import HTab.DMap (flatten, DMap(..), toMap ) +import HTab.Relations ( allRels ) + +type Model = M.Model S.NomSymbol S.NomSymbol S.PropSymbol S.RelSymbol + +buildModel :: Branch -> Model +buildModel branch = + completeModel e (relInfo branch) $ inducedModel $ H.herbrand es ps rs + where + e = encoding branch + bias = if null $ languageNoms $ inputLanguage branch + then 0 + else 1 + length ( languageNoms $ inputLanguage branch ) + es = Set.union + (Set.fromList + [(S.NomSymbol $ show (getUrfather branch (DS.Nominal n) + bias), toNomSymbol e n) + | n <- languageNoms $ inputLanguage branch] + ) + (Set.fromList + [(S.NomSymbol $ show (p + bias), S.NomSymbol $ show (p + bias)) + | p <- prefixes branch, isInTheModel branch p] + ) + ps = Set.fromList + [(S.NomSymbol $ show (pre + bias), pro) + | (pre,pro) <- prefixAndProps branch] + rs = Set.fromList $ map (toSimpSig e) + $ map (\(p1,r,p2) -> (getModelRepresentative branch p1 + bias, r, getModelRepresentative branch p2 + bias)) + $ filter (relationIsInTheModel branch) $ allRels $ accStr branch + +toSimpSig :: Encoding -> (Prefix,Rel,Prefix) -> (S.NomSymbol,S.RelSymbol,S.NomSymbol) +toSimpSig e (p1,r,p2) = (S.NomSymbol (show p1), toRelSymbol e r, S.NomSymbol (show p2)) + +prefixAndProps :: Branch -> [(Prefix,S.PropSymbol)] +prefixAndProps br = + [(pr, toPropSymbol e p_) | (pr , p_) <- prPosLitProp ++ prefWitPositive] + where clashable = toMap $ clashStr br + clashableRelevant = IntMap.filterWithKey (\k _ -> isInTheModel br k) clashable + prPosLitProp = filter (isPositiveProp . snd) $ map fst $ flatten $ DMap clashableRelevant + -- + witMap = toMap $ brWitnesses br + witMapRelevant = IntMap.filterWithKey (\k _ -> isInTheModel br k) witMap + prefWitPositive = filter (isPositiveProp . snd) $ map fst $ flatten $ DMap witMapRelevant + -- + e = encoding br + +completeModel :: Encoding -> RelInfo -> Model -> Model +completeModel e relI m = completeTransitivity e relI $ completeSymmetry e relI m + +completeTransitivity :: Encoding -> RelInfo -> Model -> Model +completeTransitivity e relI m = m{M.succs = \rs@(S.RelSymbol r) w + -> if isTransitive relI (int e r) + then getTransClos (M.succs m) rs w + else M.succs m rs w} + +completeSymmetry :: Encoding -> RelInfo -> Model -> Model +completeSymmetry e relI m = m{M.succs = \rs@(S.RelSymbol r) w + -> if isSymmetric relI (int e r) + then getSymClos (M.worlds m) (M.succs m) rs w + else M.succs m rs w} + +getTransClos :: (Ord w) => (r -> w -> Set w) -> r -> w -> Set w +getTransClos succs_ r_ w_ + = go Set.empty Set.empty succs_ r_ w_ + where go seen todo succs r w + = case Set.minView todo1 of + Nothing -> seen + Just (nextWorld,todo2) -> go (Set.insert nextWorld seen) todo2 succs r nextWorld + where todo1 = ((succs r w) `Set.union` todo) `Set.difference` seen + +getSymClos :: (Ord w) => Set w -> (r -> w -> Set w) -> r -> w -> Set w +getSymClos worlds succs_ r_ w_ + = Set.union (succs_ r_ w_) syms + where syms = Set.filter (hasAsSuccessor r_ w_) worlds + hasAsSuccessor rel world2 world1 = Set.member world2 $ succs_ rel world1 diff --git a/src/HTab/Relations.hs b/src/HTab/Relations.hs new file mode 100644 --- /dev/null +++ b/src/HTab/Relations.hs @@ -0,0 +1,90 @@ +module HTab.Relations + +( Relations(..), emptyRels, insertRelation, mergePrefixes, + successors, predecessors, allRels, null, linksFromTo ) + +where + +import qualified Data.IntMap as IntMap +import Data.IntMap ( IntMap ) + +import qualified Data.List as List + +import qualified HTab.DMap as DMap +import HTab.DMap ( DMap(..) ) + +import HTab.Formula (Prefix, Rel, DependencySet, dsShow ) +import Prelude hiding (id, pred, succ, null) + +type InRel = DMap {- Prefix Rel -} [(Prefix,DependencySet)] +type OutRel = DMap {- Prefix Rel -} [(Prefix,DependencySet)] + +data Relations = Relations { inRel :: InRel , + outRel :: OutRel } + +emptyRels :: Relations +emptyRels = Relations { inRel = DMap.empty, outRel = DMap.empty } + +null :: Relations -> Bool +null = IntMap.null . DMap.toMap . outRel + +allRels :: Relations -> [(Prefix,Rel,Prefix)] +allRels rels = [ (p1,r,p2) | ((p1,r),ds_out_s) <- DMap.flatten $ outRel rels, + (p2,_) <- ds_out_s ] + + +successors :: Relations -> Prefix -> IntMap {- Rel -} [(Prefix,DependencySet)] +successors rels p = IntMap.findWithDefault IntMap.empty p (DMap.toMap $ outRel rels) + +predecessors :: Relations -> Prefix -> IntMap {- Rel -} [(Prefix,DependencySet)] +predecessors rels p = IntMap.findWithDefault IntMap.empty p (DMap.toMap $ inRel rels) + +linksFromTo :: Relations -> Prefix -> Prefix -> [Rel] +linksFromTo rels p1 p2 + = map fst $ filter (\(_,p_d_s) -> p2 `elem` map fst p_d_s ) outs where outs = IntMap.toList $ successors rels p1 + +-- assumes you never add twice the same relation +insertRelation :: Relations -> Prefix -> Rel -> Prefix -> DependencySet -> Relations +insertRelation rels p1 r p2 ds = + let + outRelMap = DMap.toMap $ outRel rels + inRelMap = DMap.toMap $ inRel rels + outRel_ + = case IntMap.lookup p1 outRelMap of + Nothing -> DMap $ IntMap.insert p1 (IntMap.singleton r [(p2,ds)]) outRelMap + Just innerMap + -> case IntMap.lookup r innerMap of + Nothing -> DMap $ IntMap.insert p1 (IntMap.insert r [(p2,ds)] innerMap) outRelMap + Just innerInnerList -> DMap $ IntMap.insert p1 (IntMap.insert r ((p2,ds):innerInnerList) innerMap) outRelMap + inRel_ + = case IntMap.lookup p2 inRelMap of + Nothing -> DMap $ IntMap.insert p2 (IntMap.singleton r [(p1,ds)]) inRelMap + Just innerMap + -> case IntMap.lookup r innerMap of + Nothing -> DMap $ IntMap.insert p2 (IntMap.insert r [(p1,ds)] innerMap) inRelMap + Just innerInnerList -> DMap $ IntMap.insert p2 (IntMap.insert r ((p1,ds):innerInnerList) innerMap) inRelMap + in + Relations {outRel = outRel_ , inRel = inRel_ } + + +mergePrefixes :: Relations -> Prefix -> Prefix -> DependencySet -> Relations +mergePrefixes r pr ur _ | pr == ur = r +mergePrefixes r pr ur ds + = let outRel_ = DMap.moveInnerDataDMapPlusDeps ds (outRel r) pr ur + inRel_ = DMap.moveInnerDataDMapPlusDeps ds (inRel r) pr ur + in Relations { outRel = outRel_ , inRel = inRel_ } + +instance Show Relations where + show r = "\nAccesibility: " ++ prettyShowMap_ (DMap.toMap $ outRel r) (\v -> "(" ++ prettyShowMap_rel_bps_x v ++ ")") "\n " + +prettyShowMap_ :: (Show y) => IntMap y -> (y -> String) -> String -> String +prettyShowMap_ dasMap valueShow separator + = concat $ List.intersperse separator $ map (\(k,v) -> show k ++ " -> " ++ valueShow v) + $ IntMap.toList dasMap + +prettyShowMap_rel_bps_x :: (Show a) => IntMap {- Rel -} [(a,DependencySet)] -> String +prettyShowMap_rel_bps_x dasMap + = concat $ List.intersperse ", " $ map (\(r,x_bp_s) -> (++) ("-" ++ show r ++ "-> ") $ concat $ List.intersperse ", " + $ map (\(x,bp) -> show x ++ " " ++ dsShow bp) x_bp_s + ) + $ IntMap.toList dasMap diff --git a/src/HTab/RuleId.hs b/src/HTab/RuleId.hs new file mode 100644 --- /dev/null +++ b/src/HTab/RuleId.hs @@ -0,0 +1,57 @@ +---------------------------------------------------- +-- -- +-- RuleId.hs: -- +-- Miscelaneous rule data/info, that probably -- +-- should go in Rules.hs but didn't work due to -- +-- mutually recursive modules and the 'deriving' -- +-- clause.... -- +-- -- +---------------------------------------------------- +{- +Copyright (C) HyLoRes 2002-2005 +Carlos Areces - areces@loria.fr - http://www.loria.fr/~areces +Daniel Gorin - dgorin@dc.uba.ar +Juan Heguiabehere - juanh@inf.unibz.it - http://www.inf.unibz.it/~juanh/ + +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. +-} + +module HTab.RuleId(RuleId(..)) + +where + +import Control.DeepSeq ( NFData, rnf ) + +data RuleId = R_Dia -- Diamond + | R_DiaX -- DiamondX + | R_Disj -- Disjunction + | R_SemBr -- Semantic Branching + | R_At -- Satisfaction operator (@) rule + | R_Down -- Down-arrow rule + | R_NegNom -- Negation before nominal rule + | R_Exist -- Existential modality + | R_Diff -- Difference modality + | R_Discard -- Discarding a formula + | R_Clash -- Branch clash + | R_UBlocking -- Unrestricted Blocking + | R_Merge -- Equivalence classes merge + | R_RoleInc -- Role inclusion + | R_LazyBranch -- Lazy Branching + deriving(Eq, Ord, Show) + + +instance NFData RuleId where + rnf ruleId = ruleId `seq` () diff --git a/src/HTab/Rules.hs b/src/HTab/Rules.hs new file mode 100644 --- /dev/null +++ b/src/HTab/Rules.hs @@ -0,0 +1,401 @@ +module HTab.Rules +( +Rule(..),BranchModification(..), +applicableRule, applyRule, ruleToId, +applyMod +) where + +import qualified Data.Set as Set +import qualified Data.Map as Map +import qualified Data.IntMap as IntMap +import Data.Maybe ( listToMaybe, mapMaybe ) + +import HTab.Formula( Formula(..), PrFormula(..), showLess, neg, + Dependency, DependencySet, dsUnion, dsInsert, + prefix, AccFormula(..), Rel, + Prefix, + conj, replaceVar, Prop, Literal ) +import HTab.Branch( Branch(..), createNewPref, createNewProp, createNewNomTestRelevance, + BranchInfo(..), + addFormulas, addAccFormula, + addDiaRuleCheck, addDiaXRuleCheck, + addDownRuleCheck, addDiffRuleCheck, + addParentPrefix, + reduceDisjunctionProposeLazy, doLazyBranching, + getUrfatherAndDeps, isNotBlocked, merge, + diaAlreadyDone, diaXAlreadyDone, downAlreadyDone, + ReducedDisjunct(..), getUrfather, + ScheduledRule(..), TodoList(..), + deleteUEV, insertUEV_addFormula ) +import HTab.CommandLine(CmdLineParams, UnitProp(..), lazyBranching, semBranch, unitProp, strategy, noLoopCheck) +import HTab.RuleId(RuleId(..)) +import qualified HTab.DisjSet as DS + +-- a "rule" is basically a list of modifications of the structures + +data BranchModification = BM_AddFormulas [PrFormula] + | BM_AddAccFormula AccFormula + | BM_AddDiaRuleCheck Prefix (Rel,Formula) + | BM_AddDiaXRuleCheck Prefix (Rel,Formula) + | BM_AddDownRuleCheck Prefix Formula + | BM_AddDiffRuleCheck Formula (Maybe Prop) + | BM_CreateNewPref + | BM_CreateNewProp + | BM_CreateNewNomTestRelevance Formula + | BM_AddParentPrefix Prefix Prefix + | BM_Clash DependencySet PrFormula + | BM_DeleteUEV Int + | BM_InsertUEV_addFormula (Maybe Int) DependencySet (Int -> PrFormula) + | BM_Merge Prefix DS.Pointer DependencySet + | BM_DoLazyBranch Prefix Literal [PrFormula] + +-- each rule constructor contains exactly the needed data to know the effect of the rule +data Rule = DiaRule PrFormula -- creates a prefix + | DiaXRule PrFormula Dependency + | DisjRule PrFormula [PrFormula] + | SemBrRule PrFormula [[PrFormula]] + | LazyBranchRule PrFormula Prefix Literal [PrFormula] + | AtRule PrFormula + | DownRule PrFormula + | DiffRule PrFormula Dependency + | ExistRule PrFormula -- creates a prefix + | DiscardRule PrFormula + | ClashRule DependencySet PrFormula + | MergeRule Prefix DS.Pointer DependencySet + | RoleIncRule Prefix [Rel] Prefix DependencySet + +-- from the description of a rule application, creates the list of lists of modifications to the branch +-- for certain rules, we need to look in the branch to see what modifications we do + +getMods :: Branch -> Rule -> [[BranchModification]] +getMods _ (ClashRule ds f) = [[BM_Clash ds f]] +getMods _ (MergeRule p n ds)= [[BM_Merge p n ds]] + +getMods _ (RoleIncRule p1 rs p2 ds) = [[BM_AddAccFormula (AccFormula ds r p1 p2)] | r <- rs] + +getMods br (DiaRule df@(PrFormula pr ds (Dia r f))) + = if diaAlreadyDone br df + then getMods br (DiscardRule df) + else [[BM_AddParentPrefix newPr ur, + BM_AddAccFormula acctoadd, + BM_AddFormulas [toadd], + BM_AddDiaRuleCheck pr (r,f), + BM_CreateNewPref]] + where acctoadd = AccFormula (dsUnion ds ds2) r ur newPr + toadd = PrFormula newPr ds f + newPr = getNewPref br + (ur,ds2,_) = getUrfatherAndDeps br (DS.Prefix pr) + +getMods _ (DiaRule _) = error "getMods DiaRule" + +getMods _ (DiaXRule (PrFormula pr ds (DiaX mi r ev)) dep)= + [[BM_AddFormulas [PrFormula pr ds2 ev], + BM_AddDiaXRuleCheck pr (r,ev)] + ++ case mi of { Nothing -> [] ; + Just idx -> [BM_DeleteUEV idx] + } + , + [BM_AddDiaXRuleCheck pr (r,ev), + BM_InsertUEV_addFormula mi ds2 + (\i -> PrFormula pr ds2 ((neg ev) `conj` (Dia r $ DiaX (Just i) r ev)))] + ] + where ds2 = dsInsert dep ds + +getMods _ (DiaXRule _ _)= error "getMods DiaXRule" + +getMods br (ExistRule (PrFormula _ ds (E f2))) = + [[BM_AddFormulas [toadd], + BM_CreateNewPref]] + where toadd = PrFormula newPr ds f2 + newPr = getNewPref br + +getMods _ (ExistRule _) = error "getMods ExistRule" + +getMods _ (DisjRule _ toadds) = + [[BM_AddFormulas [toadd]] | toadd <- toadds] + +getMods _ (SemBrRule _ toaddss) = + [[BM_AddFormulas toadds] | toadds <- toaddss] + +getMods _ (LazyBranchRule _ pr lit pfs) = + [[BM_DoLazyBranch pr lit pfs]] + +getMods br (AtRule (PrFormula _ ds (At n f))) = + [[BM_AddFormulas [toadd]]] + where toadd = PrFormula earliestPrefix (dsUnion ds ds2) f + (earliestPrefix,ds2,_) = getUrfatherAndDeps br (DS.Nominal n) + +getMods _ (AtRule _) = error "getMods AtRules" + + +getMods br (DownRule df@(PrFormula pr ds f@(Down v f2))) + = if downAlreadyDone br df + then getMods br (DiscardRule df) + else [[BM_CreateNewNomTestRelevance f, -- order -- what about using a monadic + BM_AddFormulas [toadd1, toadd2], -- matters -- writing for the getMods functions ? + BM_AddDownRuleCheck pr f + ]] + where toadd1 = PrFormula pr ds (replaceVar v newNom f2) + toadd2 = PrFormula pr ds $ Lit newNom + newNom = nextNom br + +getMods _ (DownRule _) = error "getMods DownRule" + +getMods br (DiffRule (PrFormula pr ds_ (D f2)) d) = + case Map.lookup f2 (dDiaRlCh br) of + Nothing -> [[BM_AddDiffRuleCheck f2 Nothing, + BM_CreateNewPref, BM_CreateNewPref, + BM_CreateNewProp, + BM_AddFormulas [PrFormula newPref1 ds f2, + PrFormula newPref2 ds f2, + PrFormula newPref1 ds ( Lit newProp), + PrFormula newPref2 ds (neg $ Lit newProp), + PrFormula pr ds (neg $ Lit newProp)] + ], + [BM_AddDiffRuleCheck f2 (Just newProp), + BM_CreateNewPref, + BM_CreateNewProp, + BM_AddFormulas [PrFormula newPref1 ds f2, + PrFormula newPref1 ds ( Lit newProp), + PrFormula pr ds (neg $ Lit newProp)] + ] + ] + where newPref1 = getNewPref br + newPref2 = newPref1 + 1 + newProp = nextProp br + Just Nothing -> [[]] + Just (Just diffProp) -> [[BM_AddFormulas [PrFormula pr ds (neg $ Lit diffProp)]]] + where ds = d `dsInsert` ds_ + +getMods _ (DiffRule _ _) = error "getMods DiffRule" + + + +getMods _ (DiscardRule _) = [[]] + + +instance Show Rule where + show (MergeRule pr po _) = "merge: " ++ show (pr,po) + show (DiaRule todelete) = "diamond: " ++ showLess todelete + show (DiaXRule todelete _) = "diamondX: " ++ 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 (DiffRule todelete _) = "D: " ++ showLess todelete + show (DiscardRule todelete) = "Discard: " ++ showLess todelete + show (ClashRule bprs f) = "Clash: " ++ show bprs ++ " " ++ show f + show (RoleIncRule p1 rs p2 _) = "Role inclusion " ++ show (p1,rs,p2) + show (LazyBranchRule todelete _ _ _) + = "Lazy Branch " ++ showLess todelete + +-- +ruleToId :: Rule -> RuleId +ruleToId r = case r of + (MergeRule _ _ _) -> R_Merge + (DiaRule _ ) -> R_Dia + (DiaXRule _ _) -> R_DiaX + (DisjRule _ _) -> R_Disj + (SemBrRule _ _) -> R_SemBr + (AtRule _ ) -> R_At + (DownRule _) -> R_Down + (ExistRule _) -> R_Exist + (DiffRule _ _) -> R_Diff + (DiscardRule _) -> R_Discard + (ClashRule _ _) -> R_Clash + (RoleIncRule _ _ _ _) -> R_RoleInc + (LazyBranchRule _ _ _ _) -> R_LazyBranch + +-- the rules application strategy is defined here: +-- the first rule is the one that will be applied at the next tableau step +applicableRule :: Branch -> CmdLineParams -> Dependency -> Maybe (Rule,TodoList,Branch) +applicableRule br clp d = + case todoList br of + Fair [] -> Nothing + Fair (sr:tl) -> Just (scheduledRuleToRule br clp d sr, Fair tl, br) + _ -> listToMaybe $ mapMaybe (ruleByChar br clp d) (strategy clp) + +scheduledRuleToRule :: Branch -> CmdLineParams -> Dependency -> ScheduledRule -> Rule +scheduledRuleToRule _ _ d (SR_Inclusion p1 rs p2 ds) = RoleIncRule p1 rs p2 (dsInsert d ds) +scheduledRuleToRule _ _ _ (SR_Merge pr po ds) = MergeRule pr po ds +scheduledRuleToRule br clp d (SR_Formula pf@(PrFormula _ _ f2)) = + case f2 of + Dis _ -> if semBranch clp then semBrRule clp pf br d else disjRule clp pf br d + Dia _ _ -> DiaRule pf + DiaX _ _ _-> diaXRule pf br d + At _ _ -> AtRule pf + Down _ _ -> DownRule pf + E _ -> ExistRule pf + D _ -> DiffRule pf d + _ -> error "scheduledRuleToRule, incorrect formula kind" + +ruleByChar :: Branch -> CmdLineParams -> Dependency -> Char -> Maybe (Rule,TodoList,Branch) +ruleByChar br clp d char = + case char of + 'n' -> applicableMergeRule + '|' -> applicableDisjRule + '<' -> applicableDiaRule + '*' -> applicableDiaXRule + '@' -> applicableAtRule + 'E' -> applicableExistRule + 'D' -> applicableDiffRule + 'b' -> applicableDownRule + 'r' -> applicableRoleIncRule + _ -> error "ruleByChar" + where + todos = todoList br + + applicableDiaRule + = do (f@(PrFormula pr _ _),new) <- Set.minView $ diaTodo todos + if noLoopCheck clp + then return (DiaRule f, todos{diaTodo = new},br) + else if diaAlreadyDone br f + then return (DiscardRule f, todos{diaTodo = new} , br ) + else if isNotBlocked br pr + then return ( DiaRule f, todos{diaTodo = new}, br ) + else let ur = getUrfather br (DS.Prefix pr) + brBlocked = br{blockedDias = IntMap.insertWith (++) ur [f] (blockedDias br)} + -- blocked formulas are added one by one to the blockedDias list. + -- a better way would be to put every formula of a given blocked prefix + -- to that list, but as we do not index todo formulas by prefix we can + -- not do it. + in + return ( DiscardRule f, todos{diaTodo = new}, brBlocked) + + applicableDiaXRule = do (f,new) <- Set.minView $ diaXTodo todos + return (diaXRule f br d, todos{diaXTodo = new},br) + + applicableAtRule = do (f,new) <- Set.minView $ atTodo todos + return (AtRule f, todos{atTodo = new},br) + + applicableDownRule = do (f,new) <- Set.minView $ downTodo todos + return (DownRule f, todos{downTodo = new},br) + + applicableExistRule = do (f,new) <- Set.minView $ existTodo todos + return (ExistRule f, todos{existTodo = new},br) + + applicableDiffRule = do (f,new) <- Set.minView $ diffTodo todos + return (DiffRule f d, todos{diffTodo = new},br) + + applicableRoleIncRule = do ((ds, p1, p2, rs),new) <- Set.minView $ roleIncTodo todos + return (RoleIncRule p1 rs p2 (dsInsert d ds), todos{roleIncTodo = new},br) + + applicableMergeRule = do ((ds,p,po),new) <- Set.minView $ mergeTodo todos + return (MergeRule p po ds, todos{mergeTodo = new},br) + + applicableDisjRule + = case unitProp clp of + Eager -> {- scan all disjuncts until one can be discarded, reduced to one disjunct or clashes -} + case mapMaybe (makeInteresting clp br d) $ Set.toList $ disjTodo todos of + ((r,pf):_) -> return (r, todos{disjTodo = Set.delete pf $ disjTodo todos},br) + [] -> regularApplicableDisjRule --todo: update counter (CurCount, MaxCount) step 10 until which space out unit propagation + _ -> regularApplicableDisjRule + + regularApplicableDisjRule + = if semBranch clp + then do (f,new) <- Set.minView $ disjTodo todos + return (semBrRule clp f br d, todos{disjTodo = new},br) + else do (f,new) <- Set.minView $ disjTodo todos + return (disjRule clp f br d, todos{disjTodo = new},br) + +makeInteresting :: CmdLineParams -> Branch -> Dependency -> PrFormula -> Maybe (Rule,PrFormula) +makeInteresting clp br d df@(PrFormula pr ds (Dis fs)) + = case reduceDisjunctionProposeLazy br pr fs of + Triviality -> Just (DiscardRule df,df) + Contradiction ds_clash -> Just (ClashRule (dsUnion ds ds_clash) df,df) + Reduced new_ds disjuncts mProposed + | Set.size disjuncts == 1 -> Just (DisjRule df ( prefix ur newDeps disjuncts ), df) + | lazyBranching clp && ur <= unblockedPrefsLim br + -> case mProposed of + Nothing -> Nothing + Just lit -> Just (LazyBranchRule df ur lit [PrFormula ur newDeps (Dis disjuncts)], df) + | otherwise -> Nothing + where newDeps = dsInsert d $ dsUnion ds new_ds + ur = getUrfather br (DS.Prefix pr) + -- TODO should not insert d if the formula was actually not changed + -- --> reduceDisjunctionProposeLazy should return a boolean + -- --> or have a constructor "Unchanged" ? + +makeInteresting _ _ _ _ = error "makeInteresting on a non disjunction" + +applyRule :: CmdLineParams -> Rule -> Branch -> TodoList -> [BranchInfo] +applyRule clp rule br_ todo + = map (applyMods clp br) (getMods br rule) + where br = br_{todoList = todo} + +applyMods :: CmdLineParams -> Branch -> [BranchModification] -> BranchInfo +applyMods clp br (hd:tl) + = case (applyMod clp br hd) of + BranchOK br2 -> applyMods clp br2 tl + si@(BranchClash _ _ _ _) -> si +applyMods _ br [] = BranchOK br + + +applyMod :: CmdLineParams -> Branch -> BranchModification -> BranchInfo +applyMod clp br (BM_AddFormulas li) = addFormulas clp br li +applyMod clp br (BM_AddAccFormula accFor) = addAccFormula clp br accFor +applyMod _ br (BM_AddDiaRuleCheck pr (r,f)) = BranchOK $ addDiaRuleCheck br pr (r,f) +applyMod _ br (BM_AddDiaXRuleCheck pr (r,f)) = BranchOK $ addDiaXRuleCheck br pr (r,f) +applyMod _ br (BM_AddDownRuleCheck pr f) = BranchOK $ addDownRuleCheck br pr f +applyMod clp br (BM_CreateNewPref) = createNewPref clp br +applyMod _ br (BM_CreateNewProp) = BranchOK $ createNewProp br +applyMod _ br (BM_CreateNewNomTestRelevance f) = BranchOK $ createNewNomTestRelevance br f +applyMod _ br (BM_AddDiffRuleCheck f mp) = BranchOK $ addDiffRuleCheck br f mp +applyMod _ br (BM_AddParentPrefix son father) = BranchOK $ addParentPrefix br son father +applyMod _ br (BM_Clash ds (PrFormula pr ds2 f)) = BranchClash br pr (dsUnion ds ds2) f +applyMod _ br (BM_DeleteUEV i) = BranchOK $ deleteUEV br i +applyMod clp br (BM_InsertUEV_addFormula mi ds ff) = insertUEV_addFormula br clp mi ds ff +applyMod clp br (BM_Merge pr p ds) = merge clp br pr ds p +applyMod _ br (BM_DoLazyBranch pr l pfs) = BranchOK $ doLazyBranching pr l pfs br +-- the actual rules and their helper functions + +-- diaX (may create a discard rule) +diaXRule :: PrFormula -> Branch -> Dependency -> Rule +diaXRule f@(PrFormula pr _ (DiaX _ r f2)) br d + = if diaXAlreadyDone br pr (r,f2) + then DiscardRule f + else DiaXRule f d + +diaXRule _ _ _ = error "diaXRule" + +-- + +getNewPref :: Branch -> Prefix +getNewPref br = lastPref br + 1 + +-- disjunction +disjRule :: CmdLineParams -> PrFormula -> Branch -> Dependency -> Rule +disjRule clp df@(PrFormula pr ds (Dis fs)) br d + = if unitProp clp == UPNo + then DisjRule df $ prefix pr (dsInsert d ds) fs + else case reduceDisjunctionProposeLazy br pr fs of + Triviality -> DiscardRule df + Contradiction ds_clash -> ClashRule (dsUnion ds ds_clash) df + Reduced new_ds disjuncts _ + -> DisjRule df (prefix pr (dsInsert d $ dsUnion ds new_ds) disjuncts) +-- todo: if only one conjunct remaining, do not add d , but still create a DisjRule +disjRule _ _ _ _ = error "disjRule" + +-- semantic branching +semBrRule :: CmdLineParams -> PrFormula -> Branch -> Dependency -> Rule -- todo : unit propagation, part 2 (b) +semBrRule clp df@(PrFormula pr ds (Dis fs)) br d + = if unitProp clp == UPNo + then SemBrRule df $ sbModList $ prefix pr (dsInsert d ds) fs + else case reduceDisjunctionProposeLazy br pr fs of + Triviality -> DiscardRule df + Contradiction ds_clash -> ClashRule (dsUnion ds ds_clash) df + Reduced new_ds disjuncts _ + -> SemBrRule df (sbModList $ prefix pr (dsInsert d $ dsUnion ds new_ds) disjuncts) +-- todo same remark as above +semBrRule _ _ _ _ = error "sembrRule" + + +sbModList :: [PrFormula] -> [[PrFormula]] +sbModList fs = go fs [] + where go :: [PrFormula] -> [PrFormula] -> [[PrFormula]] + go (hd:tl) negated = + (hd:negated):(go tl ((neg_ hd):negated)) + where neg_ (PrFormula pr ds f) = PrFormula pr ds (neg f) + go [] _ = [] + diff --git a/src/HTab/Statistics.hs b/src/HTab/Statistics.hs new file mode 100644 --- /dev/null +++ b/src/HTab/Statistics.hs @@ -0,0 +1,159 @@ +---------------------------------------------------- +-- -- +-- Statistics.hs: -- +-- Functions that collect and print out -- +-- statistics -- +-- -- +---------------------------------------------------- + +{- +Copyright (C) HyLoRes 2002-2006 +Carlos Areces - areces@loria.fr - http://www.loria.fr/~areces +Daniel Gorin - dgorin@dc.uba.ar +Juan Heguiabehere - juanh@inf.unibz.it - http://www.inf.unibz.it/~juanh/ + +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. +-} + +module HTab.Statistics +( Statistics, StatisticsState, StatisticsStateIO, + recordFiredRule, recordClosedBranch, + + printOutMetricsFinal, printOutMetrics, + + initialStatisticsStateFor, + setPrintOutInterval, + + Metric, updateStep + +) where + +import Control.Monad.State(MonadState , MonadIO, modify, unless, + gets, when) + +import qualified Control.Monad.State as State(liftIO) +import Control.DeepSeq ( NFData, rnf ) + +import Data.Map(Map) +import qualified Data.Map as Map(insertWith, toList, empty) +import Data.List ( intercalate ) + +import HTab.RuleId(RuleId(..)) + +data Statistics = Stat{metrics::[Metric], + count::Int, + step::Int} + +instance NFData Statistics where + 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 + +updateMetrics :: (Metric -> Metric) -> Statistics -> Statistics +updateMetrics f stat = let s = stat{metrics = map (f $!) (metrics stat)} + in + (rnf s) `seq` s + +updateStep :: Statistics -> Statistics +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 + +defaultStats :: Statistics +defaultStats = Stat{metrics=[closedBranches, ruleApplicationCount], + count=0, step=0} + +--------------------------- Monadic Statistics functions follow ------------------------------ + + +initialStatisticsStateFor :: (MonadState Statistics m) => (m a -> Statistics -> b) -> m a -> b +initialStatisticsStateFor f = flip f defaultStats + +setPrintOutInterval :: Int -> StatisticsState () +setPrintOutInterval i = modify $ \s -> s{step = i} + +recordFiredRule :: RuleId -> StatisticsState () +recordFiredRule rule = modify (updateMetrics $ recordFiredRuleM rule) + +recordClosedBranch :: StatisticsState () +recordClosedBranch = modify (updateMetrics recordClosedBranchM) + + +printOutMetricsFinal :: Statistics -> IO () +printOutMetricsFinal stats = + do liftIO $ putStrLn "(final statistics)" + liftIO $ printOutList (metrics stats) + +printOutMetrics :: StatisticsStateIO () +printOutMetrics = do shouldPrint <- gets needsToPrintOut + when shouldPrint $ do + liftIO $ putStr "(partial statistics: iteration " + iter <- gets count + liftIO . putStr . show $ iter + liftIO $ putStrLn ")" + ms <- gets metrics + liftIO $ printOutList ms + + +printOutList :: Show a => [a] -> IO () +printOutList ms = unless ( null ms ) $ do + let separator = "\n----------------------------------\n" + let separate sep l = intercalate sep $ map show l + putStr separator + putStr (separate separator ms) + putStr separator + +-------------------------------------------- +-- Metrics +-------------------------------------------- +data Metric = RC (Map RuleId Int) -- Rule application count + |CB !Int -- Number of closed branches + +instance NFData Metric where + rnf (CB b) = rnf b + rnf (RC m) = rnf m + +type MetricModificator = Metric -> Metric + +instance Show Metric where + show (CB x) = "Closed branches: " ++ show x + show (RC x) = "Rule applications:" ++ concatMap p (Map.toList x) + where p (i,c) = "\n " ++ show i ++ " rule: " ++ show c + + +recordFiredRuleM :: RuleId -> MetricModificator +recordFiredRuleM rule (RC m) = RC (Map.insertWith (+) rule 1 m) +recordFiredRuleM _ m = m + + +recordClosedBranchM :: MetricModificator +recordClosedBranchM (CB x) = CB (x+1) +recordClosedBranchM m = m + +ruleApplicationCount :: Metric +ruleApplicationCount = RC Map.empty + +closedBranches :: Metric +closedBranches = CB 0 + +-- + +liftIO :: (MonadIO m) => IO a -> m a +liftIO = State.liftIO diff --git a/src/HTab/Tableau.hs b/src/HTab/Tableau.hs new file mode 100644 --- /dev/null +++ b/src/HTab/Tableau.hs @@ -0,0 +1,95 @@ +module HTab.Tableau + (OpenFlag(..), tableauStart) +where + +import System.Console.CmdArgs ( whenLoud ) + +import Control.Monad.Reader(ask) +import Control.Monad.State(StateT,lift,modify) +import HTab.Statistics(updateStep,printOutMetrics, + recordClosedBranch, recordFiredRule, Statistics) +import HTab.Branch(BranchInfo(..),Branch(..),BranchMonad, BranchData(..), + unfulfilledEventualities) +import HTab.CommandLine(backjumping,CmdLineParams,configureStats) +import HTab.Rules(Rule,applyRule,applicableRule,ruleToId) +import HTab.Formula(Prefix,DependencySet,Formula,dsEmpty,dsMember,dsUnion) +import HTab.ModelGen ( Model, buildModel ) + +type Depth = Int +data OpenFlag = OPEN Model | CLOSED DependencySet + +tableauStart :: CmdLineParams -> BranchInfo -> BranchMonad OpenFlag +tableauStart clp bi = liftStats (configureStats clp) >> tableau 0 bi + +tableau :: Depth -> BranchInfo -> BranchMonad OpenFlag +tableau depth branchInfo = + do logMe + bd <- ask + debugMsg_NewSection depth + case branchInfo of + BranchClash br pr bprs f -> + do debugMsg_BranchClash br pr bprs f depth + liftStats recordClosedBranch + return (CLOSED bprs) + BranchOK br -> + do debugMsg_BranchOK br + let clp = branch_clp bd + case applicableRule br clp (depth + 1) of + Nothing -> + do debugMsg_BranchOK_saturated + return $ case unfulfilledEventualities br of + Just ds -> CLOSED ds + Nothing -> OPEN $ buildModel br + Just (rule,newTodo,newBranch) -> -- of course then merge newBranch and newTodo + do debugMsg_BranchOK_applicableRule rule + liftStats $ recordFiredRule $ ruleToId rule + case applyRule clp rule newBranch newTodo of + [newBi] -> tableau (depth + 1) newBi + bis -> chooseBranch dsEmpty bis (depth + 1) + + +chooseBranch :: DependencySet -> [BranchInfo] -> Depth -> BranchMonad OpenFlag +chooseBranch currentDepSet (hd:tl) depth = + do res <- tableau depth hd + case res of + o@(OPEN _) -> return o + CLOSED depSet -> + do bd <- ask + if (backjumping $ branch_clp bd) && (not $ dsMember depth depSet) + then return $ CLOSED depSet + else chooseBranch (dsUnion currentDepSet depSet) tl depth + +chooseBranch currentDepSet [] _ = return $ CLOSED currentDepSet + +-- + +logMe :: BranchMonad () +logMe = do liftStats printOutMetrics + liftStats $ modify updateStep + +debugMsg_NewSection :: Depth -> BranchMonad () +debugMsg_NewSection depth + = liftIO $ whenLoud $ putStrLn ("\n>> Depth " ++ show depth) + +debugMsg_BranchClash :: Branch -> Prefix -> DependencySet -> Formula -> Depth -> BranchMonad () +debugMsg_BranchClash br pr bprs f depth + = liftIO $ whenLoud $ putStrLn (show br ++ "\nClasher : " ++ show (pr,bprs,depth,f)) + +debugMsg_BranchOK :: Branch -> BranchMonad () +debugMsg_BranchOK br + = liftIO $ whenLoud $ putStrLn (show br) + +debugMsg_BranchOK_applicableRule :: Rule -> BranchMonad () +debugMsg_BranchOK_applicableRule rule + = liftIO $ whenLoud $ putStrLn ("\n>> Rule : " ++ show rule) + +debugMsg_BranchOK_saturated :: BranchMonad () +debugMsg_BranchOK_saturated + = liftIO $ whenLoud $ putStrLn ("\n>> Saturated open branch") + +liftStats :: StateT Statistics IO a -> BranchMonad a +liftStats = lift + +liftIO :: IO a -> BranchMonad a +liftIO = lift . lift + diff --git a/src/htab.hs b/src/htab.hs new file mode 100644 --- /dev/null +++ b/src/htab.hs @@ -0,0 +1,61 @@ +module Main (main) + +where + +import Control.Monad ( unless ) +import Control.Applicative ( (<$>) ) + +import System.Console.CmdArgs + +import System.IO ( hPrint, stderr ) +import System.Exit ( exitWith, ExitCode(ExitFailure) ) + +import Prelude hiding ( catch ) +import Control.Exception ( catch, SomeException ) + +import HTab.Main ( runWithParams, TaskRunFlag(..) ) +import HTab.CommandLine( defaultParams, checkParams ) + +main :: IO () +main = do r <- runCmdLineVersion + `catch` \(e::SomeException) -> do + let msg = show e + unless (msg == "ExitSuccess") $ hPrint stderr msg + exit r_RUNTIME_ERROR + -- + case r of + Nothing -> exit r_DID_NOT_RUN + Just Nothing -> exit r_TIMEOUT + Just (Just SUCCESS) -> exit r_SAT + Just (Just FAILURE) -> exit r_UNSAT + -- + where r_SAT = 1 + r_UNSAT = 2 + r_TIMEOUT = 3 + r_DID_NOT_RUN = 10 + r_RUNTIME_ERROR = 13 + +exit :: Int -> IO a +exit = exitWith . ExitFailure + +runCmdLineVersion :: IO (Maybe (Maybe TaskRunFlag)) +runCmdLineVersion = + do clp <- cmdArgs $ defaultParams &= summary header &= details gpl_tag + clpOK <- checkParams clp + if clpOK + then Just <$> runWithParams clp + else return Nothing + +header :: String +header = unlines ["HTab 1.5.4", + "G. Hoffmann, C. Areces, D.Gorin and J. Heguiabehere. (c) 2002-2010.", + "http://code.google.com/p/intohylo/"] + +gpl_tag :: [String] +gpl_tag = [ + "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."] + + diff --git a/tests/coverage.sh b/tests/coverage.sh new file mode 100644 --- /dev/null +++ b/tests/coverage.sh @@ -0,0 +1,65 @@ +#!/bin/sh + +set -x +cd ../src/ + +rm -rf htab *.o *.hi HTab/*.o HTab/*.hi *.tix ../html +ghc --make -fhpc -fglasgow-exts htab.hs + +HTAB=./htab +DATA=../examples/sat + + for i in $DATA/*; do + $HTAB --showformula -f $i + $HTAB -t 2 --fairstrategy -u -f $i + $HTAB -v --stats=10 -f $i + $HTAB -t 2 -f $i + $HTAB -t 2 --lazybranching=False -f $i + $HTAB -t 2 --eager -f $i + $HTAB -t 2 --unit-prop -f $i + $HTAB -t 2 --no-unit-prop -f $i + $HTAB -t 2 --alltransitive -f $i + $HTAB -t 2 --allreflexive -f $i + $HTAB -t 2 --allsymmetric -f $i + $HTAB -t 2 --allfunctional -f $i + $HTAB -t 2 --allinjective -f $i + $HTAB -t 2 -m mod -f $i + done + +DATA=../examples/unsat + + for i in $DATA/*; do + $HTAB --showformula -f $i + $HTAB -t 2 --fairstrategy -u -f $i + $HTAB -v --stats=10 -f $i + $HTAB -t 2 -f $i + $HTAB -t 2 --lazybranching=False -f $i + $HTAB -t 2 --eager -f $i + $HTAB -t 2 --unit-prop -f $i + $HTAB -t 2 --no-unit-prop -f $i + $HTAB -t 2 --alltransitive -f $i + $HTAB -t 2 --allreflexive -f $i + $HTAB -t 2 --allsymmetric -f $i + $HTAB -t 2 --allfunctional -f $i + $HTAB -t 2 --allinjective -f $i + $HTAB -t 2 -m mod -f $i + done + +DATA=../examples/sat_no_mod + + for i in $DATA/*; do + $HTAB --showformula -f $i + $HTAB -t 2 --fairstrategy -u -f $i + $HTAB -v --stats=10 -f $i + $HTAB -t 2 -f $i + $HTAB -t 2 --lazybranching=False -f $i + $HTAB -t 2 --eager -f $i + $HTAB -t 2 --unit-prop -f $i + $HTAB -t 2 --no-unit-prop -f $i + $HTAB -t 2 -m mod -f $i + done + +$HTAB --help +hpc markup htab --destdir=../html + +rm -rf htab htab.tix mod *.o *.hi HTab/*.o HTab/*.hi out* diff --git a/tests/test-example-formulas.hs b/tests/test-example-formulas.hs new file mode 100644 --- /dev/null +++ b/tests/test-example-formulas.hs @@ -0,0 +1,86 @@ +module Main ( main ) where + +import Data.List ( tails ) +import qualified Data.Set as Set + +import Control.Applicative ( (<$>) ) +import HyLo.Util ( sequenceUntil ) + +import System.Exit ( exitFailure ) +import System.FilePath ( () ) +import System.Directory ( getDirectoryContents ) +import System.Environment ( getArgs ) + +import HyLo.Model +import HyLo.Model.Herbrand +import HyLo.InputFile +import HyLo.Signature.String ( NomSymbol(..), PropSymbol(..), RelSymbol(..) ) + + +import HTab.CommandLine +import HTab.Main + +main :: IO () +main = + do (sat_dir, sat_no_mod_dir, unsat_dir) <- parseArgs + -- + sat_tests <- map (runExpecting Sat) <$> frmFiles sat_dir + sat_no_mod_tests <- map (runExpecting SatNoMod) <$> frmFiles sat_no_mod_dir + unsat_tests <- map (runExpecting Unsat) <$> frmFiles unsat_dir + -- + success <- and <$> sequenceUntil not (sat_tests ++ sat_no_mod_tests ++ unsat_tests) + if success + then putStrLn "SUCCESS" + else putStrLn "FAILURE" >> exitFailure + +data Expected = Sat | SatNoMod | Unsat deriving (Eq, Show) + +parseArgs :: IO (FilePath, FilePath, FilePath) +parseArgs = go =<< getArgs + where go [sd, snmd, ud] = return (sd, snmd, ud) + go _ = fail "Required args: " + +frmFiles :: FilePath -> IO [FilePath] +frmFiles dir = map (dir ) . filter (endsWith ".frm") <$> + getDirectoryContents dir + +endsWith :: String -> String -> Bool +endsWith t s = t `elem` (tails s) + +runHTab :: FilePath -> IO TaskRunFlag +runHTab f = runWithParams clp + where clp = defaultParams{filename = Just f, + maxtimeout = 20, + quietMode = True, + genModel = Just modelTmpFile} + +modelTmpFile :: String +modelTmpFile = "model.tmp" + +runExpecting :: Expected -> FilePath -> IO Bool +runExpecting exp_result file = + do putStr (file ++ "......... ") + r <- runHTab file + case (r, exp_result) of + (FAILURE, Unsat) -> putStrLn "OK!" >> return True + (FAILURE, _) -> putStrLn "FAILED! (unsat)" >> return False + (SUCCESS, SatNoMod) -> putStrLn "OK!" >> return True + (SUCCESS, Sat) -> do b <- isASatisfyingModel + if b + then do putStrLn "OK!" + return True + else do putStrLn "MODELCHECK FAILED" + return False + (SUCCESS, Unsat) -> putStrLn "FAILED! (sat)" >> return False + (TIMEOUT_ , _) -> putStrLn "FAILED! (timeout)" >> return False + -- + + where isASatisfyingModel = + do fs <- parse <$> readFile file + m <- read <$> readFile modelTmpFile :: IO M + -- + let ws = Set.toList (worlds m) + -- + return $ any (\w -> and [(m,w) |= f | f <- fs]) ws + +type M = Model NomSymbol NomSymbol PropSymbol RelSymbol