packages feed

HTab (empty) → 1.5.4

raw patch · 121 files changed

+4829/−0 lines, 121 filesdep +basedep +cmdargsdep +containerssetup-changed

Dependencies added: base, cmdargs, containers, deepseq, directory, filepath, hylolib, mtl, strict

Files

+ COPYING view
@@ -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.++    <one line to give the program's name and a brief idea of what it does.>+    Copyright (C) 19yy  <name of author>++    This program is free software; you can redistribute it and/or modify+    it under the terms of the GNU General Public License as published by+    the Free Software Foundation; either version 2 of the License, or+    (at your option) any later version.++    This program is distributed in the hope that it will be useful,+    but WITHOUT ANY WARRANTY; without even the implied warranty of+    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the+    GNU General Public License for more details.++    You should have received a copy of the GNU General Public License+    along with this program; if not, write to the Free Software+    Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.++Also add information on how to contact you by electronic and paper mail.++If the program is interactive, make it output a short notice like this+when it starts in an interactive mode:++    Gnomovision version 69, Copyright (C) 19yy name of author+    Gnomovision comes with ABSOLUTELY NO WARRANTY; for details type `show w'.+    This is free software, and you are welcome to redistribute it+    under certain conditions; type `show c' for details.++The hypothetical commands `show w' and `show c' should show the appropriate+parts of the General Public License.  Of course, the commands you use may+be called something other than `show w' and `show c'; they could even be+mouse-clicks or menu items--whatever suits your program.++You should also get your employer (if you work as a programmer) or your+school, if any, to sign a "copyright disclaimer" for the program, if+necessary.  Here is a sample; alter the names:++  Yoyodyne, Inc., hereby disclaims all copyright interest in the program+  `Gnomovision' (which makes passes at compilers) written by James Hacker.++  <signature of Ty Coon>, 1 April 1989+  Ty Coon, President of Vice++This General Public License does not permit incorporating your program into+proprietary programs.  If your program is a subroutine library, you may+consider it more useful to permit linking proprietary applications with the+library.  If this is what you want to do, use the GNU Library General+Public License instead of this License.
+ HTab.cabal view
@@ -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
+ NEWS view
@@ -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
+ Setup.lhs view
@@ -0,0 +1,4 @@+#! /usr/bin/env runhaskell++> import Distribution.Simple+> main = defaultMain
+ examples/runsat.sh view
@@ -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++
+ examples/rununsat.sh view
@@ -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+
+ examples/sat/d_sat1.frm view
@@ -0,0 +1,4 @@+signature { automatic } theory+{+A (D (P1))+}
+ examples/sat/d_sat2.frm view
@@ -0,0 +1,4 @@+signature { automatic } theory+{+B N1+}
+ examples/sat/d_sat3.frm view
@@ -0,0 +1,4 @@+signature { automatic } theory+{+A B N1+}
+ examples/sat/d_sat4.frm view
@@ -0,0 +1,4 @@+signature { automatic } theory+{+B !N1+}
+ examples/sat/d_sat5.frm view
@@ -0,0 +1,4 @@+signature { automatic } theory+{+n1 & B <>n1+}
+ examples/sat/d_sat6.frm view
@@ -0,0 +1,5 @@+signature { automatic } theory+{+n1:!n2;+n1 & B D!n1+}
+ examples/sat/d_sat7.frm view
@@ -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)))+}
+ examples/sat/down01.frm view
@@ -0,0 +1,4 @@+signature { automatic } theory+{+N2 & <>( down N3 . ( N1:(N2 & !N3)))+}
+ examples/sat/spy.frm view
@@ -0,0 +1,6 @@+signature { automatic } theory+{+down (N1 []([]( down( N2 (N1:<>(N2))))));+[]<>true;+[] (down (N1 (!<>N1)))+}
+ examples/sat/test01.frm view
@@ -0,0 +1,5 @@+signature { automatic } theory++{+ !(P1 & P1)+}
+ examples/sat/test02.frm view
@@ -0,0 +1,6 @@+signature { automatic } theory++{+ !(P1 & P1);+ P2 | P1+}
+ examples/sat/test03.frm view
@@ -0,0 +1,6 @@+signature { automatic } theory++{+ !(P1 & P1) & (P3 -> P2);+ !(!P5 ->(P3 | !!P4))+}
+ examples/sat/test04.frm view
@@ -0,0 +1,7 @@+signature { automatic } theory++{+ (P1 & P1 & P1 ) -> (P3 | P4);+ (P3 -> (!P2 | (P5 -> P6)));+ P6 | P7 | !P8+}
+ examples/sat/test05.frm view
@@ -0,0 +1,8 @@+signature { automatic } theory++{+ !(P1 & P2) <--> P7 | P3;+ P5 & P3 -> (P8 | !(P10 -> P9));+ (P3 | P6) -> (P4 | !P16);+ (P7 | !P8)+}
+ examples/sat/test06.frm view
@@ -0,0 +1,5 @@+signature { automatic } theory++{+ (N1:P1) & (N2:!P1)+}
+ examples/sat/test07.frm view
@@ -0,0 +1,7 @@+signature { automatic } theory++{+ !(P1 & P1) & (P3 -> P2);+ N1 : !(!P5 ->(P3 | !!P4));+ N2 :  (N3 :  P3)+}
+ examples/sat/test08.frm view
@@ -0,0 +1,7 @@+signature { automatic } theory++{+   (<>(<>(<>(P1 <--> P2))));+   ([]P3);+   ([](P3 -> (P5 | P2)))+}
+ examples/sat/test09.frm view
@@ -0,0 +1,4 @@+signature { automatic } theory+{+(P1 & (P1 & (P1 & P1))) & (P3 & (P2 & P1) & (P1 & (P2 & P3)))+}
+ examples/sat/test10.frm view
@@ -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)))+}
+ examples/sat/test11.frm view
@@ -0,0 +1,5 @@+signature { automatic } theory+{+<>p1 & <><>!p1 & <><><>p1 & <><><><>!p1 & <><><><><>p1 & <><><><><><>!p1;+[](p1 & [](!p1 & [](p1 & [](!p1 & [](p1 & []!p1)))))+}
+ examples/sat/test12.frm view
@@ -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)   +}
+ examples/sat/test13.frm view
@@ -0,0 +1,8 @@+signature { automatic }++theory+{+[R1](<R3>p1 v p3) <--> [R3](p3 --> <R2>!p3);+[R2](p1 --> <R2>(p1 <--> (p3 v p4 v !p5)));+[R1][R2][R3](p1 v !p3 v !p5)+}
+ examples/sat/test14.frm view
@@ -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)+}
+ examples/sat/test15.frm view
@@ -0,0 +1,7 @@+signature { automatic } theory+{+[](n1 <--> [](n2 <--> [](n3 <--> []n4)));+<>[]<>(p1 <--> p2);+[](p3 -> n1:!p1);+(n1:n2)+}
+ examples/sat/test16.frm view
@@ -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)+}
+ examples/sat/test17.frm view
@@ -0,0 +1,6 @@+signature { automatic } theory+{+[R1](<R3>[R1]p3 --> n1 --> n2:n1 --> n3:n3:n4);+n1 --> ([R1] p3 v <R3><R1>[R2] (p2 v [R1]p4));+(n1:n3) v (n3:n1) <--> [R1](<R3>(n1 --> n3 ))+}
+ examples/sat/test18.frm view
@@ -0,0 +1,6 @@+signature { automatic } theory+{+([R1] p1 )<--> ([R3]p1 <--> <R2>[R1]!p3);+n1: [R2]<R1>p1 <--> p2 --> p3;+false --> (false <--> n1:n3)+}
+ examples/sat/test19.frm view
@@ -0,0 +1,10 @@+signature { automatic } theory+{+p1 --> (false --> <R1>[R2]p3);+[R2]<R1>(p1 <--> [R2](p1 v p2 v p3));+[R1][R1][R2](p1 --> [R1](p2 <--> <R2>p1));+(!p1 v !p3) --> (n1:n2);+<R1>!p1 v !p3;+<R1><R2>(!p1 v !p3) <--> <R3>(!p1 v !p3);+[R2][R1](n1:!p1 v !p3)+}
+ examples/sat/test20.frm view
@@ -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))+}
+ examples/sat/test21.frm view
@@ -0,0 +1,10 @@+signature { automatic } theory+{+n1:(n3:<R1>p3 v (n4 --> <R3> p3));+[R1]<R3>(n3:<R3>[R3] (p1 v p2 v p3) <--> n4:n2);+n1:n2 v n2:n1;+[R2](<R1>p1 <--> <R3>p4);+<R2>([R1] (p2 v !p4)) v [R3](p3 --> <R2>(<R2>!p2));+(<R2>(P32 v P31) & <R2>(!P32 v !P31)) <--> p32+}                                                                                             +
+ examples/sat/test22.frm view
@@ -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+}
+ examples/sat/test23.frm view
@@ -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)))))) +}
+ examples/sat/test24.frm view
@@ -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 +}
+ examples/sat/test25.frm view
@@ -0,0 +1,5 @@+signature { automatic } theory+{+n1:p1 v n2:p2 v n3:p3 v n4:p4;+[]!p1 & []!p2 & []!p3 & []!p4+}
+ examples/sat/test26.frm view
@@ -0,0 +1,5 @@+signature { automatic } theory+{+(n1: <>[]!p1) | (n1: []<>p2) | (n2: p3);+(n1: <>n3) | (n2: p1)+}
+ examples/sat/test27.frm view
@@ -0,0 +1,4 @@+signature { automatic } theory+{+A (p1 ^ []!p1)+}
+ examples/sat/test28.frm view
@@ -0,0 +1,5 @@+signature { automatic } theory+{+A []p1;+!p1+}
+ examples/sat/test29.frm view
@@ -0,0 +1,5 @@+signature { automatic } theory+{+A[](([]!p1) v (<>p1));+n1:<><>p1+}
+ examples/sat/test30.frm view
@@ -0,0 +1,4 @@+signature { automatic } theory+{+A(!N0 v !N1)+}
+ examples/sat/test31.frm view
@@ -0,0 +1,4 @@+signature { automatic } theory+{+A(N0 : true)+}
+ examples/sat/test32.frm view
@@ -0,0 +1,4 @@+signature { automatic } theory+{+A(N0 & E true)+}
+ examples/sat/test33.frm view
@@ -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)+}
+ examples/sat/test34.frm view
@@ -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)+}
+ examples/sat/test35.frm view
@@ -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)+}
+ examples/sat/test36.frm view
@@ -0,0 +1,7 @@+signature { automatic } theory+{+N1;+<>true;+[]<>true;+[]N1+}
+ examples/sat/test37.frm view
@@ -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))+}
+ examples/sat/test38.frm view
@@ -0,0 +1,8 @@+% had bad model building at some point with chain blocking++signature { automatic } theory++{+A<><>!N1;+[](P1 v N1) & []!P1+}
+ examples/sat/test39.frm view
@@ -0,0 +1,7 @@+signature { automatic } theory+{+P1  v N2:N1;+!N2 v (!N2 & B false);+!P1 v <>false;+N1  v []true+}
+ examples/sat/test40.frm view
@@ -0,0 +1,4 @@+begin+N0;+<>( N0 & ((<>true) & ([] <>N0:[]N0)))+end
+ examples/sat/trclos1.frm view
@@ -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)))))++}
+ examples/sat_no_mod/all1.frm view
@@ -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:<love>marie;++ bob:[lovedBy]naive;++ alice:<youngerThan>marie;+ marie:<youngerThan>bob;+ bob:<youngerThan>jean;++ unknown:<parentOf>alice++}++query (satisfiable? , "out1") {+ alice:<canManipulate>jean+}++query (satisfiable? , "out2") {+ unknown:<parentOf>jean+}++query (retrieve , "retrieve1") {+ <youngerThan>jean+}+
+ examples/unsat/d_unsat1.frm view
@@ -0,0 +1,4 @@+signature { automatic } theory+{+A D N1+}
+ examples/unsat/d_unsat2.frm view
@@ -0,0 +1,6 @@+signature { automatic } theory+{+N1 & B N1;+E P1;+E !P1+}
+ examples/unsat/d_unsat3.frm view
@@ -0,0 +1,5 @@+signature { automatic } theory+{+N1:!N2;+E B !(N1 v N2)+}
+ examples/unsat/d_unsat4.frm view
@@ -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)+}
+ examples/unsat/d_unsat5.frm view
@@ -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)))+}
+ examples/unsat/d_unsat6.frm view
@@ -0,0 +1,4 @@+signature { automatic } theory+{+<>([]!N0 ^ B false)+}
+ examples/unsat/fun_inj1.frm view
@@ -0,0 +1,13 @@+signature {+propositions { p }+nominals { n,m }+relations { r : { functional } }+}++theory++{+ n:<r><r><r><r><r>p;+ m:<r><r><r><r><r>!p;+ n:m+}
+ examples/unsat/fun_inj2.frm view
@@ -0,0 +1,14 @@+signature {+propositions { p }+nominals { n,a,b }+relations { r,+            s : { inverseof r, functional } }+}++theory++{+ a:<r><r><r><r><r><r><r><r><r><r><r>n;+ b:<r><r><r><r><r><r><r><r><r><r><r>n;+ a:!b+}
+ examples/unsat/interpol.frm view
@@ -0,0 +1,6 @@+% Interpolation formula++signature { automatic } theory+{+!((<>p1 & <>!p1) --> (([](p2 --> N1) --> <>!p2)))+}
+ examples/unsat/role_equality1.frm view
@@ -0,0 +1,15 @@+signature {+propositions { p }+nominals { }+relations { student,+            course,+            tag : { equals {student, course}} }+}++theory++{+ <tag>p;+ [student]!p;+ [course]!p+}
+ examples/unsat/role_inclusion1.frm view
@@ -0,0 +1,13 @@+signature {+propositions { p }+nominals { }+relations { s, t, r : { reflexive, subsetof {s,t}} }+}++theory++{+ <r>p;+ [s]!p;+ [t]!p+}
+ examples/unsat/symmetry1.frm view
@@ -0,0 +1,14 @@+signature {+propositions { p }+nominals { n,m }+relations { s : {symmetric}, t : {trclosureof s} }+}++theory++{+ n:<s><s><s><s>m;+ n:p;+ m:[t]!p++}
+ examples/unsat/test01.frm view
@@ -0,0 +1,5 @@+signature { automatic } theory++{+ P1 & !P1+}
+ examples/unsat/test02.frm view
@@ -0,0 +1,7 @@+signature { automatic } theory++{+ P1 | P2 | P3 | P4;+ !P1 | !P2;+ !(P1 --> ((P3 <--> P4) --> P1))+}
+ examples/unsat/test03.frm view
@@ -0,0 +1,7 @@+signature { automatic } theory+{++P1 |  P2 ;+P1 | !P2;+!P1+}
+ examples/unsat/test04.frm view
@@ -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)))))+}
+ examples/unsat/test05.frm view
@@ -0,0 +1,7 @@+signature { automatic } theory++{+ !((P1 & P2) -> ( ((P4 <--> !P7) | !P9) --> ((P1 & P2) | (P2 | !P2)) ));+ P1 | P2;+ P4 <--> ! P5+}
+ examples/unsat/test06.frm view
@@ -0,0 +1,7 @@+signature { automatic } theory++{+ N1 : (<R1> N2);+ N2 : P1;+ N1 : [R1] !P1+}
+ examples/unsat/test07.frm view
@@ -0,0 +1,5 @@+signature { automatic } theory++{+  !(([R1](P1 --> P2)) --> (([R1] P1) --> ([R1] P2)))+}
+ examples/unsat/test08.frm view
@@ -0,0 +1,5 @@+signature { automatic } theory++{+  !([R1](P1 | !P1))+}
+ examples/unsat/test09.frm view
@@ -0,0 +1,5 @@+signature { automatic } theory++{+  !(([R1](P1 & P2)) -> (([R1]P1) & ([R1]P2)))+}
+ examples/unsat/test10.frm view
@@ -0,0 +1,5 @@+signature { automatic } theory++{+   !(((<R1>P1) | (<R1>P2)) --> (<R1>(P1 | P2)))+}
+ examples/unsat/test11.frm view
@@ -0,0 +1,4 @@+signature { automatic } theory+{+!(N1 : N1)+}
+ examples/unsat/test12.frm view
@@ -0,0 +1,6 @@+signature { automatic } theory+{+N1: N2;+N1: [R1] P1;+N2: <R1> !P1+}
+ examples/unsat/test13.frm view
@@ -0,0 +1,4 @@+signature { automatic } theory+{+!([R1](P1 --> P2) --> [R1]P1 --> [R1]P2)+}
+ examples/unsat/test14.frm view
@@ -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)))))) +}
+ examples/unsat/test15.frm view
@@ -0,0 +1,4 @@+signature { automatic } theory+{+!(<>(n1 & <><><><><>(n1:n2) & (<>(p1 --> [](p3 <--> <>p1))) & <><><><><>(n2:n3)) & <>(n3 & p2) --> <>((<>(p1 --> [](p3 <--> <>p1))) & p2))+}
+ examples/unsat/test16.frm view
@@ -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)))))+}    +
+ examples/unsat/test17.frm view
@@ -0,0 +1,5 @@+signature { automatic } theory+{+!(n1:(n1 & n2:(n2 & ([](p1 -->((!(p1 -> (p2 --> p1))) v p2)) --> ([]p1 --> []p2)))))+}    +
+ examples/unsat/test18.frm view
@@ -0,0 +1,6 @@+signature { automatic } theory+{+n1:<>(n1 v (p1 ^ !p1));+n1:((<>true v (p1 --> (p2 --> p1)) v []false) --> p1);+!(n1:<>p1) +}
+ examples/unsat/test19.frm view
@@ -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)+}
+ examples/unsat/test20.frm view
@@ -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)+}
+ examples/unsat/test21.frm view
@@ -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)))) +}
+ examples/unsat/test22.frm view
@@ -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+}
+ examples/unsat/test23.frm view
@@ -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+}    +
+ examples/unsat/test24.frm view
@@ -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))))+}    ++
+ examples/unsat/test25.frm view
@@ -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))))+}    ++
+ examples/unsat/test28.frm view
@@ -0,0 +1,6 @@+signature { automatic } theory+{+n1:<>(n1 v (p1 & !p1));+n1:(<>true  --> p1);+!(n1:<>p1) +}
+ examples/unsat/test29.frm view
@@ -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)))))))))))))))))+}
+ examples/unsat/test32.frm view
@@ -0,0 +1,8 @@+signature { automatic } theory+{+n2:n1;+n1 v <R1>(n1:(n2 & !p1));+<R1>(n1:p1);+!n2 +}+
+ examples/unsat/test33.frm view
@@ -0,0 +1,4 @@+signature { automatic } theory+{+A (p1 ^ <>!p1)+}
+ examples/unsat/test34.frm view
@@ -0,0 +1,5 @@+signature { automatic } theory+{+A(P1 v P2);+N1:(!P1 & !P2)+}
+ examples/unsat/test35.frm view
@@ -0,0 +1,5 @@+signature { automatic } theory+{+down(N1 !N1)+}+
+ examples/unsat/test36.frm view
@@ -0,0 +1,4 @@+signature { automatic } theory+{+!((down (N1 dia (N1 ^ p1) )) --> p1)+}
+ examples/unsat/test37.frm view
@@ -0,0 +1,10 @@+signature { automatic } theory+{+n3:[R3](down (N1 [R1]([R1]( down( N2 (N1:<R1>N2)))))) ;+n3:<R3>n1;+n3:<R3>n2;+n3:<R3>n3;+n1:<R1>n2;+n2:<R1>n3;+n1:!<R1>n3+}
+ examples/unsat/test38.frm view
@@ -0,0 +1,5 @@+signature { automatic } theory+{+p1 v <><><><>p1 v down(N1 <>(N1:[]p1));+A !p1+}
+ examples/unsat/test39.frm view
@@ -0,0 +1,15 @@+signature {++propositions { p }+nominals     { n}+relations { r : {functional},+            s : {inverseof r} }++}++theory+{++E (p & <s><s>n) & E (!p & <s><s>n)++}
+ examples/unsat/test40.frm view
@@ -0,0 +1,14 @@+signature {++propositions { p }+nominals     { n}+relations { r : {functional} }++}++theory+{++n:<r><r><r>( p & n:<r><r><r>!p)++}
+ src/HTab/Base.hs view
@@ -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
+ src/HTab/Branch.hs view
@@ -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+
+ src/HTab/CommandLine.hs view
@@ -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<Db|*r"++checkParams :: CmdLineParams -> 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
+ src/HTab/DMap.hs view
@@ -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+
+ src/HTab/DisjSet.hs view
@@ -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.+
+ src/HTab/Formula.hs view
@@ -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
+ src/HTab/Main.hs view
@@ -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+
+ src/HTab/ModelGen.hs view
@@ -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
+ src/HTab/Relations.hs view
@@ -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
+ src/HTab/RuleId.hs view
@@ -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>+            | R_DiaX    -- DiamondX <r*>+            | 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` ()
+ src/HTab/Rules.hs view
@@ -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 [] _ = []+
+ src/HTab/Statistics.hs view
@@ -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
+ src/HTab/Tableau.hs view
@@ -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+
+ src/htab.hs view
@@ -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."]++
+ tests/coverage.sh view
@@ -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*
+ tests/test-example-formulas.hs view
@@ -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: <sat dir> <sat no model dir> <unsat dir>"++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